diff -r b87b14e885af -r 43f5dfb7fa35 src/HOL/BNF_Wellorder_Relation.thy
--- a/src/HOL/BNF_Wellorder_Relation.thy	Fri Jul 15 09:18:21 2022 +0200
+++ b/src/HOL/BNF_Wellorder_Relation.thy	Fri Jul 22 14:39:56 2022 +0200
@@ -220,27 +220,26 @@
 shows "\<exists>b. isMinim B b"
 proof-
   from spec[OF WF[unfolded wf_eq_minimal[of "r - Id"]], of B] NE obtain b where
-  *: "b \<in> B \<and> (\<forall>b'. b' \<noteq> b \<and> (b',b) \<in> r \<longrightarrow> b' \<notin> B)" by auto
-  show ?thesis
-  proof(simp add: isMinim_def, rule exI[of _ b], auto)
-    show "b \<in> B" using * by simp
-  next
-    fix b' assume As: "b' \<in> B"
-    hence **: "b \<in> Field r \<and> b' \<in> Field r" using As SUB * by auto
-    (*  *)
-    from As  * have "b' = b \<or> (b',b) \<notin> r" by auto
-    moreover
-    {assume "b' = b"
-     hence "(b,b') \<in> r"
-     using ** REFL by (auto simp add: refl_on_def)
-    }
-    moreover
-    {assume "b' \<noteq> b \<and> (b',b) \<notin> r"
-     hence "(b,b') \<in> r"
-     using ** TOTAL by (auto simp add: total_on_def)
-    }
-    ultimately show "(b,b') \<in> r" by blast
+    *: "b \<in> B \<and> (\<forall>b'. b' \<noteq> b \<and> (b',b) \<in> r \<longrightarrow> b' \<notin> B)" by auto
+  have "\<forall>b'. b' \<in> B \<longrightarrow> (b, b') \<in> r"
+  proof
+    fix b'
+    show "b' \<in> B \<longrightarrow> (b, b') \<in> r"
+    proof
+      assume As: "b' \<in> B"
+      hence **: "b \<in> Field r \<and> b' \<in> Field r" using As SUB * by auto
+      from As  * have "b' = b \<or> (b',b) \<notin> r" by auto
+      moreover have "b' = b \<Longrightarrow> (b, b') \<in> r"
+        using ** REFL by (auto simp add: refl_on_def)
+      moreover have "b' \<noteq> b \<and> (b',b) \<notin> r \<Longrightarrow> (b,b') \<in> r"
+         using ** TOTAL by (auto simp add: total_on_def)
+      ultimately show "(b,b') \<in> r" by blast
+    qed
   qed
+  then have "isMinim B b"
+    unfolding isMinim_def using * by auto
+  then show ?thesis
+    by auto
 qed
 
 lemma minim_isMinim:
@@ -395,16 +394,22 @@
 
 lemma under_ofilter:
 "ofilter (under a)"
-proof(unfold ofilter_def under_def, auto simp add: Field_def)
-  fix aa x
-  assume "(aa,a) \<in> r" "(x,aa) \<in> r"
-  thus "(x,a) \<in> r"
-  using TRANS trans_def[of r] by blast
+proof -
+  have "\<And>aa x. (aa, a) \<in> r \<Longrightarrow> (x, aa) \<in> r \<Longrightarrow> (x, a) \<in> r"
+  proof -
+    fix aa x
+    assume "(aa,a) \<in> r" "(x,aa) \<in> r"
+    then show "(x,a) \<in> r"
+      using TRANS trans_def[of r] by blast
+  qed
+  then show ?thesis unfolding ofilter_def under_def
+    by (auto simp add: Field_def)
 qed
 
 lemma underS_ofilter:
 "ofilter (underS a)"
-proof(unfold ofilter_def underS_def under_def, auto simp add: Field_def)
+  unfolding ofilter_def underS_def under_def
+proof safe
   fix aa assume "(a, aa) \<in> r" "(aa, a) \<in> r" and DIFF: "aa \<noteq> a"
   thus False
   using ANTISYM antisym_def[of r] by blast
@@ -412,7 +417,13 @@
   fix aa x
   assume "(aa,a) \<in> r" "aa \<noteq> a" "(x,aa) \<in> r"
   thus "(x,a) \<in> r"
-  using TRANS trans_def[of r] by blast
+    using TRANS trans_def[of r] by blast
+next
+  fix x
+  assume "x \<noteq> a" and "(x, a) \<in> r"
+  then show "x \<in> Field r"
+    unfolding Field_def
+    by auto
 qed
 
 lemma Field_ofilter:
@@ -430,7 +441,7 @@
   let ?One = "(\<exists>a\<in>Field r. A = underS a)"
   let ?Two = "(A = Field r)"
   show "?One \<or> ?Two"
-  proof(cases ?Two, simp)
+  proof(cases ?Two)
     let ?B = "(Field r) - A"
     let ?a = "minim ?B"
     assume "A \<noteq> Field r"
@@ -445,7 +456,7 @@
     have "A = underS ?a"
     proof
       show "A \<le> underS ?a"
-      proof(unfold underS_def, auto simp add: 4)
+      proof
         fix x assume **: "x \<in> A"
         hence 11: "x \<in> Field r" using 5 by auto
         have 12: "x \<noteq> ?a" using 4 ** by auto
@@ -458,25 +469,32 @@
          hence "?a \<in> A" using ** 13 by blast
          with 4 have False by simp
         }
-        thus "(x,?a) \<in> r" by blast
+        then have "(x,?a) \<in> r" by blast
+        thus "x \<in> underS ?a"
+          unfolding underS_def by (auto simp add: 12)
       qed
     next
       show "underS ?a \<le> A"
-      proof(unfold underS_def, auto)
+      proof
         fix x
-        assume **: "x \<noteq> ?a" and ***: "(x,?a) \<in> r"
-        hence 11: "x \<in> Field r" using Field_def by fastforce
+        assume **: "x \<in> underS ?a"
+        hence 11: "x \<in> Field r"
+         using Field_def unfolding underS_def by fastforce
          {assume "x \<notin> A"
           hence "x \<in> ?B" using 11 by auto
           hence "(?a,x) \<in> r" using 3 minim_least[of ?B x] by blast
           hence False
-          using ANTISYM antisym_def[of r] ** *** by auto
+          using ANTISYM antisym_def[of r] ** unfolding underS_def by auto
          }
         thus "x \<in> A" by blast
       qed
     qed
     ultimately have ?One using 2 by blast
     thus ?thesis by simp
+  next
+    assume "A = Field r"
+    then show ?thesis
+      by simp
   qed
 qed