Theory TransformTools

theory TransformTools
imports "Launchbury.Nominal-HOLCF" Launchbury.Terms Launchbury.Substitution Launchbury.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!: subsetD[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!: subsetD[OF supp_lift_transform])

  lemma fresh_transform[intro]: "a ♯ e ⟹ a ♯ trans n e"
    by (auto simp add: fresh_def) (auto dest!: subsetD[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