Theory NU_PreEqu

(*<*)
theory NU_PreEqu
imports NU_Fresh
begin
(*>*)

section ‹Pre-Equality›

text ‹
  Defines the relation which captures the notion of alpha-equivalence (on open terms) 
  and proves this relation is an equivalence relation.
›

inductive equ :: "fresh_envs ⇒ trm ⇒ trm ⇒ bool" (" _ ⊢ _ ≈ _" [80,80,80] 80) where
equ_abst_ab[intro!]: "⟦a≠b;(nabla ⊢ a ♯ t2);(nabla ⊢ t1 ≈ (swap [(a,b)] t2))⟧ 
                      ⟹ (nabla ⊢ Abst a t1 ≈ Abst b t2)" |
equ_abst_aa[intro!]: "(nabla ⊢ t1 ≈ t2) ⟹ (nabla ⊢ Abst a t1 ≈ Abst a t2)" |
equ_unit[intro!]:    "(nabla ⊢ Unit ≈ Unit)" |
equ_atom[intro!]:    "a=b⟹nabla ⊢ Atom a ≈ Atom b" |
equ_susp[intro!]:    "(∀ c ∈ ds pi1 pi2. (c,X) ∈ nabla) ⟹ (nabla ⊢ Susp pi1 X ≈ Susp pi2 X)" |
equ_paar[intro!]:    "⟦(nabla ⊢ t1≈t2);(nabla ⊢ s1≈s2)⟧ ⟹ (nabla ⊢ Paar t1 s1 ≈ Paar t2 s2)" |
equ_func[intro!]:    "(nabla ⊢ t1 ≈ t2) ⟹ (nabla ⊢ Func F t1 ≈ Func F t2)"

inductive_cases Equ_elims:
"nabla ⊢ Atom a ≈ Atom b"
"nabla ⊢ Unit ≈ Unit"
"nabla ⊢ Susp pi1 X ≈ Susp pi2 X"
"nabla ⊢ Paar s1 t1 ≈ Paar s2 t2"
"nabla ⊢ Func F t1 ≈ Func F t2"
"nabla ⊢ Abst a t1 ≈ Abst a t2"
"nabla ⊢ Abst a t1 ≈ Abst b t2"

lemma equ_depth: 
  assumes "nabla ⊢ t1 ≈ t2"
  shows "depth t1 = depth t2"
  using assms by (rule equ.induct, simp_all)

lemma rev_pi_pi_equ: 
  shows "(nabla ⊢ swap (rev pi) (swap pi t) ≈ t)"
proof(induct t)
  case (Susp pi' X)
  then show ?case 
    using ds_cancel_pi_left[of _ ‹rev pi @ pi› _ ‹[]›]
    ds_rev_pi_pi elem_ds ds_rev_pi_id by auto
qed (auto)
  
lemma equ_pi_right: 
  assumes "∀a ∈ ds [] pi. nabla ⊢ a ♯ t"
  shows "nabla ⊢ t ≈ swap pi t"
  using assms
proof(induct t arbitrary: pi)
   case (Abst b t')
   have "swapas pi b = b ∨ swapas pi b ≠ b" by simp
  moreover 
  { assume eq: "swapas pi b = b"
    have "nabla ⊢ Abst b t' ≈ Abst b (swap pi t')"
      by (metis Abst.hyps Abst.prems Fresh_elims(1) elem_ds eq equ_abst_aa)
    then have "nabla ⊢ Abst b t' ≈ swap pi (Abst b t')" using eq by simp
  }
  moreover
  { assume neq: "b ≠ swapas pi b"  
    obtain c where c_def: "c = swapas pi b" by simp
    have "c ∈ ds [] pi"
      by (metis append.right_neutral c_def ds_cancel_pi_front ds_cancel_pi_left ds_elem neq)
    then have one: "nabla ⊢ c ♯ Abst b t'" using assms Abst.prems by auto
    have two: "b ≠ c" using neq c_def by blast
    have "nabla ⊢ c ♯ t'" using one two by cases auto
    have "nabla ⊢ Abst b t' ≈ Abst c (swap pi t')" 
    proof(rule equ_abst_ab)
      show "b ≠ c" using neq c_def by blast
      have b_is_swap: "b = swapas (rev pi) c" using c_def by simp
      show "nabla ⊢ b ♯ swap pi t'" 
        using Abst.prems Fresh_elims(1) ds_elem fresh_swap_right neq swapas_rev_pi_a by metis
      show "nabla ⊢ t' ≈ swap [(b, c)] (swap pi t')"
      proof -
         have fresh_ext:
          "∀a ∈ ds [] ((b,c) # pi). nabla ⊢ a ♯ t'"
        proof (rule ballI)
          fix a assume A: "a ∈ ds [] ((b,c)#pi)"
          then have "a = c ∨ a ∈ ds [] pi"
            using c_def ds_7 neq by auto  
          then show "nabla ⊢ a ♯ t'"
          proof
            assume "a = c"
            with ‹nabla ⊢ c ♯ t'› show ?thesis by simp
          next
            assume "a ∈ ds [] pi"
            show ?thesis 
            proof(rule Fresh_elims(1)[of nabla a b t'], goal_cases)
              case 1
              then show ?case
                using Abst.prems ‹a ∈ ds [] pi›
              by simp
            next
              case 2
              then show ?case by simp
            next
              case 3
              have "a ≠ swapas ((b, c) # pi) a" 
                using A elem_ds
                by blast
              hence "a ≠ b" using c_def A 
                by (auto simp add: if_split)
              hence False using 3 by simp
              then show ?case by simp
          qed
        qed
      qed
        from Abst.hyps[OF fresh_ext]
        have "nabla ⊢ t' ≈ swap ([(b,c)]@pi) t'"
          by simp
        moreover have "swap ([(b,c)]@pi) t' = swap [(b,c)] (swap pi t')"
          using swap_append by blast
        ultimately show ?thesis by simp
      qed
    qed
   then have "nabla ⊢ Abst b t' ≈ swap pi (Abst b t')" using neq c_def by force
 }
  ultimately show ?case by argo
next
  case (Susp pi' X)
  have "∀a∈ds [] pi. nabla ⊢ a ♯ Susp pi' X" by fact
  then have "nabla ⊢ Susp pi' X ≈ Susp (pi @ pi') X"
   using Fresh_elims(4) equ_susp ds_def ds_cancel_pi_left
   by (metis (lifting) append_self_conv2 swapas_rev_pi_a)
  then show ?case by simp
next
  case Unit
  then show ?case 
    using equ_unit swap.simps(2) by force
next
  case (Atom b)
    then show ?case
      apply simp
    apply (rule equ_atom)
    using Fresh_elims(3) ds_elem_cp
    by metis
next
  case (Paar t1 t2)
  then have hypsp1: "(∀a∈ds [] pi.  nabla ⊢ a ♯ t1)"
    and hypsp2: "(∀a∈ds [] pi.  nabla ⊢ a ♯ t2)"
    using Paar.prems Fresh_elims(5) by meson+
  have "nabla ⊢ Paar t1 t2 ≈ Paar (swap pi t1) (swap pi t2)"
    using Paar.hyps(1,2) hypsp1 hypsp2 by blast
  then show ?case by simp
next
  case (Func f t')
  then have hypsf: "∀a∈ds [] pi. nabla ⊢ a ♯ t'" using fresh_func
    by (metis Fresh_elims(6))
  have "nabla ⊢ Func f t' ≈ Func f (swap pi t')"
    using Func.hyps hypsf by blast
  then show ?case
    by simp
qed

lemma pi_comm: 
  shows "nabla ⊢ (swap (pi @ [(a,b)]) t) ≈ (swap ([(swapas pi a, swapas pi b)] @ pi) t)"
proof(induct t)
  case (Abst c t)
  then show ?case using swapas_comm by force
next
  case (Susp π' X)
  have rew1:
    "swap (pi @ [(a,b)]) (Susp π' X) = Susp (pi @ [(a,b)] @ π') X"
    by simp
  have rew2:
    "swap ([(swapas pi a, swapas pi b)] @ pi) (Susp π' X) 
    = Susp ([(swapas pi a, swapas pi b)] @ pi @ π') X"
    by simp
  have fresh:
  "∀c ∈ ds (pi @ [(a,b)] @ π') ([(swapas pi a, swapas pi b)] @ pi @ π'). (c, X) ∈ nabla"
    using swapas_append swapas_comm ds_def by simp
  from rew1 rew2 fresh
  show ?case
    using equ_susp by simp
next
  case Unit
  then show ?case by force
next
  case (Atom c)
  then show ?case 
    using equ_atom swapas_comm by auto
next
  case (Paar t1 t2)
  then show ?case by force
next
  case (Func f t)
  then show ?case by force
qed

lemma l3_jud: 
  assumes "(nabla ⊢ t1 ≈ t2)"
  shows "(nabla ⊢ a ♯ t1) ⟶ (nabla ⊢ a ♯ t2)"
  using assms
proof(induction rule: equ.induct)
  case (equ_abst_ab b c nabla t2 t1)
  then show ?case 
    using fresh_swap_left Fresh_elims(1) fresh_abst_aa fresh_abst_ab rev_singleton_conv swapa.simps swapas.simps(1,2)
    by metis
next
  case (equ_abst_aa nabla t1 t2 b)
  then show ?case 
    using fresh_swap_left Fresh_elims(1) fresh_abst_aa fresh_abst_ab 
    by metis
next
  case (equ_unit nabla)
  then show ?case
    by blast
next
  case (equ_atom b c nabla)
  then show ?case 
    by simp
next
  case (equ_susp pi1 pi2 X nabla)
  then show ?case 
    using Fresh_elims(4) ds_elem_cp ds_rev fresh_susp swapas_append swapas_rev_pi_a
    by metis
next
  case (equ_paar nabla t1 t2 s1 s2)
  then show ?case
    using Fresh_elims(5) by blast
next
  case (equ_func nabla t1 t2 f)
  then show ?case 
    using Fresh_elims(6) by blast
qed

lemma ds_empty_equiv_1:
  assumes "ds pi1 pi2 = {}"
  shows "nabla ⊢ swap pi1 t1 ≈ t2 ⟹ nabla ⊢ swap pi2 t1 ≈ t2"
  using assms
proof(induction t1 arbitrary: t2)
  case (Abst a t1')
  then obtain b t2'
    where t2: "t2 = Abst b t2'"
    by(auto elim: equ.cases)
  with Abst have i: "nabla ⊢ Abst (swapas pi1 a) (swap pi1 t1') ≈ Abst b t2'"
    using swap.simps(4) by simp
  then show ?case
  proof(cases ‹swapas pi1 a = b›)
    case True
    then have "nabla ⊢ swap pi1 t1' ≈ t2'" 
      using Abst i Equ_elims(6) by blast
    then have ii: "nabla ⊢ swap pi2 t1' ≈ t2'"
      using Abst by simp
    then have "nabla ⊢ Abst (swapas pi2 a) (swap pi2 t1') ≈ Abst b t2'"
      using True ds_swapas_eq[OF Abst(3), of a] equ_abst_aa[OF ii, of ‹swapas pi2 a›] 
      by simp
    then show ?thesis 
      using t2 by simp
  next
    case False
    then have equ_ab_pi1: "nabla ⊢ swap pi1 t1' ≈ swap [(swapas pi1 a, b)] t2'" 
      and fresh_ab_pi1: "nabla ⊢ swapas pi1 a ♯ t2'"
      using i Equ_elims(7)[of nabla ‹swapas pi1 a› ‹swap pi1 t1'› b t2'] 
      by blast+
    have equ_ab_pi2: "nabla ⊢ swap pi2 t1' ≈ swap [(swapas pi2 a, b)] t2'"
      using equ_ab_pi1 ds_swapas_eq[OF Abst(3), of a] 
        Abst(3) Abst(1)[of ‹swap [(swapas pi1 a, b)] t2'›] by auto
    have fresh_ab_pi2: "nabla ⊢ swapas pi2 a ♯ t2'"
      using fresh_ab_pi1 ds_swapas_eq[OF Abst(3), of a] by simp
    with equ_ab_pi2 have "nabla ⊢ Abst (swapas pi2 a) (swap pi2 t1') ≈ Abst b t2'"
      using equ_abst_ab[OF False, of nabla t2'] ds_swapas_eq[OF Abst(3), of a] by simp
    then show ?thesis using t2 by simp
  qed
next
  case (Susp pi X)
  then obtain pi'
    where t2: "t2 = Susp pi' X"
    by (auto elim:equ.cases)
  with Susp have i: "nabla ⊢ Susp (pi1 @ pi) X ≈ Susp pi' X" 
    by simp
  then have "∀ c ∈ ds (pi1@pi) pi'. (c,X) ∈ nabla"
    using Equ_elims(3)[OF i] by auto
  with Susp have "∀ c ∈ ds (pi2@pi) pi'. (c,X) ∈ nabla"
    using ds_cancel_pi_left ds_sym ds_trans
    by blast
  then have "nabla ⊢ Susp (pi2 @ pi) X ≈ Susp pi' X"
    using equ_susp by simp
  then show ?case using t2 swap.simps(3) by simp
next
  case (Atom a)
  then show ?case
    using ds_swapas_eq[OF Atom(2), of a]
    by (auto elim: equ.cases)
qed (auto elim: equ.cases)

lemma ds_empty_equiv_2:
  assumes "ds pi1 pi2 = {}"
  shows "nabla ⊢ t1 ≈ swap pi1 t2 ⟹ nabla ⊢ t1 ≈ swap pi2 t2"
using assms
proof(induction t2 arbitrary: pi1 pi2 t1)
  case (Abst b t2')
  then obtain a t1'
    where t1: "t1 = Abst a t1'"
    by(auto elim: equ.cases)
  with Abst have i: "nabla ⊢ Abst a t1' ≈ Abst (swapas pi1 b) (swap pi1 t2')"
    using swap.simps(4) by simp
  then show ?case
  proof(cases ‹swapas pi1 b = a›)
    case True
    then have "nabla ⊢ t1' ≈ swap pi1 t2'" 
      using Abst i Equ_elims(6) by blast
    then have ii: "nabla ⊢ t1' ≈ swap pi2 t2'"
      using Abst by simp
    then have "nabla ⊢ Abst a t1' ≈ Abst (swapas pi2 b) (swap pi2 t2')"
      using True ds_swapas_eq[OF Abst(3), of b] equ_abst_aa[OF ii, of ‹swapas pi2 b›] 
      by simp
    then show ?thesis 
      using t1 by simp
  next
    case False
    then have equ_ab: "nabla ⊢ t1' ≈ swap [(a, swapas pi1 b)] (swap pi1 t2')" 
      and fresh_ab_pi1: "nabla ⊢ a ♯ swap pi1 t2'"
      using i Equ_elims(7) by blast+

    then have equ_ab_pi1: "nabla ⊢ t1' ≈ swap ([(a, swapas pi1 b)]@ pi1) t2'"
      using swap_append[of ‹[(a, swapas pi1 b)]› pi1 t2'] by simp

    have ds_empty: "ds ([(a, swapas pi1 b)] @ pi1) ([(a, swapas pi2 b)] @ pi2) = {}"
      using Abst(3) ds_swapas_eq[OF Abst(3), of b] 
        ds_cancel_pi_front[of ‹[(a, swapas pi1 b)]› pi1 pi2] by simp
    
    hence "nabla ⊢ t1' ≈ swap ([(a, swapas pi2 b)]@ pi2) t2'"
      using Abst(1)[OF equ_ab_pi1 ds_empty] by simp
    hence equ_ab_pi2: "nabla ⊢ t1' ≈ swap [(a, swapas pi2 b)] (swap pi2 t2')"
      using swap_append[of ‹[(a, swapas pi2 b)]› pi2 t2'] by simp

    have fresh_ab_pi2: "nabla ⊢ a ♯ swap pi2 t2'"
      using ds_empty_fresh_2 Abst(3) fresh_ab_pi1 by auto
    with equ_ab_pi2 have "nabla ⊢ Abst a t1' ≈ Abst (swapas pi2 b) (swap pi2 t2')"
      using equ_abst_ab ds_swapas_eq False assms Abst(3) by auto
    then show ?thesis using t1 by simp
  qed
next
  case (Susp pi' X)
  then obtain pi
    where t1: "t1 = Susp pi X"
    by (auto elim:equ.cases)
  with Susp have i: "nabla ⊢ Susp pi X ≈ Susp (pi1 @ pi') X" 
    by simp
  then have "∀ c ∈ ds pi (pi1 @ pi'). (c,X) ∈ nabla"
    using Equ_elims(3)[OF i] by auto
  with Susp have "∀ c ∈ ds pi (pi2 @ pi'). (c,X) ∈ nabla"
    using ds_cancel_pi_left ds_sym ds_trans
    by blast
  then have "nabla ⊢ Susp pi X ≈ Susp (pi2 @ pi') X"
    using equ_susp by simp
  then show ?case using t1 swap.simps(3) by simp
next
  case (Atom a)
  then show ?case
    using ds_swapas_eq by (auto elim: equ.cases)
qed (auto elim: equ.cases)

lemma equ_equivariance:
  assumes "nabla ⊢ t1 ≈ t2"
  shows "nabla ⊢ swap pi t1 ≈ swap pi t2"
  using assms
proof(induct rule: equ.induct)
  case (equ_abst_ab a b nabla t2' t1')
  have i: "nabla ⊢ swapas pi a ♯ swap pi t2'"
    using fresh_swap_eqvt[OF equ_abst_ab(2), of pi] by simp

  have "nabla ⊢ swap pi t1' ≈ swap (pi @ [(a,b)]) t2'"
    using equ_abst_ab(4) swap_append[of pi ‹[(a,b)]› t2'] by simp
  then have "nabla ⊢ swap pi t1' ≈ swap ([(swapas pi a, swapas pi b)] @ pi) t2'"
    using ds_empty_equiv_2[OF ds_comm[of pi a b]] by auto
  then have ii: "nabla ⊢ swap pi t1' ≈ swap [(swapas pi a, swapas pi b)] (swap pi t2')"
    using ds_empty_equiv_2[OF ds_comm[of pi a b]] 
      swap_append[of ‹[(swapas pi a, swapas pi b)]› pi t2'] by simp

  have iii: "swapas pi a ≠ swapas pi b" 
    using equ_abst_ab.hyps(1) swapas_rev_pi_a by blast
  
  with i ii
  have "nabla ⊢ Abst (swapas pi a) (swap pi t1') ≈ Abst (swapas pi b) (swap pi t2')"
    using equ.equ_abst_ab by auto
  hence "nabla ⊢ swap pi (Abst a t1') ≈ swap pi (Abst b t2')"
    using swap.simps(4) by simp
  then show ?case by simp
next
  case (equ_abst_aa nabla t1' t2' a)
  then show ?case
    using equ.equ_abst_aa by simp
next
  case (equ_susp pi1 pi2 X nabla)
  then show ?case using ds_cancel_pi_front
    by auto
qed (auto)

lemma swap_inv_side: 
  shows "nabla ⊢ swap pi t1 ≈ t2 = nabla ⊢ t1 ≈ swap (rev pi) t2"
proof
  
  {assume assm1: "nabla ⊢ swap pi t1 ≈ t2"
  from equ_equivariance[OF assm1, of ‹rev pi›]
  have "nabla ⊢ swap (rev pi @ pi) t1  ≈ swap (rev pi) t2"
    using swap_append[of ‹rev pi› pi t1] by simp
  then show "nabla ⊢ t1 ≈ swap (rev pi) t2"
    using ds_empty_equiv_1[OF ds_rev_pi_id[of pi], of nabla t1 ‹swap (rev pi) t2›] 
      swap_id[of t1] by simp}

  {assume assm2: "nabla ⊢ t1 ≈ swap (rev pi) t2"
  from equ_equivariance[OF assm2, of pi]
  have "nabla ⊢ swap pi t1 ≈ swap (pi @ rev pi) t2"
    using swap_append[of pi ‹rev pi› t2] by simp
  then show "nabla ⊢ swap pi t1 ≈ t2"
    using ds_empty_equiv_2[OF ds_pi_rev_id[of pi], of nabla ‹swap pi t1› t2] 
      swap_id[of t2] by simp}
qed

lemma equ_swap_abba:
  assumes "n = depth t1"
  shows "nabla ⊢ swap [(a,b)] t1 ≈ t2 ⟹ nabla ⊢ t1 ≈ swap [(b,a)] t2"
proof-
  assume "nabla ⊢ swap [(a,b)] t1 ≈ t2"
  with ds_baab[of b a] 
  have "nabla ⊢ swap [(b,a)] t1 ≈ t2"
    using ds_empty_equiv_1 by blast
    then show ?thesis
    using swap_inv_side[of nabla ‹[(b,a)]›] by simp
qed

lemma equ_equiv_pi: 
  assumes "∀a ∈ ds pi1 pi2. nabla ⊢ a ♯ t"
  shows "nabla ⊢ swap pi1 t ≈ swap pi2 t"
  using assms equ_pi_right[of ‹rev pi1 @ pi2› nabla t]
    swap_inv_side[of nabla pi1 t ‹swap pi2 t›] ds_rev swap_append by simp

lemma equ_symm:
  shows "(nabla ⊢ t1 ≈ t2) ⟹ (nabla ⊢ t2 ≈ t1)"
proof(induction rule: equ.induct)
  case (equ_abst_ab a b nabla t2' t1')
  have i: "nabla ⊢ b ♯ swap [(a, b)] t2'" 
    using fresh_swap_eqvt[of nabla a t2' "[(a,b)]"] equ_abst_ab(2) by auto
  with equ_abst_ab(4) 
  have b_fresh: "nabla ⊢ b ♯ t1'"
    using l3_jud by blast
  from equ_abst_ab(4) 
  have ii: "nabla ⊢ t2' ≈ swap [(b, a)] t1'"
    using equ_swap_abba by simp
  show ?case 
    using equ.equ_abst_ab[OF equ_abst_ab(1)[symmetric] b_fresh ii] by simp
next
  case (equ_abst_aa nabla t1' t2' a)
  then show ?case 
    using equ.equ_abst_aa[OF equ_abst_aa(2), of a] by simp
next
  case (equ_unit nabla)
  then show ?case by auto
next
  case (equ_atom a b nabla)
  then show ?case by auto
next
  case (equ_susp pi1 pi2 X nabla)
  then show ?case 
    using ds_sym by auto
next
  case (equ_paar nabla t1' t2' s1' s2')
  then show ?case by auto
next
  case (equ_func nabla t1' t2' f)
  then show ?case 
    using equ.equ_func[OF equ_func(2), of f] by simp
qed

lemma equ_trans:
  assumes "nabla ⊢ t1 ≈ t2" "nabla ⊢ t2 ≈ t3"
  shows "nabla ⊢ t1 ≈ t3"
  using assms
proof(induction ‹depth t1› arbitrary: t1 t2 t3 rule: nat_less_induct)
  case 1
  note IH = this
  have IH_usable: 
    "depth t1' < depth t1 ⟹ nabla ⊢ t1' ≈ t2' ⟹  nabla ⊢ t2' ≈ t3' ⟹ nabla ⊢ t1' ≈ t3'"
    for t1' t2' t3' using IH by blast
  have "nabla ⊢ t1 ≈ t2 ⟹ nabla ⊢ t2 ≈ t3 ⟹  nabla ⊢ t1 ≈ t3"
  proof-
    assume t12: "nabla ⊢ t1 ≈ t2" and t23: "nabla ⊢ t2 ≈ t3"
    show ?thesis
     proof(cases rule: equ.cases[OF ‹nabla ⊢ t1 ≈ t2›])
       case (1 a b nabla t2' t1')
       from 1(2) have deptht1: "depth t1' < depth t1"
         using depth.simps(4) by auto
       from t23 show ?thesis
       proof(cases rule: equ.cases)
         case (equ_abst_ab b c t3' t2')
         then show ?thesis 
         proof(cases "a = c")
           case True
           have i: "nabla ⊢ swap [(c,b)] t2' ≈ swap ([(c,b)]@[(b,c)]) t3'"
             using equ_equivariance[OF equ_abst_ab(5), of ‹[(c,b)]›] 1(1)
               swap_append[of ‹[(c,b)]› ‹[(b,c)]› t3'] by simp
           have ii: "nabla ⊢ swap [(c,b)] t2' ≈ t3'"
             using ds_empty_equiv_2[OF ds_baab_id[OF equ_abst_ab(3)] i] by simp
           with equ_abst_ab 1 True
           have iii: "nabla ⊢ t1' ≈ swap [(c, b)] t2'" by blast
           with ii have "nabla ⊢ t1' ≈ t3'"
             using IH_usable[OF deptht1, of ‹swap [(c, b)] t2'› t3'] 1(1)
             by simp
           then show ?thesis using True equ_abst_ab(2) 1(1,2) by auto
         next
           case False

           have deptht2: "depth (swap [(a,b)] t2') < depth t1"
              using depth.simps(4) equ_depth[OF 1(6)] swap_depth 1(3) deptht1
              equ_abst_ab(1) by simp

            from equ_abst_ab(1,4,5) 1(1,3,5)
              have ii: "nabla ⊢ a ♯ swap [(b,c)] t3'"
                using l3_jud by simp

            then have a_fresh_t3: "nabla ⊢ a ♯ t3'"
              using fresh_swap_left[OF ii] False equ_abst_ab 1 by simp
            have b_fresh_t3: "nabla ⊢ b ♯ t3'" 
              using equ_abst_ab(4) 1(1) by simp

            from 1(1) equ_abst_ab(5)
            have "nabla ⊢ swap [(a,b)] t2' ≈ swap ([(a,b)]@[(b,c)]) t3'"
              using equ_equivariance[OF equ_abst_ab(5)]
             swap_append[of ‹[(a, b)]› ‹[(b,c)]› t3'] by simp
            then have iii: "nabla ⊢ swap [(a,b)] t2' ≈ swap ([(a,b),(b,c)]) t3'"
              by simp
            
            have "ds [(a,b), (b,c)] [(a,c)] = {a,b}" 
              using ds_acabbc equ_abst_ab 1 False by simp
            with a_fresh_t3 b_fresh_t3 
            have iv: "nabla ⊢ swap [(a,b),(b,c)] t3' ≈ swap [(a,c)] t3'"
              using equ_equiv_pi by simp

            with 1(1) iii have "nabla ⊢ swap [(a,b)] t2' ≈ swap [(a,c)] t3'"
              using IH_usable[OF deptht2, of ‹swap ([(a,b),(b,c)]) t3'› ‹swap [(a,c)] t3'›]
              by simp

            with 1(1,3,6) have "nabla ⊢ t1' ≈ swap [(a,c)] t3'"
              using IH_usable[OF deptht1, of ‹swap [(a, b)] t2'› ‹swap [(a,c)] t3'›]
              equ_abst_ab(1) by simp
            
            with 1(1,2) equ_abst_ab(2) 
            show ?thesis using equ.equ_abst_ab[OF False a_fresh_t3] by simp
         qed
       next
         case (equ_abst_aa t2' t3' b)
         from this(3) 1(1)
         have i: "nabla ⊢ swap [(a,b)] t2' ≈ swap [(a,b)] t3'"
           using equ_equivariance[of nabla t2' t3' ‹[(a,b)]›] by simp

         have "nabla ⊢ b ♯ swap [(a,b)] t2'" 
           using 1(1,3,4,5) equ_abst_aa(1) fresh_swap_eqvt[of nabla a t2' ‹[(a,b)]›]
           by auto
         then have ii: "nabla ⊢ b ♯ swap [(a,b)] t3'"
           using l3_jud[OF i, of b] by simp
         have "nabla ⊢ swapas [(a,b)] b ♯ t3'"
           using fresh_swap_left[OF ii] by simp
         then have a_fresh_t3: "nabla ⊢ a ♯ t3'"
           using 1(3,4) equ_abst_aa(1) by simp

         have is_equ: "nabla ⊢ t1' ≈ swap [(a,b)] t3'"
           using 1 i IH_usable[OF deptht1, of ‹swap [(a,b)] t2'› ‹swap [(a,b)] t3'›]
           equ_abst_aa(1) by auto
          
         from a_fresh_t3 is_equ show ?thesis
           using 1 equ_abst_aa(1,2) equ.equ_abst_ab by simp
       qed (auto simp add: 1 t12)
     next
       case (2 nabla t1' t2' a)
       have deptht1: "depth t1' < depth t1"
         using depth.simps(4) 2(2) by simp
         from t23 show ?thesis 
         proof(cases rule: equ.cases)
           case (equ_abst_ab a c t3' t2')
           have "nabla ⊢ t1' ≈ swap [(a,c)] t3'"
             using 2(1,2,3,4) IH_usable[OF deptht1, of ‹t2'› ‹swap [(a,c)] t3'›] 
            equ_abst_ab(1,4,5) by simp
           then show ?thesis
             using equ.equ_abst_ab[OF equ_abst_ab(3)]
               2(1,2,3) equ_abst_ab(1,2,4) by auto
         next
           case (equ_abst_aa t2' t3' a)
           then show ?thesis 
             using 1 2(1,2,3,4) by auto
         qed (auto simp add: 2)
     next
       case (3 nabla)
        from t23 show ?thesis
        proof(cases rule: equ.cases)
          case equ_unit
          then show ?thesis using t12 by auto
        qed (auto simp add: 3)
     next
       case (4 a b nabla)
        from t23 show ?thesis 
        proof(cases rule: equ.cases)
          case (equ_atom a b)
          then show ?thesis
            using t12 by auto
        qed (auto simp add: 4)
     next
       case (5 pi1 pi2 X nabla)
        from t23 show ?thesis 
        proof(cases rule: equ.cases)
          case (equ_susp pi1 pi2 X)
          then show ?thesis 
            using ds_trans 5 by blast
        qed (auto simp add: 5)
     next
       case (6 nabla t1' t2' s1' s2')
        from t23 show ?thesis 
        proof(cases rule: equ.cases)
          case (equ_paar t2' t3' s2' s3')
          have deptht1: "depth t1' < depth t1" 
            using 6(2) by simp
         have depths1: "depth s1' < depth t1" 
           using 6(2) by simp
         have a: "nabla ⊢ t1' ≈ t2'" 
           using "6"(3,4) equ_paar by auto
         have b: "nabla ⊢ s1' ≈ s2'" 
           using "6" equ_paar by auto
         from a have t1_equal_t3: "nabla ⊢ t1' ≈ t3'" 
           using IH_usable[of t1' t2' t3'] equ_paar(3) 6(1) deptht1
           by simp
         from b have s1_equal_s3: "nabla ⊢ s1' ≈ s3'" 
           using IH_usable[of s1' s2' s3'] equ_paar(4) 6(1) depths1
           by simp
         from t1_equal_t3 s1_equal_s3 show ?thesis 
           using equ.equ_paar[of nabla t1' t3' s1' s3'] 6(1,2) equ_paar(2)
           by simp
        qed (auto simp add: 6)
     next
       case (7 nabla t1 t2 F)
        from t23 show ?thesis 
       proof(cases rule: equ.cases)
         case (equ_func t1 t2 F)
         then show ?thesis 
           using 1 7(1,2,3,4) by auto
       qed (auto simp add: 7)
     qed
   qed
   then show ?case 
     using IH(2,3) by blast
 qed

lemma pi_right_equ_help:
  assumes "(n = depth t)"
  shows "nabla ⊢ t ≈ swap pi t ⟹ ∀ a ∈ ds [] pi. nabla ⊢ a ♯ t"
  using assms 
proof(induction n arbitrary: t pi rule: nat_less_induct)
  case (1 n)
  note IH = this
  then show ?case 
    proof(cases rule: equ.cases[OF ‹nabla ⊢ t ≈ swap pi t›])
      case (1 b c nabla t2 t1)
        have deptht1: "depth t1 < n"
          using 1 depth.simps(4) IH by simp
        have swap_pi_t1_is_t2: "swap pi t1 = t2"
          using 1(2,3) by auto
        have swap_pi_b_is_c: "swapas pi b = c"
          using 1(2,3) by auto
        with swap_pi_t1_is_t2 have "nabla ⊢ t1 ≈ swap [(b, swapas pi b)] (swap pi t1)"
          using 1(1,6) by simp
        then have "nabla ⊢ t1 ≈ swap ([(b, swapas pi b)] @ pi) t1"
          using swap_append[of ‹[(b, swapas pi b)]› pi t1] by simp
        with deptht1 have "∀ a ∈ ds [] ((b, swapas pi b)#pi). nabla ⊢ a ♯ t1"
          using "1.IH" 1 by auto
        then have ds_minus_bc: "∀ a ∈ ds [] pi - {b, c}. nabla ⊢ a ♯ t1"
          using ds_equality swap_pi_b_is_c by auto
        have c_fresh_t1: "nabla ⊢ c ♯ t1"
          using 1 equ_symm l3_jud fresh_swap_eqvt Equ_elims equ_abst_ab by meson
        with ds_minus_bc have "∀ a ∈ ds [] pi - {b}. nabla ⊢ a ♯ t1"
          by auto
        then have ds_minus_b: "∀ a ∈ ds [] pi - {b}. nabla ⊢ a ♯ Abst b t1"
          using fresh_abst_ab by blast
        have b_fresh_abst_t1: "nabla ⊢ b ♯ Abst b t1"
          using fresh_abst_aa by simp
        have "∀ a ∈ ds [] pi. nabla ⊢ a ♯ Abst b t1"
        proof(rule, goal_cases)
          case (1 a)
          then show ?case
            using b_fresh_abst_t1 ds_minus_b
            by (cases "a=b", auto)
        qed
        with 1 show ?thesis
          by auto
    next
      case (2 nabla t1 t2 b)
      have deptht1: "depth t1 < n"
        using 2 depth.simps(4) IH by simp
      have swap_pi_t1_is_t2: "swap pi t1 = t2"
        using 2(2,3) by auto
      from swap_pi_t1_is_t2 deptht1 
      have "∀ a ∈ ds [] pi. nabla ⊢ a ♯ t1"
        using "1.IH" 2(1,4) by auto
      then show ?thesis 
        using 2(1,2,3) elem_ds by fastforce
    next
      case (3 nabla)
      then show ?thesis 
        by blast
    next
      case (4 a b nabla)
      then show ?thesis
        using elem_ds by force
    next
      case (5 pi1 pi2 X nabla)
      have "swap pi t = Susp (pi@pi1) X" 
        using "5"(2) by auto
      also have "... = Susp pi2 X"
        using 5(3) calculation by simp
      then have "pi@pi1 = pi2" by simp
      hence "∀c∈ds pi1 (pi@pi1). (c, X) ∈ nabla"
        using 5(4) by simp
      then show ?thesis 
        using "5"(1,2) fresh_susp ds_cancel_pi_right[of _ _ "[]" _]
        by simp
    next
      case (6 nabla t1 t2 s1 s2)
      have deptht1: "depth t1 < n"
        using 6 depth.simps(5) IH
        by simp
      have depths1: "depth s1 < n"
        using 6 depth.simps(5) IH
        by simp
      from deptht1 depths1 show ?thesis 
        using "1.IH" 6 by auto
    next
      case (7 nabla t1 t2 f)
      have deptht1: "depth t1 < n"
        using 7(2) depth.simps(5) IH 
        by auto
      have "nabla ⊢ t1 ≈ swap pi t1"
        using 7 by simp
      then have "∀ a ∈ ds [] pi. nabla ⊢ a ♯ t1"
        using 7(1) IH deptht1 by simp
      then show ?thesis 
        using 7(1,2) fresh_func[of nabla _ t1 f] 
        by simp
    qed
  qed

(*<*)
end 
(*>*)