theory FTreeImplCardinalityCorrect
imports FTreeImplCardinality FTreeAnalysisSpec CardinalityAnalysisSpec CallFutureCardinality
begin
hide_const Multiset.single
lemma pathsCard_paths_nxt: "pathsCard (paths (nxt f x)) \ record_call x\(pathsCard (paths f))"
apply transfer
apply (rule pathsCard_below)
apply auto
apply (erule below_trans[OF _ monofun_cfun_arg[OF paths_Card_above], rotated]) back
apply (auto intro: fun_belowI simp add: record_call_simp two_pred_two_add_once)
done
lemma pathsCards_none: "pathsCard (paths t) x = none \ x \ carrier t"
by transfer (auto dest: pathCards_noneD)
lemma const_on_edom_disj: "const_on f S empty \ edom f \ S = {}"
by (auto simp add: empty_is_bottom edom_def)
context FTreeAnalysisCarrier
begin
lemma carrier_Fstack: "carrier (Fstack as S) \ fv S"
by (induction S rule: Fstack.induct)
(auto simp add: empty_is_bottom[symmetric] carrier_Fexp dest!: set_mp[OF Aexp_edom])
lemma carrier_FBinds: "carrier ((FBinds \\ae) x) \ fv \"
apply (simp add: Fexp.AnalBinds_lookup)
apply (auto split: option.split simp add: empty_is_bottom[symmetric] )
apply (case_tac "ae x")
apply (auto simp add: empty_is_bottom[symmetric] carrier_Fexp dest!: set_mp[OF Aexp_edom])
by (metis (poly_guards_query) contra_subsetD domA_from_set map_of_fv_subset map_of_is_SomeD option.sel)
end
context FTreeAnalysisCorrect
begin
sublocale CardinalityPrognosisShape prognosis
proof
fix \ :: heap and ae ae' :: AEnv and u e S as
assume "ae f|` domA \ = ae' f|` domA \"
from Fexp.AnalBinds_cong[OF this]
show "prognosis ae as u (\, e, S) = prognosis ae' as u (\, e, S)" by simp
next
fix ae as a \ e S
show "const_on (prognosis ae as a (\, e, S)) (ap S) many"
proof
fix x
assume "x \ ap S"
hence "[x,x] \ paths (Fstack as S)"
by (induction S rule: Fstack.induct)
(auto 4 4 intro: set_mp[OF both_contains_arg1] set_mp[OF both_contains_arg2] paths_Cons_nxt)
hence "[x,x] \ paths (Fexp e\a \\ Fstack as S)"
by (rule set_mp[OF both_contains_arg2])
hence "[x,x] \ paths (substitute (FBinds \\ae) (thunks \) (Fexp e\a \\ Fstack as S))"
by (rule set_mp[OF substitute_contains_arg])
hence "pathCard [x,x] x \ pathsCard (paths (substitute (FBinds \\ae) (thunks \) (Fexp e\a \\ Fstack as S))) x"
by (metis fun_belowD paths_Card_above)
also have "pathCard [x,x] x = many" by (auto simp add: pathCard_def)
finally
show "prognosis ae as a (\, e, S) x = many"
by (auto intro: below_antisym)
qed
next
fix \ \ :: heap and e :: exp and ae :: AEnv and as u S
assume "map_of \ = map_of \"
hence "FBinds \ = FBinds \" and "thunks \ = thunks \" by (auto intro!: cfun_eqI thunks_cong simp add: Fexp.AnalBinds_lookup)
thus "prognosis ae as u (\, e, S) = prognosis ae as u (\, e, S)" by simp
next
fix \ :: heap and e :: exp and ae :: AEnv and as u S x
show "prognosis ae as u (\, e, S) \ prognosis ae as u (\, e, Upd x # S)" by simp
next
fix \ :: heap and e :: exp and ae :: AEnv and as a S x
assume "ae x = \"
hence "FBinds (delete x \)\ae = FBinds \\ae" by (rule Fexp.AnalBinds_delete_bot)
moreover
hence "((FBinds \\ae) x) = \" by (metis Fexp.AnalBinds_delete_lookup)
ultimately
show "prognosis ae as a (\, e, S) \ prognosis ae as a (delete x \, e, S)"
by (simp add: substitute_T_delete empty_is_bottom)
next
fix ae as a \ x S
have "once \ (pathCard [x]) x" by (simp add: two_add_simp)
also have "pathCard [x] \ pathsCard ({[],[x]})"
by (rule paths_Card_above) simp
also have "\ = pathsCard (paths (single x))" by simp
also have "single x \ (Fexp (Var x)\a)" by (rule Fexp_Var)
also have "\ \ Fexp (Var x)\a \\ Fstack as S" by (rule both_above_arg1)
also have "\ \ substitute (FBinds \\ae) (thunks \) (Fexp (Var x)\a \\ Fstack as S)" by (rule substitute_above_arg)
also have "pathsCard (paths \) x = prognosis ae as a (\, Var x, S) x" by simp
finally
show "once \ prognosis ae as a (\, Var x, S) x"
by this (rule cont2cont_fun, intro cont2cont)+
qed
sublocale CardinalityPrognosisApp prognosis
proof default
fix ae as a \ e x S
have "Fexp e\(inc\a) \\ many_calls x \\ Fstack as S = many_calls x \\ (Fexp e)\(inc\a) \\ Fstack as S"
by (metis both_assoc both_comm)
thus "prognosis ae as (inc\a) (\, e, Arg x # S) \ prognosis ae as a (\, App e x, S)"
by simp (intro pathsCard_mono' paths_mono substitute_mono2' both_mono1' Fexp_App)
qed
sublocale CardinalityPrognosisLam prognosis
proof default
fix ae as a \ e y x S
have "Fexp e[y::=x]\(pred\a) \ many_calls x \\ Fexp (Lam [y]. e)\a"
by (rule below_trans[OF Fexp_subst both_mono2'[OF Fexp_Lam]])
moreover have "Fexp (Lam [y]. e)\a \\ many_calls x \\ Fstack as S = many_calls x \\ Fexp (Lam [y]. e)\a \\ Fstack as S"
by (metis both_assoc both_comm)
ultimately
show "prognosis ae as (pred\a) (\, e[y::=x], S) \ prognosis ae as a (\, Lam [y]. e, Arg x # S)"
by simp (intro pathsCard_mono' paths_mono substitute_mono2' both_mono1')
qed
sublocale CardinalityPrognosisVar prognosis
proof default
fix \ :: heap and e :: exp and x :: var and ae :: AEnv and as u a S
assume "map_of \ x = Some e"
assume "ae x = up\u"
have "pathsCard (paths (substitute (FBinds \\ae) (thunks \) (Fexp e\u \\ Fstack as S))) = pathsCard (paths (nxt (and_then x (substitute (FBinds \\ae) (thunks \) (Fexp e\u \\ Fstack as S))) x))"
by simp
also
have "\ \ record_call x\(pathsCard (paths (and_then x (substitute (FBinds \\ae) (thunks \) (Fexp e\u \\ Fstack as S)))))"
by (rule pathsCard_paths_nxt)
also
have "\ = record_call x\(pathsCard (paths (and_then x (substitute (FBinds \\ae) (thunks \) (Fstack as S \\ Fexp e\u)))))"
by (metis both_comm)
also
have "\ = record_call x\(pathsCard (paths (and_then x (substitute (FBinds \\ae) (thunks \) (Fstack as S \\ (FBinds \\ae) x)))))"
using `map_of \ x = Some e` `ae x = up\u` by (simp add: Fexp.AnalBinds_lookup)
also
assume "isVal e"
hence "x \ thunks \" using `map_of \ x = Some e` by (metis thunksE)
hence "FBinds \\ae = f_nxt (FBinds \\ae) (thunks \) x" by (auto simp add: f_nxt_def)
hence "and_then x (substitute (FBinds \\ae) (thunks \) (Fstack as S \\ (FBinds \\ae) x)) = substitute (FBinds \\ae) (thunks \) (and_then x (Fstack as S))"
by (simp add: substitute_and_then)
also
have "and_then x (Fstack as S) \ single x \\ Fstack as S" by (rule and_then_both_single')
note pathsCard_mono'[OF paths_mono[OF substitute_mono2'[OF this]]]
also
have "single x \ Fexp (Var x)\a" by (rule Fexp_Var)
note pathsCard_mono'[OF paths_mono[OF substitute_mono2'[OF both_mono1'[OF this]]]]
finally
have "pathsCard (paths (substitute (FBinds \\ae) (thunks \) (Fexp e\u \\ Fstack as S))) \ record_call x\(pathsCard (paths (substitute (FBinds \\ae) (thunks \) (Fexp (Var x)\a \\ Fstack as S))))"
by this simp_all
thus "prognosis ae as u (\, e, S) \ record_call x\(prognosis ae as a (\, Var x, S))" by simp
next
fix \ :: heap and e :: exp and x :: var and ae :: AEnv and as u a S
assume "map_of \ x = Some e"
assume "ae x = up\u"
assume "\ isVal e"
hence "x \ thunks \" using `map_of \ x = Some e` by (metis thunksI)
hence [simp]: "f_nxt (FBinds \\ae) (thunks \) x = FBinds (delete x \)\ae"
by (auto simp add: f_nxt_def Fexp.AnalBinds_delete_to_fun_upd empty_is_bottom)
have "pathsCard (paths (substitute (FBinds (delete x \)\ae) (thunks (delete x \)) (Fexp e\u \\ Fstack as S)))
= pathsCard (paths (substitute (FBinds (delete x \)\ae) (thunks \) (Fexp e\u \\ Fstack as S)))"
by (rule arg_cong[OF substitute_cong_T]) (auto simp add: empty_is_bottom)
also have "\ = pathsCard (paths (nxt (and_then x (substitute (FBinds (delete x \)\ae) (thunks \) (Fexp e\u \\ Fstack as S))) x))"
by simp
also
have "\ \ record_call x\(pathsCard (paths (and_then x (substitute (FBinds (delete x \)\ae) (thunks \) (Fexp e\u \\ Fstack as S)))))"
by (rule pathsCard_paths_nxt)
also
have "\ = record_call x\(pathsCard (paths (and_then x (substitute (FBinds (delete x \)\ae) (thunks \) (Fstack as S \