Changeset 1035


Ignore:
Timestamp:
Jun 22, 2011, 11:06:43 PM (8 years ago)
Author:
sacerdot
Message:

Main theorem (broken because of dependent types) almost restored.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r1015 r1035  
    19791979          SFR_SP sp2)
    19801980        pbu)).
     1981
     1982theorem main_thm:
     1983 ∀M,M',ps,pol.
     1984  next_internal_pseudo_address_map M ps = Some … M' →
     1985   ∃n.
     1986      execute n (status_of_pseudo_status M ps pol)
     1987    = status_of_pseudo_status M' (execute_1_pseudo_instruction (ticks_of (code_memory … ps) pol) ps) ?.
     1988 [2: >execute_1_pseudo_instruction_preserves_code_memory @pol]
     1989 #M #M' #ps #pol #SAFE
     1990 cut
     1991  (∀ps'.
     1992    ∀prf:ps'=execute_1_pseudo_instruction (ticks_of (code_memory … ps) pol) ps.
     1993    ∃n. execute n (status_of_pseudo_status M ps pol) = status_of_pseudo_status M' ps' ?)
     1994 [ >prf >execute_1_pseudo_instruction_preserves_code_memory @pol |3: #K @(K ? (refl …))]
     1995 #ps' #EQ
     1996 whd in ⊢ (??(λ_.??(??%)?))
     1997 change with
     1998  (∃n.
     1999    execute n
     2000     (set_low_internal_ram ?
     2001       (set_high_internal_ram ?
     2002         (set_program_counter ?
     2003           (set_code_memory ?? ps (load_code_memory ?))
     2004          (sigma ? pol (program_counter ? ps)))
     2005        (high_internal_ram_of_pseudo_high_internal_ram M ?))
     2006      (low_internal_ram_of_pseudo_low_internal_ram M ?))
     2007   = set_low_internal_ram ?
     2008      (set_high_internal_ram ?
     2009        (set_program_counter ?
     2010          (set_code_memory ?? ? (load_code_memory ?))
     2011         (sigma ???)) ?) ?)
     2012 >EQ whd in match eq_rect_Type0_r normalize nodelta
     2013 >execute_1_pseudo_instruction_preserves_code_memory normalize nodelta
     2014 generalize in match EQ -EQ;
     2015 generalize in match (refl … (code_memory pseudo_assembly_program ps))
     2016 generalize in match pol generalize in ⊢ (∀_.??%? → ?)
     2017 * #preamble #instr_list #pol #EQ1 generalize in match pol -pol <EQ1 #pol #EQps' <EQps'
     2018 
     2019
    19812020
    19822021lemma main_thm0:
Note: See TracChangeset for help on using the changeset viewer.