theory TransformTools imports "Nominal-HOLCF" "Terms" "Substitution" "Env" begin default_sort type fun lift_transform :: "('a::cont_pt ⇒ exp ⇒ exp) ⇒ ('a⇩⊥ ⇒ exp ⇒ exp)" where "lift_transform t Ibottom e = e" | "lift_transform t (Iup a) e = t a e" lemma lift_transform_simps[simp]: "lift_transform t ⊥ e = e" "lift_transform t (up⋅a) e = t a e" apply (metis inst_up_pcpo lift_transform.simps(1)) apply (simp add: up_def cont_Iup) done lemma lift_transform_eqvt[eqvt]: "π ∙ lift_transform t a e = lift_transform (π ∙ t) (π ∙ a) (π ∙ e)" by (cases "a") simp_all lemma lift_transform_fun_cong[fundef_cong]: "(⋀ a. t1 a e1 = t2 a e1) ⟹ a1 = a2 ⟹ e1 = e2 ⟹ lift_transform t1 a1 e1 = lift_transform t2 a2 e2" by (cases "(t2,a2,e2)" rule: lift_transform.cases) auto lemma subst_lift_transform: assumes "⋀ a. (t a e)[x ::= y] = t a (e[x ::= y])" shows "(lift_transform t a e)[x ::=y] = lift_transform t a (e[x ::= y])" using assms by (cases a) auto definition map_transform :: "('a::cont_pt ⇒ exp ⇒ exp) ⇒ (var ⇒ 'a⇩⊥) ⇒ heap ⇒ heap" where "map_transform t ae = map_ran (λ x e . lift_transform t (ae x) e)" lemma map_transform_eqvt[eqvt]: "π ∙ map_transform t ae = map_transform (π ∙ t) (π ∙ ae)" unfolding map_transform_def by simp lemma domA_map_transform[simp]: "domA (map_transform t ae Γ) = domA Γ" unfolding map_transform_def by simp lemma length_map_transform[simp]: "length (map_transform t ae xs) = length xs" unfolding map_transform_def map_ran_def by simp lemma map_transform_delete: "map_transform t ae (delete x Γ) = delete x (map_transform t ae Γ)" unfolding map_transform_def by (simp add: map_ran_delete) lemma map_transform_restrA: "map_transform t ae (restrictA S Γ) = restrictA S (map_transform t ae Γ)" unfolding map_transform_def by (auto simp add: map_ran_restrictA) lemma delete_map_transform_env_delete: "delete x (map_transform t (env_delete x ae) Γ) = delete x (map_transform t ae Γ)" unfolding map_transform_def by (induction Γ) auto lemma map_transform_Nil[simp]: "map_transform t ae [] = []" unfolding map_transform_def by simp lemma map_transform_Cons: "map_transform t ae ((x,e)# Γ) = (x, lift_transform t (ae x) e) # (map_transform t ae Γ)" unfolding map_transform_def by simp lemma map_transform_append: "map_transform t ae (Δ@Γ) = map_transform t ae Δ @ map_transform t ae Γ" unfolding map_transform_def by (simp add: map_ran_append) lemma map_transform_fundef_cong[fundef_cong]: "(⋀x e a. (x,e) ∈ set m1 ⟹ t1 a e = t2 a e) ⟹ ae1 = ae2 ⟹ m1 = m2 ⟹ map_transform t1 ae1 m1 = map_transform t2 ae2 m2" by (induction m2 arbitrary: m1) (fastforce simp add: map_transform_Nil map_transform_Cons intro!: lift_transform_fun_cong)+ lemma map_transform_cong: "(⋀x. x ∈ domA m1 ⟹ ae x = ae' x) ⟹ m1 = m2 ⟹ map_transform t ae m1 = map_transform t ae' m2" unfolding map_transform_def by (auto intro!: map_ran_cong dest: domA_from_set) lemma map_of_map_transform: "map_of (map_transform t ae Γ) x = map_option (lift_transform t (ae x)) (map_of Γ x)" unfolding map_transform_def by (simp add: map_ran_conv) lemma supp_map_transform_step: assumes "⋀ x e a. (x, e) ∈ set Γ ⟹ supp (t a e) ⊆ supp e" shows "supp (map_transform t ae Γ) ⊆ supp Γ" using assms apply (induction Γ) apply (auto simp add: supp_Nil supp_Cons map_transform_Nil map_transform_Cons supp_Pair pure_supp) apply (case_tac "ae a") apply (fastforce)+ done lemma subst_map_transform: assumes "⋀ x' e a. (x',e) : set Γ ⟹ (t a e)[x ::= y] = t a (e[x ::= y])" shows "(map_transform t ae Γ)[x ::h=y] = map_transform t ae (Γ[x ::h= y])" using assms apply (induction Γ) apply (auto simp add: map_transform_Nil map_transform_Cons) apply (subst subst_lift_transform) apply auto done locale supp_bounded_transform = fixes trans :: "'a::cont_pt ⇒ exp ⇒ exp" assumes supp_trans: "supp (trans a e) ⊆ supp e" begin lemma supp_lift_transform: "supp (lift_transform trans a e) ⊆ supp e" by (cases "(trans, a, e)" rule:lift_transform.cases) (auto dest!: set_mp[OF supp_trans]) lemma supp_map_transform: "supp (map_transform trans ae Γ) ⊆ supp Γ" unfolding map_transform_def by (induction Γ) (auto simp add: supp_Pair supp_Cons dest!: set_mp[OF supp_lift_transform]) lemma fresh_transform[intro]: "a ♯ e ⟹ a ♯ trans n e" by (auto simp add: fresh_def) (auto dest!: set_mp[OF supp_trans]) lemma fresh_star_transform[intro]: "a ♯* e ⟹ a ♯* trans n e" by (auto simp add: fresh_star_def) lemma fresh_map_transform[intro]: "a ♯ Γ ⟹ a ♯ map_transform trans ae Γ" unfolding fresh_def using supp_map_transform by auto lemma fresh_star_map_transform[intro]: "a ♯* Γ ⟹ a ♯* map_transform trans ae Γ" by (auto simp add: fresh_star_def) end end