Changeset 945


Ignore:
Timestamp:
Jun 13, 2011, 11:15:31 AM (8 years ago)
Author:
mulligan
Message:

more small changes to proof of main thrm

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r944 r945  
    20672067 //
    20682068qed.
     2069
     2070lemma blah:
     2071  ∀p: pseudo_instruction.
     2072  ∀m: pseudo_internal_address_map.
     2073  ∀s: PseudoStatus.
     2074  ∀arg: Byte.
     2075    next_internal_pseudo_address_map0 p m s (DIRECT arg) = Some ? →
     2076      get_arg_8 (next_internal_pseudo_address_map0 p (internal_ram ? s) s (DIRECT arg)) =
     2077      get_arg_8 (internal_ram ? s) (DIRECT arg).
     2078
     2079map_address0 ... (DIRECT arg) = Some .. →
     2080  get_arg_8 (map_address0 ... (internal_ram ...) (DIRECT arg) =
     2081  get_arg_8 (internal_ram ...) (DIRECT arg)
     2082
     2083((if addressing_mode_ok M ps ACC_A∧addressing_mode_ok M ps (DIRECT ARG2) 
     2084                     then Some internal_pseudo_address_map M 
     2085                     else None internal_pseudo_address_map )
     2086                    =Some internal_pseudo_address_map M')
    20692087
    20702088lemma main_thm:
     
    22272245              @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]]
    22282246  (*|5: (* Call *)*) *)
    2229   | (* Instruction *) -pi; *; normalize nodelta;
     2247  | (* Instruction *) -pi;  whd in ⊢ (? → ??%? → ?) *; normalize nodelta;
    22302248    [1,2,3: (* ADD, ADDC, SUBB *) #arg1 #arg2 #MAP #H1 #H2 #EQ %[1,3,5:@1]
    22312249       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
Note: See TracChangeset for help on using the changeset viewer.