theory AnalBinds imports "Terms" "HOLCF-Utils" "Env" begin locale ExpAnalysis = fixes exp :: "exp ⇒ 'a::cpo → 'b::pcpo" begin fun AnalBinds :: "heap ⇒ (var ⇒ 'a⇩⊥) → (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