theory CoCallFix imports CoCallAnalysisSig CoCallAnalysisBinds ArityAnalysisSig "Env-Nominal" ArityAnalysisFix begin locale CoCallArityAnalysis = fixes cccExp :: "exp ⇒ (Arity → AEnv × CoCalls)" begin definition Aexp :: "exp ⇒ (Arity → AEnv)" where "Aexp e = (Λ a. fst (cccExp e ⋅ a))" sublocale ArityAnalysis Aexp. abbreviation Aexp_syn' ("𝒜⇘_⇙") where "𝒜⇘a⇙ ≡ (λe. Aexp e⋅a)" abbreviation Aexp_bot_syn' ("𝒜⇧⊥⇘_⇙") where "𝒜⇧⊥⇘a⇙ ≡ (λe. fup⋅(Aexp e)⋅a)" lemma Aexp_eq: "𝒜⇘a⇙ e = fst (cccExp e ⋅ a)" unfolding Aexp_def by (rule beta_cfun) (intro cont2cont) lemma fup_Aexp_eq: "fup⋅(Aexp e)⋅a = fst (fup⋅(cccExp e)⋅a)" by (cases a)(simp_all add: Aexp_eq) definition CCexp :: "exp ⇒ (Arity → CoCalls)" where "CCexp Γ = (Λ a. snd (cccExp Γ⋅a))" lemma CCexp_eq: "CCexp e⋅a = snd (cccExp e ⋅ a)" unfolding CCexp_def by (rule beta_cfun) (intro cont2cont) lemma fup_CCexp_eq: "fup⋅(CCexp e)⋅a = snd (fup⋅(cccExp e)⋅a)" by (cases a)(simp_all add: CCexp_eq) sublocale CoCallAnalysis CCexp. definition CCfix :: "heap ⇒ (AEnv × CoCalls) → CoCalls" where "CCfix Γ = (Λ aeG. (μ G'. ccBindsExtra Γ⋅(fst aeG , G') ⊔ snd aeG))" lemma CCfix_eq: "CCfix Γ⋅(ae,G) = (μ G'. ccBindsExtra Γ⋅(ae, G') ⊔ G)" unfolding CCfix_def by simp lemma CCfix_unroll: "CCfix Γ⋅(ae,G) = ccBindsExtra Γ⋅(ae, CCfix Γ⋅(ae,G)) ⊔ G" unfolding CCfix_eq apply (subst fix_eq) apply simp done lemma fup_ccExp_restr_subst': assumes "⋀ a. cc_restr S (CCexp e[x::=y]⋅a) = cc_restr S (CCexp e⋅a)" shows "cc_restr S (fup⋅(CCexp e[x::=y])⋅a) = cc_restr S (fup⋅(CCexp e)⋅a)" using assms by (cases a) (auto simp del: cc_restr_cc_restr simp add: cc_restr_cc_restr[symmetric]) lemma ccBindsExtra_restr_subst': assumes "⋀ x' e a. (x',e) ∈ set Γ ⟹ cc_restr S (CCexp e[x::=y]⋅a) = cc_restr S (CCexp e⋅a)" assumes "x ∉ S" assumes "y ∉ S" assumes "domA Γ ⊆ S" shows "cc_restr S (ccBindsExtra Γ[x::h=y]⋅(ae, G)) = cc_restr S (ccBindsExtra Γ⋅(ae f|` S , cc_restr S G))" apply (simp add: ccBindsExtra_simp ccBinds_eq ccBind_eq Int_absorb2[OF assms(4)] fv_subst_int[OF assms(3,2)]) apply (intro arg_cong2[where f = "op ⊔"] refl arg_cong[OF mapCollect_cong]) apply (subgoal_tac "k ∈ S") apply (auto intro: fup_ccExp_restr_subst'[OF assms(1)[OF map_of_SomeD]] simp add: fv_subst_int[OF assms(3,2)] fv_subst_int2[OF assms(3,2)] ccSquare_def)[1] apply (metis assms(4) contra_subsetD domI dom_map_of_conv_domA) apply (subgoal_tac "k ∈ S") apply (auto intro: fup_ccExp_restr_subst'[OF assms(1)[OF map_of_SomeD]] simp add: fv_subst_int[OF assms(3,2)] fv_subst_int2[OF assms(3,2)] ccSquare_def cc_restr_twist[where S = S] simp del: cc_restr_cc_restr)[1] apply (subst fup_ccExp_restr_subst'[OF assms(1)[OF map_of_SomeD]], assumption) apply (simp add: fv_subst_int[OF assms(3,2)] fv_subst_int2[OF assms(3,2)] ) apply (subst fup_ccExp_restr_subst'[OF assms(1)[OF map_of_SomeD]], assumption) apply (simp add: fv_subst_int[OF assms(3,2)] fv_subst_int2[OF assms(3,2)] ) apply (metis assms(4) contra_subsetD domI dom_map_of_conv_domA) done lemma ccBindsExtra_restr: assumes "domA Γ ⊆ S" shows "cc_restr S (ccBindsExtra Γ⋅(ae, G)) = cc_restr S (ccBindsExtra Γ⋅(ae f|` S, cc_restr S G))" using assms apply (simp add: ccBindsExtra_simp ccBinds_eq ccBind_eq Int_absorb2) apply (intro arg_cong2[where f = "op ⊔"] refl arg_cong[OF mapCollect_cong]) apply (subgoal_tac "k ∈ S") apply simp apply (metis contra_subsetD domI dom_map_of_conv_domA) apply (subgoal_tac "k ∈ S") apply simp apply (metis contra_subsetD domI dom_map_of_conv_domA) done lemma CCfix_restr: assumes "domA Γ ⊆ S" shows "cc_restr S (CCfix Γ⋅(ae, G)) = cc_restr S (CCfix Γ⋅(ae f|` S, cc_restr S G))" unfolding CCfix_def apply simp apply (rule parallel_fix_ind[where P = "λ x y . cc_restr S x = cc_restr S y"]) apply simp apply rule apply simp apply (subst (1 2) ccBindsExtra_restr[OF assms]) apply (auto) done lemma ccField_CCfix: shows "ccField (CCfix Γ⋅(ae, G)) ⊆ fv Γ ∪ ccField G" unfolding CCfix_def apply simp apply (rule fix_ind[where P = "λ x . ccField x ⊆ fv Γ ∪ ccField G"]) apply (auto dest!: set_mp[OF ccField_ccBindsExtra]) done lemma CCfix_restr_subst': assumes "⋀ x' e a. (x',e) ∈ set Γ ⟹ cc_restr S (CCexp e[x::=y]⋅a) = cc_restr S (CCexp e⋅a)" assumes "x ∉ S" assumes "y ∉ S" assumes "domA Γ ⊆ S" shows "cc_restr S (CCfix Γ[x::h=y]⋅(ae, G)) = cc_restr S (CCfix Γ⋅(ae f|` S, cc_restr S G))" unfolding CCfix_def apply simp apply (rule parallel_fix_ind[where P = "λ x y . cc_restr S x = cc_restr S y"]) apply simp apply rule apply simp apply (subst ccBindsExtra_restr_subst'[OF assms], assumption) apply (subst ccBindsExtra_restr[OF assms(4)]) back apply (auto) done end lemma Aexp_eqvt[eqvt]: "π ∙ (CoCallArityAnalysis.Aexp cccExp e) = CoCallArityAnalysis.Aexp (π ∙ cccExp) (π ∙ e)" apply (rule cfun_eqvtI) unfolding CoCallArityAnalysis.Aexp_eq by perm_simp rule lemma CCexp_eqvt[eqvt]: "π ∙ (CoCallArityAnalysis.CCexp cccExp e) = CoCallArityAnalysis.CCexp (π ∙ cccExp) (π ∙ e)" apply (rule cfun_eqvtI) unfolding CoCallArityAnalysis.CCexp_eq by perm_simp rule lemma CCfix_eqvt[eqvt]: "π ∙ (CoCallArityAnalysis.CCfix cccExp Γ) = CoCallArityAnalysis.CCfix (π ∙ cccExp) (π ∙ Γ)" unfolding CoCallArityAnalysis.CCfix_def by perm_simp (simp_all add: Abs_cfun_eqvt) lemma ccFix_cong[fundef_cong]: "⟦ (⋀ e. e ∈ snd ` set heap2 ⟹ cccexp1 e = cccexp2 e); heap1 = heap2 ⟧ ⟹ CoCallArityAnalysis.CCfix cccexp1 heap1 = CoCallArityAnalysis.CCfix cccexp2 heap2" unfolding CoCallArityAnalysis.CCfix_def apply (rule arg_cong) back apply (rule ccBindsExtra_cong) apply (auto simp add: CoCallArityAnalysis.CCexp_def) done context CoCallArityAnalysis begin definition cccFix :: "heap ⇒ ((AEnv × CoCalls) → (AEnv × CoCalls))" where "cccFix Γ = (Λ i. (Afix Γ⋅(fst i ⊔ (λ_.up⋅0) f|` thunks Γ), CCfix Γ⋅(Afix Γ⋅(fst i ⊔ (λ_.up⋅0) f|` (thunks Γ)), snd i)))" lemma cccFix_eq: "cccFix Γ⋅i = (Afix Γ⋅(fst i ⊔ (λ_.up⋅0) f|` thunks Γ), CCfix Γ⋅(Afix Γ⋅(fst i ⊔ (λ_.up⋅0) f|` (thunks Γ)), snd i))" unfolding cccFix_def by (rule beta_cfun)(intro cont2cont) end lemma cccFix_eqvt[eqvt]: "π ∙ (CoCallArityAnalysis.cccFix cccExp Γ) = CoCallArityAnalysis.cccFix (π ∙ cccExp) (π ∙ Γ)" apply (rule cfun_eqvtI) unfolding CoCallArityAnalysis.cccFix_eq by perm_simp rule lemma cccFix_cong[fundef_cong]: "⟦ (⋀ e. e ∈ snd ` set heap2 ⟹ cccexp1 e = cccexp2 e); heap1 = heap2 ⟧ ⟹ CoCallArityAnalysis.cccFix cccexp1 heap1 = CoCallArityAnalysis.cccFix cccexp2 heap2" unfolding CoCallArityAnalysis.cccFix_def apply (rule cfun_eqI) apply auto apply (rule arg_cong[OF Afix_cong], auto simp add: CoCallArityAnalysis.Aexp_def)[1] apply (rule arg_cong2[OF ccFix_cong Afix_cong ]) apply (auto simp add: CoCallArityAnalysis.Aexp_def) done subsubsection {* The non-recursive case *} definition ABind_nonrec :: "var ⇒ exp ⇒ AEnv × CoCalls → Arity⇩⊥" where "ABind_nonrec x e = (Λ i. (if isVal e ∨ x--x∉(snd i) then fst i x else up⋅0))" lemma ABind_nonrec_eq: "ABind_nonrec x e⋅(ae,G) = (if isVal e ∨ x--x∉G then ae x else up⋅0)" unfolding ABind_nonrec_def apply (subst beta_cfun) apply (rule cont_if_else_above) apply auto by (metis in_join join_self_below(4)) lemma ABind_nonrec_eqvt[eqvt]: "π ∙ (ABind_nonrec x e) = ABind_nonrec (π ∙ x) (π ∙ e)" apply (rule cfun_eqvtI) apply (case_tac xa, simp) unfolding ABind_nonrec_eq by perm_simp rule lemma ABind_nonrec_above_arg: "ae x ⊑ ABind_nonrec x e ⋅ (ae, G)" unfolding ABind_nonrec_eq by auto definition Aheap_nonrec where "Aheap_nonrec x e = (Λ i. esing x⋅(ABind_nonrec x e⋅i))" lemma Aheap_nonrec_simp: "Aheap_nonrec x e⋅i = esing x⋅(ABind_nonrec x e⋅i)" unfolding Aheap_nonrec_def by simp lemma Aheap_nonrec_lookup[simp]: "(Aheap_nonrec x e⋅i) x = ABind_nonrec x e⋅i" unfolding Aheap_nonrec_simp by simp lemma Aheap_nonrec_eqvt'[eqvt]: "π ∙ (Aheap_nonrec x e) = Aheap_nonrec (π ∙ x) (π ∙ e)" apply (rule cfun_eqvtI) unfolding Aheap_nonrec_simp by (perm_simp, rule) context CoCallArityAnalysis begin definition Afix_nonrec where "Afix_nonrec x e = (Λ i. fup⋅(Aexp e)⋅(ABind_nonrec x e ⋅ i) ⊔ fst i)" lemma Afix_nonrec_eq[simp]: "Afix_nonrec x e ⋅ i = fup⋅(Aexp e)⋅(ABind_nonrec x e ⋅ i) ⊔ fst i" unfolding Afix_nonrec_def by (rule beta_cfun) simp definition CCfix_nonrec where "CCfix_nonrec x e = (Λ i. ccBind x e ⋅ (Aheap_nonrec x e⋅i, snd i) ⊔ ccProd (fv e) (ccNeighbors x (snd i) - (if isVal e then {} else {x})) ⊔ snd i)" lemma CCfix_nonrec_eq[simp]: "CCfix_nonrec x e ⋅ i = ccBind x e⋅(Aheap_nonrec x e⋅i, snd i) ⊔ ccProd (fv e) (ccNeighbors x (snd i) - (if isVal e then {} else {x})) ⊔ snd i" unfolding CCfix_nonrec_def by (rule beta_cfun) (intro cont2cont) definition cccFix_nonrec :: "var ⇒ exp ⇒ ((AEnv × CoCalls) → (AEnv × CoCalls))" where "cccFix_nonrec x e = (Λ i. (Afix_nonrec x e ⋅i , CCfix_nonrec x e ⋅i))" lemma cccFix_nonrec_eq[simp]: "cccFix_nonrec x e⋅i = (Afix_nonrec x e ⋅i , CCfix_nonrec x e ⋅i)" unfolding cccFix_nonrec_def by (rule beta_cfun) (intro cont2cont) end lemma AFix_nonrec_eqvt[eqvt]: "π ∙ (CoCallArityAnalysis.Afix_nonrec cccExp x e) = CoCallArityAnalysis.Afix_nonrec (π ∙ cccExp) (π ∙ x) (π ∙ e)" apply (rule cfun_eqvtI) unfolding CoCallArityAnalysis.Afix_nonrec_eq by perm_simp rule lemma CCFix_nonrec_eqvt[eqvt]: "π ∙ (CoCallArityAnalysis.CCfix_nonrec cccExp x e) = CoCallArityAnalysis.CCfix_nonrec (π ∙ cccExp) (π ∙ x) (π ∙ e)" apply (rule cfun_eqvtI) unfolding CoCallArityAnalysis.CCfix_nonrec_eq by perm_simp rule lemma cccFix_nonrec_eqvt[eqvt]: "π ∙ (CoCallArityAnalysis.cccFix_nonrec cccExp x e) = CoCallArityAnalysis.cccFix_nonrec (π ∙ cccExp) (π ∙ x) (π ∙ e)" apply (rule cfun_eqvtI) unfolding CoCallArityAnalysis.cccFix_nonrec_eq by perm_simp rule subsubsection {* Combining the cases *} context CoCallArityAnalysis begin definition cccFix_choose :: "heap ⇒ ((AEnv × CoCalls) → (AEnv × CoCalls))" where "cccFix_choose Γ = (if nonrec Γ then case_prod cccFix_nonrec (hd Γ) else cccFix Γ)" lemma cccFix_choose_simp1[simp]: "¬ nonrec Γ ⟹ cccFix_choose Γ = cccFix Γ" unfolding cccFix_choose_def by simp lemma cccFix_choose_simp2[simp]: "x ∉ fv e ⟹ cccFix_choose [(x,e)] = cccFix_nonrec x e" unfolding cccFix_choose_def nonrec_def by auto end lemma cccFix_choose_eqvt[eqvt]: "π ∙ (CoCallArityAnalysis.cccFix_choose cccExp Γ) = CoCallArityAnalysis.cccFix_choose (π ∙ cccExp) (π ∙ Γ)" unfolding CoCallArityAnalysis.cccFix_choose_def apply (cases nonrec π rule: eqvt_cases[where x = Γ]) apply (perm_simp, rule) apply simp apply (erule nonrecE) apply (simp ) apply simp done lemma cccFix_nonrec_cong[fundef_cong]: "cccexp1 e = cccexp2 e ⟹ CoCallArityAnalysis.cccFix_nonrec cccexp1 x e = CoCallArityAnalysis.cccFix_nonrec cccexp2 x e" apply (rule cfun_eqI) unfolding CoCallArityAnalysis.cccFix_nonrec_eq unfolding CoCallArityAnalysis.Afix_nonrec_eq unfolding CoCallArityAnalysis.CCfix_nonrec_eq unfolding CoCallArityAnalysis.fup_Aexp_eq apply (simp only: ) apply (rule arg_cong[OF ccBind_cong]) apply simp unfolding CoCallArityAnalysis.CCexp_def apply simp done lemma cccFix_choose_cong[fundef_cong]: "⟦ (⋀ e. e ∈ snd ` set heap2 ⟹ cccexp1 e = cccexp2 e); heap1 = heap2 ⟧ ⟹ CoCallArityAnalysis.cccFix_choose cccexp1 heap1 = CoCallArityAnalysis.cccFix_choose cccexp2 heap2" unfolding CoCallArityAnalysis.cccFix_choose_def apply (rule cfun_eqI) apply (auto elim!: nonrecE) apply (rule arg_cong[OF cccFix_nonrec_cong], auto) apply (rule arg_cong[OF cccFix_cong], auto)[1] done end