theory ArityAnalysisAbinds
imports ArityAnalysisSig
begin
context ArityAnalysis
begin
subsubsection {* Lifting arity analysis to recursive groups *}
definition ABind :: "var ⇒ exp ⇒ (AEnv → AEnv)"
where "ABind v e = (Λ ae. fup⋅(Aexp e)⋅(ae v))"
lemma ABind_eq[simp]: "ABind v e ⋅ ae = 𝒜⇧⊥⇘ae v⇙ e"
unfolding ABind_def by (simp add: cont_fun)
fun ABinds :: "heap ⇒ (AEnv → AEnv)"
where "ABinds [] = ⊥"
| "ABinds ((v,e)#binds) = ABind v e ⊔ ABinds (delete v binds)"
lemma ABinds_strict[simp]: "ABinds Γ⋅⊥=⊥"
by (induct Γ rule: ABinds.induct) auto
lemma Abinds_reorder1: "map_of Γ v = Some e ⟹ ABinds Γ = ABind v e ⊔ ABinds (delete v Γ)"
by (induction Γ rule: ABinds.induct) (auto simp add: delete_twist)
lemma ABind_below_ABinds: "map_of Γ v = Some e ⟹ ABind v e ⊑ ABinds Γ"
by (metis "HOLCF-Join-Classes.join_above1" ArityAnalysis.Abinds_reorder1)
lemma Abinds_reorder: "map_of Γ = map_of Δ ⟹ ABinds Γ = ABinds Δ"
proof (induction Γ arbitrary: Δ rule: ABinds.induct)
case 1 thus ?case by simp
next
case (2 v e Γ Δ)
from `map_of ((v, e) # Γ) = map_of Δ`
have "(map_of ((v, e) # Γ))(v := None) = (map_of Δ)(v := None)" by simp
hence "map_of (delete v Γ) = map_of (delete v Δ)" unfolding delete_set_none by simp
hence "ABinds (delete v Γ) = ABinds (delete v Δ)" by (rule 2)
moreover
from `map_of ((v, e) # Γ) = map_of Δ`
have "map_of Δ v = Some e" by (metis map_of_Cons_code(2))
hence "ABinds Δ = ABind v e ⊔ ABinds (delete v Δ)" by (rule Abinds_reorder1)
ultimately
show ?case by auto
qed
lemma Abinds_env_cong: "(⋀ x. x∈domA Δ ⟹ ae x = ae' x) ⟹ ABinds Δ⋅ae = ABinds Δ⋅ae'"
by (induct Δ rule: ABinds.induct) auto
lemma Abinds_env_restr_cong: " ae f|` domA Δ = ae' f|` domA Δ ⟹ ABinds Δ⋅ae = ABinds Δ⋅ae'"
by (rule Abinds_env_cong) (metis env_restr_eqD)
lemma ABinds_env_restr[simp]: "ABinds Δ⋅(ae f|` domA Δ) = ABinds Δ⋅ae"
by (rule Abinds_env_restr_cong) simp
lemma Abinds_join_fresh: "ae' ` (domA Δ) ⊆ {⊥} ⟹ ABinds Δ⋅(ae ⊔ ae') = (ABinds Δ⋅ae)"
by (rule Abinds_env_cong) auto
lemma ABinds_delete_bot: "ae x = ⊥ ⟹ ABinds (delete x Γ)⋅ae = ABinds Γ⋅ae"
by (induction Γ rule: ABinds.induct) (auto simp add: delete_twist)
lemma ABinds_restr_fresh:
assumes "atom ` S ♯* Γ"
shows "ABinds Γ⋅ae f|` (- S) = ABinds Γ⋅(ae f|` (- S)) f|` (- S)"
using assms
apply (induction Γ rule:ABinds.induct)
apply simp
apply (auto simp del: fun_meet_simp simp add: env_restr_join fresh_star_Pair fresh_star_Cons fresh_star_delete)
apply (subst lookup_env_restr)
apply (metis (no_types, hide_lams) ComplI fresh_at_base(2) fresh_star_def imageI)
apply simp
done
lemma ABinds_restr:
assumes "domA Γ ⊆ S"
shows "ABinds Γ⋅ae f|` S = ABinds Γ⋅(ae f|` S) f|` S"
using assms
by (induction Γ rule:ABinds.induct) (fastforce simp del: fun_meet_simp simp add: env_restr_join)+
lemma ABinds_restr_subst:
assumes "⋀ x' e a. (x',e) ∈ set Γ ⟹ Aexp e[x::=y]⋅a f|` S = Aexp e⋅a f|` S"
assumes "x ∉ S"
assumes "y ∉ S"
assumes "domA Γ ⊆ S"
shows "ABinds Γ[x::h=y]⋅ae f|` S = ABinds Γ⋅(ae f|` S) f|` S"
using assms
apply (induction Γ rule:ABinds.induct)
apply (auto simp del: fun_meet_simp join_comm simp add: env_restr_join)
apply (rule arg_cong2[where f = join])
apply (case_tac "ae v")
apply (auto dest: set_mp[OF set_delete_subset])
done
lemma Abinds_append_disjoint: "domA Δ ∩ domA Γ = {} ⟹ ABinds (Δ @ Γ)⋅ae = ABinds Δ⋅ae ⊔ ABinds Γ⋅ae"
proof (induct Δ rule: ABinds.induct)
case 1 thus ?case by simp
next
case (2 v e Δ)
from 2(2)
have "v ∉ domA Γ" and "domA (delete v Δ) ∩ domA Γ = {}" by auto
from 2(1)[OF this(2)]
have "ABinds (delete v Δ @ Γ)⋅ae = ABinds (delete v Δ)⋅ae ⊔ ABinds Γ⋅ae".
moreover
have "delete v Γ = Γ" by (metis `v ∉ domA Γ` delete_not_domA)
ultimately
show " ABinds (((v, e) # Δ) @ Γ)⋅ae = ABinds ((v, e) # Δ)⋅ae ⊔ ABinds Γ⋅ae"
by auto
qed
lemma ABinds_restr_subset: "S ⊆ S' ⟹ ABinds (restrictA S Γ)⋅ae ⊑ ABinds (restrictA S' Γ)⋅ae"
by (induct Γ rule: ABinds.induct)
(auto simp add: join_below_iff restr_delete_twist intro: below_trans[OF _ join_above2])
lemma ABinds_restrict_edom: "ABinds (restrictA (edom ae) Γ)⋅ae = ABinds Γ⋅ae"
by (induct Γ rule: ABinds.induct) (auto simp add: edom_def restr_delete_twist)
lemma ABinds_restrict_below: "ABinds (restrictA S Γ)⋅ae ⊑ ABinds Γ⋅ae"
by (induct Γ rule: ABinds.induct)
(auto simp add: join_below_iff restr_delete_twist intro: below_trans[OF _ join_above2] simp del: fun_meet_simp join_comm)
lemma ABinds_delete_below: "ABinds (delete x Γ)⋅ae ⊑ ABinds Γ⋅ae"
by (induct Γ rule: ABinds.induct)
(auto simp add: join_below_iff delete_twist[where x = x] elim: below_trans simp del: fun_meet_simp)
end
lemma ABind_eqvt[eqvt]: "π ∙ (ArityAnalysis.ABind Aexp v e) = ArityAnalysis.ABind (π ∙ Aexp) (π ∙ v) (π ∙ e)"
apply (rule cfun_eqvtI)
unfolding ArityAnalysis.ABind_eq
by perm_simp rule
lemma ABinds_eqvt[eqvt]: "π ∙ (ArityAnalysis.ABinds Aexp Γ) = ArityAnalysis.ABinds (π ∙ Aexp) (π ∙ Γ)"
apply (rule cfun_eqvtI)
apply (induction Γ rule: ArityAnalysis.ABinds.induct)
apply (simp add: ArityAnalysis.ABinds.simps)
apply (simp add: ArityAnalysis.ABinds.simps)
apply perm_simp
apply simp
done
lemma Abinds_cong[fundef_cong]:
"⟦ (⋀ e. e ∈ snd ` set heap2 ⟹ aexp1 e = aexp2 e) ; heap1 = heap2 ⟧
⟹ ArityAnalysis.ABinds aexp1 heap1 = ArityAnalysis.ABinds aexp2 heap2"
proof (induction heap1 arbitrary:heap2 rule:ArityAnalysis.ABinds.induct)
case 1
thus ?case by (auto simp add: ArityAnalysis.ABinds.simps)
next
case prems: (2 v e as heap2)
have "snd ` set (delete v as) ⊆ snd ` set as" by (rule dom_delete_subset)
also have "… ⊆ snd `set ((v, e) # as)" by auto
also note prems(3)
finally
have "(⋀e. e ∈ snd ` set (delete v as) ⟹ aexp1 e = aexp2 e)" by -(rule prems, auto)
from prems prems(1)[OF this refl] show ?case
by (auto simp add: ArityAnalysis.ABinds.simps ArityAnalysis.ABind_def)
qed
context EdomArityAnalysis
begin
lemma fup_Aexp_lookup_fresh: "atom v ♯ e ⟹ (fup⋅(Aexp e)⋅a) v = ⊥"
by (cases a) auto
lemma edom_AnalBinds: "edom (ABinds Γ⋅ae) ⊆ fv Γ"
by (induction Γ rule: ABinds.induct)
(auto simp del: fun_meet_simp dest: set_mp[OF fup_Aexp_edom] dest: set_mp[OF fv_delete_subset])
end
end