# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1713650567 -3600
# Node ID fec5a23017b55f7c7f85f021c361088c63830f5d
# Parent  a30a1385f7d0c2a018eaca1cdc8f5939e2b11cab
Tidying up more messy proofs

diff -r a30a1385f7d0 -r fec5a23017b5 src/HOL/Nominal/Examples/Class1.thy
--- a/src/HOL/Nominal/Examples/Class1.thy	Sat Apr 20 12:08:01 2024 +0100
+++ b/src/HOL/Nominal/Examples/Class1.thy	Sat Apr 20 23:02:47 2024 +0100
@@ -189,8 +189,7 @@
   shows "([(x',x)]\<bullet>M)[x'\<turnstile>n>y]= M[x\<turnstile>n>y]"
 using a
 apply(nominal_induct M avoiding: x x' y rule: trm.strong_induct)
-apply(auto simp: abs_fresh fresh_bij fresh_atm fresh_prod fresh_right calc_atm abs_supp fin_supp)
-apply(auto simp: fresh_left calc_atm fresh_prod fresh_atm)
+ apply(auto simp: abs_fresh abs_supp fin_supp fresh_left calc_atm fresh_atm)
 done
 
 lemma crename_rename:
@@ -198,8 +197,7 @@
   shows "([(a',a)]\<bullet>M)[a'\<turnstile>c>b]= M[a\<turnstile>c>b]"
 using a
 apply(nominal_induct M avoiding: a a' b rule: trm.strong_induct)
-apply(auto simp: abs_fresh fresh_bij fresh_atm fresh_prod fresh_right calc_atm abs_supp fin_supp)
-apply(auto simp: fresh_left calc_atm fresh_prod fresh_atm)
+ apply(auto simp: abs_fresh abs_supp fin_supp fresh_left calc_atm fresh_atm)
 done
 
 lemmas rename_fresh = nrename_fresh crename_fresh 
@@ -254,12 +252,14 @@
 lemma nrename_swap:
   shows "x\<sharp>M \<Longrightarrow> [(x,y)]\<bullet>M = M[y\<turnstile>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)
+   (auto simp: abs_fresh abs_supp fin_supp fresh_left calc_atm fresh_atm)
+
 
 lemma crename_swap:
   shows "a\<sharp>M \<Longrightarrow> [(a,b)]\<bullet>M = M[b\<turnstile>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)
+   (auto simp: abs_fresh abs_supp fin_supp fresh_left calc_atm fresh_atm)
+
 
 lemma crename_ax:
   assumes a: "M[a\<turnstile>c>b] = Ax x c" "c\<noteq>a" "c\<noteq>b"
@@ -744,748 +744,333 @@
   and   pi2::"coname prm"
   shows "pi1\<bullet>(M{c:=(x).N}) = (pi1\<bullet>M){(pi1\<bullet>c):=(pi1\<bullet>x).(pi1\<bullet>N)}"
   and   "pi2\<bullet>(M{c:=(x).N}) = (pi2\<bullet>M){(pi2\<bullet>c):=(pi2\<bullet>x).(pi2\<bullet>N)}"
-apply(nominal_induct M avoiding: c x N rule: trm.strong_induct)
-apply(auto simp: eq_bij fresh_bij eqvts)
-apply(perm_simp)+
-done
+by (nominal_induct M avoiding: c x N rule: trm.strong_induct)
+   (auto simp: eq_bij fresh_bij eqvts; perm_simp)+
 
 lemma nsubst_eqvt[eqvt]:
   fixes pi1::"name prm"
   and   pi2::"coname prm"
   shows "pi1\<bullet>(M{x:=<c>.N}) = (pi1\<bullet>M){(pi1\<bullet>x):=<(pi1\<bullet>c)>.(pi1\<bullet>N)}"
   and   "pi2\<bullet>(M{x:=<c>.N}) = (pi2\<bullet>M){(pi2\<bullet>x):=<(pi2\<bullet>c)>.(pi2\<bullet>N)}"
-apply(nominal_induct M avoiding: c x N rule: trm.strong_induct)
-apply(auto simp: eq_bij fresh_bij eqvts)
-apply(perm_simp)+
-done
+by (nominal_induct M avoiding: c x N rule: trm.strong_induct)
+   (auto simp: eq_bij fresh_bij eqvts; perm_simp)+
 
 lemma supp_subst1:
   shows "supp (M{y:=<c>.P}) \<subseteq> ((supp M) - {y}) \<union> (supp P)"
-apply(nominal_induct M avoiding: y P c rule: trm.strong_induct)
-apply(auto)
-apply(auto simp: fresh_def abs_supp trm.supp supp_atm fin_supp)
-apply(blast)+
-apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(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 "\<exists>x'::name. x'\<sharp>(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 "\<exists>x'::name. x'\<sharp>(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 "\<exists>x'::name. x'\<sharp>(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 "\<exists>x'::name. x'\<sharp>(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 "\<exists>x'::name. x'\<sharp>(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 "\<exists>x'::name. x'\<sharp>(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 "\<exists>x'::name. x'\<sharp>(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 "\<exists>x'::name. x'\<sharp>(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 "\<exists>x'::name. x'\<sharp>(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 "\<exists>x'::name. x'\<sharp>(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 "\<exists>x'::name. x'\<sharp>(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 "\<exists>x'::name. x'\<sharp>(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 "\<exists>x'::name. x'\<sharp>(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 "\<exists>x'::name. x'\<sharp>(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
-
+proof (nominal_induct M avoiding: y P c rule: trm.strong_induct)
+  case (NotL coname trm name)
+  obtain x'::name where "x'\<sharp>(trm{y:=<c>.P},P)"
+    by (meson exists_fresh(1) fs_name1)
+  with NotL
+   show ?case 
+     by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_NotL; blast)
+next
+  case (AndL1 name1 trm name2)
+  obtain x'::name where "x'\<sharp>(trm{y:=<c>.P},P,name1)"
+    by (meson exists_fresh(1) fs_name1)
+  with AndL1 show ?case
+    by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_AndL1 fresh_atm; blast)
+next
+  case (AndL2 name1 trm name2)
+  obtain x'::name where "x'\<sharp>(trm{y:=<c>.P},P,name1)"
+    by (meson exists_fresh(1) fs_name1)
+  with AndL2 show ?case
+    by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_AndL2 fresh_atm; blast)
+next
+  case (OrL name1 trm1 name2 trm2 name3)
+  obtain x'::name where "x'\<sharp>(trm1{y:=<c>.P},P,name1,trm2{y:=<c>.P},name2)"
+    by (meson exists_fresh(1) fs_name1)
+  with OrL show ?case 
+    by (auto simp: fs_name1 fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_OrL fresh_atm; blast)
+next
+  case (ImpL coname trm1 name1 trm2 name2)
+  obtain x'::name where "x'\<sharp>(trm1{name2:=<c>.P},P,name1,trm2{name2:=<c>.P})"
+    by (meson exists_fresh(1) fs_name1)
+  with ImpL show ?case 
+    by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_ImpL fresh_atm; blast)
+qed (simp add: abs_supp supp_atm trm.supp fs_name1; blast)+
+
+text \<open>Identical to the previous proof\<close>
 lemma supp_subst2:
   shows "supp (M{y:=<c>.P}) \<subseteq> supp (M) \<union> ((supp P) - {c})"
-apply(nominal_induct M avoiding: y P c rule: trm.strong_induct)
-apply(auto)
-apply(auto simp: fresh_def abs_supp trm.supp supp_atm fin_supp)
-apply(blast)+
-apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(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 "\<exists>x'::name. x'\<sharp>(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 "\<exists>x'::name. x'\<sharp>(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 "\<exists>x'::name. x'\<sharp>(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 "\<exists>x'::name. x'\<sharp>(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 "\<exists>x'::name. x'\<sharp>(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 "\<exists>x'::name. x'\<sharp>(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 "\<exists>x'::name. x'\<sharp>(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 "\<exists>x'::name. x'\<sharp>(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 "\<exists>x'::name. x'\<sharp>(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 "\<exists>x'::name. x'\<sharp>(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 "\<exists>x'::name. x'\<sharp>(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 "\<exists>x'::name. x'\<sharp>(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
+proof (nominal_induct M avoiding: y P c rule: trm.strong_induct)
+  case (NotL coname trm name)
+  obtain x'::name where "x'\<sharp>(trm{y:=<c>.P},P)"
+    by (meson exists_fresh(1) fs_name1)
+  with NotL
+   show ?case 
+     by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_NotL; blast)
+next
+  case (AndL1 name1 trm name2)
+  obtain x'::name where "x'\<sharp>(trm{y:=<c>.P},P,name1)"
+    by (meson exists_fresh(1) fs_name1)
+  with AndL1 show ?case
+    by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_AndL1 fresh_atm; blast)
+next
+  case (AndL2 name1 trm name2)
+  obtain x'::name where "x'\<sharp>(trm{y:=<c>.P},P,name1)"
+    by (meson exists_fresh(1) fs_name1)
+  with AndL2 show ?case
+    by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_AndL2 fresh_atm; blast)
+next
+  case (OrL name1 trm1 name2 trm2 name3)
+  obtain x'::name where "x'\<sharp>(trm1{y:=<c>.P},P,name1,trm2{y:=<c>.P},name2)"
+    by (meson exists_fresh(1) fs_name1)
+  with OrL show ?case 
+    by (auto simp: fs_name1 fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_OrL fresh_atm; blast)
+next
+  case (ImpL coname trm1 name1 trm2 name2)
+  obtain x'::name where "x'\<sharp>(trm1{name2:=<c>.P},P,name1,trm2{name2:=<c>.P})"
+    by (meson exists_fresh(1) fs_name1)
+  with ImpL show ?case 
+    by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_ImpL fresh_atm; blast)
+qed (simp add: abs_supp supp_atm trm.supp fs_name1; blast)+
 
 lemma supp_subst3:
   shows "supp (M{c:=(x).P}) \<subseteq> ((supp M) - {c}) \<union> (supp P)"
-apply(nominal_induct M avoiding: x P c rule: trm.strong_induct)
-apply(auto)
-apply(auto simp: fresh_def abs_supp trm.supp supp_atm fin_supp)
-apply(blast)+
-apply(subgoal_tac "\<exists>x'::coname. x'\<sharp>(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 "\<exists>x'::coname. x'\<sharp>(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 "\<exists>x'::coname. x'\<sharp>(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 "\<exists>x'::coname. x'\<sharp>(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 "\<exists>x'::coname. x'\<sharp>(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 "\<exists>x'::coname. x'\<sharp>(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 "\<exists>x'::coname. x'\<sharp>(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 "\<exists>x'::coname. x'\<sharp>(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 "\<exists>x'::coname. x'\<sharp>(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 "\<exists>x'::coname. x'\<sharp>(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 "\<exists>x'::coname. x'\<sharp>(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 "\<exists>x'::coname. x'\<sharp>(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 "\<exists>x'::coname. x'\<sharp>(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 "\<exists>x'::coname. x'\<sharp>(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 "\<exists>x'::coname. x'\<sharp>(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
+proof (nominal_induct M avoiding: x P c rule: trm.strong_induct)
+  case (NotR name trm coname)
+  obtain x'::coname where "x'\<sharp>(trm{coname:=(x).P},P)"
+    by (meson exists_fresh'(2) fs_coname1)
+  with NotR show ?case
+     by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_NotR; blast)
+next
+  case (AndR coname1 trm1 coname2 trm2 coname3)
+  obtain x'::coname where x': "x'\<sharp>(trm1{coname3:=(x).P},P,trm2{coname3:=(x).P},coname1,coname2)"
+    by (meson exists_fresh'(2) fs_coname1)
+  with AndR show ?case 
+    by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_AndR; blast)
+next
+  case (OrR1 coname1 trm coname2)
+  obtain x'::coname where x': "x'\<sharp>(trm{coname2:=(x).P},P,coname1)"
+    by (meson exists_fresh'(2) fs_coname1)
+  with OrR1 show ?case 
+    by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_OrR1; blast)
+next
+  case (OrR2 coname1 trm coname2)
+  obtain x'::coname where x': "x'\<sharp>(trm{coname2:=(x).P},P,coname1)"
+    by (meson exists_fresh'(2) fs_coname1)
+  with OrR2 show ?case 
+    by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_OrR2; blast)  
+next
+  case (ImpR name coname1 trm coname2)
+  obtain x'::coname where x': "x'\<sharp>(trm{coname2:=(x).P},P,coname1)"
+    by (meson exists_fresh'(2) fs_coname1)
+  with ImpR show ?case 
+    by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_ImpR; blast)
+qed (simp add: abs_supp supp_atm trm.supp fs_name1; blast)+
+
 
 lemma supp_subst4:
   shows "supp (M{c:=(x).P}) \<subseteq> (supp M) \<union> ((supp P) - {x})"
-apply(nominal_induct M avoiding: x P c rule: trm.strong_induct)
-apply(auto)
-apply(auto simp: fresh_def abs_supp trm.supp supp_atm fin_supp)
-apply(blast)+
-apply(subgoal_tac "\<exists>x'::coname. x'\<sharp>(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 "\<exists>x'::coname. x'\<sharp>(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 "\<exists>x'::coname. x'\<sharp>(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 "\<exists>x'::coname. x'\<sharp>(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 "\<exists>x'::coname. x'\<sharp>(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 "\<exists>x'::coname. x'\<sharp>(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 "\<exists>x'::coname. x'\<sharp>(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 "\<exists>x'::coname. x'\<sharp>(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 "\<exists>x'::coname. x'\<sharp>(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 "\<exists>x'::coname. x'\<sharp>(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 "\<exists>x'::coname. x'\<sharp>(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 "\<exists>x'::coname. x'\<sharp>(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
+proof (nominal_induct M avoiding: x P c rule: trm.strong_induct)
+  case (NotR name trm coname)
+  obtain x'::coname where "x'\<sharp>(trm{coname:=(x).P},P)"
+    by (meson exists_fresh'(2) fs_coname1)
+  with NotR show ?case
+     by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_NotR; blast)
+next
+  case (AndR coname1 trm1 coname2 trm2 coname3)
+  obtain x'::coname where x': "x'\<sharp>(trm1{coname3:=(x).P},P,trm2{coname3:=(x).P},coname1,coname2)"
+    by (meson exists_fresh'(2) fs_coname1)
+  with AndR show ?case 
+    by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_AndR; blast)
+next
+  case (OrR1 coname1 trm coname2)
+  obtain x'::coname where x': "x'\<sharp>(trm{coname2:=(x).P},P,coname1)"
+    by (meson exists_fresh'(2) fs_coname1)
+  with OrR1 show ?case 
+    by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_OrR1; blast)
+next
+  case (OrR2 coname1 trm coname2)
+  obtain x'::coname where x': "x'\<sharp>(trm{coname2:=(x).P},P,coname1)"
+    by (meson exists_fresh'(2) fs_coname1)
+  with OrR2 show ?case 
+    by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_OrR2; blast)  
+next
+  case (ImpR name coname1 trm coname2)
+  obtain x'::coname where x': "x'\<sharp>(trm{coname2:=(x).P},P,coname1)"
+    by (meson exists_fresh'(2) fs_coname1)
+  with ImpR show ?case 
+    by (auto simp: fresh_prod abs_supp supp_atm trm.supp fs_name1 fresh_fun_simp_ImpR; blast)
+qed (simp add: abs_supp supp_atm trm.supp fs_name1; blast)+
 
 lemma supp_subst5:
   shows "(supp M - {y}) \<subseteq> supp (M{y:=<c>.P})"
-apply(nominal_induct M avoiding: y P c rule: trm.strong_induct)
-apply(auto)
-apply(auto simp: fresh_def abs_supp trm.supp supp_atm fin_supp)
-apply(blast)+
-apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(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 "\<exists>x'::name. x'\<sharp>(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 "\<exists>x'::name. x'\<sharp>(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 "\<exists>x'::name. x'\<sharp>(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 "\<exists>x'::name. x'\<sharp>(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 "\<exists>x'::name. x'\<sharp>(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 "\<exists>x'::name. x'\<sharp>(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
+proof (nominal_induct M avoiding: y P c rule: trm.strong_induct)
+  case (NotL coname trm name)
+  obtain x'::name where "x'\<sharp>(trm{y:=<c>.P},P)"
+    by (meson exists_fresh(1) fs_name1)
+  with NotL
+  show ?case 
+    apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_NotL)
+     apply (auto simp: fresh_def)
+    done
+next
+  case (AndL1 name1 trm name2)
+  obtain x'::name where "x'\<sharp>(trm{y:=<c>.P},P,name1)"
+    by (meson exists_fresh(1) fs_name1)
+  with AndL1 show ?case
+    apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_AndL1)
+     apply (auto simp: fresh_def)
+    done
+next
+  case (AndL2 name1 trm name2)
+  obtain x'::name where "x'\<sharp>(trm{y:=<c>.P},P,name1)"
+    by (meson exists_fresh(1) fs_name1)
+  with AndL2 show ?case
+    apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_AndL2)
+     apply (auto simp: fresh_def)
+    done
+next
+  case (OrL name1 trm1 name2 trm2 name3)
+  obtain x'::name where "x'\<sharp>(trm1{y:=<c>.P},P,name1,trm2{y:=<c>.P},name2)"
+    by (meson exists_fresh(1) fs_name1)
+  with OrL show ?case 
+    apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_OrL)
+           apply (fastforce simp: fresh_def)+
+    done
+next
+  case (ImpL coname trm1 name1 trm2 name2)
+  obtain x'::name where "x'\<sharp>(trm1{name2:=<c>.P},P,name1,trm2{name2:=<c>.P})"
+    by (meson exists_fresh(1) fs_name1)
+  with ImpL show ?case 
+    apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_ImpL)
+           apply (fastforce simp: fresh_def)+
+    done
+qed (simp add: abs_supp supp_atm trm.supp fs_name1; blast)+
 
 lemma supp_subst6:
   shows "(supp M) \<subseteq> ((supp (M{y:=<c>.P}))::coname set)"
-apply(nominal_induct M avoiding: y P c rule: trm.strong_induct)
-apply(auto)
-apply(auto simp: fresh_def abs_supp trm.supp supp_atm fin_supp)
-apply(blast)+
-apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(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 "\<exists>x'::name. x'\<sharp>(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 "\<exists>x'::name. x'\<sharp>(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 "\<exists>x'::name. x'\<sharp>(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 "\<exists>x'::name. x'\<sharp>(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 "\<exists>x'::name. x'\<sharp>(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 "\<exists>x'::name. x'\<sharp>(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
+proof (nominal_induct M avoiding: y P c rule: trm.strong_induct)
+  case (NotL coname trm name)
+  obtain x'::name where "x'\<sharp>(trm{y:=<c>.P},P)"
+    by (meson exists_fresh(1) fs_name1)
+  with NotL
+  show ?case 
+    apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_NotL)
+     apply (auto simp: fresh_def)
+    done
+next
+  case (AndL1 name1 trm name2)
+  obtain x'::name where "x'\<sharp>(trm{y:=<c>.P},P,name1)"
+    by (meson exists_fresh(1) fs_name1)
+  with AndL1 show ?case
+    apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_AndL1)
+     apply (auto simp: fresh_def)
+    done
+next
+  case (AndL2 name1 trm name2)
+  obtain x'::name where "x'\<sharp>(trm{y:=<c>.P},P,name1)"
+    by (meson exists_fresh(1) fs_name1)
+  with AndL2 show ?case
+    apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_AndL2)
+     apply (auto simp: fresh_def)
+    done
+next
+  case (OrL name1 trm1 name2 trm2 name3)
+  obtain x'::name where "x'\<sharp>(trm1{y:=<c>.P},P,name1,trm2{y:=<c>.P},name2)"
+    by (meson exists_fresh(1) fs_name1)
+  with OrL show ?case 
+    apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_OrL)
+           apply (fastforce simp: fresh_def)+
+    done
+next
+  case (ImpL coname trm1 name1 trm2 name2)
+  obtain x'::name where "x'\<sharp>(trm1{name2:=<c>.P},P,name1,trm2{name2:=<c>.P})"
+    by (meson exists_fresh(1) fs_name1)
+  with ImpL show ?case 
+    apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_ImpL)
+           apply (fastforce simp: fresh_def)+
+    done
+qed (simp add: abs_supp supp_atm trm.supp fs_name1; blast)+
 
 lemma supp_subst7:
   shows "(supp M - {c}) \<subseteq>  supp (M{c:=(x).P})"
-apply(nominal_induct M avoiding: x P c rule: trm.strong_induct)
-apply(auto)
-apply(auto simp: fresh_def abs_supp trm.supp supp_atm fin_supp)
-apply(blast)+
-apply(subgoal_tac "\<exists>x'::coname. x'\<sharp>(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 "\<exists>x'::coname. x'\<sharp>(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 "\<exists>x'::coname. x'\<sharp>(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 "\<exists>x'::coname. x'\<sharp>(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 "\<exists>x'::coname. x'\<sharp>(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 "\<exists>x'::coname. x'\<sharp>(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
-
+proof (nominal_induct M avoiding: x P c rule: trm.strong_induct)
+  case (NotR name trm coname)
+  obtain x'::coname where "x'\<sharp>(trm{coname:=(x).P},P)"
+    by (meson exists_fresh'(2) fs_coname1)
+  with NotR show ?case
+    apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_NotR)
+     apply (auto simp: fresh_def)
+    done
+next
+  case (AndR coname1 trm1 coname2 trm2 coname3)
+  obtain x'::coname where "x'\<sharp>(trm1{coname3:=(x).P},P,trm2{coname3:=(x).P},coname1,coname2)"
+    by (meson exists_fresh'(2) fs_coname1)
+  with AndR show ?case
+    apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_AndR)
+     apply (fastforce simp: fresh_def)+
+    done
+next
+  case (OrR1 coname1 trm coname2)
+  obtain x'::coname where "x'\<sharp>(trm{coname2:=(x).P},P,coname1)"
+    by (meson exists_fresh'(2) fs_coname1)
+  with OrR1 show ?case
+    apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_OrR1)
+     apply (auto simp: fresh_def)
+    done
+next
+  case (OrR2 coname1 trm coname2)
+  obtain x'::coname where "x'\<sharp>(trm{coname2:=(x).P},P,coname1)"
+    by (meson exists_fresh'(2) fs_coname1)
+  with OrR2 show ?case
+    apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_OrR2)
+     apply (auto simp: fresh_def)
+    done
+next
+  case (ImpR name coname1 trm coname2)
+  obtain x'::coname where "x'\<sharp>(trm{coname2:=(x).P},P,coname1)"
+    by (meson exists_fresh'(2) fs_coname1)
+  with ImpR show ?case
+    apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_ImpR)
+     apply (auto simp: fresh_def)
+    done
+qed (simp add: abs_supp supp_atm trm.supp fs_name1; blast)+
+  
 lemma supp_subst8:
   shows "(supp M) \<subseteq> ((supp (M{c:=(x).P}))::name set)"
-apply(nominal_induct M avoiding: x P c rule: trm.strong_induct)
-apply(auto)
-apply(auto simp: fresh_def abs_supp trm.supp supp_atm fin_supp)
-apply(blast)+
-apply(subgoal_tac "\<exists>x'::coname. x'\<sharp>(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 "\<exists>x'::coname. x'\<sharp>(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 "\<exists>x'::coname. x'\<sharp>(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 "\<exists>x'::coname. x'\<sharp>(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 "\<exists>x'::coname. x'\<sharp>(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 "\<exists>x'::coname. x'\<sharp>(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
-
+proof (nominal_induct M avoiding: x P c rule: trm.strong_induct)
+  case (NotR name trm coname)
+  obtain x'::coname where "x'\<sharp>(trm{coname:=(x).P},P)"
+    by (meson exists_fresh'(2) fs_coname1)
+  with NotR show ?case
+    apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_NotR)
+     apply (auto simp: fresh_def)
+    done
+next
+  case (AndR coname1 trm1 coname2 trm2 coname3)
+  obtain x'::coname where "x'\<sharp>(trm1{coname3:=(x).P},P,trm2{coname3:=(x).P},coname1,coname2)"
+    by (meson exists_fresh'(2) fs_coname1)
+  with AndR show ?case
+    apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_AndR)
+     apply (fastforce simp: fresh_def)+
+    done
+next
+  case (OrR1 coname1 trm coname2)
+  obtain x'::coname where "x'\<sharp>(trm{coname2:=(x).P},P,coname1)"
+    by (meson exists_fresh'(2) fs_coname1)
+  with OrR1 show ?case
+    apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_OrR1)
+     apply (auto simp: fresh_def)
+    done
+next
+  case (OrR2 coname1 trm coname2)
+  obtain x'::coname where "x'\<sharp>(trm{coname2:=(x).P},P,coname1)"
+    by (meson exists_fresh'(2) fs_coname1)
+  with OrR2 show ?case
+    apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_OrR2)
+     apply (auto simp: fresh_def)
+    done
+next
+  case (ImpR name coname1 trm coname2)
+  obtain x'::coname where "x'\<sharp>(trm{coname2:=(x).P},P,coname1)"
+    by (meson exists_fresh'(2) fs_coname1)
+  with ImpR show ?case
+    by (force simp: fresh_prod abs_supp fs_name1 supp_atm trm.supp fresh_fun_simp_ImpR)
+qed (simp add: abs_supp supp_atm trm.supp fs_name1; blast)+
+  
 lemmas subst_supp = supp_subst1 supp_subst2 supp_subst3 supp_subst4
                     supp_subst5 supp_subst6 supp_subst7 supp_subst8
 lemma subst_fresh:
@@ -1499,11 +1084,8 @@
   and   "b\<sharp>(M,P) \<Longrightarrow> b\<sharp>M{c:=(y).P}"
   and   "b\<sharp>M \<Longrightarrow> b\<sharp>M{y:=<b>.P}"
   and   "b\<sharp>(M,P) \<Longrightarrow> b\<sharp>M{y:=<c>.P}"
-apply -
-apply(insert subst_supp)
-apply(simp_all add: fresh_def supp_prod)
-apply(blast)+ 
-done
+  using subst_supp
+  by(fastforce simp add: fresh_def supp_prod)+
 
 lemma forget:
   shows "x\<sharp>M \<Longrightarrow> M{x:=<c>.P} = M"
@@ -1517,198 +1099,81 @@
   shows "M{a:=(x).N} = ([(c,a)]\<bullet>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: fresh_prod fresh_atm calc_atm trm.inject alpha)
-next
-  case NotL
-  then show ?case by (auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
-next
-  case (NotR y M d)
-  then show ?case 
-    by(auto simp: 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: fresh_prod calc_atm fresh_atm abs_fresh fresh_left)
-    apply (metis (erased, opaque_lifting))
-    by metis
-next
-  case AndL1
-  then show ?case by (auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
-next
-  case AndL2
-  then show ?case by (auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
-next
-  case (OrR1 d M e)
-  then show ?case 
-    by(auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
-next
-  case (OrR2 d M e)
-  then show ?case 
-    by(auto simp: 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: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
+     apply (metis (no_types, lifting))+
+    done
 next 
   case ImpL
   then show ?case
-    by (auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
+    by (auto simp: calc_atm alpha fresh_atm abs_fresh fresh_prod fresh_left)
        metis
 next
-  case (ImpR y d M e)
-  then show ?case
-    by(auto simp: 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
+qed (auto simp: calc_atm alpha fresh_atm abs_fresh fresh_prod fresh_left trm.inject)
 
 lemma substc_rename2:
   assumes a: "y\<sharp>(N,x)"
   shows "M{a:=(x).N} = M{a:=(y).([(y,x)]\<bullet>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: fresh_prod fresh_atm calc_atm trm.inject alpha perm_swap fresh_left)
-next
-  case NotL
-  then show ?case 
-    by (auto simp: 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: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
-    apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(N,M{d:=(y).([(y,x)]\<bullet>N)},[(y,x)]\<bullet>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
+  obtain a::coname where "a\<sharp>(N,M{d:=(y).([(y,x)]\<bullet>N)},[(y,x)]\<bullet>N)"
+    by (meson exists_fresh(2) fs_coname1)
+  with NotR show ?case
+    apply(auto simp: calc_atm alpha fresh_atm fresh_prod fresh_left)
+    by (metis (no_types, opaque_lifting) alpha(1) trm.inject(2))
 next
   case (AndR c1 M c2 M' c3)
-  then show ?case
-    apply(auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
-    apply(subgoal_tac 
-       "\<exists>a'::coname. a'\<sharp>(N,M{c3:=(y).([(y,x)]\<bullet>N)},M'{c3:=(y).([(y,x)]\<bullet>N)},[(y,x)]\<bullet>N,c1,c2,c3)")
-    apply(erule exE, simp add: fresh_prod)
-    apply(erule conjE)+
-    apply(simp add: fresh_fun_simp_AndR)
-    apply (auto simp: 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: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
-next
-  case AndL2
-  then show ?case by (auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
+  obtain a'::coname where "a'\<sharp>(N,M{c3:=(y).([(y,x)]\<bullet>N)},M'{c3:=(y).([(y,x)]\<bullet>N)},[(y,x)]\<bullet>N,c1,c2,c3)"
+    by (meson exists_fresh(2) fs_coname1)
+  with AndR show ?case
+    apply(auto simp: calc_atm alpha fresh_atm fresh_prod fresh_left)
+    by (metis (no_types, opaque_lifting) alpha(1) trm.inject(2))
 next
   case (OrR1 d M e)
-  then show ?case 
-    apply(auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
-    apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(N,M{e:=(y).([(y,x)]\<bullet>N)},[(y,x)]\<bullet>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
+  obtain a'::coname where "a'\<sharp>(N,M{e:=(y).([(y,x)]\<bullet>N)},[(y,x)]\<bullet>N,d,e)"
+    by (meson exists_fresh(2) fs_coname1)
+  with OrR1 show ?case 
+    by (auto simp: perm_swap calc_atm trm.inject alpha fresh_atm fresh_prod fresh_left fresh_fun_simp_OrR1)
 next
   case (OrR2 d M e)
-  then show ?case
-    apply(auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
-    apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(N,M{e:=(y).([(y,x)]\<bullet>N)},[(y,x)]\<bullet>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: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
-next 
-  case ImpL
-  then show ?case
-    by (auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
+  obtain a'::coname where "a'\<sharp>(N,M{e:=(y).([(y,x)]\<bullet>N)},[(y,x)]\<bullet>N,d,e)"
+    by (meson exists_fresh(2) fs_coname1)
+  with OrR2 show ?case 
+    by (auto simp: perm_swap calc_atm trm.inject alpha fresh_atm fresh_prod fresh_left fresh_fun_simp_OrR2)
 next
   case (ImpR y d M e)
-  then show ?case
-    apply(auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
-    apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(N,M{e:=(y).([(y,x)]\<bullet>N)},[(y,x)]\<bullet>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: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left perm_swap)
-qed
+  obtain a'::coname where "a'\<sharp>(N,M{e:=(y).([(y,x)]\<bullet>N)},[(y,x)]\<bullet>N,d,e)"
+    by (meson exists_fresh(2) fs_coname1)
+  with ImpR show ?case 
+    by (auto simp: perm_swap calc_atm trm.inject alpha fresh_atm fresh_prod fresh_left fresh_fun_simp_ImpR) 
+qed (auto simp: calc_atm trm.inject alpha fresh_atm fresh_prod fresh_left perm_swap)
 
 lemma substn_rename3:
   assumes a: "y\<sharp>(M,x)"
   shows "M{x:=<a>.N} = ([(y,x)]\<bullet>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: fresh_prod fresh_atm calc_atm trm.inject alpha)
-next
-  case NotR
-  then show ?case by (auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
-next
-  case (NotL d M z)
-  then show ?case 
-    by(auto simp: 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: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
-next
-  case OrR1
-  then show ?case by (auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
-next
-  case OrR2
-  then show ?case by (auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
-next
-  case (AndL1 u M v)
-  then show ?case 
-    by(auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
-next
-  case (AndL2 u M v)
-  then show ?case 
-    by(auto simp: 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: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_left abs_supp fin_supp fresh_prod)
+    apply(auto simp add: calc_atm fresh_atm abs_fresh fresh_prod fresh_left)
+    by (metis (mono_tags))+
 next
   case (ImpL d M v M' u)
   then show ?case
-    by(simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
-       (metis (poly_guards_query))
+    apply(auto simp add: calc_atm fresh_atm abs_fresh fresh_prod fresh_left)
+    by (metis (mono_tags))+
 next
   case (Cut d M y M')
   then show ?case
     apply(auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
-    apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst])
-    apply(simp add: calc_atm)
-    apply metis
-    done
-qed
+    by (metis nrename.simps(1) nrename_id nrename_rename)+
+qed (auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_left abs_supp fin_supp fresh_prod)
 
 lemma substn_rename4:
   assumes a: "c\<sharp>(N,a)"