Theory EvalHeap

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:subsetD[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