 Timestamp:
 May 26, 2011, 2:16:36 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r846 r847 9 9 definition eject : ∀A.∀P: A → Prop.(Σx:A.P x) → A ≝ λA,P,c.match c with [ dp w p ⇒ w]. 10 10 11 coercion inject : ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ inject on a:? to Σx:?.?.12 coercion eject : ∀A.∀P:A → Prop.∀c:Σx:A.P x.A ≝ eject on _c:Σx:?.? to ?.11 coercion inject nocomposites: ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ inject on a:? to Σx:?.?. 12 coercion eject nocomposites: ∀A.∀P:A → Prop.∀c:Σx:A.P x.A ≝ eject on _c:Σx:?.? to ?. 13 13 14 14 axiom VOID: Type[0]. 15 15 axiom assert_false: VOID. 16 definition bigbang: ∀A:Type[0]. ∀P:A → Prop. False → VOID → Σx:A.P x.17 #A # P #abs cases abs18 qed. 19 20 (*coercion bigbang : ∀A.∀P:A → Prop.False → ∀v:VOID.Σx:A.P x ≝ bigbang on _v:VOID to Σx:?.?.*)16 definition bigbang: ∀A:Type[0].False → VOID → A. 17 #A #abs cases abs 18 qed. 19 20 (*coercion bigbang nocomposites: ∀A:Type[0].False → ∀v:VOID.A ≝ bigbang on _v:VOID to ?.*) 21 21 22 22 lemma sig2: ∀A.∀P:A → Prop. ∀p:Σx:A.P x. P (eject … p). … … 71 71 axiom is_prefix: ∀A:Type[0]. list A → list A → Prop. 72 72 73 (* 73 74 definition build_maps' ≝ 74 75 λpseudo_program. … … 118 119 3: % [@ ([ ])] % [2: %  (* DOABLE *)] 119 120  120 121 122 121 *) 123 122 124 123 let rec encoding_check (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word) … … 130 129 hd = byte ∧ encoding_check code_memory new_pc final_pc tl 131 130 ]. 132 133 axiom sigma': pseudo_assembly_program → Word → Word.134 131 135 132 definition assembly_specification: … … 198 195 (p3_latch … ps) 199 196 (clock … ps)) ]. 200 (* 197 201 198 definition write_at_stack_pointer': 202 199 ∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝ … … 218 215 set_high_internal_ram ? s memory. 219 216 [ cases l0 % 220 2,3,4,5: cases not_implemented (* CSC: ???? normalize repeat (@ le_S_S) @ le_O_n *) 221 ] 217 2,3,4,5: normalize repeat (@ le_S_S) @ le_O_n ] 222 218 qed. 223 219 … … 254 250  <(sig2 … l7) whd in ⊢ (??? (??%)) <(sig2 … l5) % 255 251  256  (*CSC: ??? *)257  (*CSC: ??? *)258 252  % 259 253 ]
Note: See TracChangeset
for help on using the changeset viewer.