Changeset 3563
Legend:
 Unmodified
 Added
 Removed

LTS/Vm.ma
r3552 r3563 3 3 include "../src/utilities/option.ma". 4 4 include "basics/jmeq.ma". 5 6 lemma bind_inversion : ∀A,B : Type[0].∀m : option A.7 ∀f : A → option B.∀y : B.8 ! x ← m; f x = return y →9 ∃ x.(m = return x) ∧ (f x = return y).10 #A #B * [ #a] #f #y normalize #EQ [destruct]11 %{a} %{(refl …)} //12 qed.13 5 14 6 record assembler_params : Type[1] ≝ 
LTS/frame_variable_pass.ma
r3561 r3563 15 15 include "Simulation.ma". 16 16 include "variable.ma". 17 include alias "arithmetics/nat.ma". 17 18 18 19 definition update_fun : ∀A : DeqSet.∀B : Type[0].(A → B) → A → B → A → B ≝ … … 61 62 ]. 62 63 64 definition environment_rel : (variable → variable) → environment → activation_frame → Prop ≝ 65 λmap,st1,st2. 66 All … (λx.let 〈v,val〉 ≝ x in read_frame … st2 (to_shift + (map v)) O = return val) 67 st1. 68 63 69 definition store_rel : (variable → variable) → store_t → frame_store_t → Prop ≝ 64 70 λmap,st1,st2. 65 All2 … (λel1,el2.\snd el1 = \snd el2 ∧ All … (λx.let 〈v,val〉 ≝ x in read_frame … (\fst el2) (to_shift + (map v)) O = return val)66 (\fst el1))st1 (\fst st2) ∧ \snd st2 = 〈O,O〉.71 All2 … (λel1,el2.\snd el1 = \snd el2 ∧ environment_rel map (\fst el1) (\fst el2)) 72 st1 (\fst st2) ∧ \snd st2 = 〈O,O〉. 67 73 68 74 definition trans_imp_prog : (variable → variable) → Program imp_env_params imp_instr_params flat_labels → … … 84 90 cont … s2 = foldr … (λx,rem.〈\fst x,(trans_imp_instr (\snd x) map)〉 :: rem) (nil ?) (cont … s1)) 85 91 (λ_.λ_.True). 92 93 lemma eval_cond_ok: 94 ∀m: variable → variable. 95 ∀e: expr. 96 let e' ≝ map_exp e m in 97 ∀env: environment. 98 ∀env': activation_frame. 99 environment_rel m env env' → 100 ∀val. 101 sem_expr env e = Some … val → 102 frame_sem_expr env' e' = Some … val. 103 #m #e elim e 104 [ #v #env elim env 105 [ #env' #_ #val #abs normalize in abs; destruct 106  * #var #val #tl #IH #env' * #RF #Htl #val' 107 whd in ⊢ (??%? → ?); inversion (?==?) #Hv_var normalize nodelta 108 [ #Hval_val' destruct >(\P Hv_var) assumption 109  #Hread_tl @IH // assumption ]] 110  normalize // 111 *: #e1 #e2 #IH1 #IH2 #env #env' #Rel #v 112 change with (!x ← ?; ? = return ?) in match (sem_expr ?? = Some ??); 113 #H cases (bind_inversion ????? H) H #v1 * #He1 114 #H cases (bind_inversion ????? H) H #v2 * #He2 115 #H normalize in H; destruct 116 change with (m_bind ?????) in ⊢ (??%?); 117 >(IH1 … He1) // >(IH2 … He2) // ] 118 qed. 86 119 87 120 definition simulation_imp_frame ≝ 
LTS/utils.ma
r3554 r3563 17 17 include "../src/ASM/Util.ma". 18 18 include "../src/utilities/option.ma". 19 20 lemma bind_inversion : ∀A,B : Type[0].∀m : option A. 21 ∀f : A → option B.∀y : B. 22 ! x ← m; f x = return y → 23 ∃ x.(m = return x) ∧ (f x = return y). 24 #A #B * [ #a] #f #y normalize #EQ [destruct] 25 %{a} %{(refl …)} // 26 qed. 19 27 20 28 (*NO DUPLICATES in lists*)
Note: See TracChangeset
for help on using the changeset viewer.