Changeset 2447


Ignore:
Timestamp:
Nov 9, 2012, 4:01:12 PM (7 years ago)
Author:
piccolo
Message:

All axioms opened so far and that must be closed here have been
closed.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/lineariseProof.ma

    r2446 r2447  
    148148qed.
    149149
    150 axiom sigma_pc_commute:
     150lemma sigma_pc_commute:
    151151 ∀p,p',graph_prog,s1,prf.
    152152 sigma_pc_of_status p p' graph_prog (choose_sigma p p' graph_prog) s1 prf =
     
    155155  (pc (lin_prog_params p p' (linearise p graph_prog))
    156156   (linearise_status_fun p p' graph_prog (choose_sigma p p' graph_prog) s1 prf)).
     157#p #p' #prog #s #prf whd in ⊢ (??%%); change with (? = nat_of_bitvector ??);
     158whd in match (pc … (linearise_status_fun …));
     159>nat_of_bitvector_bitvector_of_nat_inverse //
     160cases daemon (* CSC: Paolo, you must prove this additional invariant! *)
     161qed.
    157162
    158163definition linearise_status_rel:
     
    170175qed.
    171176
    172 axiom fetch_function_sigma_commute:
     177(* To be added to common/Globalenvs, it strenghtens
     178   find_funct_ptr_transf *)
     179lemma
     180  find_funct_ptr_transf_eq:
     181    ∀A,B,V,iV. ∀p: program A V. ∀transf: (∀vs. A vs → B vs).
     182    ∀b: block.
     183    find_funct_ptr ? (globalenv … iV (transform_program … p transf)) b =
     184     m_map ???
     185      (transf …)
     186      (find_funct_ptr ? (globalenv … iV p) b).
     187 #A #B #V #iV #p #transf #b inversion (find_funct_ptr ???) in ⊢ (???%);
     188 [ cases daemon (* TODO in Globalenvs.ma *)
     189 | #f #H >(find_funct_ptr_transf A B … H) // ]
     190qed.
     191
     192lemma fetch_function_sigma_commute:
    173193 ∀p,p',graph_prog,sigma,st1.
    174194 ∀prf:well_formed_status ??? sigma st1.
     
    188208    (ev_genv (graph_prog_params p p' graph_prog))
    189209    (pc (graph_prog_params p p' graph_prog) st1)).
     210#p #p' #prog #sigma #st #prf whd in match fetch_function; normalize nodelta
     211whd in match function_of_block; normalize nodelta
     212>(find_funct_ptr_transf_eq … (λglobals.transf_fundef … (linearise_int_fun … globals)) …)
     213cases (find_funct_ptr ???) // * //
     214qed.
    190215
    191216lemma stm_at_sigma_commute:
Note: See TracChangeset for help on using the changeset viewer.