Ignore:
Timestamp:
Jan 5, 2013, 1:41:13 PM (7 years ago)
Author:
piccolo
Message:

ERTLtoERTLptr in place

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/lineariseProof.ma

    r2559 r2570  
    1717include "joint/Traces.ma".
    1818include "joint/semanticsUtils.ma".
     19include "common/ExtraMonads.ma".
     20(*
     21!!!SPOSTATO IN extraGlobalenvs.ma!!!!
    1922
    2023include alias "common/PositiveMap.ma".
     
    5659@add_globals_functions_miss @add_functs_functions_miss normalize //
    5760qed.
     61*)
     62
     63(* !!!spostato in semantics.ma ed aggiunto un include a extraGlobalenvs.ma!!!
    5864
    5965lemma fetch_internal_function_no_minus_one :
     
    6874  cases (symbol_for_block ???) normalize //
    6975qed.
    70    
     76
     77*)
     78
     79(*spostato in ExtraMonads.ma
     80
    7181lemma bind_option_inversion_star:
    7282  ∀A,B: Type[0].∀P : Prop.∀f: option A. ∀g: A → option B. ∀y: B.
     
    109119  ; m_frel_ext : ∀X,Y,P,F,G.(∀x,prf1,prf2.F x prf1 = G x prf2) → ∀u,v.m_frel X Y P F u v → m_frel X Y P G u v
    110120  }.
     121
     122*)
    111123
    112124(*definition IO_preserve : ∀O,I.MonadFunctRel (IOMonad O I) (IOMonad O I) ≝
     
    123135qed.*)
    124136
     137(* spostato in ExtraMonads.ma
    125138definition res_preserve : MonadFunctRel Res Res ≝
    126139  mk_MonadFunctRel ??
     
    192205  FR … H
    193206    (f x y) (g (F x prf1) (G y prf2)).
     207*)
    194208
    195209definition graph_prog_params ≝
     
    340354@opt_safe_elim #is' whd in ⊢ (??%%→?); #EQ destruct(EQ) % qed.
    341355
     356(* spostato in ExtraMonads.ma
     357
    342358lemma res_preserve_error : ∀X,Y,P,F,e,n.res_preserve X Y P F (Error … e) n.
    343359#X #Y #P #F #e #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed.
     
    351367lemma opt_safe_eq : ∀A,m,x,prf.m = Some A x → opt_safe A m prf = x.
    352368#A #m #x #prf @opt_safe_elim #x' #EQ >EQ #EQ' destruct % qed.
     369*)
    353370
    354371lemma sigma_is_pop_commute :
     
    449466      ∀z.contents bc1 z = contents bc2 z) →
    450467  nextblock m1 = nextblock m2 → m1 = m2.
     468(* spostato in ExtraMonads.ma
    451469
    452470lemma opt_preserve_none : ∀X,Y,P,F,n.opt_preserve X Y P F (None ?) n.
    453471#X #Y #P #F #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed.
     472*)
    454473
    455474lemma beloadv_sigma_commute:
     
    705724λp,graph_prog,f.«f, if_propagate … (pi2 … f)».
    706725*)
     726
     727(* spostato in ExtraMonads.ma
     728
    707729lemma m_list_map_All_ok :
    708730  ∀M : MonadProps.∀X,Y,f,l.
     
    717739    @m_return_bind
    718740qed.
     741*)
    719742
    720743definition helper_def_store__commute :
     
    15571580qed.
    15581581
     1582(*
     1583spostato in ExtraMonads.ma
    15591584
    15601585lemma res_eq_from_opt : ∀A,m,a.
     
    15711596]
    15721597qed.
    1573 
     1598*)
    15741599lemma sigma_pc_exit :
    15751600  ∀p,p',graph_prog,sigma,pc,prf.
     
    19862011%{H5} %{H3} %{H2} @H1
    19872012qed.
    1988 
     2013(* spostato in ExtraMonads.ma
    19892014lemma opt_to_res_preserve : ∀X,Y,P,F,m,n,e1,e2.
    19902015       opt_preserve X Y P F m n →
     
    20062031>EQ %
    20072032qed.
    2008 
     2033*)
    20092034lemma eval_seq_no_pc_sigma_commute :
    20102035 ∀p,p',graph_prog.
Note: See TracChangeset for help on using the changeset viewer.