Theory Class1

theory Class1
imports Nominal
theory Class1
imports "HOL-Nominal.Nominal" 
begin

section ‹Term-Calculus from Urban's PhD›

atom_decl name coname

text ‹types›

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 "a♯T" and "x♯T"
by (nominal_induct T rule: ty.strong_induct)
   (auto simp add: fresh_string)

text ‹terms›

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

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,100,100] 100) 
where
  "(Ax x a)[d⊢c>e] = (if a=d then Ax x e else Ax x a)" 
| "⟦a♯(d,e,N);x♯M⟧ ⟹ (Cut <a>.M (x).N)[d⊢c>e] = Cut <a>.(M[d⊢c>e]) (x).(N[d⊢c>e])" 
| "(NotR (x).M a)[d⊢c>e] = (if a=d then NotR (x).(M[d⊢c>e]) e else NotR (x).(M[d⊢c>e]) a)" 
| "a♯(d,e) ⟹ (NotL <a>.M x)[d⊢c>e] = (NotL <a>.(M[d⊢c>e]) x)" 
| "⟦a♯(d,e,N,c);b♯(d,e,M,c);b≠a⟧ ⟹ (AndR <a>.M <b>.N c)[d⊢c>e] = 
          (if c=d then AndR <a>.(M[d⊢c>e]) <b>.(N[d ⊢c>e]) e else AndR <a>.(M[d⊢c>e]) <b>.(N[d⊢c>e]) c)" 
| "x♯y ⟹ (AndL1 (x).M y)[d⊢c>e] = AndL1 (x).(M[d⊢c>e]) y"
| "x♯y ⟹ (AndL2 (x).M y)[d⊢c>e] = AndL2 (x).(M[d⊢c>e]) y"
| "a♯(d,e,b) ⟹ (OrR1 <a>.M b)[d⊢c>e] = (if b=d then OrR1 <a>.(M[d⊢c>e]) e else OrR1 <a>.(M[d⊢c>e]) b)"
| "a♯(d,e,b) ⟹ (OrR2 <a>.M b)[d⊢c>e] = (if b=d then OrR2 <a>.(M[d⊢c>e]) e else OrR2 <a>.(M[d⊢c>e]) b)"
| "⟦x♯(N,z);y♯(M,z);y≠x⟧ ⟹ (OrL (x).M (y).N z)[d⊢c>e] = OrL (x).(M[d⊢c>e]) (y).(N[d⊢c>e]) z"
| "a♯(d,e,b) ⟹ (ImpR (x).<a>.M b)[d⊢c>e] = 
       (if b=d then ImpR (x).<a>.(M[d⊢c>e]) e else ImpR (x).<a>.(M[d⊢c>e]) b)"
| "⟦a♯(d,e,N);x♯(M,y)⟧ ⟹ (ImpL <a>.M (x).N y)[d⊢c>e] = ImpL <a>.(M[d⊢c>e]) (x).(N[d⊢c>e]) y"
apply(finite_guess)+
apply(rule TrueI)+
apply(simp add: abs_fresh abs_supp fin_supp)+
apply(fresh_guess)+
done

nominal_primrec (freshness_context: "(u::name,v::name)") 
  nrename :: "trm ⇒ name ⇒ name ⇒ trm"      ("_[_⊢n>_]" [100,100,100] 100) 
where
  "(Ax x a)[u⊢n>v] = (if x=u then Ax v a else Ax x a)" 
| "⟦a♯N;x♯(u,v,M)⟧ ⟹ (Cut <a>.M (x).N)[u⊢n>v] = Cut <a>.(M[u⊢n>v]) (x).(N[u⊢n>v])" 
| "x♯(u,v) ⟹ (NotR (x).M a)[u⊢n>v] = NotR (x).(M[u⊢n>v]) a" 
| "(NotL <a>.M x)[u⊢n>v] = (if x=u then NotL <a>.(M[u⊢n>v]) v else NotL <a>.(M[u⊢n>v]) x)" 
| "⟦a♯(N,c);b♯(M,c);b≠a⟧ ⟹ (AndR <a>.M <b>.N c)[u⊢n>v] = AndR <a>.(M[u⊢n>v]) <b>.(N[u⊢n>v]) c" 
| "x♯(u,v,y) ⟹ (AndL1 (x).M y)[u⊢n>v] = (if y=u then AndL1 (x).(M[u⊢n>v]) v else AndL1 (x).(M[u⊢n>v]) y)"
| "x♯(u,v,y) ⟹ (AndL2 (x).M y)[u⊢n>v] = (if y=u then AndL2 (x).(M[u⊢n>v]) v else AndL2 (x).(M[u⊢n>v]) y)"
| "a♯b ⟹ (OrR1 <a>.M b)[u⊢n>v] = OrR1 <a>.(M[u⊢n>v]) b"
| "a♯b ⟹ (OrR2 <a>.M b)[u⊢n>v] = OrR2 <a>.(M[u⊢n>v]) b"
| "⟦x♯(u,v,N,z);y♯(u,v,M,z);y≠x⟧ ⟹ (OrL (x).M (y).N z)[u⊢n>v] = 
        (if z=u then OrL (x).(M[u⊢n>v]) (y).(N[u⊢n>v]) v else OrL (x).(M[u⊢n>v]) (y).(N[u⊢n>v]) z)"
| "⟦a♯b; x♯(u,v)⟧ ⟹ (ImpR (x).<a>.M b)[u⊢n>v] = ImpR (x).<a>.(M[u⊢n>v]) b"
| "⟦a♯N;x♯(u,v,M,y)⟧ ⟹ (ImpL <a>.M (x).N y)[u⊢n>v] = 
        (if y=u then ImpL <a>.(M[u⊢n>v]) (x).(N[u⊢n>v]) v else ImpL <a>.(M[u⊢n>v]) (x).(N[u⊢n>v]) y)"
apply(finite_guess)+
apply(rule TrueI)+
apply(simp add: abs_fresh abs_supp fs_name1 fs_coname1)+
apply(fresh_guess)+
done

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

lemma crename_name_eqvt[eqvt]:
  fixes pi::"name prm"
  shows "pi∙(M[d⊢c>e]) = (pi∙M)[(pi∙d)⊢c>(pi∙e)]"
apply(nominal_induct M avoiding: d e rule: trm.strong_induct)
apply(auto simp add: fresh_bij eq_bij)
done

lemma crename_coname_eqvt[eqvt]:
  fixes pi::"coname prm"
  shows "pi∙(M[d⊢c>e]) = (pi∙M)[(pi∙d)⊢c>(pi∙e)]"
apply(nominal_induct M avoiding: d e rule: trm.strong_induct)
apply(auto simp add: fresh_bij eq_bij)
done

lemma nrename_name_eqvt[eqvt]:
  fixes pi::"name prm"
  shows "pi∙(M[x⊢n>y]) = (pi∙M)[(pi∙x)⊢n>(pi∙y)]"
apply(nominal_induct M avoiding: x y rule: trm.strong_induct)
apply(auto simp add: fresh_bij eq_bij)
done

lemma nrename_coname_eqvt[eqvt]:
  fixes pi::"coname prm"
  shows "pi∙(M[x⊢n>y]) = (pi∙M)[(pi∙x)⊢n>(pi∙y)]"
apply(nominal_induct M avoiding: x y rule: trm.strong_induct)
apply(auto simp add: fresh_bij eq_bij)
done

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

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

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

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

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

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

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

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

lemma nrename_rename:
  assumes a: "x'♯M"
  shows "([(x',x)]∙M)[x'⊢n>y]= M[x⊢n>y]"
using a
apply(nominal_induct M avoiding: x x' y rule: trm.strong_induct)
apply(auto simp add: abs_fresh fresh_bij fresh_atm fresh_prod fresh_right calc_atm abs_supp fin_supp)
apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)
done

lemma crename_rename:
  assumes a: "a'♯M"
  shows "([(a',a)]∙M)[a'⊢c>b]= M[a⊢c>b]"
using a
apply(nominal_induct M avoiding: a a' b rule: trm.strong_induct)
apply(auto simp add: abs_fresh fresh_bij fresh_atm fresh_prod fresh_right calc_atm abs_supp fin_supp)
apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)
done

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

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

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

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

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

lemma nrename_swap:
  shows "x♯M ⟹ [(x,y)]∙M = M[y⊢n>x]"
by (nominal_induct M avoiding: x y rule: trm.strong_induct) 
   (simp_all add: calc_atm fresh_atm trm.inject alpha abs_fresh abs_supp fin_supp)

lemma crename_swap:
  shows "a♯M ⟹ [(a,b)]∙M = M[b⊢c>a]"
by (nominal_induct M avoiding: a b rule: trm.strong_induct) 
   (simp_all add: calc_atm fresh_atm trm.inject alpha abs_fresh abs_supp fin_supp)

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

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

text ‹substitution functions›

lemma fresh_perm_coname:
  fixes c::"coname"
  and   pi::"coname prm"
  and   M::"trm"
  assumes a: "c♯pi" "c♯M"
  shows "c♯(pi∙M)"
using a
apply -
apply(simp add: fresh_left)
apply(simp add: at_prm_fresh[OF at_coname_inst] fresh_list_rev)
done

lemma fresh_perm_name:
  fixes x::"name"
  and   pi::"name prm"
  and   M::"trm"
  assumes a: "x♯pi" "x♯M"
  shows "x♯(pi∙M)"
using a
apply -
apply(simp add: fresh_left)
apply(simp add: at_prm_fresh[OF at_name_inst] fresh_list_rev)
done

lemma fresh_fun_simp_NotL:
  assumes a: "x'♯P" "x'♯M"
  shows "fresh_fun (λx'. Cut <c>.P (x').NotL <a>.M x') = Cut <c>.P (x').NotL <a>.M x'"
using a
apply -
apply(rule fresh_fun_app)
apply(rule pt_name_inst)
apply(rule at_name_inst)
apply(finite_guess)
apply(subgoal_tac "∃n::name. n♯(c,P,a,M)")
apply(erule exE)
apply(rule_tac x="n" in exI)
apply(simp add: fresh_prod abs_fresh)
apply(fresh_guess)
apply(rule exists_fresh')
apply(simp add: fin_supp)
apply(fresh_guess)
done

lemma fresh_fun_NotL[eqvt_force]:
  fixes pi1::"name prm"
  and   pi2::"coname prm"
  shows "pi1∙fresh_fun (λx'. Cut <c>.P (x').NotL <a>.M x')=
             fresh_fun (pi1∙(λx'. Cut <c>.P (x').NotL <a>.M x'))"
  and   "pi2∙fresh_fun (λx'. Cut <c>.P (x').NotL <a>.M x')=
             fresh_fun (pi2∙(λx'. Cut <c>.P (x').NotL <a>.M x'))"
apply -
apply(perm_simp)
apply(generate_fresh "name")
apply(auto simp add: fresh_prod)
apply(simp add: fresh_fun_simp_NotL)
apply(rule sym)
apply(rule trans)
apply(rule fresh_fun_simp_NotL)
apply(rule fresh_perm_name)
apply(assumption)
apply(assumption)
apply(rule fresh_perm_name)
apply(assumption)
apply(assumption)
apply(simp add: at_prm_fresh[OF at_name_inst] swap_simps)
apply(perm_simp)
apply(subgoal_tac "∃n::name. n♯(P,M,pi2∙P,pi2∙M,pi2)")
apply(simp add: fresh_prod)
apply(auto)
apply(simp add: fresh_fun_simp_NotL calc_atm)
apply(rule exists_fresh')
apply(simp add: fin_supp)
done

lemma fresh_fun_simp_AndL1:
  assumes a: "z'♯P" "z'♯M" "z'♯x"
  shows "fresh_fun (λz'. Cut <c>.P (z').AndL1 (x).M z') = Cut <c>.P (z').AndL1 (x).M z'"
using a
apply -
apply(rule fresh_fun_app)
apply(rule pt_name_inst)
apply(rule at_name_inst)
apply(finite_guess)
apply(subgoal_tac "∃n::name. n♯(c,P,x,M)")
apply(erule exE)
apply(rule_tac x="n" in exI)
apply(simp add: fresh_prod abs_fresh)
apply(fresh_guess)
apply(rule exists_fresh')
apply(simp add: fin_supp)
apply(fresh_guess)
done

lemma fresh_fun_AndL1[eqvt_force]:
  fixes pi1::"name prm"
  and   pi2::"coname prm"
  shows "pi1∙fresh_fun (λz'. Cut <c>.P (z').AndL1 (x).M z')=
             fresh_fun (pi1∙(λz'. Cut <c>.P (z').AndL1 (x).M z'))"
  and   "pi2∙fresh_fun (λz'. Cut <c>.P (z').AndL1 (x).M z')=
             fresh_fun (pi2∙(λz'. Cut <c>.P (z').AndL1 (x).M z'))"
apply -
apply(perm_simp)
apply(subgoal_tac "∃n::name. n♯(P,M,x,pi1∙P,pi1∙M,pi1∙x,pi1)")
apply(simp add: fresh_prod)
apply(auto)
apply(simp add: fresh_fun_simp_AndL1 at_prm_fresh[OF at_name_inst] swap_simps)
apply(rule exists_fresh')
apply(simp add: fin_supp)
apply(perm_simp)
apply(subgoal_tac "∃n::name. n♯(P,M,x,pi2∙P,pi2∙M,pi2∙x,pi2)")
apply(simp add: fresh_prod)
apply(auto)
apply(simp add: fresh_fun_simp_AndL1 calc_atm)
apply(rule exists_fresh')
apply(simp add: fin_supp)
done

lemma fresh_fun_simp_AndL2:
  assumes a: "z'♯P" "z'♯M" "z'♯x"
  shows "fresh_fun (λz'. Cut <c>.P (z').AndL2 (x).M z') = Cut <c>.P (z').AndL2 (x).M z'"
using a
apply -
apply(rule fresh_fun_app)
apply(rule pt_name_inst)
apply(rule at_name_inst)
apply(finite_guess)
apply(subgoal_tac "∃n::name. n♯(c,P,x,M)")
apply(erule exE)
apply(rule_tac x="n" in exI)
apply(simp add: fresh_prod abs_fresh)
apply(fresh_guess)
apply(rule exists_fresh')
apply(simp add: fin_supp)
apply(fresh_guess)
done

lemma fresh_fun_AndL2[eqvt_force]:
  fixes pi1::"name prm"
  and   pi2::"coname prm"
  shows "pi1∙fresh_fun (λz'. Cut <c>.P (z').AndL2 (x).M z')=
             fresh_fun (pi1∙(λz'. Cut <c>.P (z').AndL2 (x).M z'))"
  and   "pi2∙fresh_fun (λz'. Cut <c>.P (z').AndL2 (x).M z')=
             fresh_fun (pi2∙(λz'. Cut <c>.P (z').AndL2 (x).M z'))"
apply -
apply(perm_simp)
apply(subgoal_tac "∃n::name. n♯(P,M,x,pi1∙P,pi1∙M,pi1∙x,pi1)")
apply(simp add: fresh_prod)
apply(auto)
apply(simp add: fresh_fun_simp_AndL2 at_prm_fresh[OF at_name_inst] swap_simps)
apply(rule exists_fresh')
apply(simp add: fin_supp)
apply(perm_simp)
apply(subgoal_tac "∃n::name. n♯(P,M,x,pi2∙P,pi2∙M,pi2∙x,pi2)")
apply(simp add: fresh_prod)
apply(auto)
apply(simp add: fresh_fun_simp_AndL2 calc_atm)
apply(rule exists_fresh')
apply(simp add: fin_supp)
done

lemma fresh_fun_simp_OrL:
  assumes a: "z'♯P" "z'♯M" "z'♯N" "z'♯u" "z'♯x"
  shows "fresh_fun (λz'. Cut <c>.P (z').OrL (x).M (u).N z') = Cut <c>.P (z').OrL (x).M (u).N z'"
using a
apply -
apply(rule fresh_fun_app)
apply(rule pt_name_inst)
apply(rule at_name_inst)
apply(finite_guess)
apply(subgoal_tac "∃n::name. n♯(c,P,x,M,u,N)")
apply(erule exE)
apply(rule_tac x="n" in exI)
apply(simp add: fresh_prod abs_fresh)
apply(fresh_guess)
apply(rule exists_fresh')
apply(simp add: fin_supp)
apply(fresh_guess)
done

lemma fresh_fun_OrL[eqvt_force]:
  fixes pi1::"name prm"
  and   pi2::"coname prm"
  shows "pi1∙fresh_fun (λz'. Cut <c>.P (z').OrL (x).M (u).N z')=
             fresh_fun (pi1∙(λz'. Cut <c>.P (z').OrL (x).M (u).N z'))"
  and   "pi2∙fresh_fun (λz'. Cut <c>.P (z').OrL (x).M (u).N z')=
             fresh_fun (pi2∙(λz'. Cut <c>.P (z').OrL (x).M (u).N z'))"
apply -
apply(perm_simp)
apply(subgoal_tac "∃n::name. n♯(P,M,N,x,u,pi1∙P,pi1∙M,pi1∙N,pi1∙x,pi1∙u,pi1)")
apply(simp add: fresh_prod)
apply(auto)
apply(simp add: fresh_fun_simp_OrL at_prm_fresh[OF at_name_inst] swap_simps)
apply(rule exists_fresh')
apply(simp add: fin_supp)
apply(perm_simp)
apply(subgoal_tac "∃n::name. n♯(P,M,N,x,u,pi2∙P,pi2∙M,pi2∙N,pi2∙x,pi2∙u,pi2)")
apply(simp add: fresh_prod)
apply(auto)
apply(simp add: fresh_fun_simp_OrL calc_atm)
apply(rule exists_fresh')
apply(simp add: fin_supp)
done

lemma fresh_fun_simp_ImpL:
  assumes a: "z'♯P" "z'♯M" "z'♯N" "z'♯x"
  shows "fresh_fun (λz'. Cut <c>.P (z').ImpL <a>.M (x).N z') = Cut <c>.P (z').ImpL <a>.M (x).N z'"
using a
apply -
apply(rule fresh_fun_app)
apply(rule pt_name_inst)
apply(rule at_name_inst)
apply(finite_guess)
apply(subgoal_tac "∃n::name. n♯(c,P,x,M,N)")
apply(erule exE)
apply(rule_tac x="n" in exI)
apply(simp add: fresh_prod abs_fresh)
apply(fresh_guess)
apply(rule exists_fresh')
apply(simp add: fin_supp)
apply(fresh_guess)
done

lemma fresh_fun_ImpL[eqvt_force]:
  fixes pi1::"name prm"
  and   pi2::"coname prm"
  shows "pi1∙fresh_fun (λz'. Cut <c>.P (z').ImpL <a>.M (x).N z')=
             fresh_fun (pi1∙(λz'. Cut <c>.P (z').ImpL <a>.M (x).N z'))"
  and   "pi2∙fresh_fun (λz'. Cut <c>.P (z').ImpL <a>.M (x).N z')=
             fresh_fun (pi2∙(λz'. Cut <c>.P (z').ImpL <a>.M (x).N z'))"
apply -
apply(perm_simp)
apply(subgoal_tac "∃n::name. n♯(P,M,N,x,pi1∙P,pi1∙M,pi1∙N,pi1∙x,pi1)")
apply(simp add: fresh_prod)
apply(auto)
apply(simp add: fresh_fun_simp_ImpL at_prm_fresh[OF at_name_inst] swap_simps)
apply(rule exists_fresh')
apply(simp add: fin_supp)
apply(perm_simp)
apply(subgoal_tac "∃n::name. n♯(P,M,N,x,pi2∙P,pi2∙M,pi2∙N,pi2∙x,pi2)")
apply(simp add: fresh_prod)
apply(auto)
apply(simp add: fresh_fun_simp_ImpL calc_atm)
apply(rule exists_fresh')
apply(simp add: fin_supp)
done

lemma fresh_fun_simp_NotR:
  assumes a: "a'♯P" "a'♯M"
  shows "fresh_fun (λa'. Cut <a'>.(NotR (y).M a') (x).P) = Cut <a'>.(NotR (y).M a') (x).P"
using a
apply -
apply(rule fresh_fun_app)
apply(rule pt_coname_inst)
apply(rule at_coname_inst)
apply(finite_guess)
apply(subgoal_tac "∃n::coname. n♯(x,P,y,M)")
apply(erule exE)
apply(rule_tac x="n" in exI)
apply(simp add: fresh_prod abs_fresh)
apply(fresh_guess)
apply(rule exists_fresh')
apply(simp add: fin_supp)
apply(fresh_guess)
done

lemma fresh_fun_NotR[eqvt_force]:
  fixes pi1::"name prm"
  and   pi2::"coname prm"
  shows "pi1∙fresh_fun (λa'. Cut <a'>.(NotR (y).M a') (x).P)=
             fresh_fun (pi1∙(λa'. Cut <a'>.(NotR (y).M a') (x).P))"
  and   "pi2∙fresh_fun (λa'. Cut <a'>.(NotR (y).M a') (x).P)=
             fresh_fun (pi2∙(λa'. Cut <a'>.(NotR (y).M a') (x).P))"
apply -
apply(perm_simp)
apply(subgoal_tac "∃n::coname. n♯(P,M,pi1∙P,pi1∙M,pi1)")
apply(simp add: fresh_prod)
apply(auto)
apply(simp add: fresh_fun_simp_NotR calc_atm)
apply(rule exists_fresh')
apply(simp add: fin_supp)
apply(perm_simp)
apply(subgoal_tac "∃n::coname. n♯(P,M,pi2∙P,pi2∙M,pi2)")
apply(simp add: fresh_prod)
apply(auto)
apply(simp add: fresh_fun_simp_NotR at_prm_fresh[OF at_coname_inst] swap_simps)
apply(rule exists_fresh')
apply(simp add: fin_supp)
done

lemma fresh_fun_simp_AndR:
  assumes a: "a'♯P" "a'♯M" "a'♯N" "a'♯b" "a'♯c"
  shows "fresh_fun (λa'. Cut <a'>.(AndR <b>.M <c>.N a') (x).P) = Cut <a'>.(AndR <b>.M <c>.N a') (x).P"
using a
apply -
apply(rule fresh_fun_app)
apply(rule pt_coname_inst)
apply(rule at_coname_inst)
apply(finite_guess)
apply(subgoal_tac "∃n::coname. n♯(x,P,b,M,c,N)")
apply(erule exE)
apply(rule_tac x="n" in exI)
apply(simp add: fresh_prod abs_fresh)
apply(fresh_guess)
apply(rule exists_fresh')
apply(simp add: fin_supp)
apply(fresh_guess)
done

lemma fresh_fun_AndR[eqvt_force]:
  fixes pi1::"name prm"
  and   pi2::"coname prm"
  shows "pi1∙fresh_fun (λa'. Cut <a'>.(AndR <b>.M <c>.N a') (x).P)=
             fresh_fun (pi1∙(λa'. Cut <a'>.(AndR <b>.M <c>.N a') (x).P))"
  and   "pi2∙fresh_fun (λa'. Cut <a'>.(AndR <b>.M <c>.N a') (x).P)=
             fresh_fun (pi2∙(λa'. Cut <a'>.(AndR <b>.M <c>.N a') (x).P))"
apply -
apply(perm_simp)
apply(subgoal_tac "∃n::coname. n♯(P,M,N,b,c,pi1∙P,pi1∙M,pi1∙N,pi1∙b,pi1∙c,pi1)")
apply(simp add: fresh_prod)
apply(auto)
apply(simp add: fresh_fun_simp_AndR calc_atm)
apply(rule exists_fresh')
apply(simp add: fin_supp)
apply(perm_simp)
apply(subgoal_tac "∃n::coname. n♯(P,M,N,b,c,pi2∙P,pi2∙M,pi2∙N,pi2∙b,pi2∙c,pi2)")
apply(simp add: fresh_prod)
apply(auto)
apply(simp add: fresh_fun_simp_AndR at_prm_fresh[OF at_coname_inst] swap_simps)
apply(rule exists_fresh')
apply(simp add: fin_supp)
done

lemma fresh_fun_simp_OrR1:
  assumes a: "a'♯P" "a'♯M" "a'♯b" 
  shows "fresh_fun (λa'. Cut <a'>.(OrR1 <b>.M a') (x).P) = Cut <a'>.(OrR1 <b>.M a') (x).P"
using a
apply -
apply(rule fresh_fun_app)
apply(rule pt_coname_inst)
apply(rule at_coname_inst)
apply(finite_guess)
apply(subgoal_tac "∃n::coname. n♯(x,P,b,M)")
apply(erule exE)
apply(rule_tac x="n" in exI)
apply(simp add: fresh_prod abs_fresh)
apply(fresh_guess)
apply(rule exists_fresh')
apply(simp add: fin_supp)
apply(fresh_guess)
done

lemma fresh_fun_OrR1[eqvt_force]:
  fixes pi1::"name prm"
  and   pi2::"coname prm"
  shows "pi1∙fresh_fun (λa'. Cut <a'>.(OrR1 <b>.M a') (x).P)=
             fresh_fun (pi1∙(λa'. Cut <a'>.(OrR1 <b>.M  a') (x).P))"
  and   "pi2∙fresh_fun (λa'. Cut <a'>.(OrR1 <b>.M a') (x).P)=
             fresh_fun (pi2∙(λa'. Cut <a'>.(OrR1 <b>.M a') (x).P))"
apply -
apply(perm_simp)
apply(subgoal_tac "∃n::coname. n♯(P,M,b,pi1∙P,pi1∙M,pi1∙b,pi1)")
apply(simp add: fresh_prod)
apply(auto)
apply(simp add: fresh_fun_simp_OrR1 calc_atm)
apply(rule exists_fresh')
apply(simp add: fin_supp)
apply(perm_simp)
apply(subgoal_tac "∃n::coname. n♯(P,M,b,pi2∙P,pi2∙M,pi2∙b,pi2)")
apply(simp add: fresh_prod)
apply(auto)
apply(simp add: fresh_fun_simp_OrR1 at_prm_fresh[OF at_coname_inst] swap_simps)
apply(rule exists_fresh')
apply(simp add: fin_supp)
done

lemma fresh_fun_simp_OrR2:
  assumes a: "a'♯P" "a'♯M" "a'♯b" 
  shows "fresh_fun (λa'. Cut <a'>.(OrR2 <b>.M a') (x).P) = Cut <a'>.(OrR2 <b>.M a') (x).P"
using a
apply -
apply(rule fresh_fun_app)
apply(rule pt_coname_inst)
apply(rule at_coname_inst)
apply(finite_guess)
apply(subgoal_tac "∃n::coname. n♯(x,P,b,M)")
apply(erule exE)
apply(rule_tac x="n" in exI)
apply(simp add: fresh_prod abs_fresh)
apply(fresh_guess)
apply(rule exists_fresh')
apply(simp add: fin_supp)
apply(fresh_guess)
done

lemma fresh_fun_OrR2[eqvt_force]:
  fixes pi1::"name prm"
  and   pi2::"coname prm"
  shows "pi1∙fresh_fun (λa'. Cut <a'>.(OrR2 <b>.M a') (x).P)=
             fresh_fun (pi1∙(λa'. Cut <a'>.(OrR2 <b>.M  a') (x).P))"
  and   "pi2∙fresh_fun (λa'. Cut <a'>.(OrR2 <b>.M a') (x).P)=
             fresh_fun (pi2∙(λa'. Cut <a'>.(OrR2 <b>.M a') (x).P))"
apply -
apply(perm_simp)
apply(subgoal_tac "∃n::coname. n♯(P,M,b,pi1∙P,pi1∙M,pi1∙b,pi1)")
apply(simp add: fresh_prod)
apply(auto)
apply(simp add: fresh_fun_simp_OrR2 calc_atm)
apply(rule exists_fresh')
apply(simp add: fin_supp)
apply(perm_simp)
apply(subgoal_tac "∃n::coname. n♯(P,M,b,pi2∙P,pi2∙M,pi2∙b,pi2)")
apply(simp add: fresh_prod)
apply(auto)
apply(simp add: fresh_fun_simp_OrR2 at_prm_fresh[OF at_coname_inst] swap_simps)
apply(rule exists_fresh')
apply(simp add: fin_supp)
done

lemma fresh_fun_simp_ImpR:
  assumes a: "a'♯P" "a'♯M" "a'♯b" 
  shows "fresh_fun (λa'. Cut <a'>.(ImpR (y).<b>.M a') (x).P) = Cut <a'>.(ImpR (y).<b>.M a') (x).P"
using a
apply -
apply(rule fresh_fun_app)
apply(rule pt_coname_inst)
apply(rule at_coname_inst)
apply(finite_guess)
apply(subgoal_tac "∃n::coname. n♯(x,P,y,b,M)")
apply(erule exE)
apply(rule_tac x="n" in exI)
apply(simp add: fresh_prod abs_fresh)
apply(fresh_guess)
apply(rule exists_fresh')
apply(simp add: fin_supp)
apply(fresh_guess)
done

lemma fresh_fun_ImpR[eqvt_force]:
  fixes pi1::"name prm"
  and   pi2::"coname prm"
  shows "pi1∙fresh_fun (λa'. Cut <a'>.(ImpR (y).<b>.M a') (x).P)=
             fresh_fun (pi1∙(λa'. Cut <a'>.(ImpR (y).<b>.M  a') (x).P))"
  and   "pi2∙fresh_fun (λa'. Cut <a'>.(ImpR (y).<b>.M a') (x).P)=
             fresh_fun (pi2∙(λa'. Cut <a'>.(ImpR (y).<b>.M a') (x).P))"
apply -
apply(perm_simp)
apply(subgoal_tac "∃n::coname. n♯(P,M,b,pi1∙P,pi1∙M,pi1∙b,pi1)")
apply(simp add: fresh_prod)
apply(auto)
apply(simp add: fresh_fun_simp_ImpR calc_atm)
apply(rule exists_fresh')
apply(simp add: fin_supp)
apply(perm_simp)
apply(subgoal_tac "∃n::coname. n♯(P,M,b,pi2∙P,pi2∙M,pi2∙b,pi2)")
apply(simp add: fresh_prod)
apply(auto)
apply(simp add: fresh_fun_simp_ImpR at_prm_fresh[OF at_coname_inst] swap_simps)
apply(rule exists_fresh')
apply(simp add: fin_supp)
done

nominal_primrec (freshness_context: "(y::name,c::coname,P::trm)")
  substn :: "trm ⇒ name   ⇒ coname ⇒ trm ⇒ trm" ("_{_:=<_>._}" [100,100,100,100] 100) 
where
  "(Ax x a){y:=<c>.P} = (if x=y then Cut <c>.P (y).Ax y a else Ax x a)" 
| "⟦a♯(c,P,N);x♯(y,P,M)⟧ ⟹ (Cut <a>.M (x).N){y:=<c>.P} = 
  (if M=Ax y a then Cut <c>.P (x).(N{y:=<c>.P}) else Cut <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}))" 
| "x♯(y,P) ⟹ (NotR (x).M a){y:=<c>.P} = NotR (x).(M{y:=<c>.P}) a" 
| "a♯(c,P) ⟹ (NotL <a>.M x){y:=<c>.P} = 
  (if x=y then fresh_fun (λx'. Cut <c>.P (x').NotL <a>.(M{y:=<c>.P}) x') else NotL <a>.(M{y:=<c>.P}) x)"
| "⟦a♯(c,P,N,d);b♯(c,P,M,d);b≠a⟧ ⟹ 
  (AndR <a>.M <b>.N d){y:=<c>.P} = AndR <a>.(M{y:=<c>.P}) <b>.(N{y:=<c>.P}) d" 
| "x♯(y,P,z) ⟹ (AndL1 (x).M z){y:=<c>.P} = 
  (if z=y then fresh_fun (λz'. Cut <c>.P (z').AndL1 (x).(M{y:=<c>.P}) z') 
   else AndL1 (x).(M{y:=<c>.P}) z)"
| "x♯(y,P,z) ⟹ (AndL2 (x).M z){y:=<c>.P} = 
  (if z=y then fresh_fun (λz'. Cut <c>.P (z').AndL2 (x).(M{y:=<c>.P}) z') 
   else AndL2 (x).(M{y:=<c>.P}) z)"
| "a♯(c,P,b) ⟹ (OrR1 <a>.M b){y:=<c>.P} = OrR1 <a>.(M{y:=<c>.P}) b"
| "a♯(c,P,b) ⟹ (OrR2 <a>.M b){y:=<c>.P} = OrR2 <a>.(M{y:=<c>.P}) b"
| "⟦x♯(y,N,P,z);u♯(y,M,P,z);x≠u⟧ ⟹ (OrL (x).M (u).N z){y:=<c>.P} = 
  (if z=y then fresh_fun (λz'. Cut <c>.P (z').OrL (x).(M{y:=<c>.P}) (u).(N{y:=<c>.P}) z') 
   else OrL (x).(M{y:=<c>.P}) (u).(N{y:=<c>.P}) z)"
| "⟦a♯(b,c,P); x♯(y,P)⟧ ⟹ (ImpR (x).<a>.M b){y:=<c>.P} = ImpR (x).<a>.(M{y:=<c>.P}) b"
| "⟦a♯(N,c,P);x♯(y,P,M,z)⟧ ⟹ (ImpL <a>.M (x).N z){y:=<c>.P} = 
  (if y=z then fresh_fun (λz'. Cut <c>.P (z').ImpL <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}) z') 
   else ImpL <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}) z)"
apply(finite_guess)+
apply(rule TrueI)+
apply(simp add: abs_fresh abs_supp)+
apply(rule impI)
apply(subgoal_tac "∃x::name. x♯(x1,P,y1)", erule exE, simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_NotL abs_fresh fresh_atm)
apply(rule exists_fresh', simp add: fin_supp)
apply(simp add: abs_fresh abs_supp)+
apply(rule impI)
apply(subgoal_tac "∃x::name. x♯(x1,P,y1)", erule exE, simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndL1 abs_fresh fresh_atm)
apply(rule exists_fresh', simp add: fin_supp)
apply(simp add: abs_fresh abs_supp)+
apply(rule impI)
apply(subgoal_tac "∃x::name. x♯(x1,P,y1)", erule exE, simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndL2 abs_fresh fresh_atm)
apply(rule exists_fresh', simp add: fin_supp)
apply(simp add: abs_fresh abs_supp)+
apply(rule impI)
apply(subgoal_tac "∃x::name. x♯(x1,P,y1,x3,y2)", erule exE, simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrL abs_fresh fresh_atm)
apply(rule exists_fresh', simp add: fin_supp)
apply(simp add: abs_fresh abs_supp)+
apply(rule impI)
apply(subgoal_tac "∃x::name. x♯(x1,P,y1,x3,y2)", erule exE, simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrL abs_fresh fresh_atm)
apply(rule exists_fresh', simp add: fin_supp)
apply(simp add: abs_fresh abs_supp)+
apply(rule impI)
apply(subgoal_tac "∃x::name. x♯(x3,P,y1,y2)", erule exE, simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpL abs_fresh fresh_atm)
apply(rule exists_fresh', simp add: fin_supp)
apply(simp add: abs_fresh abs_supp)+
apply(rule impI)
apply(subgoal_tac "∃x::name. x♯(x3,P,y1,y2)", erule exE, simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpL abs_fresh fresh_atm)
apply(rule exists_fresh', simp add: fin_supp)
apply(fresh_guess)+
done

nominal_primrec (freshness_context: "(d::name,z::coname,P::trm)")
  substc :: "trm ⇒ coname ⇒ name   ⇒ trm ⇒ trm" ("_{_:=(_)._}" [100,100,100,100] 100)
where
  "(Ax x a){d:=(z).P} = (if d=a then Cut <a>.(Ax x a) (z).P else Ax x a)" 
| "⟦a♯(d,P,N);x♯(z,P,M)⟧ ⟹ (Cut <a>.M (x).N){d:=(z).P} = 
  (if N=Ax x d then Cut <a>.(M{d:=(z).P}) (z).P else Cut <a>.(M{d:=(z).P}) (x).(N{d:=(z).P}))" 
| "x♯(z,P) ⟹ (NotR (x).M a){d:=(z).P} = 
  (if d=a then fresh_fun (λa'. Cut <a'>.NotR (x).(M{d:=(z).P}) a' (z).P) else NotR (x).(M{d:=(z).P}) a)" 
| "a♯(d,P) ⟹ (NotL <a>.M x){d:=(z).P} = NotL <a>.(M{d:=(z).P}) x" 
| "⟦a♯(P,c,N,d);b♯(P,c,M,d);b≠a⟧ ⟹ (AndR <a>.M <b>.N c){d:=(z).P} = 
  (if d=c then fresh_fun (λa'. Cut <a'>.(AndR <a>.(M{d:=(z).P}) <b>.(N{d:=(z).P}) a') (z).P)
   else AndR <a>.(M{d:=(z).P}) <b>.(N{d:=(z).P}) c)" 
| "x♯(y,z,P) ⟹ (AndL1 (x).M y){d:=(z).P} = AndL1 (x).(M{d:=(z).P}) y"
| "x♯(y,P,z) ⟹ (AndL2 (x).M y){d:=(z).P} = AndL2 (x).(M{d:=(z).P}) y"
| "a♯(d,P,b) ⟹ (OrR1 <a>.M b){d:=(z).P} = 
  (if d=b then fresh_fun (λa'. Cut <a'>.OrR1 <a>.(M{d:=(z).P}) a' (z).P) else OrR1 <a>.(M{d:=(z).P}) b)"
| "a♯(d,P,b) ⟹ (OrR2 <a>.M b){d:=(z).P} = 
  (if d=b then fresh_fun (λa'. Cut <a'>.OrR2 <a>.(M{d:=(z).P}) a' (z).P) else OrR2 <a>.(M{d:=(z).P}) b)"
| "⟦x♯(N,z,P,u);y♯(M,z,P,u);x≠y⟧ ⟹ (OrL (x).M (y).N u){d:=(z).P} = 
  OrL (x).(M{d:=(z).P}) (y).(N{d:=(z).P}) u" 
| "⟦a♯(b,d,P); x♯(z,P)⟧ ⟹ (ImpR (x).<a>.M b){d:=(z).P} = 
  (if d=b then fresh_fun (λa'. Cut <a'>.ImpR (x).<a>.(M{d:=(z).P}) a' (z).P) 
   else ImpR (x).<a>.(M{d:=(z).P}) b)"
| "⟦a♯(N,d,P);x♯(y,z,P,M)⟧ ⟹ (ImpL <a>.M (x).N y){d:=(z).P} = 
  ImpL <a>.(M{d:=(z).P}) (x).(N{d:=(z).P}) y"
apply(finite_guess)+
apply(rule TrueI)+
apply(simp add: abs_fresh abs_supp fs_name1 fs_coname1)+
apply(rule impI)
apply(subgoal_tac "∃x::coname. x♯(x1,P,y1)", erule exE, simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_NotR abs_fresh fresh_atm)
apply(rule exists_fresh', simp add: fin_supp)
apply(simp add: abs_fresh abs_supp)+
apply(rule impI)
apply(subgoal_tac "∃x::coname. x♯(x1,P,y1,x3,y2)", erule exE, simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndR abs_fresh fresh_atm)
apply(rule exists_fresh', simp add: fin_supp)
apply(simp add: abs_fresh abs_supp)+
apply(rule impI)
apply(subgoal_tac "∃x::coname. x♯(x1,P,y1,x3,y2)", erule exE, simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndR abs_fresh fresh_atm)
apply(rule exists_fresh', simp add: fin_supp)
apply(simp add: abs_fresh abs_supp)+
apply(rule impI)
apply(subgoal_tac "∃x::coname. x♯(x1,P,y1)", erule exE, simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrR1 abs_fresh fresh_atm)
apply(rule exists_fresh', simp add: fin_supp)
apply(simp add: abs_fresh abs_supp)+
apply(rule impI)
apply(subgoal_tac "∃x::coname. x♯(x1,P,y1)", erule exE, simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrR2 abs_fresh fresh_atm)
apply(rule exists_fresh', simp add: fin_supp)
apply(simp add: abs_fresh abs_supp)+
apply(rule impI)
apply(subgoal_tac "∃x::coname. x♯(x1,P,x2,y1)", erule exE, simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpR abs_fresh fresh_atm abs_supp)
apply(rule exists_fresh', simp add: fin_supp)
apply(simp add: abs_fresh abs_supp)+
apply(rule impI)
apply(subgoal_tac "∃x::coname. x♯(x1,P,x2,y1)", erule exE, simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpR abs_fresh fresh_atm)
apply(rule exists_fresh', simp add: fin_supp)
apply(simp add: abs_fresh abs_supp)+
apply(fresh_guess add: abs_fresh fresh_prod)+
done

lemma csubst_eqvt[eqvt]:
  fixes pi1::"name prm"
  and   pi2::"coname prm"
  shows "pi1∙(M{c:=(x).N}) = (pi1∙M){(pi1∙c):=(pi1∙x).(pi1∙N)}"
  and   "pi2∙(M{c:=(x).N}) = (pi2∙M){(pi2∙c):=(pi2∙x).(pi2∙N)}"
apply(nominal_induct M avoiding: c x N rule: trm.strong_induct)
apply(auto simp add: eq_bij fresh_bij eqvts)
apply(perm_simp)+
done

lemma nsubst_eqvt[eqvt]:
  fixes pi1::"name prm"
  and   pi2::"coname prm"
  shows "pi1∙(M{x:=<c>.N}) = (pi1∙M){(pi1∙x):=<(pi1∙c)>.(pi1∙N)}"
  and   "pi2∙(M{x:=<c>.N}) = (pi2∙M){(pi2∙x):=<(pi2∙c)>.(pi2∙N)}"
apply(nominal_induct M avoiding: c x N rule: trm.strong_induct)
apply(auto simp add: eq_bij fresh_bij eqvts)
apply(perm_simp)+
done

lemma supp_subst1:
  shows "supp (M{y:=<c>.P}) ⊆ ((supp M) - {y}) ∪ (supp P)"
apply(nominal_induct M avoiding: y P c rule: trm.strong_induct)
apply(auto)
apply(auto simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)+
apply(subgoal_tac "∃x'::name. x'♯(trm{y:=<c>.P},P)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_NotL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "∃x'::name. x'♯(trm{y:=<c>.P},P)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_NotL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(blast)+
apply(subgoal_tac "∃x'::name. x'♯(trm{y:=<c>.P},P,name1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndL1 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "∃x'::name. x'♯(trm{y:=<c>.P},P,name1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndL1 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "∃x'::name. x'♯(trm{y:=<c>.P},P,name1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndL1 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "∃x'::name. x'♯(trm{y:=<c>.P},P,name1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndL2 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "∃x'::name. x'♯(trm{y:=<c>.P},P,name1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndL2 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "∃x'::name. x'♯(trm{y:=<c>.P},P,name1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndL2 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "∃x'::name. x'♯(trm1{y:=<c>.P},P,name1,trm2{y:=<c>.P},name2)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "∃x'::name. x'♯(trm1{y:=<c>.P},P,name1,trm2{y:=<c>.P},name2)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "∃x'::name. x'♯(trm1{y:=<c>.P},P,name1,trm2{y:=<c>.P},name2)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "∃x'::name. x'♯(trm1{y:=<c>.P},P,name1,trm2{y:=<c>.P},name2)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(blast)+
apply(subgoal_tac "∃x'::name. x'♯(trm1{name2:=<c>.P},P,name1,trm2{name2:=<c>.P})")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "∃x'::name. x'♯(trm1{name2:=<c>.P},P,name1,trm2{name2:=<c>.P})")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "∃x'::name. x'♯(trm1{name2:=<c>.P},P,name1,trm2{name2:=<c>.P})")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(blast)+
done

lemma supp_subst2:
  shows "supp (M{y:=<c>.P}) ⊆ supp (M) ∪ ((supp P) - {c})"
apply(nominal_induct M avoiding: y P c rule: trm.strong_induct)
apply(auto)
apply(auto simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)+
apply(subgoal_tac "∃x'::name. x'♯(trm{y:=<c>.P},P)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_NotL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "∃x'::name. x'♯(trm{y:=<c>.P},P)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_NotL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "∃x'::name. x'♯(trm{y:=<c>.P},P)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_NotL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(blast)+
apply(subgoal_tac "∃x'::name. x'♯(trm{y:=<c>.P},P,name1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndL1 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "∃x'::name. x'♯(trm{y:=<c>.P},P,name1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndL1 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "∃x'::name. x'♯(trm{y:=<c>.P},P,name1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndL2 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "∃x'::name. x'♯(trm{y:=<c>.P},P,name1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndL2 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "∃x'::name. x'♯(trm1{y:=<c>.P},P,name1,trm2{y:=<c>.P},name2)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "∃x'::name. x'♯(trm1{y:=<c>.P},P,name1,trm2{y:=<c>.P},name2)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(blast)+
apply(subgoal_tac "∃x'::name. x'♯(trm1{name2:=<c>.P},P,name1,trm2{name2:=<c>.P})")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "∃x'::name. x'♯(trm1{name2:=<c>.P},P,name1,trm2{name2:=<c>.P})")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "∃x'::name. x'♯(trm1{name2:=<c>.P},P,name1,trm2{name2:=<c>.P})")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(subgoal_tac "∃x'::name. x'♯(trm1{name2:=<c>.P},P,name1,trm2{name2:=<c>.P})")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(blast)+
done

lemma supp_subst3:
  shows "supp (M{c:=(x).P}) ⊆ ((supp M) - {c}) ∪ (supp P)"
apply(nominal_induct M avoiding: x P c rule: trm.strong_induct)
apply(auto)
apply(auto simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)+
apply(subgoal_tac "∃x'::coname. x'♯(trm{coname:=(x).P},P)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_NotR abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "∃x'::coname. x'♯(trm{coname:=(x).P},P)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_NotR abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "∃x'::coname. x'♯(trm1{coname3:=(x).P},P,trm2{coname3:=(x).P},coname1,coname2)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndR abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "∃x'::coname. x'♯(trm1{coname3:=(x).P},P,trm2{coname3:=(x).P},coname1,coname2)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndR abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "∃x'::coname. x'♯(trm1{coname3:=(x).P},P,trm2{coname3:=(x).P},coname1,coname2)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndR abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "∃x'::coname. x'♯(trm1{coname3:=(x).P},P,trm2{coname3:=(x).P},coname1,coname2)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndR abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(blast)+
apply(subgoal_tac "∃x'::coname. x'♯(trm{coname2:=(x).P},P,coname1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrR1 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "∃x'::coname. x'♯(trm{coname2:=(x).P},P,coname1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrR1 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "∃x'::coname. x'♯(trm{coname2:=(x).P},P,coname1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrR1 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "∃x'::coname. x'♯(trm{coname2:=(x).P},P,coname1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrR2 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "∃x'::coname. x'♯(trm{coname2:=(x).P},P,coname1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrR2 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "∃x'::coname. x'♯(trm{coname2:=(x).P},P,coname1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrR2 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(blast)+
apply(subgoal_tac "∃x'::coname. x'♯(trm{coname2:=(x).P},P,coname1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpR abs_fresh abs_supp fin_supp fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "∃x'::coname. x'♯(trm{coname2:=(x).P},P,coname1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpR abs_fresh abs_supp fin_supp fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "∃x'::coname. x'♯(trm{coname2:=(x).P},P,coname1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpR abs_fresh abs_supp fin_supp fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(blast)+
done

lemma supp_subst4:
  shows "supp (M{c:=(x).P}) ⊆ (supp M) ∪ ((supp P) - {x})"
apply(nominal_induct M avoiding: x P c rule: trm.strong_induct)
apply(auto)
apply(auto simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)+
apply(subgoal_tac "∃x'::coname. x'♯(trm{coname:=(x).P},P)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_NotR abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "∃x'::coname. x'♯(trm{coname:=(x).P},P)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_NotR abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "∃x'::coname. x'♯(trm{coname:=(x).P},P)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_NotR abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "∃x'::coname. x'♯(trm1{coname3:=(x).P},P,trm2{coname3:=(x).P},coname1,coname2)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndR abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "∃x'::coname. x'♯(trm1{coname3:=(x).P},P,trm2{coname3:=(x).P},coname1,coname2)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndR abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(blast)+
apply(subgoal_tac "∃x'::coname. x'♯(trm{coname2:=(x).P},P,coname1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrR1 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "∃x'::coname. x'♯(trm{coname2:=(x).P},P,coname1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrR1 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "∃x'::coname. x'♯(trm{coname2:=(x).P},P,coname1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrR2 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "∃x'::coname. x'♯(trm{coname2:=(x).P},P,coname1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrR2 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(blast)+
apply(subgoal_tac "∃x'::coname. x'♯(trm{coname2:=(x).P},P,coname1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpR abs_fresh abs_supp fin_supp fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "∃x'::coname. x'♯(trm{coname2:=(x).P},P,coname1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpR abs_fresh abs_supp fin_supp fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "∃x'::coname. x'♯(trm{coname2:=(x).P},P,coname1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpR abs_fresh abs_supp fin_supp fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(blast)+
done

lemma supp_subst5:
  shows "(supp M - {y}) ⊆ supp (M{y:=<c>.P})"
apply(nominal_induct M avoiding: y P c rule: trm.strong_induct)
apply(auto)
apply(auto simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)+
apply(subgoal_tac "∃x'::name. x'♯(trm{y:=<c>.P},P)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_NotL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(blast)
apply(subgoal_tac "∃x'::name. x'♯(trm{y:=<c>.P},P,name1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndL1 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "∃x'::name. x'♯(trm{y:=<c>.P},P,name1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndL2 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "∃x'::name. x'♯(trm1{y:=<c>.P},P,name1,trm2{y:=<c>.P},name2)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "∃x'::name. x'♯(trm1{y:=<c>.P},P,name1,trm2{y:=<c>.P},name2)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(blast)
apply(subgoal_tac "∃x'::name. x'♯(trm1{name2:=<c>.P},P,name1,trm2{name2:=<c>.P})")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "∃x'::name. x'♯(trm1{name2:=<c>.P},P,name1,trm2{name2:=<c>.P})")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(blast)
done

lemma supp_subst6:
  shows "(supp M) ⊆ ((supp (M{y:=<c>.P}))::coname set)"
apply(nominal_induct M avoiding: y P c rule: trm.strong_induct)
apply(auto)
apply(auto simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)+
apply(subgoal_tac "∃x'::name. x'♯(trm{y:=<c>.P},P)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_NotL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(blast)
apply(subgoal_tac "∃x'::name. x'♯(trm{y:=<c>.P},P,name1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndL1 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "∃x'::name. x'♯(trm{y:=<c>.P},P,name1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndL2 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "∃x'::name. x'♯(trm1{y:=<c>.P},P,name1,trm2{y:=<c>.P},name2)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "∃x'::name. x'♯(trm1{y:=<c>.P},P,name1,trm2{y:=<c>.P},name2)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(blast)
apply(subgoal_tac "∃x'::name. x'♯(trm1{name2:=<c>.P},P,name1,trm2{name2:=<c>.P})")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "∃x'::name. x'♯(trm1{name2:=<c>.P},P,name1,trm2{name2:=<c>.P})")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(blast)
done

lemma supp_subst7:
  shows "(supp M - {c}) ⊆  supp (M{c:=(x).P})"
apply(nominal_induct M avoiding: x P c rule: trm.strong_induct)
apply(auto)
apply(auto simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)+
apply(subgoal_tac "∃x'::coname. x'♯(trm{coname:=(x).P},P)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_NotR abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "∃x'::coname. x'♯(trm1{coname3:=(x).P},P,trm2{coname3:=(x).P},coname1,coname2)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndR abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "∃x'::coname. x'♯(trm1{coname3:=(x).P},P,trm2{coname3:=(x).P},coname1,coname2)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndR abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(blast)+
apply(subgoal_tac "∃x'::coname. x'♯(trm{coname2:=(x).P},P,coname1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrR1 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "∃x'::coname. x'♯(trm{coname2:=(x).P},P,coname1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrR2 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(blast)+
apply(subgoal_tac "∃x'::coname. x'♯(trm{coname2:=(x).P},P,coname1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpR abs_fresh abs_supp fin_supp fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(blast)
done

lemma supp_subst8:
  shows "(supp M) ⊆ ((supp (M{c:=(x).P}))::name set)"
apply(nominal_induct M avoiding: x P c rule: trm.strong_induct)
apply(auto)
apply(auto simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)+
apply(subgoal_tac "∃x'::coname. x'♯(trm{coname:=(x).P},P)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_NotR abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "∃x'::coname. x'♯(trm1{coname3:=(x).P},P,trm2{coname3:=(x).P},coname1,coname2)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndR abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "∃x'::coname. x'♯(trm1{coname3:=(x).P},P,trm2{coname3:=(x).P},coname1,coname2)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndR abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(blast)+
apply(subgoal_tac "∃x'::coname. x'♯(trm{coname2:=(x).P},P,coname1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrR1 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "∃x'::coname. x'♯(trm{coname2:=(x).P},P,coname1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrR2 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(blast)
apply(subgoal_tac "∃x'::coname. x'♯(trm{coname2:=(x).P},P,coname1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpR abs_fresh abs_supp fin_supp fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(blast)+
done

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 "x♯P ⟹ x♯M{x:=<c>.P}"   
  and   "b♯P ⟹ b♯M{b:=(y).P}"
  and   "x♯(M,P) ⟹ x♯M{y:=<c>.P}"
  and   "x♯M ⟹ x♯M{c:=(x).P}"
  and   "x♯(M,P) ⟹ x♯M{c:=(y).P}"
  and   "b♯(M,P) ⟹ b♯M{c:=(y).P}"
  and   "b♯M ⟹ b♯M{y:=<b>.P}"
  and   "b♯(M,P) ⟹ b♯M{y:=<c>.P}"
apply -
apply(insert subst_supp)
apply(simp_all add: fresh_def supp_prod)
apply(blast)+ 
done

lemma forget:
  shows "x♯M ⟹ M{x:=<c>.P} = M"
  and   "c♯M ⟹ M{c:=(x).P} = M"
apply(nominal_induct M avoiding: x c P rule: trm.strong_induct)
apply(auto simp add: fresh_atm abs_fresh abs_supp fin_supp)
done

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 (Ax z d)
  then show ?case by (auto simp add: fresh_prod fresh_atm calc_atm trm.inject alpha)
next
  case NotL
  then show ?case by (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
next
  case (NotR y M d)
  then show ?case 
    by(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
next
  case (AndR c1 M c2 M' c3)
  then show ?case
    apply(auto simp add: fresh_prod calc_atm fresh_atm abs_fresh fresh_left)
    apply (metis (erased, hide_lams))
    by metis
next
  case AndL1
  then show ?case by (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
next
  case AndL2
  then show ?case by (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
next
  case (OrR1 d M e)
  then show ?case 
    by(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
next
  case (OrR2 d M e)
  then show ?case 
    by(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
next
  case (OrL x1 M x2 M' x3)
  then show ?case
    by (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
next 
  case ImpL
  then show ?case
    by (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
       metis
next
  case (ImpR y d M e)
  then show ?case
    by(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
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

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 (Ax z d)
  then show ?case 
    by (auto simp add: fresh_prod fresh_atm calc_atm trm.inject alpha perm_swap fresh_left)
next
  case NotL
  then show ?case 
    by (auto simp add: fresh_prod fresh_atm calc_atm trm.inject alpha perm_swap fresh_left)
next
  case (NotR y M d)
  then show ?case
    apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
    apply(subgoal_tac "∃a'::coname. a'♯(N,M{d:=(y).([(y,x)]∙N)},[(y,x)]∙N)")
    apply(erule exE, simp add: fresh_prod)
    apply(erule conjE)+
    apply(simp add: fresh_fun_simp_NotR)
    apply(simp add: trm.inject alpha perm_swap fresh_left calc_atm)
    apply(rule exists_fresh'(2)[OF fs_coname1])
    done
next
  case (AndR c1 M c2 M' c3)
  then show ?case
    apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
    apply(subgoal_tac 
       "∃a'::coname. a'♯(N,M{c3:=(y).([(y,x)]∙N)},M'{c3:=(y).([(y,x)]∙N)},[(y,x)]∙N,c1,c2,c3)")
    apply(erule exE, simp add: fresh_prod)
    apply(erule conjE)+
    apply(simp add: fresh_fun_simp_AndR)
    apply (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh subst_fresh perm_swap fresh_left)
    apply(rule exists_fresh'(2)[OF fs_coname1])
    done
next
  case AndL1
  then show ?case by (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
next
  case AndL2
  then show ?case by (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
next
  case (OrR1 d M e)
  then show ?case 
    apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
    apply(subgoal_tac "∃a'::coname. a'♯(N,M{e:=(y).([(y,x)]∙N)},[(y,x)]∙N,d,e)")
    apply(erule exE, simp add: fresh_prod)
    apply(erule conjE)+
    apply(simp add: fresh_fun_simp_OrR1)
    apply(simp add: trm.inject alpha perm_swap fresh_left calc_atm)
    apply(rule exists_fresh'(2)[OF fs_coname1])
    done
next
  case (OrR2 d M e)
  then show ?case
    apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
    apply(subgoal_tac "∃a'::coname. a'♯(N,M{e:=(y).([(y,x)]∙N)},[(y,x)]∙N,d,e)")
    apply(erule exE, simp add: fresh_prod)
    apply(erule conjE)+
    apply(simp add: fresh_fun_simp_OrR2)
    apply(simp add: trm.inject alpha perm_swap fresh_left calc_atm)
    apply(rule exists_fresh'(2)[OF fs_coname1])
    done
next
  case (OrL x1 M x2 M' x3)
  then show ?case
    by (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
next 
  case ImpL
  then show ?case
    by (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
next
  case (ImpR y d M e)
  then show ?case
    apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
    apply(subgoal_tac "∃a'::coname. a'♯(N,M{e:=(y).([(y,x)]∙N)},[(y,x)]∙N,d,e)")
    apply(erule exE, simp add: fresh_prod)
    apply(erule conjE)+
    apply(simp add: fresh_fun_simp_ImpR)
    apply(simp add: trm.inject alpha perm_swap fresh_left calc_atm)
    apply(rule exists_fresh'(2)[OF fs_coname1])
    done
next
  case (Cut d M y M')
  then show ?case
    by (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left perm_swap)
qed

lemma substn_rename3:
  assumes a: "y♯(M,x)"
  shows "M{x:=<a>.N} = ([(y,x)]∙M){y:=<a>.N}"
using a
proof(nominal_induct M avoiding: a x y N rule: trm.strong_induct)
  case (Ax z d)
  then show ?case by (auto simp add: fresh_prod fresh_atm calc_atm trm.inject alpha)
next
  case NotR
  then show ?case by (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
next
  case (NotL d M z)
  then show ?case 
    by(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
next
  case (AndR c1 M c2 M' c3)
  then show ?case
    by (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
next
  case OrR1
  then show ?case by (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
next
  case OrR2
  then show ?case by (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
next
  case (AndL1 u M v)
  then show ?case 
    by(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
next
  case (AndL2 u M v)
  then show ?case 
    by(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
next
  case (OrL x1 M x2 M' x3)
  then show ?case
    by(simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
      (metis (poly_guards_query))
next 
  case ImpR
  then show ?case
  by(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_left abs_supp fin_supp fresh_prod)
next
  case (ImpL d M v M' u)
  then show ?case
    by(simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
       (metis (poly_guards_query))
next
  case (Cut d M y M')
  then show ?case
    apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
    apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst])
    apply(simp add: calc_atm)
    apply metis
    done
qed

lemma substn_rename4:
  assumes a: "c♯(N,a)"
  shows "M{x:=<a>.N} = M{x:=<c>.([(c,a)]∙N)}"
using a
proof(nominal_induct M avoiding: x c a N rule: trm.strong_induct)
  case (Ax z d)
  then show ?case 
    by (auto simp add: fresh_prod fresh_atm calc_atm trm.inject alpha perm_swap fresh_left)
next
  case NotR
  then show ?case 
    by (auto simp add: fresh_prod fresh_atm calc_atm trm.inject alpha perm_swap fresh_left)
next
  case (NotL d M y)
  then show ?case
    apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
    apply(subgoal_tac "∃a'::name. a'♯(N,M{x:=<c>.([(c,a)]∙N)},[(c,a)]∙N)")
    apply(erule exE, simp add: fresh_prod)
    apply(erule conjE)+
    apply(simp add: fresh_fun_simp_NotL)
    apply(simp add: trm.inject alpha perm_swap fresh_left calc_atm)
    apply(rule exists_fresh'(1)[OF fs_name1])
    done
next
  case (OrL x1 M x2 M' x3)
  then show ?case
    apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
    apply(subgoal_tac 
       "∃a'::name. a'♯(N,M{x:=<c>.([(c,a)]∙N)},M'{x:=<c>.([(c,a)]∙N)},[(c,a)]∙N,x1,x2,x3)")
    apply(erule exE, simp add: fresh_prod)
    apply(erule conjE)+
    apply(simp add: fresh_fun_simp_OrL)
    apply (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh subst_fresh perm_swap fresh_left)
    apply(rule exists_fresh'(1)[OF fs_name1])
    done
next
  case OrR1
  then show ?case by (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
next
  case OrR2
  then show ?case by (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
next
  case (AndL1 u M v)
  then show ?case 
    apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
    apply(subgoal_tac "∃a'::name. a'♯(N,M{x:=<c>.([(c,a)]∙N)},[(c,a)]∙N,u,v)")
    apply(erule exE, simp add: fresh_prod)
    apply(erule conjE)+
    apply(simp add: fresh_fun_simp_AndL1)
    apply(simp add: trm.inject alpha perm_swap fresh_left calc_atm)
    apply(rule exists_fresh'(1)[OF fs_name1])
    done
next
  case (AndL2 u M v)
  then show ?case 
    apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
    apply(subgoal_tac "∃a'::name. a'♯(N,M{x:=<c>.([(c,a)]∙N)},[(c,a)]∙N,u,v)")
    apply(erule exE, simp add: fresh_prod)
    apply(erule conjE)+
    apply(simp add: fresh_fun_simp_AndL2)
    apply(simp add: trm.inject alpha perm_swap fresh_left calc_atm)
    apply(rule exists_fresh'(1)[OF fs_name1])
    done
next
  case (AndR c1 M c2 M' c3)
  then show ?case
    by (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
next 
  case ImpR
  then show ?case
    by (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
next
  case (ImpL d M y M' u)
  then show ?case
    apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
    apply(subgoal_tac "∃a'::name. a'♯(N,M{u:=<c>.([(c,a)]∙N)},M'{u:=<c>.([(c,a)]∙N)},[(c,a)]∙N,y,u)")
    apply(erule exE, simp add: fresh_prod)
    apply(erule conjE)+
    apply(simp add: fresh_fun_simp_ImpL)
    apply(simp add: trm.inject alpha perm_swap fresh_left calc_atm)
    apply(rule exists_fresh'(1)[OF fs_name1])
    done
next
  case (Cut d M y M')
  then show ?case
    by (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left perm_swap)
qed

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

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

lemmas subst_rename = substc_rename1 substc_rename2 substn_rename3 substn_rename4 subst_rename5 subst_rename6

lemma better_Cut_substn[simp]:
  assumes a: "a♯[c].P" "x♯(y,P)"
  shows "(Cut <a>.M (x).N){y:=<c>.P} = 
  (if M=Ax y a then Cut <c>.P (x).(N{y:=<c>.P}) else Cut <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}))"
proof -   
  obtain x'::"name"   where fs1: "x'♯(M,N,c,P,x,y)" by (rule exists_fresh(1), rule fin_supp, blast)
  obtain a'::"coname" where fs2: "a'♯(M,N,c,P,a)" by (rule exists_fresh(2), rule fin_supp, blast)
  have eq1: "(Cut <a>.M (x).N) = (Cut <a'>.([(a',a)]∙M) (x').([(x',x)]∙N))"
    using fs1 fs2 by (rule_tac sym, auto simp add: trm.inject alpha fresh_atm fresh_prod calc_atm)
  have eq2: "(M=Ax y a) = (([(a',a)]∙M)=Ax y a')"
    apply(auto simp add: calc_atm)
    apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])
    apply(simp add: calc_atm)
    done
  have "(Cut <a>.M (x).N){y:=<c>.P} = (Cut <a'>.([(a',a)]∙M) (x').([(x',x)]∙N)){y:=<c>.P}" 
    using eq1 by simp
  also have "… = (if ([(a',a)]∙M)=Ax y a' then Cut <c>.P (x').(([(x',x)]∙N){y:=<c>.P}) 
                              else Cut <a'>.(([(a',a)]∙M){y:=<c>.P}) (x').(([(x',x)]∙N){y:=<c>.P}))" 
    using fs1 fs2 by (auto simp add: fresh_prod fresh_left calc_atm fresh_atm)
  also have "… =(if M=Ax y a then Cut <c>.P (x).(N{y:=<c>.P}) else Cut <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}))"
    using fs1 fs2 a
    apply -
    apply(simp only: eq2[symmetric])
    apply(auto simp add: trm.inject)
    apply(simp_all add: alpha fresh_atm fresh_prod subst_fresh)
    apply(simp_all add: eqvts perm_fresh_fresh calc_atm)
    apply(auto)
    apply(rule subst_rename)
    apply(simp add: fresh_prod fresh_atm)
    apply(simp add: abs_fresh)
    apply(simp add: perm_fresh_fresh)
    done
  finally show ?thesis by simp
qed
    
lemma better_Cut_substc[simp]:
  assumes a: "a♯(c,P)" "x♯[y].P"
  shows "(Cut <a>.M (x).N){c:=(y).P} = 
  (if N=Ax x c then Cut <a>.(M{c:=(y).P}) (y).P else Cut <a>.(M{c:=(y).P}) (x).(N{c:=(y).P}))" 
proof -   
  obtain x'::"name"   where fs1: "x'♯(M,N,c,P,x,y)" by (rule exists_fresh(1), rule fin_supp, blast)
  obtain a'::"coname" where fs2: "a'♯(M,N,c,P,a)" by (rule exists_fresh(2), rule fin_supp, blast)
  have eq1: "(Cut <a>.M (x).N) = (Cut <a'>.([(a',a)]∙M) (x').([(x',x)]∙N))"
    using fs1 fs2 by (rule_tac sym, auto simp add: trm.inject alpha fresh_atm fresh_prod calc_atm)
  have eq2: "(N=Ax x c) = (([(x',x)]∙N)=Ax x' c)"
    apply(auto simp add: calc_atm)
    apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst])
    apply(simp add: calc_atm)
    done
  have "(Cut <a>.M (x).N){c:=(y).P} = (Cut <a'>.([(a',a)]∙M) (x').([(x',x)]∙N)){c:=(y).P}" 
    using eq1 by simp
  also have "… = (if ([(x',x)]∙N)=Ax x' c then  Cut <a'>.(([(a',a)]∙M){c:=(y).P}) (y).P
                              else Cut <a'>.(([(a',a)]∙M){c:=(y).P}) (x').(([(x',x)]∙N){c:=(y).P}))" 
    using fs1 fs2  by (simp add: fresh_prod fresh_left calc_atm fresh_atm trm.inject)
  also have "… =(if N=Ax x c then Cut <a>.(M{c:=(y).P}) (y).P else Cut <a>.(M{c:=(y).P}) (x).(N{c:=(y).P}))"
    using fs1 fs2 a
    apply -
    apply(simp only: eq2[symmetric])
    apply(auto simp add: trm.inject)
    apply(simp_all add: alpha fresh_atm fresh_prod subst_fresh)
    apply(simp_all add: eqvts perm_fresh_fresh calc_atm)
    apply(auto)
    apply(rule subst_rename)
    apply(simp add: fresh_prod fresh_atm)
    apply(simp add: abs_fresh)
    apply(simp add: perm_fresh_fresh)
    done
  finally show ?thesis by simp
qed

lemma better_Cut_substn':
  assumes a: "a♯[c].P" "y♯(N,x)" "M≠Ax y a"
  shows "(Cut <a>.M (x).N){y:=<c>.P} = Cut <a>.(M{y:=<c>.P}) (x).N"
using a
apply -
apply(generate_fresh "name")
apply(subgoal_tac "Cut <a>.M (x).N = Cut <a>.M (ca).([(ca,x)]∙N)")
apply(simp)
apply(subgoal_tac"y♯([(ca,x)]∙N)")
apply(simp add: forget)
apply(simp add: trm.inject)
apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1]
apply(simp add: trm.inject)
apply(rule sym)
apply(simp add: alpha fresh_prod fresh_atm)
done

lemma better_NotR_substc:
  assumes a: "d♯M"
  shows "(NotR (x).M d){d:=(z).P} = fresh_fun (λa'. Cut <a'>.NotR (x).M a' (z).P)"
using a
apply -
apply(generate_fresh "name")
apply(subgoal_tac "NotR (x).M d = NotR (c).([(c,x)]∙M) d")
apply(auto simp add: fresh_left calc_atm forget)
apply(generate_fresh "coname")
apply(rule_tac f="fresh_fun" in arg_cong)
apply(simp add:  fun_eq_iff)
apply(rule allI)
apply(simp add: trm.inject alpha fresh_prod fresh_atm)
apply(perm_simp add: trm.inject alpha fresh_prod fresh_atm fresh_left, auto)
done

lemma better_NotL_substn:
  assumes a: "y♯M"
  shows "(NotL <a>.M y){y:=<c>.P} = fresh_fun (λx'. Cut <c>.P (x').NotL <a>.M x')"
using a
apply -
apply(generate_fresh "coname")
apply(subgoal_tac "NotL <a>.M y = NotL <ca>.([(ca,a)]∙M) y")
apply(auto simp add: fresh_left calc_atm forget)
apply(generate_fresh "name")
apply(rule_tac f="fresh_fun" in arg_cong)
apply(simp add:  fun_eq_iff)
apply(rule allI)
apply(simp add: trm.inject alpha fresh_prod fresh_atm)
apply(perm_simp add: trm.inject alpha fresh_prod fresh_atm fresh_left, auto)
done

lemma better_AndL1_substn:
  assumes a: "y♯[x].M"
  shows "(AndL1 (x).M y){y:=<c>.P} = fresh_fun (λz'. Cut <c>.P (z').AndL1 (x).M z')"
using a
apply -
apply(generate_fresh "name")
apply(subgoal_tac "AndL1 (x).M y = AndL1 (ca).([(ca,x)]∙M) y")
apply(auto simp add: fresh_left calc_atm forget abs_fresh)[1]
apply(generate_fresh "name")
apply(rule_tac f="fresh_fun" in arg_cong)
apply(simp add:  fun_eq_iff)
apply(rule allI)
apply(simp add: trm.inject alpha fresh_prod fresh_atm)
apply(rule forget)
apply(simp add: fresh_left calc_atm)
apply(rule_tac f="fresh_fun" in arg_cong)
apply(simp add:  fun_eq_iff)
apply(rule allI)
apply(simp add: trm.inject alpha fresh_prod fresh_atm)
apply(rule forget)
apply(simp add: fresh_left calc_atm)
apply(perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm)
apply(auto)
done

lemma better_AndL2_substn:
  assumes a: "y♯[x].M"
  shows "(AndL2 (x).M y){y:=<c>.P} = fresh_fun (λz'. Cut <c>.P (z').AndL2 (x).M z')"
using a
apply -
apply(generate_fresh "name")
apply(subgoal_tac "AndL2 (x).M y = AndL2 (ca).([(ca,x)]∙M) y")
apply(auto simp add: fresh_left calc_atm forget abs_fresh)[1]
apply(generate_fresh "name")
apply(rule_tac f="fresh_fun" in arg_cong)
apply(simp add:  fun_eq_iff)
apply(rule allI)
apply(simp add: trm.inject alpha fresh_prod fresh_atm)
apply(rule forget)
apply(simp add: fresh_left calc_atm)
apply(rule_tac f="fresh_fun" in arg_cong)
apply(simp add:  fun_eq_iff)
apply(rule allI)
apply(simp add: trm.inject alpha fresh_prod fresh_atm)
apply(rule forget)
apply(simp add: fresh_left calc_atm)
apply(perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm)
apply(auto)
done

lemma better_AndR_substc:
  assumes a: "c♯([a].M,[b].N)"
  shows "(AndR <a>.M <b>.N c){c:=(z).P} = fresh_fun (λa'. Cut <a'>.(AndR <a>.M <b>.N a') (z).P)"
using a
apply -
apply(generate_fresh "coname")
apply(generate_fresh "coname")
apply(subgoal_tac "AndR <a>.M <b>.N c = AndR <ca>.([(ca,a)]∙M) <caa>.([(caa,b)]∙N) c")
apply(auto simp add: fresh_left calc_atm forget abs_fresh)[1]
apply(rule trans)
apply(rule substc.simps)
apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1]
apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1]
apply(auto simp add: fresh_prod fresh_atm)[1]
apply(simp)
apply(rule_tac f="fresh_fun" in arg_cong)
apply(simp add:  fun_eq_iff)
apply(rule allI)
apply(simp add: trm.inject alpha fresh_prod fresh_atm)
apply(rule conjI)
apply(rule forget)
apply(auto simp add: fresh_left calc_atm abs_fresh)[1]
apply(rule forget)
apply(auto simp add: fresh_left calc_atm abs_fresh)[1]
apply(perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm)
apply(auto)
done

lemma better_OrL_substn:
  assumes a: "x♯([y].M,[z].N)"
  shows "(OrL (y).M (z).N x){x:=<c>.P} = fresh_fun (λz'. Cut <c>.P (z').OrL (y).M (z).N z')"
using a
apply -
apply(generate_fresh "name")
apply(generate_fresh "name")
apply(subgoal_tac "OrL (y).M (z).N x = OrL (ca).([(ca,y)]∙M) (caa).([(caa,z)]∙N) x")
apply(auto simp add: fresh_left calc_atm forget abs_fresh)[1]
apply(rule trans)
apply(rule substn.simps)
apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1]
apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1]
apply(auto simp add: fresh_prod fresh_atm)[1]
apply(simp)
apply(rule_tac f="fresh_fun" in arg_cong)
apply(simp add:  fun_eq_iff)
apply(rule allI)
apply(simp add: trm.inject alpha fresh_prod fresh_atm)
apply(rule conjI)
apply(rule forget)
apply(auto simp add: fresh_left calc_atm abs_fresh)[1]
apply(rule forget)
apply(auto simp add: fresh_left calc_atm abs_fresh)[1]
apply(perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm)
apply(auto)
done

lemma better_OrR1_substc:
  assumes a: "d♯[a].M"
  shows "(OrR1 <a>.M d){d:=(z).P} = fresh_fun (λa'. Cut <a'>.OrR1 <a>.M a' (z).P)"
using a
apply -
apply(generate_fresh "coname")
apply(subgoal_tac "OrR1 <a>.M d = OrR1 <c>.([(c,a)]∙M) d")
apply(auto simp add: fresh_left calc_atm forget abs_fresh)[1]
apply(rule_tac f="fresh_fun" in arg_cong)
apply(simp add:  fun_eq_iff)
apply(rule allI)
apply(simp add: trm.inject alpha fresh_prod fresh_atm)
apply(rule forget)
apply(simp add: fresh_left calc_atm)
apply(rule_tac f="fresh_fun" in arg_cong)
apply(simp add:  fun_eq_iff)
apply(rule allI)
apply(simp add: trm.inject alpha fresh_prod fresh_atm)
apply(rule forget)
apply(simp add: fresh_left calc_atm)
apply(perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm)
apply(auto)
done

lemma better_OrR2_substc:
  assumes a: "d♯[a].M"
  shows "(OrR2 <a>.M d){d:=(z).P} = fresh_fun (λa'. Cut <a'>.OrR2 <a>.M a' (z).P)"
using a
apply -
apply(generate_fresh "coname")
apply(subgoal_tac "OrR2 <a>.M d = OrR2 <c>.([(c,a)]∙M) d")
apply(auto simp add: fresh_left calc_atm forget abs_fresh)[1]
apply(rule_tac f="fresh_fun" in arg_cong)
apply(simp add:  fun_eq_iff)
apply(rule allI)
apply(simp add: trm.inject alpha fresh_prod fresh_atm)
apply(rule forget)
apply(simp add: fresh_left calc_atm)
apply(rule_tac f="fresh_fun" in arg_cong)
apply(simp add:  fun_eq_iff)
apply(rule allI)
apply(simp add: trm.inject alpha fresh_prod fresh_atm)
apply(rule forget)
apply(simp add: fresh_left calc_atm)
apply(perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm)
apply(auto)
done

lemma better_ImpR_substc:
  assumes a: "d♯[a].M"
  shows "(ImpR (x).<a>.M d){d:=(z).P} = fresh_fun (λa'. Cut <a'>.ImpR (x).<a>.M a' (z).P)"
using a
apply -
apply(generate_fresh "coname")
apply(generate_fresh "name")
apply(subgoal_tac "ImpR (x).<a>.M d = ImpR (ca).<c>.([(c,a)]∙[(ca,x)]∙M) d")
apply(auto simp add: fresh_left calc_atm forget abs_fresh)[1]
apply(rule_tac f="fresh_fun" in arg_cong)
apply(simp add:  fun_eq_iff)
apply(rule allI)
apply(simp add: trm.inject alpha fresh_prod fresh_atm abs_perm abs_fresh fresh_left calc_atm)
apply(rule forget)
apply(simp add: fresh_left calc_atm)
apply(rule_tac f="fresh_fun" in arg_cong)
apply(simp add:  fun_eq_iff)
apply(rule allI)
apply(simp add: trm.inject alpha fresh_prod fresh_atm abs_perm fresh_left calc_atm abs_fresh)
apply(rule forget)
apply(simp add: fresh_left calc_atm)
apply(rule sym)
apply(perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm abs_fresh abs_perm)
done

lemma better_ImpL_substn:
  assumes a: "y♯(M,[x].N)"
  shows "(ImpL <a>.M (x).N y){y:=<c>.P} = fresh_fun (λz'. Cut <c>.P (z').ImpL <a>.M (x).N z')"
using a
apply -
apply(generate_fresh "coname")
apply(generate_fresh "name")
apply(subgoal_tac "ImpL <a>.M (x).N y = ImpL <ca>.([(ca,a)]∙M) (caa).([(caa,x)]∙N) y")
apply(auto simp add: fresh_left calc_atm forget abs_fresh)[1]
apply(rule_tac f="fresh_fun" in arg_cong)
apply(simp add:  fun_eq_iff)
apply(rule allI)
apply(simp add: trm.inject alpha fresh_prod fresh_atm abs_perm abs_fresh fresh_left calc_atm)
apply(rule forget)
apply(simp add: fresh_left calc_atm)
apply(auto)[1]
apply(rule sym)
apply(perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm abs_fresh abs_perm)
done

lemma freshn_after_substc:
  fixes x::"name"
  assumes a: "x♯M{c:=(y).P}"
  shows "x♯M"
using a supp_subst8
apply(simp add: fresh_def)
apply(blast)
done

lemma freshn_after_substn:
  fixes x::"name"
  assumes a: "x♯M{y:=<c>.P}" "x≠y"
  shows "x♯M"
using a
using a supp_subst5
apply(simp add: fresh_def)
apply(blast)
done

lemma freshc_after_substc:
  fixes a::"coname"
  assumes a: "a♯M{c:=(y).P}" "a≠c"
  shows "a♯M"
using a supp_subst7
apply(simp add: fresh_def)
apply(blast)
done

lemma freshc_after_substn:
  fixes a::"coname"
  assumes a: "a♯M{y:=<c>.P}" 
  shows "a♯M"
using a supp_subst6
apply(simp add: fresh_def)
apply(blast)
done

lemma substn_crename_comm:
  assumes a: "c≠a" "c≠b"
  shows "M{x:=<c>.P}[a⊢c>b] = M[a⊢c>b]{x:=<c>.(P[a⊢c>b])}"
using a
apply(nominal_induct M avoiding: x c P a b rule: trm.strong_induct)
apply(auto simp add: subst_fresh rename_fresh trm.inject)
apply(subgoal_tac "∃x'::name. x'♯(P,x,c)")
apply(erule exE)
apply(subgoal_tac "Cut <c>.P (x).Ax x a = Cut <c>.P (x').Ax x' a")
apply(simp)
apply(rule trans)
apply(rule crename.simps)
apply(simp add: fresh_prod fresh_atm)
apply(simp)
apply(simp add: trm.inject)
apply(simp add: alpha trm.inject calc_atm fresh_atm)
apply(simp add: trm.inject)
apply(simp add: alpha trm.inject calc_atm fresh_atm)
apply(rule exists_fresh')
apply(rule fin_supp)
apply(rule trans)
apply(rule better_crename_Cut)
apply(simp add: fresh_atm)
apply(simp)
apply(simp add: crename_id)
apply(rule trans)
apply(rule better_crename_Cut)
apply(simp add: fresh_atm fresh_prod)
apply(simp add: rename_fresh fresh_atm)
apply(auto simp add: fresh_atm)[1]
apply(rule trans)
apply(rule better_crename_Cut)
apply(simp add: fresh_atm)
apply(auto simp add: fresh_atm)[1]
apply(drule crename_ax)
apply(simp add: fresh_atm)
apply(simp add: fresh_atm)
apply(simp)
apply(subgoal_tac "∃x'::name. x'♯(trm{x:=<c>.P},P,P[a⊢c>b],x,trm[a⊢c>b]{x:=<c>.P[a⊢c>b]})")
apply(erule exE, simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_NotL)
apply(rule trans)
apply(rule better_crename_Cut)
apply(simp add: fresh_atm fresh_prod)
apply(simp add: rename_fresh fresh_atm)
apply(rule exists_fresh')
apply(rule fin_supp)
apply(subgoal_tac "∃x'::name. x'♯(trm{x:=<c>.P},P,P[a⊢c>b],name1,trm[a⊢c>b]{x:=<c>.P[a⊢c>b]})")
apply(erule exE, simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndL1)
apply(rule trans)
apply(rule better_crename_Cut)
apply(simp add: fresh_atm fresh_prod)
apply(simp add: rename_fresh fresh_atm)
apply(rule exists_fresh')
apply(rule fin_supp)
apply(subgoal_tac "∃x'::name. x'♯(trm{x:=<c>.P},P,P[a⊢c>b],name1,trm[a⊢c>b]{x:=<c>.P[a⊢c>b]})")
apply(erule exE, simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndL2)
apply(rule trans)
apply(rule better_crename_Cut)
apply(simp add: fresh_atm fresh_prod)
apply(simp add: rename_fresh fresh_atm)
apply(rule exists_fresh')
apply(rule fin_supp)
apply(subgoal_tac "∃x'::name. x'♯(trm1{x:=<c>.P},trm2{x:=<c>.P},P,P[a⊢c>b],name1,name2,
                                  trm1[a⊢c>b]{x:=<c>.P[a⊢c>b]},trm2[a⊢c>b]{x:=<c>.P[a⊢c>b]})")
apply(erule exE, simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrL)
apply(rule trans)
apply(rule better_crename_Cut)
apply(simp add: fresh_atm fresh_prod)
apply(simp add: rename_fresh subst_fresh fresh_atm)
apply(rule exists_fresh')
apply(rule fin_supp)
apply(subgoal_tac "∃x'::name. x'♯(trm1{name2:=<c>.P},trm2{name2:=<c>.P},P,P[a⊢c>b],name1,
                                  trm1[a⊢c>b]{name2:=<c>.P[a⊢c>b]},trm2[a⊢c>b]{name2:=<c>.P[a⊢c>b]})")
apply(erule exE, simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpL)
apply(rule trans)
apply(rule better_crename_Cut)
apply(simp add: fresh_atm fresh_prod)
apply(simp add: rename_fresh subst_fresh fresh_atm)
apply(rule exists_fresh')
apply(rule fin_supp)
done

lemma substc_crename_comm:
  assumes a: "c≠a" "c≠b"
  shows "M{c:=(x).P}[a⊢c>b] = M[a⊢c>b]{c:=(x).(P[a⊢c>b])}"
using a
apply(nominal_induct M avoiding: x c P a b rule: trm.strong_induct)
apply(auto simp add: subst_fresh rename_fresh trm.inject)
apply(rule trans)
apply(rule better_crename_Cut)
apply(simp add: fresh_atm fresh_prod)
apply(simp add: rename_fresh fresh_atm)
apply(rule trans)
apply(rule better_crename_Cut)
apply(simp add: fresh_atm fresh_prod)
apply(simp add: rename_fresh fresh_atm)
apply(drule crename_ax)
apply(simp add: fresh_atm)
apply(simp add: fresh_atm)
apply(simp)
apply(subgoal_tac "∃c'::coname. c'♯(a,b,trm{coname:=(x).P},P,P[a⊢c>b],x,trm[a⊢c>b]{coname:=(x).P[a⊢c>b]})")
apply(erule exE, simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_NotR)
apply(rule trans)
apply(rule better_crename_Cut)
apply(simp add: fresh_atm fresh_prod)
apply(simp add: rename_fresh fresh_atm)
apply(rule exists_fresh')
apply(rule fin_supp)
apply(subgoal_tac "∃c'::coname. c'♯(coname1,coname2,a,b,trm1{coname3:=(x).P},trm2{coname3:=(x).P},
                   P,P[a⊢c>b],x,trm1[a⊢c>b]{coname3:=(x).P[a⊢c>b]},trm2[a⊢c>b]{coname3:=(x).P[a⊢c>b]})")
apply(erule exE, simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndR)
apply(rule trans)
apply(rule better_crename_Cut)
apply(simp add: fresh_atm fresh_prod)
apply(simp add: rename_fresh subst_fresh fresh_atm)
apply(rule exists_fresh')
apply(rule fin_supp)
apply(subgoal_tac "∃c'::coname. c'♯(coname1,trm{coname2:=(x).P},P,P[a⊢c>b],a,b,
                         trm[a⊢c>b]{coname2:=(x).P[a⊢c>b]})")
apply(erule exE, simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrR1)
apply(rule trans)
apply(rule better_crename_Cut)
apply(simp add: fresh_atm fresh_prod)
apply(simp add: rename_fresh fresh_atm)
apply(rule exists_fresh')
apply(rule fin_supp)
apply(subgoal_tac "∃c'::coname. c'♯(coname1,trm{coname2:=(x).P},P,P[a⊢c>b],a,b,
                         trm[a⊢c>b]{coname2:=(x).P[a⊢c>b]})")
apply(erule exE, simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrR2)
apply(rule trans)
apply(rule better_crename_Cut)
apply(simp add: fresh_atm fresh_prod)
apply(simp add: rename_fresh fresh_atm)
apply(rule exists_fresh')
apply(rule fin_supp)
apply(subgoal_tac "∃c'::coname. c'♯(coname1,trm{coname2:=(x).P},P,P[a⊢c>b],a,b,
                         trm[a⊢c>b]{coname2:=(x).P[a⊢c>b]})")
apply(erule exE, simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpR)
apply(rule trans)
apply(rule better_crename_Cut)
apply(simp add: fresh_atm fresh_prod)
apply(simp add: rename_fresh fresh_atm)
apply(rule exists_fresh')
apply(rule fin_supp)
done

lemma substn_nrename_comm:
  assumes a: "x≠y" "x≠z"
  shows "M{x:=<c>.P}[y⊢n>z] = M[y⊢n>z]{x:=<c>.(P[y⊢n>z])}"
using a
apply(nominal_induct M avoiding: x c P y z rule: trm.strong_induct)
apply(auto simp add: subst_fresh rename_fresh trm.inject)
apply(rule trans)
apply(rule better_nrename_Cut)
apply(simp add: fresh_prod fresh_atm)
apply(simp add: trm.inject)
apply(rule trans)
apply(rule better_nrename_Cut)
apply(simp add: fresh_atm)
apply(simp)
apply(drule nrename_ax)
apply(simp add: fresh_atm)
apply(simp add: fresh_atm)
apply(simp)
apply(subgoal_tac "∃x'::name. x'♯(y,z,trm{x:=<c>.P},P,P[y⊢n>z],x,trm[y⊢n>z]{x:=<c>.P[y⊢n>z]})")
apply(erule exE, simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_NotL)
apply(rule trans)
apply(rule better_nrename_Cut)
apply(simp add: fresh_atm fresh_prod)
apply(simp add: fresh_atm)
apply(rule exists_fresh')
apply(rule fin_supp)
apply(subgoal_tac "∃x'::name. x'♯(trm{x:=<c>.P},P,P[y⊢n>z],name1,trm[y⊢n>z]{x:=<c>.P[y⊢n>z]},y,z)")
apply(erule exE, simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndL1)
apply(rule trans)
apply(rule better_nrename_Cut)
apply(simp add: fresh_atm fresh_prod)
apply(simp add: rename_fresh fresh_atm)
apply(rule exists_fresh')
apply(rule fin_supp)
apply(subgoal_tac "∃x'::name. x'♯(y,z,trm{x:=<c>.P},P,P[y⊢n>z],name1,trm[y⊢n>z]{x:=<c>.P[y⊢n>z]})")
apply(erule exE, simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndL2)
apply(rule trans)
apply(rule better_nrename_Cut)
apply(simp add: fresh_atm fresh_prod)
apply(simp add: rename_fresh fresh_atm)
apply(rule exists_fresh')
apply(rule fin_supp)
apply(subgoal_tac "∃x'::name. x'♯(trm1{x:=<c>.P},trm2{x:=<c>.P},P,P[y⊢n>z],name1,name2,y,z,
                                  trm1[y⊢n>z]{x:=<c>.P[y⊢n>z]},trm2[y⊢n>z]{x:=<c>.P[y⊢n>z]})")
apply(erule exE, simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrL)
apply(rule trans)
apply(rule better_nrename_Cut)
apply(simp add: fresh_atm fresh_prod)
apply(simp add: rename_fresh subst_fresh fresh_atm)
apply(rule exists_fresh')
apply(rule fin_supp)
apply(subgoal_tac "∃x'::name. x'♯(trm1{name2:=<c>.P},trm2{name2:=<c>.P},P,P[y⊢n>z],y,z,name1,
                                  trm1[y⊢n>z]{name2:=<c>.P[y⊢n>z]},trm2[y⊢n>z]{name2:=<c>.P[y⊢n>z]})")
apply(erule exE, simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpL)
apply(rule trans)
apply(rule better_nrename_Cut)
apply(simp add: fresh_atm fresh_prod)
apply(simp add: rename_fresh subst_fresh fresh_atm)
apply(rule exists_fresh')
apply(rule fin_supp)
done

lemma substc_nrename_comm:
  assumes a: "x≠y" "x≠z"
  shows "M{c:=(x).P}[y⊢n>z] = M[y⊢n>z]{c:=(x).(P[y⊢n>z])}"
using a
apply(nominal_induct M avoiding: x c P y z rule: trm.strong_induct)
apply(auto simp add: subst_fresh rename_fresh trm.inject)
apply(rule trans)
apply(rule better_nrename_Cut)
apply(simp add: fresh_atm fresh_prod)
apply(simp add: rename_fresh fresh_atm)
apply(rule trans)
apply(rule better_nrename_Cut)
apply(simp add: fresh_atm fresh_prod)
apply(simp add: rename_fresh fresh_atm)
apply(rule trans)
apply(rule better_nrename_Cut)
apply(simp add: fresh_atm fresh_prod)
apply(simp add: rename_fresh fresh_atm)
apply(rule trans)
apply(rule better_nrename_Cut)
apply(simp add: fresh_atm fresh_prod)
apply(simp add: rename_fresh fresh_atm)
apply(drule nrename_ax)
apply(simp add: fresh_atm)
apply(simp add: fresh_atm)
apply(simp)
apply(rule trans)
apply(rule better_nrename_Cut)
apply(simp add: fresh_atm fresh_prod)
apply(simp add: rename_fresh fresh_atm)
apply(drule nrename_ax)
apply(simp add: fresh_atm)
apply(simp add: fresh_atm)
apply(simp)
apply(subgoal_tac "∃c'::coname. c'♯(y,z,trm{coname:=(x).P},P,P[y⊢n>z],x,trm[y⊢n>z]{coname:=(x).P[y⊢n>z]})")
apply(erule exE, simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_NotR)
apply(rule trans)
apply(rule better_nrename_Cut)
apply(simp add: fresh_atm fresh_prod)
apply(simp add: rename_fresh fresh_atm)
apply(rule exists_fresh')
apply(rule fin_supp)
apply(subgoal_tac "∃c'::coname. c'♯(coname1,coname2,y,z,trm1{coname3:=(x).P},trm2{coname3:=(x).P},
                   P,P[y⊢n>z],x,trm1[y⊢n>z]{coname3:=(x).P[y⊢n>z]},trm2[y⊢n>z]{coname3:=(x).P[y⊢n>z]})")
apply(erule exE, simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndR)
apply(rule trans)
apply(rule better_nrename_Cut)
apply(simp add: fresh_atm fresh_prod)
apply(simp add: rename_fresh subst_fresh fresh_atm)
apply(rule exists_fresh')
apply(rule fin_supp)
apply(subgoal_tac "∃c'::coname. c'♯(coname1,trm{coname2:=(x).P},P,P[y⊢n>z],y,z,
                         trm[y⊢n>z]{coname2:=(x).P[y⊢n>z]})")
apply(erule exE, simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrR1)
apply(rule trans)
apply(rule better_nrename_Cut)
apply(simp add: fresh_atm fresh_prod)
apply(simp add: rename_fresh fresh_atm)
apply(rule exists_fresh')
apply(rule fin_supp)
apply(subgoal_tac "∃c'::coname. c'♯(coname1,trm{coname2:=(x).P},P,P[y⊢n>z],y,z,
                         trm[y⊢n>z]{coname2:=(x).P[y⊢n>z]})")
apply(erule exE, simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrR2)
apply(rule trans)
apply(rule better_nrename_Cut)
apply(simp add: fresh_atm fresh_prod)
apply(simp add: rename_fresh fresh_atm)
apply(rule exists_fresh')
apply(rule fin_supp)
apply(subgoal_tac "∃c'::coname. c'♯(coname1,trm{coname2:=(x).P},P,P[y⊢n>z],y,z,
                         trm[y⊢n>z]{coname2:=(x).P[y⊢n>z]})")
apply(erule exE, simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpR)
apply(rule trans)
apply(rule better_nrename_Cut)
apply(simp add: fresh_atm fresh_prod)
apply(simp add: rename_fresh fresh_atm)
apply(rule exists_fresh')
apply(rule fin_supp)
done

lemma substn_crename_comm':
  assumes a: "a≠c" "a♯P"
  shows "M{x:=<c>.P}[a⊢c>b] = M[a⊢c>b]{x:=<c>.P}"
using a
proof -
  assume a1: "a≠c"
  assume a2: "a♯P"
  obtain c'::"coname" where fs2: "c'♯(c,P,a,b)" by (rule exists_fresh(2), rule fin_supp, blast)
  have eq: "M{x:=<c>.P} = M{x:=<c'>.([(c',c)]∙P)}"
    using fs2
    apply -
    apply(rule subst_rename)
    apply(simp)
    done
   have eq': "M[a⊢c>b]{x:=<c>.P} = M[a⊢c>b]{x:=<c'>.([(c',c)]∙P)}"
    using fs2
    apply -
    apply(rule subst_rename)
    apply(simp)
    done
  have eq2: "([(c',c)]∙P)[a⊢c>b] = ([(c',c)]∙P)" using fs2 a2 a1
    apply -
    apply(rule rename_fresh)
    apply(simp add: fresh_left calc_atm fresh_prod fresh_atm)
    done
  have "M{x:=<c>.P}[a⊢c>b] = M{x:=<c'>.([(c',c)]∙P)}[a⊢c>b]" using eq by simp
  also have "… = M[a⊢c>b]{x:=<c'>.(([(c',c)]∙P)[a⊢c>b])}"
    using fs2
    apply -
    apply(rule substn_crename_comm)
    apply(simp_all add: fresh_prod fresh_atm)
    done
  also have "… = M[a⊢c>b]{x:=<c'>.(([(c',c)]∙P))}" using eq2 by simp
  also have "… = M[a⊢c>b]{x:=<c>.P}" using eq' by simp 
  finally show ?thesis by simp
qed

lemma substc_crename_comm':
  assumes a: "c≠a" "c≠b" "a♯P"
  shows "M{c:=(x).P}[a⊢c>b] = M[a⊢c>b]{c:=(x).P}"
using a
proof -
  assume a1: "c≠a"
  assume a1': "c≠b"
  assume a2: "a♯P"
  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
    apply -
    apply(rule subst_rename)
    apply(simp)
    done
   have eq': "([(c',c)]∙(M[a⊢c>b])){c':=(x).P} = M[a⊢c>b]{c:=(x).P}"
    using fs2
    apply -
    apply(rule subst_rename[symmetric])
    apply(simp add: rename_fresh)
    done
  have eq2: "([(c',c)]∙M)[a⊢c>b] = ([(c',c)]∙(M[a⊢c>b]))" using fs2 a2 a1 a1'
    apply -
    apply(simp add: rename_eqvts)
    apply(simp add: fresh_left calc_atm fresh_prod fresh_atm)
    done
  have "M{c:=(x).P}[a⊢c>b] = ([(c',c)]∙M){c':=(x).P}[a⊢c>b]" using eq by simp
  also have "… = ([(c',c)]∙M)[a⊢c>b]{c':=(x).P[a⊢c>b]}"
    using fs2
    apply -
    apply(rule substc_crename_comm)
    apply(simp_all add: fresh_prod fresh_atm)
    done
  also have "… = ([(c',c)]∙(M[a⊢c>b])){c':=(x).P[a⊢c>b]}" using eq2 by simp
  also have "… = ([(c',c)]∙(M[a⊢c>b])){c':=(x).P}" using a2 by (simp add: rename_fresh)
  also have "… = M[a⊢c>b]{c:=(x).P}" using eq' by simp
  finally show ?thesis by simp
qed

lemma substn_nrename_comm':
  assumes a: "x≠y" "x≠z" "y♯P"
  shows "M{x:=<c>.P}[y⊢n>z] = M[y⊢n>z]{x:=<c>.P}"
using a
proof -
  assume a1: "x≠y"
  assume a1': "x≠z"
  assume a2: "y♯P"
  obtain x'::"name" where fs2: "x'♯(x,M,y,z)" by (rule exists_fresh(1), rule fin_supp, blast)
  have eq: "M{x:=<c>.P} = ([(x',x)]∙M){x':=<c>.P}"
    using fs2
    apply -
    apply(rule subst_rename)
    apply(simp)
    done
   have eq': "([(x',x)]∙(M[y⊢n>z])){x':=<c>.P} = M[y⊢n>z]{x:=<c>.P}"
    using fs2
    apply -
    apply(rule subst_rename[symmetric])
    apply(simp add: rename_fresh)
    done
  have eq2: "([(x',x)]∙M)[y⊢n>z] = ([(x',x)]∙(M[y⊢n>z]))" using fs2 a2 a1 a1'
    apply -
    apply(simp add: rename_eqvts)
    apply(simp add: fresh_left calc_atm fresh_prod fresh_atm)
    done
  have "M{x:=<c>.P}[y⊢n>z] = ([(x',x)]∙M){x':=<c>.P}[y⊢n>z]" using eq by simp
  also have "… = ([(x',x)]∙M)[y⊢n>z]{x':=<c>.P[y⊢n>z]}"
    using fs2
    apply -
    apply(rule substn_nrename_comm)
    apply(simp_all add: fresh_prod fresh_atm)
    done
  also have "… = ([(x',x)]∙(M[y⊢n>z])){x':=<c>.P[y⊢n>z]}" using eq2 by simp
  also have "… = ([(x',x)]∙(M[y⊢n>z])){x':=<c>.P}" using a2 by (simp add: rename_fresh)
  also have "… = M[y⊢n>z]{x:=<c>.P}" using eq' by simp
  finally show ?thesis by simp
qed

lemma substc_nrename_comm':
  assumes a: "x≠y" "y♯P"
  shows "M{c:=(x).P}[y⊢n>z] = M[y⊢n>z]{c:=(x).P}"
using a
proof -
  assume a1: "x≠y"
  assume a2: "y♯P"
  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
    apply -
    apply(rule subst_rename)
    apply(simp)
    done
   have eq': "M[y⊢n>z]{c:=(x).P} = M[y⊢n>z]{c:=(x').([(x',x)]∙P)}"
    using fs2
    apply -
    apply(rule subst_rename)
    apply(simp)
    done
  have eq2: "([(x',x)]∙P)[y⊢n>z] = ([(x',x)]∙P)" using fs2 a2 a1
    apply -
    apply(rule rename_fresh)
    apply(simp add: fresh_left calc_atm fresh_prod fresh_atm)
    done
  have "M{c:=(x).P}[y⊢n>z] = M{c:=(x').([(x',x)]∙P)}[y⊢n>z]" using eq by simp
  also have "… = M[y⊢n>z]{c:=(x').(([(x',x)]∙P)[y⊢n>z])}"
    using fs2
    apply -
    apply(rule substc_nrename_comm)
    apply(simp_all add: fresh_prod fresh_atm)
    done
  also have "… = M[y⊢n>z]{c:=(x').(([(x',x)]∙P))}" using eq2 by simp
  also have "… = M[y⊢n>z]{c:=(x).P}" using eq' by simp 
  finally show ?thesis by simp
qed

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

text ‹typing contexts›

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

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

equivariance validc

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

equivariance validn

lemma fresh_ctxt:
  fixes a::"coname"
  and   x::"name"
  and   Γ::"ctxtn"
  and   Δ::"ctxtc"
  shows "a♯Γ" and "x♯Δ"
proof -
  show "a♯Γ" by (induct Γ) (auto simp add: fresh_list_nil fresh_list_cons fresh_prod fresh_atm fresh_ty)
next
  show "x♯Δ" by (induct Δ) (auto simp add: 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]: "x♯M ⟹ fin (NotL <a>.M x) x"
| [intro]: "y♯[x].M ⟹ fin (AndL1 (x).M y) y"
| [intro]: "y♯[x].M ⟹ fin (AndL2 (x).M y) y"
| [intro]: "⟦z♯[x].M;z♯[y].N⟧ ⟹ fin (OrL (x).M (y).N z) z"
| [intro]: "⟦y♯M;y♯[x].N⟧ ⟹ fin (ImpL <a>.M (x).N y) y"

equivariance fin

lemma fin_Ax_elim:
  assumes a: "fin (Ax x a) y"
  shows "x=y"
using a
apply(erule_tac fin.cases)
apply(auto simp add: trm.inject)
done

lemma fin_NotL_elim:
  assumes a: "fin (NotL <a>.M x) y"
  shows "x=y ∧ x♯M"
using a
apply(erule_tac fin.cases)
apply(auto simp add: trm.inject)
apply(subgoal_tac "y♯[aa].Ma")
apply(drule sym)
apply(simp_all add: abs_fresh)
done

lemma fin_AndL1_elim:
  assumes a: "fin (AndL1 (x).M y) z"
  shows "z=y ∧ z♯[x].M"
using a
apply(erule_tac fin.cases)
apply(auto simp add: trm.inject)
done

lemma fin_AndL2_elim:
  assumes a: "fin (AndL2 (x).M y) z"
  shows "z=y ∧ z♯[x].M"
using a
apply(erule_tac fin.cases)
apply(auto simp add: trm.inject)
done

lemma fin_OrL_elim:
  assumes a: "fin (OrL (x).M (y).N u) z"
  shows "z=u ∧ z♯[x].M ∧ z♯[y].N"
using a
apply(erule_tac fin.cases)
apply(auto simp add: trm.inject)
done

lemma fin_ImpL_elim:
  assumes a: "fin (ImpL <a>.M (x).N z) y"
  shows "z=y ∧ z♯M ∧ z♯[x].N"
using a
apply(erule_tac fin.cases)
apply(auto simp add: trm.inject)
apply(subgoal_tac "y♯[aa].Ma")
apply(drule sym)
apply(simp_all add: abs_fresh)
done

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

lemmas fin_elims = fin_Ax_elim fin_NotL_elim fin_AndL1_elim fin_AndL2_elim fin_OrL_elim 
                   fin_ImpL_elim fin_rest_elims

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

lemma not_fin_subst1:
  assumes a: "¬(fin M x)" 
  shows "¬(fin (M{c:=(y).P}) x)"
using a
apply(nominal_induct M avoiding: x c y P rule: trm.strong_induct)
apply(auto)
apply(drule fin_elims, simp)
apply(drule fin_elims, simp)
apply(drule fin_elims, simp)
apply(subgoal_tac "∃a'::coname. a'♯(trm{coname:=(y).P},P,x)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_NotR)
apply(erule fin.cases, simp_all add: trm.inject)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(drule fin_elims, simp)
apply(drule fin_elims)
apply(auto)[1]
apply(drule freshn_after_substc)
apply(simp add: fin.intros)
apply(subgoal_tac "∃a'::coname. a'♯(trm1{coname3:=(y).P},trm2{coname3:=(y).P},P,coname1,coname2,coname3,x)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndR)
apply(erule fin.cases, simp_all add: trm.inject)
apply(subgoal_tac "∃a'::coname. a'♯(trm1{coname3:=(y).P},trm2{coname3:=(y).P},P,coname1,coname2,coname3,x)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndR)
apply(erule fin.cases, simp_all add: trm.inject)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(erule fin.cases, simp_all add: trm.inject)
apply(drule fin_AndL1_elim)
apply(auto simp add: abs_fresh)[1]
apply(drule freshn_after_substc)
apply(subgoal_tac "name2♯[name1]. trm")
apply(simp add: fin.intros)
apply(simp add: abs_fresh)
apply(drule fin_AndL2_elim)
apply(auto simp add: abs_fresh)[1]
apply(drule freshn_after_substc)
apply(subgoal_tac "name2♯[name1].trm")
apply(simp add: fin.intros)
apply(simp add: abs_fresh)
apply(subgoal_tac "∃a'::coname. a'♯(trm{coname2:=(y).P},coname1,P,x)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrR1)
apply(erule fin.cases, simp_all add: trm.inject)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(erule fin.cases, simp_all add: trm.inject)
apply(subgoal_tac "∃a'::coname. a'♯(trm{coname2:=(y).P},coname1,P,x)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrR2)
apply(erule fin.cases, simp_all add: trm.inject)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(erule fin.cases, simp_all add: trm.inject)
apply(drule fin_OrL_elim)
apply(auto simp add: abs_fresh)[1]
apply(drule freshn_after_substc)+
apply(subgoal_tac "name3♯[name1].trm1 ∧ name3♯[name2].trm2")
apply(simp add: fin.intros)
apply(simp add: abs_fresh)
apply(subgoal_tac "∃a'::coname. a'♯(trm{coname2:=(y).P},coname1,P,x)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpR)
apply(erule fin.cases, simp_all add: trm.inject)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(erule fin.cases, simp_all add: trm.inject)
apply(drule fin_ImpL_elim)
apply(auto simp add: abs_fresh)[1]
apply(drule freshn_after_substc)+
apply(subgoal_tac "x♯[name1].trm2")
apply(simp add: fin.intros)
apply(simp add: abs_fresh)
done

lemma not_fin_subst2:
  assumes a: "¬(fin M x)" 
  shows "¬(fin (M{y:=<c>.P}) x)"
using a
apply(nominal_induct M avoiding: x c y P rule: trm.strong_induct)
apply(auto)
apply(erule fin.cases, simp_all add: trm.inject)
apply(erule fin.cases, simp_all add: trm.inject)
apply(erule fin.cases, simp_all add: trm.inject)
apply(erule fin.cases, simp_all add: trm.inject)
apply(subgoal_tac "∃a'::name. a'♯(trm{y:=<c>.P},P,x)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_NotL)
apply(erule fin.cases, simp_all add: trm.inject)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(drule fin_NotL_elim)
apply(auto)[1]
apply(drule freshn_after_substn)
apply(simp)
apply(simp add: fin.intros)
apply(erule fin.cases, simp_all add: trm.inject)
apply(subgoal_tac "∃a'::name. a'♯(trm{y:=<c>.P},P,name1,x)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndL1)
apply(erule fin.cases, simp_all add: trm.inject)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(drule fin_AndL1_elim)
apply(auto simp add: abs_fresh)[1]
apply(drule freshn_after_substn)
apply(simp)
apply(subgoal_tac "name2♯[name1]. trm")
apply(simp add: fin.intros)
apply(simp add: abs_fresh)
apply(subgoal_tac "∃a'::name. a'♯(trm{y:=<c>.P},P,name1,x)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndL2)
apply(erule fin.cases, simp_all add: trm.inject)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(drule fin_AndL2_elim)
apply(auto simp add: abs_fresh)[1]
apply(drule freshn_after_substn)
apply(simp)
apply(subgoal_tac "name2♯[name1].trm")
apply(simp add: fin.intros)
apply(simp add: abs_fresh)
apply(erule fin.cases, simp_all add: trm.inject)
apply(erule fin.cases, simp_all add: trm.inject)
apply(subgoal_tac "∃a'::name. a'♯(trm1{y:=<c>.P},trm2{y:=<c>.P},name1,name2,P,x)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrL)
apply(erule fin.cases, simp_all add: trm.inject)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(drule fin_OrL_elim)
apply(auto simp add: abs_fresh)[1]
apply(drule freshn_after_substn)
apply(simp)
apply(drule freshn_after_substn)
apply(simp)
apply(subgoal_tac "name3♯[name1].trm1 ∧ name3♯[name2].trm2")
apply(simp add: fin.intros)
apply(simp add: abs_fresh)
apply(erule fin.cases, simp_all add: trm.inject)
apply(subgoal_tac "∃a'::name. a'♯(trm1{name2:=<c>.P},trm2{name2:=<c>.P},name1,P,x)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpL)
apply(erule fin.cases, simp_all add: trm.inject)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(drule fin_ImpL_elim)
apply(auto simp add: abs_fresh)[1]
apply(drule freshn_after_substn)
apply(simp)
apply(drule freshn_after_substn)
apply(simp)
apply(subgoal_tac "x♯[name1].trm2")
apply(simp add: fin.intros)
apply(simp add: abs_fresh)
done

lemma fin_subst1:
  assumes a: "fin M x" "x≠y" "x♯P"
  shows "fin (M{y:=<c>.P}) x"
using a
apply(nominal_induct M avoiding: x y c P rule: trm.strong_induct)
apply(auto dest!: fin_elims simp add: subst_fresh abs_fresh)
apply(rule fin.intros, simp add: subst_fresh abs_fresh)
apply(