theory TTreeImplCardinalitySafe imports TTreeImplCardinality TTreeAnalysisSpec CardinalityAnalysisSpec 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 TTreeAnalysisCarrier 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: Texp.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_SomeD option.sel) end context TTreeAnalysisSafe begin sublocale CardinalityPrognosisShape prognosis proof fix Γ :: heap and ae ae' :: AEnv and u e S as assume "ae f|` domA Γ = ae' f|` domA Γ" from Texp.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 (Texp e⋅a ⊗⊗ Fstack as S)" by (rule set_mp[OF both_contains_arg2]) hence "[x,x] ∈ paths (substitute (FBinds Γ⋅ae) (thunks Γ) (Texp e⋅a ⊗⊗ Fstack as S))" by (rule set_mp[OF substitute_contains_arg]) hence "pathCard [x,x] x ⊑ pathsCard (paths (substitute (FBinds Γ⋅ae) (thunks Γ) (Texp 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: Texp.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 Texp.AnalBinds_delete_bot) moreover hence "((FBinds Γ⋅ae) x) = ⊥" by (metis Texp.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 ⊑ (Texp (Var x)⋅a)" by (rule Texp_Var) also have "… ⊑ Texp (Var x)⋅a ⊗⊗ Fstack as S" by (rule both_above_arg1) also have "… ⊑ substitute (FBinds Γ⋅ae) (thunks Γ) (Texp (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 fix ae as a Γ e x S have "Texp e⋅(inc⋅a) ⊗⊗ many_calls x ⊗⊗ Fstack as S = many_calls x ⊗⊗ (Texp 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' Texp_App) qed sublocale CardinalityPrognosisLam prognosis proof fix ae as a Γ e y x S have "Texp e[y::=x]⋅(pred⋅a) ⊑ many_calls x ⊗⊗ Texp (Lam [y]. e)⋅a" by (rule below_trans[OF Texp_subst both_mono2'[OF Texp_Lam]]) moreover have "Texp (Lam [y]. e)⋅a ⊗⊗ many_calls x ⊗⊗ Fstack as S = many_calls x ⊗⊗ Texp (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 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 thunksE) hence [simp]: "f_nxt (FBinds Γ⋅ae) (thunks Γ) x = FBinds Γ⋅ae" by (auto simp add: f_nxt_def) have "prognosis ae as u (Γ, e, S) = pathsCard (paths (substitute (FBinds Γ⋅ae) (thunks Γ) (Texp e⋅u ⊗⊗ Fstack as S)))" by simp also have "… = pathsCard (paths (substitute (FBinds Γ⋅ae) (thunks Γ) (nxt (single x) x ⊗⊗ Texp e⋅u ⊗⊗ Fstack as S)))" by simp also have "… = pathsCard (paths (substitute (FBinds Γ⋅ae) (thunks Γ) ((nxt (single x) x ⊗⊗ Fstack as S) ⊗⊗ Texp e⋅u )))" by (metis both_assoc both_comm) also have "… ⊑ pathsCard (paths (substitute (FBinds Γ⋅ae) (thunks Γ) (nxt (single x ⊗⊗ Fstack as S) x ⊗⊗ Texp e⋅u)))" by (intro pathsCard_mono' paths_mono substitute_mono2' both_mono1' nxt_both_left) simp also have "… = pathsCard (paths (nxt (substitute (FBinds Γ⋅ae) (thunks Γ) (single x ⊗⊗ Fstack as S)) x))" using `map_of Γ x = Some e` `ae x = up⋅u` by (simp add: Texp.AnalBinds_lookup) also have "… ⊑ record_call x ⋅(pathsCard (paths (substitute (FBinds Γ⋅ae) (thunks Γ) (single x ⊗⊗ Fstack as S))))" by (rule pathsCard_paths_nxt) also have "… ⊑ record_call x ⋅(pathsCard (paths (substitute (FBinds Γ⋅ae) (thunks Γ) ((Texp (Var x)⋅a) ⊗⊗ Fstack as S))))" by (intro monofun_cfun_arg pathsCard_mono' paths_mono substitute_mono2' both_mono1' Texp_Var) also have "… = record_call x ⋅(prognosis ae as a (Γ, Var x, S))" by simp finally show "prognosis ae as u (Γ, e, S) ⊑ record_call x⋅(prognosis ae as a (Γ, Var x, S))" by this simp_all 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 Texp.AnalBinds_delete_to_fun_upd empty_is_bottom) have "prognosis ae as u (delete x Γ, e, Upd x # S) = pathsCard (paths (substitute (FBinds (delete x Γ)⋅ae) (thunks (delete x Γ)) (Texp e⋅u ⊗⊗ Fstack as S)))" by simp also have "… = pathsCard (paths (substitute (FBinds (delete x Γ)⋅ae) (thunks Γ) (Texp e⋅u ⊗⊗ Fstack as S)))" by (rule arg_cong[OF substitute_cong_T]) (auto simp add: empty_is_bottom) also have "… = pathsCard (paths (substitute (FBinds (delete x Γ)⋅ae) (thunks Γ) (nxt (single x) x ⊗⊗ Texp e⋅u ⊗⊗ Fstack as S)))" by simp also have "… = pathsCard (paths (substitute (FBinds (delete x Γ)⋅ae) (thunks Γ) ((nxt (single x) x ⊗⊗ Fstack as S) ⊗⊗ Texp e⋅u )))" by (metis both_assoc both_comm) also have "… ⊑ pathsCard (paths (substitute (FBinds (delete x Γ)⋅ae) (thunks Γ) (nxt (single x ⊗⊗ Fstack as S) x ⊗⊗ Texp e⋅u)))" by (intro pathsCard_mono' paths_mono substitute_mono2' both_mono1' nxt_both_left) simp also have "… = pathsCard (paths (nxt (substitute (FBinds Γ⋅ae) (thunks Γ) (single x ⊗⊗ Fstack as S)) x))" using `map_of Γ x = Some e` `ae x = up⋅u` by (simp add: Texp.AnalBinds_lookup) also have "… ⊑ record_call x ⋅(pathsCard (paths (substitute (FBinds Γ⋅ae) (thunks Γ) (single x ⊗⊗ Fstack as S))))" by (rule pathsCard_paths_nxt) also have "… ⊑ record_call x ⋅(pathsCard (paths (substitute (FBinds Γ⋅ae) (thunks Γ) ((Texp (Var x)⋅a) ⊗⊗ Fstack as S))))" by (intro monofun_cfun_arg pathsCard_mono' paths_mono substitute_mono2' both_mono1' Texp_Var) also have "… = record_call x ⋅(prognosis ae as a (Γ, Var x, S))" by simp finally show "prognosis ae as u (delete x Γ, e, Upd x # S) ⊑ record_call x⋅(prognosis ae as a (Γ, Var x, S))" by this simp_all next fix Γ :: heap and e :: exp and ae :: AEnv and x :: var and as S assume "isVal e" hence "repeatable (Texp e⋅0)" by (rule Fun_repeatable) assume [simp]: "x ∉ domA Γ" have [simp]: "thunks ((x, e) # Γ) = thunks Γ" using `isVal e` by (auto simp add: thunks_Cons dest: set_mp[OF thunks_domA]) have "fup⋅(Texp e)⋅(ae x) ⊑ Texp e⋅0" by (metis fup2 monofun_cfun_arg up_zero_top) hence "substitute ((FBinds Γ⋅ae)(x := fup⋅(Texp e)⋅(ae x))) (thunks Γ) (Texp e⋅0 ⊗⊗ Fstack as S) ⊑ substitute ((FBinds Γ⋅ae)(x := Texp e⋅0)) (thunks Γ) (Texp e⋅0 ⊗⊗ Fstack as S)" by (intro substitute_mono1' fun_upd_mono below_refl monofun_cfun_arg) also have "… = substitute (((FBinds Γ⋅ae)(x := Texp e⋅0))(x := empty)) (thunks Γ) (Texp e⋅0 ⊗⊗ Fstack as S)" using `repeatable (Texp e⋅0)` by (rule substitute_remove_anyways, simp) also have "((FBinds Γ⋅ae)(x := Texp e⋅0))(x := empty) = FBinds Γ⋅ae" by (simp add: fun_upd_idem Texp.AnalBinds_not_there empty_is_bottom) finally show "prognosis ae as 0 ((x, e) # Γ, e, S) ⊑ prognosis ae as 0 (Γ, e, Upd x # S)" by (simp, intro pathsCard_mono' paths_mono) qed sublocale CardinalityPrognosisIfThenElse prognosis proof fix ae as Γ scrut e1 e2 S a have "Texp scrut⋅0 ⊗⊗ (Texp e1⋅a ⊕⊕ Texp e2⋅a) ⊑ Texp (scrut ? e1 : e2)⋅a" by (rule Texp_IfThenElse) hence "substitute (FBinds Γ⋅ae) (thunks Γ) (Texp scrut⋅0 ⊗⊗ (Texp e1⋅a ⊕⊕ Texp e2⋅a) ⊗⊗ Fstack as S) ⊑ substitute (FBinds Γ⋅ae) (thunks Γ) (Texp (scrut ? e1 : e2)⋅a ⊗⊗ Fstack as S)" by (rule substitute_mono2'[OF both_mono1']) thus "prognosis ae (a#as) 0 (Γ, scrut, Alts e1 e2 # S) ⊑ prognosis ae as a (Γ, scrut ? e1 : e2, S)" by (simp, intro pathsCard_mono' paths_mono) next fix ae as a Γ b e1 e2 S have "Texp (if b then e1 else e2)⋅a ⊑ Texp e1⋅a ⊕⊕ Texp e2⋅a" by (auto simp add: either_above_arg1 either_above_arg2) hence "substitute (FBinds Γ⋅ae) (thunks Γ) (Texp (if b then e1 else e2)⋅a ⊗⊗ Fstack as S) ⊑ substitute (FBinds Γ⋅ae) (thunks Γ) (Texp (Bool b)⋅0 ⊗⊗ (Texp e1⋅a ⊕⊕ Texp e2⋅a) ⊗⊗ Fstack as S)" by (rule substitute_mono2'[OF both_mono1'[OF below_trans[OF _ both_above_arg2]]]) thus "prognosis ae as a (Γ, if b then e1 else e2, S) ⊑ prognosis ae (a#as) 0 (Γ, Bool b, Alts e1 e2 # S)" by (auto intro!: pathsCard_mono' paths_mono) qed end context TTreeAnalysisCardinalityHeap begin definition cHeap where "cHeap Γ e = (Λ a. pathsCard (paths (Theap Γ e⋅a)))" lemma cHeap_simp: "(cHeap Γ e)⋅a = pathsCard (paths (Theap Γ e⋅a))" unfolding cHeap_def by (rule beta_cfun) (intro cont2cont) sublocale CardinalityHeap cHeap. sublocale CardinalityHeapSafe cHeap Aheap proof fix x Γ e a assume "x ∈ thunks Γ" moreover assume "many ⊑ (cHeap Γ e⋅a) x" hence "many ⊑ pathsCard (paths (Theap Γ e ⋅a)) x" unfolding cHeap_def by simp hence "∃p∈ (paths (Theap Γ e⋅a)). ¬ (one_call_in_path x p)" unfolding pathsCard_def by (auto split: if_splits) ultimately show "(Aheap Γ e⋅a) x = up⋅0" by (metis Theap_thunk) next fix Γ e a show "edom (cHeap Γ e⋅a) = edom (Aheap Γ e⋅a)" by (simp add: cHeap_def Union_paths_carrier carrier_Fheap) qed sublocale CardinalityPrognosisEdom prognosis proof fix ae as a Γ e S show "edom (prognosis ae as a (Γ, e, S)) ⊆ fv Γ ∪ fv e ∪ fv S" apply (simp add: Union_paths_carrier) apply (rule carrier_substitute_below) apply (auto simp add: carrier_Fexp dest: set_mp[OF Aexp_edom] set_mp[OF carrier_Fstack] set_mp[OF ap_fv_subset] set_mp[OF carrier_FBinds]) done qed sublocale CardinalityPrognosisLet prognosis cHeap proof fix Δ Γ :: heap and e :: exp and S :: stack and ae :: AEnv and a :: Arity and as assume "atom ` domA Δ ♯* Γ" assume "atom ` domA Δ ♯* S" assume "edom ae ⊆ domA Γ ∪ upds S" have "domA Δ ∩ edom ae = {}" using fresh_distinct[OF `atom \` domA Δ ♯* Γ`] fresh_distinct_fv[OF `atom \` domA Δ ♯* S`] `edom ae ⊆ domA Γ ∪ upds S` ups_fv_subset[of S] by auto have const_on1: "⋀ x. const_on (FBinds Δ⋅(Aheap Δ e⋅a)) (carrier ((FBinds Γ⋅ae) x)) empty" unfolding const_on_edom_disj using fresh_distinct_fv[OF `atom \` domA Δ ♯* Γ`] by (auto dest!: set_mp[OF carrier_FBinds] set_mp[OF Texp.edom_AnalBinds]) have const_on2: "const_on (FBinds Δ⋅(Aheap Δ e⋅a)) (carrier (Fstack as S)) empty" unfolding const_on_edom_disj using fresh_distinct_fv[OF `atom \` domA Δ ♯* S`] by (auto dest!: set_mp[OF carrier_FBinds] set_mp[OF carrier_Fstack] set_mp[OF Texp.edom_AnalBinds] set_mp[OF ap_fv_subset ]) have const_on3: "const_on (FBinds Γ⋅ae) (- (- domA Δ)) TTree.empty" and const_on4: "const_on (FBinds Δ⋅(Aheap Δ e⋅a)) (domA Γ) TTree.empty" unfolding const_on_edom_disj using fresh_distinct[OF `atom \` domA Δ ♯* Γ`] by (auto dest!: set_mp[OF Texp.edom_AnalBinds]) have disj1: "⋀ x. carrier ((FBinds Γ⋅ae) x) ∩ domA Δ = {}" using fresh_distinct_fv[OF `atom \` domA Δ ♯* Γ`] by (auto dest: set_mp[OF carrier_FBinds]) hence disj1': "⋀ x. carrier ((FBinds Γ⋅ae) x) ⊆ - domA Δ" by auto have disj2: "⋀ x. carrier (Fstack as S) ∩ domA Δ = {}" using fresh_distinct_fv[OF `atom \` domA Δ ♯* S`] by (auto dest!: set_mp[OF carrier_Fstack]) hence disj2': "carrier (Fstack as S) ⊆ - domA Δ" by auto { fix x have "(FBinds (Δ @ Γ)⋅(ae ⊔ Aheap Δ e⋅a)) x = (FBinds Γ⋅ae) x ⊗⊗ (FBinds Δ⋅(Aheap Δ e⋅a)) x" proof (cases "x ∈ domA Δ") case True have "map_of Γ x = None" using True fresh_distinct[OF `atom \` domA Δ ♯* Γ`] by (metis disjoint_iff_not_equal domA_def map_of_eq_None_iff) moreover have "ae x = ⊥" using True `domA Δ ∩ edom ae = {}` by auto ultimately show ?thesis using True by (auto simp add: Texp.AnalBinds_lookup empty_is_bottom[symmetric] cong: option.case_cong) next case False have "map_of Δ x = None" using False by (metis domA_def map_of_eq_None_iff) moreover have "(Aheap Δ e⋅a) x = ⊥" using False using edom_Aheap by (metis contra_subsetD edomIff) ultimately show ?thesis using False by (auto simp add: Texp.AnalBinds_lookup empty_is_bottom[symmetric] cong: option.case_cong) qed } note FBinds = ext[OF this] { have "pathsCard (paths (substitute (FBinds (Δ @ Γ)⋅(Aheap Δ e⋅a ⊔ ae)) (thunks (Δ @ Γ)) (Texp e⋅a ⊗⊗ Fstack as S))) = pathsCard (paths (substitute (FBinds Γ⋅ae) (thunks (Δ @ Γ)) (substitute (FBinds Δ⋅(Aheap Δ e⋅a)) (thunks (Δ @ Γ)) (Texp e⋅a ⊗⊗ Fstack as S))))" by (simp add: substitute_substitute[OF const_on1] FBinds) also have "substitute (FBinds Γ⋅ae) (thunks (Δ @ Γ)) = substitute (FBinds Γ⋅ae) (thunks Γ)" apply (rule substitute_cong_T) using const_on3 by (auto dest: set_mp[OF thunks_domA]) also have "substitute (FBinds Δ⋅(Aheap Δ e⋅a)) (thunks (Δ @ Γ)) = substitute (FBinds Δ⋅(Aheap Δ e⋅a)) (thunks Δ)" apply (rule substitute_cong_T) using const_on4 by (auto dest: set_mp[OF thunks_domA]) also have "substitute (FBinds Δ⋅(Aheap Δ e⋅a)) (thunks Δ) (Texp e⋅a ⊗⊗ Fstack as S) = substitute (FBinds Δ⋅(Aheap Δ e⋅a)) (thunks Δ) (Texp e⋅a) ⊗⊗ Fstack as S" by (rule substitute_only_empty_both[OF const_on2]) also note calculation } note eq_imp_below[OF this] also note env_restr_split[where S = "domA Δ"] also have "pathsCard (paths (substitute (FBinds Γ⋅ae) (thunks Γ) (substitute (FBinds Δ⋅(Aheap Δ e⋅a)) (thunks Δ) (Texp e⋅a) ⊗⊗ Fstack as S))) f|` domA Δ = pathsCard (paths (ttree_restr (domA Δ) (substitute (FBinds Δ⋅(Aheap Δ e⋅a)) (thunks Δ) (Texp e⋅a))))" by (simp add: filter_paths_conv_free_restr ttree_restr_both ttree_rest_substitute[OF disj1] ttree_restr_is_empty[OF disj2]) also have "ttree_restr (domA Δ) (substitute (FBinds Δ⋅(Aheap Δ e⋅a)) (thunks Δ) (Texp e⋅a)) ⊑ Theap Δ e⋅a" by (rule Theap_substitute) also have "pathsCard (paths (substitute (FBinds Γ⋅ae) (thunks Γ) (substitute (FBinds Δ⋅(Aheap Δ e⋅a)) (thunks Δ) (Texp e⋅a) ⊗⊗ Fstack as S))) f|` (- domA Δ) = pathsCard (paths (substitute (FBinds Γ⋅ae) (thunks Γ) (ttree_restr (- domA Δ) (substitute (FBinds Δ⋅(Aheap Δ e⋅a)) (thunks Δ) (Texp e⋅a)) ⊗⊗ Fstack as S)))" by (simp add: filter_paths_conv_free_restr2 ttree_rest_substitute2[OF disj1' const_on3] ttree_restr_both ttree_restr_noop[OF disj2']) also have "ttree_restr (- domA Δ) (substitute (FBinds Δ⋅(Aheap Δ e⋅a)) (thunks Δ) (Texp e⋅a)) ⊑ Texp (Terms.Let Δ e)⋅a" by (rule Texp_Let) finally show "prognosis (Aheap Δ e⋅a ⊔ ae) as a (Δ @ Γ, e, S) ⊑ cHeap Δ e⋅a ⊔ prognosis ae as a (Γ, Terms.Let Δ e, S)" by (simp add: cHeap_def del: fun_meet_simp) qed sublocale CardinalityPrognosisSafe prognosis cHeap Aheap Aexp .. end end