Theory AbstractTransform

theory AbstractTransform
imports Launchbury.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!: subsetD[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!: subsetD[OF supp_eqvt_at[OF prems(2)], rotated] subsetD[OF SuppTransLet] subsetD[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: subsetD[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: subsetD[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