theory AbstractTransform imports "Terms" TransformTools begin locale AbstractAnalProp = fixes PropApp :: "'a ⇒ 'a::cont_pt" fixes PropLam :: "'a ⇒ 'a" fixes AnalLet :: "heap ⇒ exp ⇒ 'a ⇒ 'b::cont_pt" fixes PropLetBody :: "'b ⇒ 'a" fixes PropLetHeap :: "'b⇒ var ⇒ 'a⇩⊥" fixes PropIfScrut :: "'a ⇒ 'a" assumes PropApp_eqvt: "π ∙ PropApp ≡ PropApp" assumes PropLam_eqvt: "π ∙ PropLam ≡ PropLam" assumes AnalLet_eqvt: "π ∙ AnalLet ≡ AnalLet" assumes PropLetBody_eqvt: "π ∙ PropLetBody ≡ PropLetBody" assumes PropLetHeap_eqvt: "π ∙ PropLetHeap ≡ PropLetHeap" assumes PropIfScrut_eqvt: "π ∙ PropIfScrut ≡ PropIfScrut" locale AbstractAnalPropSubst = AbstractAnalProp + assumes AnalLet_subst: "x ∉ domA Γ ⟹ y ∉ domA Γ ⟹ AnalLet (Γ[x::h=y]) (e[x::=y]) a = AnalLet Γ e a" locale AbstractTransform = AbstractAnalProp + constrains AnalLet :: "heap ⇒ exp ⇒ 'a::pure_cont_pt ⇒ 'b::cont_pt" fixes TransVar :: "'a ⇒ var ⇒ exp" fixes TransApp :: "'a ⇒ exp ⇒ var ⇒ exp" fixes TransLam :: "'a ⇒ var ⇒ exp ⇒ exp" fixes TransLet :: "'b ⇒ heap ⇒ exp ⇒ exp" assumes TransVar_eqvt: "π ∙ TransVar = TransVar" assumes TransApp_eqvt: "π ∙ TransApp = TransApp" assumes TransLam_eqvt: "π ∙ TransLam = TransLam" assumes TransLet_eqvt: "π ∙ TransLet = TransLet" assumes SuppTransLam: "supp (TransLam a v e) ⊆ supp e - supp v" assumes SuppTransLet: "supp (TransLet b Γ e) ⊆ supp (Γ, e) - atom ` domA Γ" begin nominal_function transform where "transform a (App e x) = TransApp a (transform (PropApp a) e) x" | "transform a (Lam [x]. e) = TransLam a x (transform (PropLam a) e)" | "transform a (Var x) = TransVar a x" | "transform a (Let Γ e) = TransLet (AnalLet Γ e a) (map_transform transform (PropLetHeap (AnalLet Γ e a)) Γ) (transform (PropLetBody (AnalLet Γ e a)) e)" | "transform a (Bool b) = (Bool b)" | "transform a (scrut ? e1 : e2) = (transform (PropIfScrut a) scrut ? transform a e1 : transform a e2)" proof goal_cases case 1 note PropApp_eqvt[eqvt_raw] PropLam_eqvt[eqvt_raw] PropLetBody_eqvt[eqvt_raw] PropLetHeap_eqvt[eqvt_raw] AnalLet_eqvt[eqvt_raw] TransVar_eqvt[eqvt] TransApp_eqvt[eqvt] TransLam_eqvt[eqvt] TransLet_eqvt[eqvt] show ?case unfolding eqvt_def transform_graph_aux_def apply rule apply perm_simp apply (rule refl) done next case prems: (3 P x) show ?case proof (cases x) fix a b assume "x = (a, b)" thus ?case using prems apply (cases b rule:Terms.exp_strong_exhaust) apply auto done qed next case prems: (10 a x e a' x' e') from prems(5) have "a' = a" and "Lam [x]. e = Lam [x']. e'" by simp_all from this(2) show ?case unfolding `a' = a` proof(rule eqvt_lam_case) fix π :: perm have "supp (TransLam a x (transform_sumC (PropLam a, e))) ⊆ supp (Lam [x]. e)" apply (rule subset_trans[OF SuppTransLam]) apply (auto simp add: exp_assn.supp supp_Pair supp_at_base pure_supp exp_assn.fsupp dest!: set_mp[OF supp_eqvt_at[OF prems(1)], rotated]) done moreover assume "supp π ♯* (Lam [x]. e)" ultimately have *: "supp π ♯* TransLam a x (transform_sumC (PropLam a, e))" by (auto simp add: fresh_star_def fresh_def) note PropApp_eqvt[eqvt_raw] PropLam_eqvt[eqvt_raw] PropLetBody_eqvt[eqvt_raw] PropLetHeap_eqvt[eqvt_raw] TransVar_eqvt[eqvt] TransApp_eqvt[eqvt] TransLam_eqvt[eqvt] TransLet_eqvt[eqvt] have "TransLam a (π ∙ x) (transform_sumC (PropLam a, π ∙ e)) = TransLam a (π ∙ x) (transform_sumC (π ∙ (PropLam a, e)))" by perm_simp rule also have "… = TransLam a (π ∙ x) (π ∙ transform_sumC (PropLam a, e))" unfolding eqvt_at_apply'[OF prems(1)] .. also have "… = π ∙ (TransLam a x (transform_sumC (PropLam a, e)))" by simp also have "… = TransLam a x (transform_sumC (PropLam a, e))" by (rule perm_supp_eq[OF *]) finally show "TransLam a (π ∙ x) (transform_sumC (PropLam a, π ∙ e)) = TransLam a x (transform_sumC (PropLam a, e))" by simp qed next case prems: (19 a as body a' as' body') note PropApp_eqvt[eqvt_raw] PropLam_eqvt[eqvt_raw] PropLetBody_eqvt[eqvt_raw] AnalLet_eqvt[eqvt_raw] PropLetHeap_eqvt[eqvt_raw] TransVar_eqvt[eqvt] TransApp_eqvt[eqvt] TransLam_eqvt[eqvt] TransLet_eqvt[eqvt] from supp_eqvt_at[OF prems(1)] have "⋀ x e a. (x, e) ∈ set as ⟹ supp (transform_sumC (a, e)) ⊆ supp e" by (auto simp add: exp_assn.fsupp supp_Pair pure_supp) hence supp_map: "⋀ae. supp (map_transform (λx0 x1. transform_sumC (x0, x1)) ae as) ⊆ supp as" by (rule supp_map_transform_step) from prems(9) have "a' = a" and "Terms.Let as body = Terms.Let as' body'" by simp_all from this(2) show ?case unfolding `a' = a` proof (rule eqvt_let_case) have "supp (TransLet (AnalLet as body a) (map_transform (λx0 x1. transform_sumC (x0, x1)) (PropLetHeap (AnalLet as body a)) as) (transform_sumC (PropLetBody (AnalLet as body a), body))) ⊆ supp (Let as body)" by (auto simp add: Let_supp supp_Pair pure_supp exp_assn.fsupp dest!: set_mp[OF supp_eqvt_at[OF prems(2)], rotated] set_mp[OF SuppTransLet] set_mp[OF supp_map]) moreover fix π :: perm assume "supp π ♯* Terms.Let as body" ultimately have *: "supp π ♯* TransLet (AnalLet as body a) (map_transform (λx0 x1. transform_sumC (x0, x1)) (PropLetHeap (AnalLet as body a)) as) (transform_sumC (PropLetBody (AnalLet as body a), body))" by (auto simp add: fresh_star_def fresh_def) have "TransLet (AnalLet (π ∙ as) (π ∙ body) a) (map_transform (λx0 x1. (π ∙ transform_sumC) (x0, x1)) (PropLetHeap (AnalLet (π ∙ as) (π ∙ body) a)) (π ∙ as)) ((π ∙ transform_sumC) (PropLetBody (AnalLet (π ∙ as) (π ∙ body) a), π ∙ body)) = π ∙ TransLet (AnalLet as body a) (map_transform (λx0 x1. transform_sumC (x0, x1)) (PropLetHeap (AnalLet as body a)) as) (transform_sumC (PropLetBody (AnalLet as body a), body))" by (simp del: Let_eq_iff Pair_eqvt add: eqvt_at_apply[OF prems(2)]) also have "… = TransLet (AnalLet as body a) (map_transform (λx0 x1. transform_sumC (x0, x1)) (PropLetHeap (AnalLet as body a)) as) (transform_sumC (PropLetBody (AnalLet as body a), body))" by (rule perm_supp_eq[OF *]) also have "map_transform (λx0 x1. transform_sumC (x0, x1)) (PropLetHeap (AnalLet (π ∙ as) (π ∙ body) a)) (π ∙ as) = map_transform (λx xa. (π ∙ transform_sumC) (x, xa)) (PropLetHeap (AnalLet (π ∙ as) (π ∙ body) a)) (π ∙ as)" apply (rule map_transform_fundef_cong[OF _ refl refl]) apply (subst (asm) set_eqvt[symmetric]) apply (subst (asm) mem_permute_set) apply (auto simp add: permute_self dest: eqvt_at_apply''[OF prems(1)[where aa = "(- π ∙ a)" for a], where p = π, symmetric]) done moreover have "(π ∙ transform_sumC) (PropLetBody (AnalLet (π ∙ as) (π ∙ body) a), π ∙ body) = transform_sumC (PropLetBody (AnalLet (π ∙ as) (π ∙ body) a), π ∙ body)" using eqvt_at_apply''[OF prems(2), where p = π] by perm_simp ultimately show "TransLet (AnalLet (π ∙ as) (π ∙ body) a) (map_transform (λx0 x1. transform_sumC (x0, x1)) (PropLetHeap (AnalLet (π ∙ as) (π ∙ body) a)) (π ∙ as)) (transform_sumC (PropLetBody (AnalLet (π ∙ as) (π ∙ body) a), π ∙ body)) = TransLet (AnalLet as body a) (map_transform (λx0 x1. transform_sumC (x0, x1)) (PropLetHeap (AnalLet as body a)) as) (transform_sumC (PropLetBody (AnalLet as body a), body))" by metis qed qed auto nominal_termination by lexicographic_order lemma supp_transform: "supp (transform a e) ⊆ supp e" proof- note PropApp_eqvt[eqvt_raw] PropLam_eqvt[eqvt_raw] PropLetBody_eqvt[eqvt_raw] AnalLet_eqvt[eqvt_raw] PropLetHeap_eqvt[eqvt_raw] TransVar_eqvt[eqvt] TransApp_eqvt[eqvt] TransLam_eqvt[eqvt] TransLet_eqvt[eqvt] note transform.eqvt[eqvt] show ?thesis apply (rule supp_fun_app_eqvt) apply (rule eqvtI) apply perm_simp apply (rule reflexive) done qed lemma fv_transform: "fv (transform a e) ⊆ fv e" unfolding fv_def by (auto dest: set_mp[OF supp_transform]) end locale AbstractTransformSubst = AbstractTransform + AbstractAnalPropSubst + assumes TransVar_subst: "(TransVar a v)[x ::= y] = (TransVar a v[x ::v= y])" assumes TransApp_subst: "(TransApp a e v)[x ::= y] = (TransApp a e[x ::= y] v[x ::v= y])" assumes TransLam_subst: "atom v ♯ (x,y) ⟹ (TransLam a v e)[x ::= y] = (TransLam a v[x ::v= y] e[x ::= y])" assumes TransLet_subst: "atom ` domA Γ ♯* (x,y) ⟹ (TransLet b Γ e)[x ::= y] = (TransLet b Γ[x ::h= y] e[x ::= y])" begin lemma subst_transform: "(transform a e)[x ::= y] = transform a e[x ::= y]" proof (nominal_induct e avoiding: x y arbitrary: a rule: exp_strong_induct_set) case (Let Δ body x y) hence *: "x ∉ domA Δ" "y ∉ domA Δ" by (auto simp add: fresh_star_def fresh_at_base) hence "AnalLet Δ[x::h=y] body[x::=y] a = AnalLet Δ body a" by (rule AnalLet_subst) with Let show ?case apply (auto simp add: fresh_star_Pair TransLet_subst simp del: Let_eq_iff) apply (rule fun_cong[OF arg_cong[where f = "TransLet b" for b]]) apply (rule subst_map_transform) apply simp done qed (simp_all add: TransVar_subst TransApp_subst TransLam_subst) end locale AbstractTransformBound = AbstractAnalProp + supp_bounded_transform + constrains PropApp :: "'a ⇒ 'a::pure_cont_pt" constrains PropLetHeap :: "'b::cont_pt ⇒ var ⇒ 'a⇩⊥" constrains trans :: "'c::cont_pt ⇒ exp ⇒ exp" fixes PropLetHeapTrans :: "'b⇒ var ⇒ 'c⇩⊥" assumes PropLetHeapTrans_eqvt: "π ∙ PropLetHeapTrans = PropLetHeapTrans" assumes TransBound_eqvt: "π ∙ trans = trans" begin sublocale AbstractTransform PropApp PropLam AnalLet PropLetBody PropLetHeap PropIfScrut "(λ a. Var)" "(λ a. App)" "(λ a. Terms.Lam)" "(λ b Γ e . Let (map_transform trans (PropLetHeapTrans b) Γ) e)" proof goal_cases case 1 note PropApp_eqvt[eqvt_raw] PropLam_eqvt[eqvt_raw] PropLetBody_eqvt[eqvt_raw] PropLetHeap_eqvt[eqvt_raw] PropIfScrut_eqvt[eqvt_raw] AnalLet_eqvt[eqvt_raw] PropLetHeapTrans_eqvt[eqvt] TransBound_eqvt[eqvt] show ?case apply standard apply ((perm_simp, rule)+)[4] apply (auto simp add: exp_assn.supp supp_at_base)[1] apply (auto simp add: Let_supp supp_Pair supp_at_base dest: set_mp[OF supp_map_transform])[1] done qed lemma isLam_transform[simp]: "isLam (transform a e) ⟷ isLam e" by (induction e rule:isLam.induct) auto lemma isVal_transform[simp]: "isVal (transform a e) ⟷ isVal e" by (induction e rule:isLam.induct) auto end locale AbstractTransformBoundSubst = AbstractAnalPropSubst + AbstractTransformBound + assumes TransBound_subst: "(trans a e)[x::=y] = trans a e[x::=y]" begin sublocale AbstractTransformSubst PropApp PropLam AnalLet PropLetBody PropLetHeap PropIfScrut "(λ a. Var)" "(λ a. App)" "(λ a. Terms.Lam)" "(λ b Γ e . Let (map_transform trans (PropLetHeapTrans b) Γ) e)" proof goal_cases case 1 note PropApp_eqvt[eqvt_raw] PropLam_eqvt[eqvt_raw] PropLetBody_eqvt[eqvt_raw] PropLetHeap_eqvt[eqvt_raw] PropIfScrut_eqvt[eqvt_raw] TransBound_eqvt[eqvt] show ?case apply standard apply simp_all[3] apply (simp del: Let_eq_iff) apply (rule arg_cong[where f = "λ x. Let x y" for y]) apply (rule subst_map_transform) apply (simp add: TransBound_subst) done qed end end