Theory Class1

theory Class1
imports "HOL-Nominal.Nominal"
begin

section ‹Term-Calculus from Urban's PhD›

atom_decl name coname

text ‹types›

unbundle no bit_operations_syntax

nominal_datatype ty =
    PR "string"
  | NOT  "ty"
  | AND  "ty" "ty"   (‹_ AND _› [100,100] 100)
  | OR   "ty" "ty"   (‹_ OR _›  [100,100] 100)
  | IMP  "ty" "ty"   (‹_ IMP _› [100,100] 100)

instantiation ty :: size
begin

nominal_primrec size_ty
where
  "size (PR s)     = (1::nat)"
| "size (NOT T)     = 1 + size T"
| "size (T1 AND T2) = 1 + size T1 + size T2"
| "size (T1 OR T2)  = 1 + size T1 + size T2"
| "size (T1 IMP T2) = 1 + size T1 + size T2"
by (rule TrueI)+

instance ..

end

lemma ty_cases:
  fixes T::ty
  shows "(s. T=PR s)  (T'. T=NOT T')  (S U. T=S OR U)  (S U. T=S AND U)  (S U. T=S IMP U)"
by (induct T rule:ty.induct) (auto)

lemma fresh_ty:
  fixes a::"coname"
  and   x::"name"
  and   T::"ty"
  shows "aT" and "xT"
by (nominal_induct T rule: ty.strong_induct)
   (auto simp: fresh_string)

text ‹terms›                               

nominal_datatype trm = 
    Ax   "name" "coname"
  | Cut  "«coname»trm" "«name»trm"            (Cut <_>._ ('(_'))._› [0,0,0,100] 101)
  | NotR "«name»trm" "coname"                 (NotR ('(_'))._ _› [0,100,100] 101)
  | NotL "«coname»trm" "name"                 (NotL <_>._ _› [0,100,100] 101)
  | AndR "«coname»trm" "«coname»trm" "coname" (AndR <_>._ <_>._ _› [0,100,0,100,100] 101)
  | AndL1 "«name»trm" "name"                  (AndL1 (_)._ _› [100,100,100] 101)
  | AndL2 "«name»trm" "name"                  (AndL2 (_)._ _› [100,100,100] 101)
  | OrR1 "«coname»trm" "coname"               (OrR1 <_>._ _› [100,100,100] 101)
  | OrR2 "«coname»trm" "coname"               (OrR2 <_>._ _› [100,100,100] 101)
  | OrL "«name»trm" "«name»trm" "name"        (OrL (_)._ (_)._ _› [100,100,100,100,100] 101)
  | ImpR "«name»(«coname»trm)" "coname"       (ImpR (_).<_>._ _› [100,100,100,100] 101)
  | ImpL "«coname»trm" "«name»trm" "name"     (ImpL <_>._ (_)._ _› [100,100,100,100,100] 101)

text ‹named terms›

nominal_datatype ntrm = Na "«name»trm" (((_):_) [100,100] 100)

text ‹conamed terms›

nominal_datatype ctrm = Co "«coname»trm" ((<_>:_) [100,100] 100)

text ‹renaming functions›

nominal_primrec (freshness_context: "(d::coname,e::coname)") 
  crename :: "trm  coname  coname  trm"  (‹_[_⊢c>_] [100,0,0] 100) 
where
  "(Ax x a)[d⊢c>e] = (if a=d then Ax x e else Ax x a)" 
| "a(d,e,N);xM  (Cut <a>.M (x).N)[d⊢c>e] = Cut <a>.(M[d⊢c>e]) (x).(N[d⊢c>e])" 
| "(NotR (x).M a)[d⊢c>e] = (if a=d then NotR (x).(M[d⊢c>e]) e else NotR (x).(M[d⊢c>e]) a)" 
| "a(d,e)  (NotL <a>.M x)[d⊢c>e] = (NotL <a>.(M[d⊢c>e]) x)" 
| "a(d,e,N,c);b(d,e,M,c);ba  (AndR <a>.M <b>.N c)[d⊢c>e] = 
          (if c=d then AndR <a>.(M[d⊢c>e]) <b>.(N[d ⊢c>e]) e else AndR <a>.(M[d⊢c>e]) <b>.(N[d⊢c>e]) c)" 
| "xy  (AndL1 (x).M y)[d⊢c>e] = AndL1 (x).(M[d⊢c>e]) y"
| "xy  (AndL2 (x).M y)[d⊢c>e] = AndL2 (x).(M[d⊢c>e]) y"
| "a(d,e,b)  (OrR1 <a>.M b)[d⊢c>e] = (if b=d then OrR1 <a>.(M[d⊢c>e]) e else OrR1 <a>.(M[d⊢c>e]) b)"
| "a(d,e,b)  (OrR2 <a>.M b)[d⊢c>e] = (if b=d then OrR2 <a>.(M[d⊢c>e]) e else OrR2 <a>.(M[d⊢c>e]) b)"
| "x(N,z);y(M,z);yx  (OrL (x).M (y).N z)[d⊢c>e] = OrL (x).(M[d⊢c>e]) (y).(N[d⊢c>e]) z"
| "a(d,e,b)  (ImpR (x).<a>.M b)[d⊢c>e] = 
       (if b=d then ImpR (x).<a>.(M[d⊢c>e]) e else ImpR (x).<a>.(M[d⊢c>e]) b)"
| "a(d,e,N);x(M,y)  (ImpL <a>.M (x).N y)[d⊢c>e] = ImpL <a>.(M[d⊢c>e]) (x).(N[d⊢c>e]) y"
  by(finite_guess | simp add: abs_fresh abs_supp fin_supp | fresh_guess)+

nominal_primrec (freshness_context: "(u::name,v::name)") 
  nrename :: "trm  name  name  trm"      (‹_[_⊢n>_] [100,0,0] 100) 
where
  "(Ax x a)[u⊢n>v] = (if x=u then Ax v a else Ax x a)" 
| "aN;x(u,v,M)  (Cut <a>.M (x).N)[u⊢n>v] = Cut <a>.(M[u⊢n>v]) (x).(N[u⊢n>v])" 
| "x(u,v)  (NotR (x).M a)[u⊢n>v] = NotR (x).(M[u⊢n>v]) a" 
| "(NotL <a>.M x)[u⊢n>v] = (if x=u then NotL <a>.(M[u⊢n>v]) v else NotL <a>.(M[u⊢n>v]) x)" 
| "a(N,c);b(M,c);ba  (AndR <a>.M <b>.N c)[u⊢n>v] = AndR <a>.(M[u⊢n>v]) <b>.(N[u⊢n>v]) c" 
| "x(u,v,y)  (AndL1 (x).M y)[u⊢n>v] = (if y=u then AndL1 (x).(M[u⊢n>v]) v else AndL1 (x).(M[u⊢n>v]) y)"
| "x(u,v,y)  (AndL2 (x).M y)[u⊢n>v] = (if y=u then AndL2 (x).(M[u⊢n>v]) v else AndL2 (x).(M[u⊢n>v]) y)"
| "ab  (OrR1 <a>.M b)[u⊢n>v] = OrR1 <a>.(M[u⊢n>v]) b"
| "ab  (OrR2 <a>.M b)[u⊢n>v] = OrR2 <a>.(M[u⊢n>v]) b"
| "x(u,v,N,z);y(u,v,M,z);yx  (OrL (x).M (y).N z)[u⊢n>v] = 
        (if z=u then OrL (x).(M[u⊢n>v]) (y).(N[u⊢n>v]) v else OrL (x).(M[u⊢n>v]) (y).(N[u⊢n>v]) z)"
| "ab; x(u,v)  (ImpR (x).<a>.M b)[u⊢n>v] = ImpR (x).<a>.(M[u⊢n>v]) b"
| "aN;x(u,v,M,y)  (ImpL <a>.M (x).N y)[u⊢n>v] = 
        (if y=u then ImpL <a>.(M[u⊢n>v]) (x).(N[u⊢n>v]) v else ImpL <a>.(M[u⊢n>v]) (x).(N[u⊢n>v]) y)"
  by(finite_guess | simp add: abs_fresh abs_supp fin_supp | fresh_guess)+

lemmas eq_bij = pt_bij[OF pt_name_inst, OF at_name_inst] pt_bij[OF pt_coname_inst, OF at_coname_inst]

lemma crename_name_eqvt[eqvt]:
  fixes pi::"name prm"
  shows "pi(M[d⊢c>e]) = (piM)[(pid)⊢c>(pie)]"
  by (nominal_induct M avoiding: d e rule: trm.strong_induct) (auto simp: fresh_bij eq_bij)

lemma crename_coname_eqvt[eqvt]:
  fixes pi::"coname prm"
  shows "pi(M[d⊢c>e]) = (piM)[(pid)⊢c>(pie)]"
  by (nominal_induct M avoiding: d e rule: trm.strong_induct)(auto simp: fresh_bij eq_bij)

lemma nrename_name_eqvt[eqvt]:
  fixes pi::"name prm"
  shows "pi(M[x⊢n>y]) = (piM)[(pix)⊢n>(piy)]"
  by(nominal_induct M avoiding: x y rule: trm.strong_induct) (auto simp: fresh_bij eq_bij)

lemma nrename_coname_eqvt[eqvt]:
  fixes pi::"coname prm"
  shows "pi(M[x⊢n>y]) = (piM)[(pix)⊢n>(piy)]"
  by(nominal_induct M avoiding: x y rule: trm.strong_induct)(auto simp: fresh_bij eq_bij)

lemmas rename_eqvts = crename_name_eqvt crename_coname_eqvt
                      nrename_name_eqvt nrename_coname_eqvt
lemma nrename_fresh:
  assumes a: "xM"
  shows "M[x⊢n>y] = M"
using a
by (nominal_induct M avoiding: x y rule: trm.strong_induct)
   (auto simp: trm.inject fresh_atm abs_fresh fin_supp abs_supp)

lemma crename_fresh:
  assumes a: "aM"
  shows "M[a⊢c>b] = M"
using a
by (nominal_induct M avoiding: a b rule: trm.strong_induct)
   (auto simp: trm.inject fresh_atm abs_fresh)

lemma nrename_nfresh:
  fixes x::"name"
  shows "xyxM[x⊢n>y]"
by (nominal_induct M avoiding: x y rule: trm.strong_induct)
   (auto simp: fresh_atm abs_fresh abs_supp fin_supp)

 lemma crename_nfresh:
  fixes x::"name"
  shows "xMxM[a⊢c>b]"
by (nominal_induct M avoiding: a b rule: trm.strong_induct)
   (auto simp: fresh_atm abs_fresh abs_supp fin_supp)

lemma crename_cfresh:
  fixes a::"coname"
  shows "abaM[a⊢c>b]"
by (nominal_induct M avoiding: a b rule: trm.strong_induct)
   (auto simp: fresh_atm abs_fresh abs_supp fin_supp)

lemma nrename_cfresh:
  fixes c::"coname"
  shows "cMcM[x⊢n>y]"
by (nominal_induct M avoiding: x y rule: trm.strong_induct)
   (auto simp: fresh_atm abs_fresh abs_supp fin_supp)

lemma nrename_nfresh':
  fixes x::"name"
  shows "x(M,z,y)xM[z⊢n>y]"
by (nominal_induct M avoiding: x z y rule: trm.strong_induct)
   (auto simp: fresh_prod fresh_atm abs_fresh abs_supp fin_supp)

lemma crename_cfresh':
  fixes a::"coname"
  shows "a(M,b,c)aM[b⊢c>c]"
by (nominal_induct M avoiding: a b c rule: trm.strong_induct)
   (auto simp: fresh_prod fresh_atm abs_fresh abs_supp fin_supp)

lemma nrename_rename:
  assumes a: "x'M"
  shows "([(x',x)]M)[x'⊢n>y]= M[x⊢n>y]"
using a
proof (nominal_induct M avoiding: x x' y rule: trm.strong_induct)
qed (auto simp: abs_fresh abs_supp fin_supp fresh_left calc_atm fresh_atm)

lemma crename_rename:
  assumes a: "a'M"
  shows "([(a',a)]M)[a'⊢c>b]= M[a⊢c>b]"
using a
proof (nominal_induct M avoiding: a a' b rule: trm.strong_induct)
qed (auto simp: abs_fresh abs_supp fin_supp fresh_left calc_atm fresh_atm)

lemmas rename_fresh = nrename_fresh crename_fresh 
                      nrename_nfresh crename_nfresh crename_cfresh nrename_cfresh
                      nrename_nfresh' crename_cfresh'
                      nrename_rename crename_rename

lemma better_nrename_Cut:
  assumes a: "x(u,v)"
  shows "(Cut <a>.M (x).N)[u⊢n>v] = Cut <a>.(M[u⊢n>v]) (x).(N[u⊢n>v])"
proof -
  obtain x'::"name"   where fs1: "x'(M,N,a,x,u,v)" by (rule exists_fresh(1), rule fin_supp, blast)
  obtain a'::"coname" where fs2: "a'(M,N,a,x,u,v)" by (rule exists_fresh(2), rule fin_supp, blast)
  have eq1: "(Cut <a>.M (x).N) = (Cut <a'>.([(a',a)]M) (x').([(x',x)]N))"
    using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
  have "(Cut <a'>.([(a',a)]M) (x').([(x',x)]N))[u⊢n>v] = 
                        Cut <a'>.(([(a',a)]M)[u⊢n>v]) (x').(([(x',x)]N)[u⊢n>v])"
    using fs1 fs2
    by (intro nrename.simps; simp add: fresh_left calc_atm)
  also have " = Cut <a>.(M[u⊢n>v]) (x).(N[u⊢n>v])" using fs1 fs2 a
    by(simp add: trm.inject alpha fresh_prod rename_eqvts calc_atm rename_fresh fresh_atm)
  finally show "(Cut <a>.M (x).N)[u⊢n>v] = Cut <a>.(M[u⊢n>v]) (x).(N[u⊢n>v])" using eq1
    by simp
qed

lemma better_crename_Cut:
  assumes a: "a(b,c)"
  shows "(Cut <a>.M (x).N)[b⊢c>c] = Cut <a>.(M[b⊢c>c]) (x).(N[b⊢c>c])"
proof -
  obtain x'::"name"   where fs1: "x'(M,N,a,x,b,c)" by (rule exists_fresh(1), rule fin_supp, blast)
  obtain a'::"coname" where fs2: "a'(M,N,a,x,b,c)" by (rule exists_fresh(2), rule fin_supp, blast)
  have eq1: "(Cut <a>.M (x).N) = (Cut <a'>.([(a',a)]M) (x').([(x',x)]N))"
    using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
  have "(Cut <a'>.([(a',a)]M) (x').([(x',x)]N))[b⊢c>c] = 
                        Cut <a'>.(([(a',a)]M)[b⊢c>c]) (x').(([(x',x)]N)[b⊢c>c])"
    using fs1 fs2
    by (intro crename.simps; simp add: fresh_left calc_atm)
  also have " = Cut <a>.(M[b⊢c>c]) (x).(N[b⊢c>c])" using fs1 fs2 a
    by(simp add: trm.inject alpha calc_atm rename_fresh fresh_atm fresh_prod rename_eqvts)
  finally show "(Cut <a>.M (x).N)[b⊢c>c] = Cut <a>.(M[b⊢c>c]) (x).(N[b⊢c>c])" using eq1
    by simp
qed

lemma crename_id:
  shows "M[a⊢c>a] = M"
by (nominal_induct M avoiding: a rule: trm.strong_induct) (auto)

lemma nrename_id:
  shows "M[x⊢n>x] = M"
by (nominal_induct M avoiding: x rule: trm.strong_induct) (auto)

lemma nrename_swap:
  shows "xM  [(x,y)]M = M[y⊢n>x]"
by (nominal_induct M avoiding: x y rule: trm.strong_induct) 
   (auto simp: abs_fresh abs_supp fin_supp fresh_left calc_atm fresh_atm)


lemma crename_swap:
  shows "aM  [(a,b)]M = M[b⊢c>a]"
by (nominal_induct M avoiding: a b rule: trm.strong_induct) 
   (auto simp: abs_fresh abs_supp fin_supp fresh_left calc_atm fresh_atm)


lemma crename_ax:
  assumes a: "M[a⊢c>b] = Ax x c" "ca" "cb"
  shows "M = Ax x c"
using a
proof (nominal_induct M avoiding: a b x c rule: trm.strong_induct)
qed (simp_all add: trm.inject split: if_splits)

lemma nrename_ax:
  assumes a: "M[x⊢n>y] = Ax z a" "zx" "zy"
  shows "M = Ax z a"
using a
proof (nominal_induct M avoiding: x y z a rule: trm.strong_induct)
qed (simp_all add: trm.inject split: if_splits)

text ‹substitution functions›

lemma fresh_perm_coname:
  fixes c::"coname"
  and   pi::"coname prm"
  and   M::"trm"
  assumes a: "cpi" "cM"
  shows "c(piM)"
  by (simp add: assms fresh_perm_app)

lemma fresh_perm_name:
  fixes x::"name"
  and   pi::"name prm"
  and   M::"trm"
  assumes a: "xpi" "xM"
  shows "x(piM)"
  by (simp add: assms fresh_perm_app)

lemma fresh_fun_simp_NotL:
  assumes a: "x'P" "x'M"
  shows "fresh_fun (λx'. Cut <c>.P (x').NotL <a>.M x') = Cut <c>.P (x').NotL <a>.M x'"
proof (rule fresh_fun_app)
  show "pt (TYPE(trm)::trm itself) (TYPE(name)::name itself)"
    by(rule pt_name_inst)
  show "at (TYPE(name)::name itself)"
    by(rule at_name_inst)
  show "finite (supp (λx'. Cut <c>.P (x').NotL <a>.M x')::name set)"
    using a by(finite_guess)
  obtain n::name where n: "n(c,P,a,M)"
    by (metis assms fresh_atm(3) fresh_prod)
  with assms have "n  (λx'. Cut <c>.P (x').NotL <a>.M x')"
    by (fresh_guess)
  then show "b. b  (λx'. Cut <c>.P (x').NotL <a>.M x', Cut <c>.P (b).NotL <a>.M b)"
    by (metis abs_fresh(1) abs_fresh(5) fresh_prod n trm.fresh(3))
  show "x'  (λx'. Cut <c>.P (x').NotL <a>.M x')"
    using assms by(fresh_guess)
qed

lemma fresh_fun_NotL[eqvt_force]:
  fixes pi1::"name prm"
  and   pi2::"coname prm"
  shows "pi1fresh_fun (λx'. Cut <c>.P (x').NotL <a>.M x')=
             fresh_fun (pi1(λx'. Cut <c>.P (x').NotL <a>.M x'))"
  and   "pi2fresh_fun (λx'. Cut <c>.P (x').NotL <a>.M x')=
             fresh_fun (pi2(λx'. Cut <c>.P (x').NotL <a>.M x'))"
   apply(perm_simp)
   apply(generate_fresh "name")
   apply(auto simp: fresh_prod fresh_fun_simp_NotL)
  apply (metis fresh_bij(1) fresh_fun_simp_NotL name_prm_coname_def)
  apply(perm_simp)
  apply(subgoal_tac "n::name. n(P,M,pi2P,pi2M,pi2)")
   apply (metis fresh_fun_simp_NotL fresh_prodD swap_simps(8) trm.perm(14) trm.perm(16))
  by (meson exists_fresh(1) fs_name1)

lemma fresh_fun_simp_AndL1:
  assumes a: "z'P" "z'M" "z'x"
  shows "fresh_fun (λz'. Cut <c>.P(z').AndL1 (x).M z') = Cut <c>.P (z').AndL1 (x).M z'"
proof (rule fresh_fun_app [OF pt_name_inst at_name_inst])
  obtain n::name where "n(c,P,x,M)"
    by (meson exists_fresh(1) fs_name1)
  then show "a. a  (λz'. Cut <c>.P(z').AndL1 x. M z', Cut <c>.P(a).AndL1 x. M a)"
    apply(intro exI [where x="n"])
    apply(simp add: fresh_prod abs_fresh)
    apply(fresh_guess)
    done
next
  show "z'  (λz'. Cut <c>.P(z').AndL1 x. M z')"
    using a by(fresh_guess)
qed finite_guess

lemma fresh_fun_AndL1[eqvt_force]:
  fixes pi1::"name prm"
  and   pi2::"coname prm"
  shows "pi1fresh_fun (λz'. Cut <c>.P (z').AndL1 (x).M z')=
             fresh_fun (pi1(λz'. Cut <c>.P (z').AndL1 (x).M z'))"
  and   "pi2fresh_fun (λz'. Cut <c>.P (z').AndL1 (x).M z')=
             fresh_fun (pi2(λz'. Cut <c>.P (z').AndL1 (x).M z'))"
apply(perm_simp)
apply(subgoal_tac "n::name. n(P,M,x,pi1P,pi1M,pi1x,pi1)")
apply(force simp add: fresh_prod fresh_fun_simp_AndL1 at_prm_fresh[OF at_name_inst] swap_simps)
  apply (meson exists_fresh(1) fs_name1)
apply(perm_simp)
apply(subgoal_tac "n::name. n(P,M,x,pi2P,pi2M,pi2x,pi2)")
apply(force simp add: fresh_prod fresh_fun_simp_AndL1 calc_atm)
  by (meson exists_fresh'(1) fs_name1)

lemma fresh_fun_simp_AndL2:
  assumes a: "z'P" "z'M" "z'x"
  shows "fresh_fun (λz'. Cut <c>.P (z').AndL2 (x).M z') = Cut <c>.P (z').AndL2 (x).M z'"
proof (rule fresh_fun_app [OF pt_name_inst at_name_inst])
  obtain n::name where "n(c,P,x,M)"
    by (meson exists_fresh(1) fs_name1)
  then show "a. a  (λz'. Cut <c>.P(z').AndL2 x. M z', Cut <c>.P(a).AndL2 x. M a)"
    apply(intro exI [where x="n"])
    apply(simp add: fresh_prod abs_fresh)
    apply(fresh_guess)
    done
next
  show "z'  (λz'. Cut <c>.P(z').AndL2 x. M z')"
    using a by(fresh_guess)           
qed finite_guess

lemma fresh_fun_AndL2[eqvt_force]:
  fixes pi1::"name prm"
  and   pi2::"coname prm"
  shows "pi1fresh_fun (λz'. Cut <c>.P (z').AndL2 (x).M z')=
             fresh_fun (pi1(λz'. Cut <c>.P (z').AndL2 (x).M z'))"
  and   "pi2fresh_fun (λz'. Cut <c>.P (z').AndL2 (x).M z')=
             fresh_fun (pi2(λz'. Cut <c>.P (z').AndL2 (x).M z'))"
   apply(perm_simp)
   apply(subgoal_tac "n::name. n(P,M,x,pi1P,pi1M,pi1x,pi1)")
    apply(force simp add: fresh_prod fresh_fun_simp_AndL2 at_prm_fresh[OF at_name_inst] swap_simps)
   apply (meson exists_fresh(1) fs_name1)
  apply(perm_simp)
  apply(subgoal_tac "n::name. n(P,M,x,pi2P,pi2M,pi2x,pi2)")
   apply(force simp add: fresh_prod fresh_fun_simp_AndL2 calc_atm)
  by (meson exists_fresh(1) fs_name1)

lemma fresh_fun_simp_OrL:
  assumes a: "z'P" "z'M" "z'N" "z'u" "z'x"
  shows "fresh_fun (λz'. Cut <c>.P(z').OrL(x).M(u).N z') = Cut <c>.P (z').OrL (x).M (u).N z'"
proof (rule fresh_fun_app [OF pt_name_inst at_name_inst])
  obtain n::name where "n(c,P,x,M,u,N)"
    by (meson exists_fresh(1) fs_name1)
  then show "a. a  (λz'. Cut <c>.P(z').OrL(x).M(u).N(z'), Cut <c>.P(a).OrL(x).M(u).N(a))"
    apply(intro exI [where x="n"])
    apply(simp add: fresh_prod abs_fresh)
    apply(fresh_guess)
    done
next
  show "z'  (λz'. Cut <c>.P(z').OrL(x).M(u).N(z'))"
    using a by(fresh_guess) 
qed finite_guess

lemma fresh_fun_OrL[eqvt_force]:
  fixes pi1::"name prm"
  and   pi2::"coname prm"
  shows "pi1fresh_fun (λz'. Cut <c>.P(z').OrL (x).M(u).N z')=
             fresh_fun (pi1(λz'. Cut <c>.P (z').OrL(x).M (u).N z'))"
  and   "pi2fresh_fun (λz'. Cut <c>.P(z').OrL (x).M(u).N z')=
             fresh_fun (pi2(λz'. Cut <c>.P(z').OrL(x).M(u).N z'))"
   apply(perm_simp)
   apply(subgoal_tac "n::name. n(P,M,N,x,u,pi1P,pi1M,pi1N,pi1x,pi1u,pi1)")
    apply(force simp add: fresh_prod fresh_fun_simp_OrL at_prm_fresh[OF at_name_inst] swap_simps)
   apply (meson exists_fresh(1) fs_name1)
  apply(perm_simp)
  apply(subgoal_tac "n::name. n(P,M,N,x,u,pi2P,pi2M,pi2N,pi2x,pi2u,pi2)")
   apply(force simp add: fresh_prod fresh_fun_simp_OrL calc_atm)
  by (meson exists_fresh(1) fs_name1)

lemma fresh_fun_simp_ImpL:
  assumes a: "z'P" "z'M" "z'N" "z'x"
  shows "fresh_fun (λz'. Cut <c>.P (z').ImpL <a>.M (x).N z') = Cut <c>.P (z').ImpL <a>.M (x).N z'"
proof (rule fresh_fun_app [OF pt_name_inst at_name_inst])
  obtain n::name where "n(c,P,x,M,N)"
    by (meson exists_fresh(1) fs_name1)
  then show "aa. aa  (λz'. Cut <c>.P(z').ImpL <a>.M(x).N z', Cut <c>.P(aa).ImpL <a>.M(x).N aa)"
    apply(intro exI [where x="n"])
    apply(simp add: fresh_prod abs_fresh)
    apply(fresh_guess)
    done
next
  show "z'  (λz'. Cut <c>.P(z').ImpL <a>.M(x).N z')"
    using a by(fresh_guess) 
qed finite_guess

lemma fresh_fun_ImpL[eqvt_force]:
  fixes pi1::"name prm"
  and   pi2::"coname prm"
  shows "pi1fresh_fun (λz'. Cut <c>.P (z').ImpL <a>.M (x).N z')=
             fresh_fun (pi1(λz'. Cut <c>.P (z').ImpL <a>.M (x).N z'))"
  and   "pi2fresh_fun (λz'. Cut <c>.P (z').ImpL <a>.M (x).N z')=
             fresh_fun (pi2(λz'. Cut <c>.P (z').ImpL <a>.M (x).N z'))"
   apply(perm_simp)
   apply(subgoal_tac "n::name. n(P,M,N,x,pi1P,pi1M,pi1N,pi1x,pi1)")
    apply(force simp add: fresh_prod fresh_fun_simp_ImpL at_prm_fresh[OF at_name_inst] swap_simps)
   apply (meson exists_fresh(1) fs_name1)
  apply(perm_simp)
  apply(subgoal_tac "n::name. n(P,M,N,x,pi2P,pi2M,pi2N,pi2x,pi2)")
   apply(force simp add: fresh_prod fresh_fun_simp_ImpL calc_atm)
  by (meson exists_fresh(1) fs_name1)

lemma fresh_fun_simp_NotR:
  assumes a: "a'P" "a'M"
  shows "fresh_fun (λa'. Cut <a'>.(NotR (y).M a') (x).P) = Cut <a'>.(NotR (y).M a') (x).P"
proof (rule fresh_fun_app [OF pt_coname_inst at_coname_inst])
  obtain n::coname where "n(x,P,y,M)"
    by (metis assms(1) assms(2) fresh_atm(4) fresh_prod)
  then show "a. a  (λa'. Cut <a'>.(NotR (y).M a') (x).P, Cut <a>.NotR(y).M(a) (x).P)"
    apply(intro exI [where x="n"])
    apply(simp add: fresh_prod abs_fresh)
    apply(fresh_guess)
    done
qed (use a in fresh_guess|finite_guess)+

lemma fresh_fun_NotR[eqvt_force]:
  fixes pi1::"name prm"
  and   pi2::"coname prm"
  shows "pi1fresh_fun (λa'. Cut <a'>.(NotR (y).M a') (x).P)=
             fresh_fun (pi1(λa'. Cut <a'>.(NotR (y).M a') (x).P))"
  and   "pi2fresh_fun (λa'. Cut <a'>.(NotR (y).M a') (x).P)=
             fresh_fun (pi2(λa'. Cut <a'>.(NotR (y).M a') (x).P))"
   apply(perm_simp)
   apply(subgoal_tac "n::coname. n(P,M,pi1P,pi1M,pi1)")
    apply(force simp add: fresh_prod fresh_fun_simp_NotR calc_atm)
   apply (meson exists_fresh(2) fs_coname1)
  apply(perm_simp)
  apply(subgoal_tac "n::coname. n(P,M,pi2P,pi2M,pi2)")
   apply(force simp: fresh_prod fresh_fun_simp_NotR at_prm_fresh[OF at_coname_inst] swap_simps)
  by (meson exists_fresh(2) fs_coname1)

lemma fresh_fun_simp_AndR:
  assumes a: "a'P" "a'M" "a'N" "a'b" "a'c"
  shows "fresh_fun (λa'. Cut <a'>.(AndR <b>.M <c>.N a') (x).P) = Cut <a'>.(AndR <b>.M <c>.N a') (x).P"
proof (rule fresh_fun_app [OF pt_coname_inst at_coname_inst])
  obtain n::coname where "n(x,P,b,M,c,N)"
    by (meson exists_fresh(2) fs_coname1)
  then show "a. a  (λa'. Cut <a'>.AndR <b>.M <c>.N(a') (x).P, Cut <a>.AndR <b>.M <c>.N(a) (x).P)"
    apply(intro exI [where x="n"])
    apply(simp add: fresh_prod abs_fresh)
    apply(fresh_guess)
    done
qed (use a in fresh_guess|finite_guess)+

lemma fresh_fun_AndR[eqvt_force]:
  fixes pi1::"name prm"
  and   pi2::"coname prm"
  shows "pi1fresh_fun (λa'. Cut <a'>.(AndR <b>.M <c>.N a') (x).P)=
             fresh_fun (pi1(λa'. Cut <a'>.(AndR <b>.M <c>.N a') (x).P))"
  and   "pi2fresh_fun (λa'. Cut <a'>.(AndR <b>.M <c>.N a') (x).P)=
             fresh_fun (pi2(λa'. Cut <a'>.(AndR <b>.M <c>.N a') (x).P))"
   apply(perm_simp)
   apply(subgoal_tac "n::coname. n(P,M,N,b,c,pi1P,pi1M,pi1N,pi1b,pi1c,pi1)")
    apply(force simp add: fresh_prod fresh_fun_simp_AndR calc_atm)
   apply (meson exists_fresh(2) fs_coname1)
  apply(perm_simp)
  apply(subgoal_tac "n::coname. n(P,M,N,b,c,pi2P,pi2M,pi2N,pi2b,pi2c,pi2)")
   apply(force simp add: fresh_prod fresh_fun_simp_AndR at_prm_fresh[OF at_coname_inst] swap_simps)
  by (meson exists_fresh(2) fs_coname1)

lemma fresh_fun_simp_OrR1:
  assumes a: "a'P" "a'M" "a'b" 
  shows "fresh_fun (λa'. Cut <a'>.(OrR1 <b>.M a') (x).P) = Cut <a'>.(OrR1 <b>.M a') (x).P"
proof (rule fresh_fun_app [OF pt_coname_inst at_coname_inst])
  obtain n::coname where "n(x,P,b,M)"
    by (meson exists_fresh(2) fs_coname1)
  then show "a. a  (λa'. Cut <a'>.OrR1 <b>.M(a') (x).P, Cut <a>.OrR1 <b>.M(a) (x).P)"
    apply(intro exI [where x="n"])
    apply(simp add: fresh_prod abs_fresh)
    apply(fresh_guess)
    done
qed (use a in fresh_guess|finite_guess)+

lemma fresh_fun_OrR1[eqvt_force]:
  fixes pi1::"name prm"
  and   pi2::"coname prm"
  shows "pi1fresh_fun (λa'. Cut <a'>.(OrR1 <b>.M a') (x).P) =
             fresh_fun (pi1(λa'. Cut <a'>.(OrR1 <b>.M  a') (x).P))" (is "?t1")
  and   "pi2fresh_fun (λa'. Cut <a'>.(OrR1 <b>.M a') (x).P) =
             fresh_fun (pi2(λa'. Cut <a'>.(OrR1 <b>.M a') (x).P))"  (is "?t2")
proof -
  obtain n::coname where "n(P,M,b,pi1P,pi1M,pi1b,pi1)"
    by (meson exists_fresh(2) fs_coname1)
  then show ?t1
    by perm_simp (force simp add: fresh_prod fresh_fun_simp_OrR1 calc_atm)
  obtain n::coname where "n(P,M,b,pi2P,pi2M,pi2b,pi2)"
    by (meson exists_fresh(2) fs_coname1)
  then show ?t2
    by perm_simp
      (force simp add: fresh_prod fresh_fun_simp_OrR1 at_prm_fresh[OF at_coname_inst] swap_simps)
qed

lemma fresh_fun_simp_OrR2:
  assumes "a'P" "a'M" "a'b" 
  shows "fresh_fun (λa'. Cut <a'>.(OrR2 <b>.M a') (x).P) = Cut <a'>.(OrR2 <b>.M a') (x).P"
proof (rule fresh_fun_app [OF pt_coname_inst at_coname_inst])
  obtain n::coname where "n(x,P,b,M)"
    by (meson exists_fresh(2) fs_coname1)
  then show "a. a  (λa'. Cut <a'>.OrR2 <b>.M(a') (x).P, Cut <a>.OrR2 <b>.M(a) (x).P)"
    apply(intro exI [where x="n"])
    apply(simp add: fresh_prod abs_fresh)
    apply(fresh_guess)
    done
qed (use assms in fresh_guess|finite_guess)+

lemma fresh_fun_OrR2[eqvt_force]:
  fixes pi1::"name prm"
  and   pi2::"coname prm"
  shows "pi1fresh_fun (λa'. Cut <a'>.(OrR2 <b>.M a') (x).P) =
             fresh_fun (pi1(λa'. Cut <a'>.(OrR2 <b>.M  a') (x).P))" (is "?t1")
  and   "pi2fresh_fun (λa'. Cut <a'>.(OrR2 <b>.M a') (x).P) =
             fresh_fun (pi2(λa'. Cut <a'>.(OrR2 <b>.M a') (x).P))"  (is "?t2")
proof -
  obtain n::coname where "n(P,M,b,pi1P,pi1M,pi1b,pi1)"
    by (meson exists_fresh(2) fs_coname1)
  then show ?t1
    by perm_simp (force simp add: fresh_prod fresh_fun_simp_OrR2 calc_atm)
  obtain n::coname where "n(P,M,b,pi2P,pi2M,pi2b,pi2)"
    by (meson exists_fresh(2) fs_coname1)
  then show ?t2
    by perm_simp
      (force simp add: fresh_prod fresh_fun_simp_OrR2 at_prm_fresh[OF at_coname_inst] swap_simps)
qed

lemma fresh_fun_simp_ImpR:
  assumes a: "a'P" "a'M" "a'b" 
  shows "fresh_fun (λa'. Cut <a'>.(ImpR (y).<b>.M a') (x).P) = Cut <a'>.(ImpR (y).<b>.M a') (x).P"
proof (rule fresh_fun_app [OF pt_coname_inst at_coname_inst])
  obtain n::coname where "n(x,P,y,b,M)"
    by (meson exists_fresh(2) fs_coname1)
  then show "a. a  (λa'. Cut <a'>.(ImpR (y).<b>.M a') (x).P, Cut <a>.(ImpR (y).<b>.M a) (x).P)"
    apply(intro exI [where x="n"])
    apply(simp add: fresh_prod abs_fresh)
    apply(fresh_guess)
    done
qed (use a in fresh_guess|finite_guess)+

lemma fresh_fun_ImpR[eqvt_force]:
  fixes pi1::"name prm"
  and   pi2::"coname prm"
  shows "pi1fresh_fun (λa'. Cut <a'>.(ImpR (y).<b>.M a') (x).P) =
             fresh_fun (pi1(λa'. Cut <a'>.(ImpR (y).<b>.M  a') (x).P))" (is "?t1")
  and   "pi2fresh_fun (λa'. Cut <a'>.(ImpR (y).<b>.M a') (x).P)=
             fresh_fun (pi2(λa'. Cut <a'>.(ImpR (y).<b>.M a') (x).P))"  (is "?t2")
proof -
  obtain n::coname where "n(P,M,b,pi1P,pi1M,pi1b,pi1)"
    by (meson exists_fresh(2) fs_coname1)
  then show ?t1
    by perm_simp (force simp add: fresh_prod fresh_fun_simp_ImpR calc_atm)
  obtain n::coname where "n(P,M,b,pi2P,pi2M,pi2b,pi2)"
    by (meson exists_fresh(2) fs_coname1)
  then show ?t2
    by perm_simp
      (force simp add: fresh_prod fresh_fun_simp_ImpR at_prm_fresh[OF at_coname_inst] swap_simps)
qed

nominal_primrec (freshness_context: "(y::name,c::coname,P::trm)")
  substn :: "trm  name    coname  trm  trm" (‹_{_:=<_>._} [100,100,100,100] 100) 
where
  "(Ax x a){y:=<c>.P} = (if x=y then Cut <c>.P (y).Ax y a else Ax x a)" 
| "a(c,P,N);x(y,P,M)  (Cut <a>.M (x).N){y:=<c>.P} = 
  (if M=Ax y a then Cut <c>.P (x).(N{y:=<c>.P}) else Cut <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}))" 
| "x(y,P)  (NotR (x).M a){y:=<c>.P} = NotR (x).(M{y:=<c>.P}) a" 
| "a(c,P)  (NotL <a>.M x){y:=<c>.P} = 
  (if x=y then fresh_fun (λx'. Cut <c>.P (x').NotL <a>.(M{y:=<c>.P}) x') else NotL <a>.(M{y:=<c>.P}) x)"
| "a(c,P,N,d);b(c,P,M,d);ba  
  (AndR <a>.M <b>.N d){y:=<c>.P} = AndR <a>.(M{y:=<c>.P}) <b>.(N{y:=<c>.P}) d" 
| "x(y,P,z)  (AndL1 (x).M z){y:=<c>.P} = 
  (if z=y then fresh_fun (λz'. Cut <c>.P (z').AndL1 (x).(M{y:=<c>.P}) z') 
   else AndL1 (x).(M{y:=<c>.P}) z)"
| "x(y,P,z)  (AndL2 (x).M z){y:=<c>.P} = 
  (if z=y then fresh_fun (λz'. Cut <c>.P (z').AndL2 (x).(M{y:=<c>.P}) z') 
   else AndL2 (x).(M{y:=<c>.P}) z)"
| "a(c,P,b)  (OrR1 <a>.M b){y:=<c>.P} = OrR1 <a>.(M{y:=<c>.P}) b"
| "a(c,P,b)  (OrR2 <a>.M b){y:=<c>.P} = OrR2 <a>.(M{y:=<c>.P}) b"
| "x(y,N,P,z);u(y,M,P,z);xu  (OrL (x).M (u).N z){y:=<c>.P} = 
  (if z=y then fresh_fun (λz'. Cut <c>.P (z').OrL (x).(M{y:=<c>.P}) (u).(N{y:=<c>.P}) z') 
   else OrL (x).(M{y:=<c>.P}) (u).(N{y:=<c>.P}) z)"
| "a(b,c,P); x(y,P)  (ImpR (x).<a>.M b){y:=<c>.P} = ImpR (x).<a>.(M{y:=<c>.P}) b"
| "a(N,c,P);x(y,P,M,z)  (ImpL <a>.M (x).N z){y:=<c>.P} = 
  (if y=z then fresh_fun (λz'. Cut <c>.P (z').ImpL <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}) z') 
   else ImpL <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}) z)"
apply(finite_guess | simp add: abs_fresh abs_supp fin_supp | fresh_guess | rule strip)+
apply(subgoal_tac "x::name. x(x1,P,y1)")
apply(force simp add: fresh_prod fresh_fun_simp_NotL abs_fresh fresh_atm)
apply (meson exists_fresh(1) fs_name1)

apply(simp add: abs_fresh abs_supp fin_supp | rule strip)+
apply(subgoal_tac "x::name. x(x1,P,y1)")
apply(force simp add: fresh_prod fresh_fun_simp_AndL1 abs_fresh fresh_atm)
apply (meson exists_fresh(1) fs_name1)

apply(simp add: abs_fresh abs_supp fin_supp | rule strip)+
apply(subgoal_tac "x::name. x(x1,P,y1)")
apply(force simp add: fresh_prod fresh_fun_simp_AndL2 abs_fresh fresh_atm)
apply (meson exists_fresh(1) fs_name1)

apply(simp add: abs_fresh abs_supp fin_supp | rule strip)+
apply(subgoal_tac "x::name. x(x1,P,y1,x3,y2)")
apply(force simp add: fresh_prod fresh_fun_simp_OrL abs_fresh fresh_atm)
apply (meson exists_fresh(1) fs_name1)

apply(simp add: abs_fresh abs_supp fin_supp | rule strip)+
apply(subgoal_tac "x::name. x(x1,P,y1,x3,y2)")
apply(force simp add: fresh_prod fresh_fun_simp_OrL abs_fresh fresh_atm)
apply (meson exists_fresh(1) fs_name1)

apply(simp add: abs_fresh abs_supp fin_supp | rule strip)+
apply(subgoal_tac "x::name. x(x3,P,y1,y2)")
apply(force simp add: fresh_prod fresh_fun_simp_ImpL abs_fresh fresh_atm)
apply (meson exists_fresh(1) fs_name1)

apply(simp add: abs_fresh abs_supp fin_supp | rule strip)+
apply(subgoal_tac "x::name. x(x3,P,y1,y2)")
apply(force simp add: fresh_prod fresh_fun_simp_ImpL abs_fresh fresh_atm)
apply (meson exists_fresh(1) fs_name1)
apply(fresh_guess)+
done

nominal_primrec (freshness_context: "(d::name,z::coname,P::trm)")
  substc :: "trm  coname  name    trm  trm" (‹_{_:=('(_'))._} [100,0,0,100] 100)
where
  "(Ax x a){d:=(z).P} = (if d=a then Cut <a>.(Ax x a) (z).P else Ax x a)" 
| "a(d,P,N);x(z,P,M)  (Cut <a>.M (x).N){d:=(z).P} = 
  (if N=Ax x d then Cut <a>.(M{d:=(z).P}) (z).P else Cut <a>.(M{d:=(z).P}) (x).(N{d:=(z).P}))" 
| "x(z,P)  (NotR (x).M a){d:=(z).P} = 
  (if d=a then fresh_fun (λa'. Cut <a'>.NotR (x).(M{d:=(z).P}) a' (z).P) else NotR (x).(M{d:=(z).P}) a)" 
| "a(d,P)  (NotL <a>.M x){d:=(z).P} = NotL <a>.(M{d:=(z).P}) x" 
| "a(P,c,N,d);b(P,c,M,d);ba  (AndR <a>.M <b>.N c){d:=(z).P} = 
  (if d=c then fresh_fun (λa'. Cut <a'>.(AndR <a>.(M{d:=(z).P}) <b>.(N{d:=(z).P}) a') (z).P)
   else AndR <a>.(M{d:=(z).P}) <b>.(N{d:=(z).P}) c)" 
| "x(y,z,P)  (AndL1 (x).M y){d:=(z).P} = AndL1 (x).(M{d:=(z).P}) y"
| "x(y,P,z)  (AndL2 (x).M y){d:=(z).P} = AndL2 (x).(M{d:=(z).P}) y"
| "a(d,P,b)  (OrR1 <a>.M b){d:=(z).P} = 
  (if d=b then fresh_fun (λa'. Cut <a'>.OrR1 <a>.(M{d:=(z).P}) a' (z).P) else OrR1 <a>.(M{d:=(z).P}) b)"
| "a(d,P,b)  (OrR2 <a>.M b){d:=(z).P} = 
  (if d=b then fresh_fun (λa'. Cut <a'>.OrR2 <a>.(M{d:=(z).P}) a' (z).P) else OrR2 <a>.(M{d:=(z).P}) b)"
| "x(N,z,P,u);y(M,z,P,u);xy  (OrL (x).M (y).N u){d:=(z).P} = 
  OrL (x).(M{d:=(z).P}) (y).(N{d:=(z).P}) u" 
| "a(b,d,P); x(z,P)  (ImpR (x).<a>.M b){d:=(z).P} = 
  (if d=b then fresh_fun (λa'. Cut <a'>.ImpR (x).<a>.(M{d:=(z).P}) a' (z).P) 
   else ImpR (x).<a>.(M{d:=(z).P}) b)"
| "a(N,d,P);x(y,z,P,M)  (ImpL <a>.M (x).N y){d:=(z).P} = 
  ImpL <a>.(M{d:=(z).P}) (x).(N{d:=(z).P}) y"
apply(finite_guess | simp add: abs_fresh abs_supp fs_name1 fs_coname1 | rule strip)+
apply(subgoal_tac "x::coname. x(x1,P,y1)")
apply(force simp add: fresh_prod fresh_fun_simp_NotR abs_fresh fresh_atm)
apply(meson exists_fresh' fin_supp)

apply(simp add: abs_fresh abs_supp fs_name1 fs_coname1 | rule strip)+
apply(subgoal_tac "x::coname. x(x1,P,y1,x3,y2)")
apply(force simp add: fresh_prod fresh_fun_simp_AndR abs_fresh fresh_atm)
apply(meson exists_fresh' fin_supp)

apply(simp add: abs_fresh abs_supp fs_name1 fs_coname1 | rule strip)+
apply(subgoal_tac "x::coname. x(x1,P,y1,x3,y2)")
apply(force simp add: fresh_prod fresh_fun_simp_AndR abs_fresh fresh_atm)
apply(meson exists_fresh' fin_supp)

apply(simp add: abs_fresh abs_supp fs_name1 fs_coname1 | rule strip)+
apply(subgoal_tac "x::coname. x(x1,P,y1)")
apply(force simp add: fresh_prod fresh_fun_simp_OrR1 abs_fresh fresh_atm)
apply(meson exists_fresh' fin_supp)

apply(simp add: abs_fresh abs_supp fs_name1 fs_coname1 | rule strip)+
apply(subgoal_tac "x::coname. x(x1,P,y1)")
apply(force simp add: fresh_prod fresh_fun_simp_OrR2 abs_fresh fresh_atm)
apply(meson exists_fresh' fin_supp)

apply(simp add: abs_fresh abs_supp | rule strip)+
apply(subgoal_tac "x::coname. x(x1,P,x2,y1)")
apply(force simp add: fresh_prod fresh_fun_simp_ImpR abs_fresh fresh_atm abs_supp)
apply(meson exists_fresh' fin_supp)

apply(simp add: abs_fresh abs_supp | rule strip)+
apply(subgoal_tac "x::coname. x(x1,P,x2,y1)")
apply(force simp add: fresh_prod fresh_fun_simp_ImpR abs_fresh fresh_atm)
apply(meson exists_fresh' fin_supp)

apply(simp add: abs_fresh | fresh_guess add: abs_fresh)+
done


lemma csubst_eqvt[eqvt]:
  fixes pi1::"name prm"
  and   pi2::"coname prm"
  shows "pi1(M{c:=(x).N}) = (pi1M){(pi1c):=(pi1x).(pi1N)}"
  and   "pi2(M{c:=(x).N}) = (pi2M){(pi2c):=(pi2x).(pi2N)}"
by (nominal_induct M avoiding: c x N rule: trm.strong_induct)
   (auto simp: eq_bij fresh_bij eqvts; perm_simp)+

lemma nsubst_eqvt[eqvt]:
  fixes pi1::"name prm"
  and   pi2::"coname prm"
  shows "pi1(M{x:=<c>.N}) = (pi1M){(pi1x):=<(pi1c)>.(pi1N)}"
  and   "pi2(M{x:=<c>.N}) = (pi2M){(pi2x):=<(pi2c)>.(pi2N)}"
by (nominal_induct M avoiding: c x N rule: trm.strong_induct)
   (auto simp: eq_bij fresh_bij eqvts; perm_simp)+

lemma supp_subst1:
  shows "supp (M{y:=<c>.P})  ((supp M) - {y})  (supp P)"
proof (nominal_induct M avoiding: y P c rule: trm.strong_induct)
  case (NotL coname trm name)
  obtain x'::name where "x'(trm{y:=<c>.P},P)"
    by (meson exists_fresh(1) fs_name1)
  with NotL
   show ?case 
     by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_NotL; blast)
next
  case (AndL1 name1 trm name2)
  obtain x'::name where "x'(trm{y:=<c>.P},P,name1)"
    by (meson exists_fresh(1) fs_name1)
  with AndL1 show ?case
    by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_AndL1 fresh_atm; blast)
next
  case (AndL2 name1 trm name2)
  obtain x'::name where "x'(trm{y:=<c>.P},P,name1)"
    by (meson exists_fresh(1) fs_name1)
  with AndL2 show ?case
    by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_AndL2 fresh_atm; blast)
next
  case (OrL name1 trm1 name2 trm2 name3)
  obtain x'::name where "x'(trm1{y:=<c>.P},P,name1,trm2{y:=<c>.P},name2)"
    by (meson exists_fresh(1) fs_name1)
  with OrL show ?case 
    by (auto simp: fs_name1 fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_OrL fresh_atm; blast)
next
  case (ImpL coname trm1 name1 trm2 name2)
  obtain x'::name where "x'(trm1{name2:=<c>.P},P,name1,trm2{name2:=<c>.P})"
    by (meson exists_fresh(1) fs_name1)
  with ImpL show ?case 
    by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_ImpL fresh_atm; blast)
qed (simp add: abs_supp supp_atm trm.supp fs_name1; blast)+

text ‹Identical to the previous proof›
lemma supp_subst2:
  shows "supp (M{y:=<c>.P})  supp (M)  ((supp P) - {c})"
proof (nominal_induct M avoiding: y P c rule: trm.strong_induct)
  case (NotL coname trm name)
  obtain x'::name where "x'(trm{y:=<c>.P},P)"
    by (meson exists_fresh(1) fs_name1)
  with NotL
   show ?case 
     by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_NotL; blast)
next
  case (AndL1 name1 trm name2)
  obtain x'::name where "x'(trm{y:=<c>.P},P,name1)"
    by (meson exists_fresh(1) fs_name1)
  with AndL1 show ?case
    by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_AndL1 fresh_atm; blast)
next
  case (AndL2 name1 trm name2)
  obtain x'::name where "x'(trm{y:=<c>.P},P,name1)"
    by (meson exists_fresh(1) fs_name1)
  with AndL2 show ?case
    by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_AndL2 fresh_atm; blast)
next
  case (OrL name1 trm1 name2 trm2 name3)
  obtain x'::name where "x'(trm1{y:=<c>.P},P,name1,trm2{y:=<c>.P},name2)"
    by (meson exists_fresh(1) fs_name1)
  with OrL show ?case 
    by (auto simp: fs_name1 fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_OrL fresh_atm; blast)
next
  case (ImpL coname trm1 name1 trm2 name2)
  obtain x'::name where "x'(trm1{name2:=<c>.P},P,name1,trm2{name2:=<c>.P})"
    by (meson exists_fresh(1) fs_name1)
  with ImpL show ?case 
    by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_ImpL fresh_atm; blast)
qed (simp add: abs_supp supp_atm trm.supp fs_name1; blast)+

lemma supp_subst3:
  shows "supp (M{c:=(x).P})  ((supp M) - {c})  (supp P)"
proof (nominal_induct M avoiding: x P c rule: trm.strong_induct)
  case (NotR name trm coname)
  obtain x'::coname where "x'(trm{coname:=(x).P},P)"
    by (meson exists_fresh'(2) fs_coname1)
  with NotR show ?case
     by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_NotR; blast)
next
  case (AndR coname1 trm1 coname2 trm2 coname3)
  obtain x'::coname where x': "x'(trm1{coname3:=(x).P},P,trm2{coname3:=(x).P},coname1,coname2)"
    by (meson exists_fresh'(2) fs_coname1)
  with AndR show ?case 
    by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_AndR; blast)
next
  case (OrR1 coname1 trm coname2)
  obtain x'::coname where x': "x'(trm{coname2:=(x).P},P,coname1)"
    by (meson exists_fresh'(2) fs_coname1)
  with OrR1 show ?case 
    by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_OrR1; blast)
next
  case (OrR2 coname1 trm coname2)
  obtain x'::coname where x': "x'(trm{coname2:=(x).P},P,coname1)"
    by (meson exists_fresh'(2) fs_coname1)
  with OrR2 show ?case 
    by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_OrR2; blast)  
next
  case (ImpR name coname1 trm coname2)
  obtain x'::coname where x': "x'(trm{coname2:=(x).P},P,coname1)"
    by (meson exists_fresh'(2) fs_coname1)
  with ImpR show ?case 
    by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_ImpR; blast)
qed (simp add: abs_supp supp_atm trm.supp fs_name1; blast)+


lemma supp_subst4:
  shows "supp (M{c:=(x).P})  (supp M)  ((supp P) - {x})"
proof (nominal_induct M avoiding: x P c rule: trm.strong_induct)
  case (NotR name trm coname)
  obtain x'::coname where "x'(trm{coname:=(x).P},P)"
    by (meson exists_fresh'(2) fs_coname1)
  with NotR show ?case
     by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_NotR; blast)
next
  case (AndR coname1 trm1 coname2 trm2 coname3)
  obtain x'::coname where x': "x'(trm1{coname3:=(x).P},P,trm2{coname3:=(x).P},coname1,coname2)"
    by (meson exists_fresh'(2) fs_coname1)
  with AndR show ?case 
    by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_AndR; blast)
next
  case (OrR1 coname1 trm coname2)
  obtain x'::coname where x': "x'(trm{coname2:=(x).P},P,coname1)"
    by (meson exists_fresh'(2) fs_coname1)
  with OrR1 show ?case 
    by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_OrR1; blast)
next
  case (OrR2 coname1 trm coname2)
  obtain x'::coname where x': "x'(trm{coname2:=(x).P},P,coname1)"
    by (meson exists_fresh'(2) fs_coname1)
  with OrR2 show ?case 
    by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_OrR2; blast)  
next
  case (ImpR name coname1 trm coname2)
  obtain x'::coname where x': "x'(trm{coname2:=(x).P},P,coname1)"
    by (meson exists_fresh'(2) fs_coname1)
  with ImpR show ?case 
    by (auto simp: fresh_prod abs_supp supp_atm trm.supp fs_name1 fresh_fun_simp_ImpR; blast)
qed (simp add: abs_supp supp_atm trm.supp fs_name1; blast)+

lemma supp_subst5:
  shows "(supp M - {y})  supp (M{y:=<c>.P})"
proof (nominal_induct M avoiding: y P c rule: trm.strong_induct)
  case (NotL coname trm name)
  obtain x'::name where "x'(trm{y:=<c>.P},P)"
    by (meson exists_fresh(1) fs_name1)
  with NotL
  show ?case 
    apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_NotL)
     apply (auto simp: fresh_def)
    done
next
  case (AndL1 name1 trm name2)
  obtain x'::name where "x'(trm{y:=<c>.P},P,name1)"
    by (meson exists_fresh(1) fs_name1)
  with AndL1 show ?case
    apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_AndL1)
     apply (auto simp: fresh_def)
    done
next
  case (AndL2 name1 trm name2)
  obtain x'::name where "x'(trm{y:=<c>.P},P,name1)"
    by (meson exists_fresh(1) fs_name1)
  with AndL2 show ?case
    apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_AndL2)
     apply (auto simp: fresh_def)
    done
next
  case (OrL name1 trm1 name2 trm2 name3)
  obtain x'::name where "x'(trm1{y:=<c>.P},P,name1,trm2{y:=<c>.P},name2)"
    by (meson exists_fresh(1) fs_name1)
  with OrL show ?case 
    apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_OrL)
           apply (fastforce simp: fresh_def)+
    done
next
  case (ImpL coname trm1 name1 trm2 name2)
  obtain x'::name where "x'(trm1{name2:=<c>.P},P,name1,trm2{name2:=<c>.P})"
    by (meson exists_fresh(1) fs_name1)
  with ImpL show ?case 
    apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_ImpL)
           apply (fastforce simp: fresh_def)+
    done
qed (simp add: abs_supp supp_atm trm.supp fs_name1; blast)+

lemma supp_subst6:
  shows "(supp M)  ((supp (M{y:=<c>.P}))::coname set)"
proof (nominal_induct M avoiding: y P c rule: trm.strong_induct)
  case (NotL coname trm name)
  obtain x'::name where "x'(trm{y:=<c>.P},P)"
    by (meson exists_fresh(1) fs_name1)
  with NotL
  show ?case 
    apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_NotL)
     apply (auto simp: fresh_def)
    done
next
  case (AndL1 name1 trm name2)
  obtain x'::name where "x'(trm{y:=<c>.P},P,name1)"
    by (meson exists_fresh(1) fs_name1)
  with AndL1 show ?case
    apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_AndL1)
     apply (auto simp: fresh_def)
    done
next
  case (AndL2 name1 trm name2)
  obtain x'::name where "x'(trm{y:=<c>.P},P,name1)"
    by (meson exists_fresh(1) fs_name1)
  with AndL2 show ?case
    apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_AndL2)
     apply (auto simp: fresh_def)
    done
next
  case (OrL name1 trm1 name2 trm2 name3)
  obtain x'::name where "x'(trm1{y:=<c>.P},P,name1,trm2{y:=<c>.P},name2)"
    by (meson exists_fresh(1) fs_name1)
  with OrL show ?case 
    apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_OrL)
           apply (fastforce simp: fresh_def)+
    done
next
  case (ImpL coname trm1 name1 trm2 name2)
  obtain x'::name where "x'(trm1{name2:=<c>.P},P,name1,trm2{name2:=<c>.P})"
    by (meson exists_fresh(1) fs_name1)
  with ImpL show ?case 
    apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_ImpL)
           apply (fastforce simp: fresh_def)+
    done
qed (simp add: abs_supp supp_atm trm.supp fs_name1; blast)+

lemma supp_subst7:
  shows "(supp M - {c})   supp (M{c:=(x).P})"
proof (nominal_induct M avoiding: x P c rule: trm.strong_induct)
  case (NotR name trm coname)
  obtain x'::coname where "x'(trm{coname:=(x).P},P)"
    by (meson exists_fresh'(2) fs_coname1)
  with NotR show ?case
    apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_NotR)
     apply (auto simp: fresh_def)
    done
next
  case (AndR coname1 trm1 coname2 trm2 coname3)
  obtain x'::coname where "x'(trm1{coname3:=(x).P},P,trm2{coname3:=(x).P},coname1,coname2)"
    by (meson exists_fresh'(2) fs_coname1)
  with AndR show ?case
    apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_AndR)
     apply (fastforce simp: fresh_def)+
    done
next
  case (OrR1 coname1 trm coname2)
  obtain x'::coname where "x'(trm{coname2:=(x).P},P,coname1)"
    by (meson exists_fresh'(2) fs_coname1)
  with OrR1 show ?case
    apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_OrR1)
     apply (auto simp: fresh_def)
    done
next
  case (OrR2 coname1 trm coname2)
  obtain x'::coname where "x'(trm{coname2:=(x).P},P,coname1)"
    by (meson exists_fresh'(2) fs_coname1)
  with OrR2 show ?case
    apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_OrR2)
     apply (auto simp: fresh_def)
    done
next
  case (ImpR name coname1 trm coname2)
  obtain x'::coname where "x'(trm{coname2:=(x).P},P,coname1)"
    by (meson exists_fresh'(2) fs_coname1)
  with ImpR show ?case
    apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_ImpR)
     apply (auto simp: fresh_def)
    done
qed (simp add: abs_supp supp_atm trm.supp fs_name1; blast)+
  
lemma supp_subst8:
  shows "(supp M)  ((supp (M{c:=(x).P}))::name set)"
proof (nominal_induct M avoiding: x P c rule: trm.strong_induct)
  case (NotR name trm coname)
  obtain x'::coname where "x'(trm{coname:=(x).P},P)"
    by (meson exists_fresh'(2) fs_coname1)
  with NotR show ?case
    apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_NotR)
     apply (auto simp: fresh_def)
    done
next
  case (AndR coname1 trm1 coname2 trm2 coname3)
  obtain x'::coname where "x'(trm1{coname3:=(x).P},P,trm2{coname3:=(x).P},coname1,coname2)"
    by (meson exists_fresh'(2) fs_coname1)
  with AndR show ?case
    apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_AndR)
     apply (fastforce simp: fresh_def)+
    done
next
  case (OrR1 coname1 trm coname2)
  obtain x'::coname where "x'(trm{coname2:=(x).P},P,coname1)"
    by (meson exists_fresh'(2) fs_coname1)
  with OrR1 show ?case
    apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_OrR1)
     apply (auto simp: fresh_def)
    done
next
  case (OrR2 coname1 trm coname2)
  obtain x'::coname where "x'(trm{coname2:=(x).P},P,coname1)"
    by (meson exists_fresh'(2) fs_coname1)
  with OrR2 show ?case
    apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_OrR2)
     apply (auto simp: fresh_def)
    done
next
  case (ImpR name coname1 trm coname2)
  obtain x'::coname where "x'(trm{coname2:=(x).P},P,coname1)"
    by (meson exists_fresh'(2) fs_coname1)
  with ImpR show ?case
    by (force simp: fresh_prod abs_supp fs_name1 supp_atm trm.supp fresh_fun_simp_ImpR)
qed (simp add: abs_supp supp_atm trm.supp fs_name1; blast)+
  
lemmas subst_supp = supp_subst1 supp_subst2 supp_subst3 supp_subst4
                    supp_subst5 supp_subst6 supp_subst7 supp_subst8
lemma subst_fresh:
  fixes x::"name"
  and   c::"coname"
  shows "xP  xM{x:=<c>.P}"   
  and   "bP  bM{b:=(y).P}"
  and   "x(M,P)  xM{y:=<c>.P}"
  and   "xM  xM{c:=(x).P}"
  and   "x(M,P)  xM{c:=(y).P}"
  and   "b(M,P)  bM{c:=(y).P}"
  and   "bM  bM{y:=<b>.P}"
  and   "b(M,P)  bM{y:=<c>.P}"
  using subst_supp
  by(fastforce simp add: fresh_def supp_prod)+

lemma forget:
  shows "xM  M{x:=<c>.P} = M"
  and   "cM  M{c:=(x).P} = M"
  by (nominal_induct M avoiding: x c P rule: trm.strong_induct)
     (auto simp: fresh_atm abs_fresh abs_supp fin_supp)

lemma substc_rename1:
  assumes a: "c(M,a)"
  shows "M{a:=(x).N} = ([(c,a)]M){c:=(x).N}"
using a
proof(nominal_induct M avoiding: c a x N rule: trm.strong_induct)
  case (AndR c1 M c2 M' c3)
  then show ?case
    apply(auto simp: fresh_prod calc_atm fresh_atm abs_fresh fresh_left)
     apply (metis (no_types, lifting))+
    done
next 
  case ImpL
  then show ?case
    by (auto simp: calc_atm alpha fresh_atm abs_fresh fresh_prod fresh_left)
       metis
next
  case (Cut d M y M')
  then show ?case
    by(simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
      (metis crename.simps(1) crename_id crename_rename)
qed (auto simp: calc_atm alpha fresh_atm abs_fresh fresh_prod fresh_left trm.inject)

lemma substc_rename2:
  assumes a: "y(N,x)"
  shows "M{a:=(x).N} = M{a:=(y).([(y,x)]N)}"
using a
proof(nominal_induct M avoiding: a x y N rule: trm.strong_induct)
  case (NotR y M d)
  obtain a::coname where "a(N,M{d:=(y).([(y,x)]N)},[(y,x)]N)"
    by (meson exists_fresh(2) fs_coname1)
  with NotR show ?case
    apply(auto simp: calc_atm alpha fresh_atm fresh_prod fresh_left)
    by (metis (no_types, opaque_lifting) alpha(1) trm.inject(2))
next
  case (AndR c1 M c2 M' c3)
  obtain a'::coname where "a'(N,M{c3:=(y).([(y,x)]N)},M'{c3:=(y).([(y,x)]N)},[(y,x)]N,c1,c2,c3)"
    by (meson exists_fresh(2) fs_coname1)
  with AndR show ?case
    apply(auto simp: calc_atm alpha fresh_atm fresh_prod fresh_left)
    by (metis (no_types, opaque_lifting) alpha(1) trm.inject(2))
next
  case (OrR1 d M e)
  obtain a'::coname where "a'(N,M{e:=(y).([(y,x)]N)},[(y,x)]N,d,e)"
    by (meson exists_fresh(2) fs_coname1)
  with OrR1 show ?case 
    by (auto simp: perm_swap calc_atm trm.inject alpha fresh_atm fresh_prod fresh_left fresh_fun_simp_OrR1)
next
  case (OrR2 d M e)
  obtain a'::coname where "a'(N,M{e:=(y).([(y,x)]N)},[(y,x)]N,d,e)"
    by (meson exists_fresh(2) fs_coname1)
  with OrR2 show ?case 
    by (auto simp: perm_swap calc_atm trm.inject alpha fresh_atm fresh_prod fresh_left fresh_fun_simp_OrR2)
next
  case (ImpR y d M e)
  obtain a'::coname where "a'(N,M{e:=(y).([(y,x)]N)},[(y,x)]N,d,e)"
    by (meson exists_fresh(2) fs_coname1)
  with ImpR show ?case 
    by (auto simp: perm_swap calc_atm trm.inject alpha fresh_atm fresh_prod fresh_left fresh_fun_simp_ImpR) 
qed (auto simp: calc_atm trm.inject alpha fresh_atm fresh_prod fresh_left perm_swap)

lemma substn_rename3:
  assumes a: "y(M,x)"
  shows "M{x:=<a>.N} = ([(y,x)]M){y:=<a>.N}"
using a
proof(nominal_induct M avoiding: a x y N rule: trm.strong_induct)
  case (OrL x1 M x2 M' x3)
  then show ?case
    apply(auto simp add: calc_atm fresh_atm abs_fresh fresh_prod fresh_left)
    by (metis (mono_tags))+
next
  case (ImpL d M v M' u)
  then show ?case
    apply(auto simp add: calc_atm fresh_atm abs_fresh fresh_prod fresh_left)
    by (metis (mono_tags))+
next
  case (Cut d M y M')
  then show ?case
    apply(auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
    by (metis nrename.simps(1) nrename_id nrename_rename)+
qed (auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_left abs_supp fin_supp fresh_prod)

lemma substn_rename4:
  assumes a: "c(N,a)"
  shows "M{x:=<a>.N} = M{x:=<c>.([(c,a)]N)}"
using a
proof(nominal_induct M avoiding: x c a N rule: trm.strong_induct)
  case (Ax z d)
  then show ?case 
    by (auto simp: fresh_prod fresh_atm calc_atm trm.inject alpha perm_swap fresh_left)
next
  case NotR
  then show ?case 
    by (auto simp: fresh_prod fresh_atm calc_atm trm.inject alpha perm_swap fresh_left)
next
  case (NotL d M y)
  then obtain a'::name where "a'(N, M{x:=<c>.([(c,a)]N)}, [(c,a)]N)"
    by (meson exists_fresh(1) fs_name1)
  with NotL show ?case
    apply(auto simp: calc_atm trm.inject fresh_atm fresh_prod fresh_left)
    by (metis (no_types, opaque_lifting) alpha(2) trm.inject(2))
next
  case (OrL x1 M x2 M' x3)
  then obtain a'::name where "a'(N,M{x:=<c>.([(c,a)]N)},M'{x:=<c>.([(c,a)]N)},[(c,a)]N,x1,x2,x3)"
    by (meson exists_fresh(1) fs_name1)  
  with OrL show ?case
    apply(auto simp: calc_atm trm.inject fresh_atm fresh_prod fresh_left)
    by (metis (no_types) alpha'(2) trm.inject(2))
next
  case (AndL1 u M v)
  then obtain a'::name where "a'(N,M{x:=<c>.([(c,a)]N)},[(c,a)]N,u,v)"
    by (meson exists_fresh(1) fs_name1)  
  with AndL1 show ?case 
    apply(auto simp: calc_atm trm.inject fresh_atm fresh_prod fresh_left)
    by (metis (mono_tags, opaque_lifting) alpha'(2) trm.inject(2))
next
  case (AndL2 u M v)
  then obtain a'::name where "a'(N,M{x:=<c>.([(c,a)]N)},[(c,a)]N,u,v)"
    by (meson exists_fresh(1) fs_name1)  
  with AndL2 show ?case 
    apply(auto simp: calc_atm trm.inject fresh_atm fresh_prod fresh_left)
    by (metis (mono_tags, opaque_lifting) alpha'(2) trm.inject(2))
next
  case (ImpL d M y M' u)
  then obtain a'::name where "a'(N,M{u:=<c>.([(c,a)]N)},M'{u:=<c>.([(c,a)]N)},[(c,a)]N,y,u)"
    by (meson exists_fresh(1) fs_name1)  
  with ImpL show ?case
    apply(auto simp: calc_atm trm.inject fresh_atm fresh_prod fresh_left)
    by (metis (no_types) alpha'(2) trm.inject(2))
next
  case (Cut d M y M')
  then show ?case
    by (auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left perm_swap)
qed (auto simp: calc_atm fresh_atm fresh_left)

lemma subst_rename5:
  assumes a: "c'(c,N)" "x'(x,M)"
  shows "M{x:=<c>.N} = ([(x',x)]M){x':=<c'>.([(c',c)]N)}"
proof -
  have "M{x:=<c>.N} = ([(x',x)]M){x':=<c>.N}" using a by (simp add: substn_rename3)
  also have " = ([(x',x)]M){x':=<c'>.([(c',c)]N)}" using a by (simp add: substn_rename4)
  finally show ?thesis by simp
qed

lemma subst_rename6:
  assumes a: "c'(c,M)" "x'(x,N)"
  shows "M{c:=(x).N} = ([(c',c)]M){c':=(x').([(x',x)]N)}"
proof -
  have "M{c:=(x).N} = ([(c',c)]M){c':=(x).N}" using a by (simp add: substc_rename1)
  also have " = ([(c',c)]M){c':=(x').([(x',x)]N)}" using a by (simp add: substc_rename2)
  finally show ?thesis by simp
qed

lemmas subst_rename = substc_rename1 substc_rename2 substn_rename3 substn_rename4 subst_rename5 subst_rename6

lemma better_Cut_substn[simp]:
  assumes a: "a[c].P" "x(y,P)"
  shows "(Cut <a>.M (x).N){y:=<c>.P} = 
  (if M=Ax y a then Cut <c>.P (x).(N{y:=<c>.P}) else Cut <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}))"
proof -   
  obtain x'::"name"   where fs1: "x'(M,N,c,P,x,y)" by (rule exists_fresh(1), rule fin_supp, blast)
  obtain a'::"coname" where fs2: "a'(M,N,c,P,a)" by (rule exists_fresh(2), rule fin_supp, blast)
  have eq1: "(Cut <a>.M (x).N) = (Cut <a'>.([(a',a)]M) (x').([(x',x)]N))"
    using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
  have eq2: "(M=Ax y a) = (([(a',a)]M)=Ax y a')"
    by (metis perm_swap(4) swap_simps(4) swap_simps(8) trm.perm(13))
  have "(Cut <a>.M (x).N){y:=<c>.P} = (Cut <a'>.([(a',a)]M) (x').([(x',x)]N)){y:=<c>.P}" 
    using eq1 by simp
  also have " = (if ([(a',a)]M)=Ax y a' then Cut <c>.P (x').(([(x',x)]N){y:=<c>.P}) 
                              else Cut <a'>.(([(a',a)]M){y:=<c>.P}) (x').(([(x',x)]N){y:=<c>.P}))" 
    using fs1 fs2 by (auto simp: fresh_prod fresh_left calc_atm fresh_atm)
  also have " =(if M=Ax y a then Cut <c>.P (x).(N{y:=<c>.P}) else Cut <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}))"
    using fs1 fs2 a
    unfolding eq2[symmetric]
    apply(auto simp: trm.inject)
    apply(simp_all add: alpha fresh_atm fresh_prod subst_fresh eqvts perm_fresh_fresh calc_atm)
    apply (simp add: fresh_atm(2) substn_rename4)
    by (metis abs_fresh(2) fresh_atm(2) fresh_prod perm_fresh_fresh(2) substn_rename4)
  finally show ?thesis by simp
qed
    
lemma better_Cut_substc[simp]:
  assumes a: "a(c,P)" "x[y].P"
  shows "(Cut <a>.M (x).N){c:=(y).P} = 
  (if N=Ax x c then Cut <a>.(M{c:=(y).P}) (y).P else Cut <a>.(M{c:=(y).P}) (x).(N{c:=(y).P}))" 
proof -   
  obtain x'::"name"   where fs1: "x'(M,N,c,P,x,y)" by (rule exists_fresh(1), rule fin_supp, blast)
  obtain a'::"coname" where fs2: "a'(M,N,c,P,a)" by (rule exists_fresh(2), rule fin_supp, blast)
  have eq1: "(Cut <a>.M (x).N) = (Cut <a'>.([(a',a)]M) (x').([(x',x)]N))"
    using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
  have eq2: "(N=Ax x c) = (([(x',x)]N)=Ax x' c)"
    by (metis perm_dj(1) perm_swap(1) swap_simps(1) trm.perm(1))
  have "(Cut <a>.M (x).N){c:=(y).P} = (Cut <a'>.([(a',a)]M) (x').([(x',x)]N)){c:=(y).P}" 
    using eq1 by simp
  also have " = (if ([(x',x)]N)=Ax x' c then  Cut <a'>.(([(a',a)]M){c:=(y).P}) (y).P
                              else Cut <a'>.(([(a',a)]M){c:=(y).P}) (x').(([(x',x)]N){c:=(y).P}))" 
    using fs1 fs2  by (simp add: fresh_prod fresh_left calc_atm fresh_atm trm.inject)
  also have " =(if N=Ax x c then Cut <a>.(M{c:=(y).P}) (y).P else Cut <a>.(M{c:=(y).P}) (x).(N{c:=(y).P}))"
    using fs1 fs2 a
    unfolding eq2[symmetric]
    apply(auto simp: trm.inject)
    apply(simp_all add: alpha fresh_atm fresh_prod subst_fresh eqvts perm_fresh_fresh calc_atm)
    by (metis abs_fresh(1) fresh_atm(1) fresh_prod perm_fresh_fresh(1) substc_rename2)
  finally show ?thesis by simp
qed

lemma better_Cut_substn':
  assumes "a[c].P" "y(N,x)" "MAx y a"
  shows "(Cut <a>.M (x).N){y:=<c>.P} = Cut <a>.(M{y:=<c>.P}) (x).N"
proof -
  obtain d::name where d: "d  (M, N, P, a, c, x, y)"
    by (meson exists_fresh(1) fs_name1)
  then have *: "y([(d,x)]N)"
    by (metis assms(2) fresh_atm(1) fresh_list_cons fresh_list_nil fresh_perm_name fresh_prod)
  with d have "Cut <a>.M (x).N = Cut <a>.M (d).([(d,x)]N)"
    by (metis (no_types, lifting) alpha(1) fresh_prodD perm_fresh_fresh(1) trm.inject(2))
  with * d assms show ?thesis
    apply(simp add: fresh_prod)
    by (smt (verit, ccfv_SIG) forget(1) trm.inject(2))
qed

lemma better_NotR_substc:
  assumes a: "dM"
  shows "(NotR (x).M d){d:=(z).P} = fresh_fun (λa'. Cut <a'>.NotR (x).M a' (z).P)"
proof -
  obtain c::name where c: "c  (M, P, d, x, z)"
    by (meson exists_fresh(1) fs_name1)
  obtain e::coname where e: "e  (M, P, d, x, z, c)"
    by (meson exists_fresh'(2) fs_coname1)
  with c have "NotR (x).M d = NotR (c).([(c,x)]M) d"
    by (metis alpha'(1) fresh_prodD(1) nrename_id nrename_swap trm.inject(3))
  with c e assms show ?thesis
    apply(simp add: fresh_prod)
    by (metis forget(2) fresh_perm_app(3) trm.inject(3))
qed

lemma better_NotL_substn:
  assumes a: "yM"
  shows "(NotL <a>.M y){y:=<c>.P} = fresh_fun (λx'. Cut <c>.P (x').NotL <a>.M x')"
proof (generate_fresh "coname")
  fix ca :: coname
  assume d: "ca  (M, P, a, c, y)"
  then have "NotL <a>.M y = NotL <ca>.([(ca,a)]M) y"
    by (metis alpha(2) fresh_prod perm_fresh_fresh(2) trm.inject(4))
  with a d show ?thesis
    apply(simp add: fresh_left calc_atm forget)
    apply (metis trm.inject(4))
    done
qed

lemma better_AndL1_substn:
  assumes a: "y[x].M"
  shows "(AndL1 (x).M y){y:=<c>.P} = fresh_fun (λz'. Cut <c>.P (z').AndL1 (x).M z')"
proof (generate_fresh "name")
  fix d:: name
  assume d: "d  (M, P, c, x, y)"
  then have §: "AndL1 (x).M y = AndL1 (d).([(d,x)]M) y"
    by (metis alpha(1) fresh_prodD(1) perm_fresh_fresh(1) trm.inject(6))
  with d have "(λz'. Cut <c>.P (z').AndL1 (d).([(d, x)]  M){x:=<c>.P} (z')) 
             = (λz'. Cut <c>.P (z').AndL1 (x).M (z'))"
    by (metis forget(1) fresh_bij(1) fresh_prodD(1) swap_simps(1) trm.inject(6))
  with d have "(λz'. Cut <c>.P (z').AndL1 d.([(d, x)]  M){y:=<c>.P} z')
             = (λz'. Cut <c>.P (z').AndL1 (x).M (z'))"
    apply(simp add: trm.inject alpha fresh_prod fresh_atm)
    by (metis abs_fresh(1) assms forget(1) fresh_atm(1) fresh_aux(1) nrename_nfresh nrename_swap)
  with d § show ?thesis
    by (simp add: fresh_left calc_atm)
qed

lemma better_AndL2_substn:
  assumes a: "y[x].M"
  shows "(AndL2 (x).M y){y:=<c>.P} = fresh_fun (λz'. Cut <c>.P (z').AndL2 (x).M z')"
proof (generate_fresh "name")
  fix d:: name
  assume d: "d  (M, P, c, x, y)"
  then have §: "AndL2 (x).M y = AndL2 (d).([(d,x)]M) y"
    by (metis alpha(1) fresh_prodD(1) perm_fresh_fresh(1) trm.inject(7))
  with d have "(λz'. Cut <c>.P (z').AndL2 (d).([(d, x)]  M){x:=<c>.P} (z')) 
             = (λz'. Cut <c>.P (z').AndL2 (x).M (z'))"
    by (metis forget(1) fresh_bij(1) fresh_prodD(1) swap_simps(1) trm.inject(7))
  with d have "(λz'. Cut <c>.P (z').AndL2 d.([(d, x)]  M){y:=<c>.P} z')
             = (λz'. Cut <c>.P (z').AndL2 (x).M (z'))"
    apply(simp add: trm.inject alpha fresh_prod fresh_atm)
    by (metis abs_fresh(1) assms forget(1) fresh_atm(1) fresh_aux(1) nrename_nfresh nrename_swap)
  with d § show ?thesis
    by (simp add: fresh_left calc_atm)
qed

lemma better_AndR_substc:
  assumes "c([a].M,[b].N)"
  shows "(AndR <a>.M <b>.N c){c:=(z).P} = fresh_fun (λa'. Cut <a'>.(AndR <a>.M <b>.N a') (z).P)"
proof (generate_fresh "coname" , generate_fresh "coname")
  fix d :: coname
    and e :: coname
  assume d: "d  (M, N, P, a, b, c, z)"
    and e: "e  (M, N, P, a, b, c, z, d)"
  then have "AndR <a>.M <b>.N c = AndR <d>.([(d,a)]M) <e>.([(e,b)]N) c"
    by (perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm) auto
  with assms d e show ?thesis
    apply (auto simp: fresh_left calc_atm fresh_prod fresh_atm)
    by (metis (no_types, opaque_lifting) abs_fresh(2) forget(2) trm.inject(5))
qed

lemma better_OrL_substn:
  assumes "x([y].M,[z].N)"
  shows "(OrL (y).M (z).N x){x:=<c>.P} = fresh_fun (λz'. Cut <c>.P (z').OrL (y).M (z).N z')"
proof (generate_fresh "name" , generate_fresh "name")
  fix d :: name
    and e :: name
  assume d: "d  (M, N, P, c, x, y, z)"
    and e: "e  (M, N, P, c, x, y, z, d)"
  with assms have "OrL (y).M (z).N x = OrL (d).([(d,y)]M) (e).([(e,z)]N) x"
    by (perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm) auto
  with assms d e show ?thesis
    apply (auto simp: fresh_left calc_atm fresh_prod fresh_atm)
    by (metis (no_types, lifting) abs_fresh(1) forget(1) trm.inject(10))
qed

lemma better_OrR1_substc:
  assumes a: "d[a].M"
  shows "(OrR1 <a>.M d){d:=(z).P} = fresh_fun (λa'. Cut <a'>.OrR1 <a>.M a' (z).P)"
proof (generate_fresh "coname")
  fix c :: coname
  assume c: "c  (M, P, a, d, z)"
  then have "OrR1 <a>.M d = OrR1 <c>.([(c,a)]M) d"
    by (perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm) auto
  with assms c show ?thesis
    apply (auto simp: fresh_left calc_atm fresh_prod fresh_atm)
    by (metis abs_fresh(2) forget(2) trm.inject(8))
qed

lemma better_OrR2_substc:
  assumes a: "d[a].M"
  shows "(OrR2 <a>.M d){d:=(z).P} = fresh_fun (λa'. Cut <a'>.OrR2 <a>.M a' (z).P)"
proof (generate_fresh "coname")
  fix c :: coname
  assume c: "c  (M, P, a, d, z)"
  then have "OrR2 <a>.M d = OrR2 <c>.([(c,a)]M) d"
    by (perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm) auto
  with assms c show ?thesis
    apply (auto simp: fresh_left calc_atm fresh_prod fresh_atm)
    by (metis abs_fresh(2) forget(2) trm.inject(9))
qed

lemma better_ImpR_substc:
  assumes "d[a].M"
  shows "(ImpR (x).<a>.M d){d:=(z).P} = fresh_fun (λa'. Cut <a'>.ImpR (x).<a>.M a' (z).P)"
proof (generate_fresh "coname" , generate_fresh "name")
  fix c :: coname
    and c' :: name
  assume c: "c  (M, P, a, d, x, z)"
    and c': "c'  (M, P, a, d, x, z, c)"
  have : "ImpR (x).<a>.M d = ImpR (c').<c>.([(c,a)][(c',x)]M) d"
    apply (rule sym)
    using c c'
    apply(perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm abs_fresh abs_perm)
    done
  with assms c c' have "fresh_fun
        (λa'. Cut <a'>.ImpR (c').<c>.(([(c, a)]  [(c', x)]  M)){d:=(z).P} a' (z).P)
      = fresh_fun (λa'. Cut <a'>.ImpR (x).<a>.M a' (z).P)"
    apply(intro arg_cong [where f="fresh_fun"])
    by(fastforce simp add: trm.inject alpha fresh_prod fresh_atm abs_perm fresh_left calc_atm abs_fresh forget)
  with assms c c'  show ?thesis
    by (auto simp: fresh_left calc_atm forget abs_fresh)
qed

lemma better_ImpL_substn:
  assumes "y(M,[x].N)"
  shows "(ImpL <a>.M (x).N y){y:=<c>.P} = fresh_fun (λz'. Cut <c>.P (z').ImpL <a>.M (x).N z')"
proof (generate_fresh "coname" , generate_fresh "name")
  fix ca :: coname
    and caa :: name
  assume d: "ca  (M, N, P, a, c, x, y)"
    and e: "caa  (M, N, P, a, c, x, y, ca)"
  have "ImpL <a>.M (x).N y = ImpL <ca>.([(ca,a)]M) (caa).([(caa,x)]N) y"
    apply(rule sym)
    using d e
    by(perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm abs_fresh abs_perm)
  with d e assms show ?thesis
    apply(simp add: fresh_left calc_atm forget abs_fresh)
    apply(intro arg_cong [where f="fresh_fun"] ext)
    apply(simp add: trm.inject alpha fresh_prod fresh_atm abs_perm abs_fresh fresh_left calc_atm)
    by (metis forget(1) fresh_aux(1) fresh_bij(1) swap_simps(1))
qed

lemma freshn_after_substc:
  fixes x::"name"
  assumes "xM{c:=(y).P}"
  shows "xM"
  by (meson assms fresh_def subsetD supp_subst8)

lemma freshn_after_substn:
  fixes x::"name"
  assumes "xM{y:=<c>.P}" "xy"
  shows "xM"
  by (meson DiffI assms fresh_def singleton_iff subset_eq supp_subst5)

lemma freshc_after_substc:
  fixes a::"coname"
  assumes "aM{c:=(y).P}" "ac"
  shows "aM"
  by (meson Diff_iff assms fresh_def in_mono singleton_iff supp_subst7)

lemma freshc_after_substn:
  fixes a::"coname"
  assumes "aM{y:=<c>.P}" 
  shows "aM"
  by (meson assms fresh_def subset_iff supp_subst6)

lemma substn_crename_comm:
  assumes "ca" "cb"
  shows "M{x:=<c>.P}[a⊢c>b] = M[a⊢c>b]{x:=<c>.(P[a⊢c>b])}"
using assms
proof (nominal_induct M avoiding: x c P a b rule: trm.strong_induct)
  case (Ax name coname)
  then show ?case
    by(auto simp: better_crename_Cut fresh_atm)
next
  case (Cut coname trm1 name trm2)
  then show ?case
    apply(simp add: rename_fresh better_crename_Cut fresh_atm)
    by (meson crename_ax)
next
  case (NotL coname trm name)
  obtain x'::name where "x'(trm{x:=<c>.P},P,P[a⊢c>b],x,trm[a⊢c>b]{x:=<c>.P[a⊢c>b]})"
    by (meson exists_fresh(1) fs_name1)
  with NotL show ?case
    apply (simp add: subst_fresh rename_fresh trm.inject)
    by (force simp: fresh_prod fresh_fun_simp_NotL better_crename_Cut fresh_atm)
next
  case (AndL1 name1 trm name2)
  obtain x'::name where "x'(trm{x:=<c>.P},P,P[a⊢c>b],name1,trm[a⊢c>b]{x:=<c>.P[a⊢c>b]})"
    by (meson exists_fresh(1) fs_name1)
  with AndL1 show ?case
    apply (simp add: subst_fresh rename_fresh trm.inject)
    apply (force simp: fresh_prod fresh_fun_simp_AndL1 better_crename_Cut fresh_atm)
    done
next
  case (AndL2 name1 trm name2)
  obtain x'::name where x': "x'(trm{x:=<c>.P},P,P[a⊢c>b],name1,trm[a⊢c>b]{x:=<c>.P[a⊢c>b]})"
    by (meson exists_fresh(1) fs_name1)
  with AndL2 show ?case
    apply (simp add: subst_fresh rename_fresh trm.inject)
    apply (auto simp: fresh_prod fresh_fun_simp_AndL2 better_crename_Cut fresh_atm)
    done
next
  case (OrL name1 trm1 name2 trm2 name3)
  obtain x'::name where x': "x'(trm1{x:=<c>.P},trm2{x:=<c>.P},P,P[a⊢c>b],name1,name2,
                                  trm1[a⊢c>b]{x:=<c>.P[a⊢c>b]},trm2[a⊢c>b]{x:=<c>.P[a⊢c>b]})"
    by (meson exists_fresh(1) fs_name1)
  with OrL show ?case
    apply (simp add: subst_fresh rename_fresh trm.inject)
    apply (auto simp: fresh_atm subst_fresh fresh_prod fresh_fun_simp_OrL better_crename_Cut)
    done
  next
  case (ImpL coname trm1 name1 trm2 name2)
  obtain x'::name where x': "x'(trm1{x:=<c>.P},trm2{x:=<c>.P},P,P[a⊢c>b],name1,name2,
                                  trm1[a⊢c>b]{x:=<c>.P[a⊢c>b]},trm2[a⊢c>b]{x:=<c>.P[a⊢c>b]})"
    by (meson exists_fresh(1) fs_name1)
  with ImpL show ?case
    apply (simp add: subst_fresh rename_fresh trm.inject)
    apply (auto simp: fresh_atm subst_fresh fresh_prod fresh_fun_simp_ImpL better_crename_Cut)
    done
qed (auto simp: subst_fresh rename_fresh)


lemma substc_crename_comm:
  assumes "ca" "cb"
  shows "M{c:=(x).P}[a⊢c>b] = M[a⊢c>b]{c:=(x).(P[a⊢c>b])}"
using assms
proof (nominal_induct M avoiding: x c P a b rule: trm.strong_induct)
  case (Ax name coname)
  then show ?case
    by(auto simp: better_crename_Cut fresh_atm)
next
  case (Cut coname trm1 name trm2)
  then show ?case
    apply(simp add: rename_fresh  better_crename_Cut)
    by (meson crename_ax)
next
  case (NotR name trm coname)
  obtain c'::coname where "c'(a,b,trm{coname:=(x).P},P,P[a⊢c>b],x,trm[a⊢c>b]{coname:=(x).P[a⊢c>b]})"
    by (meson exists_fresh' fs_coname1)
  with NotR show ?case
    apply(simp add: subst_fresh rename_fresh trm.inject)
    by(auto simp: fresh_prod fresh_fun_simp_NotR better_crename_Cut fresh_atm)
next
  case (AndR coname1 trm1 coname2 trm2 coname3)
  obtain c'::coname where "c'(coname1,coname2,a,b,trm1{coname3:=(x).P},trm2{coname3:=(x).P},
                   P,P[a⊢c>b],x,trm1[a⊢c>b]{coname3:=(x).P[a⊢c>b]},trm2[a⊢c>b]{coname3:=(x).P[a⊢c>b]})"
    by (meson exists_fresh' fs_coname1)
  with AndR show ?case
    apply(simp add: subst_fresh rename_fresh trm.inject)
    by (auto simp: fresh_prod fresh_fun_simp_AndR better_crename_Cut subst_fresh fresh_atm)
next
  case (OrR1 coname1 trm coname2)
  obtain c'::coname where "c'(coname1,trm{coname2:=(x).P},P,P[a⊢c>b],a,b, trm[a⊢c>b]{coname2:=(x).P[a⊢c>b]})"
    by (meson exists_fresh' fs_coname1)
  with OrR1 show ?case
    apply(simp add: subst_fresh rename_fresh trm.inject)
    by(auto simp: fresh_prod fresh_fun_simp_OrR1 better_crename_Cut fresh_atm)
next
  case (OrR2 coname1 trm coname2)
  obtain c'::coname where "c'(coname1,trm{coname2:=(x).P},P,P[a⊢c>b],a,b, trm[a⊢c>b]{coname2:=(x).P[a⊢c>b]})"
    by (meson exists_fresh' fs_coname1)
  with OrR2 show ?case
    apply(simp add: subst_fresh rename_fresh trm.inject)
    by(auto simp: fresh_prod fresh_fun_simp_OrR2 better_crename_Cut fresh_atm)
next
  case (ImpR name coname1 trm coname2)
  obtain c'::coname where "c'(coname1,trm{coname2:=(x).P},P,P[a⊢c>b],a,b, trm[a⊢c>b]{coname2:=(x).P[a⊢c>b]})"
    by (meson exists_fresh' fs_coname1)
  with ImpR show ?case
    apply(simp add: subst_fresh rename_fresh trm.inject)
    by(auto simp: fresh_prod fresh_fun_simp_ImpR better_crename_Cut fresh_atm)
qed (auto simp: subst_fresh rename_fresh trm.inject)


lemma substn_nrename_comm:
  assumes "xy" "xz"
  shows "M{x:=<c>.P}[y⊢n>z] = M[y⊢n>z]{x:=<c>.(P[y⊢n>z])}"
using assms
proof (nominal_induct M avoiding: x c P y z rule: trm.strong_induct)
  case (Ax name coname)
  then show ?case
    by (auto simp: better_nrename_Cut fresh_atm)
next
  case (Cut coname trm1 name trm2)
  then show ?case
    apply(clarsimp simp: subst_fresh rename_fresh trm.inject better_nrename_Cut)
    by (meson nrename_ax)
next
  case (NotL coname trm name)
  obtain x'::name where "x'(y,z,trm{x:=<c>.P},P,P[y⊢n>z],x,trm[y⊢n>z]{x:=<c>.P[y⊢n>z]})"
    by (meson exists_fresh' fs_name1)
  with NotL show ?case 
    apply(clarsimp simp: rename_fresh trm.inject)
    by (auto simp add: fresh_prod fresh_fun_simp_NotL better_nrename_Cut fresh_atm)
next
  case (AndL1 name1 trm name2)  
  obtain x'::name where "x'(trm{x:=<c>.P},P,P[y⊢n>z],name1,trm[y⊢n>z]{x:=<c>.P[y⊢n>z]},y,z)"
    by (meson exists_fresh' fs_name1)
  with AndL1 show ?case
    apply(clarsimp simp: subst_fresh rename_fresh trm.inject)
    by (auto simp add: fresh_prod fresh_fun_simp_AndL1 better_nrename_Cut fresh_atm)
next
  case (AndL2 name1 trm name2)
  obtain x'::name where "x'(trm{x:=<c>.P},P,P[y⊢n>z],name1,trm[y⊢n>z]{x:=<c>.P[y⊢n>z]},y,z)"
    by (meson exists_fresh' fs_name1)
  with AndL2 show ?case
    apply(clarsimp simp: subst_fresh rename_fresh trm.inject)
    by (auto simp add: fresh_prod fresh_fun_simp_AndL2 better_nrename_Cut fresh_atm)
next
  case (OrL name1 trm1 name2 trm2 name3)
  obtain x'::name where "x'(trm1{x:=<c>.P},trm2{x:=<c>.P},P,P[y⊢n>z],name1,name2,y,z,
                                  trm1[y⊢n>z]{x:=<c>.P[y⊢n>z]},trm2[y⊢n>z]{x:=<c>.P[y⊢n>z]})"
    by (meson exists_fresh' fs_name1)
  with OrL show ?case
    apply (clarsimp simp: subst_fresh rename_fresh trm.inject)
    by (auto simp add: fresh_prod fresh_fun_simp_OrL better_nrename_Cut subst_fresh fresh_atm)
next
  case (ImpL coname trm1 name1 trm2 name2)
  obtain x'::name where "x'(trm1{x:=<c>.P},trm2{x:=<c>.P},P,P[y⊢n>z],name1,name2,y,z,
                                  trm1[y⊢n>z]{x:=<c>.P[y⊢n>z]},trm2[y⊢n>z]{x:=<c>.P[y⊢n>z]})"
    by (meson exists_fresh' fs_name1)
  with ImpL show ?case
    apply (clarsimp simp: subst_fresh rename_fresh trm.inject)
    by (auto simp add: fresh_prod fresh_fun_simp_ImpL better_nrename_Cut subst_fresh fresh_atm)
qed (auto simp: subst_fresh rename_fresh trm.inject)
 


lemma substc_nrename_comm:
  assumes "xy" "xz"
  shows "M{c:=(x).P}[y⊢n>z] = M[y⊢n>z]{c:=(x).(P[y⊢n>z])}"
using assms
proof (nominal_induct M avoiding: x c P y z rule: trm.strong_induct)
  case (Ax name coname)
  then show ?case 
    by (auto simp: subst_fresh rename_fresh trm.inject better_nrename_Cut fresh_atm)
next
  case (Cut coname trm1 name trm2)
  then show ?case
    apply (clarsimp simp: subst_fresh rename_fresh trm.inject better_nrename_Cut fresh_atm)
    by (metis nrename_ax)
next
  case (NotR name trm coname)
  obtain c'::coname where "c'(y,z,trm{coname:=(x).P},P,P[y⊢n>z],x,trm[y⊢n>z]{coname:=(x).P[y⊢n>z]})"
    by (meson exists_fresh' fs_coname1)
  with NotR show ?case
    apply(simp add: subst_fresh rename_fresh trm.inject)
    by (auto simp add: fresh_prod fresh_fun_simp_NotR better_nrename_Cut fresh_atm)
next
  case (AndR coname1 trm1 coname2 trm2 coname3)
  obtain c'::coname where "c'(coname1,coname2,y,z,trm1{coname3:=(x).P},trm2{coname3:=(x).P},
                   P,P[y⊢n>z],x,trm1[y⊢n>z]{coname3:=(x).P[y⊢n>z]},trm2[y⊢n>z]{coname3:=(x).P[y⊢n>z]})"
    by (meson exists_fresh' fs_coname1)
  with AndR show ?case
    apply(simp add: subst_fresh rename_fresh trm.inject)
    by (auto simp add: fresh_prod fresh_fun_simp_AndR better_nrename_Cut fresh_atm subst_fresh)
next
  case (OrR1 coname1 trm coname2)
  obtain c'::coname where "c'(coname1,trm{coname2:=(x).P},P,P[y⊢n>z],y,z,
                         trm[y⊢n>z]{coname2:=(x).P[y⊢n>z]})"
    by (meson exists_fresh' fs_coname1)
  with OrR1 show ?case
    apply(simp add: subst_fresh rename_fresh trm.inject)
    by (auto simp add: fresh_prod fresh_fun_simp_OrR1 better_nrename_Cut fresh_atm subst_fresh)
next
  case (OrR2 coname1 trm coname2)
  obtain c'::coname where "c'(coname1,trm{coname2:=(x).P},P,P[y⊢n>z],y,z,
                         trm[y⊢n>z]{coname2:=(x).P[y⊢n>z]})"
    by (meson exists_fresh' fs_coname1)
  with OrR2 show ?case
    apply(simp add: subst_fresh rename_fresh trm.inject)
    by (auto simp add: fresh_prod fresh_fun_simp_OrR2 better_nrename_Cut fresh_atm subst_fresh)
next
  case (ImpR name coname1 trm coname2)
  obtain c'::coname where "c'(coname1,trm{coname2:=(x).P},P,P[y⊢n>z],y,z,
                         trm[y⊢n>z]{coname2:=(x).P[y⊢n>z]})"
    by (meson exists_fresh' fs_coname1)
  with ImpR show ?case
    apply(simp add: subst_fresh rename_fresh trm.inject)
    by (auto simp add: fresh_prod fresh_fun_simp_ImpR better_nrename_Cut fresh_atm subst_fresh)
qed (auto simp: subst_fresh rename_fresh trm.inject)


lemma substn_crename_comm':
  assumes "ac" "aP"
  shows "M{x:=<c>.P}[a⊢c>b] = M[a⊢c>b]{x:=<c>.P}"
proof -
  obtain c'::"coname" where fs2: "c'(c,P,a,b)" by (rule exists_fresh(2), rule fin_supp, blast)
  have eq: "M{x:=<c>.P} = M{x:=<c'>.([(c',c)]P)}"
    using fs2 substn_rename4 by force
   have eq': "M[a⊢c>b]{x:=<c>.P} = M[a⊢c>b]{x:=<c'>.([(c',c)]P)}"
    using fs2 by (simp add: substn_rename4)
  have eq2: "([(c',c)]P)[a⊢c>b] = ([(c',c)]P)" using fs2 assms
    by (metis crename_fresh fresh_atm(2) fresh_aux(2) fresh_prod)
  have "M{x:=<c>.P}[a⊢c>b] = M{x:=<c'>.([(c',c)]P)}[a⊢c>b]" using eq by simp
  also have " = M[a⊢c>b]{x:=<c'>.(([(c',c)]P)[a⊢c>b])}"
    using fs2
    by (simp add: fresh_atm(2) fresh_prod substn_crename_comm)
  also have " = M[a⊢c>b]{x:=<c'>.(([(c',c)]P))}" using eq2 by simp
  also have " = M[a⊢c>b]{x:=<c>.P}" using eq' by simp 
  finally show ?thesis by simp
qed

lemma substc_crename_comm':
  assumes "ca" "cb" "aP"
  shows "M{c:=(x).P}[a⊢c>b] = M[a⊢c>b]{c:=(x).P}"
proof -
  obtain c'::"coname" where fs2: "c'(c,M,a,b)" by (rule exists_fresh(2), rule fin_supp, blast)
  have eq: "M{c:=(x).P} = ([(c',c)]M){c':=(x).P}"
    using fs2 by (simp add: substc_rename1)
   have eq': "([(c',c)](M[a⊢c>b])){c':=(x).P} = M[a⊢c>b]{c:=(x).P}"
    using fs2 by (metis crename_cfresh' fresh_prod substc_rename1)
  have eq2: "([(c',c)]M)[a⊢c>b] = ([(c',c)](M[a⊢c>b]))" using fs2 assms
    by (simp add: crename_coname_eqvt fresh_atm(2) fresh_prod swap_simps(6))
  have "M{c:=(x).P}[a⊢c>b] = ([(c',c)]M){c':=(x).P}[a⊢c>b]" using eq by simp
  also have " = ([(c',c)]M)[a⊢c>b]{c':=(x).P[a⊢c>b]}"
    using fs2 assms
    by (metis crename_fresh eq eq' eq2 substc_crename_comm)
  also have " = ([(c',c)](M[a⊢c>b])){c':=(x).P[a⊢c>b]}" using eq2 by simp
  also have " = ([(c',c)](M[a⊢c>b])){c':=(x).P}" 
    using assms by (simp add: rename_fresh)
  also have " = M[a⊢c>b]{c:=(x).P}" using eq' by simp
  finally show ?thesis by simp
qed

lemma substn_nrename_comm':
  assumes "xy" "xz" "yP"
  shows "M{x:=<c>.P}[y⊢n>z] = M[y⊢n>z]{x:=<c>.P}"
proof -
  obtain x'::"name" where fs2: "x'(x,M,y,z)" by (rule exists_fresh(1), rule fin_supp, blast)
  have eq: "M{x:=<c>.P} = ([(x',x)]M){x':=<c>.P}"
    using fs2 by (simp add: substn_rename3)
   have eq': "([(x',x)](M[y⊢n>z])){x':=<c>.P} = M[y⊢n>z]{x:=<c>.P}"
    using fs2 by (metis fresh_prod nrename_nfresh' substn_rename3)
  have eq2: "([(x',x)]M)[y⊢n>z] = ([(x',x)](M[y⊢n>z]))" 
    using fs2 by (simp add: assms fresh_atm(1) fresh_prod nrename_name_eqvt swap_simps(5)) 
  have "M{x:=<c>.P}[y⊢n>z] = ([(x',x)]M){x':=<c>.P}[y⊢n>z]" using eq by simp
  also have " = ([(x',x)]M)[y⊢n>z]{x':=<c>.P[y⊢n>z]}"
    using fs2 by (metis assms eq eq' eq2 nrename_fresh substn_nrename_comm)
  also have " = ([(x',x)](M[y⊢n>z])){x':=<c>.P[y⊢n>z]}" using eq2 by simp
  also have " = ([(x',x)](M[y⊢n>z])){x':=<c>.P}" using assms by (simp add: rename_fresh)
  also have " = M[y⊢n>z]{x:=<c>.P}" using eq' by simp
  finally show ?thesis by simp
qed

lemma substc_nrename_comm':
  assumes "xy" "yP"
  shows "M{c:=(x).P}[y⊢n>z] = M[y⊢n>z]{c:=(x).P}"
proof -
  obtain x'::"name" where fs2: "x'(x,P,y,z)" by (rule exists_fresh(1), rule fin_supp, blast)
  have eq: "M{c:=(x).P} = M{c:=(x').([(x',x)]P)}"
    using fs2
    using substc_rename2 by auto
   have eq': "M[y⊢n>z]{c:=(x).P} = M[y⊢n>z]{c:=(x').([(x',x)]P)}"
    using fs2 by (simp add: substc_rename2)
  have eq2: "([(x',x)]P)[y⊢n>z] = ([(x',x)]P)"
    using fs2 by (metis assms(2) fresh_atm(1) fresh_aux(1) fresh_prod nrename_fresh)
  have "M{c:=(x).P}[y⊢n>z] = M{c:=(x').([(x',x)]P)}[y⊢n>z]" using eq by simp
  also have " = M[y⊢n>z]{c:=(x').(([(x',x)]P)[y⊢n>z])}"
    using fs2 by (simp add: fresh_atm(1) fresh_prod substc_nrename_comm)
  also have " = M[y⊢n>z]{c:=(x').(([(x',x)]P))}" using eq2 by simp
  also have " = M[y⊢n>z]{c:=(x).P}" using eq' by simp 
  finally show ?thesis by simp
qed

lemmas subst_comm = substn_crename_comm substc_crename_comm
                    substn_nrename_comm substc_nrename_comm
lemmas subst_comm' = substn_crename_comm' substc_crename_comm'
                     substn_nrename_comm' substc_nrename_comm'

text ‹typing contexts›

type_synonym ctxtn = "(name×ty) list"
type_synonym ctxtc = "(coname×ty) list"

inductive
  validc :: "ctxtc  bool"
where
  vc1[intro]: "validc []"
| vc2[intro]: "aΔ; validc Δ  validc ((a,T)#Δ)"

equivariance validc

inductive
  validn :: "ctxtn  bool"
where
  vn1[intro]: "validn []"
| vn2[intro]: "xΓ; validn Γ  validn ((x,T)#Γ)"

equivariance validn

lemma fresh_ctxt:
  fixes a::"coname"
  and   x::"name"
  and   Γ::"ctxtn"
  and   Δ::"ctxtc"
  shows "aΓ" and "xΔ"
proof -
  show "aΓ" by (induct Γ) (auto simp: fresh_list_nil fresh_list_cons fresh_prod fresh_atm fresh_ty)
next
  show "xΔ" by (induct Δ) (auto simp: fresh_list_nil fresh_list_cons fresh_prod fresh_atm fresh_ty)
qed

text ‹cut-reductions›

declare abs_perm[eqvt]

inductive
  fin :: "trm  name  bool"
where
  [intro]: "fin (Ax x a) x"
| [intro]: "xM  fin (NotL <a>.M x) x"
| [intro]: "y[x].M  fin (AndL1 (x).M y) y"
| [intro]: "y[x].M  fin (AndL2 (x).M y) y"
| [intro]: "z[x].M;z[y].N  fin (OrL (x).M (y).N z) z"
| [intro]: "yM;y[x].N  fin (ImpL <a>.M (x).N y) y"

equivariance fin

lemma fin_Ax_elim:
  assumes "fin (Ax x a) y"
  shows "x=y"
  using assms fin.simps trm.inject(1) by auto

lemma fin_NotL_elim:
  assumes a: "fin (NotL <a>.M x) y"
  shows "x=y  xM"
  using assms 
  by (cases rule: fin.cases; simp add: trm.inject; metis abs_fresh(5))

lemma fin_AndL1_elim:
  assumes a: "fin (AndL1 (x).M y) z"
  shows "z=y  z[x].M"
  using assms by (cases rule: fin.cases; simp add: trm.inject)

lemma fin_AndL2_elim:
  assumes a: "fin (AndL2 (x).M y) z"
  shows "z=y  z[x].M"
  using assms by (cases rule: fin.cases; simp add: trm.inject)

lemma fin_OrL_elim:
  assumes a: "fin (OrL (x).M (y).N u) z"
  shows "z=u  z[x].M  z[y].N"
  using assms by (cases rule: fin.cases; simp add: trm.inject)

lemma fin_ImpL_elim:
  assumes a: "fin (ImpL <a>.M (x).N z) y"
  shows "z=y  zM  z[x].N"
  using assms
  by (cases rule: fin.cases; simp add: trm.inject; metis abs_fresh(5))
 

lemma fin_rest_elims:
  shows "fin (Cut <a>.M (x).N) y  False"
  and   "fin (NotR (x).M c) y  False"
  and   "fin (AndR <a>.M <b>.N c) y  False"
  and   "fin (OrR1 <a>.M b) y  False"
  and   "fin (OrR2 <a>.M b) y  False"
  and   "fin (ImpR (x).<a>.M b) y  False"
by (erule fin.cases, simp_all add: trm.inject)+

lemmas fin_elims = fin_Ax_elim fin_NotL_elim fin_AndL1_elim fin_AndL2_elim fin_OrL_elim 
                   fin_ImpL_elim fin_rest_elims

lemma fin_rename:
  shows "fin M x  fin ([(x',x)]M) x'"
by (induct rule: fin.induct)
   (auto simp: calc_atm simp add: fresh_left abs_fresh)

lemma not_fin_subst1:
  assumes "¬(fin M x)" 
  shows "¬(fin (M{c:=(y).P}) x)"
using assms 
proof (nominal_induct M avoiding: x c y P rule: trm.strong_induct)
  case (Ax name coname)
  then show ?case 
    using fin_rest_elims(1) substc.simps(1) by presburger
next
  case (Cut coname trm1 name trm2)
  then show ?case
    using fin_rest_elims(1) substc.simps(1) by simp presburger
next
  case (NotR name trm coname)
  obtain a'::coname where "a'(trm{coname:=(y).P},P,x)"
    by (meson exists_fresh(2) fs_coname1)
  with NotR show ?case
    apply (simp add: fresh_prod trm.inject)
    using fresh_fun_simp_NotR fin_rest_elims by fastforce
next
  case (NotL coname trm name)
  then show ?case 
    using fin_NotL_elim freshn_after_substc by simp blast
next
  case (AndR coname1 trm1 coname2 trm2 coname3)
  obtain a'::coname where "a'(trm1{coname3:=(y).P},trm2{coname3:=(y).P},P,coname1,coname2,coname3,x)"
    by (meson exists_fresh(2) fs_coname1)
  with AndR show ?case
    apply (simp add: fresh_prod trm.inject)
    using fresh_fun_simp_AndR fin_rest_elims by fastforce
next
  case (AndL1 name1 trm name2)
  then show ?case 
    using fin_AndL1_elim freshn_after_substc
    by simp (metis abs_fresh(1) fin.intros(3))
next
  case (AndL2 name1 trm name2)
  then show ?case 
    using fin_AndL2_elim freshn_after_substc
    by simp (metis abs_fresh(1) fin.intros(4))
next
  case (OrR1 coname1 trm coname2)
  obtain a'::coname where "a'(trm{coname2:=(y).P},coname1,P,x)"
    by (meson exists_fresh(2) fs_coname1)
  with OrR1 show ?case
    apply (simp add: fresh_prod trm.inject)
    using fresh_fun_simp_OrR1 fin_rest_elims by fastforce
next
  case (OrR2 coname1 trm coname2)
  obtain a'::coname where "a'(trm{coname2:=(y).P},coname1,P,x)"
    by (meson exists_fresh(2) fs_coname1)
  with OrR2 show ?case
    apply (simp add: fresh_prod trm.inject)
    using fresh_fun_simp_OrR2 fin_rest_elims by fastforce
next
  case (OrL name1 trm1 name2 trm2 name3)
  then show ?case
    by simp (metis abs_fresh(1) fin.intros(5) fin_OrL_elim freshn_after_substc)
next
  case (ImpR name coname1 trm coname2)
  obtain a'::coname where "a'(trm{coname2:=(y).P},coname1,P,x)"
    by (meson exists_fresh(2) fs_coname1)
  with ImpR show ?case
    apply (simp add: fresh_prod trm.inject)
    using fresh_fun_simp_ImpR fin_rest_elims by fastforce
next
  case (ImpL coname trm1 name1 trm2 name2)
  then show ?case
    by simp (metis abs_fresh(1) fin.intros(6) fin_ImpL_elim freshn_after_substc)
qed



lemma not_fin_subst2:
  assumes "¬(fin M x)" 
  shows "¬(fin (M{y:=<c>.P}) x)"
using assms 
proof (nominal_induct M avoiding: x c y P rule: trm.strong_induct)
  case (Ax name coname)
  then show ?case
    using fin_rest_elims(1) substn.simps(1) by presburger
next
  case (Cut coname trm1 name trm2)
  then show ?case
    using fin_rest_elims(1) substc.simps(1) by simp presburger
next
  case (NotR name trm coname)
  with fin_rest_elims show ?case
    by (fastforce simp add: fresh_prod trm.inject)
next
  case (NotL coname trm name)
  obtain a'::name where "a'(trm{y:=<c>.P},P,x)"
    by (meson exists_fresh(1) fs_name1)
  with NotL show ?case 
    apply (clarsimp simp: fresh_prod fresh_fun_simp_NotL trm.inject)
    by (metis fin.intros(2) fin_NotL_elim fin_rest_elims(1) freshn_after_substn)
next
  case (AndR coname1 trm1 coname2 trm2 coname3)
  obtain a'::name where "a'(trm1{coname3:=(y).P},trm2{coname3:=(y).P},P,coname1,coname2,coname3,x)"
    by (meson exists_fresh(1) fs_name1)
  with AndR fin_rest_elims show ?case
    by (fastforce simp add: fresh_prod trm.inject)
next
  case (AndL1 name1 trm name2)
  obtain a'::name where "a'(trm{y:=<c>.P},P,name1,x)"
    by (meson exists_fresh(1) fs_name1)
  with AndL1 show ?case 
    apply (clarsimp simp: fresh_prod fresh_fun_simp_AndL1 trm.inject)
    by (metis abs_fresh(1) fin.intros(3) fin_AndL1_elim fin_rest_elims(1) freshn_after_substn)
next
  case (AndL2 name1 trm name2)
  obtain a'::name where "a'(trm{y:=<c>.P},P,name1,x)"
    by (meson exists_fresh(1) fs_name1)
  with AndL2 show ?case 
    apply (clarsimp simp: fresh_prod fresh_fun_simp_AndL2 trm.inject)
    by (metis abs_fresh(1) fin.intros(4) fin_AndL2_elim fin_rest_elims(1) freshn_after_substn)
next
  case (OrR1 coname1 trm coname2)
  then show ?case
    using fin_rest_elims by (fastforce simp: fresh_prod trm.inject)
next
  case (OrR2 coname1 trm coname2)
  then show ?case
    using fin_rest_elims by (fastforce simp: fresh_prod trm.inject)
next
  case (OrL name1 trm1 name2 trm2 name3)
  obtain a'::name where "a'(trm1{y:=<c>.P},trm2{y:=<c>.P},name1,name2,P,x)"
    by (meson exists_fresh(1) fs_name1)
  with OrL show ?case  
    apply (simp add: fresh_prod trm.inject)
    by (metis (full_types) abs_fresh(1) fin.intros(5) fin_OrL_elim fin_rest_elims(1) fresh_fun_simp_OrL freshn_after_substn)
next
  case (ImpR name coname1 trm coname2)
  with fin_rest_elims show ?case
    by (fastforce simp add: fresh_prod trm.inject)
next
  case (ImpL coname trm1 name1 trm2 name2)
  obtain a'::name where "a'(trm1{name2:=<c>.P},trm2{name2:=<c>.P},name1,P,x)"
    by (meson exists_fresh(1) fs_name1)
  with ImpL show ?case
    apply (simp add: fresh_prod trm.inject)
    by (metis abs_fresh(1) fin.intros(6) fin_ImpL_elim fin_rest_elims(1) fresh_fun_simp_ImpL freshn_after_substn)
qed


lemma fin_subst1:
  assumes "fin M x" "xy" "xP"
  shows "fin (M{y:=<c>.P}) x"
  using assms
proof (nominal_induct M avoiding: x y c P rule: trm.strong_induct)
  case (AndL1 name1 trm name2)
  then show ?case
    apply (clarsimp simp add: subst_fresh abs_fresh dest!: fin_AndL1_elim)
    by (metis abs_fresh(1) fin.intros(3) fresh_prod subst_fresh(3))
next
  case (AndL2 name1 trm name2)
  then show ?case
    apply (clarsimp simp add: subst_fresh abs_fresh dest!: fin_AndL2_elim)
    by (metis abs_fresh(1) fin.intros(4) fresh_prod subst_fresh(3))
next
  case (OrR1 coname1 trm coname2)
  then show ?case
    by (auto simp add: subst_fresh abs_fresh dest!: fin_rest_elims)
next
  case (OrR2 coname1 trm coname2)
  then show ?case
    by (auto simp add: subst_fresh abs_fresh dest!: fin_rest_elims)
next
  case (OrL name1 trm1 name2 trm2 name3)
  then show ?case
    apply (clarsimp simp add: subst_fresh abs_fresh)
    by (metis abs_fresh(1) fin.intros(5) fin_OrL_elim fresh_prod subst_fresh(3))
next
  case (ImpR name coname1 trm coname2)
  then show ?case
    by (auto simp add: subst_fresh abs_fresh dest!: fin_rest_elims)
next
  case (ImpL coname trm1 name1 trm2 name2)
  then show ?case
    apply (clarsimp simp add: subst_fresh abs_fresh)
    by (metis abs_fresh(1) fin.intros(6) fin_ImpL_elim fresh_prod subst_fresh(3))
qed (auto dest!: fin_elims simp add: subst_fresh abs_fresh)


thm abs_fresh fresh_prod

lemma fin_subst2:
  assumes "fin M y" "xy" "yP" "MAx y c" 
  shows "fin (M{c:=(x).P}) y"
using assms
proof (nominal_induct M avoiding: x y c P rule: trm.strong_induct)
  case (Ax name coname)
  then show ?case
    using fin_Ax_elim by force
next
  case (NotL coname trm name)
  then show ?case
    by simp (metis fin.intros(2) fin_NotL_elim fresh_prod subst_fresh(5)) 
next
  case (AndL1 name1 trm name2)
  then show ?case 
    by simp (metis abs_fresh(1) fin.intros(3) fin_AndL1_elim fresh_prod subst_fresh(5))
next
  case (AndL2 name1 trm name2)
  then show ?case 
    by simp (metis abs_fresh(1) fin.intros(4) fin_AndL2_elim fresh_prod subst_fresh(5)) 
next
  case (OrL name1 trm1 name2 trm2 name3)
  then show ?case
    by simp (metis abs_fresh(1) fin.intros(5) fin_OrL_elim fresh_prod subst_fresh(5))
next
  case (ImpL coname trm1 name1 trm2 name2)
  then show ?case
    by simp (metis abs_fresh(1) fin.intros(6) fin_ImpL_elim fresh_prod subst_fresh(5))
qed (use fin_rest_elims in force)+


lemma fin_substn_nrename:
  assumes "fin M x" "xy" "xP"
  shows "M[x⊢n>y]{y:=<c>.P} = Cut <c>.P (x).(M{y:=<c>.P})"
using assms [[simproc del: defined_all]]
proof (nominal_induct M avoiding: x y c P rule: trm.strong_induct)
  case (Ax name coname)
  then show ?case
    by (metis fin_Ax_elim fresh_atm(1,3) fresh_prod nrename_swap subst_rename(3) substn.simps(1) trm.fresh(1))
next
  case (NotL coname trm name)
  obtain z::name where "z  (trm,y,x,P,trm[x⊢n>y]{y:=<c>.P})"
    by (meson exists_fresh(1) fs_name1)
  with NotL show ?case 
    apply (clarsimp simp add: fresh_prod fresh_fun_simp_NotL trm.inject alpha fresh_atm calc_atm abs_fresh)
    by (metis fin_NotL_elim nrename_fresh nrename_swap substn_nrename_comm')
next
  case (AndL1 name1 trm name2)
  obtain z::name where "z  (name2,name1,P,trm[name2⊢n>y]{y:=<c>.P},y,P,trm)"
    by (meson exists_fresh(1) fs_name1)
  with AndL1 show ?case 
    using fin_AndL1_elim[OF AndL1.prems(1)]
    by simp (metis abs_fresh(1) fresh_atm(1) fresh_fun_simp_AndL1 fresh_prod nrename_fresh subst_fresh(3))
next
  case (AndL2 name1 trm name2)
  obtain z::name where "z  (name2,name1,P,trm[name2⊢n>y]{y:=<c>.P},y,P,trm)"
    by (meson exists_fresh(1) fs_name1)
  with AndL2 show ?case 
    using fin_AndL2_elim[OF AndL2.prems(1)]
    by simp (metis abs_fresh(1) fresh_atm(1) fresh_fun_simp_AndL2 fresh_prod nrename_fresh subst_fresh(3))
next
  case (OrL name1 trm1 name2 trm2 name3)
  obtain z::name where "z  (name3,name2,name1,P,trm1[name3⊢n>y]{y:=<c>.P},trm2[name3⊢n>y]{y:=<c>.P},y,P,trm1,trm2)"
    by (meson exists_fresh(1) fs_name1)
  with OrL show ?case 
    using fin_OrL_elim[OF OrL.prems(1)]
    by (auto simp add: abs_fresh fresh_fun_simp_OrL fresh_atm(1) nrename_fresh subst_fresh(3))
next
  case (ImpL coname trm1 name1 trm2 name2)
  obtain z::name where "z  (name1,x,P,trm1[x⊢n>y]{y:=<c>.P},trm2[x⊢n>y]{y:=<c>.P},y,P,trm1,trm2)"
    by (meson exists_fresh(1) fs_name1)
  with ImpL show ?case 
    using fin_ImpL_elim[OF ImpL.prems(1)]
    by (auto simp add: abs_fresh fresh_fun_simp_ImpL fresh_atm(1) nrename_fresh subst_fresh(3))
qed (use fin_rest_elims in force)+

inductive
  fic :: "trm  coname  bool"
where
  [intro]: "fic (Ax x a) a"
| [intro]: "aM  fic (NotR (x).M a) a"
| [intro]: "c[a].M;c[b].N  fic (AndR <a>.M <b>.N c) c"
| [intro]: "b[a].M  fic (OrR1 <a>.M b) b"
| [intro]: "b[a].M  fic (OrR2 <a>.M b) b"
| [intro]: "b[a].M  fic (ImpR (x).<a>.M b) b"

equivariance fic

lemma fic_Ax_elim:
  assumes "fic (Ax x a) b"
  shows "a=b"
  using assms by (auto simp: trm.inject elim!: fic.cases)

lemma fic_NotR_elim:
  assumes "fic (NotR (x).M a) b"
  shows "a=b  bM"
  using assms
  by (auto simp: trm.inject elim!: fic.cases) (metis abs_fresh(6))

lemma fic_OrR1_elim:
  assumes "fic (OrR1 <a>.M b) c"
  shows "b=c  c[a].M"
  using assms by (auto simp: trm.inject elim!: fic.cases)

lemma fic_OrR2_elim:
  assumes "fic (OrR2 <a>.M b) c"
  shows "b=c  c[a].M"
  using assms by (auto simp: trm.inject elim!: fic.cases)

lemma fic_AndR_elim:
  assumes "fic (AndR <a>.M <b>.N c) d"
  shows "c=d  d[a].M  d[b].N"
  using assms by (auto simp: trm.inject elim!: fic.cases)

lemma fic_ImpR_elim:
  assumes a: "fic (ImpR (x).<a>.M b) c"
  shows "b=c  b[a].M"
  using assms by (auto simp: trm.inject elim!: fic.cases) (metis abs_fresh(6))

lemma fic_rest_elims:
  shows "fic (Cut <a>.M (x).N) d  False"
  and   "fic (NotL <a>.M x) d  False"
  and   "fic (OrL (x).M (y).N z) d  False"
  and   "fic (AndL1 (x).M y) d  False"
  and   "fic (AndL2 (x).M y) d  False"
  and   "fic (ImpL <a>.M (x).N y) d  False"
by (erule fic.cases, simp_all add: trm.inject)+

lemmas fic_elims = fic_Ax_elim fic_NotR_elim fic_OrR1_elim fic_OrR2_elim fic_AndR_elim 
                   fic_ImpR_elim fic_rest_elims

lemma fic_rename:
  shows "fic M a  fic ([(a',a)]M) a'"
by (induct rule: fic.induct)
   (auto simp: calc_atm simp add: fresh_left abs_fresh)

lemma not_fic_subst1:
  assumes "¬(fic M a)" 
  shows "¬(fic (M{y:=<c>.P}) a)"
using assms
proof (nominal_induct M avoiding: a c y P rule: trm.strong_induct)
  case (Ax name coname)
  then show ?case
    using fic_rest_elims(1) substn.simps(1) by presburger
next
  case (Cut coname trm1 name trm2)
  then show ?case
    by (metis abs_fresh(2) better_Cut_substn fic_rest_elims(1) fresh_prod)
next
  case (NotR name trm coname)
  then show ?case
    by (metis fic.intros(2) fic_NotR_elim fresh_prod freshc_after_substn substn.simps(3))
next
  case (NotL coname trm name)
  obtain x'::name where "x'  (trm{y:=<c>.P},P,a)"
    by (meson exists_fresh(1) fs_name1)
  with NotL show ?case
    by (simp add: fic.intros fresh_prod) (metis fic_rest_elims(1,2) fresh_fun_simp_NotL)
next
  case (AndR coname1 trm1 coname2 trm2 coname3)
  then show ?case
    by simp (metis abs_fresh(2) fic.intros(3) fic_AndR_elim freshc_after_substn)
next
  case (AndL1 name1 trm name2)
  obtain x'::name where "x'  (trm{y:=<c>.P},P,name1,a)"
    by (meson exists_fresh(1) fs_name1)
  with AndL1 fic_rest_elims show ?case
    by (simp add: fic.intros fresh_prod)(metis fresh_fun_simp_AndL1)
next
  case (AndL2 name1 trm name2)
  obtain x'::name where "x'  (trm{y:=<c>.P},P,name1,a)"
    by (meson exists_fresh(1) fs_name1)
  with AndL2 fic_rest_elims show ?case
    by (simp add: fic.intros fresh_prod) (metis fresh_fun_simp_AndL2)
next
  case (OrR1 coname1 trm coname2)
  then show ?case
    by simp (metis abs_fresh(2) fic.simps fic_OrR1_elim freshc_after_substn)
next
  case (OrR2 coname1 trm coname2)
  then show ?case
    by simp (metis abs_fresh(2) fic.simps fic_OrR2_elim freshc_after_substn)
next
  case (OrL name1 trm1 name2 trm2 name3)
  obtain x'::name where "x'  (trm1{y:=<c>.P},trm2{y:=<c>.P},P,name1,name2,a)"
    by (meson exists_fresh(1) fs_name1)
  with OrL fic_rest_elims show ?case
    by (simp add: fic.intros fresh_prod) (metis fresh_fun_simp_OrL)
next
  case (ImpR name coname1 trm coname2)
  then show ?case 
    by simp (metis abs_fresh(2) fic.intros(6) fic_ImpR_elim freshc_after_substn)
next
  case (ImpL coname trm1 name1 trm2 name2)
  obtain x'::name where "x'  (trm1{name2:=<c>.P},trm2{name2:=<c>.P},P,name1,name2,a)"
    by (meson exists_fresh(1) fs_name1)
  with ImpL fic_rest_elims fresh_fun_simp_ImpL show ?case
    by (simp add: fresh_prod) fastforce
qed

lemma not_fic_subst2:
  assumes "¬(fic M a)" 
  shows "¬(fic (M{c:=(y).P}) a)"
using assms
proof (nominal_induct M avoiding: a c y P rule: trm.strong_induct)
  case (NotR name trm coname)
  obtain c'::coname where "c'(trm{coname:=(y).P},P,a)"
    by (meson exists_fresh'(2) fs_coname1)
  with NotR fic_rest_elims show ?case
    apply (clarsimp simp: fresh_prod fresh_fun_simp_NotR)
    by (metis fic.intros(2) fic_NotR_elim freshc_after_substc)
next
  case (AndR coname1 trm1 coname2 trm2 coname3)
  obtain c'::coname where "c'(trm1{coname3:=(y).P},trm2{coname3:=(y).P},P,coname1,coname2,a)"
    by (meson exists_fresh'(2) fs_coname1)
  with AndR fic_rest_elims show ?case
    apply (clarsimp simp: fresh_prod fresh_fun_simp_AndR)
    by (metis abs_fresh(2) fic.intros(3) fic_AndR_elim freshc_after_substc)
next
  case (OrR1 coname1 trm coname2)
  obtain c'::coname where "c'(trm{coname2:=(y).P},P,coname1,a)"
    by (meson exists_fresh'(2) fs_coname1)
  with OrR1 fic_rest_elims show ?case
    apply (clarsimp simp: fresh_prod fresh_fun_simp_OrR1)
    by (metis abs_fresh(2) fic.intros(4) fic_OrR1_elim freshc_after_substc)
next
  case (OrR2 coname1 trm coname2)
  obtain c'::coname where "c'(trm{coname2:=(y).P},P,coname1,a)"
    by (meson exists_fresh'(2) fs_coname1)
  with OrR2 fic_rest_elims show ?case
    apply (clarsimp simp: fresh_prod fresh_fun_simp_OrR2)
    by (metis abs_fresh(2) fic.simps fic_OrR2_elim freshc_after_substc)
next
  case (ImpR name coname1 trm coname2)
  obtain c'::coname where "c'(trm{coname2:=(y).P},P,coname1,a)"
    by (meson exists_fresh'(2) fs_coname1)
  with ImpR fic_rest_elims show ?case
    apply (clarsimp simp: fresh_prod fresh_fun_simp_ImpR)
    by (metis abs_fresh(2) fic.intros(6) fic_ImpR_elim freshc_after_substc)
qed (use fic_rest_elims in auto)

lemma fic_subst1:
  assumes "fic M a" "ab" "aP"
  shows "fic (M{b:=(x).P}) a"
using assms
proof (nominal_induct M avoiding: x b a P rule: trm.strong_induct)
  case (Ax name coname)
  then show ?case
    using fic_Ax_elim by force
next
  case (NotR name trm coname)
  with fic_NotR_elim show ?case
    by (fastforce simp add: fresh_prod subst_fresh)
next
  case (AndR coname1 trm1 coname2 trm2 coname3)
  with fic_AndR_elim show ?case
    by (fastforce simp add: abs_fresh fresh_prod subst_fresh)
next
  case (OrR1 coname1 trm coname2)
  with fic_OrR1_elim show ?case
    by (fastforce simp add: abs_fresh fresh_prod subst_fresh)
next
  case (OrR2 coname1 trm coname2)
  with fic_OrR2_elim show ?case
    by (fastforce simp add: abs_fresh fresh_prod subst_fresh)
next
  case (ImpR name coname1 trm coname2)
  with fic_ImpR_elim show ?case
    by (fastforce simp add: abs_fresh fresh_prod subst_fresh)
qed (use fic_rest_elims in force)+

lemma fic_subst2:
  assumes "fic M a" "ca" "aP" "MAx x a" 
  shows "fic (M{x:=<c>.P}) a"
using assms
proof (nominal_induct M avoiding: x a c P rule: trm.strong_induct)
  case (Ax name coname)
  then show ?case
    using fic_Ax_elim by force
next
  case (NotR name trm coname)
  with fic_NotR_elim show ?case
    by (fastforce simp add: fresh_prod subst_fresh)
next
  case (AndR coname1 trm1 coname2 trm2 coname3)
  with fic_AndR_elim show ?case
    by simp (metis abs_fresh(2) crename_cfresh crename_fresh fic.intros(3) fresh_atm(2) substn_crename_comm')
next
  case (OrR1 coname1 trm coname2)
  with fic_OrR1_elim show ?case
    by (fastforce simp add: abs_fresh fresh_prod subst_fresh)
next
  case (OrR2 coname1 trm coname2)
  with fic_OrR2_elim show ?case
    by (fastforce simp add: abs_fresh fresh_prod subst_fresh)
next
  case (ImpR name coname1 trm coname2)
  with fic_ImpR_elim show ?case
    by (fastforce simp add: abs_fresh fresh_prod subst_fresh)
qed (use fic_rest_elims in force)+

lemma fic_substc_crename:
  assumes "fic M a" "ab" "aP"
  shows "M[a⊢c>b]{b:=(y).P} = Cut <a>.(M{b:=(y).P}) (y).P"
using assms
proof (nominal_induct M avoiding: a b  y P rule: trm.strong_induct)
  case (Ax name coname)
  with fic_Ax_elim show ?case
    by(force simp add: trm.inject alpha(2) fresh_atm(2,4) swap_simps(4,8))
next
  case (Cut coname trm1 name trm2)
  with fic_rest_elims show ?case by force
next
  case (NotR name trm coname)
  with fic_NotR_elim[OF NotR.prems(1)] show ?case
    by (simp add: trm.inject crename_fresh fresh_fun_simp_NotR subst_fresh(6))
next
  case (AndR coname1 trm1 coname2 trm2 coname3)
  with AndR fic_AndR_elim[OF AndR.prems(1)] show ?case
    by (simp add: abs_fresh rename_fresh fresh_fun_simp_AndR fresh_atm(2) subst_fresh(6))
next
  case (OrR1 coname1 trm coname2)
  with fic_OrR1_elim[OF OrR1.prems(1)] show ?case
    by (simp add: abs_fresh rename_fresh fresh_fun_simp_OrR1 fresh_atm(2) subst_fresh(6))
next
  case (OrR2 coname1 trm coname2)
  with fic_OrR2_elim[OF OrR2.prems(1)] show ?case
    by (simp add: abs_fresh rename_fresh fresh_fun_simp_OrR2 fresh_atm(2) subst_fresh(6))
next
  case (ImpR name coname1 trm coname2)
  with fic_ImpR_elim[OF ImpR.prems(1)] crename_fresh show ?case
    by (force simp add: abs_fresh fresh_fun_simp_ImpR fresh_atm(2) subst_fresh(6))
qed (use fic_rest_elims in force)+

inductive
  l_redu :: "trm  trm  bool" (‹_ l _› [100,100] 100)
where
  LAxR:  "xM; ab; fic M a  Cut <a>.M (x).(Ax x b) l M[a⊢c>b]"
| LAxL:  "aM; xy; fin M x  Cut <a>.(Ax y a) (x).M l M[x⊢n>y]"
| LNot:  "y(M,N); x(N,y); a(M,N,b); bM; yx; ba 
          Cut <a>.(NotR (x).M a) (y).(NotL <b>.N y) l Cut <b>.N (x).M" 
| LAnd1: "b([a1].M1,[a2].M2,N,a1,a2); y([x].N,M1,M2,x); x(M1,M2); a1(M2,N); a2(M1,N); a1a2 
          Cut <b>.(AndR <a1>.M1 <a2>.M2 b) (y).(AndL1 (x).N y) l Cut <a1>.M1 (x).N"
| LAnd2: "b([a1].M1,[a2].M2,N,a1,a2); y([x].N,M1,M2,x); x(M1,M2); a1(M2,N); a2(M1,N); a1a2 
          Cut <b>.(AndR <a1>.M1 <a2>.M2 b) (y).(AndL2 (x).N y) l Cut <a2>.M2 (x).N"
| LOr1:  "b([a].M,N1,N2,a); y([x1].N1,[x2].N2,M,x1,x2); x1(M,N2); x2(M,N1); a(N1,N2); x1x2 
          Cut <b>.(OrR1 <a>.M b) (y).(OrL (x1).N1 (x2).N2 y) l Cut <a>.M (x1).N1"
| LOr2:  "b([a].M,N1,N2,a); y([x1].N1,[x2].N2,M,x1,x2); x1(M,N2); x2(M,N1); a(N1,N2); x1x2 
          Cut <b>.(OrR2 <a>.M b) (y).(OrL (x1).N1 (x2).N2 y) l Cut <a>.M (x2).N2"
| LImp:  "z(N,[y].P,[x].M,y,x); b([a].M,[c].N,P,c,a); x(N,[y].P,y); 
          c(P,[a].M,b,a); a([c].N,P); y(N,[x].M) 
          Cut <b>.(ImpR (x).<a>.M b) (z).(ImpL <c>.N (y).P z) l Cut <a>.(Cut <c>.N (x).M) (y).P"

equivariance l_redu

lemma l_redu_eqvt':
  fixes pi1::"name prm"
  and   pi2::"coname prm"
  shows "(pi1M) l (pi1M')  M l M'"
  and   "(pi2M) l (pi2M')  M l M'"
  using l_redu.eqvt perm_pi_simp by metis+

nominal_inductive l_redu
  by (force simp add: abs_fresh fresh_atm rename_fresh fresh_prod abs_supp fin_supp)+


lemma fresh_l_redu_x:
  fixes z::"name"
  shows "M l M'  zM  zM'"
proof (induct rule: l_redu.induct)
  case (LAxL a M x y)
  then show ?case
    by (metis abs_fresh(1,5) nrename_nfresh nrename_rename trm.fresh(1,3))
next
  case (LImp z N y P x M b a c)
  then show ?case
    apply (simp add: abs_fresh fresh_prod)
    by (metis abs_fresh(3,5) abs_supp(5) fs_name1)
qed (auto simp add: abs_fresh fresh_prod crename_nfresh)

lemma fresh_l_redu_a:
  fixes c::"coname"
  shows "M l M'  cM  cM'"
proof (induct rule: l_redu.induct)
  case (LAxR x M a b)
  then show ?case
    apply (simp add: abs_fresh)
    by (metis crename_cfresh crename_rename)
next
  case (LAxL a M x y)
  with nrename_cfresh show ?case
    by (simp add: abs_fresh)
qed (auto simp add: abs_fresh fresh_prod crename_nfresh)


lemmas fresh_l_redu = fresh_l_redu_x fresh_l_redu_a

lemma better_LAxR_intro[intro]:
  shows "fic M a  Cut <a>.M (x).(Ax x b) l M[a⊢c>b]"
proof -
  assume fin: "fic M a"
  obtain x'::"name" where fs1: "x'(M,x)" by (rule exists_fresh(1), rule fin_supp, blast)
  obtain a'::"coname" where fs2: "a'(a,M,b)" by (rule exists_fresh(2), rule fin_supp, blast)
  have "Cut <a>.M (x).(Ax x b) =  Cut <a'>.([(a',a)]M) (x').(Ax x' b)"
    using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
  also have " l ([(a',a)]M)[a'⊢c>b]" using fs1 fs2 fin
    by (auto intro: l_redu.intros simp add: fresh_left calc_atm fic_rename)
  also have " = M[a⊢c>b]" using fs1 fs2 by (simp add: crename_rename)
  finally show ?thesis by simp
qed
    
lemma better_LAxL_intro[intro]:
  shows "fin M x  Cut <a>.(Ax y a) (x).M l M[x⊢n>y]"
proof -
  assume fin: "fin M x"
  obtain x'::"name" where fs1: "x'(y,M,x)" by (rule exists_fresh(1), rule fin_supp, blast)
  obtain a'::"coname" where fs2: "a'(a,M)" by (rule exists_fresh(2), rule fin_supp, blast)
  have "Cut <a>.(Ax y a) (x).M = Cut <a'>.(Ax y a') (x').([(x',x)]M)"
    using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
  also have " l ([(x',x)]M)[x'⊢n>y]" using fs1 fs2 fin
    by (auto intro: l_redu.intros simp add: fresh_left calc_atm fin_rename)
  also have " = M[x⊢n>y]" using fs1 fs2 by (simp add: nrename_rename)
  finally show ?thesis by simp
qed

lemma better_LNot_intro[intro]:
  shows "yN; aM  Cut <a>.(NotR (x).M a) (y).(NotL <b>.N y) l Cut <b>.N (x).M"
proof -
  assume fs: "yN" "aM"
  obtain x'::"name" where f1: "x'(y,N,M,x)" by (rule exists_fresh(1), rule fin_supp, blast)
  obtain y'::"name" where f2: "y'(y,N,M,x,x')" by (rule exists_fresh(1), rule fin_supp, blast)
  obtain a'::"coname" where f3: "a'(a,M,N,b)" by (rule exists_fresh(2), rule fin_supp, blast)
  obtain b'::"coname" where f4: "b'(a,M,N,b,a')" by (rule exists_fresh(2), rule fin_supp, blast)
  have "Cut <a>.(NotR (x).M a) (y).(NotL <b>.N y) 
                      = Cut <a'>.(NotR (x).([(a',a)]M) a') (y').(NotL <b>.([(y',y)]N) y')"
    using f1 f2 f3 f4 
    by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm abs_fresh)
  also have " = Cut <a'>.(NotR (x).M a') (y').(NotL <b>.N y')"
    using f1 f2 f3 f4 fs by (perm_simp)
  also have " = Cut <a'>.(NotR (x').([(x',x)]M) a') (y').(NotL <b'>.([(b',b)]N) y')"
    using f1 f2 f3 f4 
    by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
  also have " l Cut <b'>.([(b',b)]N) (x').([(x',x)]M)"
    using f1 f2 f3 f4 fs
    by (auto intro:  l_redu.intros simp add: fresh_prod fresh_left calc_atm fresh_atm)
  also have " = Cut <b>.N (x).M"
    using f1 f2 f3 f4 by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
  finally show ?thesis by simp
qed 

lemma better_LAnd1_intro[intro]:
  shows "a([b1].M1,[b2].M2); y[x].N 
          Cut <a>.(AndR <b1>.M1 <b2>.M2 a) (y).(AndL1 (x).N y) l Cut <b1>.M1 (x).N"
proof -
  assume fs: "a([b1].M1,[b2].M2)" "y[x].N"
  obtain x'::"name" where f1: "x'(y,N,M1,M2,x)" by (rule exists_fresh(1), rule fin_supp, blast)
  obtain y'::"name" where f2: "y'(y,N,M1,M2,x,x')" by (rule exists_fresh(1), rule fin_supp, blast)
  obtain a'::"coname" where f3: "a'(a,M1,M2,N,b1,b2)" by (rule exists_fresh(2), rule fin_supp, blast)
  obtain b1'::"coname" where f4:"b1'(a,M1,M2,N,b1,b2,a')" by (rule exists_fresh(2), rule fin_supp, blast)
  obtain b2'::"coname" where f5:"b2'(a,M1,M2,N,b1,b2,a',b1')" by (rule exists_fresh(2),rule fin_supp, blast)
  have "Cut <a>.(AndR <b1>.M1 <b2>.M2 a) (y).(AndL1 (x).N y)
                      = Cut <a'>.(AndR <b1>.M1 <b2>.M2 a') (y').(AndL1 (x).N y')"
    using f1 f2 f3 f4 fs
    apply(rule_tac sym)
    apply(perm_simp add: trm.inject alpha calc_atm fresh_prod fresh_left fresh_atm abs_fresh)
    apply(auto simp: perm_fresh_fresh)
    done
  also have " = Cut <a'>.(AndR <b1'>.([(b1',b1)]M1) <b2'>.([(b2',b2)]M2) a') 
                                                               (y').(AndL1 (x').([(x',x)]N) y')"
    using f1 f2 f3 f4 f5 fs 
    apply(rule_tac sym)
    apply(perm_simp add: trm.inject alpha calc_atm fresh_prod fresh_left fresh_atm abs_fresh)
    done
  also have " l Cut <b1'>.([(b1',b1)]M1) (x').([(x',x)]N)"
    using f1 f2 f3 f4 f5 fs
    apply -
    apply(rule l_redu.intros)
    apply(auto simp: abs_fresh fresh_prod fresh_left calc_atm fresh_atm)
    done
  also have " = Cut <b1>.M1 (x).N"
    using f1 f2 f3 f4 f5 fs by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
  finally show ?thesis by simp
qed 

lemma better_LAnd2_intro[intro]:
  shows "a([b1].M1,[b2].M2); y[x].N 
          Cut <a>.(AndR <b1>.M1 <b2>.M2 a) (y).(AndL2 (x).N y) l Cut <b2>.M2 (x).N"
proof -
  assume fs: "a([b1].M1,[b2].M2)" "y[x].N"
  obtain x'::"name" where f1: "x'(y,N,M1,M2,x)" by (rule exists_fresh(1), rule fin_supp, blast)
  obtain y'::"name" where f2: "y'(y,N,M1,M2,x,x')" by (rule exists_fresh(1), rule fin_supp, blast)
  obtain a'::"coname" where f3: "a'(a,M1,M2,N,b1,b2)" by (rule exists_fresh(2), rule fin_supp, blast)
  obtain b1'::"coname" where f4:"b1'(a,M1,M2,N,b1,b2,a')" by (rule exists_fresh(2), rule fin_supp, blast)
  obtain b2'::"coname" where f5:"b2'(a,M1,M2,N,b1,b2,a',b1')" by (rule exists_fresh(2),rule fin_supp, blast)
  have "Cut <a>.(AndR <b1>.M1 <b2>.M2 a) (y).(AndL2 (x).N y)
                      = Cut <a'>.(AndR <b1>.M1 <b2>.M2 a') (y').(AndL2 (x).N y')"
    using f1 f2 f3 f4 fs
    apply(rule_tac sym)
    apply(perm_simp add: trm.inject alpha calc_atm fresh_prod fresh_left fresh_atm abs_fresh)
    apply(auto simp: perm_fresh_fresh)
    done
  also have " = Cut <a'>.(AndR <b1'>.([(b1',b1)]M1) <b2'>.([(b2',b2)]M2) a') 
                                                               (y').(AndL2 (x').([(x',x)]N) y')"
    using f1 f2 f3 f4 f5 fs 
    apply(rule_tac sym)
    apply(perm_simp add: trm.inject alpha calc_atm fresh_prod fresh_left fresh_atm abs_fresh)
    done
  also have " l Cut <b2'>.([(b2',b2)]M2) (x').([(x',x)]N)"
    using f1 f2 f3 f4 f5 fs
    apply -
    apply(rule l_redu.intros)
    apply(auto simp: abs_fresh fresh_prod fresh_left calc_atm fresh_atm)
    done
  also have " = Cut <b2>.M2 (x).N"
    using f1 f2 f3 f4 f5 fs by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
  finally show ?thesis by simp
qed

lemma better_LOr1_intro[intro]:
  shows "y([x1].N1,[x2].N2); b[a].M 
          Cut <b>.(OrR1 <a>.M b) (y).(OrL (x1).N1 (x2).N2 y) l Cut <a>.M (x1).N1"
proof -
  assume fs: "y([x1].N1,[x2].N2)" "b[a].M"
  obtain y'::"name" where f1: "y'(y,M,N1,N2,x1,x2)" by (rule exists_fresh(1), rule fin_supp, blast)
  obtain x1'::"name" where f2: "x1'(y,M,N1,N2,x1,x2,y')" by (rule exists_fresh(1), rule fin_supp, blast)
  obtain x2'::"name" where f3: "x2'(y,M,N1,N2,x1,x2,y',x1')" by (rule exists_fresh(1), rule fin_supp, blast)
  obtain a'::"coname" where f4: "a'(a,N1,N2,M,b)" by (rule exists_fresh(2), rule fin_supp, blast)
  obtain b'::"coname" where f5: "b'(a,N1,N2,M,b,a')" by (rule exists_fresh(2),rule fin_supp, blast)
  have "Cut <b>.(OrR1 <a>.M b) (y).(OrL (x1).N1 (x2).N2 y)
                      = Cut <b'>.(OrR1 <a>.M b') (y').(OrL (x1).N1 (x2).N2 y')"
    using f1 f2 f3 f4 f5 fs
    apply(rule_tac sym)
    apply(perm_simp add: trm.inject alpha calc_atm fresh_prod fresh_left fresh_atm abs_fresh)
    apply(auto simp: perm_fresh_fresh)
    done
  also have " = Cut <b'>.(OrR1 <a'>.([(a',a)]M) b') 
              (y').(OrL (x1').([(x1',x1)]N1) (x2').([(x2',x2)]N2) y')"   
    using f1 f2 f3 f4 f5 fs 
    apply(rule_tac sym)
    apply(perm_simp add: trm.inject alpha calc_atm fresh_prod fresh_left fresh_atm abs_fresh)
    done
  also have " l Cut <a'>.([(a',a)]M) (x1').([(x1',x1)]N1)"
    using f1 f2 f3 f4 f5 fs
    apply -
    apply(rule l_redu.intros)
    apply(auto simp: abs_fresh fresh_prod fresh_left calc_atm fresh_atm)
    done
  also have " = Cut <a>.M (x1).N1"
    using f1 f2 f3 f4 f5 fs by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
  finally show ?thesis by simp
qed

lemma better_LOr2_intro[intro]:
  shows "y([x1].N1,[x2].N2); b[a].M 
          Cut <b>.(OrR2 <a>.M b) (y).(OrL (x1).N1 (x2).N2 y) l Cut <a>.M (x2).N2"
proof -
  assume fs: "y([x1].N1,[x2].N2)" "b[a].M"
  obtain y'::"name" where f1: "y'(y,M,N1,N2,x1,x2)" by (rule exists_fresh(1), rule fin_supp, blast)
  obtain x1'::"name" where f2: "x1'(y,M,N1,N2,x1,x2,y')" by (rule exists_fresh(1), rule fin_supp, blast)
  obtain x2'::"name" where f3: "x2'(y,M,N1,N2,x1,x2,y',x1')" by (rule exists_fresh(1), rule fin_supp, blast)
  obtain a'::"coname" where f4: "a'(a,N1,N2,M,b)" by (rule exists_fresh(2), rule fin_supp, blast)
  obtain b'::"coname" where f5: "b'(a,N1,N2,M,b,a')" by (rule exists_fresh(2),rule fin_supp, blast)
  have "Cut <b>.(OrR2 <a>.M b) (y).(OrL (x1).N1 (x2).N2 y)
                      = Cut <b'>.(OrR2 <a>.M b') (y').(OrL (x1).N1 (x2).N2 y')"
    using f1 f2 f3 f4 f5 fs
    apply(rule_tac sym)
    apply(perm_simp add: trm.inject alpha calc_atm fresh_prod fresh_left fresh_atm abs_fresh)
    apply(auto simp: perm_fresh_fresh)
    done
  also have " = Cut <b'>.(OrR2 <a'>.([(a',a)]M) b') 
              (y').(OrL (x1').([(x1',x1)]N1) (x2').([(x2',x2)]N2) y')"   
    using f1 f2 f3 f4 f5 fs 
    apply(rule_tac sym)
    apply(perm_simp add: trm.inject alpha calc_atm fresh_prod fresh_left fresh_atm abs_fresh)
    done
  also have " l Cut <a'>.([(a',a)]M) (x2').([(x2',x2)]N2)"
    using f1 f2 f3 f4 f5 fs
    apply -
    apply(rule l_redu.intros)
    apply(auto simp: abs_fresh fresh_prod fresh_left calc_atm fresh_atm)
    done
  also have " = Cut <a>.M (x2).N2"
    using f1 f2 f3 f4 f5 fs by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
  finally show ?thesis by simp
qed 

lemma better_LImp_intro[intro]:
  shows "z(N,[y].P); b[a].M; aN 
          Cut <b>.(ImpR (x).<a>.M b) (z).(ImpL <c>.N (y).P z) l Cut <a>.(Cut <c>.N (x).M) (y).P"
proof -
  assume fs: "z(N,[y].P)" "b[a].M" "aN"
  obtain y'::"name" and x'::"name" and z'::"name" 
    where f1: "y'(y,M,N,P,z,x)" and f2: "x'(y,M,N,P,z,x,y')" and f3: "z'(y,M,N,P,z,x,y',x')"
    by (meson exists_fresh(1) fs_name1)
  obtain a'::"coname" and b'::"coname" and c'::"coname" 
    where f4: "a'(a,N,P,M,b)" and f5: "b'(a,N,P,M,b,c,a')" and f6: "c'(a,N,P,M,b,c,a',b')"
    by (meson exists_fresh(2) fs_coname1)
  have "Cut <b>.(ImpR (x).<a>.M b) (z).(ImpL <c>.N (y).P z)
                      =  Cut <b'>.(ImpR (x).<a>.M b') (z').(ImpL <c>.N (y).P z')"
    using f1 f2 f3 f4 f5 fs
    apply(rule_tac sym)
    apply(perm_simp add: trm.inject alpha calc_atm fresh_prod fresh_left fresh_atm abs_fresh)
    apply(auto simp: perm_fresh_fresh)
    done
  also have " = Cut <b'>.(ImpR (x').<a'>.([(a',a)]([(x',x)]M)) b') 
                           (z').(ImpL <c'>.([(c',c)]N) (y').([(y',y)]P) z')"
    using f1 f2 f3 f4 f5 f6 fs 
    apply(rule_tac sym)
    apply(simp add: trm.inject alpha fresh_prod fresh_atm abs_perm calc_atm fresh_left abs_fresh)
    done
  also have " l Cut <a'>.(Cut <c'>.([(c',c)]N) (x').([(a',a)][(x',x)]M)) (y').([(y',y)]P)"
    using f1 f2 f3 f4 f5 f6 fs
    apply -
    apply(rule l_redu.intros)
    apply(auto simp: abs_fresh fresh_prod fresh_left calc_atm fresh_atm)
    done
  also have " = Cut <a>.(Cut <c>.N (x).M) (y).P"
    using f1 f2 f3 f4 f5 f6 fs 
    apply(simp add: trm.inject)
    apply(perm_simp add: alpha fresh_prod fresh_atm)
    apply(simp add: trm.inject abs_fresh alpha(1) fresh_perm_app(4) perm_compose(4) perm_dj(4))
    apply (metis alpha'(2) crename_fresh crename_swap swap_simps(2,4,6))
    done
  finally show ?thesis by simp
qed 

lemma alpha_coname:
  fixes M::"trm"
    and   a::"coname"
  assumes "[a].M = [b].N" "c(a,b,M,N)"
  shows "M = [(a,c)][(b,c)]N"
  by (metis alpha_fresh'(2) assms fresh_atm(2) fresh_prod)

lemma alpha_name:
  fixes M::"trm"
    and   x::"name"
  assumes "[x].M = [y].N" "z(x,y,M,N)"
  shows "M = [(x,z)][(y,z)]N"
  by (metis alpha_fresh'(1) assms fresh_atm(1) fresh_prod)

lemma alpha_name_coname:
  fixes M::"trm"
  and   x::"name"
  and   a::"coname"
assumes "[x].[b].M = [y].[c].N" "z(x,y,M,N)" "a(b,c,M,N)"
  shows "M = [(x,z)][(b,a)][(c,a)][(y,z)]N"
  using assms
  apply(clarsimp simp: alpha_fresh fresh_prod fresh_atm 
      abs_supp fin_supp abs_fresh abs_perm fresh_left calc_atm)
  by (metis perm_swap(1,2))


lemma Cut_l_redu_elim:
  assumes "Cut <a>.M (x).N l R"
  shows "(b. R = M[a⊢c>b])  (y. R = N[x⊢n>y]) 
  (y M' b N'. M = NotR (y).M' a  N = NotL <b>.N' x  R = Cut <b>.N' (y).M'  fic M a  fin N x) 
  (b M1 c M2 y N'. M = AndR <b>.M1 <c>.M2 a  N = AndL1 (y).N' x  R = Cut <b>.M1 (y).N' 
                                                                             fic M a  fin N x) 
  (b M1 c M2 y N'. M = AndR <b>.M1 <c>.M2 a  N = AndL2 (y).N' x  R = Cut <c>.M2 (y).N' 
                                                                             fic M a  fin N x) 
  (b N' z M1 y M2. M = OrR1 <b>.N' a  N = OrL (z).M1 (y).M2 x  R = Cut <b>.N' (z).M1 
                                                                             fic M a  fin N x) 
  (b N' z M1 y M2. M = OrR2 <b>.N' a  N = OrL (z).M1 (y).M2 x  R = Cut <b>.N' (y).M2 
                                                                             fic M a  fin N x) 
  (z b M' c N1 y N2. M = ImpR (z).<b>.M' a  N = ImpL <c>.N1 (y).N2 x  
            R = Cut <b>.(Cut <c>.N1 (z).M') (y).N2  b(c,N1)  fic M a  fin N x)"
using assms
proof (cases rule: l_redu.cases)
  case (LAxR x M a b)
  then show ?thesis
    apply(simp add: trm.inject)
    by (metis alpha(2) crename_rename)
next
  case (LAxL a M x y)
  then show ?thesis
    apply(simp add: trm.inject)
    by (metis alpha(1) nrename_rename)
next
  case (LNot y M N x a b)
  then show ?thesis
    apply(simp add: trm.inject)
    apply(rule disjI2)
    apply(rule disjI2)
    apply(rule disjI1)
    apply(erule conjE)+
    apply(generate_fresh "coname")
    apply(simp add: abs_fresh fresh_prod fresh_atm)
    apply(auto)[1]
    apply(drule_tac c="c" in  alpha_coname)
     apply(simp add: fresh_prod fresh_atm abs_fresh)
    apply(simp add: calc_atm)
    apply(rule exI)+
    apply(rule conjI)
     apply(rule refl)
    apply(generate_fresh "name")
    apply(simp add: calc_atm abs_fresh fresh_prod fresh_atm fresh_left)
    apply(auto)[1]
    apply(drule_tac z="ca" in  alpha_name)
     apply(simp add: fresh_prod fresh_atm abs_fresh)
    apply(simp add: calc_atm)
    apply(rule exI)+
    apply(rule conjI)
     apply(rule refl)
    apply(auto simp: calc_atm abs_fresh fresh_left)[1]
    using nrename_fresh nrename_swap apply presburger
    using crename_fresh crename_swap by presburger
next
  case (LAnd1 b a1 M1 a2 M2 N y x)
  then show ?thesis
    apply -
    apply(rule disjI2)
    apply(rule disjI2)
    apply(rule disjI2)
    apply(rule disjI1)
    apply(clarsimp simp add: trm.inject)
    apply(generate_fresh "coname")
    apply(clarsimp simp add: abs_fresh fresh_prod fresh_atm)
    apply(drule_tac c="c" in  alpha_coname)
     apply(simp add: fresh_prod fresh_atm abs_fresh)
    apply(simp)
    apply(rule exI)+
    apply(rule conjI)
     apply(rule exI)+
     apply(rule_tac s="a" and t="[(a,c)][(b,c)]b" in subst)
      apply(simp add: calc_atm)
     apply(rule refl)
    apply(generate_fresh "name")
    apply(simp add: abs_fresh fresh_prod fresh_atm)
    apply(auto)[1]
       apply(drule_tac z="ca" in  alpha_name)
        apply(simp add: fresh_prod fresh_atm abs_fresh)
       apply(simp)
       apply (metis swap_simps(6))
      apply(generate_fresh "name")
      apply(simp add: abs_fresh fresh_prod fresh_atm)
      apply(auto)[1]
      apply(drule_tac z="cb" in  alpha_name)
       apply(simp add: fresh_prod fresh_atm abs_fresh)
      apply(simp)
      apply(perm_simp)
      apply (smt (verit, del_insts) abs_fresh(1,2) abs_perm(1,2) fic.intros(3) fin.intros(3) fresh_bij(1) perm_fresh_fresh(1,2) swap_simps(1,6))
     apply(perm_simp)+
     apply(generate_fresh "name")
     apply(simp add: abs_fresh fresh_prod fresh_atm)
     apply(auto)[1]
     apply(drule_tac z="cb" in  alpha_name)
      apply(simp add: fresh_prod fresh_atm abs_fresh)
     apply(perm_simp)
     apply (smt (verit) abs_fresh(1,2) abs_perm(1,2) fic.intros(3) fin.intros(3) perm_fresh_fresh(1,2) perm_swap(3) swap_simps(1,6))
    apply(perm_simp)+
    apply(generate_fresh "name")
    apply(simp add: abs_fresh fresh_prod fresh_atm)
    apply(auto)[1]
    apply(drule_tac z="cb" in  alpha_name)
     apply(simp add: fresh_prod fresh_atm abs_fresh cong: conj_cong)
    apply(perm_simp)
    by (smt (verit, best) abs_fresh(1,2) abs_perm(1) alpha(2) fic.intros(3) fin.intros(3) fresh_bij(1,2) perm_fresh_fresh(1,2) swap_simps(2,3))
next
  case (LAnd2 b a1 M1 a2 M2 N y x)
  then show ?thesis
    apply -
    apply(rule disjI2)
    apply(rule disjI2)
    apply(rule disjI2)
    apply(rule disjI2)
    apply(rule disjI1)
    apply(clarsimp simp add: trm.inject)
    apply(generate_fresh "coname")
    apply(clarsimp simp add: abs_fresh fresh_prod fresh_atm)
    apply(drule_tac c="c" in  alpha_coname)
     apply(simp add: fresh_prod fresh_atm abs_fresh)
    apply(simp)
    apply(rule exI)+
    apply(rule conjI)
     apply(rule_tac s="a" and t="[(a,c)][(b,c)]b" in subst)
      apply(simp add: calc_atm)
     apply(rule refl)
    apply(generate_fresh "name")
    apply(auto simp add: abs_fresh fresh_prod fresh_atm)
       apply(drule_tac z="ca" in  alpha_name)
        apply(simp add: fresh_prod fresh_atm abs_fresh)
       apply (metis swap_simps(6))
      apply(generate_fresh "name")
      apply(simp add: abs_fresh fresh_prod fresh_atm)
      apply(auto)[1]
      apply(drule_tac z="cb" in  alpha_name)
       apply(simp add: fresh_prod fresh_atm abs_fresh)
      apply(perm_simp)
      apply (smt (verit, ccfv_threshold) abs_fresh(1,2) abs_perm(1) fic.intros(3) fin.intros(4) fresh_bij(1,2) perm_fresh_fresh(1,2) swap_simps(1,4,6))
     apply(generate_fresh "name")
     apply(simp add: abs_fresh fresh_prod fresh_atm)
     apply(auto)[1]
     apply(drule_tac z="cb" in  alpha_name)
      apply(simp add: fresh_prod fresh_atm abs_fresh)
     apply(simp)
     apply(perm_simp)
     apply (smt (verit) abs_fresh(1,2) abs_perm(1,2) fic.intros(3) fin.intros(4) fresh_bij(1) perm_fresh_fresh(1,2) swap_simps(1,6))
    apply(generate_fresh "name")
    apply(clarsimp simp add: abs_fresh fresh_prod fresh_atm)
    apply(drule_tac z="cb" in  alpha_name)
     apply(simp add: fresh_prod fresh_atm abs_fresh)
    apply(perm_simp)
    by (smt (verit, ccfv_SIG) abs_fresh(1,2) abs_perm(1) alpha(2) fic.intros(3) fin.intros(4) fresh_bij(1,2) perm_fresh_fresh(1,2) swap_simps(2,3))
next
  case (LOr1 b a M N1 N2 y x1 x2)
  then show ?thesis
    apply -
    apply(rule disjI2)
    apply(rule disjI2)
    apply(rule disjI2)
    apply(rule disjI2)
    apply(rule disjI2)
    apply(rule disjI1)
    apply(clarsimp simp add: trm.inject)
    apply(generate_fresh "coname")
    apply(simp add: abs_fresh fresh_prod fresh_atm)
    apply(auto)[1]
    apply(drule_tac c="c" in  alpha_coname)
     apply(simp add: fresh_prod fresh_atm abs_fresh)
    apply(simp)
    apply(perm_simp)
    apply(rule exI)+
    apply(rule conjI)
     apply(rule_tac s="a" and t="[(a,c)][(b,c)]b" in subst)
      apply(simp add: calc_atm)
     apply(rule refl)
    apply(generate_fresh "name")
    apply(simp add: abs_fresh fresh_prod fresh_atm)
    apply(auto)[1]
     apply(drule_tac z="ca" in  alpha_name)
      apply(simp add: fresh_prod fresh_atm abs_fresh)
     apply(simp)
     apply(rule exI)+
     apply(rule conjI)
      apply(rule exI)+
      apply(rule_tac s="x" and t="[(x,ca)][(y,ca)]y" in subst)
       apply(simp add: calc_atm)
      apply(rule refl)
     apply(auto simp: fresh_left calc_atm abs_fresh alpha perm_fresh_fresh split: if_splits)[1]
        apply(perm_simp)+
    apply(generate_fresh "name")
    apply(simp add: abs_fresh fresh_prod fresh_atm)
    apply(auto)[1]
    apply(drule_tac z="cb" in  alpha_name)
     apply(simp add: fresh_prod fresh_atm abs_fresh)
    apply(simp)
    apply(rule exI)+
    apply(rule conjI)
     apply(rule exI)+
     apply(rule_tac s="x" and t="[(x,cb)][(y,cb)]y" in subst)
      apply(simp add: calc_atm)
     apply(rule refl)
    apply(auto simp: fresh_left calc_atm abs_fresh alpha perm_fresh_fresh split: if_splits)[1]
     apply(perm_simp)+
    done
next
  case (LOr2 b a M N1 N2 y x1 x2)
  then show ?thesis
    apply -
    apply(rule disjI2)
    apply(rule disjI2)
    apply(rule disjI2)
    apply(rule disjI2)
    apply(rule disjI2)
    apply(rule disjI2)
    apply(rule disjI1)
    apply(simp add: trm.inject)
    apply(erule conjE)+
    apply(generate_fresh "coname")
    apply(simp add: abs_fresh fresh_prod fresh_atm)
    apply(auto)[1]
    apply(drule_tac c="c" in  alpha_coname)
     apply(simp add: fresh_prod fresh_atm abs_fresh)
    apply(simp)
     apply(perm_simp)
    apply(rule exI)+
    apply(rule conjI)
     apply(rule_tac s="a" and t="[(a,c)][(b,c)]b" in subst)
      apply(simp add: calc_atm)
     apply(rule refl)
     apply(generate_fresh "name")
     apply(simp add: abs_fresh fresh_prod fresh_atm)
     apply(auto)[1]
      apply(drule_tac z="ca" in  alpha_name)
       apply(simp add: fresh_prod fresh_atm abs_fresh)
      apply(simp)
      apply(rule exI)+
      apply(rule conjI)
      apply(rule_tac s="x" and t="[(x,ca)][(y,ca)]y" in subst)
       apply(simp add: calc_atm)
      apply(rule refl)
      apply(auto simp: fresh_left calc_atm abs_fresh alpha perm_fresh_fresh split: if_splits)[1]
     apply(perm_simp)+
     apply(generate_fresh "name")
     apply(simp add: abs_fresh fresh_prod fresh_atm)
     apply(auto)[1]
     apply(drule_tac z="cb" in  alpha_name)
      apply(simp add: fresh_prod fresh_atm abs_fresh)
     apply(simp)
     apply(rule exI)+
     apply(rule conjI)
     apply(rule_tac s="x" and t="[(x,cb)][(y,cb)]y" in subst)
      apply(simp add: calc_atm)
     apply(rule refl)
     apply(auto simp: fresh_left calc_atm abs_fresh alpha perm_fresh_fresh split: if_splits)[1]
       apply(perm_simp)+
    done
next
  case (LImp z N y P x M b a c)
  then show ?thesis
    apply(intro disjI2)
    apply(clarsimp simp add: trm.inject)
    apply(generate_fresh "coname")
    apply(clarsimp simp add: abs_fresh fresh_prod fresh_atm)
    apply(drule_tac c="ca" in  alpha_coname)
     apply(simp add: fresh_prod fresh_atm abs_fresh)
    apply(simp)
    apply(perm_simp)
    apply(rule exI)+
    apply(rule conjI)
     apply(rule_tac s="a" and t="[(a,ca)][(b,ca)]b" in subst)
      apply(simp add: calc_atm)
     apply(rule refl)
    apply(generate_fresh "name")
    apply(simp add: abs_fresh fresh_prod fresh_atm)
    apply(auto)[1]
     apply(drule_tac z="caa" in  alpha_name)
      apply(simp add: fresh_prod fresh_atm abs_fresh)
     apply(simp)
     apply(perm_simp)
     apply(rule exI)+
     apply(rule conjI)
      apply(rule_tac s="x" and t="[(x,caa)][(z,caa)]z" in subst)
       apply(simp add: calc_atm)
      apply(rule refl)
     apply(auto simp: fresh_left calc_atm abs_fresh alpha perm_fresh_fresh split: if_splits)[1]
       apply(perm_simp)+
    apply(generate_fresh "name")
    apply(simp add: abs_fresh fresh_prod fresh_atm)
    apply(auto)[1]
    apply(drule_tac z="cb" in  alpha_name)
     apply(simp add: fresh_prod fresh_atm abs_fresh)
    apply(simp)
    apply(perm_simp)
    apply(rule exI)+
    apply(rule conjI)
     apply(rule_tac s="x" and t="[(x,cb)][(z,cb)]z" in subst)
      apply(simp add: calc_atm)
     apply(rule refl)
    apply(auto simp: fresh_left calc_atm abs_fresh alpha perm_fresh_fresh split: if_splits)[1]
     apply(perm_simp)+
    done
qed


inductive
  c_redu :: "trm  trm  bool" (‹_ c _› [100,100] 100)
where
  left[intro]:  "¬fic M a; aN; xM  Cut <a>.M (x).N c M{a:=(x).N}"
| right[intro]: "¬fin N x; aN; xM  Cut <a>.M (x).N c N{x:=<a>.M}"

equivariance c_redu

nominal_inductive c_redu
 by (simp_all add: abs_fresh subst_fresh)

lemma better_left[intro]:
  shows "¬fic M a  Cut <a>.M (x).N c M{a:=(x).N}"
proof -
  assume not_fic: "¬fic M a"
  obtain x'::"name" where fs1: "x'(N,M,x)" by (rule exists_fresh(1), rule fin_supp, blast)
  obtain a'::"coname" where fs2: "a'(a,M,N)" by (rule exists_fresh(2), rule fin_supp, blast)
  have "Cut <a>.M (x).N =  Cut <a'>.([(a',a)]M) (x').([(x',x)]N)"
    using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
  also have " c ([(a',a)]M){a':=(x').([(x',x)]N)}" using fs1 fs2 not_fic
    apply(intro left)
    apply (metis fic_rename perm_swap(4))
    apply(simp add: fresh_left calc_atm)+
    done
  also have " = M{a:=(x).N}" using fs1 fs2
    by (simp add: subst_rename[symmetric] fresh_atm fresh_prod fresh_left calc_atm)
  finally show ?thesis by simp
qed

lemma better_right[intro]:
  shows "¬fin N x  Cut <a>.M (x).N c N{x:=<a>.M}"
proof -
  assume not_fin: "¬fin N x"
  obtain x'::"name" where fs1: "x'(N,M,x)" by (rule exists_fresh(1), rule fin_supp, blast)
  obtain a'::"coname" where fs2: "a'(a,M,N)" by (rule exists_fresh(2), rule fin_supp, blast)
  have "Cut <a>.M (x).N =  Cut <a'>.([(a',a)]M) (x').([(x',x)]N)"
    using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
  also have " c ([(x',x)]N){x':=<a'>.([(a',a)]M)}" using fs1 fs2 not_fin
    apply (intro right)
    apply (metis fin_rename perm_swap(3))
    apply (simp add: fresh_left calc_atm)+
    done
  also have " = N{x:=<a>.M}" using fs1 fs2
    by (simp add: subst_rename[symmetric] fresh_atm fresh_prod fresh_left calc_atm)
  finally show ?thesis by simp
qed

lemma fresh_c_redu:
  fixes x::"name"
  and   c::"coname"
  shows "M c M'  xM  xM'"
  and   "M c M'  cM  cM'"
  by (induct rule: c_redu.induct) (auto simp: abs_fresh rename_fresh subst_fresh)+

inductive
  a_redu :: "trm  trm  bool" (‹_ a _› [100,100] 100)
where
  al_redu[intro]: "Ml M'  M a M'"
| ac_redu[intro]: "Mc M'  M a M'"
| a_Cut_l: "aN; xM; Ma M'  Cut <a>.M (x).N a Cut <a>.M' (x).N"
| a_Cut_r: "aN; xM; Na N'  Cut <a>.M (x).N a Cut <a>.M (x).N'"
| a_NotL[intro]: "Ma M'  NotL <a>.M x a NotL <a>.M' x"
| a_NotR[intro]: "Ma M'  NotR (x).M a a NotR (x).M' a"
| a_AndR_l: "a(N,c); b(M,c); ba; Ma M'  AndR <a>.M <b>.N c a AndR <a>.M' <b>.N c"
| a_AndR_r: "a(N,c); b(M,c); ba; Na N'  AndR <a>.M <b>.N c a AndR <a>.M <b>.N' c"
| a_AndL1: "xy; Ma M'  AndL1 (x).M y a AndL1 (x).M' y"
| a_AndL2: "xy; Ma M'  AndL2 (x).M y a AndL2 (x).M' y"
| a_OrL_l: "x(N,z); y(M,z); yx; Ma M'  OrL (x).M (y).N z a OrL (x).M' (y).N z"
| a_OrL_r: "x(N,z); y(M,z); yx; Na N'  OrL (x).M (y).N z a OrL (x).M (y).N' z"
| a_OrR1: "ab; Ma M'  OrR1 <a>.M b a OrR1 <a>.M' b"
| a_OrR2: "ab; Ma M'  OrR2 <a>.M b a OrR2 <a>.M' b"
| a_ImpL_l: "aN; x(M,y); Ma M'  ImpL <a>.M (x).N y a ImpL <a>.M' (x).N y"
| a_ImpL_r: "aN; x(M,y); Na N'  ImpL <a>.M (x).N y a ImpL <a>.M (x).N' y"
| a_ImpR: "ab; Ma M'  ImpR (x).<a>.M b a ImpR (x).<a>.M' b"

lemma fresh_a_redu1:
  fixes x::"name"
  shows "M a M'  xM  xM'"
  by (induct rule: a_redu.induct) (auto simp: fresh_l_redu fresh_c_redu abs_fresh abs_supp fin_supp)

lemma fresh_a_redu2:
  fixes c::"coname"
  shows "M a M'  cM  cM'"
  by (induct rule: a_redu.induct) (auto simp: fresh_l_redu fresh_c_redu abs_fresh abs_supp fin_supp)

lemmas fresh_a_redu = fresh_a_redu1 fresh_a_redu2

equivariance a_redu

nominal_inductive a_redu
  by (simp_all add: abs_fresh fresh_atm fresh_prod abs_supp fin_supp fresh_a_redu)

lemma better_CutL_intro[intro]:
  shows "Ma M'  Cut <a>.M (x).N a Cut <a>.M' (x).N"
proof -
  assume red: "Ma M'"
  obtain x'::"name"   where fs1: "x'(M,N,x)" by (rule exists_fresh(1), rule fin_supp, blast)
  obtain a'::"coname" where fs2: "a'(M,N,a)" by (rule exists_fresh(2), rule fin_supp, blast)
  have "Cut <a>.M (x).N =  Cut <a'>.([(a',a)]M) (x').([(x',x)]N)"
    using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
  also have " a  Cut <a'>.([(a',a)]M') (x').([(x',x)]N)" using fs1 fs2 red
    by (auto intro: a_redu.intros simp add: fresh_left calc_atm a_redu.eqvt)
  also have " = Cut <a>.M' (x).N" 
    using fs1 fs2 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu)
  finally show ?thesis by simp
qed

lemma better_CutR_intro[intro]:
  shows "Na N'  Cut <a>.M (x).N a Cut <a>.M (x).N'"
proof -
  assume red: "Na N'"
  obtain x'::"name"   where fs1: "x'(M,N,x)" by (rule exists_fresh(1), rule fin_supp, blast)
  obtain a'::"coname" where fs2: "a'(M,N,a)" by (rule exists_fresh(2), rule fin_supp, blast)
  have "Cut <a>.M (x).N =  Cut <a'>.([(a',a)]M) (x').([(x',x)]N)"
    using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
  also have " a  Cut <a'>.([(a',a)]M) (x').([(x',x)]N')" using fs1 fs2 red
    by (auto intro: a_redu.intros simp add: fresh_left calc_atm a_redu.eqvt)
  also have " = Cut <a>.M (x).N'" 
    using fs1 fs2 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu)
  finally show ?thesis by simp
qed
    
lemma better_AndRL_intro[intro]:
  shows "Ma M'  AndR <a>.M <b>.N c a AndR <a>.M' <b>.N c"
proof -
  assume red: "Ma M'"
  obtain b'::"coname" where fs1: "b'(M,N,a,b,c)" by (rule exists_fresh(2), rule fin_supp, blast)
  obtain a'::"coname" where fs2: "a'(M,N,a,b,c,b')" by (rule exists_fresh(2), rule fin_supp, blast)
  have "AndR <a>.M <b>.N c =  AndR <a'>.([(a',a)]M) <b'>.([(b',b)]N) c"
    using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
  also have " a  AndR <a'>.([(a',a)]M') <b'>.([(b',b)]N) c" using fs1 fs2 red
    by (auto intro: a_redu.intros simp add: fresh_left calc_atm a_redu.eqvt fresh_atm fresh_prod)
  also have " = AndR <a>.M' <b>.N c" 
    using fs1 fs2 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu)
  finally show ?thesis by simp
qed

lemma better_AndRR_intro[intro]:
  shows "Na N'  AndR <a>.M <b>.N c a AndR <a>.M <b>.N' c"
proof -
  assume red: "Na N'"
  obtain b'::"coname" where fs1: "b'(M,N,a,b,c)" by (rule exists_fresh(2), rule fin_supp, blast)
  obtain a'::"coname" where fs2: "a'(M,N,a,b,c,b')" by (rule exists_fresh(2), rule fin_supp, blast)
  have "AndR <a>.M <b>.N c =  AndR <a'>.([(a',a)]M) <b'>.([(b',b)]N) c"
    using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
  also have " a  AndR <a'>.([(a',a)]M) <b'>.([(b',b)]N') c" using fs1 fs2 red
    by (auto intro: a_redu.intros simp add: fresh_left calc_atm a_redu.eqvt fresh_atm fresh_prod)
  also have " = AndR <a>.M <b>.N' c" 
    using fs1 fs2 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu)
  finally show ?thesis by simp
qed

lemma better_AndL1_intro[intro]:
  shows "Ma M'  AndL1 (x).M y a AndL1 (x).M' y"
proof -
  assume red: "Ma M'"
  obtain x'::"name" where fs1: "x'(M,y,x)" by (rule exists_fresh(1), rule fin_supp, blast)
  have "AndL1 (x).M y = AndL1 (x').([(x',x)]M) y"
    using fs1 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
  also have " a AndL1 (x').([(x',x)]M') y" using fs1 red
    by (auto intro: a_redu.intros simp add: fresh_left calc_atm a_redu.eqvt fresh_atm fresh_prod)
  also have " = AndL1 (x).M' y" 
    using fs1 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu)
  finally show ?thesis by simp
qed

lemma better_AndL2_intro[intro]:
  shows "Ma M'  AndL2 (x).M y a AndL2 (x).M' y"
proof -
  assume red: "Ma M'"
  obtain x'::"name" where fs1: "x'(M,y,x)" by (rule exists_fresh(1), rule fin_supp, blast)
  have "AndL2 (x).M y = AndL2 (x').([(x',x)]M) y"
    using fs1 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
  also have " a AndL2 (x').([(x',x)]M') y" using fs1 red
    by (auto intro: a_redu.intros simp add: fresh_left calc_atm a_redu.eqvt fresh_atm fresh_prod)
  also have " = AndL2 (x).M' y" 
    using fs1 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu)
  finally show ?thesis by simp
qed

lemma better_OrLL_intro[intro]:
  shows "Ma M'  OrL (x).M (y).N z a OrL (x).M' (y).N z"
proof -
  assume red: "Ma M'"
  obtain x'::"name" where fs1: "x'(M,N,x,y,z)" by (rule exists_fresh(1), rule fin_supp, blast)
  obtain y'::"name" where fs2: "y'(M,N,x,y,z,x')" by (rule exists_fresh(1), rule fin_supp, blast)
  have "OrL (x).M (y).N z =  OrL (x').([(x',x)]M) (y').([(y',y)]N) z"
    using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
  also have " a OrL (x').([(x',x)]M') (y').([(y',y)]N) z" using fs1 fs2 red
    by (auto intro: a_redu.intros simp add: fresh_left calc_atm a_redu.eqvt fresh_atm fresh_prod)
  also have " = OrL (x).M' (y).N z" 
    using fs1 fs2 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu)
  finally show ?thesis by simp
qed

lemma better_OrLR_intro[intro]:
  shows "Na N'  OrL (x).M (y).N z a OrL (x).M (y).N' z"
proof -
  assume red: "Na N'"
  obtain x'::"name" where fs1: "x'(M,N,x,y,z)" by (rule exists_fresh(1), rule fin_supp, blast)
  obtain y'::"name" where fs2: "y'(M,N,x,y,z,x')" by (rule exists_fresh(1), rule fin_supp, blast)
  have "OrL (x).M (y).N z =  OrL (x').([(x',x)]M) (y').([(y',y)]N) z"
    using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
  also have " a OrL (x').([(x',x)]M) (y').([(y',y)]N') z" using fs1 fs2 red
    by (auto intro: a_redu.intros simp add: fresh_left calc_atm a_redu.eqvt fresh_atm fresh_prod)
  also have " = OrL (x).M (y).N' z" 
    using fs1 fs2 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu)
  finally show ?thesis by simp
qed

lemma better_OrR1_intro[intro]:
  shows "Ma M'  OrR1 <a>.M b a OrR1 <a>.M' b"
proof -
  assume red: "Ma M'"
  obtain a'::"coname" where fs1: "a'(M,b,a)" by (rule exists_fresh(2), rule fin_supp, blast)
  have "OrR1 <a>.M b = OrR1 <a'>.([(a',a)]M) b"
    using fs1 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
  also have " a OrR1 <a'>.([(a',a)]M') b" using fs1 red
    by (auto intro: a_redu.intros simp add: fresh_left calc_atm a_redu.eqvt fresh_atm fresh_prod)
  also have " = OrR1 <a>.M' b" 
    using fs1 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu)
  finally show ?thesis by simp
qed

lemma better_OrR2_intro[intro]:
  shows "Ma M'  OrR2 <a>.M b a OrR2 <a>.M' b"
proof -
  assume red: "Ma M'"
  obtain a'::"coname" where fs1: "a'(M,b,a)" by (rule exists_fresh(2), rule fin_supp, blast)
  have "OrR2 <a>.M b = OrR2 <a'>.([(a',a)]M) b"
    using fs1 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
  also have " a OrR2 <a'>.([(a',a)]M') b" using fs1 red
    by (auto intro: a_redu.intros simp add: fresh_left calc_atm a_redu.eqvt fresh_atm fresh_prod)
  also have " = OrR2 <a>.M' b" 
    using fs1 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu)
  finally show ?thesis by simp
qed

lemma better_ImpLL_intro[intro]:
  shows "Ma M'  ImpL <a>.M (x).N y a ImpL <a>.M' (x).N y"
proof -
  assume red: "Ma M'"
  obtain x'::"name"   where fs1: "x'(M,N,x,y)" by (rule exists_fresh(1), rule fin_supp, blast)
  obtain a'::"coname" where fs2: "a'(M,N,a)" by (rule exists_fresh(2), rule fin_supp, blast)
  have "ImpL <a>.M (x).N y =  ImpL <a'>.([(a',a)]M) (x').([(x',x)]N) y"
    using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
  also have " a  ImpL <a'>.([(a',a)]M') (x').([(x',x)]N) y" using fs1 fs2 red
    by (auto intro: a_redu.intros simp add: fresh_left calc_atm a_redu.eqvt fresh_atm fresh_prod)
  also have " = ImpL <a>.M' (x).N y" 
    using fs1 fs2 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu)
  finally show ?thesis by simp
qed

lemma better_ImpLR_intro[intro]:
  shows "Na N'  ImpL <a>.M (x).N y a ImpL <a>.M (x).N' y"
proof -
  assume red: "Na N'"
  obtain x'::"name"   where fs1: "x'(M,N,x,y)" by (rule exists_fresh(1), rule fin_supp, blast)
  obtain a'::"coname" where fs2: "a'(M,N,a)" by (rule exists_fresh(2), rule fin_supp, blast)
  have "ImpL <a>.M (x).N y =  ImpL <a'>.([(a',a)]M) (x').([(x',x)]N) y"
    using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
  also have " a  ImpL <a'>.([(a',a)]M) (x').([(x',x)]N') y" using fs1 fs2 red
    by (auto intro: a_redu.intros simp add: fresh_left calc_atm a_redu.eqvt fresh_atm fresh_prod)
  also have " = ImpL <a>.M (x).N' y" 
    using fs1 fs2 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu)
  finally show ?thesis by simp
qed

lemma better_ImpR_intro[intro]:
  shows "Ma M'  ImpR (x).<a>.M b a ImpR (x).<a>.M' b"
proof -
  assume red: "Ma M'"
  obtain a'::"coname" where fs2: "a'(M,a,b)" by (rule exists_fresh(2), rule fin_supp, blast)
  have "ImpR (x).<a>.M b = ImpR (x).<a'>.([(a',a)]M) b"
    using fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
  also have " a ImpR (x).<a'>.([(a',a)]M') b" using fs2 red
    by (auto intro: a_redu.intros simp add: fresh_left calc_atm a_redu.eqvt fresh_atm fresh_prod)
  also have " = ImpR (x).<a>.M' b" 
    using fs2 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu)
  finally show ?thesis by simp
qed

text ‹axioms do not reduce›

lemma ax_do_not_l_reduce:
  shows "Ax x a l M  False"
by (erule_tac l_redu.cases) (simp_all add: trm.inject)
 
lemma ax_do_not_c_reduce:
  shows "Ax x a c M  False"
by (erule_tac c_redu.cases) (simp_all add: trm.inject)

lemma ax_do_not_a_reduce:
  shows "Ax x a a M  False"
apply(erule_tac a_redu.cases) 
apply(simp_all add: trm.inject)
  using ax_do_not_l_reduce ax_do_not_c_reduce by blast+

lemma a_redu_NotL_elim:
  assumes "NotL <a>.M x a R"
  shows "M'. R = NotL <a>.M' x  MaM'"
  using assms
  apply(erule_tac a_redu.cases, simp_all add: trm.inject)
    apply(erule_tac l_redu.cases, simp_all add: trm.inject)
   apply(erule_tac c_redu.cases, simp_all add: trm.inject)
  apply (smt (verit, best) a_redu.eqvt(2) alpha(2) fresh_a_redu2)+
  done

lemma a_redu_NotR_elim:
  assumes "NotR (x).M a a R"
  shows "M'. R = NotR (x).M' a  MaM'"
  using assms
  apply(erule_tac a_redu.cases, simp_all add: trm.inject)
    apply(erule_tac l_redu.cases, simp_all add: trm.inject)
   apply(erule_tac c_redu.cases, simp_all add: trm.inject)
  apply (smt (verit, best) a_redu.eqvt(1) alpha(1) fresh_a_redu1)+
  done

lemma a_redu_AndR_elim:
  assumes "AndR <a>.M <b>.N ca R"
  shows "(M'. R = AndR <a>.M' <b>.N c  MaM')  (N'. R = AndR <a>.M <b>.N' c  NaN')"
  using assms
  apply(erule_tac a_redu.cases, simp_all add: trm.inject)
     apply(erule_tac l_redu.cases, simp_all add: trm.inject)
    apply(erule_tac c_redu.cases, simp_all add: trm.inject)
   apply (smt (verit) a_redu.eqvt(2) alpha'(2) fresh_a_redu2)
  by (metis a_NotL a_redu_NotL_elim trm.inject(4))

lemma a_redu_AndL1_elim:
  assumes "AndL1 (x).M y a R"
  shows "M'. R = AndL1 (x).M' y  MaM'"
  using assms
  apply(erule_tac a_redu.cases, simp_all add: trm.inject)
    apply(erule_tac l_redu.cases, simp_all add: trm.inject)
   apply(erule_tac c_redu.cases, simp_all add: trm.inject)
  by (metis a_NotR a_redu_NotR_elim trm.inject(3))

lemma a_redu_AndL2_elim:
  assumes a: "AndL2 (x).M y a R"
  shows "M'. R = AndL2 (x).M' y  MaM'"
  using a
  apply(erule_tac a_redu.cases, simp_all add: trm.inject)
  apply(erule_tac l_redu.cases, simp_all add: trm.inject)
   apply(erule_tac c_redu.cases, simp_all add: trm.inject)
  by (metis a_NotR a_redu_NotR_elim trm.inject(3))

lemma a_redu_OrL_elim:
  assumes "OrL (x).M (y).N za R"
  shows "(M'. R = OrL (x).M' (y).N z  MaM')  (N'. R = OrL (x).M (y).N' z  NaN')"
  using assms
  apply(erule_tac a_redu.cases, simp_all add: trm.inject)
     apply(erule_tac l_redu.cases, simp_all add: trm.inject)
    apply(erule_tac c_redu.cases, simp_all add: trm.inject)
   apply (metis a_NotR a_redu_NotR_elim trm.inject(3))+
done

lemma a_redu_OrR1_elim:
  assumes "OrR1 <a>.M b a R"
  shows "M'. R = OrR1 <a>.M' b  MaM'"
  using assms
  apply(erule_tac a_redu.cases, simp_all add: trm.inject)
    apply(erule_tac l_redu.cases, simp_all add: trm.inject)
   apply(erule_tac c_redu.cases, simp_all add: trm.inject)
  by (metis a_NotL a_redu_NotL_elim trm.inject(4))

lemma a_redu_OrR2_elim:
  assumes a: "OrR2 <a>.M b a R"
  shows "M'. R = OrR2 <a>.M' b  MaM'"
  using assms
  apply(erule_tac a_redu.cases, simp_all add: trm.inject)
    apply(erule_tac l_redu.cases, simp_all add: trm.inject)
   apply(erule_tac c_redu.cases, simp_all add: trm.inject)
  by (metis a_redu_OrR1_elim better_OrR1_intro trm.inject(8))

lemma a_redu_ImpL_elim:
  assumes a: "ImpL <a>.M (y).N za R"
  shows "(M'. R = ImpL <a>.M' (y).N z  MaM')  (N'. R = ImpL <a>.M (y).N' z  NaN')"
  using assms
  apply(erule_tac a_redu.cases, simp_all add: trm.inject)
     apply(erule_tac l_redu.cases, simp_all add: trm.inject)
    apply(erule_tac c_redu.cases, simp_all add: trm.inject)
   apply (smt (verit) a_redu.eqvt(2) alpha'(2) fresh_a_redu2)
  by (metis a_NotR a_redu_NotR_elim trm.inject(3))

lemma a_redu_ImpR_elim:
  assumes a: "ImpR (x).<a>.M b a R"
  shows "M'. R = ImpR (x).<a>.M' b  MaM'"
using a [[simproc del: defined_all]]
apply(erule_tac a_redu.cases, simp_all add: trm.inject)
apply(erule_tac l_redu.cases, simp_all add: trm.inject)
apply(erule_tac c_redu.cases, simp_all add: trm.inject)
apply(auto)
apply(rotate_tac 3)
apply(erule_tac a_redu.cases, simp_all add: trm.inject)
apply(erule_tac l_redu.cases, simp_all add: trm.inject)
  apply(erule_tac c_redu.cases, simp_all add: trm.inject)
apply(auto simp: alpha a_redu.eqvt abs_perm abs_fresh)
apply(rule_tac x="([(a,aa)]M'a)" in exI)
apply(auto simp: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu perm_swap)
apply(rule_tac x="([(a,aaa)]M'a)" in exI)
apply(auto simp: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu perm_swap)
apply(rule_tac x="([(a,aa)]M'a)" in exI)
apply(auto simp: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu perm_swap)
apply(rule_tac x="([(a,aaa)]M'a)" in exI)
apply(auto simp: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu perm_swap)
apply(rule_tac x="([(x,xa)]M'a)" in exI)
apply(auto simp: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu perm_swap)
apply(rule_tac x="([(x,xa)]M'a)" in exI)
apply(auto simp: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu perm_swap)
apply(rule_tac x="([(a,aa)][(x,xa)]M'a)" in exI)
apply(auto simp: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu perm_swap)
apply(rule sym)
apply(rule trans)
apply(rule perm_compose)
apply(simp add: calc_atm perm_swap)
apply(rule_tac x="([(a,aaa)][(x,xa)]M'a)" in exI)
apply(auto simp: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu perm_swap)
apply(rule sym)
apply(rule trans)
apply(rule perm_compose)
apply(simp add: calc_atm perm_swap)
apply(rule_tac x="([(x,xaa)]M'a)" in exI)
apply(auto simp: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu perm_swap)
apply(rule_tac x="([(x,xaa)]M'a)" in exI)
apply(auto simp: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu perm_swap)
apply(rule_tac x="([(a,aa)][(x,xaa)]M'a)" in exI)
apply(auto simp: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu perm_swap)
  apply (simp add: cp_coname_name1 perm_dj(4) perm_swap(3,4))
  apply(rule_tac x="([(a,aaa)][(x,xaa)]M'a)" in exI)
by(simp add: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu perm_swap perm_compose(4) perm_dj(4))

text ‹Transitive Closure›

abbreviation
 a_star_redu :: "trm  trm  bool" (‹_ a* _› [80,80] 80)
where
  "M a* M'  (a_redu)** M M'"

lemmas a_starI = r_into_rtranclp

lemma a_starE:
  assumes a: "M a* M'"
  shows "M = M'  (N. M a N  N a* M')"
  using a  by (induct) (auto)

lemma a_star_refl:
  shows "M a* M"
  by blast

declare rtranclp_trans [trans]

text ‹congruence rules for a*›

lemma ax_do_not_a_star_reduce:
  shows "Ax x a a* M  M = Ax x a"
  using a_starE ax_do_not_a_reduce by blast


lemma a_star_CutL:
    "M a* M'  Cut <a>.M (x).N a* Cut <a>.M' (x).N"
by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+

lemma a_star_CutR:
    "N a* N' Cut <a>.M (x).N a* Cut <a>.M (x).N'"
by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+

lemma a_star_Cut:
    "M a* M'; N a* N'  Cut <a>.M (x).N a* Cut <a>.M' (x).N'"
by (blast intro!: a_star_CutL a_star_CutR intro: rtranclp_trans)

lemma a_star_NotR:
    "M a* M'  NotR (x).M a a* NotR (x).M' a"
by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+

lemma a_star_NotL:
    "M a* M'  NotL <a>.M x a* NotL <a>.M' x"
by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+

lemma a_star_AndRL:
    "M a* M' AndR <a>.M <b>.N c a* AndR <a>.M' <b>.N c"
by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+

lemma a_star_AndRR:
    "N a* N' AndR <a>.M <b>.N c a* AndR <a>.M <b>.N' c"
by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+

lemma a_star_AndR:
    "M a* M'; N a* N'  AndR <a>.M <b>.N c a* AndR <a>.M' <b>.N' c"
by (blast intro!: a_star_AndRL a_star_AndRR intro: rtranclp_trans)

lemma a_star_AndL1:
    "M a* M'  AndL1 (x).M y a* AndL1 (x).M' y"
by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+

lemma a_star_AndL2:
    "M a* M'  AndL2 (x).M y a* AndL2 (x).M' y"
by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+

lemma a_star_OrLL:
    "M a* M' OrL (x).M (y).N z a* OrL (x).M' (y).N z"
by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+

lemma a_star_OrLR:
    "N a* N' OrL (x).M (y).N z a* OrL (x).M (y).N' z"
by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+

lemma a_star_OrL:
    "M a* M'; N a* N'  OrL (x).M (y).N z a* OrL (x).M' (y).N' z"
by (blast intro!: a_star_OrLL a_star_OrLR intro: rtranclp_trans)

lemma a_star_OrR1:
    "M a* M'  OrR1 <a>.M b a* OrR1 <a>.M' b"
by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+

lemma a_star_OrR2:
    "M a* M'  OrR2 <a>.M b a* OrR2 <a>.M' b"
by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+

lemma a_star_ImpLL:
    "M a* M' ImpL <a>.M (y).N z a* ImpL <a>.M' (y).N z"
by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+

lemma a_star_ImpLR:
    "N a* N' ImpL <a>.M (y).N z a* ImpL <a>.M (y).N' z"
by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+

lemma a_star_ImpL:
    "M a* M'; N a* N'  ImpL <a>.M (y).N z a* ImpL <a>.M' (y).N' z"
by (blast intro!: a_star_ImpLL a_star_ImpLR intro: rtranclp_trans)

lemma a_star_ImpR:
    "M a* M'  ImpR (x).<a>.M b a* ImpR (x).<a>.M' b"
by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+

lemmas a_star_congs = a_star_Cut a_star_NotR a_star_NotL a_star_AndR a_star_AndL1 a_star_AndL2
                      a_star_OrL a_star_OrR1 a_star_OrR2 a_star_ImpL a_star_ImpR

lemma a_star_redu_NotL_elim:
  assumes "NotL <a>.M x a* R"
  shows "M'. R = NotL <a>.M' x  M a* M'"
  using assms by (induct set: rtranclp) (use a_redu_NotL_elim in force)+

lemma a_star_redu_NotR_elim:
  assumes "NotR (x).M a a* R"
  shows "M'. R = NotR (x).M' a  M a* M'"
  using assms by (induct set: rtranclp) (use a_redu_NotR_elim in force)+

lemma a_star_redu_AndR_elim:
  assumes "AndR <a>.M <b>.N ca* R"
  shows "(M' N'. R = AndR <a>.M' <b>.N' c  M a* M'  N a* N')"
  using assms by (induct set: rtranclp) (use a_redu_AndR_elim in force)+

lemma a_star_redu_AndL1_elim:
  assumes "AndL1 (x).M y a* R"
  shows "M'. R = AndL1 (x).M' y  M a* M'"
  using assms by (induct set: rtranclp) (use a_redu_AndL1_elim in force)+

lemma a_star_redu_AndL2_elim:
  assumes "AndL2 (x).M y a* R"
  shows "M'. R = AndL2 (x).M' y  M a* M'"
  using assms by (induct set: rtranclp) (use a_redu_AndL2_elim in force)+

lemma a_star_redu_OrL_elim:
  assumes "OrL (x).M (y).N z a* R"
  shows "(M' N'. R = OrL (x).M' (y).N' z  M a* M'  N a* N')"
  using assms by (induct set: rtranclp) (use a_redu_OrL_elim in force)+

lemma a_star_redu_OrR1_elim:
  assumes "OrR1 <a>.M y a* R"
  shows "M'. R = OrR1 <a>.M' y  M a* M'"
  using assms by (induct set: rtranclp) (use a_redu_OrR1_elim in force)+

lemma a_star_redu_OrR2_elim:
  assumes "OrR2 <a>.M y a* R"
  shows "M'. R = OrR2 <a>.M' y  M a* M'"
  using assms by (induct set: rtranclp) (use a_redu_OrR2_elim in force)+

lemma a_star_redu_ImpR_elim:
  assumes "ImpR (x).<a>.M y a* R"
  shows "M'. R = ImpR (x).<a>.M' y  M a* M'"
  using assms by (induct set: rtranclp) (use a_redu_ImpR_elim in force)+

lemma a_star_redu_ImpL_elim:
  assumes "ImpL <a>.M (y).N z a* R"
  shows "(M' N'. R = ImpL <a>.M' (y).N' z  M a* M'  N a* N')"
  using assms by (induct set: rtranclp) (use a_redu_ImpL_elim in force)+

text ‹Substitution›

lemma subst_not_fin1:
  shows "¬fin(M{x:=<c>.P}) x"
proof (nominal_induct M avoiding: x c P rule: trm.strong_induct)
  case (Ax name coname)
  with fin_rest_elims show ?case
    by (auto simp: fin_Ax_elim)
next
  case (NotL coname trm name)
  obtain x'::name where "x'(trm{x:=<c>.P},P)"
    by (meson exists_fresh(1) fs_name1)
  with NotL fin_NotL_elim fresh_fun_simp_NotL show ?case
    by simp (metis fin_rest_elims(1) fresh_prod)
next
  case (AndL1 name1 trm name2)
  obtain x'::name where "x'  (trm{x:=<c>.P},P,name1)"
    by (meson exists_fresh(1) fs_name1)
  with AndL1 fin_AndL1_elim fresh_fun_simp_AndL1 show ?case
    by simp (metis fin_rest_elims(1) fresh_prod)
next
  case (AndL2 name2 trm name2)
  obtain x'::name where "x'  (trm{x:=<c>.P},P,name2)"
    by (meson exists_fresh(1) fs_name1)
  with AndL2 fin_AndL2_elim fresh_fun_simp_AndL2 better_AndL2_substn show ?case
    by (metis abs_fresh(1) fresh_atm(1) not_fin_subst2)
next
  case (OrL name1 trm1 name2 trm2 name3)
  obtain x'::name where "x'  (trm1{x:=<c>.P},P,name1,trm2{x:=<c>.P},name2)"
    by (meson exists_fresh(1) fs_name1)
  with OrL fin_OrL_elim fresh_fun_simp_OrL show ?case
    by simp (metis fin_rest_elims(1) fresh_prod)
next
  case (ImpL coname trm1 name1 trm2 name2)
  obtain x'::name where "x'  (trm1{name2:=<c>.P},P,name1,trm2{name2:=<c>.P})"
    by (meson exists_fresh(1) fs_name1)
  with ImpL fin_ImpL_elim fresh_fun_simp_ImpL show ?case
    by simp (metis fin_rest_elims(1) fresh_prod)
qed (use fin_rest_elims not_fin_subst2 in auto)

lemmas subst_not_fin2 = not_fin_subst1

text ‹Reductions›

lemma fin_l_reduce:
  assumes "fin M x" and "M l M'"
  shows "fin M' x"
  using assms fin_rest_elims(1) l_redu.simps by fastforce

lemma fin_c_reduce:
  assumes "fin M x" and "M c M'"
  shows "fin M' x"
  using assms c_redu.simps fin_rest_elims(1) by fastforce

lemma fin_a_reduce:
  assumes  a: "fin M x"
  and      b: "M a M'"
  shows "fin M' x"
using assms
proof (induct)
  case (1 x a)
  then show ?case
    using ax_do_not_a_reduce by auto
next
  case (2 x M a)
  then show ?case
    using a_redu_NotL_elim fresh_a_redu1 by blast
next
  case (3 y x M)
  then show ?case
    by (metis a_redu_AndL1_elim abs_fresh(1) fin.intros(3) fresh_a_redu1)
next
  case (4 y x M)
  then show ?case
    by (metis a_redu_AndL2_elim abs_fresh(1) fin.intros(4) fresh_a_redu1)
next
  case (5 z x M y N)
  then show ?case
    by (smt (verit) a_redu_OrL_elim abs_fresh(1) fin.intros(5) fresh_a_redu1)
next
  case (6 y M x N a)
  then show ?case
    by (smt (verit, best) a_redu_ImpL_elim abs_fresh(1) fin.simps fresh_a_redu1)
qed


lemma fin_a_star_reduce:
  assumes  a: "fin M x"
  and      b: "M a* M'"
  shows "fin M' x"
using b a by (induct set: rtranclp)(auto simp: fin_a_reduce)

lemma fic_l_reduce:
  assumes  a: "fic M x"
  and      b: "M l M'"
  shows "fic M' x"
  using b a
  by induction (use fic_rest_elims in force)+

lemma fic_c_reduce:
  assumes a: "fic M x"
  and     b: "M c M'"
  shows "fic M' x"
using b a
  by induction (use fic_rest_elims in force)+

lemma fic_a_reduce:
  assumes a: "fic M x"
  and     b: "M a M'"
shows "fic M' x"
  using assms
proof induction
  case (1 x a)
  then show ?case
    using ax_do_not_a_reduce by fastforce
next
  case (2 a M x)
  then show ?case
    using a_redu_NotR_elim fresh_a_redu2 by blast
next
  case (3 c a M b N)
  then show ?case
    by (smt (verit) a_redu_AndR_elim abs_fresh(2) fic.intros(3) fresh_a_redu2)
next
  case (4 b a M)
  then show ?case
    by (metis a_redu_OrR1_elim abs_fresh(2) fic.intros(4) fresh_a_redu2)
next
  case (5 b a M)
  then show ?case
    by (metis a_redu_OrR2_elim abs_fresh(2) fic.simps fresh_a_redu2)
next
  case (6 b a M x)
  then show ?case
    by (metis a_redu_ImpR_elim abs_fresh(2) fic.simps fresh_a_redu2)
qed


lemma fic_a_star_reduce:
  assumes  a: "fic M x"
  and      b: "M a* M'"
  shows "fic M' x"
using b a
  by (induct set: rtranclp) (auto simp: fic_a_reduce)

text ‹substitution properties›

lemma subst_with_ax1:
  shows "M{x:=<a>.Ax y a} a* M[x⊢n>y]"
proof(nominal_induct M avoiding: x a y rule: trm.strong_induct)
  case (Ax z b x a y)
  show "(Ax z b){x:=<a>.Ax y a} a* (Ax z b)[x⊢n>y]"
  proof (cases "z=x")
    case True
    assume eq: "z=x"
    have "(Ax z b){x:=<a>.Ax y a} = Cut <a>.Ax y a (x).Ax x b" using eq by simp
    also have " a* (Ax x b)[x⊢n>y]" by blast
    finally show "Ax z b{x:=<a>.Ax y a} a* (Ax z b)[x⊢n>y]" using eq by simp
  next
    case False
    assume neq: "zx"
    then show "(Ax z b){x:=<a>.Ax y a} a* (Ax z b)[x⊢n>y]" using neq by simp
  qed
next
  case (Cut b M z N x a y)
  have fs: "bx" "ba" "by" "bN" "zx" "za" "zy" "zM" by fact+
  have ih1: "M{x:=<a>.Ax y a} a* M[x⊢n>y]" by fact
  have ih2: "N{x:=<a>.Ax y a} a* N[x⊢n>y]" by fact
  show "(Cut <b>.M (z).N){x:=<a>.Ax y a} a* (Cut <b>.M (z).N)[x⊢n>y]"
  proof (cases "M = Ax x b")
    case True
    assume eq: "M = Ax x b"
    have "(Cut <b>.M (z).N){x:=<a>.Ax y a} = Cut <a>.Ax y a (z).(N{x:=<a>.Ax y a})" using fs eq by simp
    also have " a* Cut <a>.Ax y a (z).(N[x⊢n>y])" using ih2 a_star_congs by blast
    also have " = Cut <b>.(M[x⊢n>y]) (z).(N[x⊢n>y])" using eq
      by (simp add: trm.inject alpha calc_atm fresh_atm)
    finally show "(Cut <b>.M (z).N){x:=<a>.Ax y a} a* (Cut <b>.M (z).N)[x⊢n>y]" using fs by simp
  next
    case False
    assume neq: "M  Ax x b"
    have "(Cut <b>.M (z).N){x:=<a>.Ax y a} = Cut <b>.(M{x:=<a>.Ax y a}) (z).(N{x:=<a>.Ax y a})" 
      using fs neq by simp
    also have " a* Cut <b>.(M[x⊢n>y]) (z).(N[x⊢n>y])" using ih1 ih2 a_star_congs by blast
    finally show "(Cut <b>.M (z).N){x:=<a>.Ax y a} a* (Cut <b>.M (z).N)[x⊢n>y]" using fs by simp
  qed
next
  case (NotR z M b x a y)
  have fs: "zx" "za" "zy" "zb" by fact+
  have ih: "M{x:=<a>.Ax y a} a* M[x⊢n>y]" by fact
  have "(NotR (z).M b){x:=<a>.Ax y a} = NotR (z).(M{x:=<a>.Ax y a}) b" using fs by simp
  also have " a* NotR (z).(M[x⊢n>y]) b" using ih by (auto intro: a_star_congs)
  finally show "(NotR (z).M b){x:=<a>.Ax y a} a* (NotR (z).M b)[x⊢n>y]" using fs by simp
next
  case (NotL b M z x a y)  
  have fs: "bx" "ba" "by" "bz" by fact+
  have ih: "M{x:=<a>.Ax y a} a* M[x⊢n>y]" by fact
  show "(NotL <b>.M z){x:=<a>.Ax y a} a* (NotL <b>.M z)[x⊢n>y]"
  proof(cases "z=x")
    case True
    assume eq: "z=x"
    obtain x'::"name" where new: "x'(Ax y a,M{x:=<a>.Ax y a})" by (rule exists_fresh(1)[OF fs_name1])
    have "(NotL <b>.M z){x:=<a>.Ax y a} = 
                        fresh_fun (λx'. Cut <a>.Ax y a (x').NotL <b>.(M{x:=<a>.Ax y a}) x')"
      using eq fs by simp
    also have " = Cut <a>.Ax y a (x').NotL <b>.(M{x:=<a>.Ax y a}) x'" 
      using new by (simp add: fresh_fun_simp_NotL fresh_prod)
    also have " a* (NotL <b>.(M{x:=<a>.Ax y a}) x')[x'⊢n>y]"
      using new 
      by (intro a_starI al_redu better_LAxL_intro) auto
    also have " = NotL <b>.(M{x:=<a>.Ax y a}) y" using new by (simp add: nrename_fresh)
    also have " a* NotL <b>.(M[x⊢n>y]) y" using ih by (auto intro: a_star_congs)
    also have " = (NotL <b>.M z)[x⊢n>y]" using eq by simp
    finally show "(NotL <b>.M z){x:=<a>.Ax y a} a* (NotL <b>.M z)[x⊢n>y]" by simp
  next
    case False
    assume neq: "zx"
    have "(NotL <b>.M z){x:=<a>.Ax y a} = NotL <b>.(M{x:=<a>.Ax y a}) z" using fs neq by simp
    also have " a* NotL <b>.(M[x⊢n>y]) z" using ih by (auto intro: a_star_congs)
    finally show "(NotL <b>.M z){x:=<a>.Ax y a} a* (NotL <b>.M z)[x⊢n>y]" using neq by simp
  qed
next
  case (AndR c M d N e x a y)
  have fs: "cx" "ca" "cy" "dx" "da" "dy" "dc" "cN" "ce" "dM" "de" by fact+
  have ih1: "M{x:=<a>.Ax y a} a* M[x⊢n>y]" by fact
  have ih2: "N{x:=<a>.Ax y a} a* N[x⊢n>y]" by fact
  have "(AndR <c>.M <d>.N e){x:=<a>.Ax y a} = AndR <c>.(M{x:=<a>.Ax y a}) <d>.(N{x:=<a>.Ax y a}) e"
    using fs by simp
  also have " a* AndR <c>.(M[x⊢n>y]) <d>.(N[x⊢n>y]) e" using ih1 ih2 by (auto intro: a_star_congs)
  finally show "(AndR <c>.M <d>.N e){x:=<a>.Ax y a} a* (AndR <c>.M <d>.N e)[x⊢n>y]"
    using fs by simp
next
  case (AndL1 u M v x a y)
  have fs: "ux" "ua" "uy" "uv" by fact+
  have ih: "M{x:=<a>.Ax y a} a* M[x⊢n>y]" by fact
  show "(AndL1 (u).M v){x:=<a>.Ax y a} a* (AndL1 (u).M v)[x⊢n>y]"
  proof(cases "v=x")
    case True
    assume eq: "v=x"
    obtain v'::"name" where new: "v'(Ax y a,M{x:=<a>.Ax y a},u)" by (rule exists_fresh(1)[OF fs_name1])
    have "(AndL1 (u).M v){x:=<a>.Ax y a} = 
                        fresh_fun (λv'. Cut <a>.Ax y a (v').AndL1 (u).(M{x:=<a>.Ax y a}) v')"
      using eq fs by simp
    also have " = Cut <a>.Ax y a (v').AndL1 (u).(M{x:=<a>.Ax y a}) v'" 
      using new by (simp add: fresh_fun_simp_AndL1 fresh_prod)
    also have " a* (AndL1 (u).(M{x:=<a>.Ax y a}) v')[v'⊢n>y]"
      using new 
      by (intro a_starI a_redu.intros better_LAxL_intro fin.intros) (simp add: abs_fresh)
    also have " = AndL1 (u).(M{x:=<a>.Ax y a}) y" using fs new
      by (auto simp: fresh_prod fresh_atm nrename_fresh)
    also have " a* AndL1 (u).(M[x⊢n>y]) y" using ih by (auto intro: a_star_congs)
    also have " = (AndL1 (u).M v)[x⊢n>y]" using eq fs by simp
    finally show "(AndL1 (u).M v){x:=<a>.Ax y a} a* (AndL1 (u).M v)[x⊢n>y]" by simp
  next
    case False
    assume neq: "vx"
    have "(AndL1 (u).M v){x:=<a>.Ax y a} = AndL1 (u).(M{x:=<a>.Ax y a}) v" using fs neq by simp
    also have " a* AndL1 (u).(M[x⊢n>y]) v" using ih by (auto intro: a_star_congs)
    finally show "(AndL1 (u).M v){x:=<a>.Ax y a} a* (AndL1 (u).M v)[x⊢n>y]" using fs neq by simp
  qed
next
  case (AndL2 u M v x a y)
  have fs: "ux" "ua" "uy" "uv" by fact+
  have ih: "M{x:=<a>.Ax y a} a* M[x⊢n>y]" by fact
  show "(AndL2 (u).M v){x:=<a>.Ax y a} a* (AndL2 (u).M v)[x⊢n>y]"
  proof(cases "v=x")
    case True
    assume eq: "v=x"
    obtain v'::"name" where new: "v'(Ax y a,M{x:=<a>.Ax y a},u)" by (rule exists_fresh(1)[OF fs_name1])
    have "(AndL2 (u).M v){x:=<a>.Ax y a} = 
                        fresh_fun (λv'. Cut <a>.Ax y a (v').AndL2 (u).(M{x:=<a>.Ax y a}) v')"
      using eq fs by simp
    also have " = Cut <a>.Ax y a (v').AndL2 (u).(M{x:=<a>.Ax y a}) v'" 
      using new by (simp add: fresh_fun_simp_AndL2 fresh_prod)
    also have " a* (AndL2 (u).(M{x:=<a>.Ax y a}) v')[v'⊢n>y]"
      using new 
      by (intro a_starI a_redu.intros better_LAxL_intro fin.intros) (simp add: abs_fresh)
    also have " = AndL2 (u).(M{x:=<a>.Ax y a}) y" using fs new
      by (auto simp: fresh_prod fresh_atm nrename_fresh)
    also have " a* AndL2 (u).(M[x⊢n>y]) y" using ih by (auto intro: a_star_congs)
    also have " = (AndL2 (u).M v)[x⊢n>y]" using eq fs by simp
    finally show "(AndL2 (u).M v){x:=<a>.Ax y a} a* (AndL2 (u).M v)[x⊢n>y]" by simp
  next
    case False
    assume neq: "vx"
    have "(AndL2 (u).M v){x:=<a>.Ax y a} = AndL2 (u).(M{x:=<a>.Ax y a}) v" using fs neq by simp
    also have " a* AndL2 (u).(M[x⊢n>y]) v" using ih by (auto intro: a_star_congs)
    finally show "(AndL2 (u).M v){x:=<a>.Ax y a} a* (AndL2 (u).M v)[x⊢n>y]" using fs neq by simp
  qed
next
  case (OrR1 c M d  x a y)
  have fs: "cx" "ca" "cy" "cd" by fact+
  have ih: "M{x:=<a>.Ax y a} a* M[x⊢n>y]" by fact
  have "(OrR1 <c>.M d){x:=<a>.Ax y a} = OrR1 <c>.(M{x:=<a>.Ax y a}) d" using fs by (simp add: fresh_atm)
  also have " a* OrR1 <c>.(M[x⊢n>y]) d" using ih by (auto intro: a_star_congs)
  finally show "(OrR1 <c>.M d){x:=<a>.Ax y a} a* (OrR1 <c>.M d)[x⊢n>y]" using fs by simp
next
  case (OrR2 c M d  x a y)
  have fs: "cx" "ca" "cy" "cd" by fact+
  have ih: "M{x:=<a>.Ax y a} a* M[x⊢n>y]" by fact
  have "(OrR2 <c>.M d){x:=<a>.Ax y a} = OrR2 <c>.(M{x:=<a>.Ax y a}) d" using fs by (simp add: fresh_atm)
  also have " a* OrR2 <c>.(M[x⊢n>y]) d" using ih by (auto intro: a_star_congs)
  finally show "(OrR2 <c>.M d){x:=<a>.Ax y a} a* (OrR2 <c>.M d)[x⊢n>y]" using fs by simp
next
  case (OrL u M v N z x a y)
  have fs: "ux" "ua" "uy" "vx" "va" "vy" "vu" "uN" "uz" "vM" "vz" by fact+
  have ih1: "M{x:=<a>.Ax y a} a* M[x⊢n>y]" by fact
  have ih2: "N{x:=<a>.Ax y a} a* N[x⊢n>y]" by fact
  show "(OrL (u).M (v).N z){x:=<a>.Ax y a} a* (OrL (u).M (v).N z)[x⊢n>y]"
  proof(cases "z=x")
    case True
    assume eq: "z=x"
    obtain z'::"name" where new: "z'(Ax y a,M{x:=<a>.Ax y a},N{x:=<a>.Ax y a},u,v,y,a)" 
      by (rule exists_fresh(1)[OF fs_name1])
    have "(OrL (u).M (v).N z){x:=<a>.Ax y a} = 
                 fresh_fun (λz'. Cut <a>.Ax y a (z').OrL (u).(M{x:=<a>.Ax y a}) (v).(N{x:=<a>.Ax y a}) z')"
      using eq fs by simp
    also have " = Cut <a>.Ax y a (z').OrL (u).(M{x:=<a>.Ax y a}) (v).(N{x:=<a>.Ax y a}) z'" 
      using new by (simp add: fresh_fun_simp_OrL)
    also have " a* (OrL (u).(M{x:=<a>.Ax y a}) (v).(N{x:=<a>.Ax y a}) z')[z'⊢n>y]"
      using new 
      by (intro a_starI a_redu.intros better_LAxL_intro fin.intros) (simp_all add: abs_fresh)
    also have " = OrL (u).(M{x:=<a>.Ax y a}) (v).(N{x:=<a>.Ax y a}) y" using fs new
      by (auto simp: fresh_prod fresh_atm nrename_fresh subst_fresh)
    also have " a* OrL (u).(M[x⊢n>y]) (v).(N[x⊢n>y]) y" 
      using ih1 ih2 by (auto intro: a_star_congs)
    also have " = (OrL (u).M (v).N z)[x⊢n>y]" using eq fs by simp
    finally show "(OrL (u).M (v).N z){x:=<a>.Ax y a} a* (OrL (u).M (v).N z)[x⊢n>y]" by simp
  next
    case False
    assume neq: "zx"
    have "(OrL (u).M (v).N z){x:=<a>.Ax y a} = OrL (u).(M{x:=<a>.Ax y a}) (v).(N{x:=<a>.Ax y a}) z" 
      using fs neq by simp
    also have " a* OrL (u).(M[x⊢n>y]) (v).(N[x⊢n>y]) z" 
      using ih1 ih2 by (auto intro: a_star_congs)
    finally show "(OrL (u).M (v).N z){x:=<a>.Ax y a} a* (OrL (u).M (v).N z)[x⊢n>y]" using fs neq by simp
  qed
next
  case (ImpR z c M d x a y)
  have fs: "zx" "za" "zy" "cx" "ca" "cy" "zd" "cd" by fact+
  have ih: "M{x:=<a>.Ax y a} a* M[x⊢n>y]" by fact
  have "(ImpR (z).<c>.M d){x:=<a>.Ax y a} = ImpR (z).<c>.(M{x:=<a>.Ax y a}) d" using fs by simp
  also have " a* ImpR (z).<c>.(M[x⊢n>y]) d" using ih by (auto intro: a_star_congs)
  finally show "(ImpR (z).<c>.M d){x:=<a>.Ax y a} a* (ImpR (z).<c>.M d)[x⊢n>y]" using fs by simp
next
  case (ImpL c M u N v x a y)
  have fs: "cx" "ca" "cy" "ux" "ua" "uy" "cN" "cv" "uM" "uv" by fact+
  have ih1: "M{x:=<a>.Ax y a} a* M[x⊢n>y]" by fact
  have ih2: "N{x:=<a>.Ax y a} a* N[x⊢n>y]" by fact
  show "(ImpL <c>.M (u).N v){x:=<a>.Ax y a} a* (ImpL <c>.M (u).N v)[x⊢n>y]"
  proof(cases "v=x")
    case True
    assume eq: "v=x"
    obtain v'::"name" where new: "v'(Ax y a,M{x:=<a>.Ax y a},N{x:=<a>.Ax y a},y,a,u)" 
      by (rule exists_fresh(1)[OF fs_name1])
    have "(ImpL <c>.M (u).N v){x:=<a>.Ax y a} = 
                 fresh_fun (λv'. Cut <a>.Ax y a (v').ImpL <c>.(M{x:=<a>.Ax y a}) (u).(N{x:=<a>.Ax y a}) v')"
      using eq fs by simp 
    also have " = Cut <a>.Ax y a (v').ImpL <c>.(M{x:=<a>.Ax y a}) (u).(N{x:=<a>.Ax y a}) v'" 
      using new by (simp add: fresh_fun_simp_ImpL)
    also have " a* (ImpL <c>.(M{x:=<a>.Ax y a}) (u).(N{x:=<a>.Ax y a}) v')[v'⊢n>y]"
      using new 
      by (intro a_starI a_redu.intros better_LAxL_intro fin.intros) (simp_all add: abs_fresh)
    also have " = ImpL <c>.(M{x:=<a>.Ax y a}) (u).(N{x:=<a>.Ax y a}) y" using fs new
      by (auto simp: fresh_prod subst_fresh fresh_atm trm.inject alpha rename_fresh)
    also have " a* ImpL <c>.(M[x⊢n>y]) (u).(N[x⊢n>y]) y" 
      using ih1 ih2 by (auto intro: a_star_congs)
    also have " = (ImpL <c>.M (u).N v)[x⊢n>y]" using eq fs by simp
    finally show "(ImpL <c>.M (u).N v){x:=<a>.Ax y a} a* (ImpL <c>.M (u).N v)[x⊢n>y]" using fs by simp
  next
    case False
    assume neq: "vx"
    have "(ImpL <c>.M (u).N v){x:=<a>.Ax y a} = ImpL <c>.(M{x:=<a>.Ax y a}) (u).(N{x:=<a>.Ax y a}) v" 
      using fs neq by simp
    also have " a* ImpL <c>.(M[x⊢n>y]) (u).(N[x⊢n>y]) v" 
      using ih1 ih2 by (auto intro: a_star_congs)
    finally show "(ImpL <c>.M (u).N v){x:=<a>.Ax y a} a* (ImpL <c>.M (u).N v)[x⊢n>y]" 
      using fs neq by simp
  qed
qed

lemma subst_with_ax2:
  shows "M{b:=(x).Ax x a} a* M[b⊢c>a]"
proof(nominal_induct M avoiding: b a x rule: trm.strong_induct)
  case (Ax z c b a x)
  show "(Ax z c){b:=(x).Ax x a} a* (Ax z c)[b⊢c>a]"
  proof (cases "c=b")
    case True
    assume eq: "c=b"
    have "(Ax z c){b:=(x).Ax x a} = Cut <b>.Ax z c (x).Ax x a" using eq by simp
    also have " a* (Ax z c)[b⊢c>a]" using eq by blast
    finally show "(Ax z c){b:=(x).Ax x a} a* (Ax z c)[b⊢c>a]" by simp
  next
    case False
    assume neq: "cb"
    then show "(Ax z c){b:=(x).Ax x a} a* (Ax z c)[b⊢c>a]" by simp
  qed
next
  case (Cut c M z N b a x)
  have fs: "cb" "ca" "cx" "cN" "zb" "za" "zx" "zM" by fact+
  have ih1: "M{b:=(x).Ax x a} a* M[b⊢c>a]" by fact
  have ih2: "N{b:=(x).Ax x a} a* N[b⊢c>a]" by fact
  show "(Cut <c>.M (z).N){b:=(x).Ax x a} a* (Cut <c>.M (z).N)[b⊢c>a]"
  proof (cases "N = Ax z b")
    case True
    assume eq: "N = Ax z b"
    have "(Cut <c>.M (z).N){b:=(x).Ax x a} = Cut <c>.(M{b:=(x).Ax x a}) (x).Ax x a" using eq fs by simp 
    also have " a* Cut <c>.(M[b⊢c>a]) (x).Ax x a" using ih1 a_star_congs by blast
    also have " = Cut <c>.(M[b⊢c>a]) (z).(N[b⊢c>a])" using eq fs
      by (simp add: trm.inject alpha calc_atm fresh_atm)
    finally show "(Cut <c>.M (z).N){b:=(x).Ax x a} a* (Cut <c>.M (z).N)[b⊢c>a]" using fs by simp
  next
    case False
    assume neq: "N  Ax z b"
    have "(Cut <c>.M (z).N){b:=(x).Ax x a} = Cut <c>.(M{b:=(x).Ax x a}) (z).(N{b:=(x).Ax x a})" 
      using fs neq by simp
    also have " a* Cut <c>.(M[b⊢c>a]) (z).(N[b⊢c>a])" using ih1 ih2 a_star_congs by blast
    finally show "(Cut <c>.M (z).N){b:=(x).Ax x a} a* (Cut <c>.M (z).N)[b⊢c>a]" using fs by simp
  qed
next
  case (NotR z M c b a x)
  have fs: "zb" "za" "zx" "zc" by fact+
  have ih: "M{b:=(x).Ax x a} a* M[b⊢c>a]" by fact
  show "(NotR (z).M c){b:=(x).Ax x a} a* (NotR (z).M c)[b⊢c>a]"
  proof (cases "c=b")
    case True
    assume eq: "c=b"
    obtain a'::"coname" where new: "a'(Ax x a,M{b:=(x).Ax x a})" by (rule exists_fresh(2)[OF fs_coname1])
    have "(NotR (z).M c){b:=(x).Ax x a} = 
                        fresh_fun (λa'. Cut <a'>.NotR (z).M{b:=(x).Ax x a} a' (x).Ax x a)" 
      using eq fs by simp
    also have " = Cut <a'>.NotR (z).M{b:=(x).Ax x a} a' (x).Ax x a"
      using new by (simp add: fresh_fun_simp_NotR fresh_prod)
    also have " a* (NotR (z).(M{b:=(x).Ax x a}) a')[a'⊢c>a]"
      using new 
      by (intro a_starI a_redu.intros better_LAxR_intro fic.intros) auto
    also have " = NotR (z).(M{b:=(x).Ax x a}) a" using new by (simp add: crename_fresh)
    also have " a* NotR (z).(M[b⊢c>a]) a" using ih by (auto intro: a_star_congs)
    also have " = (NotR (z).M c)[b⊢c>a]" using eq by simp
    finally show "(NotR (z).M c){b:=(x).Ax x a} a* (NotR (z).M c)[b⊢c>a]" by simp
  next
    case False
    assume neq: "cb"
    have "(NotR (z).M c){b:=(x).Ax x a} = NotR (z).(M{b:=(x).Ax x a}) c" using fs neq by simp
    also have " a* NotR (z).(M[b⊢c>a]) c" using ih by (auto intro: a_star_congs)
    finally show "(NotR (z).M c){b:=(x).Ax x a} a* (NotR (z).M c)[b⊢c>a]" using neq by simp
  qed
next
  case (NotL c M z b a x)  
  have fs: "cb" "ca" "cx" "cz" by fact+
  have ih: "M{b:=(x).Ax x a} a* M[b⊢c>a]" by fact
  have "(NotL <c>.M z){b:=(x).Ax x a} = NotL <c>.(M{b:=(x).Ax x a}) z" using fs by simp
  also have " a* NotL <c>.(M[b⊢c>a]) z" using ih by (auto intro: a_star_congs)
  finally show "(NotL <c>.M z){b:=(x).Ax x a} a* (NotL <c>.M z)[b⊢c>a]" using fs by simp
next
  case (AndR c M d N e b a x)
  have fs: "cb" "ca" "cx" "db" "da" "dx" "dc" "cN" "ce" "dM" "de" by fact+
  have ih1: "M{b:=(x).Ax x a} a* M[b⊢c>a]" by fact
  have ih2: "N{b:=(x).Ax x a} a* N[b⊢c>a]" by fact
  show "(AndR <c>.M <d>.N e){b:=(x).Ax x a} a* (AndR <c>.M <d>.N e)[b⊢c>a]"
  proof(cases "e=b")
    case True
    assume eq: "e=b"
    obtain e'::"coname" where new: "e'(Ax x a,M{b:=(x).Ax x a},N{b:=(x).Ax x a},c,d)" 
      by (rule exists_fresh(2)[OF fs_coname1])
    have "(AndR <c>.M <d>.N e){b:=(x).Ax x a} = 
               fresh_fun (λe'. Cut <e'>.AndR <c>.(M{b:=(x).Ax x a}) <d>.(N{b:=(x).Ax x a}) e' (x).Ax x a)"
      using eq fs by simp
    also have " = Cut <e'>.AndR <c>.(M{b:=(x).Ax x a}) <d>.(N{b:=(x).Ax x a}) e' (x).Ax x a"
      using new by (simp add: fresh_fun_simp_AndR fresh_prod)
    also have " a* (AndR <c>.(M{b:=(x).Ax x a}) <d>.(N{b:=(x).Ax x a}) e')[e'⊢c>a]"
      using new 
      by (intro a_starI a_redu.intros better_LAxR_intro fic.intros) (simp_all add: abs_fresh)
    also have " = AndR <c>.(M{b:=(x).Ax x a}) <d>.(N{b:=(x).Ax x a}) a" using fs new
      by (auto simp: fresh_prod fresh_atm subst_fresh crename_fresh)
    also have " a* AndR <c>.(M[b⊢c>a]) <d>.(N[b⊢c>a]) a" using ih1 ih2 by (auto intro: a_star_congs)
    also have " = (AndR <c>.M <d>.N e)[b⊢c>a]" using eq fs by simp
    finally show "(AndR <c>.M <d>.N e){b:=(x).Ax x a} a* (AndR <c>.M <d>.N e)[b⊢c>a]" by simp
  next
    case False
    assume neq: "eb"
    have "(AndR <c>.M <d>.N e){b:=(x).Ax x a} = AndR <c>.(M{b:=(x).Ax x a}) <d>.(N{b:=(x).Ax x a}) e"
      using fs neq by simp
    also have " a* AndR <c>.(M[b⊢c>a]) <d>.(N[b⊢c>a]) e" using ih1 ih2 by (auto intro: a_star_congs)
    finally show "(AndR <c>.M <d>.N e){b:=(x).Ax x a} a* (AndR <c>.M <d>.N e)[b⊢c>a]"
      using fs neq by simp
  qed
next
  case (AndL1 u M v b a x)
  have fs: "ub" "ua" "ux" "uv" by fact+
  have ih: "M{b:=(x).Ax x a} a* M[b⊢c>a]" by fact
  have "(AndL1 (u).M v){b:=(x).Ax x a} = AndL1 (u).(M{b:=(x).Ax x a}) v" using fs by simp
  also have " a* AndL1 (u).(M[b⊢c>a]) v" using ih by (auto intro: a_star_congs)
  finally show "(AndL1 (u).M v){b:=(x).Ax x a} a* (AndL1 (u).M v)[b⊢c>a]" using fs by simp
next
  case (AndL2 u M v b a x)
  have fs: "ub" "ua" "ux" "uv" by fact+
  have ih: "M{b:=(x).Ax x a} a* M[b⊢c>a]" by fact
  have "(AndL2 (u).M v){b:=(x).Ax x a} = AndL2 (u).(M{b:=(x).Ax x a}) v" using fs by simp
  also have " a* AndL2 (u).(M[b⊢c>a]) v" using ih by (auto intro: a_star_congs)
  finally show "(AndL2 (u).M v){b:=(x).Ax x a} a* (AndL2 (u).M v)[b⊢c>a]" using fs by simp
next
  case (OrR1 c M d  b a x)
  have fs: "cb" "ca" "cx" "cd" by fact+
  have ih: "M{b:=(x).Ax x a} a* M[b⊢c>a]" by fact
  show "(OrR1 <c>.M d){b:=(x).Ax x a} a* (OrR1 <c>.M d)[b⊢c>a]"
  proof(cases "d=b")
    case True
    assume eq: "d=b"
    obtain a'::"coname" where new: "a'(Ax x a,M{b:=(x).Ax x a},c,x,a)" 
      by (rule exists_fresh(2)[OF fs_coname1])
    have "(OrR1 <c>.M d){b:=(x).Ax x a} = 
             fresh_fun (λa'. Cut <a'>.OrR1 <c>.M{b:=(x).Ax x a} a' (x).Ax x a)" using fs eq by (simp)
    also have " = Cut <a'>.OrR1 <c>.M{b:=(x).Ax x a} a' (x).Ax x a"
      using new by (simp add: fresh_fun_simp_OrR1)
    also have " a* (OrR1 <c>.M{b:=(x).Ax x a} a')[a'⊢c>a]"
      using new 
      by (intro a_starI a_redu.intros better_LAxR_intro fic.intros) (simp_all add: abs_fresh)
    also have " = OrR1 <c>.M{b:=(x).Ax x a} a" using fs new
      by (auto simp: fresh_prod fresh_atm crename_fresh subst_fresh)
    also have " a* OrR1 <c>.(M[b⊢c>a]) a" using ih by (auto intro: a_star_congs)
    also have " = (OrR1 <c>.M d)[b⊢c>a]" using eq fs by simp
    finally show "(OrR1 <c>.M d){b:=(x).Ax x a} a* (OrR1 <c>.M d)[b⊢c>a]" by simp
  next
    case False
    assume neq: "db"
    have "(OrR1 <c>.M d){b:=(x).Ax x a} = OrR1 <c>.(M{b:=(x).Ax x a}) d" using fs neq by (simp)
    also have " a* OrR1 <c>.(M[b⊢c>a]) d" using ih by (auto intro: a_star_congs)
    finally show "(OrR1 <c>.M d){b:=(x).Ax x a} a* (OrR1 <c>.M d)[b⊢c>a]" using fs neq by simp
  qed
next
  case (OrR2 c M d  b a x)
  have fs: "cb" "ca" "cx" "cd" by fact+
  have ih: "M{b:=(x).Ax x a} a* M[b⊢c>a]" by fact
  show "(OrR2 <c>.M d){b:=(x).Ax x a} a* (OrR2 <c>.M d)[b⊢c>a]"
  proof(cases "d=b")
    case True
    assume eq: "d=b"
    obtain a'::"coname" where new: "a'(Ax x a,M{b:=(x).Ax x a},c,x,a)" 
      by (rule exists_fresh(2)[OF fs_coname1])
    have "(OrR2 <c>.M d){b:=(x).Ax x a} = 
             fresh_fun (λa'. Cut <a'>.OrR2 <c>.M{b:=(x).Ax x a} a' (x).Ax x a)" using fs eq by (simp)
    also have " = Cut <a'>.OrR2 <c>.M{b:=(x).Ax x a} a' (x).Ax x a"
      using new by (simp add: fresh_fun_simp_OrR2)
    also have " a* (OrR2 <c>.M{b:=(x).Ax x a} a')[a'⊢c>a]"
      using new 
      by (intro a_starI a_redu.intros better_LAxR_intro fic.intros) (simp_all add: abs_fresh)
    also have " = OrR2 <c>.M{b:=(x).Ax x a} a" using fs new
      by (auto simp: fresh_prod fresh_atm crename_fresh subst_fresh)
    also have " a* OrR2 <c>.(M[b⊢c>a]) a" using ih by (auto intro: a_star_congs)
    also have " = (OrR2 <c>.M d)[b⊢c>a]" using eq fs by simp
    finally show "(OrR2 <c>.M d){b:=(x).Ax x a} a* (OrR2 <c>.M d)[b⊢c>a]" by simp
  next
    case False
    assume neq: "db"
    have "(OrR2 <c>.M d){b:=(x).Ax x a} = OrR2 <c>.(M{b:=(x).Ax x a}) d" using fs neq by (simp)
    also have " a* OrR2 <c>.(M[b⊢c>a]) d" using ih by (auto intro: a_star_congs)
    finally show "(OrR2 <c>.M d){b:=(x).Ax x a} a* (OrR2 <c>.M d)[b⊢c>a]" using fs neq by simp
  qed
next
  case (OrL u M v N z b a x)
  have fs: "ub" "ua" "ux" "vb" "va" "vx" "vu" "uN" "uz" "vM" "vz" by fact+
  have ih1: "M{b:=(x).Ax x a} a* M[b⊢c>a]" by fact
  have ih2: "N{b:=(x).Ax x a} a* N[b⊢c>a]" by fact
  have "(OrL (u).M (v).N z){b:=(x).Ax x a} = OrL (u).(M{b:=(x).Ax x a}) (v).(N{b:=(x).Ax x a}) z" 
    using fs by simp
  also have " a* OrL (u).(M[b⊢c>a]) (v).(N[b⊢c>a]) z" using ih1 ih2 by (auto intro: a_star_congs)
  finally show "(OrL (u).M (v).N z){b:=(x).Ax x a} a* (OrL (u).M (v).N z)[b⊢c>a]" using fs by simp
next
  case (ImpR z c M d b a x)
  have fs: "zb" "za" "zx" "cb" "ca" "cx" "zd" "cd" by fact+
  have ih: "M{b:=(x).Ax x a} a* M[b⊢c>a]" by fact
  show "(ImpR (z).<c>.M d){b:=(x).Ax x a} a* (ImpR (z).<c>.M d)[b⊢c>a]"
  proof(cases "b=d")
    case True
    assume eq: "b=d"
    obtain a'::"coname" where new: "a'(Ax x a,M{b:=(x).Ax x a},x,a,c)" 
      by (rule exists_fresh(2)[OF fs_coname1])
    have "(ImpR (z).<c>.M d){b:=(x).Ax x a} =
                fresh_fun (λa'. Cut <a'>.ImpR z.<c>.M{b:=(x).Ax x a} a' (x).Ax x a)" using fs eq by simp
    also have " = Cut <a'>.ImpR z.<c>.M{b:=(x).Ax x a} a' (x).Ax x a" 
      using new by (simp add: fresh_fun_simp_ImpR)
    also have " a* (ImpR z.<c>.M{b:=(x).Ax x a} a')[a'⊢c>a]"
      using new 
      by (intro a_starI a_redu.intros better_LAxR_intro fic.intros) (simp_all add: abs_fresh)
    also have " = ImpR z.<c>.M{b:=(x).Ax x a} a" using fs new
      by (auto simp: fresh_prod crename_fresh subst_fresh fresh_atm)
    also have " a* ImpR z.<c>.(M[b⊢c>a]) a" using ih by (auto intro: a_star_congs)
    also have " = (ImpR z.<c>.M b)[b⊢c>a]" using eq fs by simp
    finally show "(ImpR (z).<c>.M d){b:=(x).Ax x a} a* (ImpR (z).<c>.M d)[b⊢c>a]" using eq by simp
  next
    case False
    assume neq: "bd"
    have "(ImpR (z).<c>.M d){b:=(x).Ax x a} = ImpR (z).<c>.(M{b:=(x).Ax x a}) d" using fs neq by simp
    also have " a* ImpR (z).<c>.(M[b⊢c>a]) d" using ih by (auto intro: a_star_congs)
    finally show "(ImpR (z).<c>.M d){b:=(x).Ax x a} a* (ImpR (z).<c>.M d)[b⊢c>a]" using neq fs by simp
  qed
next
  case (ImpL c M u N v b a x)
  have fs: "cb" "ca" "cx" "ub" "ua" "ux" "cN" "cv" "uM" "uv" by fact+
  have ih1: "M{b:=(x).Ax x a} a* M[b⊢c>a]" by fact
  have ih2: "N{b:=(x).Ax x a} a* N[b⊢c>a]" by fact
  have "(ImpL <c>.M (u).N v){b:=(x).Ax x a} = ImpL <c>.(M{b:=(x).Ax x a}) (u).(N{b:=(x).Ax x a}) v" 
    using fs by simp
  also have " a* ImpL <c>.(M[b⊢c>a]) (u).(N[b⊢c>a]) v" 
    using ih1 ih2 by (auto intro: a_star_congs)
  finally show "(ImpL <c>.M (u).N v){b:=(x).Ax x a} a* (ImpL <c>.M (u).N v)[b⊢c>a]" 
    using fs by simp
qed

text ‹substitution lemmas›

lemma not_Ax1: "¬(bM)  M{b:=(y).Q}  Ax x a"
proof (nominal_induct M avoiding: b y Q x a rule: trm.strong_induct)
  case (NotR name trm coname)
  then show ?case
    by (metis fin.intros(1) fin_rest_elims(2) subst_not_fin2)
next
  case (AndR coname1 trm1 coname2 trm2 coname3)
  then show ?case
    by (metis fin.intros(1) fin_rest_elims(3) subst_not_fin2)
next
  case (OrR1 coname1 trm coname2)
  then show ?case
    by (metis fin.intros(1) fin_rest_elims(4) subst_not_fin2)
next
  case (OrR2 coname1 trm coname2)
  then show ?case
    by (metis fin.intros(1) fin_rest_elims(5) subst_not_fin2)
next
  case (ImpR name coname1 trm coname2)
  then show ?case
    by (metis fin.intros(1) fin_rest_elims(6) subst_not_fin2)
qed (auto simp: fresh_atm abs_fresh abs_supp fin_supp)



lemma not_Ax2: "¬(xM)  M{x:=<b>.Q}  Ax y a"
proof (nominal_induct M avoiding: b y Q x a rule: trm.strong_induct)
  case (NotL coname trm name)
  then show ?case
    by (metis fic.intros(1) fic_rest_elims(2) not_fic_subst1)
next
  case (AndL1 name1 trm name2)
  then show ?case
    by (metis fic.intros(1) fic_rest_elims(4) not_fic_subst1)
next
  case (AndL2 name1 trm name2)
  then show ?case
    by (metis fic.intros(1) fic_rest_elims(5) not_fic_subst1)
next
  case (OrL name1 trm1 name2 trm2 name3)
  then show ?case
    by (metis fic.intros(1) fic_rest_elims(3) not_fic_subst1)
next
  case (ImpL coname trm1 name1 trm2 name2)
  then show ?case
    by (metis fic.intros(1) fic_rest_elims(6) not_fic_subst1)
qed (auto simp: fresh_atm abs_fresh abs_supp fin_supp)


lemma interesting_subst1:
  assumes a: "xy" "xP" "yP" 
  shows "N{y:=<c>.P}{x:=<c>.P} = N{x:=<c>.Ax y c}{y:=<c>.P}"
  using a
proof(nominal_induct N avoiding: x y c P rule: trm.strong_induct)
  case (Cut d M u M' x' y' c P)
  with assms show ?case
    apply (simp add: abs_fresh)
    by (smt (verit) forget(1) not_Ax2)
next
  case (NotL d M u)
  obtain x'::name and x''::name 
    where "x'  (P,M{y:=<c>.P},M{x:=<c>.Ax y c}{y:=<c>.P},y,x)"
      and  "x'' (P,M{x:=<c>.Ax y c},M{x:=<c>.Ax y c}{y:=<c>.P},Ax y c,y,x)"
    by (meson exists_fresh(1) fs_name1)
  then show ?case
    using NotL
    by (auto simp: perm_fresh_fresh(1) swap_simps(3,7) trm.inject alpha forget 
        fresh_atm abs_fresh fresh_fun_simp_NotL fresh_prod)
next
  case (AndL1 u M d)
  obtain x'::name and x''::name 
    where "x'  (P,M{y:=<c>.P},M{x:=<c>.Ax y c}{y:=<c>.P},u,y,x)"
      and  "x'' (P,Ax y c,M{x:=<c>.Ax y c},M{x:=<c>.Ax y c}{y:=<c>.P},u,y,x)"
    by (meson exists_fresh(1) fs_name1)
  then show ?case
    using AndL1
    by (auto simp: perm_fresh_fresh(1) swap_simps(3,7) trm.inject alpha forget 
        fresh_atm abs_fresh fresh_fun_simp_AndL1 fresh_prod)
next
  case (AndL2 u M d)
  obtain x'::name and x''::name 
    where "x'  (P,M{y:=<c>.P},M{x:=<c>.Ax y c}{y:=<c>.P},u,y,x)"
      and  "x'' (P,Ax y c,M{x:=<c>.Ax y c},M{x:=<c>.Ax y c}{y:=<c>.P},u,y,x)"
    by (meson exists_fresh(1) fs_name1)
  then show ?case
    using AndL2
    by (auto simp: perm_fresh_fresh(1) swap_simps(3,7) trm.inject alpha forget 
        fresh_atm abs_fresh fresh_fun_simp_AndL2 fresh_prod)
next
  case (OrL x1 M x2 M' x3)
  obtain x'::name and x''::name 
    where "x'  (P,M{y:=<c>.P},M{x:=<c>.Ax y c}{y:=<c>.P},
                       M'{y:=<c>.P},M'{x:=<c>.Ax y c}{y:=<c>.P},x1,x2,x3,y,x)"
      and  "x'' (P,Ax y c,M{x:=<c>.Ax y c},M{x:=<c>.Ax y c}{y:=<c>.P},
                                        M'{x:=<c>.Ax y c},M'{x:=<c>.Ax y c}{y:=<c>.P},x1,x2,x3,y,x)"
    by (meson exists_fresh(1) fs_name1)
  then show ?case
    using OrL
    by (auto simp: perm_fresh_fresh(1) swap_simps(3,7) trm.inject alpha forget 
        fresh_atm abs_fresh fresh_fun_simp_OrL fresh_prod subst_fresh)
next
  case (ImpL a M x1 M' x2)
  obtain x'::name and x''::name 
    where "x'  (P,M{x2:=<c>.P},M{x:=<c>.Ax x2 c}{x2:=<c>.P},
                                        M'{x2:=<c>.P},M'{x:=<c>.Ax x2 c}{x2:=<c>.P},x1,y,x)"
      and  "x'' (P,Ax y c,M{x2:=<c>.Ax y c},M{x2:=<c>.Ax y c}{y:=<c>.P},
                                        M'{x2:=<c>.Ax y c},M'{x2:=<c>.Ax y c}{y:=<c>.P},x1,x2,y,x)"
    by (meson exists_fresh(1) fs_name1)
  then show ?case
    using ImpL
    by (auto simp: perm_fresh_fresh(1) swap_simps(3,7) trm.inject alpha forget 
        fresh_atm abs_fresh fresh_fun_simp_ImpL fresh_prod subst_fresh)
qed (auto simp: abs_fresh fresh_atm forget trm.inject subst_fresh)

lemma interesting_subst1':
  assumes "xy" "xP" "yP" 
  shows "N{y:=<c>.P}{x:=<c>.P} = N{x:=<a>.Ax y a}{y:=<c>.P}"
proof -
  show ?thesis
  proof (cases "c=a")
    case True with assms show ?thesis 
      by (simp add: interesting_subst1)
  next
    case False 
    then have "N{x:=<a>.Ax y a} = N{x:=<c>.([(c,a)]Ax y a)}"
      by (simp add: fresh_atm(2,4) fresh_prod substn_rename4)
    with assms show ?thesis
      by (simp add: interesting_subst1 swap_simps) 
  qed
qed

lemma interesting_subst2:
  assumes a: "ab" "aP" "bP" 
  shows "N{a:=(y).P}{b:=(y).P} = N{b:=(y).Ax y a}{a:=(y).P}"
  using a
proof(nominal_induct N avoiding: a b y P rule: trm.strong_induct)
  case Ax
  then show ?case
    by (auto simp: abs_fresh fresh_atm forget trm.inject)
next 
  case (Cut d M u M' x' y' c P)
  with assms show ?case
    apply(auto simp: trm.inject)
      apply (force simp add: abs_fresh forget)
     apply (simp add: abs_fresh forget)
    by (smt (verit, ccfv_threshold) abs_fresh(1) better_Cut_substc forget(2) fresh_prod not_Ax1)
next
  case NotL
  then show ?case
    by (auto simp: abs_fresh fresh_atm forget)
next
  case (NotR u M d)
  obtain a' a''::coname 
    where "a'  (b,P,M{d:=(y).P},M{b:=(y).Ax y d}{d:=(y).P},u,y)"
      and  "a''  (P,M{d:=(y).Ax y a},M{d:=(y).Ax y a}{a:=(y).P},Ax y a,y,d)"
    by (meson exists_fresh'(2) fs_coname1)
  with NotR show ?case
    by (auto simp: abs_fresh fresh_atm forget fresh_prod fresh_fun_simp_NotR)
next
  case (AndR d1 M d2 M' d3)
  obtain a' a''::coname 
    where "a'  (P,M{d3:=(y).P},M{b:=(y).Ax y d3}{d3:=(y).P},
                   M'{d3:=(y).P},M'{b:=(y).Ax y d3}{d3:=(y).P},d1,d2,d3,b,y)"
      and "a''  (P,Ax y a,M{d3:=(y).Ax y a},M{d3:=(y).Ax y a}{a:=(y).P},
                   M'{d3:=(y).Ax y a},M'{d3:=(y).Ax y a}{a:=(y).P},d1,d2,d3,y,b)"
    by (meson exists_fresh'(2) fs_coname1)
  with AndR show ?case
    apply(auto simp: abs_fresh fresh_atm forget trm.inject subst_fresh)
     apply(auto simp only: fresh_prod fresh_fun_simp_AndR)
     apply (force simp:  forget abs_fresh subst_fresh fresh_atm)+
    done
next
  case (AndL1 u M d)
  then show ?case
    by (auto simp: abs_fresh fresh_atm forget trm.inject subst_fresh)
next
  case (AndL2 u M d)
  then show ?case
    by (auto simp: abs_fresh fresh_atm forget trm.inject subst_fresh)
next
  case (OrR1 d M e)
  obtain a' a''::coname 
    where "a'  (b,P,M{e:=(y).P},M{b:=(y).Ax y e}{e:=(y).P},d,e)"
      and "a''  (b,P,Ax y a,M{e:=(y).Ax y a},M{e:=(y).Ax y a}{a:=(y).P},d,e)"
    by (meson exists_fresh'(2) fs_coname1)
  with OrR1 show ?case
    by (auto simp: abs_fresh fresh_atm forget fresh_prod fresh_fun_simp_OrR1)
next
  case (OrR2 d M e)
  obtain a' a''::coname 
    where "a'  (b,P,M{e:=(y).P},M{b:=(y).Ax y e}{e:=(y).P},d,e)"
      and  "a''  (b,P,Ax y a,M{e:=(y).Ax y a},M{e:=(y).Ax y a}{a:=(y).P},d,e)"
    by (meson exists_fresh'(2) fs_coname1)
  with OrR2 show ?case
    by (auto simp: abs_fresh fresh_atm forget fresh_prod fresh_fun_simp_OrR2)
next
  case (OrL x1 M x2 M' x3)
  then show ?case
    by(auto simp: abs_fresh fresh_atm forget trm.inject subst_fresh)
next
  case ImpL
  then show ?case
    by (auto simp: abs_fresh fresh_atm forget trm.inject subst_fresh)
next
  case (ImpR u e M d)
  obtain a' a''::coname 
    where "a'  (b,e,d,P,M{d:=(y).P},M{b:=(y).Ax y d}{d:=(y).P})"
      and  "a''  (e,d,P,Ax y a,M{d:=(y).Ax y a},M{d:=(y).Ax y a}{a:=(y).P})"
    by (meson exists_fresh'(2) fs_coname1)
  with ImpR show ?case
    by (auto simp: abs_fresh fresh_atm forget fresh_prod fresh_fun_simp_ImpR)
qed 

lemma interesting_subst2':
  assumes "ab" "aP" "bP" 
  shows "N{a:=(y).P}{b:=(y).P} = N{b:=(z).Ax z a}{a:=(y).P}"
proof -
  show ?thesis
  proof (cases "z=y")
    case True then show ?thesis using assms by (simp add: interesting_subst2)
  next
    case False 
    then have "N{b:=(z).Ax z a} = N{b:=(y).([(y,z)]Ax z a)}"
      by (metis fresh_atm(1,3) fresh_prod substc_rename2 trm.fresh(1))
    with False assms show ?thesis
      by (simp add: interesting_subst2 calc_atm)
  qed
qed


lemma subst_subst1:
  assumes a: "a(Q,b)" "x(y,P,Q)" "bQ" "yP" 
  shows "M{x:=<a>.P}{b:=(y).Q} = M{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}"
  using a
proof(nominal_induct M avoiding: x a P b y Q rule: trm.strong_induct)
  case (Ax z c)
  then show ?case
    by (auto simp add: abs_fresh fresh_prod fresh_atm subst_fresh trm.inject forget)
next
  case (Cut c M z N)
  then show ?case
    apply (clarsimp simp add: abs_fresh fresh_prod fresh_atm subst_fresh)
    apply (metis forget not_Ax1 not_Ax2)
    done
next
  case (NotR z M c)
  then show ?case
    by (auto simp: forget fresh_prod fresh_atm subst_fresh abs_fresh fresh_fun_simp_NotR)
next
  case (NotL c M z)
  obtain x'::name where "x'  (P,M{x:=<a>.P},P{b:=(y).Q},M{b:=(y).Q}{x:=<a>.P{b:=(y).Q}},y,Q)"
    by (meson exists_fresh(1) fs_name1)
  with NotL show ?case  
    apply(auto simp: fresh_prod fresh_atm abs_fresh subst_fresh subst_fresh fresh_fun_simp_NotL)
    by (metis fresh_fun_simp_NotL fresh_prod subst_fresh(5))
next
  case (AndR c1 M c2 N c3)
  then show ?case  
    by (auto simp: forget fresh_prod fresh_atm subst_fresh abs_fresh fresh_fun_simp_AndR)
next
  case (AndL1 z1 M z2)
  obtain x'::name where "x'  (P,M{x:=<a>.P},P{b:=(y).Q},z1,y,Q,M{b:=(y).Q}{x:=<a>.P{b:=(y).Q}})"
    by (meson exists_fresh(1) fs_name1)
  with AndL1 show ?case  
    apply(auto simp: fresh_prod fresh_atm abs_fresh subst_fresh fresh_fun_simp_AndL1)
    by (metis fresh_atm(1) fresh_fun_simp_AndL1 fresh_prod subst_fresh(5))
next
  case (AndL2 z1 M z2)
  obtain x'::name where "x'  (P,M{x:=<a>.P},P{b:=(y).Q},z1,y,Q,M{b:=(y).Q}{x:=<a>.P{b:=(y).Q}})"
    by (meson exists_fresh(1) fs_name1)
  with AndL2 show ?case  
    apply(auto simp: fresh_prod fresh_atm abs_fresh subst_fresh fresh_fun_simp_AndL2)
    by (metis fresh_atm(1) fresh_fun_simp_AndL2 fresh_prod subst_fresh(5))
next
  case (OrL z1 M z2 N z3)
  obtain x'::name where "x'  (P,M{x:=<a>.P},M{b:=(y).Q}{x:=<a>.P{b:=(y).Q}},z2,z3,a,y,Q,
                                     P{b:=(y).Q},N{x:=<a>.P},N{b:=(y).Q}{x:=<a>.P{b:=(y).Q}},z1)"
    by (meson exists_fresh(1) fs_name1)
  with OrL show ?case  
    apply(auto simp: fresh_prod fresh_atm abs_fresh subst_fresh fresh_fun_simp_OrL)
    by (metis (full_types) fresh_atm(1) fresh_fun_simp_OrL fresh_prod subst_fresh(5))
next
  case (OrR1 c1 M c2)
  then show ?case  
    by (auto simp: forget fresh_prod fresh_atm subst_fresh abs_fresh fresh_fun_simp_OrR1)
next
  case (OrR2 c1 M c2)
  then show ?case  
    by (auto simp: forget fresh_prod fresh_atm subst_fresh abs_fresh fresh_fun_simp_OrR2)
next
  case (ImpR z c M d)
  then show ?case  
    by (auto simp: forget fresh_prod fresh_atm subst_fresh abs_fresh fresh_fun_simp_ImpR)
next
  case (ImpL c M z N u)
  obtain z'::name where "z'  (P,P{b:=(y).Q},M{u:=<a>.P},N{u:=<a>.P},y,Q,
                        M{b:=(y).Q}{u:=<a>.P{b:=(y).Q}},N{b:=(y).Q}{u:=<a>.P{b:=(y).Q}},z)"
    by (meson exists_fresh(1) fs_name1)
  with ImpL show ?case  
    apply(auto simp: fresh_prod fresh_atm abs_fresh subst_fresh fresh_fun_simp_ImpL)
    by (metis (full_types) fresh_atm(1) fresh_prod subst_fresh(5) fresh_fun_simp_ImpL)
qed

lemma subst_subst2:
  assumes a: "a(b,P,N)" "x(y,P,M)" "b(M,N)" "yP"
  shows "M{a:=(x).N}{y:=<b>.P} = M{y:=<b>.P}{a:=(x).N{y:=<b>.P}}"
  using a
proof(nominal_induct M avoiding: a x N y b P rule: trm.strong_induct)
  case (Ax z c)
  then show ?case
    by (auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget trm.inject)
next
  case (Cut d M' u M'')
  then show ?case
    apply (clarsimp simp add: abs_fresh fresh_prod fresh_atm subst_fresh)
    apply (metis forget not_Ax1 not_Ax2)
    done
next
  case (NotR z M' d) 
  obtain a'::coname where "a'  (y,P,N,N{y:=<b>.P},M'{d:=(x).N},M'{y:=<b>.P}{d:=(x).N{y:=<b>.P}})"
    by (meson exists_fresh'(2) fs_coname1)
  with NotR show ?case
    apply(simp add: fresh_atm subst_fresh)
    apply(auto simp only: fresh_prod fresh_fun_simp_NotR; simp add: abs_fresh NotR)
    done
next
  case (NotL d M' z) 
  obtain x'::name where "x'  (z,y,P,N,N{y:=<b>.P},M'{y:=<b>.P},M'{y:=<b>.P}{a:=(x).N{y:=<b>.P}})"
    by (meson exists_fresh(1) fs_name1)
  with NotL show ?case  
    apply(simp add: fresh_prod fresh_atm abs_fresh)
    apply(auto simp only: fresh_fun_simp_NotL)
    by (auto simp: subst_fresh abs_fresh fresh_atm forget)
next
  case (AndR d M' e M'' f) 
  obtain a'::coname where "a'  (P,b,d,e,N,N{y:=<b>.P},M'{f:=(x).N},M''{f:=(x).N},
                  M'{y:=<b>.P}{f:=(x).N{y:=<b>.P}},M''{y:=<b>.P}{f:=(x).N{y:=<b>.P}})"
    by (meson exists_fresh'(2) fs_coname1)
  with AndR show ?case
    apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod)
    apply(subgoal_tac "a'::coname. a'(P,b,d,e,N,N{y:=<b>.P},M'{f:=(x).N},M''{f:=(x).N},
                  M'{y:=<b>.P}{f:=(x).N{y:=<b>.P}},M''{y:=<b>.P}{f:=(x).N{y:=<b>.P}})")
     apply(erule exE, simp add: fresh_prod)
     apply(erule conjE)+
     apply(simp add: fresh_fun_simp_AndR)
     apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp)
    apply(rule exists_fresh'(2)[OF fs_coname1])
    done
next
  case (AndL1 z M' u) 
  obtain x'::name where "x'  (P,b,z,u,x,N,M'{y:=<b>.P},M'{y:=<b>.P}{a:=(x).N{y:=<b>.P}})"
    by (meson exists_fresh(1) fs_name1)
  with AndL1 show ?case  
    by (force simp add: fresh_prod fresh_atm fresh_fun_simp_AndL1 subst_fresh abs_fresh forget)
next
  case (AndL2 z M' u) 
  obtain x'::name where "x'  (P,b,z,u,x,N,M'{y:=<b>.P},M'{y:=<b>.P}{a:=(x).N{y:=<b>.P}})"
    by (meson exists_fresh(1) fs_name1)
  with AndL2 show ?case  
    by (force simp add: fresh_prod fresh_atm fresh_fun_simp_AndL2 subst_fresh abs_fresh forget) 
next
  case (OrL u M' v M'' w) 
  obtain x'::name where "x'  (P,b,u,w,v,N,N{y:=<b>.P},M'{y:=<b>.P},M''{y:=<b>.P},
                  M'{y:=<b>.P}{a:=(x).N{y:=<b>.P}},M''{y:=<b>.P}{a:=(x).N{y:=<b>.P}})"
    by (meson exists_fresh(1) fs_name1)
  with OrL show ?case  
    by (force simp add: fresh_prod fresh_atm fresh_fun_simp_OrL subst_fresh abs_fresh forget)
next
  case (OrR1 e M' f) 
  obtain c'::coname where c': "c'  (P,b,e,f,x,N,N{y:=<b>.P},
                                        M'{f:=(x).N},M'{y:=<b>.P}{f:=(x).N{y:=<b>.P}})"
    by (meson exists_fresh(2) fs_coname1)
  with OrR1 show ?case  
    apply (clarsimp simp: fresh_prod fresh_fun_simp_OrR1)
    apply (clarsimp simp: subst_fresh abs_fresh fresh_atm)
    using c' apply (auto simp: fresh_prod fresh_fun_simp_OrR1)
    done
next
  case (OrR2 e M' f) 
  obtain c'::coname where c': "c'  (P,b,e,f,x,N,N{y:=<b>.P},
                                        M'{f:=(x).N},M'{y:=<b>.P}{f:=(x).N{y:=<b>.P}})"
    by (meson exists_fresh(2) fs_coname1)
  with OrR2 show ?case  
    apply (clarsimp simp: fresh_prod fresh_fun_simp_OrR2)
    apply (clarsimp simp: subst_fresh abs_fresh fresh_atm)
    using c' apply (auto simp: fresh_prod fresh_fun_simp_OrR2)
    done
next
  case (ImpR x e M' f) 
  obtain c'::coname where c': "c'  (P,b,e,f,x,N,N{y:=<b>.P},
                                     M'{f:=(x).N},M'{y:=<b>.P}{f:=(x).N{y:=<b>.P}})"
    by (meson exists_fresh(2) fs_coname1)
  with ImpR show ?case  
    apply (clarsimp simp: fresh_prod fresh_fun_simp_ImpR)
    apply (clarsimp simp: subst_fresh abs_fresh fresh_atm)
    using c' apply (auto simp add: abs_fresh abs_supp fin_supp fresh_prod fresh_fun_simp_ImpR)
    done
next
  case (ImpL e M' v M'' w) 
  obtain z'::name where z': "z'  (P,b,e,w,v,N,N{y:=<b>.P},M'{w:=<b>.P},M''{w:=<b>.P},
                  M'{w:=<b>.P}{a:=(x).N{w:=<b>.P}},M''{w:=<b>.P}{a:=(x).N{w:=<b>.P}})"
    by (meson exists_fresh(1) fs_name1)
  with ImpL show ?case  
    by (force simp add: fresh_prod fresh_atm fresh_fun_simp_ImpL subst_fresh abs_fresh forget)
qed

lemma subst_subst3:
  assumes a: "a(P,N,c)" "c(M,N)" "x(y,P,M)" "y(P,x)" "MAx y a"
  shows "N{x:=<a>.M}{y:=<c>.P} = N{y:=<c>.P}{x:=<a>.(M{y:=<c>.P})}"
  using a
proof(nominal_induct N avoiding: x y a c M P rule: trm.strong_induct)
  case (Ax z c)
  then show ?case
    by(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
next
  case (Cut d M' u M'')
  then show ?case
    apply(simp add: fresh_atm fresh_prod trm.inject abs_fresh)
    apply(auto)
       apply(auto simp add: fresh_atm trm.inject forget)
     apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp)
    apply (metis forget(1) not_Ax2)
     apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp)
     apply(rule sym)
     apply(rule trans)
      apply(rule better_Cut_substn)
       apply(simp add: abs_fresh subst_fresh)
      apply(simp add: fresh_prod subst_fresh fresh_atm)
     apply(simp)
    by (metis forget(1) not_Ax2)
next
  case NotR
  then show ?case
    by(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
next
  case (NotL d M' u)
  then show ?case
    apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
     apply(subgoal_tac "x'::name. x'(y,P,M,M{y:=<c>.P},M'{x:=<a>.M},M'{y:=<c>.P}{x:=<a>.M{y:=<c>.P}})")
      apply(erule exE, simp add: fresh_prod)
      apply(erule conjE)+
      apply(simp add: fresh_fun_simp_NotL)
     apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp)
     apply(rule exists_fresh'(1)[OF fs_name1])
    apply(subgoal_tac "x'::name. x'(x,y,P,M,M'{y:=<c>.P},M'{y:=<c>.P}{x:=<a>.M{y:=<c>.P}})")
     apply(erule exE, simp add: fresh_prod)
     apply(erule conjE)+
     apply(simp add: fresh_fun_simp_NotL)
     apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp)
    apply(rule exists_fresh'(1)[OF fs_name1])
    done
next
  case AndR
  then show ?case
    by(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
next
  case (AndL1 u M' v)
  then show ?case
    apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
     apply(subgoal_tac "x'::name. x'(u,y,v,P,M,M{y:=<c>.P},M'{x:=<a>.M},M'{y:=<c>.P}{x:=<a>.M{y:=<c>.P}})")
      apply(erule exE, simp add: fresh_prod)
      apply(erule conjE)+
      apply(simp add: fresh_fun_simp_AndL1)
     apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp)
     apply(rule exists_fresh'(1)[OF fs_name1])
    apply(subgoal_tac "x'::name. x'(x,y,u,v,P,M,M'{y:=<c>.P},M'{y:=<c>.P}{x:=<a>.M{y:=<c>.P}})")
     apply(erule exE, simp add: fresh_prod)
     apply(erule conjE)+
     apply(simp add: fresh_fun_simp_AndL1)
     apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp)
    apply(rule exists_fresh'(1)[OF fs_name1])
    done
next
  case (AndL2 u M' v)
  then show ?case
    apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
     apply(subgoal_tac "x'::name. x'(u,y,v,P,M,M{y:=<c>.P},M'{x:=<a>.M},M'{y:=<c>.P}{x:=<a>.M{y:=<c>.P}})")
      apply(erule exE, simp add: fresh_prod)
      apply(erule conjE)+
      apply(simp add: fresh_fun_simp_AndL2)
     apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp)
     apply(rule exists_fresh'(1)[OF fs_name1])
    apply(subgoal_tac "x'::name. x'(x,y,u,v,P,M,M'{y:=<c>.P},M'{y:=<c>.P}{x:=<a>.M{y:=<c>.P}})")
     apply(erule exE, simp add: fresh_prod)
     apply(erule conjE)+
     apply(simp add: fresh_fun_simp_AndL2)     
     apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp)
    apply(rule exists_fresh'(1)[OF fs_name1])
    done
next
  case OrR1
  then show ?case
    by(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
next
  case OrR2
  then show ?case
    by(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
next
  case (OrL x1 M' x2 M'' x3)
  then show ?case
    apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
     apply(subgoal_tac "x'::name. x'(y,P,M,M{y:=<c>.P},M'{x:=<a>.M},M'{y:=<c>.P}{x:=<a>.M{y:=<c>.P}},
                                      x1,x2,x3,M''{x:=<a>.M},M''{y:=<c>.P}{x:=<a>.M{y:=<c>.P}})")
      apply(erule exE, simp add: fresh_prod)
      apply(erule conjE)+
      apply(simp add: fresh_fun_simp_OrL)
     apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp)
     apply(rule exists_fresh'(1)[OF fs_name1])
    apply(subgoal_tac "x'::name. x'(x,y,P,M,M'{y:=<c>.P},M'{y:=<c>.P}{x:=<a>.M{y:=<c>.P}},
                                      x1,x2,x3,M''{y:=<c>.P},M''{y:=<c>.P}{x:=<a>.M{y:=<c>.P}})")
     apply(erule exE, simp add: fresh_prod)
     apply(erule conjE)+
     apply(simp add: fresh_fun_simp_OrL)
     apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp)
    apply(rule exists_fresh'(1)[OF fs_name1])
    done
next
  case ImpR
  then show ?case
    by(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
next
  case (ImpL d M' x1 M'' x2)
  then show ?case
    apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
     apply(subgoal_tac "x'::name. x'(y,P,M,M{y:=<c>.P},M'{x2:=<a>.M},M'{y:=<c>.P}{x2:=<a>.M{y:=<c>.P}},
                                      x1,x2,M''{x2:=<a>.M},M''{y:=<c>.P}{x2:=<a>.M{y:=<c>.P}})")
      apply(erule exE, simp add: fresh_prod)
      apply(erule conjE)+
      apply(simp add: fresh_fun_simp_ImpL)
     apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp)
     apply(rule exists_fresh'(1)[OF fs_name1])
    apply(subgoal_tac "x'::name. x'(x,y,P,M,M'{x2:=<c>.P},M'{x2:=<c>.P}{x:=<a>.M{x2:=<c>.P}},
                                      x1,x2,M''{x2:=<c>.P},M''{x2:=<c>.P}{x:=<a>.M{x2:=<c>.P}})")
     apply(erule exE, simp add: fresh_prod)
     apply(erule conjE)+
     apply(simp add: fresh_fun_simp_ImpL)
     apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp)
    apply(rule exists_fresh'(1)[OF fs_name1])
    done
qed

lemma subst_subst4:
  assumes a: "x(P,N,y)" "y(M,N)" "a(c,P,M)" "c(P,a)" "MAx x c"
  shows "N{a:=(x).M}{c:=(y).P} = N{c:=(y).P}{a:=(x).(M{c:=(y).P})}"
  using a
proof(nominal_induct N avoiding: x y a c M P rule: trm.strong_induct)
  case (Cut d M' u M'')
  then show ?case
    apply(simp add: fresh_atm fresh_prod trm.inject abs_fresh)
    apply(auto)
       apply(simp add: fresh_atm)
       apply(simp add: trm.inject)
       apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp)
      apply (metis forget(2) not_Ax1)
     apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp)
    apply(rule sym)
    apply(rule trans)
     apply(rule better_Cut_substc)
      apply(simp add: fresh_prod subst_fresh fresh_atm)
     apply(simp add: abs_fresh subst_fresh)
    apply(auto)
    by (metis forget(2) not_Ax1)
next
  case (NotR u M' d)
  then show ?case
    apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
     apply(generate_fresh "coname")
     apply(fresh_fun_simp)
     apply(fresh_fun_simp)
      apply(simp add: abs_fresh subst_fresh)
      apply(simp add: abs_fresh subst_fresh)
     apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp)
    apply(generate_fresh "coname")
    apply(fresh_fun_simp)
    apply(fresh_fun_simp)
     apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp)
    done
next
  case (AndR d M e M' f)
  then show ?case
    apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
     apply(generate_fresh "coname")
     apply(fresh_fun_simp)
     apply(fresh_fun_simp)
      apply(simp add: abs_fresh subst_fresh)
     apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp)
    apply(generate_fresh "coname")
    apply(fresh_fun_simp)
    apply(fresh_fun_simp)
     apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp)
    done
next
  case (OrR1 d M' e)
  then show ?case
    apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
     apply(generate_fresh "coname")
     apply(fresh_fun_simp)
     apply(fresh_fun_simp)
      apply(simp add: abs_fresh subst_fresh)
     apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp)
    apply(generate_fresh "coname")
    apply(fresh_fun_simp)
    apply(fresh_fun_simp)
     apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp)
    done
next
  case (OrR2 d M' e)
  then show ?case
    apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
     apply(generate_fresh "coname")
     apply(fresh_fun_simp)
     apply(fresh_fun_simp)
      apply(simp add: abs_fresh subst_fresh)
     apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp)
    apply(generate_fresh "coname")
    apply(fresh_fun_simp)
    apply(fresh_fun_simp)
     apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp)
    done
next
  case (ImpR u d M' e)
  then show ?case
    apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
      apply(generate_fresh "coname")
      apply(fresh_fun_simp)
      apply(fresh_fun_simp)
      apply(simp add: abs_fresh subst_fresh)
     apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp)
    apply(generate_fresh "coname")
    apply(fresh_fun_simp)
    apply(fresh_fun_simp)
     apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp)+
    done
qed (auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)


end