
diff -r ffef122946a3 -r 1effd04264cc src/HOL/Nominal/Examples/Class1.thy
--- a/src/HOL/Nominal/Examples/Class1.thy	Fri Jul 19 22:29:32 2024 +0100
+++ b/src/HOL/Nominal/Examples/Class1.thy	Sat Jul 20 16:47:04 2024 +0100
@@ -1087,9 +1087,8 @@
 lemma forget:
   shows "x\<sharp>M \<Longrightarrow> M{x:=<c>.P} = M"
   and   "c\<sharp>M \<Longrightarrow> M{c:=(x).P} = M"
-apply(nominal_induct M avoiding: x c P rule: trm.strong_induct)
-apply(auto simp: fresh_atm abs_fresh abs_supp fin_supp)
-done
+  by (nominal_induct M avoiding: x c P rule: trm.strong_induct)
+     (auto simp: fresh_atm abs_fresh abs_supp fin_supp)
 
 lemma substc_rename1:
   assumes a: "c\<sharp>(M,a)"
@@ -2119,108 +2118,51 @@
     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"
+  assumes "fin M x" "x\<noteq>y" "x\<sharp>P"
   shows "M[x\<turnstile>n>y]{y:=<c>.P} = Cut <c>.P (x).(M{y:=<c>.P})"
-using a [[simproc del: defined_all]]
-apply(nominal_induct M avoiding: x y c P rule: trm.strong_induct)
-apply(drule fin_Ax_elim)
-apply(simp)
-apply(simp add: trm.inject)
-apply(simp add: alpha calc_atm fresh_atm)
-apply(simp)
-apply(drule fin_rest_elims)
-apply(simp)
-apply(drule fin_rest_elims)
-apply(simp)
-apply(drule fin_NotL_elim)
-apply(simp)
-apply(subgoal_tac "\<exists>z::name. z\<sharp>(trm,y,x,P,trm[x\<turnstile>n>y]{y:=<c>.P})")
-apply(erule exE, simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_NotL)
-apply(simp add: trm.inject alpha fresh_atm calc_atm abs_fresh)
-apply(rule conjI)
-apply(simp add: nsubst_eqvt calc_atm)
-apply(simp add: perm_fresh_fresh)
-apply(simp add: nrename_fresh)
-apply(rule subst_fresh)
-apply(simp)
-apply(rule exists_fresh')
-apply(rule fin_supp)
-apply(drule fin_rest_elims)
-apply(simp)
-apply(drule fin_AndL1_elim)
-apply(simp)
-apply(subgoal_tac "\<exists>z::name. z\<sharp>(name2,name1,P,trm[name2\<turnstile>n>y]{y:=<c>.P},y,P,trm)")
-apply(erule exE, simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_AndL1)
-apply(simp add: trm.inject alpha fresh_atm calc_atm abs_fresh)
-apply(rule conjI)
-apply(simp add: nsubst_eqvt calc_atm)
-apply(simp add: perm_fresh_fresh)
-apply(simp add: nrename_fresh)
-apply(rule subst_fresh)
-apply(simp)
-apply(rule exists_fresh')
-apply(rule fin_supp)
-apply(drule fin_AndL2_elim)
-apply(simp)
-apply(subgoal_tac "\<exists>z::name. z\<sharp>(name2,name1,P,trm[name2\<turnstile>n>y]{y:=<c>.P},y,P,trm)")
-apply(erule exE, simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_AndL2)
-apply(simp add: trm.inject alpha fresh_atm calc_atm abs_fresh)
-apply(rule conjI)
-apply(simp add: nsubst_eqvt calc_atm)
-apply(simp add: perm_fresh_fresh)
-apply(simp add: nrename_fresh)
-apply(rule subst_fresh)
-apply(simp)
-apply(rule exists_fresh')
-apply(rule fin_supp)
-apply(drule fin_rest_elims)
-apply(simp)
-apply(drule fin_rest_elims)
-apply(simp)
-apply(drule fin_OrL_elim)
-apply(simp add: abs_fresh)
-apply(simp add: subst_fresh rename_fresh)
-apply(subgoal_tac "\<exists>z::name. z\<sharp>(name3,name2,name1,P,trm1[name3\<turnstile>n>y]{y:=<c>.P},trm2[name3\<turnstile>n>y]{y:=<c>.P},y,P,trm1,trm2)")
-apply(erule exE, simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_OrL)
-apply(simp add: trm.inject alpha fresh_atm calc_atm abs_fresh)
-apply(rule conjI)
-apply(simp add: nsubst_eqvt calc_atm)
-apply(simp add: perm_fresh_fresh)
-apply(simp add: nrename_fresh)
-apply(simp add: nsubst_eqvt calc_atm)
-apply(simp add: perm_fresh_fresh)
-apply(simp add: nrename_fresh)
-apply(rule exists_fresh')
-apply(rule fin_supp)
-apply(drule fin_rest_elims)
-apply(simp)
-apply(drule fin_ImpL_elim)
-apply(simp add: abs_fresh)
-apply(simp add: subst_fresh rename_fresh)
-apply(subgoal_tac "\<exists>z::name. z\<sharp>(name1,x,P,trm1[x\<turnstile>n>y]{y:=<c>.P},trm2[x\<turnstile>n>y]{y:=<c>.P},y,P,trm1,trm2)")
-apply(erule exE, simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_ImpL)
-apply(simp add: trm.inject alpha fresh_atm calc_atm abs_fresh)
-apply(rule conjI)
-apply(simp add: nsubst_eqvt calc_atm)
-apply(simp add: perm_fresh_fresh)
-apply(simp add: nrename_fresh)
-apply(simp add: nsubst_eqvt calc_atm)
-apply(simp add: perm_fresh_fresh)
-apply(simp add: nrename_fresh)
-apply(rule exists_fresh')
-apply(rule fin_supp)
-done
+using assms [[simproc del: defined_all]]
+proof (nominal_induct M avoiding: x y c P rule: trm.strong_induct)
+  case (Ax name coname)
+  then show ?case
+    by (metis fin_Ax_elim fresh_atm(1,3) fresh_prod nrename_swap subst_rename(3) substn.simps(1) trm.fresh(1))
+next
+  case (NotL coname trm name)
+  obtain z::name where "z \<sharp> (trm,y,x,P,trm[x\<turnstile>n>y]{y:=<c>.P})"
+    by (meson exists_fresh(1) fs_name1)
+  with NotL show ?case 
+    apply (clarsimp simp add: fresh_prod fresh_fun_simp_NotL trm.inject alpha fresh_atm calc_atm abs_fresh)
+    by (metis fin_NotL_elim nrename_fresh nrename_swap substn_nrename_comm')
+next
+  case (AndL1 name1 trm name2)
+  obtain z::name where "z \<sharp> (name2,name1,P,trm[name2\<turnstile>n>y]{y:=<c>.P},y,P,trm)"
+    by (meson exists_fresh(1) fs_name1)
+  with AndL1 show ?case 
+    using fin_AndL1_elim[OF AndL1.prems(1)]
+    by simp (metis abs_fresh(1) fresh_atm(1) fresh_fun_simp_AndL1 fresh_prod nrename_fresh subst_fresh(3))
+next
+  case (AndL2 name1 trm name2)
+  obtain z::name where "z \<sharp> (name2,name1,P,trm[name2\<turnstile>n>y]{y:=<c>.P},y,P,trm)"
+    by (meson exists_fresh(1) fs_name1)
+  with AndL2 show ?case 
+    using fin_AndL2_elim[OF AndL2.prems(1)]
+    by simp (metis abs_fresh(1) fresh_atm(1) fresh_fun_simp_AndL2 fresh_prod nrename_fresh subst_fresh(3))
+next
+  case (OrL name1 trm1 name2 trm2 name3)
+  obtain z::name where "z \<sharp> (name3,name2,name1,P,trm1[name3\<turnstile>n>y]{y:=<c>.P},trm2[name3\<turnstile>n>y]{y:=<c>.P},y,P,trm1,trm2)"
+    by (meson exists_fresh(1) fs_name1)
+  with OrL show ?case 
+    using fin_OrL_elim[OF OrL.prems(1)]
+    by (auto simp add: abs_fresh fresh_fun_simp_OrL fresh_atm(1) nrename_fresh subst_fresh(3))
+next
+  case (ImpL coname trm1 name1 trm2 name2)
+  obtain z::name where "z \<sharp> (name1,x,P,trm1[x\<turnstile>n>y]{y:=<c>.P},trm2[x\<turnstile>n>y]{y:=<c>.P},y,P,trm1,trm2)"
+    by (meson exists_fresh(1) fs_name1)
+  with ImpL show ?case 
+    using fin_ImpL_elim[OF ImpL.prems(1)]
+    by (auto simp add: abs_fresh fresh_fun_simp_ImpL fresh_atm(1) nrename_fresh subst_fresh(3))
+qed (use fin_rest_elims in force)+
 
 inductive
   fic :: "trm \<Rightarrow> coname \<Rightarrow> bool"
@@ -2283,157 +2225,110 @@
    (auto simp: calc_atm simp add: fresh_left abs_fresh)
 
 lemma not_fic_subst1:
-  assumes a: "\<not>(fic M a)" 
+  assumes "\<not>(fic M a)" 
   shows "\<not>(fic (M{y:=<c>.P}) a)"
-using a
-apply(nominal_induct M avoiding: a c y P rule: trm.strong_induct)
-apply(auto)
-apply(drule fic_elims, simp)
-apply(drule fic_elims, simp)
-apply(drule fic_elims, simp)
-apply(drule fic_elims)
-apply(auto)[1]
-apply(drule freshc_after_substn)
-apply(simp add: fic.intros)
-apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(trm{y:=<c>.P},P,a)")
-apply(erule exE)
-apply(simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_NotL)
-apply(drule fic_elims, simp)
-apply(rule exists_fresh'(1)[OF fs_name1])
-apply(drule fic_elims, simp)
-apply(drule fic_elims)
-apply(auto)[1]
-apply(simp add: abs_fresh fresh_atm)
-apply(drule freshc_after_substn)
-apply(drule freshc_after_substn)
-apply(simp add: fic.intros abs_fresh)
-apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(trm{y:=<c>.P},P,name1,a)")
-apply(erule exE)
-apply(simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_AndL1)
-apply(drule fic_elims, simp)
-apply(rule exists_fresh'(1)[OF fs_name1])
-apply(drule fic_elims, simp)
-apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(trm{y:=<c>.P},P,name1,a)")
-apply(erule exE)
-apply(simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_AndL2)
-apply(drule fic_elims, simp)
-apply(rule exists_fresh'(1)[OF fs_name1])
-apply(drule fic_elims, simp)
-apply(drule fic_elims)
-apply(auto)[1]
-apply(simp add: abs_fresh fresh_atm)
-apply(drule freshc_after_substn)
-apply(simp add: fic.intros abs_fresh)
-apply(drule fic_elims)
-apply(auto)[1]
-apply(simp add: abs_fresh fresh_atm)
-apply(drule freshc_after_substn)
-apply(simp add: fic.intros abs_fresh)
-apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(trm1{y:=<c>.P},trm2{y:=<c>.P},P,name1,name2,a)")
-apply(erule exE)
-apply(simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_OrL)
-apply(drule fic_elims, simp)
-apply(rule exists_fresh'(1)[OF fs_name1])
-apply(drule fic_elims, simp)
-apply(drule fic_elims, simp)
-apply(simp add: abs_fresh fresh_atm)
-apply(drule freshc_after_substn)
-apply(simp add: fic.intros abs_fresh)
-apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(trm1{name2:=<c>.P},trm2{name2:=<c>.P},P,name1,name2,a)")
-apply(erule exE)
-apply(simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_ImpL)
-apply(drule fic_elims, simp)
-apply(rule exists_fresh'(1)[OF fs_name1])
-apply(drule fic_elims, simp)
-done
+using assms
+proof (nominal_induct M avoiding: a c y P rule: trm.strong_induct)
+  case (Ax name coname)
+  then show ?case
+    using fic_rest_elims(1) substn.simps(1) by presburger
+next
+  case (Cut coname trm1 name trm2)
+  then show ?case
+    by (metis abs_fresh(2) better_Cut_substn fic_rest_elims(1) fresh_prod)
+next
+  case (NotR name trm coname)
+  then show ?case
+    by (metis fic.intros(2) fic_NotR_elim fresh_prod freshc_after_substn substn.simps(3))
+next
+  case (NotL coname trm name)
+  obtain x'::name where "x' \<sharp> (trm{y:=<c>.P},P,a)"
+    by (meson exists_fresh(1) fs_name1)
+  with NotL show ?case
+    by (simp add: fic.intros fresh_prod) (metis fic_rest_elims(1,2) fresh_fun_simp_NotL)
+next
+  case (AndR coname1 trm1 coname2 trm2 coname3)
+  then show ?case
+    by simp (metis abs_fresh(2) fic.intros(3) fic_AndR_elim freshc_after_substn)
+next
+  case (AndL1 name1 trm name2)
+  obtain x'::name where "x' \<sharp> (trm{y:=<c>.P},P,name1,a)"
+    by (meson exists_fresh(1) fs_name1)
+  with AndL1 fic_rest_elims show ?case
+    by (simp add: fic.intros fresh_prod)(metis fresh_fun_simp_AndL1)
+next
+  case (AndL2 name1 trm name2)
+  obtain x'::name where "x' \<sharp> (trm{y:=<c>.P},P,name1,a)"
+    by (meson exists_fresh(1) fs_name1)
+  with AndL2 fic_rest_elims show ?case
+    by (simp add: fic.intros fresh_prod) (metis fresh_fun_simp_AndL2)
+next
+  case (OrR1 coname1 trm coname2)
+  then show ?case
+    by simp (metis abs_fresh(2) fic.simps fic_OrR1_elim freshc_after_substn)
+next
+  case (OrR2 coname1 trm coname2)
+  then show ?case
+    by simp (metis abs_fresh(2) fic.simps fic_OrR2_elim freshc_after_substn)
+next
+  case (OrL name1 trm1 name2 trm2 name3)
+  obtain x'::name where "x' \<sharp> (trm1{y:=<c>.P},trm2{y:=<c>.P},P,name1,name2,a)"
+    by (meson exists_fresh(1) fs_name1)
+  with OrL fic_rest_elims show ?case
+    by (simp add: fic.intros fresh_prod) (metis fresh_fun_simp_OrL)
+next
+  case (ImpR name coname1 trm coname2)
+  then show ?case 
+    by simp (metis abs_fresh(2) fic.intros(6) fic_ImpR_elim freshc_after_substn)
+next
+  case (ImpL coname trm1 name1 trm2 name2)
+  obtain x'::name where "x' \<sharp> (trm1{name2:=<c>.P},trm2{name2:=<c>.P},P,name1,name2,a)"
+    by (meson exists_fresh(1) fs_name1)
+  with ImpL fic_rest_elims fresh_fun_simp_ImpL show ?case
+    by (simp add: fresh_prod) fastforce
+qed
 
 lemma not_fic_subst2:
-  assumes a: "\<not>(fic M a)" 
+  assumes "\<not>(fic M a)" 
   shows "\<not>(fic (M{c:=(y).P}) a)"
-using a
-apply(nominal_induct M avoiding: a c y P rule: trm.strong_induct)
-apply(auto)
-apply(drule fic_elims, simp)
-apply(drule fic_elims, simp)
-apply(drule fic_elims, simp)
-apply(subgoal_tac "\<exists>c'::coname. c'\<sharp>(trm{coname:=(y).P},P,a)")
-apply(erule exE)
-apply(simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_NotR)
-apply(drule fic_elims, simp)
-apply(rule exists_fresh'(2)[OF fs_coname1])
-apply(drule fic_elims, simp)
-apply(drule freshc_after_substc)
-apply(simp)
-apply(simp add: fic.intros abs_fresh)
-apply(drule fic_elims, simp)
-apply(subgoal_tac "\<exists>c'::coname. c'\<sharp>(trm1{coname3:=(y).P},trm2{coname3:=(y).P},P,coname1,coname2,a)")
-apply(erule exE)
-apply(simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_AndR)
-apply(drule fic_elims, simp)
-apply(rule exists_fresh'(2)[OF fs_coname1])
-apply(drule fic_elims, simp)
-apply(auto)[1]
-apply(simp add: abs_fresh fresh_atm)
-apply(drule freshc_after_substc)
-apply(simp)
-apply(drule freshc_after_substc)
-apply(simp)
-apply(simp add: fic.intros abs_fresh)
-apply(drule fic_elims, simp)
-apply(drule fic_elims, simp)
-apply(subgoal_tac "\<exists>c'::coname. c'\<sharp>(trm{coname2:=(y).P},P,coname1,a)")
-apply(erule exE)
-apply(simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_OrR1)
-apply(drule fic_elims, simp)
-apply(rule exists_fresh'(2)[OF fs_coname1])
-apply(drule fic_elims, simp)
-apply(simp add: abs_fresh fresh_atm)
-apply(drule freshc_after_substc)
-apply(simp)
-apply(simp add: fic.intros abs_fresh)
-apply(subgoal_tac "\<exists>c'::coname. c'\<sharp>(trm{coname2:=(y).P},P,coname1,a)")
-apply(erule exE)
-apply(simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_OrR2)
-apply(drule fic_elims, simp)
-apply(rule exists_fresh'(2)[OF fs_coname1])
-apply(drule fic_elims, simp)
-apply(simp add: abs_fresh fresh_atm)
-apply(drule freshc_after_substc)
-apply(simp)
-apply(simp add: fic.intros abs_fresh)
-apply(drule fic_elims, simp)
-apply(subgoal_tac "\<exists>c'::coname. c'\<sharp>(trm{coname2:=(y).P},P,coname1,a)")
-apply(erule exE)
-apply(simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_ImpR)
-apply(drule fic_elims, simp)
-apply(rule exists_fresh'(2)[OF fs_coname1])
-apply(drule fic_elims, simp)
-apply(simp add: abs_fresh fresh_atm)
-apply(drule freshc_after_substc)
-apply(simp)
-apply(simp add: fic.intros abs_fresh)
-apply(drule fic_elims, simp)
-done
+using assms
+proof (nominal_induct M avoiding: a c y P rule: trm.strong_induct)
+  case (NotR name trm coname)
+  obtain c'::coname where "c'\<sharp>(trm{coname:=(y).P},P,a)"
+    by (meson exists_fresh'(2) fs_coname1)
+  with NotR fic_rest_elims show ?case
+    apply (clarsimp simp: fresh_prod fresh_fun_simp_NotR)
+    by (metis fic.intros(2) fic_NotR_elim freshc_after_substc)
+next
+  case (AndR coname1 trm1 coname2 trm2 coname3)
+  obtain c'::coname where "c'\<sharp>(trm1{coname3:=(y).P},trm2{coname3:=(y).P},P,coname1,coname2,a)"
+    by (meson exists_fresh'(2) fs_coname1)
+  with AndR fic_rest_elims show ?case
+    apply (clarsimp simp: fresh_prod fresh_fun_simp_AndR)
+    by (metis abs_fresh(2) fic.intros(3) fic_AndR_elim freshc_after_substc)
+next
+  case (OrR1 coname1 trm coname2)
+  obtain c'::coname where "c'\<sharp>(trm{coname2:=(y).P},P,coname1,a)"
+    by (meson exists_fresh'(2) fs_coname1)
+  with OrR1 fic_rest_elims show ?case
+    apply (clarsimp simp: fresh_prod fresh_fun_simp_OrR1)
+    by (metis abs_fresh(2) fic.intros(4) fic_OrR1_elim freshc_after_substc)
+next
+  case (OrR2 coname1 trm coname2)
+  obtain c'::coname where "c'\<sharp>(trm{coname2:=(y).P},P,coname1,a)"
+    by (meson exists_fresh'(2) fs_coname1)
+  with OrR2 fic_rest_elims show ?case
+    apply (clarsimp simp: fresh_prod fresh_fun_simp_OrR2)
+    by (metis abs_fresh(2) fic.simps fic_OrR2_elim freshc_after_substc)
+next
+  case (ImpR name coname1 trm coname2)
+  obtain c'::coname where "c'\<sharp>(trm{coname2:=(y).P},P,coname1,a)"
+    by (meson exists_fresh'(2) fs_coname1)
+  with ImpR fic_rest_elims show ?case
+    apply (clarsimp simp: fresh_prod fresh_fun_simp_ImpR)
+    by (metis abs_fresh(2) fic.intros(6) fic_ImpR_elim freshc_after_substc)
+qed (use fic_rest_elims in auto)
+
 
 lemma fic_subst1:
   assumes a: "fic M a" "a\<noteq>b" "a\<sharp>P"




