theory CoCallImplSafe imports CoCallAnalysisImpl CoCallAnalysisSpec ArityAnalysisFixProps begin locale CoCallImplSafe begin sublocale CoCallAnalysisImpl. lemma ccNeighbors_Int_ccrestr: "(ccNeighbors x G ∩ S) = ccNeighbors x (cc_restr (insert x S) G) ∩ S" by transfer auto lemma assumes "x ∉ S" and "y ∉ S" shows CCexp_subst: "cc_restr S (CCexp e[y::=x]⋅a) = cc_restr S (CCexp e⋅a)" and Aexp_restr_subst: "(Aexp e[y::=x]⋅a) f|` S = (Aexp e⋅a) f|` S" using assms proof (nominal_induct e avoiding: x y arbitrary: a S rule: exp_strong_induct_rec_set) case (Var b v) case 1 show ?case by auto case 2 thus ?case by auto next case (App e v) case 1 with App show ?case by (auto simp add: Int_insert_left fv_subst_int simp del: join_comm intro: join_mono) case 2 with App show ?case by (auto simp add: env_restr_join simp del: fun_meet_simp) next case (Lam v e) case 1 with Lam show ?case by (auto simp add: CCexp_pre_simps cc_restr_predCC Diff_Int_distrib2 fv_subst_int env_restr_join env_delete_env_restr_swap[symmetric] simp del: CCexp_simps) case 2 with Lam show ?case by (auto simp add: env_restr_join env_delete_env_restr_swap[symmetric] simp del: fun_meet_simp) next case (Let Γ e x y) hence [simp]: "x ∉ domA Γ " "y ∉ domA Γ" by (metis (erased, hide_lams) bn_subst domA_not_fresh fresh_def fresh_star_at_base fresh_star_def obtain_fresh subst_is_fresh(2))+ note Let(1,2)[simp] from Let(3) have "¬ nonrec (Γ[y::h=x])" by (simp add: nonrec_subst) case [simp]: 1 have "cc_restr (S ∪ domA Γ) (CCfix Γ[y::h=x]⋅(Afix Γ[y::h=x]⋅(Aexp e[y::=x]⋅a ⊔ (λ_. up⋅0) f|` thunks Γ), CCexp e[y::=x]⋅a)) = cc_restr (S ∪ domA Γ) (CCfix Γ⋅ (Afix Γ⋅ (Aexp e⋅ a ⊔ (λ_. up⋅0) f|` thunks Γ), CCexp e⋅ a))" apply (subst CCfix_restr_subst') apply (erule Let(4)) apply auto[5] apply (subst CCfix_restr) back apply simp apply (subst Afix_restr_subst') apply (erule Let(5)) apply auto[5] apply (subst Afix_restr) back apply simp apply (simp only: env_restr_join) apply (subst Let(7)) apply auto[2] apply (subst Let(6)) apply auto[2] apply rule done thus ?case using Let(1,2) `¬ nonrec Γ` `¬ nonrec (Γ[y::h=x])` by (auto simp add: fresh_star_Pair elim: cc_restr_eq_subset[rotated] ) case [simp]: 2 have "Afix Γ[y::h=x]⋅(Aexp e[y::=x]⋅a ⊔ (λ_. up⋅0) f|` (thunks Γ)) f|` (S ∪ domA Γ) = Afix Γ⋅(Aexp e⋅a ⊔ (λ_. up⋅0) f|` (thunks Γ)) f|` (S ∪ domA Γ)" apply (subst Afix_restr_subst') apply (erule Let(5)) apply auto[5] apply (subst Afix_restr) back apply auto[1] apply (simp only: env_restr_join) apply (subst Let(7)) apply auto[2] apply rule done thus ?case using Let(1,2) using `¬ nonrec Γ` `¬ nonrec (Γ[y::h=x])` by (auto simp add: fresh_star_Pair elim:env_restr_eq_subset[rotated]) next case (Let_nonrec x' e exp x y) from Let_nonrec(1,2) have "x ≠ x'" "y ≠ x'" by (simp_all add: fresh_at_base) note Let_nonrec(1,2)[simp] from `x' ∉ fv e` `y ≠ x'` `x ≠ x'` have [simp]: "x' ∉ fv (e[y::=x])" by (auto simp add: fv_subst_eq) note `x' ∉ fv e`[simp] `y ≠ x'` [simp]`x ≠ x'` [simp] case [simp]: 1 have "⋀ a. cc_restr {x'} (CCexp exp[y::=x]⋅a) = cc_restr {x'} (CCexp exp⋅a)" by (rule Let_nonrec(6)) auto from arg_cong[where f = "λx. x'--x'∈x", OF this] have [simp]: "x'--x'∈CCexp exp[y::=x]⋅a ⟷ x'--x'∈CCexp exp⋅a" by auto have [simp]: "⋀ a. Aexp e[y::=x]⋅a f|` S = Aexp e⋅a f|` S" by (rule Let_nonrec(5)) auto have [simp]: "⋀ a. fup⋅(Aexp e[y::=x])⋅a f|` S = fup⋅(Aexp e)⋅a f|` S" by (case_tac a) auto have [simp]: "Aexp exp[y::=x]⋅a f|` S = Aexp exp⋅a f|` S" by (rule Let_nonrec(7)) auto have "Aexp exp[y::=x]⋅a f|` {x'} = Aexp exp⋅a f|` {x'}" by (rule Let_nonrec(7)) auto from fun_cong[OF this, where x = x'] have [simp]: "(Aexp exp[y::=x]⋅a) x' = (Aexp exp⋅a) x'" by auto have [simp]: "⋀ a. cc_restr S (CCexp exp[y::=x]⋅a) = cc_restr S (CCexp exp⋅a)" by (rule Let_nonrec(6)) auto have [simp]: "⋀ a. cc_restr S (CCexp e[y::=x]⋅a) = cc_restr S (CCexp e⋅a)" by (rule Let_nonrec(4)) auto have [simp]: "⋀ a. cc_restr S (fup⋅(CCexp e[y::=x])⋅a) = cc_restr S (fup⋅(CCexp e)⋅a)" by (rule fup_ccExp_restr_subst') simp have [simp]: "fv e[y::=x] ∩ S = fv e ∩ S" by (auto simp add: fv_subst_eq) have [simp]: "ccNeighbors x' (CCexp exp[y::=x]⋅a) ∩ - {x'} ∩ S = ccNeighbors x' (CCexp exp⋅a) ∩ - {x'} ∩ S" apply (simp only: Int_assoc) apply (subst (1 2) ccNeighbors_Int_ccrestr) apply (subst Let_nonrec(6)) apply auto[2] apply rule done have [simp]: "ccNeighbors x' (CCexp exp[y::=x]⋅a) ∩ S = ccNeighbors x' (CCexp exp⋅a) ∩ S" apply (subst (1 2) ccNeighbors_Int_ccrestr) apply (subst Let_nonrec(6)) apply auto[2] apply rule done show "cc_restr S (CCexp (let x' be e in exp )[y::=x]⋅a) = cc_restr S (CCexp (let x' be e in exp )⋅a)" apply (subst subst_let_be) apply auto[2] apply (subst (1 2) CCexp_simps(6)) apply fact+ apply (simp only: cc_restr_cc_delete_twist) apply (rule arg_cong) back apply (simp add: Diff_eq ccBind_eq ABind_nonrec_eq) done show "Aexp (let x' be e in exp )[y::=x]⋅a f|` S = Aexp (let x' be e in exp )⋅a f|` S" by (simp add: env_restr_join env_delete_env_restr_swap[symmetric] ABind_nonrec_eq) next case (IfThenElse scrut e1 e2) case [simp]: 2 from IfThenElse show "cc_restr S (CCexp (scrut ? e1 : e2)[y::=x]⋅a) = cc_restr S (CCexp (scrut ? e1 : e2)⋅a)" by (auto simp del: edom_env env_restr_empty env_restr_empty_iff simp add: edom_env[symmetric]) from IfThenElse(2,4,6) show "Aexp (scrut ? e1 : e2)[y::=x]⋅a f|` S = Aexp (scrut ? e1 : e2)⋅a f|` S" by (auto simp add: env_restr_join simp del: fun_meet_simp) qed auto sublocale ArityAnalysisSafe Aexp by standard (simp_all add:Aexp_restr_subst) sublocale ArityAnalysisLetSafe Aexp Aheap proof fix Γ e a show "edom (Aheap Γ e⋅a) ⊆ domA Γ" by (cases "nonrec Γ") (auto simp add: Aheap_nonrec_simp dest: set_mp[OF edom_esing_subset] elim!: nonrecE) next fix x y :: var and Γ :: heap and e :: exp assume assms: "x ∉ domA Γ" "y ∉ domA Γ" from Aexp_restr_subst[OF assms(2,1)] have **: "⋀ a. Aexp e[x::=y]⋅a f|` domA Γ = Aexp e⋅a f|` domA Γ". show "Aheap Γ[x::h=y] e[x::=y] = Aheap Γ e" proof(cases "nonrec Γ") case [simp]: False from assms have "atom ` domA Γ ♯* x" and "atom ` domA Γ ♯* y" by (auto simp add: fresh_star_at_base image_iff) hence [simp]: "¬ nonrec (Γ[x::h=y])" by (simp add: nonrec_subst) show ?thesis apply (rule cfun_eqI) apply simp apply (subst Afix_restr_subst[OF assms subset_refl]) apply (subst Afix_restr[OF subset_refl]) back apply (simp add: env_restr_join) apply (subst **) apply simp done next case True from assms have "atom ` domA Γ ♯* x" and "atom ` domA Γ ♯* y" by (auto simp add: fresh_star_at_base image_iff) with True have *: "nonrec (Γ[x::h=y])" by (simp add: nonrec_subst) from True obtain x' e' where [simp]: "Γ = [(x',e')]" "x' ∉ fv e'" by (auto elim: nonrecE) from * have [simp]: "x' ∉ fv (e'[x::=y])" by (auto simp add: nonrec_def) from fun_cong[OF **, where x = x'] have [simp]: "⋀ a. (Aexp e[x::=y]⋅a) x' = (Aexp e⋅a) x'" by simp from CCexp_subst[OF assms(2,1)] have "⋀ a. cc_restr {x'} (CCexp e[x::=y]⋅a) = cc_restr {x'} (CCexp e⋅a)" by simp from arg_cong[where f = "λx. x'--x'∈x", OF this] have [simp]: "⋀ a. x'--x'∈(CCexp e[x::=y]⋅a) ⟷ x'--x'∈(CCexp e⋅a)" by simp show ?thesis apply - apply (rule cfun_eqI) apply (auto simp add: Aheap_nonrec_simp ABind_nonrec_eq) done qed next fix Γ e a show "ABinds Γ⋅(Aheap Γ e⋅a) ⊔ Aexp e⋅a ⊑ Aheap Γ e⋅a ⊔ Aexp (Let Γ e)⋅a" proof(cases "nonrec Γ") case False thus ?thesis by (auto simp add: Aheap_def join_below_iff env_restr_join2 Compl_partition intro: below_trans[OF _ Afix_above_arg]) next case True then obtain x e' where [simp]: "Γ = [(x,e')]" "x ∉ fv e'" by (auto elim: nonrecE) hence "⋀ a. x ∉ edom (fup⋅(Aexp e')⋅a)" by (auto dest:set_mp[OF fup_Aexp_edom]) hence [simp]: "⋀ a. (fup⋅(Aexp e')⋅a) x = ⊥" by (simp add: edomIff) show ?thesis apply (rule env_restr_below_split[where S = "{x}"]) apply (rule env_restr_belowI2) apply (auto simp add: Aheap_nonrec_simp join_below_iff env_restr_join env_delete_restr) apply (rule ABind_nonrec_above_arg) apply (rule below_trans[OF _ join_above2]) apply (rule below_trans[OF _ join_above2]) apply (rule below_refl) done qed qed definition ccHeap_nonrec where "ccHeap_nonrec x e exp = (Λ n. CCfix_nonrec x e⋅(Aexp exp⋅n, CCexp exp⋅n))" lemma ccHeap_nonrec_eq: "ccHeap_nonrec x e exp⋅n = CCfix_nonrec x e⋅(Aexp exp⋅n, CCexp exp⋅n)" unfolding ccHeap_nonrec_def by (rule beta_cfun) (intro cont2cont) definition ccHeap_rec :: "heap ⇒ exp ⇒ Arity → CoCalls" where "ccHeap_rec Γ e = (Λ a. CCfix Γ⋅(Afix Γ⋅(Aexp e⋅a ⊔ (λ_.up⋅0) f|` (thunks Γ)), CCexp e⋅a))" lemma ccHeap_rec_eq: "ccHeap_rec Γ e⋅a = CCfix Γ⋅(Afix Γ⋅(Aexp e⋅a ⊔ (λ_.up⋅0) f|` (thunks Γ)), CCexp e⋅a)" unfolding ccHeap_rec_def by simp definition ccHeap :: "heap ⇒ exp ⇒ Arity → CoCalls" where "ccHeap Γ = (if nonrec Γ then case_prod ccHeap_nonrec (hd Γ) else ccHeap_rec Γ)" lemma ccHeap_simp1: "¬ nonrec Γ ⟹ ccHeap Γ e⋅a = CCfix Γ⋅(Afix Γ⋅(Aexp e⋅a ⊔ (λ_.up⋅0) f|` (thunks Γ)), CCexp e⋅a)" by (simp add: ccHeap_def ccHeap_rec_eq) lemma ccHeap_simp2: "x ∉ fv e ⟹ ccHeap [(x,e)] exp⋅n = CCfix_nonrec x e⋅(Aexp exp⋅n, CCexp exp⋅n)" by (simp add: ccHeap_def ccHeap_nonrec_eq nonrec_def) sublocale CoCallAritySafe CCexp Aexp ccHeap Aheap proof fix e a x show "CCexp e⋅(inc⋅a) ⊔ ccProd {x} (insert x (fv e)) ⊑ CCexp (App e x)⋅a" by simp next fix y e n show "cc_restr (fv (Lam [y]. e)) (CCexp e⋅(pred⋅n)) ⊑ CCexp (Lam [y]. e)⋅n" by (auto simp add: CCexp_pre_simps predCC_eq dest!: set_mp[OF ccField_cc_restr] simp del: CCexp_simps) next fix x y :: var and S e a assume "x ∉ S" and "y ∉ S" thus "cc_restr S (CCexp e[y::=x]⋅a) ⊑ cc_restr S (CCexp e⋅a)" by (rule eq_imp_below[OF CCexp_subst]) next fix e assume "isVal e" thus "CCexp e⋅0 = ccSquare (fv e)" by (induction e rule: isVal.induct) (auto simp add: predCC_eq) next fix Γ e a show "cc_restr (- domA Γ) (ccHeap Γ e⋅a) ⊑ CCexp (Let Γ e)⋅a" proof(cases "nonrec Γ") case False thus "cc_restr (- domA Γ) (ccHeap Γ e⋅a) ⊑ CCexp (Let Γ e)⋅a" by (simp add: ccHeap_simp1[OF False, symmetric] del: cc_restr_join) next case True thus ?thesis by (auto simp add: ccHeap_simp2 Diff_eq elim!: nonrecE simp del: cc_restr_join) qed next fix Δ :: heap and e a show "CCexp e⋅a ⊑ ccHeap Δ e⋅a" by (cases "nonrec Δ") (auto simp add: ccHeap_simp1 ccHeap_simp2 arg_cong[OF CCfix_unroll, where f = "op ⊑ x" for x ] elim!: nonrecE) fix x e' a' assume "map_of Δ x = Some e'" hence [simp]: "x ∈ domA Δ" by (metis domI dom_map_of_conv_domA) assume "(Aheap Δ e⋅a) x = up⋅a'" show "CCexp e'⋅a' ⊑ ccHeap Δ e⋅a" proof(cases "nonrec Δ") case False from `(Aheap Δ e⋅a) x = up⋅a'` False have "(Afix Δ⋅(Aexp e⋅a ⊔ (λ_.up⋅0)f|` (thunks Δ))) x = up⋅a'" by (simp add: Aheap_def) hence "CCexp e'⋅a' ⊑ ccBind x e'⋅(Afix Δ⋅(Aexp e⋅a ⊔ (λ_.up⋅0)f|` (thunks Δ)), CCfix Δ⋅(Afix Δ⋅(Aexp e⋅a ⊔ (λ_.up⋅0)f|` (thunks Δ)), CCexp e⋅a))" by (auto simp add: ccBind_eq dest: set_mp[OF ccField_CCexp]) also have "ccBind x e'⋅(Afix Δ⋅(Aexp e⋅a ⊔ (λ_.up⋅0)f|` (thunks Δ)), CCfix Δ⋅(Afix Δ⋅(Aexp e⋅a ⊔ (λ_.up⋅0)f|` (thunks Δ)), CCexp e⋅a)) ⊑ ccHeap Δ e⋅a" using `map_of Δ x = Some e'` False by (fastforce simp add: ccHeap_simp1 ccHeap_rec_eq ccBindsExtra_simp ccBinds_eq arg_cong[OF CCfix_unroll, where f = "op ⊑ x" for x ] intro: below_trans[OF _ join_above2]) finally show "CCexp e'⋅a' ⊑ ccHeap Δ e⋅a" by this simp_all next case True with `map_of Δ x = Some e'` have [simp]: "Δ = [(x,e')]" "x ∉ fv e'" by (auto elim!: nonrecE split: if_splits) show ?thesis proof(cases "x--x∉CCexp e⋅a ∨ isVal e'") case True with `(Aheap Δ e⋅a) x = up⋅a'` have [simp]: "(CoCallArityAnalysis.Aexp cCCexp e⋅a) x = up⋅a'" by (auto simp add: Aheap_nonrec_simp ABind_nonrec_eq split: if_splits) have "CCexp e'⋅a' ⊑ ccSquare (fv e')" unfolding below_ccSquare by (rule ccField_CCexp) then show ?thesis using True by (auto simp add: ccHeap_simp2 ccBind_eq Aheap_nonrec_simp ABind_nonrec_eq below_trans[OF _ join_above2] simp del: below_ccSquare ) next case False from `(Aheap Δ e⋅a) x = up⋅a'` have [simp]: "a' = 0" using False by (auto simp add: Aheap_nonrec_simp ABind_nonrec_eq split: if_splits) show ?thesis using False by (auto simp add: ccHeap_simp2 ccBind_eq Aheap_nonrec_simp ABind_nonrec_eq simp del: below_ccSquare ) qed qed show "ccProd (fv e') (ccNeighbors x (ccHeap Δ e⋅a) - {x} ∩ thunks Δ) ⊑ ccHeap Δ e⋅a" proof (cases "nonrec Δ") case [simp]: False have "ccProd (fv e') (ccNeighbors x (ccHeap Δ e⋅a) - {x} ∩ thunks Δ) ⊑ ccProd (fv e') (ccNeighbors x (ccHeap Δ e⋅a))" by (rule ccProd_mono2) auto also have "… ⊑ (⨆x↦e'∈map_of Δ. ccProd (fv e') (ccNeighbors x (ccHeap Δ e⋅a)))" using `map_of Δ x = Some e'` by (rule below_lubmapI) also have "… ⊑ ccBindsExtra Δ⋅(Afix Δ⋅(Aexp e⋅a ⊔ (λ_.up⋅0)f|` (thunks Δ)), ccHeap Δ e⋅a)" by (simp add: ccBindsExtra_simp below_trans[OF _ join_above2]) also have "… ⊑ ccHeap Δ e⋅a" by (simp add: ccHeap_simp1 arg_cong[OF CCfix_unroll, where f = "op ⊑ x" for x]) finally show ?thesis by this simp_all next case True with `map_of Δ x = Some e'` have [simp]: "Δ = [(x,e')]" "x ∉ fv e'" by (auto elim!: nonrecE split: if_splits) have [simp]: "(ccNeighbors x (ccBind x e'⋅(Aexp e⋅a, CCexp e⋅a))) = {}" by (auto simp add: ccBind_eq dest!: set_mp[OF ccField_cc_restr] set_mp[OF ccField_fup_CCexp]) show ?thesis proof(cases "isVal e' ∧ x--x∈CCexp e⋅a") case True have "ccNeighbors x (ccHeap Δ e⋅a) = ccNeighbors x (ccBind x e'⋅(Aheap_nonrec x e'⋅(Aexp e⋅a, CCexp e⋅a), CCexp e⋅a)) ∪ ccNeighbors x (ccProd (fv e') (ccNeighbors x (CCexp e⋅a) - (if isVal e' then {} else {x}))) ∪ ccNeighbors x (CCexp e⋅a)" by (auto simp add: ccHeap_simp2 ) also have "ccNeighbors x (ccBind x e'⋅(Aheap_nonrec x e'⋅(Aexp e⋅a, CCexp e⋅a), CCexp e⋅a)) = {}" by (auto simp add: ccBind_eq dest!: set_mp[OF ccField_cc_restr] set_mp[OF ccField_fup_CCexp]) also have "ccNeighbors x (ccProd (fv e') (ccNeighbors x (CCexp e⋅a) - (if isVal e' then {} else {x}))) ⊆ ccNeighbors x (ccProd (fv e') (ccNeighbors x (CCexp e⋅a)))" by (simp add: ccNeighbors_ccProd) also have "… ⊆ fv e'" by (simp add: ccNeighbors_ccProd) finally have "ccNeighbors x (ccHeap Δ e⋅a) - {x} ∩ thunks Δ ⊆ ccNeighbors x (CCexp e⋅a) ∪ fv e'" by auto hence "ccProd (fv e') (ccNeighbors x (ccHeap Δ e⋅a) - {x} ∩ thunks Δ) ⊑ ccProd (fv e') (ccNeighbors x (CCexp e⋅a) ∪ fv e')" by (rule ccProd_mono2) also have "… ⊑ ccProd (fv e') (ccNeighbors x (CCexp e⋅a)) ⊔ ccProd (fv e') (fv e')" by simp also have "ccProd (fv e') (ccNeighbors x (CCexp e⋅a)) ⊑ ccHeap Δ e⋅a" using `map_of Δ x = Some e'` `(Aheap Δ e⋅a) x = up⋅a'` True by (auto simp add: ccHeap_simp2 below_trans[OF _ join_above2]) also have "ccProd (fv e') (fv e') = ccSquare (fv e')" by (simp add: ccSquare_def) also have "… ⊑ ccHeap Δ e⋅a" using `map_of Δ x = Some e'` `(Aheap Δ e⋅a) x = up⋅a'` True by (auto simp add: ccHeap_simp2 ccBind_eq below_trans[OF _ join_above2]) also note join_self finally show ?thesis by this simp_all next case False have "ccNeighbors x (ccHeap Δ e⋅a) = ccNeighbors x (ccBind x e'⋅(Aheap_nonrec x e'⋅(Aexp e⋅a, CCexp e⋅a), CCexp e⋅a)) ∪ ccNeighbors x (ccProd (fv e') (ccNeighbors x (CCexp e⋅a) - (if isVal e' then {} else {x}))) ∪ ccNeighbors x (CCexp e⋅a)" by (auto simp add: ccHeap_simp2 ) also have "ccNeighbors x (ccBind x e'⋅(Aheap_nonrec x e'⋅(Aexp e⋅a, CCexp e⋅a), CCexp e⋅a)) = {}" by (auto simp add: ccBind_eq dest!: set_mp[OF ccField_cc_restr] set_mp[OF ccField_fup_CCexp]) also have "ccNeighbors x (ccProd (fv e') (ccNeighbors x (CCexp e⋅a) - (if isVal e' then {} else {x}) )) = {}" using False by (auto simp add: ccNeighbors_ccProd) finally have "ccNeighbors x (ccHeap Δ e⋅a) ⊆ ccNeighbors x (CCexp e⋅a)" by auto hence"ccNeighbors x (ccHeap Δ e⋅a) - {x} ∩ thunks Δ ⊆ ccNeighbors x (CCexp e⋅a) - {x} ∩ thunks Δ" by auto hence "ccProd (fv e') (ccNeighbors x (ccHeap Δ e⋅a) - {x} ∩ thunks Δ ) ⊑ ccProd (fv e') (ccNeighbors x (CCexp e⋅a) - {x} ∩ thunks Δ )" by (rule ccProd_mono2) also have "… ⊑ ccHeap Δ e⋅a" using `map_of Δ x = Some e'` `(Aheap Δ e⋅a) x = up⋅a'` False by (auto simp add: ccHeap_simp2 thunks_Cons below_trans[OF _ join_above2]) finally show ?thesis by this simp_all qed qed next fix x Γ e a assume [simp]: "¬ nonrec Γ" assume "x ∈ thunks Γ" hence [simp]: "x ∈ domA Γ" by (rule set_mp[OF thunks_domA]) assume "x ∈ edom (Aheap Γ e⋅a)" from `x ∈ thunks Γ` have "(Afix Γ⋅(Aexp e⋅a ⊔ (λ_.up⋅0)f|` (thunks Γ))) x = up⋅0" by (subst Afix_unroll) simp thus "(Aheap Γ e⋅a) x = up⋅0" by simp next fix x Γ e a assume "nonrec Γ" then obtain x' e' where [simp]: "Γ = [(x',e')]" "x' ∉ fv e'" by (auto elim: nonrecE) assume "x ∈ thunks Γ" hence [simp]: "x = x'" "¬ isVal e'" by (auto simp add: thunks_Cons split: if_splits) assume "x--x ∈ CCexp e⋅a" hence [simp]: "x'--x'∈ CCexp e⋅a" by simp from `x ∈ thunks Γ` have "(Afix Γ⋅(Aexp e⋅a ⊔ (λ_.up⋅0)f|` (thunks Γ))) x = up⋅0" by (subst Afix_unroll) simp show "(Aheap Γ e⋅a) x = up⋅0" by (auto simp add: Aheap_nonrec_simp ABind_nonrec_eq) next fix scrut e1 a e2 show "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 simp qed end end