theory AnalBinds
imports Launchbury.Terms "Launchbury.HOLCF-Utils" Launchbury.Env
begin

locale ExpAnalysis =
  fixes exp :: "exp → 'a::cpo → 'b::pcpo"
begin

fun AnalBinds :: "heap → (var → 'a_\<bottom>) → (var → 'b)"
  where "AnalBinds [] = (Λ ae. ⊥)"
      | "AnalBinds ((x,e)#Γ) = (Λ ae. (AnalBinds Γ⋅ae)(x := fup⋅(exp e)⋅(ae x)))"

lemma AnalBinds_Nil_simp[simp]: "AnalBinds []⋅ae = ⊥" by simp

lemma AnalBinds_Cons[simp]:
  "AnalBinds ((x,e)#Γ)⋅ae = (AnalBinds Γ⋅ae)(x := fup⋅(exp e)⋅(ae x))" 
  by simp

lemmas AnalBinds.simps[simp del]

lemma AnalBinds_not_there: "x ∉ domA Γ ==> (AnalBinds Γ⋅ae) x = ⊥"
  by (induction Γ rule: AnalBinds.induct) auto
 
lemma AnalBinds_cong:
  assumes "ae f|` domA Γ = ae' f|` domA Γ"
  shows "AnalBinds Γ⋅ae = AnalBinds Γ⋅ae'"
using env_restr_eqD[OF assms]
by (induction Γ rule: AnalBinds.induct) (auto split: if_splits)

lemma AnalBinds_lookup: "(AnalBinds Γ⋅ae) x = (case map_of Γ x of Some e → fup⋅(exp e)⋅(ae x) | None → ⊥)"
  by (induction Γ rule: AnalBinds.induct) auto

lemma AnalBinds_delete_bot: "ae x = ⊥ ==> AnalBinds (delete x Γ)⋅ae = AnalBinds Γ⋅ae"
  by (auto simp add: AnalBinds_lookup split:option.split simp add: delete_conv)

lemma AnalBinds_delete_below: "AnalBinds (delete x Γ)⋅ae ⊑ AnalBinds Γ⋅ae"
  by (auto intro: fun_belowI simp add: AnalBinds_lookup split:option.split)

lemma AnalBinds_delete_lookup[simp]: "(AnalBinds (delete x Γ)⋅ae) x = ⊥"
  by (auto  simp add: AnalBinds_lookup split:option.split)

lemma AnalBinds_delete_to_fun_upd: "AnalBinds (delete x Γ)⋅ae = (AnalBinds Γ⋅ae)(x := ⊥)"
  by (auto  simp add: AnalBinds_lookup split:option.split)
 
lemma edom_AnalBinds: "edom (AnalBinds Γ⋅ae) ⊆ domA Γ ∩ edom ae"
  by (induction Γ rule: AnalBinds.induct) (auto  simp add: edom_def)

end

end