theory NoCardinalityAnalysis imports CardinalityAnalysisSpec ArityAnalysisStack begin locale NoCardinalityAnalysis = ArityAnalysisLetSafe + assumes Aheap_thunk: "x ∈ thunks Γ ⟹ (Aheap Γ e⋅a) x = up⋅0" begin definition a2c :: "Arity⇩⊥ → two" where "a2c = (Λ a. if a ⊑ ⊥ then ⊥ else many)" lemma a2c_simp: "a2c⋅a = (if a ⊑ ⊥ then ⊥ else many)" unfolding a2c_def by (rule beta_cfun[OF cont_if_else_above]) auto lemma a2c_eqvt[eqvt]: "π ∙ a2c = a2c" unfolding a2c_def apply perm_simp apply (rule Abs_cfun_eqvt) apply (rule cont_if_else_above) apply auto done definition ae2ce :: "AEnv ⇒ (var ⇒ two)" where "ae2ce ae x = a2c⋅(ae x)" lemma ae2ce_cont: "cont ae2ce" by (auto simp add: ae2ce_def) lemmas cont_compose[OF ae2ce_cont, cont2cont, simp] lemma ae2ce_eqvt[eqvt]: "π ∙ ae2ce ae x = ae2ce (π ∙ ae) (π ∙ x)" unfolding ae2ce_def by perm_simp rule lemma ae2ce_to_env_restr: "ae2ce ae = (λ_ . many) f|` edom ae" by (auto simp add: ae2ce_def lookup_env_restr_eq edom_def a2c_simp) lemma edom_ae2ce[simp]: "edom (ae2ce ae) = edom ae" unfolding edom_def by (auto simp add: ae2ce_def a2c_simp) definition cHeap :: "heap ⇒ exp ⇒ Arity → (var ⇒ two)" where "cHeap Γ e = (Λ a. ae2ce (Aheap Γ e⋅a))" lemma cHeap_simp[simp]: "cHeap Γ e⋅a = ae2ce (Aheap Γ e⋅a)" unfolding cHeap_def by simp sublocale CardinalityHeap cHeap. sublocale CardinalityHeapSafe cHeap Aheap apply standard apply (erule Aheap_thunk) apply simp done fun prognosis where "prognosis ae as a (Γ, e, S) = ((λ_. many) f|` (edom (ABinds Γ⋅ae) ∪ edom (Aexp e⋅a) ∪ edom (AEstack as S)))" lemma record_all_noop[simp]: "record_call x⋅((λ_. many) f|` S) = (λ_. many) f|` S" by (auto simp add: record_call_def lookup_env_restr_eq) lemma const_on_restr_constI[intro]: "S' ⊆ S ⟹ const_on ((λ _. x) f|` S) S' x" by fastforce lemma ap_subset_edom_AEstack: "ap S ⊆ edom (AEstack as S)" by (induction as S rule:AEstack.induct) (auto simp del: fun_meet_simp) sublocale CardinalityPrognosis prognosis. sublocale CardinalityPrognosisShape prognosis proof (standard, goal_cases) case 1 thus ?case by (simp cong: Abinds_env_restr_cong) next case 2 thus ?case by (simp cong: Abinds_reorder) next case 3 thus ?case by (auto dest: set_mp[OF ap_subset_edom_AEstack]) next case 4 thus ?case by (auto intro: env_restr_mono2 ) next case (5 ae x as a Γ e S) from `ae x = ⊥` have "ABinds (delete x Γ)⋅ae = ABinds Γ⋅ae" by (rule ABinds_delete_bot) thus ?case by simp next case (6 ae as a Γ x S) from Aexp_Var[where n = a and x = x] have "(Aexp (Var x)⋅a) x ≠ ⊥" by auto hence "x ∈ edom (Aexp (Var x)⋅a)" by (simp add: edomIff) thus ?case by simp qed sublocale CardinalityPrognosisApp prognosis proof (standard, goal_cases) case 1 thus ?case using edom_mono[OF Aexp_App] by (auto intro!: env_restr_mono2) qed sublocale CardinalityPrognosisLam prognosis proof (standard, goal_cases) case (1 ae as a Γ e y x S) have "edom (Aexp e[y::=x]⋅(pred⋅a)) ⊆ insert x (edom (env_delete y (Aexp e⋅(pred⋅a))))" by (auto dest: set_mp[OF edom_mono[OF Aexp_subst]] ) also have "… ⊆ insert x (edom (Aexp (Lam [y]. e)⋅a))" using edom_mono[OF Aexp_Lam] by auto finally show ?case by (auto intro!: env_restr_mono2) qed sublocale CardinalityPrognosisVar prognosis proof (standard, goal_cases) case prems: 1 thus ?case by (auto intro!: env_restr_mono2 simp add: Abinds_reorder1[OF prems(1)]) next case prems: 2 thus ?case by (auto intro!: env_restr_mono2 simp add: Abinds_reorder1[OF prems(1)]) (metis Aexp_Var edomIff not_up_less_UU) next case (3 e x Γ ae as S) have "fup⋅(Aexp e)⋅(ae x) ⊑ Aexp e⋅0" by (cases "ae x") (auto intro: monofun_cfun_arg) from edom_mono[OF this] show ?case by (auto intro!: env_restr_mono2 dest: set_mp[OF edom_mono[OF ABinds_delete_below]]) qed sublocale CardinalityPrognosisIfThenElse prognosis proof (standard, goal_cases) case (1 ae a as Γ scrut e1 e2 S) have "edom (Aexp scrut⋅0 ⊔ Aexp e1⋅a ⊔ Aexp e2⋅a) ⊆ edom (Aexp (scrut ? e1 : e2)⋅a)" by (rule edom_mono[OF Aexp_IfThenElse]) thus ?case by (auto intro!: env_restr_mono2) next case (2 ae as a Γ b e1 e2 S) show ?case by (auto intro!: env_restr_mono2) qed sublocale CardinalityPrognosisLet prognosis cHeap Aheap proof (standard, goal_cases) case prems: (1 Δ Γ S ae e a as) from set_mp[OF prems(3)] fresh_distinct[OF prems(1)] fresh_distinct_fv[OF prems(2)] have "ae f|` domA Δ = ⊥" by (auto dest: set_mp[OF ups_fv_subset]) hence [simp]: "ABinds Δ⋅(ae ⊔ Aheap Δ e⋅a) = ABinds Δ⋅(Aheap Δ e⋅a)" by (simp cong: Abinds_env_restr_cong add: env_restr_join) from fresh_distinct[OF prems(1)] have "Aheap Δ e⋅a f|` domA Γ = ⊥" by (auto dest!: set_mp[OF edom_Aheap]) hence [simp]: "ABinds Γ⋅(ae ⊔ Aheap Δ e⋅a) = ABinds Γ⋅ae" by (simp cong: Abinds_env_restr_cong add: env_restr_join) have "edom (ABinds (Δ @ Γ)⋅(Aheap Δ e⋅a ⊔ ae)) ∪ edom (Aexp e⋅a) = edom (ABinds Δ⋅(Aheap Δ e⋅a)) ∪ edom (ABinds Γ⋅ae) ∪ edom (Aexp e⋅a) " by (simp add: Abinds_append_disjoint[OF fresh_distinct[OF prems(1)]] Un_commute) also have "… = edom (ABinds Γ⋅ae) ∪ edom (ABinds Δ⋅(Aheap Δ e⋅a) ⊔ Aexp e⋅a)" by force also have "… ⊆ edom (ABinds Γ⋅ae) ∪ edom (Aheap Δ e⋅a ⊔ Aexp (Let Δ e)⋅a)" using edom_mono[OF Aexp_Let] by force also have "… = edom (Aheap Δ e⋅a) ∪ edom (ABinds Γ⋅ae) ∪ edom (Aexp (Let Δ e)⋅a)" by auto finally have "edom (ABinds (Δ @ Γ)⋅(Aheap Δ e⋅a ⊔ ae)) ∪ edom (Aexp e⋅a) ⊆ edom (Aheap Δ e⋅a) ∪ edom (ABinds Γ⋅ae) ∪ edom (Aexp (Let Δ e)⋅a)". hence "edom (ABinds (Δ @ Γ)⋅(Aheap Δ e⋅a ⊔ ae)) ∪ edom (Aexp e⋅a) ∪ edom (AEstack as S) ⊆ edom (Aheap Δ e⋅a) ∪ edom (ABinds Γ⋅ae) ∪ edom (Aexp (Let Δ e)⋅a) ∪ edom (AEstack as S)" by auto thus ?case by (simp add: ae2ce_to_env_restr env_restr_join2 Un_assoc[symmetric] env_restr_mono2) qed sublocale CardinalityPrognosisEdom prognosis by standard (auto dest: set_mp[OF Aexp_edom] set_mp[OF ap_fv_subset] set_mp[OF edom_AnalBinds] set_mp[OF edom_AEstack]) sublocale CardinalityPrognosisSafe prognosis cHeap Aheap Aexp.. end end