theory ArityAnalysisFix
imports ArityAnalysisSig ArityAnalysisAbinds
begin
context ArityAnalysis
begin
definition Afix :: "heap ⇒ (AEnv → AEnv)"
where "Afix Γ = (Λ ae. (μ ae'. ABinds Γ ⋅ ae' ⊔ ae))"
lemma Afix_eq: "Afix Γ⋅ae = (μ ae'. (ABinds Γ⋅ae') ⊔ ae)"
unfolding Afix_def by simp
lemma Afix_strict[simp]: "Afix Γ⋅⊥ = ⊥"
unfolding Afix_eq
by (rule fix_eqI) auto
lemma Afix_least_below: "ABinds Γ ⋅ ae' ⊑ ae' ⟹ ae ⊑ ae' ⟹ Afix Γ ⋅ ae ⊑ ae'"
unfolding Afix_eq
by (auto intro: fix_least_below)
lemma Afix_unroll: "Afix Γ⋅ae = ABinds Γ ⋅ (Afix Γ⋅ae) ⊔ ae"
unfolding Afix_eq
apply (subst fix_eq)
by simp
lemma Abinds_below_Afix: "ABinds Δ ⊑ Afix Δ"
apply (rule cfun_belowI)
apply (simp add: Afix_eq)
apply (subst fix_eq, simp)
apply (rule below_trans[OF _ join_above2])
apply (rule monofun_cfun_arg)
apply (subst fix_eq, simp)
done
lemma Afix_above_arg: "ae ⊑ Afix Γ ⋅ ae"
by (subst Afix_unroll) simp
lemma Abinds_Afix_below[simp]: "ABinds Γ⋅(Afix Γ⋅ae) ⊑ Afix Γ⋅ae"
apply (subst Afix_unroll) back
apply simp
done
lemma Afix_reorder: "map_of Γ = map_of Δ ⟹ Afix Γ = Afix Δ"
by (intro cfun_eqI)(simp add: Afix_eq cong: Abinds_reorder)
lemma Afix_repeat_singleton: "(μ xa. Afix Γ⋅(esing x⋅(n ⊔ xa x) ⊔ ae)) = Afix Γ⋅(esing x⋅n ⊔ ae)"
apply (rule below_antisym)
defer
apply (subst fix_eq, simp)
apply (intro monofun_cfun_arg join_mono below_refl join_above1)
apply (rule fix_least_below, simp)
apply (rule Afix_least_below, simp)
apply (intro join_below below_refl iffD2[OF esing_below_iff] below_trans[OF _ fun_belowD[OF Afix_above_arg]] below_trans[OF _ Afix_above_arg] join_above1)
apply simp
done
lemma Afix_join_fresh: "ae' ` (domA Δ) ⊆ {⊥} ⟹ Afix Δ⋅(ae ⊔ ae') = (Afix Δ⋅ae) ⊔ ae'"
apply (rule below_antisym)
apply (rule Afix_least_below)
apply (subst Abinds_join_fresh, simp)
apply (rule below_trans[OF Abinds_Afix_below join_above1])
apply (rule join_below)
apply (rule below_trans[OF Afix_above_arg join_above1])
apply (rule join_above2)
apply (rule join_below[OF monofun_cfun_arg [OF join_above1]])
apply (rule below_trans[OF join_above2 Afix_above_arg])
done
lemma Afix_restr_fresh:
assumes "atom ` S ♯* Γ"
shows "Afix Γ⋅ae f|` (- S) = Afix Γ⋅(ae f|` (- S)) f|` (- S)"
unfolding Afix_eq
proof (rule parallel_fix_ind[where P = "λ x y . x f|` (- S) = y f|` (- S)"], goal_cases)
case 1
show ?case by simp
next
case 2
show ?case ..
next
case prems: (3 aeL aeR)
have "(ABinds Γ⋅aeL ⊔ ae) f|` (- S) = ABinds Γ⋅aeL f|` (- S) ⊔ ae f|` (- S)" by (simp add: env_restr_join)
also have "… = ABinds Γ⋅(aeL f|` (- S)) f|` (- S) ⊔ ae f|` (- S)" by (rule arg_cong[OF ABinds_restr_fresh[OF assms]])
also have "… = ABinds Γ⋅(aeR f|` (- S)) f|` (- S) ⊔ ae f|` (- S)" unfolding prems ..
also have "… = ABinds Γ⋅aeR f|` (- S) ⊔ ae f|` (- S)" by (rule arg_cong[OF ABinds_restr_fresh[OF assms, symmetric]])
also have "… = (ABinds Γ⋅aeR ⊔ ae f|` (- S)) f|` (- S)" by (simp add: env_restr_join)
finally show ?case by simp
qed
lemma Afix_restr:
assumes "domA Γ ⊆ S"
shows "Afix Γ⋅ae f|` S = Afix Γ⋅(ae f|` S) f|` S"
unfolding Afix_eq
apply (rule parallel_fix_ind[where P = "λ x y . x f|`S = y f|` S"])
apply simp
apply rule
apply (auto simp add: env_restr_join)
apply (metis ABinds_restr[OF assms, symmetric])
done
lemma Afix_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 "Afix Γ[x::h=y]⋅ae f|` S = Afix Γ⋅(ae f|` S) f|` S"
unfolding Afix_eq
apply (rule parallel_fix_ind[where P = "λ x y . x f|`S = y f|` S"])
apply simp
apply rule
apply (auto simp add: env_restr_join)
apply (subst ABinds_restr_subst[OF assms]) apply assumption
apply (subst ABinds_restr[OF assms(4)]) back
apply simp
done
lemma Afix_subst_approx:
assumes "⋀ v n. v ∈ domA Γ ⟹ Aexp (the (map_of Γ v))[y::=x]⋅n ⊑ (Aexp (the (map_of Γ v))⋅n)(y := ⊥, x := up⋅0)"
assumes "x ∉ domA Γ"
assumes "y ∉ domA Γ"
shows "Afix Γ[y::h= x]⋅(ae(y := ⊥, x := up⋅0)) ⊑ (Afix Γ⋅ae)(y := ⊥, x := up⋅0)"
unfolding Afix_eq
proof (rule parallel_fix_ind[where P = "λ aeL aeR . aeL ⊑ aeR(y := ⊥, x := up⋅0)"], goal_cases)
case 1
show ?case by simp
next
case 2
show ?case..
next
case (3 aeL aeR)
hence "ABinds Γ[y::h=x]⋅aeL ⊑ ABinds Γ[y::h=x]⋅(aeR (y := ⊥, x := up⋅0))" by (rule monofun_cfun_arg)
also have "… ⊑ (ABinds Γ⋅aeR)(y := ⊥, x := up⋅0)"
using assms
proof (induction rule: ABinds.induct, goal_cases)
case 1
thus ?case by simp
next
case prems: (2 v e Γ)
have "⋀n. Aexp e[y::=x]⋅n ⊑ (Aexp e⋅n)(y := ⊥, x := up⋅0)" using prems(2)[where v = v] by auto
hence IH1: "⋀ n. fup⋅(Aexp e[y::=x])⋅n ⊑ (fup⋅(Aexp e)⋅n)(y := ⊥, x := up⋅0)" by (case_tac n) auto
have "ABinds (delete v Γ)[y::h=x]⋅(aeR(y := ⊥, x := up⋅0)) ⊑ (ABinds (delete v Γ)⋅aeR)(y := ⊥, x := up⋅0)"
apply (rule prems) using prems(2,3,4) by fastforce+
hence IH2: "ABinds (delete v Γ[y::h=x])⋅(aeR(y := ⊥, x := up⋅0)) ⊑ (ABinds (delete v Γ)⋅aeR)(y := ⊥, x := up⋅0)"
unfolding subst_heap_delete.
have [simp]: "(aeR(y := ⊥, x := up⋅0)) v = aeR v" using prems(3,4) by auto
show ?case by (simp del: fun_upd_apply join_comm) (rule join_mono[OF IH1 IH2])
qed
finally have "ABinds Γ[y::h=x]⋅aeL ⊑ (ABinds Γ⋅aeR)(y := ⊥, x := up⋅0)"
by this simp
thus ?case
by (auto simp add: join_below_iff elim: below_trans)
qed
end
lemma Afix_eqvt[eqvt]: "π ∙ (ArityAnalysis.Afix Aexp Γ) = ArityAnalysis.Afix (π ∙ Aexp) (π ∙ Γ)"
unfolding ArityAnalysis.Afix_def
by perm_simp (simp add: Abs_cfun_eqvt)
lemma Afix_cong[fundef_cong]:
"⟦ (⋀ e. e ∈ snd ` set heap2 ⟹ aexp1 e = aexp2 e); heap1 = heap2 ⟧
⟹ ArityAnalysis.Afix aexp1 heap1 = ArityAnalysis.Afix aexp2 heap2"
unfolding ArityAnalysis.Afix_def by (metis Abinds_cong)
context EdomArityAnalysis
begin
lemma Afix_edom: "edom (Afix Γ ⋅ ae) ⊆ fv Γ ∪ edom ae"
unfolding Afix_eq
by (rule fix_ind[where P = "λ ae' . edom ae' ⊆ fv Γ ∪ edom ae"] )
(auto dest: set_mp[OF edom_AnalBinds])
lemma ABinds_lookup_fresh:
"atom v ♯ Γ ⟹ (ABinds Γ⋅ae) v = ⊥"
by (induct Γ rule: ABinds.induct) (auto simp add: fresh_Cons fresh_Pair fup_Aexp_lookup_fresh fresh_delete)
lemma Afix_lookup_fresh:
assumes "atom v ♯ Γ"
shows "(Afix Γ⋅ae) v = ae v"
apply (rule below_antisym)
apply (subst Afix_eq)
apply (rule fix_ind[where P = "λ ae'. ae' v ⊑ ae v"])
apply (auto simp add: ABinds_lookup_fresh[OF assms] fun_belowD[OF Afix_above_arg])
done
lemma Afix_comp2join_fresh:
"atom ` (domA Δ) ♯* Γ ⟹ ABinds Δ⋅(Afix Γ⋅ae) = ABinds Δ⋅ae"
proof (induct Δ rule: ABinds.induct)
case 1 show ?case by (simp add: Afix_above_arg del: fun_meet_simp)
next
case (2 v e Δ)
from 2(2)
have "atom v ♯ Γ" and "atom ` domA (delete v Δ) ♯* Γ"
by (auto simp add: fresh_star_def)
from 2(1)[OF this(2)]
show ?case by (simp del: fun_meet_simp add: Afix_lookup_fresh[OF `atom v ♯ Γ`])
qed
lemma Afix_append_fresh:
assumes "atom ` domA Δ ♯* Γ"
shows "Afix (Δ @ Γ)⋅ae = Afix Γ⋅(Afix Δ⋅ae)"
proof (rule below_antisym)
show *: "Afix (Δ @ Γ)⋅ae ⊑ Afix Γ⋅(Afix Δ⋅ae)"
apply (rule Afix_least_below)
apply (simp add: Abinds_append_disjoint[OF fresh_distinct[OF assms]] Afix_comp2join_fresh[OF assms])
apply (rule below_trans[OF join_mono[OF Abinds_Afix_below Abinds_Afix_below]])
apply (simp_all add: Afix_above_arg below_trans[OF Afix_above_arg Afix_above_arg])
done
next
show "Afix Γ⋅(Afix Δ⋅ae) ⊑ Afix (Δ @ Γ)⋅ae"
proof (rule Afix_least_below)
show "ABinds Γ⋅(Afix (Δ @ Γ)⋅ae) ⊑ Afix (Δ @ Γ)⋅ae"
apply (rule below_trans[OF _ Abinds_Afix_below])
apply (subst Abinds_append_disjoint[OF fresh_distinct[OF assms]])
apply simp
done
have "ABinds Δ⋅(Afix (Δ @ Γ)⋅ae) ⊑ Afix (Δ @ Γ)⋅ae"
apply (rule below_trans[OF _ Abinds_Afix_below])
apply (subst Abinds_append_disjoint[OF fresh_distinct[OF assms]])
apply simp
done
thus "Afix Δ⋅ae ⊑ Afix (Δ @ Γ)⋅ae"
apply (rule Afix_least_below)
apply (rule Afix_above_arg)
done
qed
qed
lemma Afix_e_to_heap:
"Afix (delete x Γ)⋅(fup⋅(Aexp e)⋅n ⊔ ae) ⊑ Afix ((x, e) # delete x Γ)⋅(esing x⋅n ⊔ ae)"
apply (simp add: Afix_eq)
apply (rule fix_least_below, simp)
apply (intro join_below)
apply (subst fix_eq, simp)
apply (subst fix_eq, simp)
apply (rule below_trans[OF _ join_above2])
apply (rule below_trans[OF _ join_above2])
apply (rule below_trans[OF _ join_above2])
apply (rule monofun_cfun_arg)
apply (subst fix_eq, simp)
apply (subst fix_eq, simp) back apply (simp add: below_trans[OF _ join_above2])
done
lemma Afix_e_to_heap':
"Afix (delete x Γ)⋅(Aexp e⋅n) ⊑ Afix ((x, e) # delete x Γ)⋅(esing x⋅(up⋅n))"
using Afix_e_to_heap[where ae = ⊥ and n = "up⋅n"] by simp
end
end