# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1730463353 0
# Node ID 137b0b107c4b1d5d4fd443cc0e3140fde763a267
# Parent  d6daa049c1dbf5f64ab97a1f8ef69afd141adec8
Trying to clean up these horribly ugly old proofs, but the requirement of constructivity makes it very difficult

diff -r d6daa049c1db -r 137b0b107c4b src/HOL/Proofs/Lambda/Lambda.thy
--- a/src/HOL/Proofs/Lambda/Lambda.thy	Thu Oct 31 18:43:32 2024 +0100
+++ b/src/HOL/Proofs/Lambda/Lambda.thy	Fri Nov 01 12:15:53 2024 +0000
@@ -59,9 +59,9 @@
 inductive beta :: "[dB, dB] => bool"  (infixl \<open>\<rightarrow>\<^sub>\<beta>\<close> 50)
   where
     beta [simp, intro!]: "Abs s \<degree> t \<rightarrow>\<^sub>\<beta> s[t/0]"
-  | appL [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> s \<degree> u \<rightarrow>\<^sub>\<beta> t \<degree> u"
-  | appR [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> u \<degree> s \<rightarrow>\<^sub>\<beta> u \<degree> t"
-  | abs [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> Abs s \<rightarrow>\<^sub>\<beta> Abs t"
+  | appL [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t \<Longrightarrow> s \<degree> u \<rightarrow>\<^sub>\<beta> t \<degree> u"
+  | appR [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t \<Longrightarrow> u \<degree> s \<rightarrow>\<^sub>\<beta> u \<degree> t"
+  | abs [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t \<Longrightarrow> Abs s \<rightarrow>\<^sub>\<beta> Abs t"
 
 abbreviation
   beta_reds :: "[dB, dB] => bool"  (infixl \<open>\<rightarrow>\<^sub>\<beta>\<^sup>*\<close> 50) where
@@ -79,19 +79,19 @@
 subsection \<open>Congruence rules\<close>
 
 lemma rtrancl_beta_Abs [intro!]:
-    "s \<rightarrow>\<^sub>\<beta>\<^sup>* s' ==> Abs s \<rightarrow>\<^sub>\<beta>\<^sup>* Abs s'"
+    "s \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<Longrightarrow> Abs s \<rightarrow>\<^sub>\<beta>\<^sup>* Abs s'"
   by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
 
 lemma rtrancl_beta_AppL:
-    "s \<rightarrow>\<^sub>\<beta>\<^sup>* s' ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t"
+    "s \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<Longrightarrow> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t"
   by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
 
 lemma rtrancl_beta_AppR:
-    "t \<rightarrow>\<^sub>\<beta>\<^sup>* t' ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s \<degree> t'"
+    "t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<Longrightarrow> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s \<degree> t'"
   by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
 
 lemma rtrancl_beta_App [intro]:
-    "[| s \<rightarrow>\<^sub>\<beta>\<^sup>* s'; t \<rightarrow>\<^sub>\<beta>\<^sup>* t' |] ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t'"
+    "\<lbrakk>s \<rightarrow>\<^sub>\<beta>\<^sup>* s'; t \<rightarrow>\<^sub>\<beta>\<^sup>* t'\<rbrakk> \<Longrightarrow> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t'"
   by (blast intro!: rtrancl_beta_AppL rtrancl_beta_AppR intro: rtranclp_trans)
 
 
@@ -100,10 +100,10 @@
 lemma subst_eq [simp]: "(Var k)[u/k] = u"
   by (simp add: subst_Var)
 
-lemma subst_gt [simp]: "i < j ==> (Var j)[u/i] = Var (j - 1)"
+lemma subst_gt [simp]: "i < j \<Longrightarrow> (Var j)[u/i] = Var (j - 1)"
   by (simp add: subst_Var)
 
-lemma subst_lt [simp]: "j < i ==> (Var j)[u/i] = Var j"
+lemma subst_lt [simp]: "j < i \<Longrightarrow> (Var j)[u/i] = Var j"
   by (simp add: subst_Var)
 
 lemma lift_lift:
@@ -151,39 +151,58 @@
   Normalization. \medskip\<close>
 
 theorem subst_preserves_beta [simp]:
-    "r \<rightarrow>\<^sub>\<beta> s ==> r[t/i] \<rightarrow>\<^sub>\<beta> s[t/i]"
+    "r \<rightarrow>\<^sub>\<beta> s \<Longrightarrow> r[t/i] \<rightarrow>\<^sub>\<beta> s[t/i]"
   by (induct arbitrary: t i set: beta) (simp_all add: subst_subst [symmetric])
 
-theorem subst_preserves_beta': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> r[t/i] \<rightarrow>\<^sub>\<beta>\<^sup>* s[t/i]"
-  apply (induct set: rtranclp)
-   apply (rule rtranclp.rtrancl_refl)
-  apply (erule rtranclp.rtrancl_into_rtrancl)
-  apply (erule subst_preserves_beta)
-  done
+theorem subst_preserves_beta': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s \<Longrightarrow> r[t/i] \<rightarrow>\<^sub>\<beta>\<^sup>* s[t/i]"
+proof (induct set: rtranclp)
+  case base
+  then show ?case
+    by (iprover intro: rtrancl_refl)
+next
+  case (step y z)
+  then show ?case
+    by (iprover intro: rtranclp.simps subst_preserves_beta)
+qed
 
 theorem lift_preserves_beta [simp]:
-    "r \<rightarrow>\<^sub>\<beta> s ==> lift r i \<rightarrow>\<^sub>\<beta> lift s i"
+    "r \<rightarrow>\<^sub>\<beta> s \<Longrightarrow> lift r i \<rightarrow>\<^sub>\<beta> lift s i"
   by (induct arbitrary: i set: beta) auto
 
-theorem lift_preserves_beta': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> lift r i \<rightarrow>\<^sub>\<beta>\<^sup>* lift s i"
-  apply (induct set: rtranclp)
-   apply (rule rtranclp.rtrancl_refl)
-  apply (erule rtranclp.rtrancl_into_rtrancl)
-  apply (erule lift_preserves_beta)
-  done
+theorem lift_preserves_beta': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s \<Longrightarrow> lift r i \<rightarrow>\<^sub>\<beta>\<^sup>* lift s i"
+proof (induct set: rtranclp)
+  case base
+  then show ?case
+    by (iprover intro: rtrancl_refl)
+next
+  case (step y z)
+  then show ?case
+    by (iprover intro: lift_preserves_beta rtranclp.simps)
+qed
 
-theorem subst_preserves_beta2 [simp]: "r \<rightarrow>\<^sub>\<beta> s ==> t[r/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t[s/i]"
-  apply (induct t arbitrary: r s i)
-    apply (simp add: subst_Var r_into_rtranclp)
-   apply (simp add: rtrancl_beta_App)
-  apply (simp add: rtrancl_beta_Abs)
-  done
+theorem subst_preserves_beta2 [simp]: "r \<rightarrow>\<^sub>\<beta> s \<Longrightarrow> t[r/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t[s/i]"
+proof (induct t arbitrary: r s i)
+  case (Var x)
+  then show ?case
+    by (simp add: subst_Var r_into_rtranclp)
+next
+  case (App t1 t2)
+  then show ?case 
+    by (simp add: rtrancl_beta_App)
+next
+  case (Abs t)
+  then show ?case by (simp add: rtrancl_beta_Abs)
+qed
 
-theorem subst_preserves_beta2': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> t[r/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t[s/i]"
-  apply (induct set: rtranclp)
-   apply (rule rtranclp.rtrancl_refl)
-  apply (erule rtranclp_trans)
-  apply (erule subst_preserves_beta2)
-  done
+
+theorem subst_preserves_beta2': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s \<Longrightarrow> t[r/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t[s/i]"
+proof (induct set: rtranclp)
+  case base
+  then show ?case by (iprover intro: rtrancl_refl)
+next
+  case (step y z)
+  then show ?case
+    by (iprover intro: rtranclp_trans subst_preserves_beta2)
+qed
 
 end
diff -r d6daa049c1db -r 137b0b107c4b src/HOL/Proofs/Lambda/LambdaType.thy
--- a/src/HOL/Proofs/Lambda/LambdaType.thy	Thu Oct 31 18:43:32 2024 +0100
+++ b/src/HOL/Proofs/Lambda/LambdaType.thy	Fri Nov 01 12:15:53 2024 +0000
@@ -76,49 +76,49 @@
 
 lemma lists_typings:
     "e \<tturnstile> ts : Ts \<Longrightarrow> listsp (\<lambda>t. \<exists>T. e \<turnstile> t : T) ts"
-  apply (induct ts arbitrary: Ts)
-   apply (case_tac Ts)
-     apply simp
-     apply (rule listsp.Nil)
-    apply simp
-  apply (case_tac Ts)
-   apply simp
-  apply simp
-  apply (rule listsp.Cons)
-   apply blast
-  apply blast
-  done
+proof (induct ts arbitrary: Ts)
+  case Nil
+  then show ?case
+    by simp
+next
+  case c: (Cons a ts)
+  show ?case
+  proof (cases Ts)
+    case Nil
+    with c show ?thesis
+      by simp
+  next
+    case (Cons T list)
+    with c show ?thesis  by force
+  qed
+qed
 
 lemma types_snoc: "e \<tturnstile> ts : Ts \<Longrightarrow> e \<turnstile> t : T \<Longrightarrow> e \<tturnstile> ts @ [t] : Ts @ [T]"
-  apply (induct ts arbitrary: Ts)
-  apply simp
-  apply (case_tac Ts)
-  apply simp+
-  done
+  by (induct ts arbitrary: Ts) (auto split: list.split_asm)
 
 lemma types_snoc_eq: "e \<tturnstile> ts @ [t] : Ts @ [T] =
   (e \<tturnstile> ts : Ts \<and> e \<turnstile> t : T)"
-  apply (induct ts arbitrary: Ts)
-  apply (case_tac Ts)
-  apply simp+
-  apply (case_tac Ts)
-  apply (case_tac "ts @ [t]")
-  apply simp+
-  done
+proof (induct ts arbitrary: Ts)
+  case Nil
+  then show ?case
+    by (auto split: list.split)
+next
+  case (Cons a ts)
+  have "\<not> e \<tturnstile> ts @ [t] : []"
+  by (cases "ts @ [t]"; simp) 
+  with Cons show ?case 
+    by (auto split: list.split)
+qed
 
+text \<open>Cannot use \<open>rev_exhaust\<close> from the \<open>List\<close> theory, since it is not constructive\<close>
 lemma rev_exhaust2 [extraction_expand]:
   obtains (Nil) "xs = []"  |  (snoc) ys y where "xs = ys @ [y]"
-  \<comment> \<open>Cannot use \<open>rev_exhaust\<close> from the \<open>List\<close>
-    theory, since it is not constructive\<close>
-  apply (subgoal_tac "\<forall>ys. xs = rev ys \<longrightarrow> thesis")
-  apply (erule_tac x="rev xs" in allE)
-  apply simp
-  apply (rule allI)
-  apply (rule impI)
-  apply (case_tac ys)
-  apply simp
-  apply simp
-  done
+proof -
+  have \<section>: "xs = rev ys \<Longrightarrow> thesis" for ys
+    by (cases ys) (simp_all add: local.Nil snoc)
+  show thesis
+    using \<section> [of "rev xs"] by simp
+qed
 
 lemma types_snocE:
   assumes \<open>e \<tturnstile> ts @ [t] : Ts\<close>
@@ -139,44 +139,22 @@
 
 lemma list_app_typeD:
     "e \<turnstile> t \<degree>\<degree> ts : T \<Longrightarrow> \<exists>Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<and> e \<tturnstile> ts : Ts"
-  apply (induct ts arbitrary: t T)
-   apply simp
-  apply (rename_tac a b t T)
-  apply atomize
-  apply simp
-  apply (erule_tac x = "t \<degree> a" in allE)
-  apply (erule_tac x = T in allE)
-  apply (erule impE)
-   apply assumption
-  apply (elim exE conjE)
-  apply (ind_cases "e \<turnstile> t \<degree> u : T" for t u T)
-  apply (rule_tac x = "Ta # Ts" in exI)
-  apply simp
-  done
+proof (induct ts arbitrary: t T)
+  case Nil
+  then show ?case by auto
+next
+  case (Cons a b t T)
+  then show ?case
+    by (auto simp: split: list.split)
+qed
 
 lemma list_app_typeE:
   "e \<turnstile> t \<degree>\<degree> ts : T \<Longrightarrow> (\<And>Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> C) \<Longrightarrow> C"
-  by (insert list_app_typeD) fast
+  using list_app_typeD by iprover
 
 lemma list_app_typeI:
     "e \<turnstile> t : Ts \<Rrightarrow> T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> e \<turnstile> t \<degree>\<degree> ts : T"
-  apply (induct ts arbitrary: t T Ts)
-   apply simp
-  apply (rename_tac a b t T Ts)
-  apply atomize
-  apply (case_tac Ts)
-   apply simp
-  apply simp
-  apply (erule_tac x = "t \<degree> a" in allE)
-  apply (erule_tac x = T in allE)
-  apply (rename_tac list)
-  apply (erule_tac x = list in allE)
-  apply (erule impE)
-   apply (erule conjE)
-   apply (erule typing.App)
-   apply assumption
-  apply blast
-  done
+  by (induct ts arbitrary: t  Ts) (auto simp add: split: list.split_asm)
 
 text \<open>
 For the specific case where the head of the term is a variable,
@@ -187,92 +165,78 @@
 
 theorem var_app_type_eq:
   "e \<turnstile> Var i \<degree>\<degree> ts : T \<Longrightarrow> e \<turnstile> Var i \<degree>\<degree> ts : U \<Longrightarrow> T = U"
-  apply (induct ts arbitrary: T U rule: rev_induct)
-  apply simp
-  apply (ind_cases "e \<turnstile> Var i : T" for T)
-  apply (ind_cases "e \<turnstile> Var i : T" for T)
-  apply simp
-  apply simp
-  apply (ind_cases "e \<turnstile> t \<degree> u : T" for t u T)
-  apply (ind_cases "e \<turnstile> t \<degree> u : T" for t u T)
-  apply atomize
-  apply (erule_tac x="Ta \<Rightarrow> T" in allE)
-  apply (erule_tac x="Tb \<Rightarrow> U" in allE)
-  apply (erule impE)
-  apply assumption
-  apply (erule impE)
-  apply assumption
-  apply simp
-  done
+  by (induct ts arbitrary: T U rule: rev_induct) auto
 
 lemma var_app_types: "e \<turnstile> Var i \<degree>\<degree> ts \<degree>\<degree> us : T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow>
   e \<turnstile> Var i \<degree>\<degree> ts : U \<Longrightarrow> \<exists>Us. U = Us \<Rrightarrow> T \<and> e \<tturnstile> us : Us"
-  apply (induct us arbitrary: ts Ts U)
-  apply simp
-  apply (erule var_app_type_eq)
-  apply assumption
-  apply simp
-  apply (rename_tac a b ts Ts U)
-  apply atomize
-  apply (case_tac U)
-  apply (rule FalseE)
-  apply simp
-  apply (erule list_app_typeE)
-  apply (ind_cases "e \<turnstile> t \<degree> u : T" for t u T)
-  apply (rename_tac nat Tsa Ta)
-  apply (drule_tac T="Atom nat" and U="Ta \<Rightarrow> Tsa \<Rrightarrow> T" in var_app_type_eq)
-  apply assumption
-  apply simp
-  apply (rename_tac nat type1 type2)
-  apply (erule_tac x="ts @ [a]" in allE)
-  apply (erule_tac x="Ts @ [type1]" in allE)
-  apply (erule_tac x="type2" in allE)
-  apply simp
-  apply (erule impE)
-  apply (rule types_snoc)
-  apply assumption
-  apply (erule list_app_typeE)
-  apply (ind_cases "e \<turnstile> t \<degree> u : T" for t u T)
-  apply (drule_tac T="type1 \<Rightarrow> type2" and U="Ta \<Rightarrow> Tsa \<Rrightarrow> T" in var_app_type_eq)
-  apply assumption
-  apply simp
-  apply (erule impE)
-  apply (rule typing.App)
-  apply assumption
-  apply (erule list_app_typeE)
-  apply (ind_cases "e \<turnstile> t \<degree> u : T" for t u T)
-  apply (frule_tac T="type1 \<Rightarrow> type2" and U="Ta \<Rightarrow> Tsa \<Rrightarrow> T" in var_app_type_eq)
-  apply assumption
-  apply simp
-  apply (erule exE)
-  apply (rule_tac x="type1 # Us" in exI)
-  apply simp
-  apply (erule list_app_typeE)
-  apply (ind_cases "e \<turnstile> t \<degree> u : T" for t u T)
-  apply (frule_tac T="type1 \<Rightarrow> Us \<Rrightarrow> T" and U="Ta \<Rightarrow> Tsa \<Rrightarrow> T" in var_app_type_eq)
-  apply assumption
-  apply simp
-  done
+proof (induct us arbitrary: ts Ts U)
+  case Nil
+  then show ?case
+    by (simp add: var_app_type_eq)
+next
+  case (Cons a b ts Ts U)
+  then show ?case
+    apply atomize
+    apply (case_tac U)
+     apply (rule FalseE)
+     apply simp
+     apply (erule list_app_typeE)
+     apply (ind_cases "e \<turnstile> t \<degree> u : T" for t u T)
+     apply (rename_tac nat Ts' T')
+     apply (drule_tac T="Atom nat" and U="T' \<Rightarrow> Ts' \<Rrightarrow> T" in var_app_type_eq)
+      apply assumption
+     apply simp
+    apply (rename_tac type1 type2)
+    apply (erule_tac x="ts @ [a]" in allE)
+    apply (erule_tac x="Ts @ [type1]" in allE)
+    apply (erule_tac x="type2" in allE)
+    apply simp
+    apply (erule impE)
+     apply (rule types_snoc)
+      apply assumption
+     apply (erule list_app_typeE)
+     apply (ind_cases "e \<turnstile> t \<degree> u : T" for t u T)
+    using var_app_type_eq apply fastforce
+    apply (erule impE)
+     apply (rule typing.App)
+      apply assumption
+     apply (erule list_app_typeE)
+     apply (ind_cases "e \<turnstile> t \<degree> u : T" for t u T)
+    using var_app_type_eq apply fastforce
+    apply (erule exE)
+    apply (rule_tac x="type1 # Us" in exI)
+    apply simp
+    apply (erule list_app_typeE)
+    apply (ind_cases "e \<turnstile> t \<degree> u : T" for t u T)
+    using var_app_type_eq by fastforce
+qed
 
 lemma var_app_typesE: "e \<turnstile> Var i \<degree>\<degree> ts : T \<Longrightarrow>
   (\<And>Ts. e \<turnstile> Var i : Ts \<Rrightarrow> T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> P) \<Longrightarrow> P"
-  apply (drule var_app_types [of _ _ "[]", simplified])
-  apply (iprover intro: typing.Var)+
-  done
+  by (iprover intro: typing.Var dest: var_app_types [of _ _ "[]", simplified])
 
-lemma abs_typeE: "e \<turnstile> Abs t : T \<Longrightarrow> (\<And>U V. e\<langle>0:U\<rangle> \<turnstile> t : V \<Longrightarrow> P) \<Longrightarrow> P"
-  apply (cases T)
-  apply (rule FalseE)
-  apply (erule typing.cases)
-  apply simp_all
-  apply atomize
-  apply (rename_tac type1 type2)
-  apply (erule_tac x="type1" in allE)
-  apply (erule_tac x="type2" in allE)
-  apply (erule mp)
-  apply (erule typing.cases)
-  apply simp_all
-  done
+lemma abs_typeE:
+  assumes "e \<turnstile> Abs t : T" "\<And>U V. e\<langle>0:U\<rangle> \<turnstile> t : V \<Longrightarrow> P"
+  shows "P"
+proof (cases T)
+  case (Atom x1)
+  with assms(1) show ?thesis
+    apply-
+    apply (rule FalseE)
+    apply (erule typing.cases)
+      apply simp_all
+    done
+next
+  case (Fun type1 type2)
+  with assms show ?thesis
+    apply atomize
+    apply (erule_tac x="type1" in allE)
+    apply (erule_tac x="type2" in allE)
+    apply (erule mp)
+    apply (erule typing.cases)
+      apply simp_all
+    done
+qed
 
 
 subsection \<open>Lifting preserves well-typedness\<close>
@@ -282,57 +246,44 @@
 
 lemma lift_types:
   "e \<tturnstile> ts : Ts \<Longrightarrow> e\<langle>i:U\<rangle> \<tturnstile> (map (\<lambda>t. lift t i) ts) : Ts"
-  apply (induct ts arbitrary: Ts)
-   apply simp
-  apply (case_tac Ts)
-   apply auto
-  done
+  by (induct ts arbitrary: Ts) (auto split: list.split)
 
 
 subsection \<open>Substitution lemmas\<close>
 
 lemma subst_lemma:
     "e \<turnstile> t : T \<Longrightarrow> e' \<turnstile> u : U \<Longrightarrow> e = e'\<langle>i:U\<rangle> \<Longrightarrow> e' \<turnstile> t[u/i] : T"
-  apply (induct arbitrary: e' i U u set: typing)
-    apply (rule_tac x = x and y = i in linorder_cases)
-      apply auto
-  apply blast
-  done
+proof (induct arbitrary: e' i U u set: typing)
+  case (Var env x T)
+  then show ?case
+    by (force simp add: shift_def)
+next
+  case (Abs env T t U)
+  then show ?case by force
+qed auto
 
 lemma substs_lemma:
   "e \<turnstile> u : T \<Longrightarrow> e\<langle>i:T\<rangle> \<tturnstile> ts : Ts \<Longrightarrow>
      e \<tturnstile> (map (\<lambda>t. t[u/i]) ts) : Ts"
-  apply (induct ts arbitrary: Ts)
-   apply (case_tac Ts)
-    apply simp
-   apply simp
-  apply atomize
-  apply (case_tac Ts)
-   apply simp
-  apply simp
-  apply (erule conjE)
-  apply (erule (1) subst_lemma)
-  apply (rule refl)
-  done
+proof (induct ts arbitrary: Ts)
+  case Nil
+  then show ?case
+    by auto
+next
+  case (Cons a ts)
+  with subst_lemma show ?case
+    by (auto split: list.split)
+qed
 
 
 subsection \<open>Subject reduction\<close>
 
 lemma subject_reduction: "e \<turnstile> t : T \<Longrightarrow> t \<rightarrow>\<^sub>\<beta> t' \<Longrightarrow> e \<turnstile> t' : T"
-  apply (induct arbitrary: t' set: typing)
-    apply blast
-   apply blast
-  apply atomize
-  apply (ind_cases "s \<degree> t \<rightarrow>\<^sub>\<beta> t'" for s t t')
-    apply hypsubst
-    apply (ind_cases "env \<turnstile> Abs t : T \<Rightarrow> U" for env t T U)
-    apply (rule subst_lemma)
-      apply assumption
-     apply assumption
-    apply (rule ext)
-    apply (case_tac x)
-     apply auto
-  done
+proof (induct arbitrary: t' set: typing)
+  case (App env s T U t)
+  with subst_lemma show ?case
+    by auto
+qed auto
 
 theorem subject_reduction': "t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<Longrightarrow> e \<turnstile> t : T \<Longrightarrow> e \<turnstile> t' : T"
   by (induct set: rtranclp) (iprover intro: subject_reduction)+
diff -r d6daa049c1db -r 137b0b107c4b src/HOL/Proofs/Lambda/NormalForm.thy
--- a/src/HOL/Proofs/Lambda/NormalForm.thy	Thu Oct 31 18:43:32 2024 +0100
+++ b/src/HOL/Proofs/Lambda/NormalForm.thy	Fri Nov 01 12:15:53 2024 +0000
@@ -52,15 +52,10 @@
   by (induct xs) simp_all
 
 lemma listall_app: "listall P (xs @ ys) = (listall P xs \<and> listall P ys)"
-  apply (induct xs)
-   apply (rule iffI, simp, simp)
-  apply (rule iffI, simp, simp)
-  done
+  by (induct xs; intro iffI; simp)
 
 lemma listall_snoc [simp]: "listall P (xs @ [x]) = (listall P xs \<and> P x)"
-  apply (rule iffI)
-  apply (simp add: listall_app)+
-  done
+  by (rule iffI; simp add: listall_app)
 
 lemma listall_cong [cong, extraction_expand]:
   "xs = ys \<Longrightarrow> listall P xs = listall P ys"
@@ -82,18 +77,26 @@
 monos listall_def
 
 lemma nat_eq_dec: "\<And>n::nat. m = n \<or> m \<noteq> n"
-  apply (induct m)
-  apply (case_tac n)
-  apply (case_tac [3] n)
-  apply (simp only: nat.simps, iprover?)+
-  done
+proof (induction m)
+  case 0
+  then show ?case
+    by (cases n; simp only: nat.simps; iprover)
+next
+  case (Suc m)
+  then show ?case
+    by (cases n; simp only: nat.simps; iprover)
+qed
 
 lemma nat_le_dec: "\<And>n::nat. m < n \<or> \<not> (m < n)"
-  apply (induct m)
-  apply (case_tac n)
-    apply (case_tac [3] n)
-  apply (simp del: simp_thms subst_all, iprover?)+
-  done
+proof (induction m)
+  case 0
+  then show ?case
+    by (cases n; simp only: order.irrefl zero_less_Suc; iprover)
+next
+  case (Suc m)
+  then show ?case
+    by (cases n; simp only: not_less_zero Suc_less_eq; iprover)
+qed
 
 lemma App_NF_D: assumes NF: "NF (Var n \<degree>\<degree> ts)"
   shows "listall NF ts" using NF
@@ -103,11 +106,11 @@
 subsection \<open>Properties of \<open>NF\<close>\<close>
 
 lemma Var_NF: "NF (Var n)"
-  apply (subgoal_tac "NF (Var n \<degree>\<degree> [])")
-   apply simp
-  apply (rule NF.App)
-  apply simp
-  done
+proof -
+  have "NF (Var n \<degree>\<degree> [])"
+    by (rule NF.App) simp
+  then show ?thesis by simp
+qed
 
 lemma Abs_NF:
   assumes NF: "NF (Abs t \<degree>\<degree> ts)"
@@ -127,39 +130,29 @@
 
 lemma subst_Var_NF: "NF t \<Longrightarrow> NF (t[Var i/j])"
   apply (induct arbitrary: i j set: NF)
-  apply simp
-  apply (frule listall_conj1)
-  apply (drule listall_conj2)
-  apply (drule_tac i=i and j=j in subst_terms_NF)
-  apply assumption
-  apply (rule_tac m1=x and n1=j in nat_eq_dec [THEN disjE])
-  apply simp
-  apply (erule NF.App)
-  apply (rule_tac m1=j and n1=x in nat_le_dec [THEN disjE])
-  apply simp
-  apply (iprover intro: NF.App)
-  apply simp
-  apply (iprover intro: NF.App)
-  apply simp
-  apply (iprover intro: NF.Abs)
+   apply simp
+   apply (frule listall_conj1)
+   apply (drule listall_conj2)
+   apply (drule_tac i=i and j=j in subst_terms_NF)
+    apply assumption
+   apply (rule_tac m1=x and n1=j in nat_eq_dec [THEN disjE])
+    apply simp
+    apply (erule NF.App)
+   apply (rule_tac m1=j and n1=x in nat_le_dec [THEN disjE])
+    apply (simp_all add: NF.App NF.Abs)
   done
 
 lemma app_Var_NF: "NF t \<Longrightarrow> \<exists>t'. t \<degree> Var i \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'"
   apply (induct set: NF)
-  apply (simplesubst app_last)  \<comment> \<open>Using \<open>subst\<close> makes extraction fail\<close>
-  apply (rule exI)
-  apply (rule conjI)
-  apply (rule rtranclp.rtrancl_refl)
-  apply (rule NF.App)
-  apply (drule listall_conj1)
-  apply (simp add: listall_app)
-  apply (rule Var_NF)
-  apply (rule exI)
-  apply (rule conjI)
-  apply (rule rtranclp.rtrancl_into_rtrancl)
-  apply (rule rtranclp.rtrancl_refl)
-  apply (rule beta)
-  apply (erule subst_Var_NF)
+   apply (simplesubst app_last)  \<comment> \<open>Using \<open>subst\<close> makes extraction fail\<close>
+   apply (rule exI)
+   apply (rule conjI)
+    apply (rule rtranclp.rtrancl_refl)
+   apply (rule NF.App)
+   apply (drule listall_conj1)
+   apply (simp add: listall_app)
+   apply (rule Var_NF)
+  apply (iprover intro: rtranclp.rtrancl_into_rtrancl rtranclp.rtrancl_refl beta subst_Var_NF)
   done
 
 lemma lift_terms_NF: "listall NF ts \<Longrightarrow>
@@ -169,20 +162,12 @@
 
 lemma lift_NF: "NF t \<Longrightarrow> NF (lift t i)"
   apply (induct arbitrary: i set: NF)
-  apply (frule listall_conj1)
-  apply (drule listall_conj2)
-  apply (drule_tac i=i in lift_terms_NF)
-  apply assumption
-  apply (rule_tac m1=x and n1=i in nat_le_dec [THEN disjE])
-  apply simp
-  apply (rule NF.App)
-  apply assumption
-  apply simp
-  apply (rule NF.App)
-  apply assumption
-  apply simp
-  apply (rule NF.Abs)
-  apply simp
+   apply (frule listall_conj1)
+   apply (drule listall_conj2)
+   apply (drule_tac i=i in lift_terms_NF)
+    apply assumption
+   apply (rule_tac m1=x and n1=i in nat_le_dec [THEN disjE])
+    apply (simp_all add: NF.App NF.Abs)
   done
 
 text \<open>
diff -r d6daa049c1db -r 137b0b107c4b src/HOL/Proofs/Lambda/ParRed.thy
--- a/src/HOL/Proofs/Lambda/ParRed.thy	Thu Oct 31 18:43:32 2024 +0100
+++ b/src/HOL/Proofs/Lambda/ParRed.thy	Fri Nov 01 12:15:53 2024 +0000
@@ -103,13 +103,11 @@
 subsection \<open>Confluence (via complete developments)\<close>
 
 lemma diamond_par_beta2: "diamond par_beta"
-  apply (unfold diamond_def commute_def square_def)
-  apply (blast intro: par_beta_cd)
-  done
+  unfolding diamond_def commute_def square_def
+  by (blast intro: par_beta_cd)
 
 theorem beta_confluent: "confluent beta"
-  apply (rule diamond_par_beta2 diamond_to_confluence
+  by (rule diamond_par_beta2 diamond_to_confluence
     par_beta_subset_beta beta_subset_par_beta)+
-  done
 
 end
diff -r d6daa049c1db -r 137b0b107c4b src/HOL/Proofs/Lambda/WeakNorm.thy
--- a/src/HOL/Proofs/Lambda/WeakNorm.thy	Thu Oct 31 18:43:32 2024 +0100
+++ b/src/HOL/Proofs/Lambda/WeakNorm.thy	Fri Nov 01 12:15:53 2024 +0000
@@ -266,16 +266,18 @@
 extract type_NF
 
 lemma rtranclR_rtrancl_eq: "rtranclpR r a b = r\<^sup>*\<^sup>* a b"
-  apply (rule iffI)
-  apply (erule rtranclpR.induct)
-  apply (rule rtranclp.rtrancl_refl)
-  apply (erule rtranclp.rtrancl_into_rtrancl)
-  apply assumption
-  apply (erule rtranclp.induct)
-  apply (rule rtranclpR.rtrancl_refl)
-  apply (erule rtranclpR.rtrancl_into_rtrancl)
-  apply assumption
-  done
+proof
+  show "rtranclpR r a b \<Longrightarrow> r\<^sup>*\<^sup>* a b"
+    apply (erule rtranclpR.induct)
+     apply (rule rtranclp.rtrancl_refl)
+    apply (metis rtranclp.rtrancl_into_rtrancl)
+    done
+  show "r\<^sup>*\<^sup>* a b \<Longrightarrow> rtranclpR r a b"
+    apply (erule rtranclp.induct)
+     apply (rule rtranclpR.rtrancl_refl)
+    apply (metis rtranclpR.rtrancl_into_rtrancl)
+    done
+qed
 
 lemma NFR_imp_NF: "NFR nf t \<Longrightarrow> NF t"
   apply (erule NFR.induct)