theory ArityAnalysisAbinds
imports ArityAnalysisSig
begin
context ArityAnalysis
begin
subsection {* 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 = fup\(Aexp e)\(ae v)"
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_above_arg: "ae \ ABinds \ \ ae"
proof (induction rule:ABinds.induct)
show "\ \ ABinds []\ae" by auto
next
fix v e \
assume assm: "ae \ ABinds (delete v \)\ae"
also have "\ \ ABinds ((v, e) # \)\ae" by auto
finally show "ae \ ABinds ((v, e) # \)\ae" by this simp
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 goal1 thus ?case by (auto simp add: ArityAnalysis.ABinds.simps)
next
case (goal2 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 goal2(3)
finally
have "(\e. e \ snd ` set (delete v as) \ aexp1 e = aexp2 e)" by -(rule goal2, auto)
note goal2(1)[OF this refl] with goal2
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