theory CoCallImplFTreeCorrect
imports CoCallImplFTree CoCallAnalysisSpec FTreeAnalysisSpec CallFutureCardinality
begin
hide_const Multiset.single
lemma valid_lists_many_calls:
assumes "\ one_call_in_path x p"
assumes "p \ valid_lists S G"
shows "x \ ccManyCalls G"
using assms(2,1)
proof(induction rule:valid_lists.induct[case_names Nil Cons])
case Nil thus ?case by simp
next
case (Cons xs x')
show ?case
proof(cases "one_call_in_path x xs")
case False
from Cons.IH[OF this]
show ?thesis.
next
case True
with `\ one_call_in_path x (x' # xs)`
have [simp]: "x' = x" by (auto split: if_splits)
have "x \ set xs"
proof(rule ccontr)
assume "x \ set xs"
hence "no_call_in_path x xs" by (metis no_call_in_path_set_conv)
hence "one_call_in_path x (x # xs)" by simp
with Cons show False by simp
qed
with `set xs \ ccNeighbors x' G`
have "x \ ccNeighbors x G" by auto
thus ?thesis by simp
qed
qed
context CoCallArityEdom
begin
lemma carrier_Fexp': "carrier (Fexp e\a) \ fv e"
unfolding Fexp_simp carrier_ccFTree
by (rule Aexp_edom)
end
context CoCallArityCorrect
begin
lemma carrier_AnalBinds_below:
"carrier ((Fexp.AnalBinds \\(Aheap \ e\a)) x) \ edom ((ABinds \)\(Aheap \ e\a))"
by (auto simp add: Fexp.AnalBinds_lookup Fexp_def split: option.splits
elim!: set_mp[OF edom_mono[OF monofun_cfun_fun[OF ABind_below_ABinds]]])
sublocale FTreeAnalysisCarrier Fexp
apply default unfolding Fexp_simp carrier_ccFTree..
sublocale FTreeAnalysisCorrect Fexp
proof default
fix x e a
from edom_mono[OF Aexp_App]
have *: "{x} \ edom (Aexp e\(inc\a)) \ edom (Aexp (App e x)\a)" by auto
have **: "{x} \ edom (Aexp e\(inc\a)) \ insert x (fv e)"
by (intro subset_trans[OF *] subset_trans[OF Aexp_edom]) auto
have "many_calls x \\ Fexp e\(inc\a) = many_calls x \\ ccFTree (edom (Aexp e\(inc\a))) (ccExp e\(inc\a))"
unfolding Fexp_simp..
also have "\ = ccFTree {x} (ccProd {x} {x}) \\ ccFTree (edom (Aexp e\(inc\a))) (ccExp e\(inc\a))"
unfolding many_calls_ccFTree..
also have "\ \ ccFTree ({x} \ edom (Aexp e\(inc\a))) (ccProd {x} {x} \ ccExp e\(inc\a) \ ccProd {x} (edom (Aexp e\(inc\a))))"
by (rule interleave_ccFTree)
also have "\ \ ccFTree (edom (Aexp (App e x)\a)) (ccProd {x} {x} \ ccExp e\(inc\a) \ ccProd {x} (edom (Aexp e\(inc\a))))"
by (rule ccFTree_mono1[OF *])
also have "ccProd {x} {x} \ ccExp e\(inc\a) \ ccProd {x} (edom (Aexp e\(inc\a))) = ccExp e\(inc\a) \ ccProd {x} ({x} \ (edom (Aexp e\(inc\a))))"
by (simp add: ccProd_union2[symmetric] del: ccProd_union2)
also have "ccProd {x} ({x} \ (edom (Aexp e\(inc\a)))) \ ccProd {x} (insert x (fv e))"
by (rule ccProd_mono2[OF **])
also have "ccExp e\(inc\a) \ ccProd {x} (insert x (fv e)) \ ccExp (App e x)\a"
by (rule ccExp_App)
also have "ccFTree (edom (Aexp (App e x)\a)) (ccExp (App e x)\a) = Fexp (App e x)\a"
unfolding Fexp_simp..
finally
show "many_calls x \\ Fexp e\(inc\a) \ Fexp (App e x)\a"
by this simp_all
next
fix y e n
from edom_mono[OF Aexp_Lam]
have *: "edom (Aexp e\(pred\n)) - {y} \ edom (Aexp (Lam [y]. e)\n)" by auto
have "without y (Fexp e\(pred\n)) = without y (ccFTree (edom (Aexp e\(pred\n))) (ccExp e\(pred\n)))"
unfolding Fexp_simp..
also have "\ = ccFTree (edom (Aexp e\(pred\n)) - {y}) (ccExp e\(pred\n))"
by (rule without_ccFTree)
also have "\ \ ccFTree (edom (Aexp (Lam [y]. e)\n)) (ccExp e\(pred\n))"
by (rule ccFTree_mono1[OF *])
also have "\ = ccFTree (edom (Aexp (Lam [y]. e)\n)) (cc_restr ((edom (Aexp (Lam [y]. e)\n))) (ccExp e\(pred\n)))"
by (rule ccFTree_cc_restr)
also have "(cc_restr ((edom (Aexp (Lam [y]. e)\n))) (ccExp e\(pred\n))) \ (cc_restr (fv (Lam [y]. e)) (ccExp e\(pred\n)))"
by (rule cc_restr_mono1[OF Aexp_edom])
also have "\ \ ccExp (Lam [y]. e)\n"
by (rule ccExp_Lam)
also have "ccFTree (edom (Aexp (Lam [y]. e)\n)) (ccExp (Lam [y]. e)\n) = Fexp (Lam [y]. e)\n"
unfolding Fexp_simp..
finally
show "without y (Fexp e\(pred\n)) \ Fexp (Lam [y]. e)\n" by this simp_all
next
fix e y x a
from edom_mono[OF Aexp_subst]
have *: "edom (Aexp e[y::=x]\a) \ insert x (edom (Aexp e\a) - {y})" by simp
have "Fexp e[y::=x]\a = ccFTree (edom (Aexp e[y::=x]\a)) (ccExp e[y::=x]\a)"
unfolding Fexp_simp..
also have "\ \ ccFTree (insert x (edom (Aexp e\a) - {y})) (ccExp e[y::=x]\a)"
by (rule ccFTree_mono1[OF *])
also have "\ \ many_calls x \\ without x (\)"
by (rule paths_many_calls_subset)
also have "without x (ccFTree (insert x (edom (Aexp e\a) - {y})) (ccExp e[y::=x]\a))
= ccFTree (edom (Aexp e\a) - {y} - {x}) (ccExp e[y::=x]\a)"
by simp
also have "\ \ ccFTree (edom (Aexp e\a) - {y} - {x}) (ccExp e\a)"
by (rule ccFTree_cong_below[OF ccExp_subst]) auto
also have "\ = without y (ccFTree (edom (Aexp e\a) - {x}) (ccExp e\a))"
by simp (metis Diff_insert Diff_insert2)
also have "ccFTree (edom (Aexp e\a) - {x}) (ccExp e\a) \ ccFTree (edom (Aexp e\a)) (ccExp e\a)"
by (rule ccFTree_mono1) auto
also have "\ = Fexp e\a"
unfolding Fexp_simp..
finally
show "Fexp e[y::=x]\a \ many_calls x \\ without y (Fexp e\a)"
by this simp_all
next
fix v a
have "up\a \ (Aexp (Var v)\a) v" by (rule Aexp_Var)
hence "v \ edom (Aexp (Var v)\a)" by (auto simp add: edom_def)
hence "[v] \ valid_lists (edom (Aexp (Var v)\a)) (ccExp (Var v)\a)"
by auto
thus "single v \ Fexp (Var v)\a"
unfolding Fexp_simp by (auto intro: single_below)
next
fix scrut e1 a e2
have "ccFTree (edom (Aexp e1\a)) (ccExp e1\a) \\ ccFTree (edom (Aexp e2\a)) (ccExp e2\a)
\ ccFTree (edom (Aexp e1\a) \ edom (Aexp e2\a)) (ccExp e1\a \ ccExp e2\a)"
by (rule either_ccFTree)
note both_mono2'[OF this]
also
have "ccFTree (edom (Aexp scrut\0)) (ccExp scrut\0) \\ ccFTree (edom (Aexp e1\a) \ edom (Aexp e2\a)) (ccExp e1\a \ ccExp e2\a)
\ ccFTree (edom (Aexp scrut\0) \ (edom (Aexp e1\a) \ edom (Aexp e2\a))) (ccExp scrut\0 \ (ccExp e1\a \ ccExp e2\a) \ ccProd (edom (Aexp scrut\0)) (edom (Aexp e1\a) \ edom (Aexp e2\a)))"
by (rule interleave_ccFTree)
also
have "edom (Aexp scrut\0) \ (edom (Aexp e1\a) \ edom (Aexp e2\a)) = edom (Aexp scrut\0 \ Aexp e1\a \ Aexp e2\a)" by auto
also
have "Aexp scrut\0 \ Aexp e1\a \ Aexp e2\a \ Aexp (scrut ? e1 : e2)\a"
by (rule Aexp_IfThenElse)
also
have "ccExp scrut\0 \ (ccExp e1\a \ ccExp e2\a) \ ccProd (edom (Aexp scrut\0)) (edom (Aexp e1\a) \ edom (Aexp e2\a)) \
ccExp (scrut ? e1 : e2)\a"
by (rule ccExp_IfThenElse)
finally
show "Fexp scrut\0 \\ (Fexp e1\