Changeset 2570 for src/joint/lineariseProof.ma
 Timestamp:
 Jan 5, 2013, 1:41:13 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/lineariseProof.ma
r2559 r2570 17 17 include "joint/Traces.ma". 18 18 include "joint/semanticsUtils.ma". 19 include "common/ExtraMonads.ma". 20 (* 21 !!!SPOSTATO IN extraGlobalenvs.ma!!!! 19 22 20 23 include alias "common/PositiveMap.ma". … … 56 59 @add_globals_functions_miss @add_functs_functions_miss normalize // 57 60 qed. 61 *) 62 63 (* !!!spostato in semantics.ma ed aggiunto un include a extraGlobalenvs.ma!!! 58 64 59 65 lemma fetch_internal_function_no_minus_one : … … 68 74 cases (symbol_for_block ???) normalize // 69 75 qed. 70 76 77 *) 78 79 (*spostato in ExtraMonads.ma 80 71 81 lemma bind_option_inversion_star: 72 82 ∀A,B: Type[0].∀P : Prop.∀f: option A. ∀g: A → option B. ∀y: B. … … 109 119 ; 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 110 120 }. 121 122 *) 111 123 112 124 (*definition IO_preserve : ∀O,I.MonadFunctRel (IOMonad O I) (IOMonad O I) ≝ … … 123 135 qed.*) 124 136 137 (* spostato in ExtraMonads.ma 125 138 definition res_preserve : MonadFunctRel Res Res ≝ 126 139 mk_MonadFunctRel ?? … … 192 205 FR … H 193 206 (f x y) (g (F x prf1) (G y prf2)). 207 *) 194 208 195 209 definition graph_prog_params ≝ … … 340 354 @opt_safe_elim #is' whd in ⊢ (??%%→?); #EQ destruct(EQ) % qed. 341 355 356 (* spostato in ExtraMonads.ma 357 342 358 lemma res_preserve_error : ∀X,Y,P,F,e,n.res_preserve X Y P F (Error … e) n. 343 359 #X #Y #P #F #e #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed. … … 351 367 lemma opt_safe_eq : ∀A,m,x,prf.m = Some A x → opt_safe A m prf = x. 352 368 #A #m #x #prf @opt_safe_elim #x' #EQ >EQ #EQ' destruct % qed. 369 *) 353 370 354 371 lemma sigma_is_pop_commute : … … 449 466 ∀z.contents bc1 z = contents bc2 z) → 450 467 nextblock m1 = nextblock m2 → m1 = m2. 468 (* spostato in ExtraMonads.ma 451 469 452 470 lemma opt_preserve_none : ∀X,Y,P,F,n.opt_preserve X Y P F (None ?) n. 453 471 #X #Y #P #F #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed. 472 *) 454 473 455 474 lemma beloadv_sigma_commute: … … 705 724 λp,graph_prog,f.«f, if_propagate … (pi2 … f)». 706 725 *) 726 727 (* spostato in ExtraMonads.ma 728 707 729 lemma m_list_map_All_ok : 708 730 ∀M : MonadProps.∀X,Y,f,l. … … 717 739 @m_return_bind 718 740 qed. 741 *) 719 742 720 743 definition helper_def_store__commute : … … 1557 1580 qed. 1558 1581 1582 (* 1583 spostato in ExtraMonads.ma 1559 1584 1560 1585 lemma res_eq_from_opt : ∀A,m,a. … … 1571 1596 ] 1572 1597 qed. 1573 1598 *) 1574 1599 lemma sigma_pc_exit : 1575 1600 ∀p,p',graph_prog,sigma,pc,prf. … … 1986 2011 %{H5} %{H3} %{H2} @H1 1987 2012 qed. 1988 2013 (* spostato in ExtraMonads.ma 1989 2014 lemma opt_to_res_preserve : ∀X,Y,P,F,m,n,e1,e2. 1990 2015 opt_preserve X Y P F m n → … … 2006 2031 >EQ % 2007 2032 qed. 2008 2033 *) 2009 2034 lemma eval_seq_no_pc_sigma_commute : 2010 2035 ∀p,p',graph_prog.
Note: See TracChangeset
for help on using the changeset viewer.