Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


Quelle  Class1.thy

  Sprache: Isabelle
 

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)[dc>e] = (if a=d then Ax x e else Ax x a)" 
"[a(d,e,N);xM] ==> (Cut .M (x).N)[dc>e] = Cut .(M[dc>e]) (x).(N[dc>e])" 
"(NotR (x).M a)[dc>e] = (if a=d then NotR (x).(M[dc>e]) e else NotR (x).(M[dc>e]) a)" 
"a(d,e) ==> (NotL
.M x)[dc>e] = (NotL .(M[dc>e]) x)" 
"[a(d,e,N,c);b(d,e,M,c);ba] ==> (AndR
.M .N c)[dc>e] =
          (if c=d then AndR
.(M[dc>e]) .(N[d c>e]) e else AndR .(M[dc>e]) .(N[dc>e]) c)" 
"xy ==> (AndL1 (x).M y)[dc>e] = AndL1 (x).(M[dc>e]) y"
"xy ==> (AndL2 (x).M y)[dc>e] = AndL2 (x).(M[dc>e]) y"
"a(d,e,b) ==> (OrR1
.M b)[dc>e] = (if b=d then OrR1 .(M[dc>e]) e else OrR1 .(M[dc>e]) b)"
"a(d,e,b) ==> (OrR2
.M b)[dc>e] = (if b=d then OrR2 .(M[dc>e]) e else OrR2 .(M[dc>e]) b)"
"[x(N,z);y(M,z);yx] ==> (OrL (x).M (y).N z)[dc>e] = OrL (x).(M[dc>e]) (y).(N[dc>e]) z"
"a(d,e,b) ==> (ImpR (x).
.M b)[dc>e] =
       (if b=d then ImpR (x).
.(M[dc>e]) e else ImpR (x)..(M[dc>e]) b)"
"[a(d,e,N);x(M,y)] ==> (ImpL
.M (x).N y)[dc>e] = ImpL .(M[dc>e]) (x).(N[dc>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)[un>v] = (if x=u then Ax v a else Ax x a)" 
"[aN;x(u,v,M)] ==> (Cut
.M (x).N)[un>v] = Cut .(M[un>v]) (x).(N[un>v])" 
"x(u,v) ==> (NotR (x).M a)[un>v] = NotR (x).(M[un>v]) a" 
"(NotL
.M x)[un>v] = (if x=u then NotL .(M[un>v]) v else NotL .(M[un>v]) x)" 
"[a(N,c);b(M,c);ba] ==> (AndR
.M .N c)[un>v] = AndR .(M[un>v]) .(N[un>v]) c" 
"x(u,v,y) ==> (AndL1 (x).M y)[un>v] = (if y=u then AndL1 (x).(M[un>v]) v else AndL1 (x).(M[un>v]) y)"
"x(u,v,y) ==> (AndL2 (x).M y)[un>v] = (if y=u then AndL2 (x).(M[un>v]) v else AndL2 (x).(M[un>v]) y)"
"ab ==> (OrR1
.M b)[un>v] = OrR1 .(M[un>v]) b"
"ab ==> (OrR2
.M b)[un>v] = OrR2 .(M[un>v]) b"
"[x(u,v,N,z);y(u,v,M,z);yx] ==> (OrL (x).M (y).N z)[un>v] =
        (if z=u then OrL (x).(M[un>v]) (y).(N[un>v]) v else OrL (x).(M[un>v]) (y).(N[un>v]) z)"
"[ab; x(u,v)] ==> (ImpR (x).
.M b)[un>v] = ImpR (x)..(M[un>v]) b"
"[aN;x(u,v,M,y)] ==> (ImpL
.M (x).N y)[un>v] =
        (if y=u then ImpL
.(M[un>v]) (x).(N[un>v]) v else ImpL .(M[un>v]) (x).(N[un>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[dc>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[dc>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[xn>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[xn>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[xn>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[ac>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 "xy==>xM[xn>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 "xM==>xM[ac>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 "ab==>aM[ac>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 "cM==>cM[xn>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[zn>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[bc>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[xn>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[ac>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
.M (x).N)[un>v] = Cut .(M[un>v]) (x).(N[un>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
.M (x).N) = (Cut .([(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)]M) (x').([(x',x)]N))[un>v] =
                        Cut .(([(a',a)]M)[un>v]) (x').(([(x',x)]N)[un>v])"
    using fs1 fs2
    by (intro nrename.simps; simp add: fresh_left calc_atm)
  also have " = Cut
.(M[un>v]) (x).(N[un>v])" using fs1 fs2 a
    by(simp add: trm.inject alpha fresh_prod rename_eqvts calc_atm rename_fresh fresh_atm)
  finally show "(Cut
.M (x).N)[un>v] = Cut .(M[un>v]) (x).(N[un>v])" using eq1
    by simp
qed

lemma better_crename_Cut:
  assumes a: "a(b,c)"
  shows "(Cut
.M (x).N)[bc>c] = Cut .(M[bc>c]) (x).(N[bc>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
.M (x).N) = (Cut .([(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)]M) (x').([(x',x)]N))[bc>c] =
                        Cut .(([(a',a)]M)[bc>c]) (x').(([(x',x)]N)[bc>c])"
    using fs1 fs2
    by (intro crename.simps; simp add: fresh_left calc_atm)
  also have " = Cut
.(M[bc>c]) (x).(N[bc>c])" using fs1 fs2 a
    by(simp add: trm.inject alpha calc_atm rename_fresh fresh_atm fresh_prod rename_eqvts)
  finally show "(Cut
.M (x).N)[bc>c] = Cut .(M[bc>c]) (x).(N[bc>c])" using eq1
    by simp
qed

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

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

lemma nrename_swap:
  shows "xM ==> [(x,y)]M = M[yn>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[bc>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[ac>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[xn>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 .P (x').NotL
.M x') = Cut .P (x').NotL .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 .P (x').NotL
.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 .P (x').NotL
.M x')"
    by (fresh_guess)
  then show "b. b (λx'. Cut .P (x').NotL
.M x', Cut .P (b).NotL .M b)"
    by (metis abs_fresh(1) abs_fresh(5) fresh_prod n trm.fresh(3))
  show "x' (λx'. Cut .P (x').NotL
.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 .P (x').NotL
.M x')=
             fresh_fun (pi1(λx'. Cut .P (x').NotL
.M x'))"
  and   "pi2fresh_fun (λx'. Cut .P (x').NotL
.M x')=
             fresh_fun (pi2(λx'. Cut .P (x').NotL
.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 .P(z').AndL1 (x).M z') = Cut .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 .P(z').AndL1 x. M z', Cut .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 .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 .P (z').AndL1 (x).M z')=
             fresh_fun (pi1(λz'. Cut .P (z').AndL1 (x).M z'))"
  and   "pi2fresh_fun (λz'. Cut .P (z').AndL1 (x).M z')=
             fresh_fun (pi2(λz'. Cut .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 .P (z').AndL2 (x).M z') = Cut .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 .P(z').AndL2 x. M z', Cut .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 .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 .P (z').AndL2 (x).M z')=
             fresh_fun (pi1(λz'. Cut .P (z').AndL2 (x).M z'))"
  and   "pi2fresh_fun (λz'. Cut .P (z').AndL2 (x).M z')=
             fresh_fun (pi2(λz'. Cut .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 .P(z').OrL(x).M(u).N z') = Cut .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 .P(z').OrL(x).M(u).N(z'), Cut .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 .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 .P(z').OrL (x).M(u).N z')=
             fresh_fun (pi1(λz'. Cut .P (z').OrL(x).M (u).N z'))"
  and   "pi2fresh_fun (λz'. Cut .P(z').OrL (x).M(u).N z')=
             fresh_fun (pi2(λz'. Cut .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 .P (z').ImpL
.M (x).N z') = Cut .P (z').ImpL .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 .P(z').ImpL
.M(x).N z', Cut .P(aa).ImpL .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 .P(z').ImpL
.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 .P (z').ImpL
.M (x).N z')=
             fresh_fun (pi1(λz'. Cut .P (z').ImpL
.M (x).N z'))"
  and   "pi2fresh_fun (λz'. Cut .P (z').ImpL
.M (x).N z')=
             fresh_fun (pi2(λz'. Cut .P (z').ImpL
.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 .(NotR (y).M a') (x).P) = Cut .(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 .(NotR (y).M a') (x).P, Cut
.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 .(NotR (y).M a') (x).P)=
             fresh_fun (pi1(λa'. Cut .(NotR (y).M a') (x).P))"
  and   "pi2fresh_fun (λa'. Cut .(NotR (y).M a') (x).P)=
             fresh_fun (pi2(λa'. Cut .(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 .(AndR .M .N a') (x).P) = Cut .(AndR .M .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 .AndR .M .N(a') (x).P, Cut
.AndR .M .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 .(AndR .M .N a') (x).P)=
             fresh_fun (pi1(λa'. Cut .(AndR .M .N a') (x).P))"
  and   "pi2fresh_fun (λa'. Cut .(AndR .M .N a') (x).P)=
             fresh_fun (pi2(λa'. Cut .(AndR .M .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 .(OrR1 .M a') (x).P) = Cut .(OrR1 .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 .OrR1 .M(a') (x).P, Cut
.OrR1 .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 .(OrR1 .M a') (x).P) =
             fresh_fun (pi1(λa'. Cut .(OrR1 .M a') (x).P))" (is "?t1")
  and   "pi2fresh_fun (λa'. Cut .(OrR1 .M a') (x).P) =
             fresh_fun (pi2(λa'. Cut .(OrR1 .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 .(OrR2 .M a') (x).P) = Cut .(OrR2 .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 .OrR2 .M(a') (x).P, Cut
.OrR2 .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 .(OrR2 .M a') (x).P) =
             fresh_fun (pi1(λa'. Cut .(OrR2 .M a') (x).P))" (is "?t1")
  and   "pi2fresh_fun (λa'. Cut .(OrR2 .M a') (x).P) =
             fresh_fun (pi2(λa'. Cut .(OrR2 .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 .(ImpR (y)..M a') (x).P) = Cut .(ImpR (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,b,M)"
    by (meson exists_fresh(2) fs_coname1)
  then show "a. a (λa'. Cut .(ImpR (y)..M a') (x).P, Cut
.(ImpR (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_ImpR[eqvt_force]:
  fixes pi1::"name prm"
  and   pi2::"coname prm"
  shows "pi1fresh_fun (λa'. Cut .(ImpR (y)..M a') (x).P) =
             fresh_fun (pi1(λa'. Cut .(ImpR (y)..M a') (x).P))" (is "?t1")
  and   "pi2fresh_fun (λa'. Cut .(ImpR (y)..M a') (x).P)=
             fresh_fun (pi2(λa'. Cut .(ImpR (y)..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:=.P} = (if x=y then Cut .P (y).Ax y a else Ax x a)" 
"[a(c,P,N);x(y,P,M)] ==> (Cut
.M (x).N){y:=.P} =
  (if M=Ax y a then Cut .P (x).(N{y:=.P}) else Cut
.(M{y:=.P}) (x).(N{y:=.P}))" 
"x(y,P) ==> (NotR (x).M a){y:=.P} = NotR (x).(M{y:=.P}) a" 
"a(c,P) ==> (NotL
.M x){y:=.P} =
  (if x=y then fresh_fun (λx'. Cut .P (x').NotL
.(M{y:=.P}) x') else NotL .(M{y:=.P}) x)"
"[a(c,P,N,d);b(c,P,M,d);ba] ==>
  (AndR
.M .N d){y:=.P} = AndR .(M{y:=.P}) .(N{y:=.P}) d" 
"x(y,P,z) ==> (AndL1 (x).M z){y:=.P} =
  (if z=y then fresh_fun (λz'. Cut .P (z').AndL1 (x).(M{y:=.P}) z')
   else AndL1 (x).(M{y:=.P}) z)"
"x(y,P,z) ==> (AndL2 (x).M z){y:=.P} =
  (if z=y then fresh_fun (λz'. Cut .P (z').AndL2 (x).(M{y:=.P}) z')
   else AndL2 (x).(M{y:=.P}) z)"
"a(c,P,b) ==> (OrR1
.M b){y:=.P} = OrR1 .(M{y:=.P}) b"
"a(c,P,b) ==> (OrR2
.M b){y:=.P} = OrR2 .(M{y:=.P}) b"
"[x(y,N,P,z);u(y,M,P,z);xu] ==> (OrL (x).M (u).N z){y:=.P} =
  (if z=y then fresh_fun (λz'. Cut .P (z').OrL (x).(M{y:=.P}) (u).(N{y:=.P}) z')
   else OrL (x).(M{y:=.P}) (u).(N{y:=.P}) z)"
"[a(b,c,P); x(y,P)] ==> (ImpR (x).
.M b){y:=.P} = ImpR (x)..(M{y:=.P}) b"
"[a(N,c,P);x(y,P,M,z)] ==> (ImpL
.M (x).N z){y:=.P} =
  (if y=z then fresh_fun (λz'. Cut .P (z').ImpL
.(M{y:=.P}) (x).(N{y:=.P}) z')
   else ImpL
.(M{y:=.P}) (x).(N{y:=.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
.(Ax x a) (z).P else Ax x a)" 
"[a(d,P,N);x(z,P,M)] ==> (Cut
.M (x).N){d:=(z).P} =
  (if N=Ax x d then Cut
.(M{d:=(z).P}) (z).P else Cut .(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 .NotR (x).(M{d:=(z).P}) a' (z).P) else NotR (x).(M{d:=(z).P}) a)" 
"a(d,P) ==> (NotL
.M x){d:=(z).P} = NotL .(M{d:=(z).P}) x" 
"[a(P,c,N,d);b(P,c,M,d);ba] ==> (AndR
.M .N c){d:=(z).P} =
  (if d=c then fresh_fun (λa'. Cut .(AndR
.(M{d:=(z).P}) .(N{d:=(z).P}) a') (z).P)
   else AndR
.(M{d:=(z).P}) .(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
.M b){d:=(z).P} =
  (if d=b then fresh_fun (λa'. Cut .OrR1
.(M{d:=(z).P}) a' (z).P) else OrR1 .(M{d:=(z).P}) b)"
"a(d,P,b) ==> (OrR2
.M b){d:=(z).P} =
  (if d=b then fresh_fun (λa'. Cut .OrR2
.(M{d:=(z).P}) a' (z).P) else OrR2 .(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).
.M b){d:=(z).P} =
  (if d=b then fresh_fun (λa'. Cut .ImpR (x).
.(M{d:=(z).P}) a' (z).P)
   else ImpR (x).
.(M{d:=(z).P}) b)"
"[a(N,d,P);x(y,z,P,M)] ==> (ImpL
.M (x).N y){d:=(z).P} =
  ImpL
.(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:=.N}) = (pi1M){(pi1x):=<(pi1c)>.(pi1N)}"
  and   "pi2(M{x:=.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:=.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:=.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:=.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:=.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:=.P},P,name1,trm2{y:=.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:=.P},P,name1,trm2{name2:=.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:=.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:=.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:=.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:=.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:=.P},P,name1,trm2{y:=.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:=.P},P,name1,trm2{name2:=.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:=.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:=.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:=.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:=.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:=.P},P,name1,trm2{y:=.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:=.P},P,name1,trm2{name2:=.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:=.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:=.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:=.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:=.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:=.P},P,name1,trm2{y:=.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:=.P},P,name1,trm2{name2:=.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:=.P}"   
  and   "bP ==> bM{b:=(y).P}"
  and   "x(M,P) ==> xM{y:=.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:=.P}"
  and   "b(M,P) ==> bM{y:=.P}"
  using subst_supp
  by(fastforce simp add: fresh_def supp_prod)+

lemma forget:
  shows "xM ==> M{x:=.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:=
.N} = ([(y,x)]M){y:=.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:=
.N} = M{x:=.([(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,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,a)]N)},M'{x:=.([(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,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,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,a)]N)},M'{u:=.([(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:=.N} = ([(x',x)]M){x':=.([(c',c)]N)}"
proof -
  have "M{x:=.N} = ([(x',x)]M){x':=.N}" using a by (simp add: substn_rename3)
  also have " = ([(x',x)]M){x':=.([(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
.M (x).N){y:=.P} =
  (if M=Ax y a then Cut .P (x).(N{y:=.P}) else Cut
.(M{y:=.P}) (x).(N{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
.M (x).N) = (Cut .([(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
.M (x).N){y:=.P} = (Cut .([(a',a)]M) (x').([(x',x)]N)){y:=.P}" 
    using eq1 by simp
  also have " = (if ([(a',a)]M)=Ax y a' then Cut .P (x').(([(x',x)]N){y:=.P})
                              else Cut .(([(a',a)]M){y:=.P}) (x').(([(x',x)]N){y:=.P}))" 
    using fs1 fs2 by (auto simp: fresh_prod fresh_left calc_atm fresh_atm)
  also have " =(if M=Ax y a then Cut .P (x).(N{y:=.P}) else Cut
.(M{y:=.P}) (x).(N{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)
    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
.M (x).N){c:=(y).P} =
  (if N=Ax x c then Cut
.(M{c:=(y).P}) (y).P else Cut .(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
.M (x).N) = (Cut .([(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
.M (x).N){c:=(y).P} = (Cut .([(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)]M){c:=(y).P}) (y).P
                              else Cut .(([(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
.(M{c:=(y).P}) (y).P else Cut .(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
.M (x).N){y:=.P} = Cut .(M{y:=.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
.M (x).N = Cut .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 .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
.M y){y:=.P} = fresh_fun (λx'. Cut .P (x').NotL .M x')"
proof (generate_fresh "coname")
  fix ca :: coname
  assume d: "ca (M, P, a, c, y)"
  then have "NotL
.M y = NotL .([(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:=.P} = fresh_fun (λz'. Cut .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 .P (z').AndL1 (d).([(d, x)] M){x:=.P} (z'))
             = (λz'. Cut .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 .P (z').AndL1 d.([(d, x)] M){y:=.P} z')
             = (λz'. Cut .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:=.P} = fresh_fun (λz'. Cut .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 .P (z').AndL2 (d).([(d, x)] M){x:=.P} (z'))
             = (λz'. Cut .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 .P (z').AndL2 d.([(d, x)] M){y:=.P} z')
             = (λz'. Cut .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
.M .N c){c:=(z).P} = fresh_fun (λa'. Cut .(AndR .M .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
.M .N c = AndR .([(d,a)]M) .([(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:=.P} = fresh_fun (λz'. Cut .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
.M d){d:=(z).P} = fresh_fun (λa'. Cut .OrR1 .M a' (z).P)"
proof (generate_fresh "coname")
  fix c :: coname
  assume c: "c (M, P, a, d, z)"
  then have "OrR1
.M d = OrR1 .([(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
.M d){d:=(z).P} = fresh_fun (λa'. Cut .OrR2 .M a' (z).P)"
proof (generate_fresh "coname")
  fix c :: coname
  assume c: "c (M, P, a, d, z)"
  then have "OrR2
.M d = OrR2 .([(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).
.M d){d:=(z).P} = fresh_fun (λa'. Cut .ImpR (x)..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).
.M d = ImpR (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 .ImpR (c')..(([(c, a)] [(c', x)] M)){d:=(z).P} a' (z).P)
      = fresh_fun (λa'. Cut .ImpR (x).
.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
.M (x).N y){y:=.P} = fresh_fun (λz'. Cut .P (z').ImpL .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
.M (x).N y = ImpL .([(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:=.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:=.P}" 
  shows "aM"
  by (meson assms fresh_def subset_iff supp_subst6)

lemma substn_crename_comm:
  assumes "ca" "cb"
  shows "M{x:=.P}[ac>b] = M[ac>b]{x:=.(P[ac>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:=.P},P,P[ac>b],x,trm[ac>b]{x:=.P[ac>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:=.P},P,P[ac>b],name1,trm[ac>b]{x:=.P[ac>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:=.P},P,P[ac>b],name1,trm[ac>b]{x:=.P[ac>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:=.P},trm2{x:=.P},P,P[ac>b],name1,name2,
                                  trm1[ac>b]{x:=.P[ac>b]},trm2[ac>b]{x:=.P[ac>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:=.P},trm2{x:=.P},P,P[ac>b],name1,name2,
                                  trm1[ac>b]{x:=.P[ac>b]},trm2[ac>b]{x:=.P[ac>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}[ac>b] = M[ac>b]{c:=(x).(P[ac>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[ac>b],x,trm[ac>b]{coname:=(x).P[ac>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[ac>b],x,trm1[ac>b]{coname3:=(x).P[ac>b]},trm2[ac>b]{coname3:=(x).P[ac>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[ac>b],a,b, trm[ac>b]{coname2:=(x).P[ac>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[ac>b],a,b, trm[ac>b]{coname2:=(x).P[ac>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[ac>b],a,b, trm[ac>b]{coname2:=(x).P[ac>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:=.P}[yn>z] = M[yn>z]{x:=.(P[yn>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:=.P},P,P[yn>z],x,trm[yn>z]{x:=.P[yn>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:=.P},P,P[yn>z],name1,trm[yn>z]{x:=.P[yn>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:=.P},P,P[yn>z],name1,trm[yn>z]{x:=.P[yn>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:=.P},trm2{x:=.P},P,P[yn>z],name1,name2,y,z,
                                  trm1[yn>z]{x:=.P[yn>z]},trm2[yn>z]{x:=.P[yn>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:=.P},trm2{x:=.P},P,P[yn>z],name1,name2,y,z,
                                  trm1[yn>z]{x:=.P[yn>z]},trm2[yn>z]{x:=.P[yn>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}[yn>z] = M[yn>z]{c:=(x).(P[yn>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[yn>z],x,trm[yn>z]{coname:=(x).P[yn>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[yn>z],x,trm1[yn>z]{coname3:=(x).P[yn>z]},trm2[yn>z]{coname3:=(x).P[yn>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[yn>z],y,z,
                         trm[yn>z]{coname2:=(x).P[yn>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[yn>z],y,z,
                         trm[yn>z]{coname2:=(x).P[yn>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[yn>z],y,z,
                         trm[yn>z]{coname2:=(x).P[yn>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:=.P}[ac>b] = M[ac>b]{x:=.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:=.P} = M{x:=.([(c',c)]P)}"
    using fs2 substn_rename4 by force
   have eq': "M[ac>b]{x:=.P} = M[ac>b]{x:=.([(c',c)]P)}"
    using fs2 by (simp add: substn_rename4)
  have eq2: "([(c',c)]P)[ac>b] = ([(c',c)]P)" using fs2 assms
    by (metis crename_fresh fresh_atm(2) fresh_aux(2) fresh_prod)
  have "M{x:=.P}[ac>b] = M{x:=.([(c',c)]P)}[ac>b]" using eq by simp
  also have " = M[ac>b]{x:=.(([(c',c)]P)[ac>b])}"
    using fs2
    by (simp add: fresh_atm(2) fresh_prod substn_crename_comm)
  also have " = M[ac>b]{x:=.(([(c',c)]P))}" using eq2 by simp
  also have " = M[ac>b]{x:=.P}" using eq' by simp 
  finally show ?thesis by simp
qed

lemma substc_crename_comm':
  assumes "ca" "cb" "aP"
  shows "M{c:=(x).P}[ac>b] = M[ac>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[ac>b])){c':=(x).P} = M[ac>b]{c:=(x).P}"
    using fs2 by (metis crename_cfresh' fresh_prod substc_rename1)
  have eq2: "([(c',c)]M)[ac>b] = ([(c',c)](M[ac>b]))" using fs2 assms
    by (simp add: crename_coname_eqvt fresh_atm(2) fresh_prod swap_simps(6))
  have "M{c:=(x).P}[ac>b] = ([(c',c)]M){c':=(x).P}[ac>b]" using eq by simp
  also have " = ([(c',c)]M)[ac>b]{c':=(x).P[ac>b]}"
    using fs2 assms
    by (metis crename_fresh eq eq' eq2 substc_crename_comm)
  also have " = ([(c',c)](M[ac>b])){c':=(x).P[ac>b]}" using eq2 by simp
  also have " = ([(c',c)](M[ac>b])){c':=(x).P}" 
    using assms by (simp add: rename_fresh)
  also have " = M[ac>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:=.P}[yn>z] = M[yn>z]{x:=.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:=.P} = ([(x',x)]M){x':=.P}"
    using fs2 by (simp add: substn_rename3)
   have eq': "([(x',x)](M[yn>z])){x':=.P} = M[yn>z]{x:=.P}"
    using fs2 by (metis fresh_prod nrename_nfresh' substn_rename3)
  have eq2: "([(x',x)]M)[yn>z] = ([(x',x)](M[yn>z]))" 
    using fs2 by (simp add: assms fresh_atm(1) fresh_prod nrename_name_eqvt swap_simps(5)) 
  have "M{x:=.P}[yn>z] = ([(x',x)]M){x':=.P}[yn>z]" using eq by simp
  also have " = ([(x',x)]M)[yn>z]{x':=.P[yn>z]}"
    using fs2 by (metis assms eq eq' eq2 nrename_fresh substn_nrename_comm)
  also have " = ([(x',x)](M[yn>z])){x':=.P[yn>z]}" using eq2 by simp
  also have " = ([(x',x)](M[yn>z])){x':=.P}" using assms by (simp add: rename_fresh)
  also have " = M[yn>z]{x:=.P}" using eq' by simp
  finally show ?thesis by simp
qed

lemma substc_nrename_comm':
  assumes "xy" "yP"
  shows "M{c:=(x).P}[yn>z] = M[yn>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[yn>z]{c:=(x).P} = M[yn>z]{c:=(x').([(x',x)]P)}"
    using fs2 by (simp add: substc_rename2)
  have eq2: "([(x',x)]P)[yn>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}[yn>z] = M{c:=(x').([(x',x)]P)}[yn>z]" using eq by simp
  also have " = M[yn>z]{c:=(x').(([(x',x)]P)[yn>z])}"
    using fs2 by (simp add: fresh_atm(1) fresh_prod substc_nrename_comm)
  also have " = M[yn>z]{c:=(x').(([(x',x)]P))}" using eq2 by simp
  also have " = M[yn>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
.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
.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
.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
.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
.M (x).N) y ==> False"
  and   "fin (NotR (x).M c) y ==> False"
  and   "fin (AndR
.M .N c) y ==> False"
  and   "fin (OrR1
.M b) y ==> False"
  and   "fin (OrR2
.M b) y ==> False"
  and   "fin (ImpR (x).
.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:=.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:=.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:=.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:=.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:=.P},trm2{y:=.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:=.P},trm2{name2:=.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:=.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[xn>y]{y:=.P} = Cut .P (x).(M{y:=.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[xn>y]{y:=.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[name2n>y]{y:=.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[name2n>y]{y:=.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[name3n>y]{y:=.P},trm2[name3n>y]{y:=.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[xn>y]{y:=.P},trm2[xn>y]{y:=.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
.M .N c) c"
| [intro]: "b[a].M ==> fic (OrR1
.M b) b"
| [intro]: "b[a].M ==> fic (OrR2
.M b) b"
| [intro]: "[b[a].M] ==> fic (ImpR (x).
.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
.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
.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
.M .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).
.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
.M (x).N) d ==> False"
  and   "fic (NotL
.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
.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:=.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:=.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:=.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:=.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:=.P},trm2{y:=.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:=.P},trm2{name2:=.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:=.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[ac>b]{b:=(y).P} = Cut
.(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
.M (x).(Ax x b) 🪙l M[ac>b]"
| LAxL:  "[aM; xy; fin M x] ==> Cut
.(Ax y a) (x).M 🪙l M[xn>y]"
| LNot:  "[y(M,N); x(N,y); a(M,N,b); bM; yx; ba] ==>
          Cut
.(NotR (x).M a) (y).(NotL .N y) 🪙l Cut .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 .(AndR .M1 .M2 b) (y).(AndL1 (x).N y) 🪙l Cut .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 .(AndR .M1 .M2 b) (y).(AndL2 (x).N y) 🪙l Cut .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 .(OrR1
.M b) (y).(OrL (x1).N1 (x2).N2 y) 🪙l Cut .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 .(OrR2
.M b) (y).(OrL (x1).N1 (x2).N2 y) 🪙l Cut .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 .(ImpR (x).
.M b) (z).(ImpL .N (y).P z) 🪙l Cut .(Cut .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
.M (x).(Ax x b) 🪙l M[ac>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
.M (x).(Ax x b) = Cut .([(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[ac>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
.(Ax y a) (x).M 🪙l M[xn>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
.(Ax y a) (x).M = Cut .(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[xn>y]" using fs1 fs2 by (simp add: nrename_rename)
  finally show ?thesis by simp
qed

lemma better_LNot_intro[intro]:
  shows "[yN; aM] ==> Cut
.(NotR (x).M a) (y).(NotL .N y) 🪙l Cut .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
.(NotR (x).M a) (y).(NotL .N y)
                      = Cut .(NotR (x).([(a',a)]M) a') (y').(NotL .([(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 .(NotR (x).M a') (y').(NotL .N y')"
    using f1 f2 f3 f4 fs by (perm_simp)
  also have " = Cut .(NotR (x').([(x',x)]M) a') (y').(NotL .([(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)]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 .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
.(AndR .M1 .M2 a) (y).(AndL1 (x).N y) 🪙l Cut .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
.(AndR .M1 .M2 a) (y).(AndL1 (x).N y)
                      = Cut .(AndR .M1 .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 .(AndR .([(b1',b1)]M1) .([(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)]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 .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
.(AndR .M1 .M2 a) (y).(AndL2 (x).N y) 🪙l Cut .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
.(AndR .M1 .M2 a) (y).(AndL2 (x).N y)
                      = Cut .(AndR .M1 .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 .(AndR .([(b1',b1)]M1) .([(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)]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 .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 .(OrR1
.M b) (y).(OrL (x1).N1 (x2).N2 y) 🪙l Cut .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 .(OrR1
.M b) (y).(OrL (x1).N1 (x2).N2 y)
                      = Cut .(OrR1
.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 .(OrR1 .([(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)]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
.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 .(OrR2
.M b) (y).(OrL (x1).N1 (x2).N2 y) 🪙l Cut .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 .(OrR2
.M b) (y).(OrL (x1).N1 (x2).N2 y)
                      = Cut .(OrR2
.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 .(OrR2 .([(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)]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
.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 .(ImpR (x).
.M b) (z).(ImpL .N (y).P z) 🪙l Cut .(Cut .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 .(ImpR (x).
.M b) (z).(ImpL .N (y).P z)
                      = Cut .(ImpR (x).
.M b') (z').(ImpL .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 .(ImpR (x')..([(a',a)]([(x',x)]M)) b')
                           (z').(ImpL .([(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 .(Cut .([(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
.(Cut .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
.M (x).N 🪙l R"
  shows "(b. R = M[ac>b]) (y. R = N[xn>y])
  (y M' b N'. M = NotR (y).M' a N = NotL .N' x R = Cut .N' (y).M' fic M a fin N x)
  (b M1 c M2 y N'. M = AndR .M1 .M2 a N = AndL1 (y).N' x R = Cut .M1 (y).N'
                                                                             fic M a fin N x)
  (b M1 c M2 y N'. M = AndR .M1 .M2 a N = AndL2 (y).N' x R = Cut .M2 (y).N'
                                                                             fic M a fin N x)
  (b N' z M1 y M2. M = OrR1 .N' a N = OrL (z).M1 (y).M2 x R = Cut .N' (z).M1
                                                                             fic M a fin N x)
  (b N' z M1 y M2. M = OrR2 .N' a N = OrL (z).M1 (y).M2 x R = Cut .N' (y).M2
                                                                             fic M a fin N x)
  (z b M' c N1 y N2. M = ImpR (z)..M' a N = ImpL .N1 (y).N2 x
            R = Cut .(Cut .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
.M (x).N 🪙c M{a:=(x).N}"
| right[intro]: "[¬fin N x; aN; xM] ==> Cut
.M (x).N 🪙c N{x:=.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
.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
.M (x).N = Cut .([(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
.M (x).N 🪙c N{x:=.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
.M (x).N = Cut .([(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)]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:=
.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]: "M🪙l M' ==> M 🪙a M'"
| ac_redu[intro]: "M🪙c M' ==> M 🪙a M'"
| a_Cut_l: "[aN; xM; M🪙a M'] ==> Cut
.M (x).N 🪙a Cut .M' (x).N"
| a_Cut_r: "[aN; xM; N🪙a N'] ==> Cut
.M (x).N 🪙a Cut .M (x).N'"
| a_NotL[intro]: "M🪙a M' ==> NotL
.M x 🪙a NotL .M' x"
| a_NotR[intro]: "M🪙a M' ==> NotR (x).M a 🪙a NotR (x).M' a"
| a_AndR_l: "[a(N,c); b(M,c); ba; M🪙a M'] ==> AndR
.M .N c 🪙a AndR .M' .N c"
| a_AndR_r: "[a(N,c); b(M,c); ba; N🪙a N'] ==> AndR
.M .N c 🪙a AndR .M .N' c"
| a_AndL1: "[xy; M🪙a M'] ==> AndL1 (x).M y 🪙a AndL1 (x).M' y"
| a_AndL2: "[xy; M🪙a M'] ==> AndL2 (x).M y 🪙a AndL2 (x).M' y"
| a_OrL_l: "[x(N,z); y(M,z); yx; M🪙a M'] ==> OrL (x).M (y).N z 🪙a OrL (x).M' (y).N z"
| a_OrL_r: "[x(N,z); y(M,z); yx; N🪙a N'] ==> OrL (x).M (y).N z 🪙a OrL (x).M (y).N' z"
| a_OrR1: "[ab; M🪙a M'] ==> OrR1
.M b 🪙a OrR1 .M' b"
| a_OrR2: "[ab; M🪙a M'] ==> OrR2
.M b 🪙a OrR2 .M' b"
| a_ImpL_l: "[aN; x(M,y); M🪙a M'] ==> ImpL
.M (x).N y 🪙a ImpL .M' (x).N y"
| a_ImpL_r: "[aN; x(M,y); N🪙a N'] ==> ImpL
.M (x).N y 🪙a ImpL .M (x).N' y"
| a_ImpR: "[ab; M🪙a M'] ==> ImpR (x).
.M b 🪙a ImpR (x)..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 "M🪙a M' ==> Cut
.M (x).N 🪙a Cut .M' (x).N"
proof -
  assume red: "M🪙a 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
.M (x).N = Cut .([(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)]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
.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 "N🪙a N' ==> Cut
.M (x).N 🪙a Cut .M (x).N'"
proof -
  assume red: "N🪙a 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
.M (x).N = Cut .([(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)]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
.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 "M🪙a M' ==> AndR
.M .N c 🪙a AndR .M' .N c"
proof -
  assume red: "M🪙a 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
.M .N c = AndR .([(a',a)]M) .([(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)]M') .([(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
.M' .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 "N🪙a N' ==> AndR
.M .N c 🪙a AndR .M .N' c"
proof -
  assume red: "N🪙a 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
.M .N c = AndR .([(a',a)]M) .([(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)]M) .([(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
.M .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 "M🪙a M' ==> AndL1 (x).M y 🪙a AndL1 (x).M' y"
proof -
  assume red: "M🪙a 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 "M🪙a M' ==> AndL2 (x).M y 🪙a AndL2 (x).M' y"
proof -
  assume red: "M🪙a 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 "M🪙a M' ==> OrL (x).M (y).N z 🪙a OrL (x).M' (y).N z"
proof -
  assume red: "M🪙a 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 "N🪙a N' ==> OrL (x).M (y).N z 🪙a OrL (x).M (y).N' z"
proof -
  assume red: "N🪙a 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 "M🪙a M' ==> OrR1
.M b 🪙a OrR1 .M' b"
proof -
  assume red: "M🪙a M'"
  obtain a'::"coname" where fs1: "a'(M,b,a)" by (rule exists_fresh(2), rule fin_supp, blast)
  have "OrR1
.M b = OrR1 .([(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)]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
.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 "M🪙a M' ==> OrR2
.M b 🪙a OrR2 .M' b"
proof -
  assume red: "M🪙a M'"
  obtain a'::"coname" where fs1: "a'(M,b,a)" by (rule exists_fresh(2), rule fin_supp, blast)
  have "OrR2
.M b = OrR2 .([(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)]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
.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 "M🪙a M' ==> ImpL
.M (x).N y 🪙a ImpL .M' (x).N y"
proof -
  assume red: "M🪙a 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
.M (x).N y = ImpL .([(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)]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
.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 "N🪙a N' ==> ImpL
.M (x).N y 🪙a ImpL .M (x).N' y"
proof -
  assume red: "N🪙a 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
.M (x).N y = ImpL .([(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)]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
.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 "M🪙a M' ==> ImpR (x).
.M b 🪙a ImpR (x)..M' b"
proof -
  assume red: "M🪙a M'"
  obtain a'::"coname" where fs2: "a'(M,a,b)" by (rule exists_fresh(2), rule fin_supp, blast)
  have "ImpR (x).
.M b = ImpR (x)..([(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)]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).
.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
.M x 🪙a R"
  shows "M'. R = NotL
.M' x M🪙aM'"
  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 M🪙aM'"
  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
.M .N c🪙a R"
  shows "(M'. R = AndR
.M' .N c M🪙aM') (N'. R = AndR .M .N' c N🪙aN')"
  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 M🪙aM'"
  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 M🪙aM'"
  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 z🪙a R"
  shows "(M'. R = OrL (x).M' (y).N z M🪙aM') (N'. R = OrL (x).M (y).N' z N🪙aN')"
  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
.M b 🪙a R"
  shows "M'. R = OrR1
.M' b M🪙aM'"
  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
.M b 🪙a R"
  shows "M'. R = OrR2
.M' b M🪙aM'"
  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
.M (y).N z🪙a R"
  shows "(M'. R = ImpL
.M' (y).N z M🪙aM') (N'. R = ImpL .M (y).N' z N🪙aN')"
  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).
.M b 🪙a R"
  shows "M'. R = ImpR (x).
.M' b M🪙aM'"
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
.M (x).N 🪙a* Cut .M' (x).N"
by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+

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

lemma a_star_Cut:
    "[M 🪙a* M'; N 🪙a* N'] ==> Cut
.M (x).N 🪙a* Cut .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
.M x 🪙a* NotL .M' x"
by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+

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

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

lemma a_star_AndR:
    "[M 🪙a* M'; N 🪙a* N'] ==> AndR
.M .N c 🪙a* AndR .M' .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
.M b 🪙a* OrR1 .M' b"
by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+

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

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

lemma a_star_ImpLR:
    "N 🪙a* N'==> ImpL
.M (y).N z 🪙a* ImpL .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
.M (y).N z 🪙a* ImpL .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).
.M b 🪙a* ImpR (x)..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
.M x 🪙a* R"
  shows "M'. R = NotL
.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
.M .N c🪙a* R"
  shows "(M' N'. R = AndR
.M' .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
.M y 🪙a* R"
  shows "M'. R = OrR1
.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
.M y 🪙a* R"
  shows "M'. R = OrR2
.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).
.M y 🪙a* R"
  shows "M'. R = ImpR (x).
.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
.M (y).N z 🪙a* R"
  shows "(M' N'. R = ImpL
.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:=.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:=.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:=.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:=.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:=.P},P,name1,trm2{x:=.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:=.P},P,name1,trm2{name2:=.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:=
.Ax y a} 🪙a* M[xn>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:=
.Ax y a} 🪙a* (Ax z b)[xn>y]"
  proof (cases "z=x")
    case True
    assume eq: "z=x"
    have "(Ax z b){x:=
.Ax y a} = Cut .Ax y a (x).Ax x b" using eq by simp
    also have " 🪙a* (Ax x b)[xn>y]" by blast
    finally show "Ax z b{x:=
.Ax y a} 🪙a* (Ax z b)[xn>y]" using eq by simp
  next
    case False
    assume neq: "zx"
    then show "(Ax z b){x:=
.Ax y a} 🪙a* (Ax z b)[xn>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:=
.Ax y a} 🪙a* M[xn>y]" by fact
  have ih2: "N{x:=
.Ax y a} 🪙a* N[xn>y]" by fact
  show "(Cut .M (z).N){x:=
.Ax y a} 🪙a* (Cut .M (z).N)[xn>y]"
  proof (cases "M = Ax x b")
    case True
    assume eq: "M = Ax x b"
    have "(Cut .M (z).N){x:=
.Ax y a} = Cut .Ax y a (z).(N{x:=.Ax y a})" using fs eq by simp
    also have " 🪙a* Cut
.Ax y a (z).(N[xn>y])" using ih2 a_star_congs by blast
    also have " = Cut .(M[xn>y]) (z).(N[xn>y])" using eq
      by (simp add: trm.inject alpha calc_atm fresh_atm)
    finally show "(Cut .M (z).N){x:=
.Ax y a} 🪙a* (Cut .M (z).N)[xn>y]" using fs by simp
  next
    case False
    assume neq: "M Ax x b"
    have "(Cut .M (z).N){x:=
.Ax y a} = Cut .(M{x:=.Ax y a}) (z).(N{x:=.Ax y a})" 
      using fs neq by simp
    also have " 🪙a* Cut .(M[xn>y]) (z).(N[xn>y])" using ih1 ih2 a_star_congs by blast
    finally show "(Cut .M (z).N){x:=
.Ax y a} 🪙a* (Cut .M (z).N)[xn>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:=
.Ax y a} 🪙a* M[xn>y]" by fact
  have "(NotR (z).M b){x:=
.Ax y a} = NotR (z).(M{x:=.Ax y a}) b" using fs by simp
  also have " 🪙a* NotR (z).(M[xn>y]) b" using ih by (auto intro: a_star_congs)
  finally show "(NotR (z).M b){x:=
.Ax y a} 🪙a* (NotR (z).M b)[xn>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:=
.Ax y a} 🪙a* M[xn>y]" by fact
  show "(NotL .M z){x:=
.Ax y a} 🪙a* (NotL .M z)[xn>y]"
  proof(cases "z=x")
    case True
    assume eq: "z=x"
    obtain x'::"name" where new: "x'(Ax y a,M{x:=
.Ax y a})" by (rule exists_fresh(1)[OF fs_name1])
    have "(NotL .M z){x:=
.Ax y a} =
                        fresh_fun (λx'. Cut
.Ax y a (x').NotL .(M{x:=.Ax y a}) x')"
      using eq fs by simp
    also have " = Cut
.Ax y a (x').NotL .(M{x:=.Ax y a}) x'" 
      using new by (simp add: fresh_fun_simp_NotL fresh_prod)
    also have " 🪙a* (NotL .(M{x:=
.Ax y a}) x')[x'n>y]"
      using new 
      by (intro a_starI al_redu better_LAxL_intro) auto
    also have " = NotL .(M{x:=
.Ax y a}) y" using new by (simp add: nrename_fresh)
    also have " 🪙a* NotL .(M[xn>y]) y" using ih by (auto intro: a_star_congs)
    also have " = (NotL .M z)[xn>y]" using eq by simp
    finally show "(NotL .M z){x:=
.Ax y a} 🪙a* (NotL .M z)[xn>y]" by simp
  next
    case False
    assume neq: "zx"
    have "(NotL .M z){x:=
.Ax y a} = NotL .(M{x:=.Ax y a}) z" using fs neq by simp
    also have " 🪙a* NotL .(M[xn>y]) z" using ih by (auto intro: a_star_congs)
    finally show "(NotL .M z){x:=
.Ax y a} 🪙a* (NotL .M z)[xn>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:=
.Ax y a} 🪙a* M[xn>y]" by fact
  have ih2: "N{x:=
.Ax y a} 🪙a* N[xn>y]" by fact
  have "(AndR .M .N e){x:=
.Ax y a} = AndR .(M{x:=.Ax y a}) .(N{x:=.Ax y a}) e"
    using fs by simp
  also have " 🪙a* AndR .(M[xn>y]) .(N[xn>y]) e" using ih1 ih2 by (auto intro: a_star_congs)
  finally show "(AndR .M .N e){x:=
.Ax y a} 🪙a* (AndR .M .N e)[xn>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:=
.Ax y a} 🪙a* M[xn>y]" by fact
  show "(AndL1 (u).M v){x:=
.Ax y a} 🪙a* (AndL1 (u).M v)[xn>y]"
  proof(cases "v=x")
    case True
    assume eq: "v=x"
    obtain v'::"name" where new: "v'(Ax y a,M{x:=
.Ax y a},u)" by (rule exists_fresh(1)[OF fs_name1])
    have "(AndL1 (u).M v){x:=
.Ax y a} =
                        fresh_fun (λv'. Cut
.Ax y a (v').AndL1 (u).(M{x:=.Ax y a}) v')"
      using eq fs by simp
    also have " = Cut
.Ax y a (v').AndL1 (u).(M{x:=.Ax y a}) v'" 
      using new by (simp add: fresh_fun_simp_AndL1 fresh_prod)
    also have " 🪙a* (AndL1 (u).(M{x:=
.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:=
.Ax y a}) y" using fs new
      by (auto simp: fresh_prod fresh_atm nrename_fresh)
    also have " 🪙a* AndL1 (u).(M[xn>y]) y" using ih by (auto intro: a_star_congs)
    also have " = (AndL1 (u).M v)[xn>y]" using eq fs by simp
    finally show "(AndL1 (u).M v){x:=
.Ax y a} 🪙a* (AndL1 (u).M v)[xn>y]" by simp
  next
    case False
    assume neq: "vx"
    have "(AndL1 (u).M v){x:=
.Ax y a} = AndL1 (u).(M{x:=.Ax y a}) v" using fs neq by simp
    also have " 🪙a* AndL1 (u).(M[xn>y]) v" using ih by (auto intro: a_star_congs)
    finally show "(AndL1 (u).M v){x:=
.Ax y a} 🪙a* (AndL1 (u).M v)[xn>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:=
.Ax y a} 🪙a* M[xn>y]" by fact
  show "(AndL2 (u).M v){x:=
.Ax y a} 🪙a* (AndL2 (u).M v)[xn>y]"
  proof(cases "v=x")
    case True
    assume eq: "v=x"
    obtain v'::"name" where new: "v'(Ax y a,M{x:=
.Ax y a},u)" by (rule exists_fresh(1)[OF fs_name1])
    have "(AndL2 (u).M v){x:=
.Ax y a} =
                        fresh_fun (λv'. Cut
.Ax y a (v').AndL2 (u).(M{x:=.Ax y a}) v')"
      using eq fs by simp
    also have " = Cut
.Ax y a (v').AndL2 (u).(M{x:=.Ax y a}) v'" 
      using new by (simp add: fresh_fun_simp_AndL2 fresh_prod)
    also have " 🪙a* (AndL2 (u).(M{x:=
.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:=
.Ax y a}) y" using fs new
      by (auto simp: fresh_prod fresh_atm nrename_fresh)
    also have " 🪙a* AndL2 (u).(M[xn>y]) y" using ih by (auto intro: a_star_congs)
    also have " = (AndL2 (u).M v)[xn>y]" using eq fs by simp
    finally show "(AndL2 (u).M v){x:=
.Ax y a} 🪙a* (AndL2 (u).M v)[xn>y]" by simp
  next
    case False
    assume neq: "vx"
    have "(AndL2 (u).M v){x:=
.Ax y a} = AndL2 (u).(M{x:=.Ax y a}) v" using fs neq by simp
    also have " 🪙a* AndL2 (u).(M[xn>y]) v" using ih by (auto intro: a_star_congs)
    finally show "(AndL2 (u).M v){x:=
.Ax y a} 🪙a* (AndL2 (u).M v)[xn>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:=
.Ax y a} 🪙a* M[xn>y]" by fact
  have "(OrR1 .M d){x:=
.Ax y a} = OrR1 .(M{x:=.Ax y a}) d" using fs by (simp add: fresh_atm)
  also have " 🪙a* OrR1 .(M[xn>y]) d" using ih by (auto intro: a_star_congs)
  finally show "(OrR1 .M d){x:=
.Ax y a} 🪙a* (OrR1 .M d)[xn>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:=
.Ax y a} 🪙a* M[xn>y]" by fact
  have "(OrR2 .M d){x:=
.Ax y a} = OrR2 .(M{x:=.Ax y a}) d" using fs by (simp add: fresh_atm)
  also have " 🪙a* OrR2 .(M[xn>y]) d" using ih by (auto intro: a_star_congs)
  finally show "(OrR2 .M d){x:=
.Ax y a} 🪙a* (OrR2 .M d)[xn>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:=
.Ax y a} 🪙a* M[xn>y]" by fact
  have ih2: "N{x:=
.Ax y a} 🪙a* N[xn>y]" by fact
  show "(OrL (u).M (v).N z){x:=
.Ax y a} 🪙a* (OrL (u).M (v).N z)[xn>y]"
  proof(cases "z=x")
    case True
    assume eq: "z=x"
    obtain z'::"name" where new: "z'(Ax y a,M{x:=
.Ax y a},N{x:=.Ax y a},u,v,y,a)" 
      by (rule exists_fresh(1)[OF fs_name1])
    have "(OrL (u).M (v).N z){x:=
.Ax y a} =
                 fresh_fun (λz'. Cut
.Ax y a (z').OrL (u).(M{x:=.Ax y a}) (v).(N{x:=.Ax y a}) z')"
      using eq fs by simp
    also have " = Cut
.Ax y a (z').OrL (u).(M{x:=.Ax y a}) (v).(N{x:=.Ax y a}) z'" 
      using new by (simp add: fresh_fun_simp_OrL)
    also have " 🪙a* (OrL (u).(M{x:=
.Ax y a}) (v).(N{x:=.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:=
.Ax y a}) (v).(N{x:=.Ax y a}) y" using fs new
      by (auto simp: fresh_prod fresh_atm nrename_fresh subst_fresh)
    also have " 🪙a* OrL (u).(M[xn>y]) (v).(N[xn>y]) y" 
      using ih1 ih2 by (auto intro: a_star_congs)
    also have " = (OrL (u).M (v).N z)[xn>y]" using eq fs by simp
    finally show "(OrL (u).M (v).N z){x:=
.Ax y a} 🪙a* (OrL (u).M (v).N z)[xn>y]" by simp
  next
    case False
    assume neq: "zx"
    have "(OrL (u).M (v).N z){x:=
.Ax y a} = OrL (u).(M{x:=.Ax y a}) (v).(N{x:=.Ax y a}) z" 
      using fs neq by simp
    also have " 🪙a* OrL (u).(M[xn>y]) (v).(N[xn>y]) z" 
      using ih1 ih2 by (auto intro: a_star_congs)
    finally show "(OrL (u).M (v).N z){x:=
.Ax y a} 🪙a* (OrL (u).M (v).N z)[xn>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:=
.Ax y a} 🪙a* M[xn>y]" by fact
  have "(ImpR (z)..M d){x:=
.Ax y a} = ImpR (z)..(M{x:=.Ax y a}) d" using fs by simp
  also have " 🪙a* ImpR (z)..(M[xn>y]) d" using ih by (auto intro: a_star_congs)
  finally show "(ImpR (z)..M d){x:=
.Ax y a} 🪙a* (ImpR (z)..M d)[xn>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:=
.Ax y a} 🪙a* M[xn>y]" by fact
  have ih2: "N{x:=
.Ax y a} 🪙a* N[xn>y]" by fact
  show "(ImpL .M (u).N v){x:=
.Ax y a} 🪙a* (ImpL .M (u).N v)[xn>y]"
  proof(cases "v=x")
    case True
    assume eq: "v=x"
    obtain v'::"name" where new: "v'(Ax y a,M{x:=
.Ax y a},N{x:=.Ax y a},y,a,u)" 
      by (rule exists_fresh(1)[OF fs_name1])
    have "(ImpL .M (u).N v){x:=
.Ax y a} =
                 fresh_fun (λv'. Cut
.Ax y a (v').ImpL .(M{x:=.Ax y a}) (u).(N{x:=.Ax y a}) v')"
      using eq fs by simp 
    also have " = Cut
.Ax y a (v').ImpL .(M{x:=.Ax y a}) (u).(N{x:=.Ax y a}) v'" 
      using new by (simp add: fresh_fun_simp_ImpL)
    also have " 🪙a* (ImpL .(M{x:=
.Ax y a}) (u).(N{x:=.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 .(M{x:=
.Ax y a}) (u).(N{x:=.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 .(M[xn>y]) (u).(N[xn>y]) y" 
      using ih1 ih2 by (auto intro: a_star_congs)
    also have " = (ImpL .M (u).N v)[xn>y]" using eq fs by simp
    finally show "(ImpL .M (u).N v){x:=
.Ax y a} 🪙a* (ImpL .M (u).N v)[xn>y]" using fs by simp
  next
    case False
    assume neq: "vx"
    have "(ImpL .M (u).N v){x:=
.Ax y a} = ImpL .(M{x:=.Ax y a}) (u).(N{x:=.Ax y a}) v
      using fs neq by simp
    also have " 🪙a* ImpL .(M[xn>y]) (u).(N[xn>y]) v" 
      using ih1 ih2 by (auto intro: a_star_congs)
    finally show "(ImpL .M (u).N v){x:=
.Ax y a} 🪙a* (ImpL .M (u).N v)[xn>y]" 
      using fs neq by simp
  qed
qed

lemma subst_with_ax2:
  shows "M{b:=(x).Ax x a} 🪙a* M[bc>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)[bc>a]"
  proof (cases "c=b")
    case True
    assume eq: "c=b"
    have "(Ax z c){b:=(x).Ax x a} = Cut .Ax z c (x).Ax x a" using eq by simp
    also have " 🪙a* (Ax z c)[bc>a]" using eq by blast
    finally show "(Ax z c){b:=(x).Ax x a} 🪙a* (Ax z c)[bc>a]" by simp
  next
    case False
    assume neq: "cb"
    then show "(Ax z c){b:=(x).Ax x a} 🪙a* (Ax z c)[bc>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[bc>a]" by fact
  have ih2: "N{b:=(x).Ax x a} 🪙a* N[bc>a]" by fact
  show "(Cut .M (z).N){b:=(x).Ax x a} 🪙a* (Cut .M (z).N)[bc>a]"
  proof (cases "N = Ax z b")
    case True
    assume eq: "N = Ax z b"
    have "(Cut .M (z).N){b:=(x).Ax x a} = Cut .(M{b:=(x).Ax x a}) (x).Ax x a" using eq fby simp 
    also have " 🪙a* Cut .(M[bc>a]) (x).Ax x a" using ih1 a_star_congs by blast
    also have " = Cut .(M[bc>a]) (z).(N[bc>a])" using eq fs
      by (simp add: trm.inject alpha calc_atm fresh_atm)
    finally show "(Cut .M (z).N){b:=(x).Ax x a} 🪙a* (Cut .M (z).N)[bc>a]" using fs by simp
  next
    case False
    assume neq: "N Ax z b"
    have "(Cut .M (z).N){b:=(x).Ax x a} = Cut .(M{b:=(x).Ax x a}) (z).(N{b:=(x).Ax x a})" 
      using fs neq by simp
    also have " 🪙a* Cut .(M[bc>a]) (z).(N[bc>a])" using ih1 ih2 a_star_congs by blast
    finally show "(Cut .M (z).N){b:=(x).Ax x a} 🪙a* (Cut .M (z).N)[bc>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[bc>a]" by fact
  show "(NotR (z).M c){b:=(x).Ax x a} 🪙a* (NotR (z).M c)[bc>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 .NotR (z).M{b:=(x).Ax x a} a' (x).Ax x a)" 
      using eq fs by simp
    also have " = Cut .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[bc>a]) a" using ih by (auto intro: a_star_congs)
    also have " = (NotR (z).M c)[bc>a]" using eq by simp
    finally show "(NotR (z).M c){b:=(x).Ax x a} 🪙a* (NotR (z).M c)[bc>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[bc>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)[bc>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[bc>a]" by fact
  have "(NotL .M z){b:=(x).Ax x a} = NotL .(M{b:=(x).Ax x a}) z" using fs by simp
  also have " 🪙a* NotL .(M[bc>a]) z" using ih by (auto intro: a_star_congs)
  finally show "(NotL .M z){b:=(x).Ax x a} 🪙a* (NotL .M z)[bc>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[bc>a]" by fact
  have ih2: "N{b:=(x).Ax x a} 🪙a* N[bc>a]" by fact
  show "(AndR .M .N e){b:=(x).Ax x a} 🪙a* (AndR .M .N e)[bc>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 .M .N e){b:=(x).Ax x a} =
               fresh_fun (λe'. Cut .AndR .(M{b:=(x).Ax x a}) .(N{b:=(x).Ax x a}) e' (x).Ax x a)"
      using eq fs by simp
    also have " = Cut .AndR .(M{b:=(x).Ax x a}) .(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 .(M{b:=(x).Ax x a}) .(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 .(M{b:=(x).Ax x a}) .(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 .(M[bc>a]) .(N[bc>a]) a" using ih1 ih2 by (auto intro: a_star_congs)
    also have " = (AndR .M .N e)[bc>a]" using eq fs by simp
    finally show "(AndR .M .N e){b:=(x).Ax x a} 🪙a* (AndR .M .N e)[bc>a]" by simp
  next
    case False
    assume neq: "eb"
    have "(AndR .M .N e){b:=(x).Ax x a} = AndR .(M{b:=(x).Ax x a}) .(N{b:=(x).Ax x a}) e"
      using fs neq by simp
    also have " 🪙a* AndR .(M[bc>a]) .(N[bc>a]) e" using ih1 ih2 by (auto intro: a_star_congs)
    finally show "(AndR .M .N e){b:=(x).Ax x a} 🪙a* (AndR .M .N e)[bc>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[bc>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[bc>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)[bc>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[bc>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[bc>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)[bc>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[bc>a]" by fact
  show "(OrR1 .M d){b:=(x).Ax x a} 🪙a* (OrR1 .M d)[bc>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 .M d){b:=(x).Ax x a} =
             fresh_fun (λa'. Cut .OrR1 .M{b:=(x).Ax x a} a' (x).Ax x a)" using fs eq by (simp)
    also have " = Cut .OrR1 .M{b:=(x).Ax x a} a' (x).Ax x a"
      using new by (simp add: fresh_fun_simp_OrR1)
    also have " 🪙a* (OrR1 .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 .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 .(M[bc>a]) a" using ih by (auto intro: a_star_congs)
    also have " = (OrR1 .M d)[bc>a]" using eq fs by simp
    finally show "(OrR1 .M d){b:=(x).Ax x a} 🪙a* (OrR1 .M d)[bc>a]" by simp
  next
    case False
    assume neq: "db"
    have "(OrR1 .M d){b:=(x).Ax x a} = OrR1 .(M{b:=(x).Ax x a}) d" using fs neq by (simp)
    also have " 🪙a* OrR1 .(M[bc>a]) d" using ih by (auto intro: a_star_congs)
    finally show "(OrR1 .M d){b:=(x).Ax x a} 🪙a* (OrR1 .M d)[bc>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[bc>a]" by fact
  show "(OrR2 .M d){b:=(x).Ax x a} 🪙a* (OrR2 .M d)[bc>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 .M d){b:=(x).Ax x a} =
             fresh_fun (λa'. Cut .OrR2 .M{b:=(x).Ax x a} a' (x).Ax x a)" using fs eq by (simp)
    also have " = Cut .OrR2 .M{b:=(x).Ax x a} a' (x).Ax x a"
      using new by (simp add: fresh_fun_simp_OrR2)
    also have " 🪙a* (OrR2 .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 .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 .(M[bc>a]) a" using ih by (auto intro: a_star_congs)
    also have " = (OrR2 .M d)[bc>a]" using eq fs by simp
    finally show "(OrR2 .M d){b:=(x).Ax x a} 🪙a* (OrR2 .M d)[bc>a]" by simp
  next
    case False
    assume neq: "db"
    have "(OrR2 .M d){b:=(x).Ax x a} = OrR2 .(M{b:=(x).Ax x a}) d" using fs neq by (simp)
    also have " 🪙a* OrR2 .(M[bc>a]) d" using ih by (auto intro: a_star_congs)
    finally show "(OrR2 .M d){b:=(x).Ax x a} 🪙a* (OrR2 .M d)[bc>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[bc>a]" by fact
  have ih2: "N{b:=(x).Ax x a} 🪙a* N[bc>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[bc>a]) (v).(N[bc>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)[bc>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[bc>a]" by fact
  show "(ImpR (z)..M d){b:=(x).Ax x a} 🪙a* (ImpR (z)..M d)[bc>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)..M d){b:=(x).Ax x a} =
                fresh_fun (λa'. Cut .ImpR z..M{b:=(x).Ax x a} a' (x).Ax x a)" using fs eq by simp
    also have " = Cut .ImpR z..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..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..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..(M[bc>a]) a" using ih by (auto intro: a_star_congs)
    also have " = (ImpR z..M b)[bc>a]" using eq fs by simp
    finally show "(ImpR (z)..M d){b:=(x).Ax x a} 🪙a* (ImpR (z)..M d)[bc>a]" using eq by simp
  next
    case False
    assume neq: "bd"
    have "(ImpR (z)..M d){b:=(x).Ax x a} = ImpR (z)..(M{b:=(x).Ax x a}) d" using fs neq by simp
    also have " 🪙a* ImpR (z)..(M[bc>a]) d" using ih by (auto intro: a_star_congs)
    finally show "(ImpR (z)..M d){b:=(x).Ax x a} 🪙a* (ImpR (z)..M d)[bc>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[bc>a]" by fact
  have ih2: "N{b:=(x).Ax x a} 🪙a* N[bc>a]" by fact
  have "(ImpL .M (u).N v){b:=(x).Ax x a} = ImpL .(M{b:=(x).Ax x a}) (u).(N{b:=(x).Ax x a}) v" 
    using fs by simp
  also have " 🪙a* ImpL .(M[bc>a]) (u).(N[bc>a]) v" 
    using ih1 ih2 by (auto intro: a_star_congs)
  finally show "(ImpL .M (u).N v){b:=(x).Ax x a} 🪙a* (ImpL .M (u).N v)[bc>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:=.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:=.P}{x:=.P} = N{x:=.Ax y c}{y:=.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:=.P},M{x:=.Ax y c}{y:=.P},y,x)"
      and  "x'' (P,M{x:=.Ax y c},M{x:=.Ax y c}{y:=.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:=.P},M{x:=.Ax y c}{y:=.P},u,y,x)"
      and  "x'' (P,Ax y c,M{x:=.Ax y c},M{x:=.Ax y c}{y:=.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:=.P},M{x:=.Ax y c}{y:=.P},u,y,x)"
      and  "x'' (P,Ax y c,M{x:=.Ax y c},M{x:=.Ax y c}{y:=.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:=.P},M{x:=.Ax y c}{y:=.P},
                       M'{y:=.P},M'{x:=.Ax y c}{y:=.P},x1,x2,x3,y,x)"
      and  "x'' (P,Ax y c,M{x:=.Ax y c},M{x:=.Ax y c}{y:=.P},
                                        M'{x:=.Ax y c},M'{x:=.Ax y c}{y:=.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:=.P},M{x:=.Ax x2 c}{x2:=.P},
                                        M'{x2:=.P},M'{x:=.Ax x2 c}{x2:=.P},x1,y,x)"
      and  "x'' (P,Ax y c,M{x2:=.Ax y c},M{x2:=.Ax y c}{y:=.P},
                                        M'{x2:=.Ax y c},M'{x2:=.Ax y c}{y:=.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:=.P}{x:=.P} = N{x:=
.Ax y a}{y:=.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:=
.Ax y a} = N{x:=.([(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:=
.P}{b:=(y).Q} = M{b:=(y).Q}{x:=.(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:=
.P},P{b:=(y).Q},M{b:=(y).Q}{x:=.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:=
.P},P{b:=(y).Q},z1,y,Q,M{b:=(y).Q}{x:=.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:=
.P},P{b:=(y).Q},z1,y,Q,M{b:=(y).Q}{x:=.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:=
.P},M{b:=(y).Q}{x:=.P{b:=(y).Q}},z2,z3,a,y,Q,
                                     P{b:=(y).Q},N{x:=
.P},N{b:=(y).Q}{x:=.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:=
.P},N{u:=.P},y,Q,
                        M{b:=(y).Q}{u:=
.P{b:=(y).Q}},N{b:=(y).Q}{u:=.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:=.P} = M{y:=.P}{a:=(x).N{y:=.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:=.P},M'{d:=(x).N},M'{y:=.P}{d:=(x).N{y:=.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:=.P},M'{y:=.P},M'{y:=.P}{a:=(x).N{y:=.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:=.P},M'{f:=(x).N},M''{f:=(x).N},
                  M'{y:=.P}{f:=(x).N{y:=.P}},M''{y:=.P}{f:=(x).N{y:=.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:=.P},M'{f:=(x).N},M''{f:=(x).N},
                  M'{y:=.P}{f:=(x).N{y:=.P}},M''{y:=.P}{f:=(x).N{y:=.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:=.P},M'{y:=.P}{a:=(x).N{y:=.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:=.P},M'{y:=.P}{a:=(x).N{y:=.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:=.P},M'{y:=.P},M''{y:=.P},
                  M'{y:=.P}{a:=(x).N{y:=.P}},M''{y:=.P}{a:=(x).N{y:=.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:=.P},
                                        M'{f:=(x).N},M'{y:=.P}{f:=(x).N{y:=.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:=.P},
                                        M'{f:=(x).N},M'{y:=.P}{f:=(x).N{y:=.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:=.P},
                                     M'{f:=(x).N},M'{y:=.P}{f:=(x).N{y:=.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:=.P},M'{w:=.P},M''{w:=.P},
                  M'{w:=.P}{a:=(x).N{w:=.P}},M''{w:=.P}{a:=(x).N{w:=.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:=
.M}{y:=.P} = N{y:=.P}{x:=.(M{y:=.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:=.P},M'{x:=
.M},M'{y:=.P}{x:=.M{y:=.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:=.P},M'{y:=.P}{x:=
.M{y:=.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:=.P},M'{x:=
.M},M'{y:=.P}{x:=.M{y:=.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:=.P},M'{y:=.P}{x:=
.M{y:=.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:=.P},M'{x:=
.M},M'{y:=.P}{x:=.M{y:=.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:=.P},M'{y:=.P}{x:=
.M{y:=.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:=.P},M'{x:=
.M},M'{y:=.P}{x:=.M{y:=.P}},
                                      x1,x2,x3,M''{x:=
.M},M''{y:=.P}{x:=.M{y:=.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:=.P},M'{y:=.P}{x:=
.M{y:=.P}},
                                      x1,x2,x3,M''{y:=.P},M''{y:=.P}{x:=
.M{y:=.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:=.P},M'{x2:=
.M},M'{y:=.P}{x2:=.M{y:=.P}},
                                      x1,x2,M''{x2:=
.M},M''{y:=.P}{x2:=.M{y:=.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:=.P},M'{x2:=.P}{x:=
.M{x2:=.P}},
                                      x1,x2,M''{x2:=.P},M''{x2:=.P}{x:=
.M{x2:=.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

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.677Angebot  (Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-28) ¤

*Eine klare Vorstellung vom Zielzustand






Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.






                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....

Besucherstatistik

Besucherstatistik

Monitoring

Montastic status badge