# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1721844479 -3600
# Node ID 21bb6d17d58e3f31d34b9bf8e0b400a87c17f25e
# Parent  e65eed943bee9057f88d021a7a30669293f007ad
Adjusting the precedences to reduce syntactic ambiguity

diff -r e65eed943bee -r 21bb6d17d58e src/HOL/Nominal/Examples/Class1.thy
--- a/src/HOL/Nominal/Examples/Class1.thy	Tue Jul 23 15:54:43 2024 +0100
+++ b/src/HOL/Nominal/Examples/Class1.thy	Wed Jul 24 19:07:59 2024 +0100
@@ -73,7 +73,7 @@
 text \<open>renaming functions\<close>
 
 nominal_primrec (freshness_context: "(d::coname,e::coname)") 
-  crename :: "trm \<Rightarrow> coname \<Rightarrow> coname \<Rightarrow> trm"  ("_[_\<turnstile>c>_]" [100,100,100] 100) 
+  crename :: "trm \<Rightarrow> coname \<Rightarrow> coname \<Rightarrow> trm"  ("_[_\<turnstile>c>_]" [100,0,0] 100) 
 where
   "(Ax x a)[d\<turnstile>c>e] = (if a=d then Ax x e else Ax x a)" 
 | "\<lbrakk>a\<sharp>(d,e,N);x\<sharp>M\<rbrakk> \<Longrightarrow> (Cut <a>.M (x).N)[d\<turnstile>c>e] = Cut <a>.(M[d\<turnstile>c>e]) (x).(N[d\<turnstile>c>e])" 
@@ -92,7 +92,7 @@
   by(finite_guess | simp add: abs_fresh abs_supp fin_supp | fresh_guess)+
 
 nominal_primrec (freshness_context: "(u::name,v::name)") 
-  nrename :: "trm \<Rightarrow> name \<Rightarrow> name \<Rightarrow> trm"      ("_[_\<turnstile>n>_]" [100,100,100] 100) 
+  nrename :: "trm \<Rightarrow> name \<Rightarrow> name \<Rightarrow> trm"      ("_[_\<turnstile>n>_]" [100,0,0] 100) 
 where
   "(Ax x a)[u\<turnstile>n>v] = (if x=u then Ax v a else Ax x a)" 
 | "\<lbrakk>a\<sharp>N;x\<sharp>(u,v,M)\<rbrakk> \<Longrightarrow> (Cut <a>.M (x).N)[u\<turnstile>n>v] = Cut <a>.(M[u\<turnstile>n>v]) (x).(N[u\<turnstile>n>v])" 
@@ -3477,7 +3477,7 @@
 text \<open>Transitive Closure\<close>
 
 abbreviation
- a_star_redu :: "trm \<Rightarrow> trm \<Rightarrow> bool" ("_ \<longrightarrow>\<^sub>a* _" [100,100] 100)
+ a_star_redu :: "trm \<Rightarrow> trm \<Rightarrow> bool" ("_ \<longrightarrow>\<^sub>a* _" [80,80] 80)
 where
   "M \<longrightarrow>\<^sub>a* M' \<equiv> (a_redu)\<^sup>*\<^sup>* M M'"
 
@@ -3581,500 +3581,199 @@
                       a_star_OrL a_star_OrR1 a_star_OrR2 a_star_ImpL a_star_ImpR
 
 lemma a_star_redu_NotL_elim:
-  assumes a: "NotL <a>.M x \<longrightarrow>\<^sub>a* R"
+  assumes "NotL <a>.M x \<longrightarrow>\<^sub>a* R"
   shows "\<exists>M'. R = NotL <a>.M' x \<and> M \<longrightarrow>\<^sub>a* M'"
-using a
-apply(induct set: rtranclp)
-apply(auto)
-apply(drule a_redu_NotL_elim)
-apply(auto)
-done
+  using assms by (induct set: rtranclp) (use a_redu_NotL_elim in force)+
 
 lemma a_star_redu_NotR_elim:
-  assumes a: "NotR (x).M a \<longrightarrow>\<^sub>a* R"
+  assumes "NotR (x).M a \<longrightarrow>\<^sub>a* R"
   shows "\<exists>M'. R = NotR (x).M' a \<and> M \<longrightarrow>\<^sub>a* M'"
-using a
-apply(induct set: rtranclp)
-apply(auto)
-apply(drule a_redu_NotR_elim)
-apply(auto)
-done
+  using assms by (induct set: rtranclp) (use a_redu_NotR_elim in force)+
 
 lemma a_star_redu_AndR_elim:
-  assumes a: "AndR <a>.M <b>.N c\<longrightarrow>\<^sub>a* R"
+  assumes "AndR <a>.M <b>.N c\<longrightarrow>\<^sub>a* R"
   shows "(\<exists>M' N'. R = AndR <a>.M' <b>.N' c \<and> M \<longrightarrow>\<^sub>a* M' \<and> N \<longrightarrow>\<^sub>a* N')"
-using a
-apply(induct set: rtranclp)
-apply(auto)
-apply(drule a_redu_AndR_elim)
-apply(auto simp: alpha trm.inject)
-done
+  using assms by (induct set: rtranclp) (use a_redu_AndR_elim in force)+
 
 lemma a_star_redu_AndL1_elim:
-  assumes a: "AndL1 (x).M y \<longrightarrow>\<^sub>a* R"
+  assumes "AndL1 (x).M y \<longrightarrow>\<^sub>a* R"
   shows "\<exists>M'. R = AndL1 (x).M' y \<and> M \<longrightarrow>\<^sub>a* M'"
-using a
-apply(induct set: rtranclp)
-apply(auto)
-apply(drule a_redu_AndL1_elim)
-apply(auto simp: alpha trm.inject)
-done
+  using assms by (induct set: rtranclp) (use a_redu_AndL1_elim in force)+
 
 lemma a_star_redu_AndL2_elim:
-  assumes a: "AndL2 (x).M y \<longrightarrow>\<^sub>a* R"
+  assumes "AndL2 (x).M y \<longrightarrow>\<^sub>a* R"
   shows "\<exists>M'. R = AndL2 (x).M' y \<and> M \<longrightarrow>\<^sub>a* M'"
-using a
-apply(induct set: rtranclp)
-apply(auto)
-apply(drule a_redu_AndL2_elim)
-apply(auto simp: alpha trm.inject)
-done
+  using assms by (induct set: rtranclp) (use a_redu_AndL2_elim in force)+
 
 lemma a_star_redu_OrL_elim:
-  assumes a: "OrL (x).M (y).N z \<longrightarrow>\<^sub>a* R"
+  assumes "OrL (x).M (y).N z \<longrightarrow>\<^sub>a* R"
   shows "(\<exists>M' N'. R = OrL (x).M' (y).N' z \<and> M \<longrightarrow>\<^sub>a* M' \<and> N \<longrightarrow>\<^sub>a* N')"
-using a
-apply(induct set: rtranclp)
-apply(auto)
-apply(drule a_redu_OrL_elim)
-apply(auto simp: alpha trm.inject)
-done
+  using assms by (induct set: rtranclp) (use a_redu_OrL_elim in force)+
 
 lemma a_star_redu_OrR1_elim:
-  assumes a: "OrR1 <a>.M y \<longrightarrow>\<^sub>a* R"
+  assumes "OrR1 <a>.M y \<longrightarrow>\<^sub>a* R"
   shows "\<exists>M'. R = OrR1 <a>.M' y \<and> M \<longrightarrow>\<^sub>a* M'"
-using a
-apply(induct set: rtranclp)
-apply(auto)
-apply(drule a_redu_OrR1_elim)
-apply(auto simp: alpha trm.inject)
-done
+  using assms by (induct set: rtranclp) (use a_redu_OrR1_elim in force)+
 
 lemma a_star_redu_OrR2_elim:
-  assumes a: "OrR2 <a>.M y \<longrightarrow>\<^sub>a* R"
+  assumes "OrR2 <a>.M y \<longrightarrow>\<^sub>a* R"
   shows "\<exists>M'. R = OrR2 <a>.M' y \<and> M \<longrightarrow>\<^sub>a* M'"
-using a
-apply(induct set: rtranclp)
-apply(auto)
-apply(drule a_redu_OrR2_elim)
-apply(auto simp: alpha trm.inject)
-done
+  using assms by (induct set: rtranclp) (use a_redu_OrR2_elim in force)+
 
 lemma a_star_redu_ImpR_elim:
-  assumes a: "ImpR (x).<a>.M y \<longrightarrow>\<^sub>a* R"
+  assumes "ImpR (x).<a>.M y \<longrightarrow>\<^sub>a* R"
   shows "\<exists>M'. R = ImpR (x).<a>.M' y \<and> M \<longrightarrow>\<^sub>a* M'"
-using a
-apply(induct set: rtranclp)
-apply(auto)
-apply(drule a_redu_ImpR_elim)
-apply(auto simp: alpha trm.inject)
-done
+  using assms by (induct set: rtranclp) (use a_redu_ImpR_elim in force)+
 
 lemma a_star_redu_ImpL_elim:
-  assumes a: "ImpL <a>.M (y).N z \<longrightarrow>\<^sub>a* R"
+  assumes "ImpL <a>.M (y).N z \<longrightarrow>\<^sub>a* R"
   shows "(\<exists>M' N'. R = ImpL <a>.M' (y).N' z \<and> M \<longrightarrow>\<^sub>a* M' \<and> N \<longrightarrow>\<^sub>a* N')"
-using a
-apply(induct set: rtranclp)
-apply(auto)
-apply(drule a_redu_ImpL_elim)
-apply(auto simp: alpha trm.inject)
-done
+  using assms by (induct set: rtranclp) (use a_redu_ImpL_elim in force)+
 
 text \<open>Substitution\<close>
 
 lemma subst_not_fin1:
   shows "\<not>fin(M{x:=<c>.P}) x"
-apply(nominal_induct M avoiding: x c P rule: trm.strong_induct)
-apply(auto)
-apply(drule fin_elims, simp)
-apply(drule fin_elims, simp)
-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>x'::name. x'\<sharp>(trm{x:=<c>.P},P)")
-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(erule fin.cases, simp_all add: trm.inject)
-apply(erule fin.cases, simp_all add: trm.inject)
-apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(trm{x:=<c>.P},P,name1)")
-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(erule fin.cases, simp_all add: trm.inject)
-apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(trm{x:=<c>.P},P,name1)")
-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(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>x'::name. x'\<sharp>(trm1{x:=<c>.P},P,name1,trm2{x:=<c>.P},name2)")
-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(erule fin.cases, simp_all add: trm.inject)
-apply(erule fin.cases, simp_all add: trm.inject)
-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)
-apply(erule fin.cases, simp_all add: trm.inject)
-apply(rule exists_fresh'(1)[OF fs_name1])
-apply(erule fin.cases, simp_all add: trm.inject)
-done
-
-lemma subst_not_fin2:
-  assumes a: "\<not>fin M y"
-  shows "\<not>fin(M{c:=(x).P}) y" 
-using a
-apply(nominal_induct M avoiding: x c P y 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>c'::coname. c'\<sharp>(trm{coname:=(x).P},P)")
-apply(erule exE)
-apply(simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_NotR)
-apply(drule fin_elims, simp)
-apply(rule exists_fresh'(2)[OF fs_coname1])
-apply(drule fin_elims, simp)
-apply(drule fin_elims, simp)
-apply(drule freshn_after_substc)
-apply(simp add: fin.intros)
-apply(subgoal_tac "\<exists>c'::coname. c'\<sharp>(trm1{coname3:=(x).P},P,coname1,trm2{coname3:=(x).P},coname2)")
-apply(erule exE)
-apply(simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_AndR)
-apply(drule fin_elims, simp)
-apply(rule exists_fresh'(2)[OF fs_coname1])
-apply(drule fin_elims, simp)
-apply(drule fin_elims, simp)
-apply(simp add: abs_fresh fresh_atm)
-apply(drule freshn_after_substc)
-apply(simp add: fin.intros abs_fresh)
-apply(drule fin_elims, simp)
-apply(simp add: abs_fresh fresh_atm)
-apply(drule freshn_after_substc)
-apply(simp add: fin.intros abs_fresh)
-apply(subgoal_tac "\<exists>c'::coname. c'\<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)
-apply(drule fin_elims, simp)
-apply(rule exists_fresh'(2)[OF fs_coname1])
-apply(drule fin_elims, simp)
-apply(subgoal_tac "\<exists>c'::coname. c'\<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)
-apply(drule fin_elims, simp)
-apply(rule exists_fresh'(2)[OF fs_coname1])
-apply(drule fin_elims, simp)
-apply(drule fin_elims, simp)
-apply(auto)[1]
-apply(simp add: abs_fresh fresh_atm)
-apply(drule freshn_after_substc)
-apply(drule freshn_after_substc)
-apply(simp add: fin.intros abs_fresh)
-apply(subgoal_tac "\<exists>c'::coname. c'\<sharp>(trm{coname2:=(x).P},P,coname1,coname2)")
-apply(erule exE)
-apply(simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_ImpR)
-apply(drule fin_elims, simp)
-apply(rule exists_fresh'(2)[OF fs_coname1])
-apply(drule fin_elims, simp)
-apply(drule fin_elims, simp)
-apply(auto)[1]
-apply(simp add: abs_fresh fresh_atm)
-apply(drule freshn_after_substc)
-apply(drule freshn_after_substc)
-apply(simp add: fin.intros abs_fresh)
-done
-
-lemma subst_not_fic1:
-  shows "\<not>fic (M{a:=(x).P}) a"
-apply(nominal_induct M avoiding: a x P rule: trm.strong_induct)
-apply(auto)
-apply(erule fic.cases, simp_all add: trm.inject)
-apply(erule fic.cases, simp_all add: trm.inject)
-apply(erule fic.cases, simp_all add: trm.inject)
-apply(erule fic.cases, simp_all add: trm.inject)
-apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(trm{coname:=(x).P},P)")
-apply(erule exE)
-apply(simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_NotR)
-apply(erule fic.cases, simp_all add: trm.inject)
-apply(rule exists_fresh'(2)[OF fs_coname1])
-apply(erule fic.cases, simp_all add: trm.inject)
-apply(erule fic.cases, simp_all add: trm.inject)
-apply(subgoal_tac "\<exists>a'::coname. a'\<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)
-apply(erule fic.cases, simp_all add: trm.inject)
-apply(rule exists_fresh'(2)[OF fs_coname1])
-apply(erule fic.cases, simp_all add: trm.inject)
-apply(erule fic.cases, simp_all add: trm.inject)
-apply(erule fic.cases, simp_all add: trm.inject)
-apply(subgoal_tac "\<exists>a'::coname. a'\<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)
-apply(erule fic.cases, simp_all add: trm.inject)
-apply(rule exists_fresh'(2)[OF fs_coname1])
-apply(erule fic.cases, simp_all add: trm.inject)
-apply(subgoal_tac "\<exists>a'::coname. a'\<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)
-apply(erule fic.cases, simp_all add: trm.inject)
-apply(rule exists_fresh'(2)[OF fs_coname1])
-apply(erule fic.cases, simp_all add: trm.inject)
-apply(erule fic.cases, simp_all add: trm.inject)
-apply(subgoal_tac "\<exists>a'::coname. a'\<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)
-apply(erule fic.cases, simp_all add: trm.inject)
-apply(rule exists_fresh'(2)[OF fs_coname1])
-apply(erule fic.cases, simp_all add: trm.inject)
-apply(erule fic.cases, simp_all add: trm.inject)
-done
-
-lemma subst_not_fic2:
-  assumes a: "\<not>fic M a"
-  shows "\<not>fic(M{x:=<b>.P}) a" 
-using a
-apply(nominal_induct M avoiding: x a P b 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, simp)
-apply(drule freshc_after_substn)
-apply(simp add: fic.intros)
-apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(trm{x:=<b>.P},P)")
-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, simp)
-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{x:=<b>.P},P,name1)")
-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{x:=<b>.P},P,name1)")
-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, simp)
-apply(simp add: abs_fresh fresh_atm)
-apply(drule freshc_after_substn)
-apply(simp add: fic.intros abs_fresh)
-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{x:=<b>.P},P,name1,trm2{x:=<b>.P},name2)")
-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:=<b>.P},trm2{name2:=<b>.P},P,name1)")
-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
+proof (nominal_induct M avoiding: x c P rule: trm.strong_induct)
+  case (Ax name coname)
+  with fin_rest_elims show ?case
+    by (auto simp: fin_Ax_elim)
+next
+  case (NotL coname trm name)
+  obtain x'::name where "x'\<sharp>(trm{x:=<c>.P},P)"
+    by (meson exists_fresh(1) fs_name1)
+  with NotL fin_NotL_elim fresh_fun_simp_NotL show ?case
+    by simp (metis fin_rest_elims(1) fresh_prod)
+next
+  case (AndL1 name1 trm name2)
+  obtain x'::name where "x' \<sharp> (trm{x:=<c>.P},P,name1)"
+    by (meson exists_fresh(1) fs_name1)
+  with AndL1 fin_AndL1_elim fresh_fun_simp_AndL1 show ?case
+    by simp (metis fin_rest_elims(1) fresh_prod)
+next
+  case (AndL2 name2 trm name2)
+  obtain x'::name where "x' \<sharp> (trm{x:=<c>.P},P,name2)"
+    by (meson exists_fresh(1) fs_name1)
+  with AndL2 fin_AndL2_elim fresh_fun_simp_AndL2 better_AndL2_substn show ?case
+    by (metis abs_fresh(1) fresh_atm(1) not_fin_subst2)
+next
+  case (OrL name1 trm1 name2 trm2 name3)
+  obtain x'::name where "x' \<sharp> (trm1{x:=<c>.P},P,name1,trm2{x:=<c>.P},name2)"
+    by (meson exists_fresh(1) fs_name1)
+  with OrL fin_OrL_elim fresh_fun_simp_OrL show ?case
+    by simp (metis fin_rest_elims(1) fresh_prod)
+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 fin_ImpL_elim fresh_fun_simp_ImpL show ?case
+    by simp (metis fin_rest_elims(1) fresh_prod)
+qed (use fin_rest_elims not_fin_subst2 in auto)
+
+lemmas subst_not_fin2 = not_fin_subst1
 
 text \<open>Reductions\<close>
 
 lemma fin_l_reduce:
-  assumes  a: "fin M x"
-  and      b: "M \<longrightarrow>\<^sub>l M'"
+  assumes "fin M x" and "M \<longrightarrow>\<^sub>l M'"
   shows "fin M' x"
-using b a
-apply(induct)
-apply(erule fin.cases)
-apply(simp_all add: trm.inject)
-apply(rotate_tac 3)
-apply(erule fin.cases)
-apply(simp_all add: trm.inject)
-apply(erule fin.cases, simp_all add: trm.inject)+
-done
+  using assms fin_rest_elims(1) l_redu.simps by fastforce
 
 lemma fin_c_reduce:
-  assumes  a: "fin M x"
-  and      b: "M \<longrightarrow>\<^sub>c M'"
+  assumes "fin M x" and "M \<longrightarrow>\<^sub>c M'"
   shows "fin M' x"
-using b a
-apply(induct)
-apply(erule fin.cases, simp_all add: trm.inject)+
-done
+  using assms c_redu.simps fin_rest_elims(1) by fastforce
 
 lemma fin_a_reduce:
   assumes  a: "fin M x"
   and      b: "M \<longrightarrow>\<^sub>a M'"
   shows "fin M' x"
-using a b
-apply(induct)
-apply(drule ax_do_not_a_reduce)
-apply(simp)
-apply(drule a_redu_NotL_elim)
-apply(auto)
-apply(rule fin.intros)
-apply(simp add: fresh_a_redu)
-apply(drule a_redu_AndL1_elim)
-apply(auto)
-apply(rule fin.intros)
-apply(force simp add: abs_fresh fresh_a_redu)
-apply(drule a_redu_AndL2_elim)
-apply(auto)
-apply(rule fin.intros)
-apply(force simp add: abs_fresh fresh_a_redu)
-apply(drule a_redu_OrL_elim)
-apply(auto)
-apply(rule fin.intros)
-apply(force simp add: abs_fresh fresh_a_redu)
-apply(force simp add: abs_fresh fresh_a_redu)
-apply(rule fin.intros)
-apply(force simp add: abs_fresh fresh_a_redu)
-apply(force simp add: abs_fresh fresh_a_redu)
-apply(drule a_redu_ImpL_elim)
-apply(auto)
-apply(rule fin.intros)
-apply(force simp add: abs_fresh fresh_a_redu)
-apply(force simp add: abs_fresh fresh_a_redu)
-apply(rule fin.intros)
-apply(force simp add: abs_fresh fresh_a_redu)
-apply(force simp add: abs_fresh fresh_a_redu)
-done
+using assms
+proof (induct)
+  case (1 x a)
+  then show ?case
+    using ax_do_not_a_reduce by auto
+next
+  case (2 x M a)
+  then show ?case
+    using a_redu_NotL_elim fresh_a_redu1 by blast
+next
+  case (3 y x M)
+  then show ?case
+    by (metis a_redu_AndL1_elim abs_fresh(1) fin.intros(3) fresh_a_redu1)
+next
+  case (4 y x M)
+  then show ?case
+    by (metis a_redu_AndL2_elim abs_fresh(1) fin.intros(4) fresh_a_redu1)
+next
+  case (5 z x M y N)
+  then show ?case
+    by (smt (verit) a_redu_OrL_elim abs_fresh(1) fin.intros(5) fresh_a_redu1)
+next
+  case (6 y M x N a)
+  then show ?case
+    by (smt (verit, best) a_redu_ImpL_elim abs_fresh(1) fin.simps fresh_a_redu1)
+qed
+
 
 lemma fin_a_star_reduce:
   assumes  a: "fin M x"
   and      b: "M \<longrightarrow>\<^sub>a* M'"
   shows "fin M' x"
-using b a
-apply(induct set: rtranclp)
-apply(auto simp: fin_a_reduce)
-done
+using b a by (induct set: rtranclp)(auto simp: fin_a_reduce)
 
 lemma fic_l_reduce:
   assumes  a: "fic M x"
   and      b: "M \<longrightarrow>\<^sub>l M'"
   shows "fic M' x"
-using b a
-apply(induct)
-apply(erule fic.cases)
-apply(simp_all add: trm.inject)
-apply(rotate_tac 3)
-apply(erule fic.cases)
-apply(simp_all add: trm.inject)
-apply(erule fic.cases, simp_all add: trm.inject)+
-done
+  using b a
+  by induction (use fic_rest_elims in force)+
 
 lemma fic_c_reduce:
   assumes a: "fic M x"
   and     b: "M \<longrightarrow>\<^sub>c M'"
   shows "fic M' x"
 using b a
-apply(induct)
-apply(erule fic.cases, simp_all add: trm.inject)+
-done
+  by induction (use fic_rest_elims in force)+
 
 lemma fic_a_reduce:
   assumes a: "fic M x"
   and     b: "M \<longrightarrow>\<^sub>a M'"
-  shows "fic M' x"
-using a b
-apply(induct)
-apply(drule ax_do_not_a_reduce)
-apply(simp)
-apply(drule a_redu_NotR_elim)
-apply(auto)
-apply(rule fic.intros)
-apply(simp add: fresh_a_redu)
-apply(drule a_redu_AndR_elim)
-apply(auto)
-apply(rule fic.intros)
-apply(force simp add: abs_fresh fresh_a_redu)
-apply(force simp add: abs_fresh fresh_a_redu)
-apply(rule fic.intros)
-apply(force simp add: abs_fresh fresh_a_redu)
-apply(force simp add: abs_fresh fresh_a_redu)
-apply(drule a_redu_OrR1_elim)
-apply(auto)
-apply(rule fic.intros)
-apply(force simp add: abs_fresh fresh_a_redu)
-apply(drule a_redu_OrR2_elim)
-apply(auto)
-apply(rule fic.intros)
-apply(force simp add: abs_fresh fresh_a_redu)
-apply(drule a_redu_ImpR_elim)
-apply(auto)
-apply(rule fic.intros)
-apply(force simp add: abs_fresh fresh_a_redu)
-done
+shows "fic M' x"
+  using assms
+proof induction
+  case (1 x a)
+  then show ?case
+    using ax_do_not_a_reduce by fastforce
+next
+  case (2 a M x)
+  then show ?case
+    using a_redu_NotR_elim fresh_a_redu2 by blast
+next
+  case (3 c a M b N)
+  then show ?case
+    by (smt (verit) a_redu_AndR_elim abs_fresh(2) fic.intros(3) fresh_a_redu2)
+next
+  case (4 b a M)
+  then show ?case
+    by (metis a_redu_OrR1_elim abs_fresh(2) fic.intros(4) fresh_a_redu2)
+next
+  case (5 b a M)
+  then show ?case
+    by (metis a_redu_OrR2_elim abs_fresh(2) fic.simps fresh_a_redu2)
+next
+  case (6 b a M x)
+  then show ?case
+    by (metis a_redu_ImpR_elim abs_fresh(2) fic.simps fresh_a_redu2)
+qed
+
 
 lemma fic_a_star_reduce:
   assumes  a: "fic M x"
   and      b: "M \<longrightarrow>\<^sub>a* M'"
   shows "fic M' x"
 using b a
-apply(induct set: rtranclp)
-apply(auto simp: fic_a_reduce)
-done
+  by (induct set: rtranclp) (auto simp: fic_a_reduce)
 
 text \<open>substitution properties\<close>