theory "EvalHeap" imports "AList-Utils" "Env" "../Nominal2/Nominal2" "HOLCF-Utils" begin subsubsection {* Conversion from heaps to environments *} fun evalHeap :: "('var × 'exp) list ⇒ ('exp ⇒ 'value::{pure,pcpo}) ⇒ 'var ⇒ 'value" where "evalHeap [] _ = ⊥" | "evalHeap ((x,e)#h) eval = (evalHeap h eval) (x := eval e)" lemma cont2cont_evalHeap[simp, cont2cont]: "(⋀ e . e ∈ snd ` set h ⟹ cont (λρ. eval ρ e)) ⟹ cont (λ ρ. evalHeap h (eval ρ))" by(induct h, auto) lemma evalHeap_eqvt[eqvt]: "π ∙ evalHeap h eval = evalHeap (π ∙ h) (π ∙ eval)" by (induct h) (auto simp add:fun_upd_eqvt simp del: fun_upd_apply) lemma edom_evalHeap_subset:"edom (evalHeap h eval) ⊆ domA h" by (induct h eval rule:evalHeap.induct) (auto dest:set_mp[OF edom_fun_upd_subset] simp del: fun_upd_apply) lemma evalHeap_cong[fundef_cong]: "⟦ heap1 = heap2 ; (⋀ e. e ∈ snd ` set heap2 ⟹ eval1 e = eval2 e) ⟧ ⟹ evalHeap heap1 eval1 = evalHeap heap2 eval2" by (induct heap2 eval2 arbitrary:heap1 rule:evalHeap.induct, auto) lemma lookupEvalHeap: assumes "v ∈ domA h" shows "(evalHeap h f) v = f (the (map_of h v))" using assms by (induct h f rule: evalHeap.induct) auto lemma lookupEvalHeap': assumes "map_of Γ v = Some e" shows "(evalHeap Γ f) v = f e" using assms by (induct Γ f rule: evalHeap.induct) auto lemma lookupEvalHeap_other[simp]: assumes "v ∉ domA Γ" shows "(evalHeap Γ f) v = ⊥" using assms by (induct Γ f rule: evalHeap.induct) auto lemma env_restr_evalHeap_noop: "domA h ⊆ S ⟹ env_restr S (evalHeap h eval) = evalHeap h eval" apply (rule ext) apply (case_tac "x ∈ S") apply (auto simp add: lookupEvalHeap intro: lookupEvalHeap_other) done lemma env_restr_evalHeap_same[simp]: "env_restr (domA h) (evalHeap h eval) = evalHeap h eval" by (simp add: env_restr_evalHeap_noop) lemma evalHeap_cong': "⟦ (⋀ x. x ∈ domA heap ⟹ eval1 (the (map_of heap x)) = eval2 (the (map_of heap x))) ⟧ ⟹ evalHeap heap eval1 = evalHeap heap eval2" apply (rule ext) apply (case_tac "x ∈ domA heap") apply (auto simp add: lookupEvalHeap) done lemma lookupEvalHeapNotAppend[simp]: assumes "x ∉ domA Γ" shows "(evalHeap (Γ@h) f) x = evalHeap h f x" using assms by (induct Γ, auto) lemma evalHeap_delete[simp]: "evalHeap (delete x Γ) eval = env_delete x (evalHeap Γ eval)" by (induct Γ) auto lemma evalHeap_mono: "x ∉ domA Γ ⟹ evalHeap Γ eval ⊑ evalHeap ((x, e) # Γ) eval" apply simp apply (rule fun_belowI) apply (case_tac "xa ∈ domA Γ") apply (case_tac "xa = x") apply auto done subsubsection {* Reordering lemmas *} lemma evalHeap_reorder: assumes "map_of Γ = map_of Δ" shows "evalHeap Γ h = evalHeap Δ h" proof (rule ext) from assms have *: "domA Γ = domA Δ" by (metis dom_map_of_conv_domA) fix x show "evalHeap Γ h x = evalHeap Δ h x" using assms(1) * apply (cases "x ∈ domA Γ") apply (auto simp add: lookupEvalHeap) done qed lemma evalHeap_reorder_head: assumes "x ≠ y" shows "evalHeap ((x,e1)#(y,e2)#Γ) eval = evalHeap ((y,e2)#(x,e1)#Γ) eval" by (rule evalHeap_reorder) (simp add: fun_upd_twist[OF assms]) lemma evalHeap_reorder_head_append: assumes "x ∉ domA Γ" shows "evalHeap ((x,e)#Γ@Δ) eval = evalHeap (Γ @ ((x,e)#Δ)) eval" by (rule evalHeap_reorder) (simp, metis assms dom_map_of_conv_domA map_add_upd_left) lemma evalHeap_subst_exp: assumes "eval e = eval e'" shows "evalHeap ((x,e)#Γ) eval = evalHeap ((x,e')#Γ) eval" by (simp add: assms) end