Changeset 945 for src

Timestamp:

Jun 13, 2011, 11:15:31 AM (10 years ago)

Author:

mulligan

Message:

more small changes to proof of main thrm

File:

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

src/ASM/AssemblyProof.ma

@@ -2067 +2067 @@
  //
 qed.
+
+lemma blah:
+  ∀p: pseudo_instruction.
+  ∀m: pseudo_internal_address_map.
+  ∀s: PseudoStatus.
+  ∀arg: Byte.
+    next_internal_pseudo_address_map0 p m s (DIRECT arg) = Some ? →
+      get_arg_8 (next_internal_pseudo_address_map0 p (internal_ram ? s) s (DIRECT arg)) =
+      get_arg_8 (internal_ram ? s) (DIRECT arg).
+
+map_address0 ... (DIRECT arg) = Some .. →
+  get_arg_8 (map_address0 ... (internal_ram ...) (DIRECT arg) =
+  get_arg_8 (internal_ram ...) (DIRECT arg)
+
+((if addressing_mode_ok M ps ACC_A∧addressing_mode_ok M ps (DIRECT ARG2) 
+                     then Some internal_pseudo_address_map M 
+                     else None internal_pseudo_address_map )
+                    =Some internal_pseudo_address_map M')
 
 lemma main_thm:
@@ -2227 +2245 @@
               @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]]
   (*|5: (* Call *)*) *)
-  | (* Instruction *) -pi; *; normalize nodelta;
+  | (* Instruction *) -pi;  whd in ⊢ (? → ??%? → ?) *; normalize nodelta;
     [1,2,3: (* ADD, ADDC, SUBB *) #arg1 #arg2 #MAP #H1 #H2 #EQ %[1,3,5:@1]
        normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)