# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1721424556 -3600
# Node ID f2eb4fa955250aaadb209a032acdca56b68a279a
# Parent  673add17a05e6737173cd22d745ff66a80d99d63
more proof tidying

diff -r 673add17a05e -r f2eb4fa95525 src/HOL/Nominal/Examples/Class1.thy
--- a/src/HOL/Nominal/Examples/Class1.thy	Wed Jul 17 21:25:37 2024 +0100
+++ b/src/HOL/Nominal/Examples/Class1.thy	Fri Jul 19 22:29:16 2024 +0100
@@ -14,7 +14,7 @@
     PR "string"
   | NOT  "ty"
   | AND  "ty" "ty"   ("_ AND _" [100,100] 100)
-  | OR   "ty" "ty"   ("_ OR _" [100,100] 100)
+  | OR   "ty" "ty"   ("_ OR _"  [100,100] 100)
   | IMP  "ty" "ty"   ("_ IMP _" [100,100] 100)
 
 instantiation ty :: size
@@ -529,21 +529,24 @@
 lemma fresh_fun_OrR1[eqvt_force]:
   fixes pi1::"name prm"
   and   pi2::"coname prm"
-  shows "pi1\<bullet>fresh_fun (\<lambda>a'. Cut <a'>.(OrR1 <b>.M a') (x).P)=
-             fresh_fun (pi1\<bullet>(\<lambda>a'. Cut <a'>.(OrR1 <b>.M  a') (x).P))"
-  and   "pi2\<bullet>fresh_fun (\<lambda>a'. Cut <a'>.(OrR1 <b>.M a') (x).P)=
-             fresh_fun (pi2\<bullet>(\<lambda>a'. Cut <a'>.(OrR1 <b>.M a') (x).P))"
-   apply(perm_simp)
-   apply(subgoal_tac "\<exists>n::coname. n\<sharp>(P,M,b,pi1\<bullet>P,pi1\<bullet>M,pi1\<bullet>b,pi1)")
-    apply(force simp add: fresh_prod fresh_fun_simp_OrR1 calc_atm)
-   apply (meson exists_fresh(2) fs_coname1)
-  apply(perm_simp)
-  apply(subgoal_tac "\<exists>n::coname. n\<sharp>(P,M,b,pi2\<bullet>P,pi2\<bullet>M,pi2\<bullet>b,pi2)")
-   apply(force simp add: fresh_prod fresh_fun_simp_OrR1 at_prm_fresh[OF at_coname_inst] swap_simps)
-  by (meson exists_fresh(2) fs_coname1)
+  shows "pi1\<bullet>fresh_fun (\<lambda>a'. Cut <a'>.(OrR1 <b>.M a') (x).P) =
+             fresh_fun (pi1\<bullet>(\<lambda>a'. Cut <a'>.(OrR1 <b>.M  a') (x).P))" (is "?t1")
+  and   "pi2\<bullet>fresh_fun (\<lambda>a'. Cut <a'>.(OrR1 <b>.M a') (x).P) =
+             fresh_fun (pi2\<bullet>(\<lambda>a'. Cut <a'>.(OrR1 <b>.M a') (x).P))"  (is "?t2")
+proof -
+  obtain n::coname where "n\<sharp>(P,M,b,pi1\<bullet>P,pi1\<bullet>M,pi1\<bullet>b,pi1)"
+    by (meson exists_fresh(2) fs_coname1)
+  then show ?t1
+    by perm_simp (force simp add: fresh_prod fresh_fun_simp_OrR1 calc_atm)
+  obtain n::coname where "n\<sharp>(P,M,b,pi2\<bullet>P,pi2\<bullet>M,pi2\<bullet>b,pi2)"
+    by (meson exists_fresh(2) fs_coname1)
+  then show ?t2
+    by perm_simp
+      (force simp add: fresh_prod fresh_fun_simp_OrR1 at_prm_fresh[OF at_coname_inst] swap_simps)
+qed
 
 lemma fresh_fun_simp_OrR2:
-  assumes a: "a'\<sharp>P" "a'\<sharp>M" "a'\<sharp>b" 
+  assumes "a'\<sharp>P" "a'\<sharp>M" "a'\<sharp>b" 
   shows "fresh_fun (\<lambda>a'. Cut <a'>.(OrR2 <b>.M a') (x).P) = Cut <a'>.(OrR2 <b>.M a') (x).P"
 proof (rule fresh_fun_app [OF pt_coname_inst at_coname_inst])
   obtain n::coname where "n\<sharp>(x,P,b,M)"
@@ -553,23 +556,26 @@
     apply(simp add: fresh_prod abs_fresh)
     apply(fresh_guess)
     done
-qed (use a in \<open>fresh_guess|finite_guess\<close>)+
+qed (use assms in \<open>fresh_guess|finite_guess\<close>)+
 
 lemma fresh_fun_OrR2[eqvt_force]:
   fixes pi1::"name prm"
   and   pi2::"coname prm"
-  shows "pi1\<bullet>fresh_fun (\<lambda>a'. Cut <a'>.(OrR2 <b>.M a') (x).P)=
-             fresh_fun (pi1\<bullet>(\<lambda>a'. Cut <a'>.(OrR2 <b>.M  a') (x).P))"
-  and   "pi2\<bullet>fresh_fun (\<lambda>a'. Cut <a'>.(OrR2 <b>.M a') (x).P)=
-             fresh_fun (pi2\<bullet>(\<lambda>a'. Cut <a'>.(OrR2 <b>.M a') (x).P))"
-   apply(perm_simp)
-   apply(subgoal_tac "\<exists>n::coname. n\<sharp>(P,M,b,pi1\<bullet>P,pi1\<bullet>M,pi1\<bullet>b,pi1)")
-    apply(force simp add: fresh_prod fresh_fun_simp_OrR2 calc_atm)
-   apply (meson exists_fresh(2) fs_coname1)
-  apply(perm_simp)
-  apply(subgoal_tac "\<exists>n::coname. n\<sharp>(P,M,b,pi2\<bullet>P,pi2\<bullet>M,pi2\<bullet>b,pi2)")
-   apply(force simp add: fresh_prod fresh_fun_simp_OrR2 at_prm_fresh[OF at_coname_inst] swap_simps)
-  by (meson exists_fresh(2) fs_coname1)
+  shows "pi1\<bullet>fresh_fun (\<lambda>a'. Cut <a'>.(OrR2 <b>.M a') (x).P) =
+             fresh_fun (pi1\<bullet>(\<lambda>a'. Cut <a'>.(OrR2 <b>.M  a') (x).P))" (is "?t1")
+  and   "pi2\<bullet>fresh_fun (\<lambda>a'. Cut <a'>.(OrR2 <b>.M a') (x).P) =
+             fresh_fun (pi2\<bullet>(\<lambda>a'. Cut <a'>.(OrR2 <b>.M a') (x).P))"  (is "?t2")
+proof -
+  obtain n::coname where "n\<sharp>(P,M,b,pi1\<bullet>P,pi1\<bullet>M,pi1\<bullet>b,pi1)"
+    by (meson exists_fresh(2) fs_coname1)
+  then show ?t1
+    by perm_simp (force simp add: fresh_prod fresh_fun_simp_OrR2 calc_atm)
+  obtain n::coname where "n\<sharp>(P,M,b,pi2\<bullet>P,pi2\<bullet>M,pi2\<bullet>b,pi2)"
+    by (meson exists_fresh(2) fs_coname1)
+  then show ?t2
+    by perm_simp
+      (force simp add: fresh_prod fresh_fun_simp_OrR2 at_prm_fresh[OF at_coname_inst] swap_simps)
+qed
 
 lemma fresh_fun_simp_ImpR:
   assumes a: "a'\<sharp>P" "a'\<sharp>M" "a'\<sharp>b" 
@@ -587,18 +593,21 @@
 lemma fresh_fun_ImpR[eqvt_force]:
   fixes pi1::"name prm"
   and   pi2::"coname prm"
-  shows "pi1\<bullet>fresh_fun (\<lambda>a'. Cut <a'>.(ImpR (y).<b>.M a') (x).P)=
-             fresh_fun (pi1\<bullet>(\<lambda>a'. Cut <a'>.(ImpR (y).<b>.M  a') (x).P))"
+  shows "pi1\<bullet>fresh_fun (\<lambda>a'. Cut <a'>.(ImpR (y).<b>.M a') (x).P) =
+             fresh_fun (pi1\<bullet>(\<lambda>a'. Cut <a'>.(ImpR (y).<b>.M  a') (x).P))" (is "?t1")
   and   "pi2\<bullet>fresh_fun (\<lambda>a'. Cut <a'>.(ImpR (y).<b>.M a') (x).P)=
-             fresh_fun (pi2\<bullet>(\<lambda>a'. Cut <a'>.(ImpR (y).<b>.M a') (x).P))"
-   apply(perm_simp)
-   apply(subgoal_tac "\<exists>n::coname. n\<sharp>(P,M,b,pi1\<bullet>P,pi1\<bullet>M,pi1\<bullet>b,pi1)")
-    apply(force simp add: fresh_prod fresh_fun_simp_ImpR calc_atm)
-   apply (meson exists_fresh(2) fs_coname1)
-  apply(perm_simp)
-  apply(subgoal_tac "\<exists>n::coname. n\<sharp>(P,M,b,pi2\<bullet>P,pi2\<bullet>M,pi2\<bullet>b,pi2)")
-   apply(force simp add: fresh_prod fresh_fun_simp_ImpR at_prm_fresh[OF at_coname_inst] swap_simps)
-  by (meson exists_fresh(2) fs_coname1)
+             fresh_fun (pi2\<bullet>(\<lambda>a'. Cut <a'>.(ImpR (y).<b>.M a') (x).P))"  (is "?t2")
+proof -
+  obtain n::coname where "n\<sharp>(P,M,b,pi1\<bullet>P,pi1\<bullet>M,pi1\<bullet>b,pi1)"
+    by (meson exists_fresh(2) fs_coname1)
+  then show ?t1
+    by perm_simp (force simp add: fresh_prod fresh_fun_simp_ImpR calc_atm)
+  obtain n::coname where "n\<sharp>(P,M,b,pi2\<bullet>P,pi2\<bullet>M,pi2\<bullet>b,pi2)"
+    by (meson exists_fresh(2) fs_coname1)
+  then show ?t2
+    by perm_simp
+      (force simp add: fresh_prod fresh_fun_simp_ImpR at_prm_fresh[OF at_coname_inst] swap_simps)
+qed
 
 nominal_primrec (freshness_context: "(y::name,c::coname,P::trm)")
   substn :: "trm \<Rightarrow> name   \<Rightarrow> coname \<Rightarrow> trm \<Rightarrow> trm" ("_{_:=<_>._}" [100,100,100,100] 100) 
@@ -1257,6 +1266,7 @@
     unfolding eq2[symmetric]
     apply(auto simp: trm.inject)
     apply(simp_all add: alpha fresh_atm fresh_prod subst_fresh eqvts perm_fresh_fresh calc_atm)
+    apply (simp add: fresh_atm(2) substn_rename4)
     by (metis abs_fresh(2) fresh_atm(2) fresh_prod perm_fresh_fresh(2) substn_rename4)
   finally show ?thesis by simp
 qed
@@ -1894,240 +1904,220 @@
    (auto simp: calc_atm simp add: fresh_left abs_fresh)
 
 lemma not_fin_subst1:
-  assumes a: "\<not>(fin M x)" 
+  assumes "\<not>(fin M x)" 
   shows "\<not>(fin (M{c:=(y).P}) x)"
-using a [[simproc del: defined_all]]
-apply(nominal_induct M avoiding: x c y P rule: trm.strong_induct)
-apply(auto)
-apply(drule fin_elims, simp)
-apply(drule fin_elims, simp)
-apply(drule fin_elims, simp)
-apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(trm{coname:=(y).P},P,x)")
-apply(erule exE)
-apply(simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_NotR)
-apply(erule fin.cases, simp_all add: trm.inject)
-apply(rule exists_fresh'(2)[OF fs_coname1])
-apply(drule fin_elims, simp)
-apply(drule fin_elims)
-apply(auto)[1]
-apply(drule freshn_after_substc)
-apply(simp add: fin.intros)
-apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(trm1{coname3:=(y).P},trm2{coname3:=(y).P},P,coname1,coname2,coname3,x)")
-apply(erule exE)
-apply(simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_AndR)
-apply(erule fin.cases, simp_all add: trm.inject)
-apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(trm1{coname3:=(y).P},trm2{coname3:=(y).P},P,coname1,coname2,coname3,x)")
-apply(erule exE)
-apply(simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_AndR)
-apply(erule fin.cases, simp_all add: trm.inject)
-apply(rule exists_fresh'(2)[OF fs_coname1])
-apply(erule fin.cases, simp_all add: trm.inject)
-apply(drule fin_AndL1_elim)
-apply(auto simp: abs_fresh)[1]
-apply(drule freshn_after_substc)
-apply(subgoal_tac "name2\<sharp>[name1]. trm")
-apply(simp add: fin.intros)
-apply(simp add: abs_fresh)
-apply(drule fin_AndL2_elim)
-apply(auto simp: abs_fresh)[1]
-apply(drule freshn_after_substc)
-apply(subgoal_tac "name2\<sharp>[name1].trm")
-apply(simp add: fin.intros)
-apply(simp add: abs_fresh)
-apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(trm{coname2:=(y).P},coname1,P,x)")
-apply(erule exE)
-apply(simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_OrR1)
-apply(erule fin.cases, simp_all add: trm.inject)
-apply(rule exists_fresh'(2)[OF fs_coname1])
-apply(erule fin.cases, simp_all add: trm.inject)
-apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(trm{coname2:=(y).P},coname1,P,x)")
-apply(erule exE)
-apply(simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_OrR2)
-apply(erule fin.cases, simp_all add: trm.inject)
-apply(rule exists_fresh'(2)[OF fs_coname1])
-apply(erule fin.cases, simp_all add: trm.inject)
-apply(drule fin_OrL_elim)
-apply(auto simp: abs_fresh)[1]
-apply(drule freshn_after_substc)+
-apply(subgoal_tac "name3\<sharp>[name1].trm1 \<and> name3\<sharp>[name2].trm2")
-apply(simp add: fin.intros)
-apply(simp add: abs_fresh)
-apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(trm{coname2:=(y).P},coname1,P,x)")
-apply(erule exE)
-apply(simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_ImpR)
-apply(erule fin.cases, simp_all add: trm.inject)
-apply(rule exists_fresh'(2)[OF fs_coname1])
-apply(erule fin.cases, simp_all add: trm.inject)
-apply(drule fin_ImpL_elim)
-apply(auto simp: abs_fresh)[1]
-apply(drule freshn_after_substc)+
-apply(subgoal_tac "x\<sharp>[name1].trm2")
-apply(simp add: fin.intros)
-apply(simp add: abs_fresh)
-done
+using assms 
+proof (nominal_induct M avoiding: x c y P rule: trm.strong_induct)
+  case (Ax name coname)
+  then show ?case 
+    using fin_rest_elims(1) substc.simps(1) by presburger
+next
+  case (Cut coname trm1 name trm2)
+  then show ?case
+    using fin_rest_elims(1) substc.simps(1) by simp presburger
+next
+  case (NotR name trm coname)
+  obtain a'::coname where "a'\<sharp>(trm{coname:=(y).P},P,x)"
+    by (meson exists_fresh(2) fs_coname1)
+  with NotR show ?case
+    apply (simp add: fresh_prod trm.inject)
+    using fresh_fun_simp_NotR fin_rest_elims by fastforce
+next
+  case (NotL coname trm name)
+  then show ?case 
+    using fin_NotL_elim freshn_after_substc by simp blast
+next
+  case (AndR coname1 trm1 coname2 trm2 coname3)
+  obtain a'::coname where "a'\<sharp>(trm1{coname3:=(y).P},trm2{coname3:=(y).P},P,coname1,coname2,coname3,x)"
+    by (meson exists_fresh(2) fs_coname1)
+  with AndR show ?case
+    apply (simp add: fresh_prod trm.inject)
+    using fresh_fun_simp_AndR fin_rest_elims by fastforce
+next
+  case (AndL1 name1 trm name2)
+  then show ?case 
+    using fin_AndL1_elim freshn_after_substc
+    by simp (metis abs_fresh(1) fin.intros(3))
+next
+  case (AndL2 name1 trm name2)
+  then show ?case 
+    using fin_AndL2_elim freshn_after_substc
+    by simp (metis abs_fresh(1) fin.intros(4))
+next
+  case (OrR1 coname1 trm coname2)
+  obtain a'::coname where "a'\<sharp>(trm{coname2:=(y).P},coname1,P,x)"
+    by (meson exists_fresh(2) fs_coname1)
+  with OrR1 show ?case
+    apply (simp add: fresh_prod trm.inject)
+    using fresh_fun_simp_OrR1 fin_rest_elims by fastforce
+next
+  case (OrR2 coname1 trm coname2)
+  obtain a'::coname where "a'\<sharp>(trm{coname2:=(y).P},coname1,P,x)"
+    by (meson exists_fresh(2) fs_coname1)
+  with OrR2 show ?case
+    apply (simp add: fresh_prod trm.inject)
+    using fresh_fun_simp_OrR2 fin_rest_elims by fastforce
+next
+  case (OrL name1 trm1 name2 trm2 name3)
+  then show ?case
+    by simp (metis abs_fresh(1) fin.intros(5) fin_OrL_elim freshn_after_substc)
+next
+  case (ImpR name coname1 trm coname2)
+  obtain a'::coname where "a'\<sharp>(trm{coname2:=(y).P},coname1,P,x)"
+    by (meson exists_fresh(2) fs_coname1)
+  with ImpR show ?case
+    apply (simp add: fresh_prod trm.inject)
+    using fresh_fun_simp_ImpR fin_rest_elims by fastforce
+next
+  case (ImpL coname trm1 name1 trm2 name2)
+  then show ?case
+    by simp (metis abs_fresh(1) fin.intros(6) fin_ImpL_elim freshn_after_substc)
+qed
+
+
 
 lemma not_fin_subst2:
-  assumes a: "\<not>(fin M x)" 
+  assumes "\<not>(fin M x)" 
   shows "\<not>(fin (M{y:=<c>.P}) x)"
-using a [[simproc del: defined_all]]
-apply(nominal_induct M avoiding: x c y P rule: trm.strong_induct)
-apply(auto)
-apply(erule fin.cases, simp_all add: trm.inject)
-apply(erule fin.cases, simp_all add: trm.inject)
-apply(erule fin.cases, simp_all add: trm.inject)
-apply(erule fin.cases, simp_all add: trm.inject)
-apply(subgoal_tac "\<exists>a'::name. a'\<sharp>(trm{y:=<c>.P},P,x)")
-apply(erule exE)
-apply(simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_NotL)
-apply(erule fin.cases, simp_all add: trm.inject)
-apply(rule exists_fresh'(1)[OF fs_name1])
-apply(drule fin_NotL_elim)
-apply(auto)[1]
-apply(drule freshn_after_substn)
-apply(simp)
-apply(simp add: fin.intros)
-apply(erule fin.cases, simp_all add: trm.inject)
-apply(subgoal_tac "\<exists>a'::name. a'\<sharp>(trm{y:=<c>.P},P,name1,x)")
-apply(erule exE)
-apply(simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_AndL1)
-apply(erule fin.cases, simp_all add: trm.inject)
-apply(rule exists_fresh'(1)[OF fs_name1])
-apply(drule fin_AndL1_elim)
-apply(auto simp: abs_fresh)[1]
-apply(drule freshn_after_substn)
-apply(simp)
-apply(subgoal_tac "name2\<sharp>[name1]. trm")
-apply(simp add: fin.intros)
-apply(simp add: abs_fresh)
-apply(subgoal_tac "\<exists>a'::name. a'\<sharp>(trm{y:=<c>.P},P,name1,x)")
-apply(erule exE)
-apply(simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_AndL2)
-apply(erule fin.cases, simp_all add: trm.inject)
-apply(rule exists_fresh'(1)[OF fs_name1])
-apply(drule fin_AndL2_elim)
-apply(auto simp: abs_fresh)[1]
-apply(drule freshn_after_substn)
-apply(simp)
-apply(subgoal_tac "name2\<sharp>[name1].trm")
-apply(simp add: fin.intros)
-apply(simp add: abs_fresh)
-apply(erule fin.cases, simp_all add: trm.inject)
-apply(erule fin.cases, simp_all add: trm.inject)
-apply(subgoal_tac "\<exists>a'::name. a'\<sharp>(trm1{y:=<c>.P},trm2{y:=<c>.P},name1,name2,P,x)")
-apply(erule exE)
-apply(simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_OrL)
-apply(erule fin.cases, simp_all add: trm.inject)
-apply(rule exists_fresh'(1)[OF fs_name1])
-apply(drule fin_OrL_elim)
-apply(auto simp: abs_fresh)[1]
-apply(drule freshn_after_substn)
-apply(simp)
-apply(drule freshn_after_substn)
-apply(simp)
-apply(subgoal_tac "name3\<sharp>[name1].trm1 \<and> name3\<sharp>[name2].trm2")
-apply(simp add: fin.intros)
-apply(simp add: abs_fresh)
-apply(erule fin.cases, simp_all add: trm.inject)
-apply(subgoal_tac "\<exists>a'::name. a'\<sharp>(trm1{name2:=<c>.P},trm2{name2:=<c>.P},name1,P,x)")
-apply(erule exE)
-apply(simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_ImpL)
-apply(erule fin.cases, simp_all add: trm.inject)
-apply(rule exists_fresh'(1)[OF fs_name1])
-apply(drule fin_ImpL_elim)
-apply(auto simp: abs_fresh)[1]
-apply(drule freshn_after_substn)
-apply(simp)
-apply(drule freshn_after_substn)
-apply(simp)
-apply(subgoal_tac "x\<sharp>[name1].trm2")
-apply(simp add: fin.intros)
-apply(simp add: abs_fresh)
-done
+using assms 
+proof (nominal_induct M avoiding: x c y P rule: trm.strong_induct)
+  case (Ax name coname)
+  then show ?case
+    using fin_rest_elims(1) substn.simps(1) by presburger
+next
+  case (Cut coname trm1 name trm2)
+  then show ?case
+    using fin_rest_elims(1) substc.simps(1) by simp presburger
+next
+  case (NotR name trm coname)
+  with fin_rest_elims show ?case
+    by (fastforce simp add: fresh_prod trm.inject)
+next
+  case (NotL coname trm name)
+  obtain a'::name where "a'\<sharp>(trm{y:=<c>.P},P,x)"
+    by (meson exists_fresh(1) fs_name1)
+  with NotL show ?case 
+    apply (clarsimp simp: fresh_prod fresh_fun_simp_NotL trm.inject)
+    by (metis fin.intros(2) fin_NotL_elim fin_rest_elims(1) freshn_after_substn)
+next
+  case (AndR coname1 trm1 coname2 trm2 coname3)
+  obtain a'::name where "a'\<sharp>(trm1{coname3:=(y).P},trm2{coname3:=(y).P},P,coname1,coname2,coname3,x)"
+    by (meson exists_fresh(1) fs_name1)
+  with AndR fin_rest_elims show ?case
+    by (fastforce simp add: fresh_prod trm.inject)
+next
+  case (AndL1 name1 trm name2)
+  obtain a'::name where "a'\<sharp>(trm{y:=<c>.P},P,name1,x)"
+    by (meson exists_fresh(1) fs_name1)
+  with AndL1 show ?case 
+    apply (clarsimp simp: fresh_prod fresh_fun_simp_AndL1 trm.inject)
+    by (metis abs_fresh(1) fin.intros(3) fin_AndL1_elim fin_rest_elims(1) freshn_after_substn)
+next
+  case (AndL2 name1 trm name2)
+  obtain a'::name where "a'\<sharp>(trm{y:=<c>.P},P,name1,x)"
+    by (meson exists_fresh(1) fs_name1)
+  with AndL2 show ?case 
+    apply (clarsimp simp: fresh_prod fresh_fun_simp_AndL2 trm.inject)
+    by (metis abs_fresh(1) fin.intros(4) fin_AndL2_elim fin_rest_elims(1) freshn_after_substn)
+next
+  case (OrR1 coname1 trm coname2)
+  then show ?case
+    using fin_rest_elims by (fastforce simp: fresh_prod trm.inject)
+next
+  case (OrR2 coname1 trm coname2)
+  then show ?case
+    using fin_rest_elims by (fastforce simp: fresh_prod trm.inject)
+next
+  case (OrL name1 trm1 name2 trm2 name3)
+  obtain a'::name where "a'\<sharp>(trm1{y:=<c>.P},trm2{y:=<c>.P},name1,name2,P,x)"
+    by (meson exists_fresh(1) fs_name1)
+  with OrL show ?case  
+    apply (simp add: fresh_prod trm.inject)
+    by (metis (full_types) abs_fresh(1) fin.intros(5) fin_OrL_elim fin_rest_elims(1) fresh_fun_simp_OrL freshn_after_substn)
+next
+  case (ImpR name coname1 trm coname2)
+  with fin_rest_elims show ?case
+    by (fastforce simp add: fresh_prod trm.inject)
+next
+  case (ImpL coname trm1 name1 trm2 name2)
+  obtain a'::name where "a'\<sharp>(trm1{name2:=<c>.P},trm2{name2:=<c>.P},name1,P,x)"
+    by (meson exists_fresh(1) fs_name1)
+  with ImpL show ?case
+    apply (simp add: fresh_prod trm.inject)
+    by (metis abs_fresh(1) fin.intros(6) fin_ImpL_elim fin_rest_elims(1) fresh_fun_simp_ImpL freshn_after_substn)
+qed
+
 
 lemma fin_subst1:
-  assumes a: "fin M x" "x\<noteq>y" "x\<sharp>P"
+  assumes "fin M x" "x\<noteq>y" "x\<sharp>P"
   shows "fin (M{y:=<c>.P}) x"
-using a
-apply(nominal_induct M avoiding: x y c P rule: trm.strong_induct)
-apply(auto dest!: fin_elims simp add: subst_fresh abs_fresh)
-apply(rule fin.intros, simp add: subst_fresh abs_fresh)
-apply(rule fin.intros, simp add: subst_fresh abs_fresh)
-apply(rule fin.intros, simp add: subst_fresh abs_fresh)
-apply(rule fin.intros, simp add: subst_fresh abs_fresh)
-apply(rule fin.intros, simp add: subst_fresh abs_fresh, simp add: subst_fresh abs_fresh)
-apply(rule fin.intros, simp add: subst_fresh abs_fresh, simp add: subst_fresh abs_fresh)
-apply(rule fin.intros, simp add: subst_fresh abs_fresh, simp add: subst_fresh abs_fresh)
-apply(rule fin.intros, simp add: subst_fresh abs_fresh, simp add: subst_fresh abs_fresh)
-apply(rule fin.intros, simp add: subst_fresh abs_fresh, simp add: subst_fresh abs_fresh)
-done
+  using assms
+proof (nominal_induct M avoiding: x y c P rule: trm.strong_induct)
+  case (AndL1 name1 trm name2)
+  then show ?case
+    apply (clarsimp simp add: subst_fresh abs_fresh dest!: fin_AndL1_elim)
+    by (metis abs_fresh(1) fin.intros(3) fresh_prod subst_fresh(3))
+next
+  case (AndL2 name1 trm name2)
+  then show ?case
+    apply (clarsimp simp add: subst_fresh abs_fresh dest!: fin_AndL2_elim)
+    by (metis abs_fresh(1) fin.intros(4) fresh_prod subst_fresh(3))
+next
+  case (OrR1 coname1 trm coname2)
+  then show ?case
+    by (auto simp add: subst_fresh abs_fresh dest!: fin_rest_elims)
+next
+  case (OrR2 coname1 trm coname2)
+  then show ?case
+    by (auto simp add: subst_fresh abs_fresh dest!: fin_rest_elims)
+next
+  case (OrL name1 trm1 name2 trm2 name3)
+  then show ?case
+    apply (clarsimp simp add: subst_fresh abs_fresh)
+    by (metis abs_fresh(1) fin.intros(5) fin_OrL_elim fresh_prod subst_fresh(3))
+next
+  case (ImpR name coname1 trm coname2)
+  then show ?case
+    by (auto simp add: subst_fresh abs_fresh dest!: fin_rest_elims)
+next
+  case (ImpL coname trm1 name1 trm2 name2)
+  then show ?case
+    apply (clarsimp simp add: subst_fresh abs_fresh)
+    by (metis abs_fresh(1) fin.intros(6) fin_ImpL_elim fresh_prod subst_fresh(3))
+qed (auto dest!: fin_elims simp add: subst_fresh abs_fresh)
+
+
+thm abs_fresh fresh_prod
 
 lemma fin_subst2:
-  assumes a: "fin M y" "x\<noteq>y" "y\<sharp>P" "M\<noteq>Ax y c" 
+  assumes "fin M y" "x\<noteq>y" "y\<sharp>P" "M\<noteq>Ax y c" 
   shows "fin (M{c:=(x).P}) y"
-using a
-apply(nominal_induct M avoiding: x y c P rule: trm.strong_induct)
-apply(drule fin_elims)
-apply(simp add: trm.inject)
-apply(rule fin.intros)
-apply(drule fin_elims, simp)
-apply(drule fin_elims, simp)
-apply(drule fin_elims, simp)
-apply(rule fin.intros)
-apply(rule subst_fresh)
-apply(simp)
-apply(drule fin_elims, simp)
-apply(drule fin_elims, simp)
-apply(rule fin.intros)
-apply(simp add: abs_fresh fresh_atm)
-apply(rule subst_fresh)
-apply(auto)[1]
-apply(drule fin_elims, simp)
-apply(rule fin.intros)
-apply(simp add: abs_fresh fresh_atm)
-apply(rule subst_fresh)
-apply(auto)[1]
-apply(drule fin_elims, simp)
-apply(drule fin_elims, simp)
-apply(drule fin_elims, simp)
-apply(rule fin.intros)
-apply(simp add: abs_fresh fresh_atm)
-apply(rule subst_fresh)
-apply(auto)[1]
-apply(simp add: abs_fresh fresh_atm)
-apply(rule subst_fresh)
-apply(auto)[1]
-apply(drule fin_elims, simp)
-apply(drule fin_elims, simp)
-apply(rule fin.intros)
-apply(simp add: abs_fresh fresh_atm)
-apply(rule subst_fresh)
-apply(auto)[1]
-apply(simp add: abs_fresh fresh_atm)
-apply(rule subst_fresh)
-apply(auto)[1]
-done
+using assms
+proof (nominal_induct M avoiding: x y c P rule: trm.strong_induct)
+  case (Ax name coname)
+  then show ?case
+    using fin_Ax_elim by force
+next
+  case (NotL coname trm name)
+  then show ?case
+    by simp (metis fin.intros(2) fin_NotL_elim fresh_prod subst_fresh(5)) 
+next
+  case (AndL1 name1 trm name2)
+  then show ?case 
+    by simp (metis abs_fresh(1) fin.intros(3) fin_AndL1_elim fresh_prod subst_fresh(5))
+next
+  case (AndL2 name1 trm name2)
+  then show ?case 
+    by simp (metis abs_fresh(1) fin.intros(4) fin_AndL2_elim fresh_prod subst_fresh(5)) 
+next
+  case (OrL name1 trm1 name2 trm2 name3)
+  then show ?case
+    by simp (metis abs_fresh(1) fin.intros(5) fin_OrL_elim fresh_prod subst_fresh(5))
+next
+  case (ImpL coname trm1 name1 trm2 name2)
+  then show ?case
+    by simp (metis abs_fresh(1) fin.intros(6) fin_ImpL_elim fresh_prod subst_fresh(5))
+qed (use fin_rest_elims in force)+
 
 lemma fin_substn_nrename:
   assumes a: "fin M x" "x\<noteq>y" "x\<sharp>P"