Changeset 2281


Ignore:
Timestamp:
Jul 31, 2012, 2:22:35 AM (7 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Test.ma

    r2279 r2281  
    445445qed.
    446446
    447 lemma set_low_internal_ram_status_of_pseudo_status:
    448  ∀cm,sigma,policy,M,s,s',ram.
    449   s' = status_of_pseudo_status M cm s sigma policy →
    450   set_low_internal_ram (BitVectorTrie Byte 16)
    451   (code_memory_of_pseudo_assembly_program cm sigma policy)
    452   s'
    453   (low_internal_ram_of_pseudo_low_internal_ram M sigma ram)
    454   = status_of_pseudo_status M cm
    455     (set_low_internal_ram pseudo_assembly_program cm s ram) sigma policy.
    456   #cm #sigma #policy #M #s #s' #ram #s_refl >s_refl //
    457 qed.
    458 
    459447(* Real axiom ATM *)
    460448axiom insert_low_internal_ram_of_pseudo_low_internal_ram:
     
    573561qed.
    574562
     563definition internal_pseudo_address_map_equal_up_to_low ≝
     564 λM,M': internal_pseudo_address_map. \snd M = \snd M' ∧ \snd (\fst M) = \snd (\fst M').
     565
     566lemma set_low_internal_ram_status_of_pseudo_status2:
     567 ∀cm,sigma,policy,M,M',s,s',ram,ram'.
     568  internal_pseudo_address_map_equal_up_to_low M M' →
     569  s' = status_of_pseudo_status M' cm s sigma policy →
     570  ram'=internal_ram_of_pseudo_internal_ram sigma ram (\fst (\fst M)) →
     571  set_low_internal_ram (BitVectorTrie Byte 16)
     572  (code_memory_of_pseudo_assembly_program cm sigma policy)
     573  s'
     574  ram'
     575  = status_of_pseudo_status M cm
     576    (set_low_internal_ram pseudo_assembly_program cm s ram) sigma policy.
     577  #cm #sigma #policy #M #M' #s #s' #ram #ram' #M_refl #s_refl >s_refl #ram_refl >ram_refl
     578  cases M' in M_refl; * #low' #high' #accA' cases M * #low #high #accA #H cases H
     579  #accA_refl #high_refl destruct whd in ⊢ (??%%); @split_eq_status %
     580qed.
     581
     582lemma set_low_internal_ram_status_of_pseudo_status:
     583 ∀cm,sigma,policy,M,s,s',ram,ram'.
     584  s' = status_of_pseudo_status M cm s sigma policy →
     585  ram'=internal_ram_of_pseudo_internal_ram sigma ram (\fst (\fst M)) →
     586  set_low_internal_ram (BitVectorTrie Byte 16)
     587  (code_memory_of_pseudo_assembly_program cm sigma policy)
     588  s'
     589  ram'
     590  = status_of_pseudo_status M cm
     591    (set_low_internal_ram pseudo_assembly_program cm s ram) sigma policy.
     592  #cm #sigma #policy #M #s #s' #ram #ram' @set_low_internal_ram_status_of_pseudo_status2
     593  % %
     594qed.
     595
    575596lemma set_register_status_of_pseudo_status:
    576597 ∀M,sigma,policy,cm,s,s',r,v,v'.
     
    586607 whd in match set_register; normalize nodelta
    587608 >bit_address_of_register_status_of_pseudo_status
     609 @set_low_internal_ram_status_of_pseudo_status try %
    588610 >(insert_low_internal_ram_status_of_pseudo_status … v_ok)
    589  @set_low_internal_ram_status_of_pseudo_status %
     611 cases M * #low #high #accA %
    590612qed.
    591613
     
    19451967*)
    19461968
    1947 definition internal_pseudo_address_map_equal_up_to_low ≝
    1948  λM,M': internal_pseudo_address_map. \snd M = \snd M' ∧ \snd (\fst M) = \snd (\fst M').
    1949 
    1950 lemma set_low_internal_ram_status_of_pseudo_status:
    1951  ∀cm,sigma,policy,M,M',s,s',ram,ram'.
    1952   internal_pseudo_address_map_equal_up_to_low M M' →
    1953   s' = status_of_pseudo_status M' cm s sigma policy →
    1954   ram'=internal_ram_of_pseudo_internal_ram sigma ram (\fst (\fst M)) →
    1955   set_low_internal_ram (BitVectorTrie Byte 16)
    1956   (code_memory_of_pseudo_assembly_program cm sigma policy)
    1957   s'
    1958   ram'
    1959   = status_of_pseudo_status M cm
    1960     (set_low_internal_ram pseudo_assembly_program cm s ram) sigma policy.
    1961   #cm #sigma #policy #M #M' #s #s' #ram #ram' #M_refl #s_refl >s_refl #ram_refl >ram_refl
    1962   cases M' in M_refl; * #low' #high' #accA' cases M * #low #high #accA #H cases H
    1963   #accA_refl #high_refl destruct whd in ⊢ (??%%); @split_eq_status %
    1964 qed.
    19651969
    19661970definition internal_pseudo_address_map_equal_up_to_high ≝
     
    20212025    whd in match high_internal_ram_of_pseudo_high_internal_ram; normalize nodelta
    20222026    @insert_internal_ram_of_pseudo_internal_ram assumption
    2023   | @(set_low_internal_ram_status_of_pseudo_status … 〈low',high',accA'〉 〈low,high,accA〉)
     2027  | @(set_low_internal_ram_status_of_pseudo_status2 … 〈low',high',accA'〉 〈low,high,accA〉)
    20242028    try @refl try assumption
    20252029    whd in match status_of_pseudo_status; normalize nodelta
Note: See TracChangeset for help on using the changeset viewer.