# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1722076868 -3600
# Node ID 7157c61c84616b35c91b6c3b82d31fb28a718b7a
# Parent  49b38572a9f1acf968c430eb0b18ca52cbb04b28
More simplification of apply proofs

diff -r 49b38572a9f1 -r 7157c61c8461 src/HOL/Nominal/Examples/Class1.thy
--- a/src/HOL/Nominal/Examples/Class1.thy	Wed Jul 24 19:08:08 2024 +0100
+++ b/src/HOL/Nominal/Examples/Class1.thy	Sat Jul 27 11:41:08 2024 +0100
@@ -3838,11 +3838,7 @@
       using new by (simp add: fresh_fun_simp_NotL fresh_prod)
     also have "\<dots> \<longrightarrow>\<^sub>a* (NotL <b>.(M{x:=<a>.Ax y a}) x')[x'\<turnstile>n>y]"
       using new 
-      apply(rule_tac a_starI)
-      apply(rule al_redu)
-      apply(rule better_LAxL_intro)
-      apply(auto)
-      done
+      by (intro a_starI al_redu better_LAxL_intro) auto
     also have "\<dots> = NotL <b>.(M{x:=<a>.Ax y a}) y" using new by (simp add: nrename_fresh)
     also have "\<dots> \<longrightarrow>\<^sub>a* NotL <b>.(M[x\<turnstile>n>y]) y" using ih by (auto intro: a_star_congs)
     also have "\<dots> = (NotL <b>.M z)[x\<turnstile>n>y]" using eq by simp
@@ -3880,12 +3876,7 @@
       using new by (simp add: fresh_fun_simp_AndL1 fresh_prod)
     also have "\<dots> \<longrightarrow>\<^sub>a* (AndL1 (u).(M{x:=<a>.Ax y a}) v')[v'\<turnstile>n>y]"
       using new 
-      apply(rule_tac a_starI)
-      apply(rule a_redu.intros)
-      apply(rule better_LAxL_intro)
-      apply(rule fin.intros)
-      apply(simp add: abs_fresh)
-      done
+      by (intro a_starI a_redu.intros better_LAxL_intro fin.intros) (simp add: abs_fresh)
     also have "\<dots> = AndL1 (u).(M{x:=<a>.Ax y a}) y" using fs new
       by (auto simp: fresh_prod fresh_atm nrename_fresh)
     also have "\<dots> \<longrightarrow>\<^sub>a* AndL1 (u).(M[x\<turnstile>n>y]) y" using ih by (auto intro: a_star_congs)
@@ -3914,12 +3905,7 @@
       using new by (simp add: fresh_fun_simp_AndL2 fresh_prod)
     also have "\<dots> \<longrightarrow>\<^sub>a* (AndL2 (u).(M{x:=<a>.Ax y a}) v')[v'\<turnstile>n>y]"
       using new 
-      apply(rule_tac a_starI)
-      apply(rule a_redu.intros)
-      apply(rule better_LAxL_intro)
-      apply(rule fin.intros)
-      apply(simp add: abs_fresh)
-      done
+      by (intro a_starI a_redu.intros better_LAxL_intro fin.intros) (simp add: abs_fresh)
     also have "\<dots> = AndL2 (u).(M{x:=<a>.Ax y a}) y" using fs new
       by (auto simp: fresh_prod fresh_atm nrename_fresh)
     also have "\<dots> \<longrightarrow>\<^sub>a* AndL2 (u).(M[x\<turnstile>n>y]) y" using ih by (auto intro: a_star_congs)
@@ -3964,12 +3950,7 @@
       using new by (simp add: fresh_fun_simp_OrL)
     also have "\<dots> \<longrightarrow>\<^sub>a* (OrL (u).(M{x:=<a>.Ax y a}) (v).(N{x:=<a>.Ax y a}) z')[z'\<turnstile>n>y]"
       using new 
-      apply(rule_tac a_starI)
-      apply(rule a_redu.intros)
-      apply(rule better_LAxL_intro)
-      apply(rule fin.intros)
-      apply(simp_all add: abs_fresh)
-      done
+      by (intro a_starI a_redu.intros better_LAxL_intro fin.intros) (simp_all add: abs_fresh)
     also have "\<dots> = OrL (u).(M{x:=<a>.Ax y a}) (v).(N{x:=<a>.Ax y a}) y" using fs new
       by (auto simp: fresh_prod fresh_atm nrename_fresh subst_fresh)
     also have "\<dots> \<longrightarrow>\<^sub>a* OrL (u).(M[x\<turnstile>n>y]) (v).(N[x\<turnstile>n>y]) y" 
@@ -4010,12 +3991,7 @@
       using new by (simp add: fresh_fun_simp_ImpL)
     also have "\<dots> \<longrightarrow>\<^sub>a* (ImpL <c>.(M{x:=<a>.Ax y a}) (u).(N{x:=<a>.Ax y a}) v')[v'\<turnstile>n>y]"
       using new 
-      apply(rule_tac a_starI)
-      apply(rule a_redu.intros)
-      apply(rule better_LAxL_intro)
-      apply(rule fin.intros)
-      apply(simp_all add: abs_fresh)
-      done
+      by (intro a_starI a_redu.intros better_LAxL_intro fin.intros) (simp_all add: abs_fresh)
     also have "\<dots> = ImpL <c>.(M{x:=<a>.Ax y a}) (u).(N{x:=<a>.Ax y a}) y" using fs new
       by (auto simp: fresh_prod subst_fresh fresh_atm trm.inject alpha rename_fresh)
     also have "\<dots> \<longrightarrow>\<^sub>a* ImpL <c>.(M[x\<turnstile>n>y]) (u).(N[x\<turnstile>n>y]) y" 
@@ -4088,12 +4064,7 @@
       using new by (simp add: fresh_fun_simp_NotR fresh_prod)
     also have "\<dots> \<longrightarrow>\<^sub>a* (NotR (z).(M{b:=(x).Ax x a}) a')[a'\<turnstile>c>a]"
       using new 
-      apply(rule_tac a_starI)
-      apply(rule a_redu.intros)
-      apply(rule better_LAxR_intro)
-      apply(rule fic.intros)
-      apply(simp)
-      done
+      by (intro a_starI a_redu.intros better_LAxR_intro fic.intros) auto
     also have "\<dots> = NotR (z).(M{b:=(x).Ax x a}) a" using new by (simp add: crename_fresh)
     also have "\<dots> \<longrightarrow>\<^sub>a* NotR (z).(M[b\<turnstile>c>a]) a" using ih by (auto intro: a_star_congs)
     also have "\<dots> = (NotR (z).M c)[b\<turnstile>c>a]" using eq by simp
@@ -4130,12 +4101,7 @@
       using new by (simp add: fresh_fun_simp_AndR fresh_prod)
     also have "\<dots> \<longrightarrow>\<^sub>a* (AndR <c>.(M{b:=(x).Ax x a}) <d>.(N{b:=(x).Ax x a}) e')[e'\<turnstile>c>a]"
       using new 
-      apply(rule_tac a_starI)
-      apply(rule a_redu.intros)
-      apply(rule better_LAxR_intro)
-      apply(rule fic.intros)
-      apply(simp_all add: abs_fresh)
-      done
+      by (intro a_starI a_redu.intros better_LAxR_intro fic.intros) (simp_all add: abs_fresh)
     also have "\<dots> = AndR <c>.(M{b:=(x).Ax x a}) <d>.(N{b:=(x).Ax x a}) a" using fs new
       by (auto simp: fresh_prod fresh_atm subst_fresh crename_fresh)
     also have "\<dots> \<longrightarrow>\<^sub>a* AndR <c>.(M[b\<turnstile>c>a]) <d>.(N[b\<turnstile>c>a]) a" using ih1 ih2 by (auto intro: a_star_congs)
@@ -4180,12 +4146,7 @@
       using new by (simp add: fresh_fun_simp_OrR1)
     also have "\<dots> \<longrightarrow>\<^sub>a* (OrR1 <c>.M{b:=(x).Ax x a} a')[a'\<turnstile>c>a]"
       using new 
-      apply(rule_tac a_starI)
-      apply(rule a_redu.intros)
-      apply(rule better_LAxR_intro)
-      apply(rule fic.intros)
-      apply(simp_all add: abs_fresh)
-      done
+      by (intro a_starI a_redu.intros better_LAxR_intro fic.intros) (simp_all add: abs_fresh)
     also have "\<dots> = OrR1 <c>.M{b:=(x).Ax x a} a" using fs new
       by (auto simp: fresh_prod fresh_atm crename_fresh subst_fresh)
     also have "\<dots> \<longrightarrow>\<^sub>a* OrR1 <c>.(M[b\<turnstile>c>a]) a" using ih by (auto intro: a_star_congs)
@@ -4214,12 +4175,7 @@
       using new by (simp add: fresh_fun_simp_OrR2)
     also have "\<dots> \<longrightarrow>\<^sub>a* (OrR2 <c>.M{b:=(x).Ax x a} a')[a'\<turnstile>c>a]"
       using new 
-      apply(rule_tac a_starI)
-      apply(rule a_redu.intros)
-      apply(rule better_LAxR_intro)
-      apply(rule fic.intros)
-      apply(simp_all add: abs_fresh)
-      done
+      by (intro a_starI a_redu.intros better_LAxR_intro fic.intros) (simp_all add: abs_fresh)
     also have "\<dots> = OrR2 <c>.M{b:=(x).Ax x a} a" using fs new
       by (auto simp: fresh_prod fresh_atm crename_fresh subst_fresh)
     also have "\<dots> \<longrightarrow>\<^sub>a* OrR2 <c>.(M[b\<turnstile>c>a]) a" using ih by (auto intro: a_star_congs)
@@ -4257,12 +4213,7 @@
       using new by (simp add: fresh_fun_simp_ImpR)
     also have "\<dots> \<longrightarrow>\<^sub>a* (ImpR z.<c>.M{b:=(x).Ax x a} a')[a'\<turnstile>c>a]"
       using new 
-      apply(rule_tac a_starI)
-      apply(rule a_redu.intros)
-      apply(rule better_LAxR_intro)
-      apply(rule fic.intros)
-      apply(simp_all add: abs_fresh)
-      done
+      by (intro a_starI a_redu.intros better_LAxR_intro fic.intros) (simp_all add: abs_fresh)
     also have "\<dots> = ImpR z.<c>.M{b:=(x).Ax x a} a" using fs new
       by (auto simp: fresh_prod crename_fresh subst_fresh fresh_atm)
     also have "\<dots> \<longrightarrow>\<^sub>a* ImpR z.<c>.(M[b\<turnstile>c>a]) a" using ih by (auto intro: a_star_congs)
@@ -4290,468 +4241,141 @@
 
 text \<open>substitution lemmas\<close>
 
-lemma not_Ax1:
-  shows "\<not>(b\<sharp>M) \<Longrightarrow> M{b:=(y).Q} \<noteq> Ax x a"
-apply(nominal_induct M avoiding: b y Q x a rule: trm.strong_induct)
-apply(auto simp: fresh_atm abs_fresh abs_supp fin_supp)
-apply(subgoal_tac "\<exists>x'::coname. x'\<sharp>(trm{coname:=(y).Q},Q)")
-apply(erule exE)
-apply(simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_NotR abs_fresh fresh_atm)
-apply(rule exists_fresh'(2)[OF fs_coname1])
-apply(subgoal_tac "\<exists>x'::coname. x'\<sharp>(trm{coname:=(y).Q},Q)")
-apply(erule exE)
-apply(simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_NotR abs_fresh fresh_atm)
-apply(rule exists_fresh'(2)[OF fs_coname1])
-apply(subgoal_tac "\<exists>x'::coname. x'\<sharp>(trm1{coname3:=(y).Q},Q,trm2{coname3:=(y).Q},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(rule exists_fresh'(2)[OF fs_coname1])
-apply(subgoal_tac "\<exists>x'::coname. x'\<sharp>(trm1{coname3:=(y).Q},Q,trm2{coname3:=(y).Q},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(rule exists_fresh'(2)[OF fs_coname1])
-apply(subgoal_tac "\<exists>x'::coname. x'\<sharp>(trm1{coname3:=(y).Q},Q,trm2{coname3:=(y).Q},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(rule exists_fresh'(2)[OF fs_coname1])
-apply(subgoal_tac "\<exists>x'::coname. x'\<sharp>(trm{coname2:=(y).Q},Q,coname1)")
-apply(erule exE)
-apply(simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_OrR1 abs_fresh fresh_atm)
-apply(rule exists_fresh'(2)[OF fs_coname1])
-apply(subgoal_tac "\<exists>x'::coname. x'\<sharp>(trm{coname2:=(y).Q},Q,coname1)")
-apply(erule exE)
-apply(simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_OrR1 abs_fresh fresh_atm)
-apply(rule exists_fresh'(2)[OF fs_coname1])
-apply(subgoal_tac "\<exists>x'::coname. x'\<sharp>(trm{coname2:=(y).Q},Q,coname1)")
-apply(erule exE)
-apply(simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_OrR2 abs_fresh fresh_atm)
-apply(rule exists_fresh'(2)[OF fs_coname1])
-apply(subgoal_tac "\<exists>x'::coname. x'\<sharp>(trm{coname2:=(y).Q},Q,coname1)")
-apply(erule exE)
-apply(simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_OrR2 abs_fresh fresh_atm)
-apply(rule exists_fresh'(2)[OF fs_coname1])
-apply(subgoal_tac "\<exists>x'::coname. x'\<sharp>(trm{coname2:=(y).Q},Q,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(rule exists_fresh'(2)[OF fs_coname1])
-apply(subgoal_tac "\<exists>x'::coname. x'\<sharp>(trm{coname2:=(y).Q},Q,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(rule exists_fresh'(2)[OF fs_coname1])
-done
-
-lemma not_Ax2:
-  shows "\<not>(x\<sharp>M) \<Longrightarrow> M{x:=<b>.Q} \<noteq> Ax y a"
-apply(nominal_induct M avoiding: b y Q x a rule: trm.strong_induct)
-apply(auto simp: fresh_atm abs_fresh abs_supp fin_supp)
-apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(trm{x:=<b>.Q},Q)")
-apply(erule exE)
-apply(simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_NotL abs_fresh fresh_atm)
-apply(rule exists_fresh'(1)[OF fs_name1])
-apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(trm{x:=<b>.Q},Q)")
-apply(erule exE)
-apply(simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_NotL abs_fresh fresh_atm)
-apply(rule exists_fresh'(1)[OF fs_name1])
-apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(trm{x:=<b>.Q},Q,name1)")
-apply(erule exE)
-apply(simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_AndL1 abs_fresh fresh_atm)
-apply(rule exists_fresh'(1)[OF fs_name1])
-apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(trm{x:=<b>.Q},Q,name1)")
-apply(erule exE)
-apply(simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_AndL1 abs_fresh fresh_atm)
-apply(rule exists_fresh'(1)[OF fs_name1])
-apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(trm{x:=<b>.Q},Q,name1)")
-apply(erule exE)
-apply(simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_AndL2 abs_fresh fresh_atm)
-apply(rule exists_fresh'(1)[OF fs_name1])
-apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(trm{x:=<b>.Q},Q,name1)")
-apply(erule exE)
-apply(simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_AndL2 abs_fresh fresh_atm)
-apply(rule exists_fresh'(1)[OF fs_name1])
-apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(trm1{x:=<b>.Q},Q,trm2{x:=<b>.Q},name1,name2)")
-apply(erule exE)
-apply(simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_OrL abs_fresh fresh_atm)
-apply(rule exists_fresh'(1)[OF fs_name1])
-apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(trm1{x:=<b>.Q},Q,trm2{x:=<b>.Q},name1,name2)")
-apply(erule exE)
-apply(simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_OrL abs_fresh fresh_atm)
-apply(rule exists_fresh'(1)[OF fs_name1])
-apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(trm1{x:=<b>.Q},Q,trm2{x:=<b>.Q},name1,name2)")
-apply(erule exE)
-apply(simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_OrL abs_fresh fresh_atm)
-apply(rule exists_fresh'(1)[OF fs_name1])
-apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(trm1{name2:=<b>.Q},Q,trm2{name2:=<b>.Q},name1)")
-apply(erule exE)
-apply(simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_ImpL abs_fresh fresh_atm)
-apply(rule exists_fresh'(1)[OF fs_name1])
-apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(trm1{name2:=<b>.Q},Q,trm2{name2:=<b>.Q},name1)")
-apply(erule exE)
-apply(simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_ImpL abs_fresh fresh_atm)
-apply(rule exists_fresh'(1)[OF fs_name1])
-apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(trm1{name2:=<b>.Q},Q,trm2{name2:=<b>.Q},name1)")
-apply(erule exE)
-apply(simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_ImpL abs_fresh fresh_atm)
-apply(rule exists_fresh'(1)[OF fs_name1])
-done
+lemma not_Ax1: "\<not>(b\<sharp>M) \<Longrightarrow> M{b:=(y).Q} \<noteq> Ax x a"
+proof (nominal_induct M avoiding: b y Q x a rule: trm.strong_induct)
+  case (NotR name trm coname)
+  then show ?case
+    by (metis fin.intros(1) fin_rest_elims(2) subst_not_fin2)
+next
+  case (AndR coname1 trm1 coname2 trm2 coname3)
+  then show ?case
+    by (metis fin.intros(1) fin_rest_elims(3) subst_not_fin2)
+next
+  case (OrR1 coname1 trm coname2)
+  then show ?case
+    by (metis fin.intros(1) fin_rest_elims(4) subst_not_fin2)
+next
+  case (OrR2 coname1 trm coname2)
+  then show ?case
+    by (metis fin.intros(1) fin_rest_elims(5) subst_not_fin2)
+next
+  case (ImpR name coname1 trm coname2)
+  then show ?case
+    by (metis fin.intros(1) fin_rest_elims(6) subst_not_fin2)
+qed (auto simp: fresh_atm abs_fresh abs_supp fin_supp)
+
+
+
+lemma not_Ax2: "\<not>(x\<sharp>M) \<Longrightarrow> M{x:=<b>.Q} \<noteq> Ax y a"
+proof (nominal_induct M avoiding: b y Q x a rule: trm.strong_induct)
+  case (NotL coname trm name)
+  then show ?case
+    by (metis fic.intros(1) fic_rest_elims(2) not_fic_subst1)
+next
+  case (AndL1 name1 trm name2)
+  then show ?case
+    by (metis fic.intros(1) fic_rest_elims(4) not_fic_subst1)
+next
+  case (AndL2 name1 trm name2)
+  then show ?case
+    by (metis fic.intros(1) fic_rest_elims(5) not_fic_subst1)
+next
+  case (OrL name1 trm1 name2 trm2 name3)
+  then show ?case
+    by (metis fic.intros(1) fic_rest_elims(3) not_fic_subst1)
+next
+  case (ImpL coname trm1 name1 trm2 name2)
+  then show ?case
+    by (metis fic.intros(1) fic_rest_elims(6) not_fic_subst1)
+qed (auto simp: fresh_atm abs_fresh abs_supp fin_supp)
+
 
 lemma interesting_subst1:
   assumes a: "x\<noteq>y" "x\<sharp>P" "y\<sharp>P" 
   shows "N{y:=<c>.P}{x:=<c>.P} = N{x:=<c>.Ax y c}{y:=<c>.P}"
 using a
 proof(nominal_induct N avoiding: x y c P rule: trm.strong_induct)
-  case Ax
-  then show ?case
-    by (auto simp: abs_fresh fresh_atm forget trm.inject)
-next 
   case (Cut d M u M' x' y' c P)
   with assms show ?case
-    apply(simp)
-    apply(auto)
-    apply(rule trans)
-    apply(rule better_Cut_substn)
-    apply(simp add: abs_fresh)
-    apply(simp)
-    apply(simp)
-    apply(auto)
-    apply(rule sym)
-    apply(rule trans)
-    apply(rule better_Cut_substn)
-    apply(simp add: abs_fresh)
-    apply(simp)
-    apply(simp)
-    apply(simp add: trm.inject alpha forget)
-    apply(rule trans)
-    apply(rule better_Cut_substn)
-    apply(simp add: abs_fresh)
-    apply(simp)
-    apply(simp)
-    apply(auto)
-    apply(rule sym)
-    apply(rule trans)
-    apply(rule better_Cut_substn)
-    apply(simp add: abs_fresh)
-    apply(simp)
-    apply(simp)
-    apply(rule impI)
-    apply(simp add: trm.inject alpha forget)
-    apply(simp add: trm.inject alpha forget)
-    apply(rule trans)
-    apply(rule better_Cut_substn)
-    apply(simp add: abs_fresh)
-    apply(simp)
-    apply(simp)
-    apply(auto)
-    apply(rule sym)
-    apply(rule trans)
-    apply(rule better_Cut_substn)
-    apply(simp add: abs_fresh)
-    apply(simp)
-    apply(simp)
-    apply(rule sym)
-    apply(rule trans)
-    apply(rule better_Cut_substn)
-    apply(simp add: abs_fresh)
-    apply(simp)
-    apply(simp)
-    apply(simp add: trm.inject alpha forget)
-    apply(rule trans)
-    apply(rule better_Cut_substn)
-    apply(simp add: abs_fresh)
-    apply(simp)
-    apply(simp)
-    apply(rule sym)
-    apply(rule trans)
-    apply(rule better_Cut_substn)
-    apply(simp add: abs_fresh)
-    apply(simp)
-    apply(simp)
-    apply(rule trans)
-    apply(rule better_Cut_substn)
-    apply(simp add: abs_fresh)
-    apply(simp)
-    apply(simp)
-    apply(auto)
-    apply(case_tac "y'\<sharp>M")
-    apply(simp add: forget)
-    apply(simp add: not_Ax2)
-    apply(rule sym)
-    apply(rule trans)
-    apply(rule better_Cut_substn)
-    apply(simp add: abs_fresh)
-    apply(simp)
-    apply(simp)
-    apply(auto)
-    apply(case_tac "x'\<sharp>M")
-    apply(simp add: forget)
-    apply(simp add: not_Ax2)
-    done
-next
-  case NotR
-  then show ?case
-    by (auto simp: abs_fresh fresh_atm forget)
+    apply (simp add: abs_fresh)
+    by (smt (verit) forget(1) not_Ax2)
 next
   case (NotL d M u)
+  obtain x'::name and x''::name 
+      where "x' \<sharp> (P,M{y:=<c>.P},M{x:=<c>.Ax y c}{y:=<c>.P},y,x)"
+       and  "x''\<sharp> (P,M{x:=<c>.Ax y c},M{x:=<c>.Ax y c}{y:=<c>.P},Ax y c,y,x)"
+    by (meson exists_fresh(1) fs_name1)
   then show ?case
-    apply (auto simp: abs_fresh fresh_atm forget)
-    apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(P,M{y:=<c>.P},M{x:=<c>.Ax y c}{y:=<c>.P},y,x)")
-    apply(erule exE, simp add: fresh_prod)
-    apply(erule conjE)+
-    apply(simp add: fresh_fun_simp_NotL)
-    apply(rule trans)
-    apply(rule better_Cut_substn)
-    apply(simp add: abs_fresh)
-    apply(simp)
-    apply(simp)
-    apply(auto simp: fresh_atm)
-    apply(simp add: trm.inject alpha forget)
-    apply(rule exists_fresh'(1)[OF fs_name1])
-    apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(P,M{x:=<c>.Ax y c},M{x:=<c>.Ax y c}{y:=<c>.P},Ax y c,y,x)")
-    apply(erule exE, simp only: fresh_prod)
-    apply(erule conjE)+
-    apply(simp only: fresh_fun_simp_NotL)
-    apply(rule sym)
-    apply(rule trans)
-    apply(rule better_Cut_substn)
-    apply(simp add: abs_fresh)
-    apply(simp)
-    apply(simp)
-    apply(simp add: trm.inject alpha forget subst_fresh)
-    apply(rule trans)
-    apply(rule substn.simps)
-    apply(simp add: abs_fresh fresh_prod fresh_atm)
-    apply(simp add: fresh_atm)
-    apply(rule exists_fresh'(1)[OF fs_name1])
-    done
-next
-  case (AndR d1 M d2 M' d3)
-  then show ?case
-    by (auto simp: abs_fresh fresh_atm forget trm.inject subst_fresh)
+    using NotL
+    by (auto simp: perm_fresh_fresh(1) swap_simps(3,7) trm.inject alpha forget 
+           fresh_atm abs_fresh fresh_fun_simp_NotL fresh_prod)
 next
   case (AndL1 u M d)
+  obtain x'::name and x''::name 
+      where "x' \<sharp> (P,M{y:=<c>.P},M{x:=<c>.Ax y c}{y:=<c>.P},u,y,x)"
+       and  "x''\<sharp> (P,Ax y c,M{x:=<c>.Ax y c},M{x:=<c>.Ax y c}{y:=<c>.P},u,y,x)"
+    by (meson exists_fresh(1) fs_name1)
   then show ?case
-    apply(auto simp: abs_fresh fresh_atm forget trm.inject subst_fresh)
-    apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(P,M{y:=<c>.P},M{x:=<c>.Ax y c}{y:=<c>.P},u,y,x)")
-    apply(erule exE, simp add: fresh_prod)
-    apply(erule conjE)+
-    apply(simp add: fresh_fun_simp_AndL1)
-    apply(rule trans)
-    apply(rule better_Cut_substn)
-    apply(simp add: abs_fresh)
-    apply(simp)
-    apply(simp)
-    apply(auto simp: fresh_atm)
-    apply(simp add: trm.inject alpha forget)
-    apply(rule exists_fresh'(1)[OF fs_name1])
-    apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(P,Ax y c,M{x:=<c>.Ax y c},M{x:=<c>.Ax y c}{y:=<c>.P},u,y,x)")
-    apply(erule exE, simp only: fresh_prod)
-    apply(erule conjE)+
-    apply(simp only: fresh_fun_simp_AndL1)
-    apply(rule sym)
-    apply(rule trans)
-    apply(rule better_Cut_substn)
-    apply(simp add: abs_fresh)
-    apply(simp)
-    apply(simp)
-    apply(auto simp: fresh_atm)
-    apply(rule exists_fresh'(1)[OF fs_name1])
-    done
+    using AndL1
+    by (auto simp: perm_fresh_fresh(1) swap_simps(3,7) trm.inject alpha forget 
+           fresh_atm abs_fresh fresh_fun_simp_AndL1 fresh_prod)
 next
   case (AndL2 u M d)
+  obtain x'::name and x''::name 
+      where "x' \<sharp> (P,M{y:=<c>.P},M{x:=<c>.Ax y c}{y:=<c>.P},u,y,x)"
+       and  "x''\<sharp> (P,Ax y c,M{x:=<c>.Ax y c},M{x:=<c>.Ax y c}{y:=<c>.P},u,y,x)"
+    by (meson exists_fresh(1) fs_name1)
   then show ?case
-    apply(auto simp: abs_fresh fresh_atm forget trm.inject subst_fresh)
-    apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(P,M{y:=<c>.P},M{x:=<c>.Ax y c}{y:=<c>.P},u,y,x)")
-    apply(erule exE, simp add: fresh_prod)
-    apply(erule conjE)+
-    apply(simp add: fresh_fun_simp_AndL2)
-    apply(rule trans)
-    apply(rule better_Cut_substn)
-    apply(simp add: abs_fresh)
-    apply(simp)
-    apply(simp)
-    apply(auto simp: fresh_atm)
-    apply(simp add: trm.inject alpha forget)
-    apply(rule exists_fresh'(1)[OF fs_name1])
-    apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(P,Ax y c,M{x:=<c>.Ax y c},M{x:=<c>.Ax y c}{y:=<c>.P},u,y,x)")
-    apply(erule exE, simp only: fresh_prod)
-    apply(erule conjE)+
-    apply(simp only: fresh_fun_simp_AndL2)
-    apply(rule sym)
-    apply(rule trans)
-    apply(rule better_Cut_substn)
-    apply(simp add: abs_fresh)
-    apply(simp)
-    apply(simp)
-    apply(auto simp: fresh_atm)
-    apply(rule exists_fresh'(1)[OF fs_name1])
-    done
-next
-  case OrR1
-  then show ?case
-    by (auto simp: abs_fresh fresh_atm forget trm.inject subst_fresh)
-next
-  case OrR2
-  then show ?case
-    by (auto simp: abs_fresh fresh_atm forget trm.inject subst_fresh)
+    using AndL2
+    by (auto simp: perm_fresh_fresh(1) swap_simps(3,7) trm.inject alpha forget 
+           fresh_atm abs_fresh fresh_fun_simp_AndL2 fresh_prod)
 next
   case (OrL x1 M x2 M' x3)
+  obtain x'::name and x''::name 
+      where "x' \<sharp> (P,M{y:=<c>.P},M{x:=<c>.Ax y c}{y:=<c>.P},
+                       M'{y:=<c>.P},M'{x:=<c>.Ax y c}{y:=<c>.P},x1,x2,x3,y,x)"
+       and  "x''\<sharp> (P,Ax y c,M{x:=<c>.Ax y c},M{x:=<c>.Ax y c}{y:=<c>.P},
+                                        M'{x:=<c>.Ax y c},M'{x:=<c>.Ax y c}{y:=<c>.P},x1,x2,x3,y,x)"
+    by (meson exists_fresh(1) fs_name1)
   then show ?case
-    apply(auto simp: abs_fresh fresh_atm forget trm.inject subst_fresh)
-    apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(P,M{y:=<c>.P},M{x:=<c>.Ax y c}{y:=<c>.P},
-                                        M'{y:=<c>.P},M'{x:=<c>.Ax y c}{y:=<c>.P},x1,x2,x3,y,x)")
-    apply(erule exE, simp add: fresh_prod)
-    apply(erule conjE)+
-    apply(simp add: fresh_fun_simp_OrL)
-    apply(rule trans)
-    apply(rule better_Cut_substn)
-    apply(simp add: abs_fresh)
-    apply(simp)
-    apply(simp)
-    apply(auto simp: fresh_atm)
-    apply(simp add: trm.inject alpha forget)
-    apply(rule trans)
-    apply(rule substn.simps)
-    apply(simp add: abs_fresh subst_fresh fresh_atm)
-    apply(simp add: abs_fresh subst_fresh fresh_atm)
-    apply(force)
-    apply(simp)
-    apply(rule exists_fresh'(1)[OF fs_name1])
-    apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(P,Ax y c,M{x:=<c>.Ax y c},M{x:=<c>.Ax y c}{y:=<c>.P},
-                                        M'{x:=<c>.Ax y c},M'{x:=<c>.Ax y c}{y:=<c>.P},x1,x2,x3,y,x)")
-    apply(erule exE, simp only: fresh_prod)
-    apply(erule conjE)+
-    apply(simp only: fresh_fun_simp_OrL)
-    apply(rule sym)
-    apply(rule trans)
-    apply(rule better_Cut_substn)
-    apply(simp add: abs_fresh)
-    apply(simp)
-    apply(simp)
-    apply(simp add: trm.inject alpha)
-    apply(rule trans)
-    apply(rule substn.simps)
-    apply(simp add: abs_fresh subst_fresh fresh_atm)
-    apply(simp add: abs_fresh subst_fresh fresh_atm)
-    apply(force)
-    apply(simp)
-    apply(auto simp: fresh_atm)
-    apply(rule exists_fresh'(1)[OF fs_name1])
-    done
-next
-  case ImpR
-  then show ?case
-    by (auto simp: abs_fresh fresh_atm forget trm.inject subst_fresh)
+    using OrL
+    by (auto simp: perm_fresh_fresh(1) swap_simps(3,7) trm.inject alpha forget 
+           fresh_atm abs_fresh fresh_fun_simp_OrL fresh_prod subst_fresh)
 next
   case (ImpL a M x1 M' x2)
+  obtain x'::name and x''::name 
+      where "x' \<sharp> (P,M{x2:=<c>.P},M{x:=<c>.Ax x2 c}{x2:=<c>.P},
+                                        M'{x2:=<c>.P},M'{x:=<c>.Ax x2 c}{x2:=<c>.P},x1,y,x)"
+       and  "x''\<sharp> (P,Ax y c,M{x2:=<c>.Ax y c},M{x2:=<c>.Ax y c}{y:=<c>.P},
+                                        M'{x2:=<c>.Ax y c},M'{x2:=<c>.Ax y c}{y:=<c>.P},x1,x2,y,x)"
+    by (meson exists_fresh(1) fs_name1)
   then show ?case
-    apply(auto simp: abs_fresh fresh_atm forget trm.inject subst_fresh)
-    apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(P,M{x2:=<c>.P},M{x:=<c>.Ax x2 c}{x2:=<c>.P},
-                                        M'{x2:=<c>.P},M'{x:=<c>.Ax x2 c}{x2:=<c>.P},x1,y,x)")
-    apply(erule exE, simp add: fresh_prod)
-    apply(erule conjE)+
-    apply(simp add: fresh_fun_simp_ImpL)
-    apply(rule trans)
-    apply(rule better_Cut_substn)
-    apply(simp add: abs_fresh)
-    apply(simp)
-    apply(simp)
-    apply(auto simp: fresh_atm)
-    apply(simp add: trm.inject alpha forget)
-    apply(rule trans)
-    apply(rule substn.simps)
-    apply(simp add: abs_fresh subst_fresh fresh_atm)
-    apply(simp add: abs_fresh subst_fresh fresh_atm)
-    apply(force)
-    apply(rule exists_fresh'(1)[OF fs_name1])
-    apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(P,Ax y c,M{x2:=<c>.Ax y c},M{x2:=<c>.Ax y c}{y:=<c>.P},
-                                        M'{x2:=<c>.Ax y c},M'{x2:=<c>.Ax y c}{y:=<c>.P},x1,x2,y,x)")
-    apply(erule exE, simp only: fresh_prod)
-    apply(erule conjE)+
-    apply(simp only: fresh_fun_simp_ImpL)
-    apply(rule sym)
-    apply(rule trans)
-    apply(rule better_Cut_substn)
-    apply(simp add: abs_fresh)
-    apply(simp)
-    apply(simp)
-    apply(simp add: trm.inject alpha)
-    apply(rule trans)
-    apply(rule substn.simps)
-    apply(simp add: abs_fresh subst_fresh fresh_atm)
-    apply(simp add: abs_fresh subst_fresh fresh_atm)
-    apply(simp)
-    apply(auto simp: fresh_atm)
-    apply(rule exists_fresh'(1)[OF fs_name1])
-    done
-qed 
+    using ImpL
+    by (auto simp: perm_fresh_fresh(1) swap_simps(3,7) trm.inject alpha forget 
+           fresh_atm abs_fresh fresh_fun_simp_ImpL fresh_prod subst_fresh)
+qed (auto simp: abs_fresh fresh_atm forget trm.inject subst_fresh)
 
 lemma interesting_subst1':
-  assumes a: "x\<noteq>y" "x\<sharp>P" "y\<sharp>P" 
+  assumes "x\<noteq>y" "x\<sharp>P" "y\<sharp>P" 
   shows "N{y:=<c>.P}{x:=<c>.P} = N{x:=<a>.Ax y a}{y:=<c>.P}"
 proof -
   show ?thesis
   proof (cases "c=a")
-    case True then show ?thesis using a by (simp add: interesting_subst1)
+    case True with assms show ?thesis 
+      by (simp add: interesting_subst1)
   next
-    case False then show ?thesis using a
-      apply - 
-      apply(subgoal_tac "N{x:=<a>.Ax y a} = N{x:=<c>.([(c,a)]\<bullet>Ax y a)}") 
-      apply(simp add: interesting_subst1 calc_atm)
-      apply(rule subst_rename)
-      apply(simp add: fresh_prod fresh_atm)
-      done
+    case False 
+    then have "N{x:=<a>.Ax y a} = N{x:=<c>.([(c,a)]\<bullet>Ax y a)}"
+      by (simp add: fresh_atm(2,4) fresh_prod substn_rename4)
+    with assms show ?thesis
+      by (simp add: interesting_subst1 swap_simps) 
   qed
 qed
 
 lemma interesting_subst2:
   assumes a: "a\<noteq>b" "a\<sharp>P" "b\<sharp>P" 
   shows "N{a:=(y).P}{b:=(y).P} = N{b:=(y).Ax y a}{a:=(y).P}"
-using a
+  using a
 proof(nominal_induct N avoiding: a b y P rule: trm.strong_induct)
   case Ax
   then show ?case
@@ -4759,144 +4383,34 @@
 next 
   case (Cut d M u M' x' y' c P)
   with assms show ?case
-    apply(simp)
     apply(auto simp: trm.inject)
-    apply(rule trans)
-    apply(rule better_Cut_substc)
-    apply(simp)
-    apply(simp add: abs_fresh)
-    apply(simp add: forget)
-    apply(auto)
-    apply(rule sym)
-    apply(rule trans)
-    apply(rule better_Cut_substc)
-    apply(simp add: abs_fresh)
-    apply(simp add: abs_fresh)
-    apply(simp)
-    apply(rule sym)
-    apply(rule trans)
-    apply(rule better_Cut_substc)
-    apply(simp add: abs_fresh)
-    apply(simp add: abs_fresh) 
-    apply(simp)
-    apply(rule sym)
-    apply(rule trans)
-    apply(rule better_Cut_substc)
-    apply(simp add: abs_fresh)
-    apply(simp add: abs_fresh)
-    apply(simp)
-    apply(rule sym)
-    apply(rule trans)
-    apply(rule better_Cut_substc)
-    apply(simp add: abs_fresh)
-    apply(simp add: abs_fresh)
-    apply(simp)
-    apply(rule trans)
-    apply(rule better_Cut_substc)
-    apply(simp add: abs_fresh)
-    apply(simp add: abs_fresh)
-    apply(auto)[1]
-    apply(rule sym)
-    apply(rule trans)
-    apply(rule better_Cut_substc)
-    apply(simp add: abs_fresh)
-    apply(simp add: abs_fresh)
-    apply(simp)
-    apply(rule impI)
-    apply(simp add: fresh_atm trm.inject alpha forget)
-    apply(case_tac "x'\<sharp>M'")
-    apply(simp add: forget)
-    apply(simp add: not_Ax1)
-    apply(rule sym)
-    apply(rule trans)
-    apply(rule better_Cut_substc)
-    apply(simp add: abs_fresh)
-    apply(simp add: abs_fresh)
-    apply(auto)
-    apply(case_tac "y'\<sharp>M'")
-    apply(simp add: forget)
-    apply(simp add: not_Ax1)
-    done
+      apply (force simp add: abs_fresh forget)
+     apply (simp add: abs_fresh forget)
+    by (smt (verit, ccfv_threshold) abs_fresh(1) better_Cut_substc forget(2) fresh_prod not_Ax1)
 next
   case NotL
   then show ?case
     by (auto simp: abs_fresh fresh_atm forget)
 next
   case (NotR u M d)
-  then show ?case
-    apply (auto simp: abs_fresh fresh_atm forget)
-    apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(b,P,M{d:=(y).P},M{b:=(y).Ax y d}{d:=(y).P},u,y)")
-    apply(erule exE, simp add: fresh_prod)
-    apply(erule conjE)+
-    apply(simp add: fresh_fun_simp_NotR)
-    apply(rule trans)
-    apply(rule better_Cut_substc)
-    apply(simp add: abs_fresh)
-    apply(simp add: abs_fresh)
-    apply(simp)
-    apply(auto simp: fresh_atm)
-    apply(simp add: trm.inject alpha forget)
-    apply(rule exists_fresh'(2)[OF fs_coname1])
-    apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(P,M{d:=(y).Ax y a},M{d:=(y).Ax y a}{a:=(y).P},Ax y a,y,d)")
-    apply(erule exE, simp only: fresh_prod)
-    apply(erule conjE)+
-    apply(simp only: fresh_fun_simp_NotR)
-    apply(rule sym)
-    apply(rule trans)
-    apply(rule better_Cut_substc)
-    apply(simp add: abs_fresh)
-    apply(simp add: abs_fresh)
-    apply(simp)
-    apply(simp add: trm.inject alpha forget subst_fresh)
-    apply(rule trans)
-    apply(rule substc.simps)
-    apply(simp add: abs_fresh fresh_prod fresh_atm)
-    apply(simp add: fresh_atm)
-    apply(rule exists_fresh'(2)[OF fs_coname1])
-    done
+  obtain a' a''::coname 
+      where "a' \<sharp> (b,P,M{d:=(y).P},M{b:=(y).Ax y d}{d:=(y).P},u,y)"
+       and  "a'' \<sharp> (P,M{d:=(y).Ax y a},M{d:=(y).Ax y a}{a:=(y).P},Ax y a,y,d)"
+    by (meson exists_fresh'(2) fs_coname1)
+  with NotR show ?case
+    by (auto simp: abs_fresh fresh_atm forget fresh_prod fresh_fun_simp_NotR)
 next
   case (AndR d1 M d2 M' d3)
-  then show ?case
+  obtain a' a''::coname 
+      where "a' \<sharp> (P,M{d3:=(y).P},M{b:=(y).Ax y d3}{d3:=(y).P},
+                   M'{d3:=(y).P},M'{b:=(y).Ax y d3}{d3:=(y).P},d1,d2,d3,b,y)"
+       and "a'' \<sharp> (P,Ax y a,M{d3:=(y).Ax y a},M{d3:=(y).Ax y a}{a:=(y).P},
+                   M'{d3:=(y).Ax y a},M'{d3:=(y).Ax y a}{a:=(y).P},d1,d2,d3,y,b)"
+    by (meson exists_fresh'(2) fs_coname1)
+  with AndR show ?case
     apply(auto simp: abs_fresh fresh_atm forget trm.inject subst_fresh)
-    apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(P,M{d3:=(y).P},M{b:=(y).Ax y d3}{d3:=(y).P},
-                                        M'{d3:=(y).P},M'{b:=(y).Ax y d3}{d3:=(y).P},d1,d2,d3,b,y)")
-    apply(erule exE, simp add: fresh_prod)
-    apply(erule conjE)+
-    apply(simp add: fresh_fun_simp_AndR)
-    apply(rule trans)
-    apply(rule better_Cut_substc)
-    apply(simp add: abs_fresh fresh_atm)
-    apply(simp add: abs_fresh fresh_atm)
-    apply(simp)
-    apply(auto simp: fresh_atm)
-    apply(simp add: trm.inject alpha forget)
-    apply(rule trans)
-    apply(rule substc.simps)
-    apply(simp add: abs_fresh subst_fresh fresh_atm)
-    apply(simp add: abs_fresh subst_fresh fresh_atm)
-    apply(force)
-    apply(simp)
-    apply(rule exists_fresh'(2)[OF fs_coname1])
-    apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(P,Ax y a,M{d3:=(y).Ax y a},M{d3:=(y).Ax y a}{a:=(y).P},
-                                        M'{d3:=(y).Ax y a},M'{d3:=(y).Ax y a}{a:=(y).P},d1,d2,d3,y,b)")
-    apply(erule exE, simp only: fresh_prod)
-    apply(erule conjE)+
-    apply(simp only: fresh_fun_simp_AndR)
-    apply(rule sym)
-    apply(rule trans)
-    apply(rule better_Cut_substc)
-    apply(simp add: abs_fresh)
-    apply(simp add: abs_fresh)
-    apply(simp)
-    apply(simp add: trm.inject alpha)
-    apply(rule trans)
-    apply(rule substc.simps)
-    apply(simp add: abs_fresh subst_fresh fresh_atm)
-    apply(simp add: abs_fresh subst_fresh fresh_atm)
-    apply(force)
-    apply(simp)
-    apply(auto simp: fresh_atm)
-    apply(rule exists_fresh'(2)[OF fs_coname1])
+    apply(auto simp only: fresh_prod fresh_fun_simp_AndR)
+     apply (force simp:  forget abs_fresh subst_fresh fresh_atm)+
     done
 next
   case (AndL1 u M d)
@@ -4908,70 +4422,20 @@
     by (auto simp: abs_fresh fresh_atm forget trm.inject subst_fresh)
 next
   case (OrR1 d M e)
-  then show ?case
-    apply (auto simp: abs_fresh fresh_atm forget)
-    apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(b,P,M{e:=(y).P},M{b:=(y).Ax y e}{e:=(y).P},d,e)")
-    apply(erule exE, simp add: fresh_prod)
-    apply(erule conjE)+
-    apply(simp add: fresh_fun_simp_OrR1)
-    apply(rule trans)
-    apply(rule better_Cut_substc)
-    apply(simp add: abs_fresh)
-    apply(simp add: abs_fresh)
-    apply(simp)
-    apply(auto simp: fresh_atm)
-    apply(simp add: trm.inject alpha forget)
-    apply(rule exists_fresh'(2)[OF fs_coname1])
-    apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(b,P,Ax y a,M{e:=(y).Ax y a},M{e:=(y).Ax y a}{a:=(y).P},d,e)")
-    apply(erule exE, simp only: fresh_prod)
-    apply(erule conjE)+
-    apply(simp only: fresh_fun_simp_OrR1)
-    apply(rule sym)
-    apply(rule trans)
-    apply(rule better_Cut_substc)
-    apply(simp add: abs_fresh)
-    apply(simp add: abs_fresh)
-    apply(simp)
-    apply(simp add: trm.inject alpha forget subst_fresh)
-    apply(rule trans)
-    apply(rule substc.simps)
-    apply(simp add: abs_fresh fresh_prod fresh_atm)
-    apply(simp add: fresh_atm)
-    apply(rule exists_fresh'(2)[OF fs_coname1])
-    done
+  obtain a' a''::coname 
+    where "a' \<sharp> (b,P,M{e:=(y).P},M{b:=(y).Ax y e}{e:=(y).P},d,e)"
+       and  "a'' \<sharp> (b,P,Ax y a,M{e:=(y).Ax y a},M{e:=(y).Ax y a}{a:=(y).P},d,e)"
+    by (meson exists_fresh'(2) fs_coname1)
+  with OrR1 show ?case
+    by (auto simp: abs_fresh fresh_atm forget fresh_prod fresh_fun_simp_OrR1)
 next
   case (OrR2 d M e)
-  then show ?case
-    apply (auto simp: abs_fresh fresh_atm forget)
-    apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(b,P,M{e:=(y).P},M{b:=(y).Ax y e}{e:=(y).P},d,e)")
-    apply(erule exE, simp add: fresh_prod)
-    apply(erule conjE)+
-    apply(simp add: fresh_fun_simp_OrR2)
-    apply(rule trans)
-    apply(rule better_Cut_substc)
-    apply(simp add: abs_fresh)
-    apply(simp add: abs_fresh)
-    apply(simp)
-    apply(auto simp: fresh_atm)
-    apply(simp add: trm.inject alpha forget)
-    apply(rule exists_fresh'(2)[OF fs_coname1])
-    apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(b,P,Ax y a,M{e:=(y).Ax y a},M{e:=(y).Ax y a}{a:=(y).P},d,e)")
-    apply(erule exE, simp only: fresh_prod)
-    apply(erule conjE)+
-    apply(simp only: fresh_fun_simp_OrR2)
-    apply(rule sym)
-    apply(rule trans)
-    apply(rule better_Cut_substc)
-    apply(simp add: abs_fresh)
-    apply(simp add: abs_fresh)
-    apply(simp)
-    apply(simp add: trm.inject alpha forget subst_fresh)
-    apply(rule trans)
-    apply(rule substc.simps)
-    apply(simp add: abs_fresh fresh_prod fresh_atm)
-    apply(simp add: fresh_atm)
-    apply(rule exists_fresh'(2)[OF fs_coname1])
-    done
+  obtain a' a''::coname 
+    where "a' \<sharp> (b,P,M{e:=(y).P},M{b:=(y).Ax y e}{e:=(y).P},d,e)"
+       and  "a'' \<sharp> (b,P,Ax y a,M{e:=(y).Ax y a},M{e:=(y).Ax y a}{a:=(y).P},d,e)"
+    by (meson exists_fresh'(2) fs_coname1)
+  with OrR2 show ?case
+    by (auto simp: abs_fresh fresh_atm forget fresh_prod fresh_fun_simp_OrR2)
 next
   case (OrL x1 M x2 M' x3)
   then show ?case
@@ -4982,56 +4446,27 @@
     by (auto simp: abs_fresh fresh_atm forget trm.inject subst_fresh)
 next
   case (ImpR u e M d)
-  then show ?case
-    apply(auto simp: abs_fresh fresh_atm forget trm.inject subst_fresh)
-    apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(b,e,d,P,M{d:=(y).P},M{b:=(y).Ax y d}{d:=(y).P})")
-    apply(erule exE, simp add: fresh_prod)
-    apply(erule conjE)+
-    apply(simp add: fresh_fun_simp_ImpR)
-    apply(rule trans)
-    apply(rule better_Cut_substc)
-    apply(simp add: abs_fresh)
-    apply(simp add: abs_fresh)
-    apply(simp)
-    apply(auto simp: fresh_atm)
-    apply(simp add: trm.inject alpha forget)
-    apply(rule exists_fresh'(2)[OF fs_coname1])
-    apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(e,d,P,Ax y a,M{d:=(y).Ax y a},M{d:=(y).Ax y a}{a:=(y).P})")
-    apply(erule exE, simp only: fresh_prod)
-    apply(erule conjE)+
-    apply(simp only: fresh_fun_simp_ImpR)
-    apply(rule sym)
-    apply(rule trans)
-    apply(rule better_Cut_substc)
-    apply(simp add: abs_fresh)
-    apply(simp add: abs_fresh)
-    apply(simp)
-    apply(simp add: trm.inject alpha)
-    apply(rule trans)
-    apply(rule substc.simps)
-    apply(simp add: abs_fresh subst_fresh fresh_atm)
-    apply(simp add: abs_fresh subst_fresh fresh_atm)
-    apply(simp)
-    apply(auto simp: fresh_atm)
-    apply(rule exists_fresh'(2)[OF fs_coname1])
-    done
+  obtain a' a''::coname 
+    where "a' \<sharp> (b,e,d,P,M{d:=(y).P},M{b:=(y).Ax y d}{d:=(y).P})"
+       and  "a'' \<sharp> (e,d,P,Ax y a,M{d:=(y).Ax y a},M{d:=(y).Ax y a}{a:=(y).P})"
+    by (meson exists_fresh'(2) fs_coname1)
+  with ImpR show ?case
+    by (auto simp: abs_fresh fresh_atm forget fresh_prod fresh_fun_simp_ImpR)
 qed 
 
 lemma interesting_subst2':
-  assumes a: "a\<noteq>b" "a\<sharp>P" "b\<sharp>P" 
+  assumes "a\<noteq>b" "a\<sharp>P" "b\<sharp>P" 
   shows "N{a:=(y).P}{b:=(y).P} = N{b:=(z).Ax z a}{a:=(y).P}"
 proof -
   show ?thesis
   proof (cases "z=y")
-    case True then show ?thesis using a by (simp add: interesting_subst2)
+    case True then show ?thesis using assms by (simp add: interesting_subst2)
   next
-    case False then show ?thesis using a
-      apply - 
-      apply(subgoal_tac "N{b:=(z).Ax z a} = N{b:=(y).([(y,z)]\<bullet>Ax z a)}") 
-      apply(simp add: interesting_subst2 calc_atm)
-      apply(rule subst_rename)
-      apply(simp add: fresh_prod fresh_atm)
-      done
+    case False 
+    then have "N{b:=(z).Ax z a} = N{b:=(y).([(y,z)]\<bullet>Ax z a)}"
+      by (metis fresh_atm(1,3) fresh_prod substc_rename2 trm.fresh(1))
+    with False assms show ?thesis
+      by (simp add: interesting_subst2 calc_atm)
   qed
 qed