# HG changeset patch
# User wenzelm
# Date 1731789394 -3600
# Node ID 2575f1bd226be0e976633686b2e6a087292336de
# Parent  d8f77c1c97034e1a8d73ebdeb035cc3ecb14ef54
tuned proofs;

diff -r d8f77c1c9703 -r 2575f1bd226b src/HOL/Hahn_Banach/Function_Norm.thy
--- a/src/HOL/Hahn_Banach/Function_Norm.thy	Sat Nov 16 20:22:26 2024 +0100
+++ b/src/HOL/Hahn_Banach/Function_Norm.thy	Sat Nov 16 21:36:34 2024 +0100
@@ -113,13 +113,13 @@
       proof
         fix y assume y: "y \<in> B V f"
         show "y \<le> b"
-        proof cases
-          assume "y = 0"
+        proof (cases "y = 0")
+          case True
           then show ?thesis unfolding b_def by arith
         next
           txt \<open>The second case is \<open>y = \<bar>f x\<bar> / \<parallel>x\<parallel>\<close> for some
             \<open>x \<in> V\<close> with \<open>x \<noteq> 0\<close>.\<close>
-          assume "y \<noteq> 0"
+          case False
           with y obtain x where y_rep: "y = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>"
               and x: "x \<in> V" and neq: "x \<noteq> 0"
             by (auto simp add: B_def divide_inverse)
@@ -132,7 +132,7 @@
           also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>"
           proof (rule mult_right_mono)
             from c x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..
-            from gt have "0 < inverse \<parallel>x\<parallel>" 
+            from gt have "0 < inverse \<parallel>x\<parallel>"
               by (rule positive_imp_inverse_positive)
             then show "0 \<le> inverse \<parallel>x\<parallel>" by (rule order_less_imp_le)
           qed
@@ -140,7 +140,7 @@
             by (rule Groups.mult.assoc)
           also
           from gt have "\<parallel>x\<parallel> \<noteq> 0" by simp
-          then have "\<parallel>x\<parallel> * inverse \<parallel>x\<parallel> = 1" by simp 
+          then have "\<parallel>x\<parallel> * inverse \<parallel>x\<parallel> = 1" by simp
           also have "c * 1 \<le> b" by (simp add: b_def)
           finally show "y \<le> b" .
         qed
@@ -205,8 +205,8 @@
   interpret continuous V f norm by fact
   interpret linearform V f by fact
   show ?thesis
-  proof cases
-    assume "x = 0"
+  proof (cases "x = 0")
+    case True
     then have "\<bar>f x\<bar> = \<bar>f 0\<bar>" by simp
     also have "f 0 = 0" by rule unfold_locales
     also have "\<bar>\<dots>\<bar> = 0" by simp
@@ -216,7 +216,7 @@
     with a have "0 \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" by (simp add: zero_le_mult_iff)
     finally show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" .
   next
-    assume "x \<noteq> 0"
+    case False
     with x have neq: "\<parallel>x\<parallel> \<noteq> 0" by simp
     then have "\<bar>f x\<bar> = (\<bar>f x\<bar> * inverse \<parallel>x\<parallel>) * \<parallel>x\<parallel>" by simp
     also have "\<dots> \<le>  \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
@@ -250,11 +250,11 @@
   proof (rule fn_norm_leastB [folded B_def fn_norm_def])
     fix b assume b: "b \<in> B V f"
     show "b \<le> c"
-    proof cases
-      assume "b = 0"
+    proof (cases "b = 0")
+      case True
       with ge show ?thesis by simp
     next
-      assume "b \<noteq> 0"
+      case False
       with b obtain x where b_rep: "b = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>"
         and x_neq: "x \<noteq> 0" and x: "x \<in> V"
         by (auto simp add: B_def divide_inverse)
@@ -272,7 +272,7 @@
       qed
       finally show ?thesis .
     qed
-  qed (insert \<open>continuous V f norm\<close>, simp_all add: continuous_def)
+  qed (use \<open>continuous V f norm\<close> in \<open>simp_all add: continuous_def\<close>)
 qed
 
 end
diff -r d8f77c1c9703 -r 2575f1bd226b src/HOL/Hahn_Banach/Hahn_Banach.thy
--- a/src/HOL/Hahn_Banach/Hahn_Banach.thy	Sat Nov 16 20:22:26 2024 +0100
+++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy	Sat Nov 16 21:36:34 2024 +0100
@@ -59,39 +59,36 @@
   then have M: "M = \<dots>" by (simp only:)
   from E have F: "vectorspace F" ..
   note FE = \<open>F \<unlhd> E\<close>
-  {
-    fix c assume cM: "c \<in> chains M" and ex: "\<exists>x. x \<in> c"
-    have "\<Union>c \<in> M"
-      \<comment> \<open>Show that every non-empty chain \<open>c\<close> of \<open>M\<close> has an upper bound in \<open>M\<close>:\<close>
-      \<comment> \<open>\<open>\<Union>c\<close> is greater than any element of the chain \<open>c\<close>, so it suffices to show \<open>\<Union>c \<in> M\<close>.\<close>
-      unfolding M_def
-    proof (rule norm_pres_extensionI)
-      let ?H = "domain (\<Union>c)"
-      let ?h = "funct (\<Union>c)"
+  have "\<Union>c \<in> M" if cM: "c \<in> chains M" and ex: "\<exists>x. x \<in> c" for c
+    \<comment> \<open>Show that every non-empty chain \<open>c\<close> of \<open>M\<close> has an upper bound in \<open>M\<close>:\<close>
+    \<comment> \<open>\<open>\<Union>c\<close> is greater than any element of the chain \<open>c\<close>, so it suffices to show \<open>\<Union>c \<in> M\<close>.\<close>
+    unfolding M_def
+  proof (rule norm_pres_extensionI)
+    let ?H = "domain (\<Union>c)"
+    let ?h = "funct (\<Union>c)"
 
-      have a: "graph ?H ?h = \<Union>c"
-      proof (rule graph_domain_funct)
-        fix x y z assume "(x, y) \<in> \<Union>c" and "(x, z) \<in> \<Union>c"
-        with M_def cM show "z = y" by (rule sup_definite)
-      qed
-      moreover from M cM a have "linearform ?H ?h"
-        by (rule sup_lf)
-      moreover from a M cM ex FE E have "?H \<unlhd> E"
-        by (rule sup_subE)
-      moreover from a M cM ex FE have "F \<unlhd> ?H"
-        by (rule sup_supF)
-      moreover from a M cM ex have "graph F f \<subseteq> graph ?H ?h"
-        by (rule sup_ext)
-      moreover from a M cM have "\<forall>x \<in> ?H. ?h x \<le> p x"
-        by (rule sup_norm_pres)
-      ultimately show "\<exists>H h. \<Union>c = graph H h
-          \<and> linearform H h
-          \<and> H \<unlhd> E
-          \<and> F \<unlhd> H
-          \<and> graph F f \<subseteq> graph H h
-          \<and> (\<forall>x \<in> H. h x \<le> p x)" by blast
+    have a: "graph ?H ?h = \<Union>c"
+    proof (rule graph_domain_funct)
+      fix x y z assume "(x, y) \<in> \<Union>c" and "(x, z) \<in> \<Union>c"
+      with M_def cM show "z = y" by (rule sup_definite)
     qed
-  }
+    moreover from M cM a have "linearform ?H ?h"
+      by (rule sup_lf)
+    moreover from a M cM ex FE E have "?H \<unlhd> E"
+      by (rule sup_subE)
+    moreover from a M cM ex FE have "F \<unlhd> ?H"
+      by (rule sup_supF)
+    moreover from a M cM ex have "graph F f \<subseteq> graph ?H ?h"
+      by (rule sup_ext)
+    moreover from a M cM have "\<forall>x \<in> ?H. ?h x \<le> p x"
+      by (rule sup_norm_pres)
+    ultimately show "\<exists>H h. \<Union>c = graph H h
+        \<and> linearform H h
+        \<and> H \<unlhd> E
+        \<and> F \<unlhd> H
+        \<and> graph F f \<subseteq> graph H h
+        \<and> (\<forall>x \<in> H. h x \<le> p x)" by blast
+  qed
   then have "\<exists>g \<in> M. \<forall>x \<in> M. g \<subseteq> x \<longrightarrow> x = g"
   \<comment> \<open>With Zorn's Lemma we can conclude that there is a maximal element in \<open>M\<close>. \<^smallskip>\<close>
   proof (rule Zorn's_Lemma)
@@ -371,11 +368,11 @@
   have q: "seminorm E p"
   proof
     fix x y a assume x: "x \<in> E" and y: "y \<in> E"
-    
+
     txt \<open>\<open>p\<close> is positive definite:\<close>
     have "0 \<le> \<parallel>f\<parallel>\<hyphen>F" by (rule ge_zero)
     moreover from x have "0 \<le> \<parallel>x\<parallel>" ..
-    ultimately show "0 \<le> p x"  
+    ultimately show "0 \<le> p x"
       by (simp add: p_def zero_le_mult_iff)
 
     txt \<open>\<open>p\<close> is absolutely homogeneous:\<close>
diff -r d8f77c1c9703 -r 2575f1bd226b src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy
--- a/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy	Sat Nov 16 20:22:26 2024 +0100
+++ b/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy	Sat Nov 16 21:36:34 2024 +0100
@@ -61,21 +61,22 @@
     then show "\<exists>u. \<forall>y \<in> ?S. y \<le> u" ..
   qed
   then obtain xi where xi: "lub ?S xi" ..
-  {
-    fix y assume "y \<in> F"
-    then have "a y \<in> ?S" by blast
-    with xi have "a y \<le> xi" by (rule lub.upper)
-  }
-  moreover {
-    fix y assume y: "y \<in> F"
-    from xi have "xi \<le> b y"
+  have "a y \<le> xi" if "y \<in> F" for y
+  proof -
+    from that have "a y \<in> ?S" by blast
+    with xi show ?thesis by (rule lub.upper)
+  qed
+  moreover have "xi \<le> b y" if y: "y \<in> F" for y
+  proof -
+    from xi
+    show ?thesis
     proof (rule lub.least)
       fix au assume "au \<in> ?S"
       then obtain u where u: "u \<in> F" and au: "au = a u" by blast
       from u y have "a u \<le> b y" by (rule r)
       with au show "au \<le> b y" by (simp only:)
     qed
-  }
+  qed
   ultimately show "\<exists>xi. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> b y" by blast
 qed
 
@@ -106,83 +107,78 @@
       have "lin x0 \<unlhd> E" ..
       with HE show "vectorspace (H + lin x0)" using E ..
     qed
-    {
-      fix x1 x2 assume x1: "x1 \<in> H'" and x2: "x2 \<in> H'"
-      show "h' (x1 + x2) = h' x1 + h' x2"
-      proof -
-        from H' x1 x2 have "x1 + x2 \<in> H'"
-          by (rule vectorspace.add_closed)
-        with x1 x2 obtain y y1 y2 a a1 a2 where
-          x1x2: "x1 + x2 = y + a \<cdot> x0" and y: "y \<in> H"
-          and x1_rep: "x1 = y1 + a1 \<cdot> x0" and y1: "y1 \<in> H"
-          and x2_rep: "x2 = y2 + a2 \<cdot> x0" and y2: "y2 \<in> H"
-          unfolding H'_def sum_def lin_def by blast
-        
-        have ya: "y1 + y2 = y \<and> a1 + a2 = a" using E HE _ y x0
-        proof (rule decomp_H') text_raw \<open>\label{decomp-H-use}\<close>
-          from HE y1 y2 show "y1 + y2 \<in> H"
-            by (rule subspace.add_closed)
-          from x0 and HE y y1 y2
-          have "x0 \<in> E"  "y \<in> E"  "y1 \<in> E"  "y2 \<in> E" by auto
-          with x1_rep x2_rep have "(y1 + y2) + (a1 + a2) \<cdot> x0 = x1 + x2"
-            by (simp add: add_ac add_mult_distrib2)
-          also note x1x2
-          finally show "(y1 + y2) + (a1 + a2) \<cdot> x0 = y + a \<cdot> x0" .
-        qed
-        
-        from h'_def x1x2 E HE y x0
-        have "h' (x1 + x2) = h y + a * xi"
-          by (rule h'_definite)
-        also have "\<dots> = h (y1 + y2) + (a1 + a2) * xi"
-          by (simp only: ya)
-        also from y1 y2 have "h (y1 + y2) = h y1 + h y2"
-          by simp
-        also have "\<dots> + (a1 + a2) * xi = (h y1 + a1 * xi) + (h y2 + a2 * xi)"
-          by (simp add: distrib_right)
-        also from h'_def x1_rep E HE y1 x0
-        have "h y1 + a1 * xi = h' x1"
-          by (rule h'_definite [symmetric])
-        also from h'_def x2_rep E HE y2 x0
-        have "h y2 + a2 * xi = h' x2"
-          by (rule h'_definite [symmetric])
-        finally show ?thesis .
+    show "h' (x1 + x2) = h' x1 + h' x2" if x1: "x1 \<in> H'" and x2: "x2 \<in> H'" for x1 x2
+    proof -
+      from H' x1 x2 have "x1 + x2 \<in> H'"
+        by (rule vectorspace.add_closed)
+      with x1 x2 obtain y y1 y2 a a1 a2 where
+        x1x2: "x1 + x2 = y + a \<cdot> x0" and y: "y \<in> H"
+        and x1_rep: "x1 = y1 + a1 \<cdot> x0" and y1: "y1 \<in> H"
+        and x2_rep: "x2 = y2 + a2 \<cdot> x0" and y2: "y2 \<in> H"
+        unfolding H'_def sum_def lin_def by blast
+
+      have ya: "y1 + y2 = y \<and> a1 + a2 = a" using E HE _ y x0
+      proof (rule decomp_H') text_raw \<open>\label{decomp-H-use}\<close>
+        from HE y1 y2 show "y1 + y2 \<in> H"
+          by (rule subspace.add_closed)
+        from x0 and HE y y1 y2
+        have "x0 \<in> E"  "y \<in> E"  "y1 \<in> E"  "y2 \<in> E" by auto
+        with x1_rep x2_rep have "(y1 + y2) + (a1 + a2) \<cdot> x0 = x1 + x2"
+          by (simp add: add_ac add_mult_distrib2)
+        also note x1x2
+        finally show "(y1 + y2) + (a1 + a2) \<cdot> x0 = y + a \<cdot> x0" .
       qed
-    next
-      fix x1 c assume x1: "x1 \<in> H'"
-      show "h' (c \<cdot> x1) = c * (h' x1)"
-      proof -
-        from H' x1 have ax1: "c \<cdot> x1 \<in> H'"
-          by (rule vectorspace.mult_closed)
-        with x1 obtain y a y1 a1 where
-            cx1_rep: "c \<cdot> x1 = y + a \<cdot> x0" and y: "y \<in> H"
-          and x1_rep: "x1 = y1 + a1 \<cdot> x0" and y1: "y1 \<in> H"
-          unfolding H'_def sum_def lin_def by blast
-        
-        have ya: "c \<cdot> y1 = y \<and> c * a1 = a" using E HE _ y x0
-        proof (rule decomp_H')
-          from HE y1 show "c \<cdot> y1 \<in> H"
-            by (rule subspace.mult_closed)
-          from x0 and HE y y1
-          have "x0 \<in> E"  "y \<in> E"  "y1 \<in> E" by auto
-          with x1_rep have "c \<cdot> y1 + (c * a1) \<cdot> x0 = c \<cdot> x1"
-            by (simp add: mult_assoc add_mult_distrib1)
-          also note cx1_rep
-          finally show "c \<cdot> y1 + (c * a1) \<cdot> x0 = y + a \<cdot> x0" .
-        qed
-        
-        from h'_def cx1_rep E HE y x0 have "h' (c \<cdot> x1) = h y + a * xi"
-          by (rule h'_definite)
-        also have "\<dots> = h (c \<cdot> y1) + (c * a1) * xi"
-          by (simp only: ya)
-        also from y1 have "h (c \<cdot> y1) = c * h y1"
-          by simp
-        also have "\<dots> + (c * a1) * xi = c * (h y1 + a1 * xi)"
-          by (simp only: distrib_left)
-        also from h'_def x1_rep E HE y1 x0 have "h y1 + a1 * xi = h' x1"
-          by (rule h'_definite [symmetric])
-        finally show ?thesis .
+
+      from h'_def x1x2 E HE y x0
+      have "h' (x1 + x2) = h y + a * xi"
+        by (rule h'_definite)
+      also have "\<dots> = h (y1 + y2) + (a1 + a2) * xi"
+        by (simp only: ya)
+      also from y1 y2 have "h (y1 + y2) = h y1 + h y2"
+        by simp
+      also have "\<dots> + (a1 + a2) * xi = (h y1 + a1 * xi) + (h y2 + a2 * xi)"
+        by (simp add: distrib_right)
+      also from h'_def x1_rep E HE y1 x0
+      have "h y1 + a1 * xi = h' x1"
+        by (rule h'_definite [symmetric])
+      also from h'_def x2_rep E HE y2 x0
+      have "h y2 + a2 * xi = h' x2"
+        by (rule h'_definite [symmetric])
+      finally show ?thesis .
+    qed
+    show "h' (c \<cdot> x1) = c * (h' x1)" if x1: "x1 \<in> H'" for x1 c
+    proof -
+      from H' x1 have ax1: "c \<cdot> x1 \<in> H'"
+        by (rule vectorspace.mult_closed)
+      with x1 obtain y a y1 a1 where
+          cx1_rep: "c \<cdot> x1 = y + a \<cdot> x0" and y: "y \<in> H"
+        and x1_rep: "x1 = y1 + a1 \<cdot> x0" and y1: "y1 \<in> H"
+        unfolding H'_def sum_def lin_def by blast
+
+      have ya: "c \<cdot> y1 = y \<and> c * a1 = a" using E HE _ y x0
+      proof (rule decomp_H')
+        from HE y1 show "c \<cdot> y1 \<in> H"
+          by (rule subspace.mult_closed)
+        from x0 and HE y y1
+        have "x0 \<in> E"  "y \<in> E"  "y1 \<in> E" by auto
+        with x1_rep have "c \<cdot> y1 + (c * a1) \<cdot> x0 = c \<cdot> x1"
+          by (simp add: mult_assoc add_mult_distrib1)
+        also note cx1_rep
+        finally show "c \<cdot> y1 + (c * a1) \<cdot> x0 = y + a \<cdot> x0" .
       qed
-    }
+
+      from h'_def cx1_rep E HE y x0 have "h' (c \<cdot> x1) = h y + a * xi"
+        by (rule h'_definite)
+      also have "\<dots> = h (c \<cdot> y1) + (c * a1) * xi"
+        by (simp only: ya)
+      also from y1 have "h (c \<cdot> y1) = c * h y1"
+        by simp
+      also have "\<dots> + (c * a1) * xi = c * (h y1 + a1 * xi)"
+        by (simp only: distrib_left)
+      also from h'_def x1_rep E HE y1 x0 have "h y1 + a1 * xi = h' x1"
+        by (rule h'_definite [symmetric])
+      finally show ?thesis .
+    qed
   qed
 qed
 
@@ -218,7 +214,7 @@
         unfolding H'_def sum_def lin_def by blast
       from y have y': "y \<in> E" ..
       from y have ay: "inverse a \<cdot> y \<in> H" by simp
-      
+
       from h'_def x_rep E HE y x0 have "h' x = h y + a * xi"
         by (rule h'_definite)
       also have "\<dots> \<le> p (y + a \<cdot> x0)"
@@ -237,7 +233,7 @@
         with lz have "a * xi \<le>
           a * (- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))"
           by (simp add: mult_left_mono_neg order_less_imp_le)
-        
+
         also have "\<dots> =
           - a * (p (inverse a \<cdot> y + x0)) - a * (h (inverse a \<cdot> y))"
           by (simp add: right_diff_distrib)
diff -r d8f77c1c9703 -r 2575f1bd226b src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy
--- a/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy	Sat Nov 16 20:22:26 2024 +0100
+++ b/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy	Sat Nov 16 21:36:34 2024 +0100
@@ -300,11 +300,10 @@
   from FE show "F \<noteq> {}" by (rule subspace.non_empty)
   from graph M cM ex have "graph F f \<subseteq> graph H h" by (rule sup_ext)
   then show "F \<subseteq> H" ..
-  fix x y assume "x \<in> F" and "y \<in> F"
-  with FE show "x + y \<in> F" by (rule subspace.add_closed)
-next
-  fix x a assume "x \<in> F"
-  with FE show "a \<cdot> x \<in> F" by (rule subspace.mult_closed)
+  show "x + y \<in> F" if "x \<in> F" and "y \<in> F" for x y
+    using FE that by (rule subspace.add_closed)
+  show "a \<cdot> x \<in> F" if "x \<in> F" for x a
+    using FE that by (rule subspace.mult_closed)
 qed
 
 text \<open>
@@ -409,37 +408,32 @@
   interpret seminorm E p by fact
   interpret linearform H h by fact
   have H: "vectorspace H" using \<open>vectorspace E\<close> ..
-  {
-    assume l: ?L
-    show ?R
-    proof
-      fix x assume x: "x \<in> H"
-      have "h x \<le> \<bar>h x\<bar>" by arith
-      also from l x have "\<dots> \<le> p x" ..
-      finally show "h x \<le> p x" .
+  show ?R if l: ?L
+  proof
+    fix x assume x: "x \<in> H"
+    have "h x \<le> \<bar>h x\<bar>" by arith
+    also from l x have "\<dots> \<le> p x" ..
+    finally show "h x \<le> p x" .
+  qed
+  show ?L if r: ?R
+  proof
+    fix x assume x: "x \<in> H"
+    show "\<bar>b\<bar> \<le> a" when "- a \<le> b" "b \<le> a" for a b :: real
+      using that by arith
+    from \<open>linearform H h\<close> and H x
+    have "- h x = h (- x)" by (rule linearform.neg [symmetric])
+    also
+    from H x have "- x \<in> H" by (rule vectorspace.neg_closed)
+    with r have "h (- x) \<le> p (- x)" ..
+    also have "\<dots> = p x"
+      using \<open>seminorm E p\<close> \<open>vectorspace E\<close>
+    proof (rule seminorm.minus)
+      from x show "x \<in> E" ..
     qed
-  next
-    assume r: ?R
-    show ?L
-    proof
-      fix x assume x: "x \<in> H"
-      show "\<bar>b\<bar> \<le> a" when "- a \<le> b" "b \<le> a" for a b :: real
-        using that by arith
-      from \<open>linearform H h\<close> and H x
-      have "- h x = h (- x)" by (rule linearform.neg [symmetric])
-      also
-      from H x have "- x \<in> H" by (rule vectorspace.neg_closed)
-      with r have "h (- x) \<le> p (- x)" ..
-      also have "\<dots> = p x"
-        using \<open>seminorm E p\<close> \<open>vectorspace E\<close>
-      proof (rule seminorm.minus)
-        from x show "x \<in> E" ..
-      qed
-      finally have "- h x \<le> p x" .
-      then show "- p x \<le> h x" by simp
-      from r x show "h x \<le> p x" ..
-    qed
-  }
+    finally have "- h x \<le> p x" .
+    then show "- p x \<le> h x" by simp
+    from r x show "h x \<le> p x" ..
+  qed
 qed
 
 end
diff -r d8f77c1c9703 -r 2575f1bd226b src/HOL/Hahn_Banach/Normed_Space.thy
--- a/src/HOL/Hahn_Banach/Normed_Space.thy	Sat Nov 16 20:22:26 2024 +0100
+++ b/src/HOL/Hahn_Banach/Normed_Space.thy	Sat Nov 16 21:36:34 2024 +0100
@@ -101,8 +101,8 @@
   interpret normed_vectorspace E norm by fact
   show ?thesis
   proof
-    show "vectorspace F" by (rule vectorspace) unfold_locales
-  next
+    show "vectorspace F"
+      by (rule vectorspace) unfold_locales
     have "Normed_Space.norm E norm" ..
     with subset show "Normed_Space.norm F norm"
       by (simp add: norm_def seminorm_def norm_axioms_def)
diff -r d8f77c1c9703 -r 2575f1bd226b src/HOL/Hahn_Banach/Subspace.thy
--- a/src/HOL/Hahn_Banach/Subspace.thy	Sat Nov 16 20:22:26 2024 +0100
+++ b/src/HOL/Hahn_Banach/Subspace.thy	Sat Nov 16 21:36:34 2024 +0100
@@ -110,9 +110,7 @@
 proof
   show "V \<noteq> {}" ..
   show "V \<subseteq> V" ..
-next
-  fix x y assume x: "x \<in> V" and y: "y \<in> V"
-  fix a :: real
+  fix a :: real and x y assume x: "x \<in> V" and y: "y \<in> V"
   from x y show "x + y \<in> V" by simp
   from x show "a \<cdot> x \<in> V" by simp
 qed
@@ -181,14 +179,13 @@
   shows "lin x \<unlhd> V"
 proof
   from x show "lin x \<noteq> {}" by auto
-next
   show "lin x \<subseteq> V"
   proof
     fix x' assume "x' \<in> lin x"
     then obtain a where "x' = a \<cdot> x" ..
     with x show "x' \<in> V" by simp
   qed
-next
+
   fix x' x'' assume x': "x' \<in> lin x" and x'': "x'' \<in> lin x"
   show "x' + x'' \<in> lin x"
   proof -
@@ -199,8 +196,7 @@
     also have "\<dots> \<in> lin x" ..
     finally show ?thesis .
   qed
-  fix a :: real
-  show "a \<cdot> x' \<in> lin x"
+  show "a \<cdot> x' \<in> lin x" for a :: real
   proof -
     from x' obtain a' where "x' = a' \<cdot> x" ..
     with x have "a \<cdot> x' = (a * a') \<cdot> x" by (simp add: mult_assoc)
@@ -294,7 +290,7 @@
         "u \<in> U" and "v \<in> V" ..
       then show "x \<in> E" by simp
     qed
-  next
+
     fix x y assume x: "x \<in> U + V" and y: "y \<in> U + V"
     show "x + y \<in> U + V"
     proof -
@@ -308,7 +304,7 @@
         using x y by (simp_all add: add_ac)
       then show ?thesis ..
     qed
-    fix a show "a \<cdot> x \<in> U + V"
+    show "a \<cdot> x \<in> U + V" for a
     proof -
       from x obtain u v where "x = u + v" and "u \<in> U" and "v \<in> V" ..
       then have "a \<cdot> u \<in> U" and "a \<cdot> v \<in> V"
@@ -359,7 +355,7 @@
     from v2 v1 have v: "v2 - v1 \<in> V"
       by (rule vectorspace.diff_closed [OF V])
     with eq have u': " u1 - u2 \<in> V" by (simp only:)
-    
+
     show "u1 = u2"
     proof (rule add_minus_eq)
       from u1 show "u1 \<in> E" ..
@@ -405,14 +401,14 @@
           then obtain a where xx': "x = a \<cdot> x'"
             by blast
           have "x = 0"
-          proof cases
-            assume "a = 0"
+          proof (cases "a = 0")
+            case True
             with xx' and x' show ?thesis by simp
           next
-            assume a: "a \<noteq> 0"
+            case False
             from x have "x \<in> H" ..
             with xx' have "inverse a \<cdot> a \<cdot> x' \<in> H" by simp
-            with a and x' have "x' \<in> H" by (simp add: mult_assoc2)
+            with False and x' have "x' \<in> H" by (simp add: mult_assoc2)
             with \<open>x' \<notin> H\<close> show ?thesis by contradiction
           qed
           then show "x \<in> {0}" ..
diff -r d8f77c1c9703 -r 2575f1bd226b src/HOL/Hahn_Banach/Zorn_Lemma.thy
--- a/src/HOL/Hahn_Banach/Zorn_Lemma.thy	Sat Nov 16 20:22:26 2024 +0100
+++ b/src/HOL/Hahn_Banach/Zorn_Lemma.thy	Sat Nov 16 21:36:34 2024 +0100
@@ -27,17 +27,15 @@
   proof
     fix c assume "c \<in> chains S"
     show "\<exists>y \<in> S. \<forall>z \<in> c. z \<subseteq> y"
-    proof cases
+    proof (cases "c = {}")
       txt \<open>If \<open>c\<close> is an empty chain, then every element in \<open>S\<close> is an upper
         bound of \<open>c\<close>.\<close>
-
-      assume "c = {}"
+      case True
       with aS show ?thesis by fast
-
+    next
       txt \<open>If \<open>c\<close> is non-empty, then \<open>\<Union>c\<close> is an upper bound of \<open>c\<close>, lying in
         \<open>S\<close>.\<close>
-    next
-      assume "c \<noteq> {}"
+      case False
       show ?thesis
       proof
         show "\<forall>z \<in> c. z \<subseteq> \<Union>c" by fast