Changeset 911 for src/ASM/AssemblyProof.ma

Timestamp:

Jun 9, 2011, 10:38:21 AM (9 years ago)

Author:

sacerdot

Message:

Type of set_code_memory generalized.

File:

• src/ASM/AssemblyProof.ma (modified) (2 diffs)

src/ASM/AssemblyProof.ma

@@ -1523 +1523 @@
 qed.
 *)
+
+axiom execute_1_pseudo_instruction_preserves_code_memory:
+ ∀ticks_of,ps.
+  code_memory … (execute_1_pseudo_instruction ticks_of ps) = code_memory … ps.
+
 (*
 lemma execute_code_memory_unchanged:
@@ -1576 +1581 @@
   match status_of_pseudo_status ps' with [ None ⇒ True | Some s'' ⇒
   let s' ≝ execute_1 s in
-   s = s'']].
+   s' = s'']].
  #ticks_of #ps
- whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
+ whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ λ_.%])
+ whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ λ_.match % with [ _ ⇒ ? | _ ⇒ ? ]])
+ >execute_1_pseudo_instruction_preserves_code_memory
  cases (assembly (code_memory pseudo_assembly_program ps)) [%] * #cm #costs whd
+ change with (? (set_code_memory ?? ps (load_code_memory (\fst 〈cm,costs〉))) = ?)
  whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
  generalize in match (sig2 … (execute_1_pseudo_instruction' ticks_of ps))