Ignore:
Timestamp:
Jun 9, 2011, 2:15:32 PM (8 years ago)
Author:
sacerdot
Message:

Back to a readable statement.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r916 r919  
    15871587lemma main_thm:
    15881588 ∀ticks_of.
    1589  ∀ps: PseudoStatus.
    1590   match status_of_pseudo_status ps with [ None ⇒ True | Some s ⇒
    1591   let ps' ≝ execute_1_pseudo_instruction ticks_of ps in
    1592   match status_of_pseudo_status ps' with [ None ⇒ True | Some s'' ⇒
    1593   let s' ≝ execute_1 s in
    1594    s' = s'']].
    1595  #ticks_of #ps
    1596  whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ λ_.%])
    1597  whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ λ_.match % with [ _ ⇒ ? | _ ⇒ ? ]])
     1589 ∀ps,s,s''.
     1590  status_of_pseudo_status ps = Some … s →
     1591  status_of_pseudo_status (execute_1_pseudo_instruction ticks_of ps) = Some … s'' →
     1592   execute_1 s = s''.
     1593 #ticks_of #ps #s #s'' whd in ⊢ (??%? → ??%? → ?)
    15981594 >execute_1_pseudo_instruction_preserves_code_memory
    1599  generalize in match (fetch_assembly_pseudo2 (code_memory … ps))
    1600  cases (build_maps (code_memory pseudo_assembly_program ps))
    1601  cases (assembly (code_memory pseudo_assembly_program ps)) [%] * #cm #costs whd
    1602  change with (execute_1 (set_program_counter ? (set_code_memory ?? ps (load_code_memory (\fst 〈cm,costs〉))) ?) = ?)
    1603  change with (? = set_program_counter ? (set_code_memory ?? (execute_1_pseudo_instruction ticks_of ps) (load_code_memory (\fst 〈cm,costs〉))) ?)
    1604  whd in ⊢ (??%?)
     1595 cases (assembly (code_memory … ps)) [#abs @⊥ normalize in abs; destruct (abs)]
     1596 * #assembled #costs whd in ⊢ (??%? → ??%? → ?)
     1597 #H1 generalize in match (option_destruct_Some ??? H1) -H1; #H1 <H1 -H1;
     1598 #H2 generalize in match (option_destruct_Some ??? H2) -H2; #H2 <H2 -H2;
     1599 change with
     1600  (execute_1 (set_program_counter ? (set_code_memory ?? ps (load_code_memory assembled)) ?)
     1601   = set_program_counter ? (set_code_memory ?? (execute_1_pseudo_instruction ticks_of ps) (load_code_memory assembled)) ?)
Note: See TracChangeset for help on using the changeset viewer.