--- 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
--- 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>
--- 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)
--- 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
--- 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)
--- 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}" ..
--- 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