Changeset 919 for src/ASM/AssemblyProof.ma

Timestamp:

Jun 9, 2011, 2:15:32 PM (10 years ago)

Author:

sacerdot

Message:

Back to a readable statement.

File:

• src/ASM/AssemblyProof.ma (modified) (1 diff)

src/ASM/AssemblyProof.ma

@@ -1587 +1587 @@
 lemma main_thm:
  ∀ticks_of.
- ∀ps: PseudoStatus.
-  match status_of_pseudo_status ps with [ None ⇒ True | Some s ⇒
-  let ps' ≝ execute_1_pseudo_instruction ticks_of ps in
-  match status_of_pseudo_status ps' with [ None ⇒ True | Some s'' ⇒
-  let s' ≝ execute_1 s in
-   s' = s'']].
- #ticks_of #ps
- whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ λ_.%])
- whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ λ_.match % with [ _ ⇒ ? | _ ⇒ ? ]])
+ ∀ps,s,s''.
+  status_of_pseudo_status ps = Some … s →
+  status_of_pseudo_status (execute_1_pseudo_instruction ticks_of ps) = Some … s'' →
+   execute_1 s = s''.
+ #ticks_of #ps #s #s'' whd in ⊢ (??%? → ??%? → ?)
  >execute_1_pseudo_instruction_preserves_code_memory
- generalize in match (fetch_assembly_pseudo2 (code_memory … ps))
- cases (build_maps (code_memory pseudo_assembly_program ps))
- cases (assembly (code_memory pseudo_assembly_program ps)) [%] * #cm #costs whd
- change with (execute_1 (set_program_counter ? (set_code_memory ?? ps (load_code_memory (\fst 〈cm,costs〉))) ?) = ?)
- change with (? = set_program_counter ? (set_code_memory ?? (execute_1_pseudo_instruction ticks_of ps) (load_code_memory (\fst 〈cm,costs〉))) ?)
- whd in ⊢ (??%?)
+ cases (assembly (code_memory … ps)) [#abs @⊥ normalize in abs; destruct (abs)]
+ * #assembled #costs whd in ⊢ (??%? → ??%? → ?)
+ #H1 generalize in match (option_destruct_Some ??? H1) -H1; #H1 <H1 -H1;
+ #H2 generalize in match (option_destruct_Some ??? H2) -H2; #H2 <H2 -H2;
+ change with
+  (execute_1 (set_program_counter ? (set_code_memory ?? ps (load_code_memory assembled)) ?)
+   = set_program_counter ? (set_code_memory ?? (execute_1_pseudo_instruction ticks_of ps) (load_code_memory assembled)) ?)