Changeset 3563 for LTS/frame_variable_pass.ma
- Timestamp:
- Jun 16, 2015, 4:00:03 PM (6 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
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 ≝
Note: See TracChangeset
for help on using the changeset viewer.