Changeset 2281 for src/ASM/Test.ma

Timestamp:

Jul 31, 2012, 2:22:35 AM (8 years ago)

Author:

sacerdot

Message:

...

File:

• src/ASM/Test.ma (modified) (5 diffs)

src/ASM/Test.ma

@@ -445 +445 @@
 qed.
 
-lemma set_low_internal_ram_status_of_pseudo_status:
- ∀cm,sigma,policy,M,s,s',ram.
-  s' = status_of_pseudo_status M cm s sigma policy →
-  set_low_internal_ram (BitVectorTrie Byte 16)
-  (code_memory_of_pseudo_assembly_program cm sigma policy)
-  s'
-  (low_internal_ram_of_pseudo_low_internal_ram M sigma ram)
-  = status_of_pseudo_status M cm
-    (set_low_internal_ram pseudo_assembly_program cm s ram) sigma policy.
-  #cm #sigma #policy #M #s #s' #ram #s_refl >s_refl //
-qed.
-
 (* Real axiom ATM *)
 axiom insert_low_internal_ram_of_pseudo_low_internal_ram:
@@ -573 +561 @@
 qed.
 
+definition internal_pseudo_address_map_equal_up_to_low ≝
+ λM,M': internal_pseudo_address_map. \snd M = \snd M' ∧ \snd (\fst M) = \snd (\fst M').
+
+lemma set_low_internal_ram_status_of_pseudo_status2:
+ ∀cm,sigma,policy,M,M',s,s',ram,ram'.
+  internal_pseudo_address_map_equal_up_to_low M M' →
+  s' = status_of_pseudo_status M' cm s sigma policy →
+  ram'=internal_ram_of_pseudo_internal_ram sigma ram (\fst (\fst M)) →
+  set_low_internal_ram (BitVectorTrie Byte 16)
+  (code_memory_of_pseudo_assembly_program cm sigma policy)
+  s'
+  ram'
+  = status_of_pseudo_status M cm
+    (set_low_internal_ram pseudo_assembly_program cm s ram) sigma policy.
+  #cm #sigma #policy #M #M' #s #s' #ram #ram' #M_refl #s_refl >s_refl #ram_refl >ram_refl
+  cases M' in M_refl; * #low' #high' #accA' cases M * #low #high #accA #H cases H
+  #accA_refl #high_refl destruct whd in ⊢ (??%%); @split_eq_status %
+qed.
+
+lemma set_low_internal_ram_status_of_pseudo_status:
+ ∀cm,sigma,policy,M,s,s',ram,ram'.
+  s' = status_of_pseudo_status M cm s sigma policy →
+  ram'=internal_ram_of_pseudo_internal_ram sigma ram (\fst (\fst M)) →
+  set_low_internal_ram (BitVectorTrie Byte 16)
+  (code_memory_of_pseudo_assembly_program cm sigma policy)
+  s'
+  ram'
+  = status_of_pseudo_status M cm
+    (set_low_internal_ram pseudo_assembly_program cm s ram) sigma policy.
+  #cm #sigma #policy #M #s #s' #ram #ram' @set_low_internal_ram_status_of_pseudo_status2
+  % %
+qed.
+
 lemma set_register_status_of_pseudo_status:
  ∀M,sigma,policy,cm,s,s',r,v,v'.
@@ -586 +607 @@
  whd in match set_register; normalize nodelta
  >bit_address_of_register_status_of_pseudo_status
+ @set_low_internal_ram_status_of_pseudo_status try %
  >(insert_low_internal_ram_status_of_pseudo_status … v_ok)
- @set_low_internal_ram_status_of_pseudo_status %
+ cases M * #low #high #accA %
 qed.
 
@@ -1945 +1967 @@
 *)
 
-definition internal_pseudo_address_map_equal_up_to_low ≝
- λM,M': internal_pseudo_address_map. \snd M = \snd M' ∧ \snd (\fst M) = \snd (\fst M').
-
-lemma set_low_internal_ram_status_of_pseudo_status:
- ∀cm,sigma,policy,M,M',s,s',ram,ram'.
-  internal_pseudo_address_map_equal_up_to_low M M' →
-  s' = status_of_pseudo_status M' cm s sigma policy →
-  ram'=internal_ram_of_pseudo_internal_ram sigma ram (\fst (\fst M)) →
-  set_low_internal_ram (BitVectorTrie Byte 16)
-  (code_memory_of_pseudo_assembly_program cm sigma policy)
-  s'
-  ram'
-  = status_of_pseudo_status M cm
-    (set_low_internal_ram pseudo_assembly_program cm s ram) sigma policy.
-  #cm #sigma #policy #M #M' #s #s' #ram #ram' #M_refl #s_refl >s_refl #ram_refl >ram_refl
-  cases M' in M_refl; * #low' #high' #accA' cases M * #low #high #accA #H cases H
-  #accA_refl #high_refl destruct whd in ⊢ (??%%); @split_eq_status %
-qed.
 
 definition internal_pseudo_address_map_equal_up_to_high ≝
@@ -2021 +2025 @@
     whd in match high_internal_ram_of_pseudo_high_internal_ram; normalize nodelta
     @insert_internal_ram_of_pseudo_internal_ram assumption
-  | @(set_low_internal_ram_status_of_pseudo_status … 〈low',high',accA'〉 〈low,high,accA〉)
+  | @(set_low_internal_ram_status_of_pseudo_status2 … 〈low',high',accA'〉 〈low,high,accA〉)
     try @refl try assumption
     whd in match status_of_pseudo_status; normalize nodelta