Changeset 919 for src/ASM/AssemblyProof.ma
- Timestamp:
- Jun 9, 2011, 2:15:32 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r916 r919 1587 1587 lemma main_thm: 1588 1588 ∀ticks_of. 1589 ∀ps: PseudoStatus. 1590 match status_of_pseudo_status ps with [ None ⇒ True | Some s ⇒ 1591 let ps' ≝ execute_1_pseudo_instruction ticks_of ps in 1592 match status_of_pseudo_status ps' with [ None ⇒ True | Some s'' ⇒ 1593 let s' ≝ execute_1 s in 1594 s' = s'']]. 1595 #ticks_of #ps 1596 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ λ_.%]) 1597 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ λ_.match % with [ _ ⇒ ? | _ ⇒ ? ]]) 1589 ∀ps,s,s''. 1590 status_of_pseudo_status ps = Some … s → 1591 status_of_pseudo_status (execute_1_pseudo_instruction ticks_of ps) = Some … s'' → 1592 execute_1 s = s''. 1593 #ticks_of #ps #s #s'' whd in ⊢ (??%? → ??%? → ?) 1598 1594 >execute_1_pseudo_instruction_preserves_code_memory 1599 generalize in match (fetch_assembly_pseudo2 (code_memory … ps)) 1600 cases (build_maps (code_memory pseudo_assembly_program ps)) 1601 cases (assembly (code_memory pseudo_assembly_program ps)) [%] * #cm #costs whd 1602 change with (execute_1 (set_program_counter ? (set_code_memory ?? ps (load_code_memory (\fst 〈cm,costs〉))) ?) = ?) 1603 change with (? = set_program_counter ? (set_code_memory ?? (execute_1_pseudo_instruction ticks_of ps) (load_code_memory (\fst 〈cm,costs〉))) ?) 1604 whd in ⊢ (??%?) 1595 cases (assembly (code_memory … ps)) [#abs @⊥ normalize in abs; destruct (abs)] 1596 * #assembled #costs whd in ⊢ (??%? → ??%? → ?) 1597 #H1 generalize in match (option_destruct_Some ??? H1) -H1; #H1 <H1 -H1; 1598 #H2 generalize in match (option_destruct_Some ??? H2) -H2; #H2 <H2 -H2; 1599 change with 1600 (execute_1 (set_program_counter ? (set_code_memory ?? ps (load_code_memory assembled)) ?) 1601 = set_program_counter ? (set_code_memory ?? (execute_1_pseudo_instruction ticks_of ps) (load_code_memory assembled)) ?)
Note: See TracChangeset
for help on using the changeset viewer.