theory CallArityEnd2EndSafe imports CallArityEnd2End CardArityTransformSafe CoCallImplSafe CoCallImplTTreeSafe TTreeImplCardinalitySafe begin locale CallArityEnd2EndSafe begin sublocale CoCallImplSafe. sublocale CallArityEnd2End. abbreviation transform_syn' ("𝒯⇘_⇙") where "𝒯⇘a⇙ ≡ transform a" lemma end2end: "c ⇒⇧* c' ⟹ ¬ boring_step c' ⟹ heap_upds_ok_conf c ⟹ consistent (ae, ce, a, as, r) c ⟹ ∃ae' ce' a' as' r'. consistent (ae', ce', a', as', r') c' ∧ conf_transform (ae, ce, a, as, r) c ⇒⇩G⇧* conf_transform (ae', ce', a', as', r') c'" by (rule card_arity_transform_safe) theorem end2end_closed: assumes closed: "fv e = ({} :: var set)" assumes "([], e, []) ⇒⇧* (Γ,v,[])" and "isVal v" obtains Γ' and v' where "([], 𝒯⇘0⇙ e, []) ⇒⇧* (Γ',v',[])" and "isVal v'" and "card (domA Γ') ≤ card (domA Γ)" proof- note assms(2) moreover have "¬ boring_step (Γ,v,[])" by (simp add: boring_step.simps) moreover have "heap_upds_ok_conf ([], e, [])" by simp moreover have "consistent (⊥,⊥,0,[],[]) ([], e, [])" using closed by (rule closed_consistent) ultimately obtain ae ce a as r where *: "consistent (ae, ce, a, as, r) (Γ,v,[])" and **: "conf_transform (⊥, ⊥, 0, [], []) ([],e,[]) ⇒⇩G⇧* conf_transform (ae, ce, a, as, r) (Γ,v,[])" by (metis end2end) let ?Γ = "map_transform Aeta_expand ae (map_transform transform ae (restrictA (-set r) Γ))" let ?v = "transform a v" from * have "set r ⊆ domA Γ" by auto have "conf_transform (⊥, ⊥, 0, [], []) ([],e,[]) = ([],transform 0 e,[])" by simp with ** have "([], transform 0 e, []) ⇒⇩G⇧* (?Γ, ?v, map Dummy (rev r))" by simp have "isVal ?v" using `isVal v` by simp have "fv (transform 0 e) = ({} :: var set)" using closed by (auto dest: set_mp[OF fv_transform]) note sestoftUnGC'[OF `([], transform 0 e, []) ⇒⇩G⇧* (?Γ, ?v, map Dummy (rev r))` `isVal ?v` `fv (transform 0 e) = {}`] then obtain Γ' where "([], transform 0 e, []) ⇒⇧* (Γ', ?v, [])" and "?Γ = restrictA (- set r) Γ'" and "set r ⊆ domA Γ'" by auto have "card (domA Γ) = card (domA ?Γ ∪ (set r ∩ domA Γ))" by (rule arg_cong[where f = card]) auto also have "… = card (domA ?Γ) + card (set r ∩ domA Γ)" by (rule card_Un_disjoint) auto also note `?Γ = restrictA (- set r) Γ'` also have "set r ∩ domA Γ = set r ∩ domA Γ'" using `set r ⊆ domA Γ` `set r ⊆ domA Γ'` by auto also have "card (domA (restrictA (- set r) Γ')) + card (set r ∩ domA Γ') = card (domA Γ')" by (subst card_Un_disjoint[symmetric]) (auto intro: arg_cong[where f = card]) finally have "card (domA Γ') ≤ card (domA Γ)" by simp with `([], transform 0 e, []) ⇒⇧* (Γ', ?v, [])` `isVal ?v` show thesis using that by blast qed lemma fresh_var_eqE[elim_format]: "fresh_var e = x ⟹ x ∉ fv e" by (metis fresh_var_not_free) lemma example1: fixes e :: exp fixes f g x y z :: var assumes Aexp_e: "⋀a. Aexp e⋅a = esing x⋅(up⋅a) ⊔ esing y⋅(up⋅a)" assumes ccExp_e: "⋀a. CCexp e⋅a = ⊥" assumes [simp]: "transform 1 e = e" assumes "isVal e" assumes disj: "y ≠ f" "y ≠ g" "x ≠ y" "z ≠ f" "z ≠ g" "y ≠ x" assumes fresh: "atom z ♯ e" shows "transform 1 (let y be App (Var f) g in (let x be e in (Var x))) = let y be (Lam [z]. App (App (Var f) g) z) in (let x be (Lam [z]. App e z) in (Var x))" proof- from arg_cong[where f = edom, OF Aexp_e] have "x ∈ fv e" by simp (metis Aexp_edom' insert_subset) hence [simp]: "¬ nonrec [(x,e)]" by (simp add: nonrec_def) from `isVal e` have [simp]: "thunks [(x, e)] = {}" by (simp add: thunks_Cons) have [simp]: "CCfix [(x, e)]⋅(esing x⋅(up⋅1) ⊔ esing y⋅(up⋅1), ⊥) = ⊥" unfolding CCfix_def apply (simp add: fix_bottom_iff ccBindsExtra_simp) apply (simp add: ccBind_eq disj ccExp_e) done have [simp]: "Afix [(x, e)]⋅(esing x⋅(up⋅1)) = esing x⋅(up⋅1) ⊔ esing y⋅(up⋅1)" unfolding Afix_def apply simp apply (rule fix_eqI) apply (simp add: disj Aexp_e) apply (case_tac "z x") apply (auto simp add: disj Aexp_e) done have [simp]: "Aheap [(y, App (Var f) g)] (let x be e in Var x)⋅1 = esing y⋅((Aexp (let x be e in Var x )⋅1) y)" by (auto simp add: Aheap_nonrec_simp ABind_nonrec_eq pure_fresh fresh_at_base disj) have [simp]: "(Aexp (let x be e in Var x)⋅1) = esing y⋅(up⋅1)" by (simp add: env_restr_join disj) have [simp]: "Aheap [(x, e)] (Var x)⋅1 = esing x⋅(up⋅1)" by (simp add: env_restr_join disj) have [simp]: "Aeta_expand 1 (App (Var f) g) = (Lam [z]. App (App (Var f) g) z)" apply (simp add: one_is_inc_zero del: exp_assn.eq_iff) apply (subst change_Lam_Variable[of z "fresh_var (App (Var f) g)"]) apply (auto simp add: fresh_Pair fresh_at_base pure_fresh disj intro!: flip_fresh_fresh elim!: fresh_var_eqE) done have [simp]: "Aeta_expand 1 e = (Lam [z]. App e z)" apply (simp add: one_is_inc_zero del: exp_assn.eq_iff) apply (subst change_Lam_Variable[of z "fresh_var e"]) apply (auto simp add: fresh_Pair fresh_at_base pure_fresh disj fresh intro!: flip_fresh_fresh elim!: fresh_var_eqE) done show ?thesis by (simp del: Let_eq_iff add: map_transform_Cons disj[symmetric]) qed end end