--- a/src/HOL/Real/HahnBanach/Bounds.thy Tue Jul 15 16:50:09 2008 +0200
+++ b/src/HOL/Real/HahnBanach/Bounds.thy Tue Jul 15 19:39:37 2008 +0200
@@ -28,7 +28,8 @@
shows "\<Squnion>A = (x::'a::order)"
proof -
interpret lub [A x] by fact
- show ?thesis proof (unfold the_lub_def)
+ show ?thesis
+ proof (unfold the_lub_def)
from `lub A x` show "The (lub A) = x"
proof
fix x' assume lub': "lub A x'"
@@ -73,7 +74,7 @@
shows "\<exists>x. lub A x"
proof -
from ex_upper have "\<exists>y. isUb UNIV A y"
- by (unfold isUb_def setle_def) blast
+ unfolding isUb_def setle_def by blast
with nonempty have "\<exists>x. isLub UNIV A x"
by (rule reals_complete)
then show ?thesis by (simp only: lub_compat)
--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy Tue Jul 15 16:50:09 2008 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy Tue Jul 15 19:39:37 2008 +0200
@@ -5,7 +5,9 @@
header {* The norm of a function *}
-theory FunctionNorm imports NormedSpace FunctionOrder begin
+theory FunctionNorm
+imports NormedSpace FunctionOrder
+begin
subsection {* Continuous linear forms*}
@@ -97,7 +99,7 @@
proof (rule real_complete)
txt {* First we have to show that @{text B} is non-empty: *}
have "0 \<in> B V f" ..
- thus "\<exists>x. x \<in> B V f" ..
+ then show "\<exists>x. x \<in> B V f" ..
txt {* Then we have to show that @{text B} is bounded: *}
show "\<exists>c. \<forall>y \<in> B V f. y \<le> c"
@@ -116,7 +118,7 @@
show "y \<le> b"
proof cases
assume "y = 0"
- thus ?thesis by (unfold b_def) arith
+ then show ?thesis unfolding b_def by arith
next
txt {* The second case is @{text "y = \<bar>f x\<bar> / \<parallel>x\<parallel>"} for some
@{text "x \<in> V"} with @{text "x \<noteq> 0"}. *}
@@ -135,21 +137,21 @@
from c x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..
from gt have "0 < inverse \<parallel>x\<parallel>"
by (rule positive_imp_inverse_positive)
- thus "0 \<le> inverse \<parallel>x\<parallel>" by (rule order_less_imp_le)
+ then show "0 \<le> inverse \<parallel>x\<parallel>" by (rule order_less_imp_le)
qed
also have "\<dots> = c * (\<parallel>x\<parallel> * inverse \<parallel>x\<parallel>)"
by (rule real_mult_assoc)
also
from gt have "\<parallel>x\<parallel> \<noteq> 0" by simp
- hence "\<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 le_maxI1)
finally show "y \<le> b" .
qed
qed
- thus ?thesis ..
+ then show ?thesis ..
qed
qed
- then show ?thesis by (unfold fn_norm_def) (rule the_lubI_ex)
+ then show ?thesis unfolding fn_norm_def by (rule the_lubI_ex)
qed
lemma (in normed_vectorspace_with_fn_norm) fn_norm_ub [iff?]:
@@ -185,7 +187,6 @@
So it is @{text "\<ge> 0"} if all elements in @{text B} are @{text "\<ge>
0"}, provided the supremum exists and @{text B} is not empty. *}
have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
-(* unfolding B_def fn_norm_def *)
using `continuous V norm f` by (rule fn_norm_works)
moreover have "0 \<in> B V f" ..
ultimately show ?thesis ..
@@ -205,7 +206,8 @@
proof -
interpret continuous [V norm f] by fact
interpret linearform [V f] .
- show ?thesis proof cases
+ show ?thesis
+ proof cases
assume "x = 0"
then have "\<bar>f x\<bar> = \<bar>f 0\<bar>" by simp
also have "f 0 = 0" by rule unfold_locales
@@ -245,7 +247,8 @@
shows "\<parallel>f\<parallel>\<hyphen>V \<le> c"
proof -
interpret continuous [V norm f] by fact
- show ?thesis proof (rule fn_norm_leastB [folded B_def fn_norm_def])
+ show ?thesis
+ 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
--- a/src/HOL/Real/HahnBanach/FunctionOrder.thy Tue Jul 15 16:50:09 2008 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy Tue Jul 15 19:39:37 2008 +0200
@@ -5,7 +5,9 @@
header {* An order on functions *}
-theory FunctionOrder imports Subspace Linearform begin
+theory FunctionOrder
+imports Subspace Linearform
+begin
subsection {* The graph of a function *}
@@ -27,14 +29,14 @@
"graph F f = {(x, f x) | x. x \<in> F}"
lemma graphI [intro]: "x \<in> F \<Longrightarrow> (x, f x) \<in> graph F f"
- by (unfold graph_def) blast
+ unfolding graph_def by blast
lemma graphI2 [intro?]: "x \<in> F \<Longrightarrow> \<exists>t \<in> graph F f. t = (x, f x)"
- by (unfold graph_def) blast
+ unfolding graph_def by blast
lemma graphE [elim?]:
"(x, y) \<in> graph F f \<Longrightarrow> (x \<in> F \<Longrightarrow> y = f x \<Longrightarrow> C) \<Longrightarrow> C"
- by (unfold graph_def) blast
+ unfolding graph_def by blast
subsection {* Functions ordered by domain extension *}
@@ -47,15 +49,15 @@
lemma graph_extI:
"(\<And>x. x \<in> H \<Longrightarrow> h x = h' x) \<Longrightarrow> H \<subseteq> H'
\<Longrightarrow> graph H h \<subseteq> graph H' h'"
- by (unfold graph_def) blast
+ unfolding graph_def by blast
lemma graph_extD1 [dest?]:
"graph H h \<subseteq> graph H' h' \<Longrightarrow> x \<in> H \<Longrightarrow> h x = h' x"
- by (unfold graph_def) blast
+ unfolding graph_def by blast
lemma graph_extD2 [dest?]:
"graph H h \<subseteq> graph H' h' \<Longrightarrow> H \<subseteq> H'"
- by (unfold graph_def) blast
+ unfolding graph_def by blast
subsection {* Domain and function of a graph *}
@@ -81,7 +83,8 @@
lemma graph_domain_funct:
assumes uniq: "\<And>x y z. (x, y) \<in> g \<Longrightarrow> (x, z) \<in> g \<Longrightarrow> z = y"
shows "graph (domain g) (funct g) = g"
-proof (unfold domain_def funct_def graph_def, auto) (* FIXME !? *)
+ unfolding domain_def funct_def graph_def
+proof auto (* FIXME !? *)
fix a b assume g: "(a, b) \<in> g"
from g show "(a, SOME y. (a, y) \<in> g) \<in> g" by (rule someI2)
from g show "\<exists>y. (a, y) \<in> g" ..
@@ -119,13 +122,13 @@
\<Longrightarrow> (\<And>H h. g = graph H h \<Longrightarrow> linearform H h
\<Longrightarrow> H \<unlhd> E \<Longrightarrow> F \<unlhd> H \<Longrightarrow> graph F f \<subseteq> graph H h
\<Longrightarrow> \<forall>x \<in> H. h x \<le> p x \<Longrightarrow> C) \<Longrightarrow> C"
- by (unfold norm_pres_extensions_def) blast
+ unfolding norm_pres_extensions_def by blast
lemma norm_pres_extensionI2 [intro]:
"linearform H h \<Longrightarrow> H \<unlhd> E \<Longrightarrow> F \<unlhd> H
\<Longrightarrow> graph F f \<subseteq> graph H h \<Longrightarrow> \<forall>x \<in> H. h x \<le> p x
\<Longrightarrow> graph H h \<in> norm_pres_extensions E p F f"
- by (unfold norm_pres_extensions_def) blast
+ unfolding norm_pres_extensions_def by blast
lemma norm_pres_extensionI: (* FIXME ? *)
"\<exists>H h. g = graph H h
@@ -134,6 +137,6 @@
\<and> F \<unlhd> H
\<and> graph F f \<subseteq> graph H h
\<and> (\<forall>x \<in> H. h x \<le> p x) \<Longrightarrow> g \<in> norm_pres_extensions E p F f"
- by (unfold norm_pres_extensions_def) blast
+ unfolding norm_pres_extensions_def by blast
end
--- a/src/HOL/Real/HahnBanach/HahnBanach.thy Tue Jul 15 16:50:09 2008 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy Tue Jul 15 19:39:37 2008 +0200
@@ -5,7 +5,9 @@
header {* The Hahn-Banach Theorem *}
-theory HahnBanach imports HahnBanachLemmas begin
+theory HahnBanach
+imports HahnBanachLemmas
+begin
text {*
We present the proof of two different versions of the Hahn-Banach
@@ -66,7 +68,7 @@
interpret seminorm [E p] by fact
interpret linearform [F f] by fact
def M \<equiv> "norm_pres_extensions E p F f"
- hence M: "M = \<dots>" by (simp only:)
+ then have M: "M = \<dots>" by (simp only:)
from E have F: "vectorspace F" ..
note FE = `F \<unlhd> E`
{
@@ -74,7 +76,8 @@
have "\<Union>c \<in> M"
-- {* Show that every non-empty chain @{text c} of @{text M} has an upper bound in @{text M}: *}
-- {* @{text "\<Union>c"} is greater than any element of the chain @{text c}, so it suffices to show @{text "\<Union>c \<in> M"}. *}
- proof (unfold M_def, rule norm_pres_extensionI)
+ unfolding M_def
+ proof (rule norm_pres_extensionI)
let ?H = "domain (\<Union>c)"
let ?h = "funct (\<Union>c)"
@@ -101,12 +104,13 @@
\<and> (\<forall>x \<in> H. h x \<le> p x)" by blast
qed
}
- hence "\<exists>g \<in> M. \<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x"
+ then have "\<exists>g \<in> M. \<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x"
-- {* With Zorn's Lemma we can conclude that there is a maximal element in @{text M}. \skp *}
proof (rule Zorn's_Lemma)
-- {* We show that @{text M} is non-empty: *}
show "graph F f \<in> M"
- proof (unfold M_def, rule norm_pres_extensionI2)
+ unfolding M_def
+ proof (rule norm_pres_extensionI2)
show "linearform F f" by fact
show "F \<unlhd> E" by fact
from F show "F \<unlhd> F" by (rule vectorspace.subspace_refl)
@@ -116,12 +120,12 @@
qed
then obtain g where gM: "g \<in> M" and gx: "\<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x"
by blast
- from gM [unfolded M_def] obtain H h where
+ from gM obtain H h where
g_rep: "g = graph H h"
and linearform: "linearform H h"
and HE: "H \<unlhd> E" and FH: "F \<unlhd> H"
and graphs: "graph F f \<subseteq> graph H h"
- and hp: "\<forall>x \<in> H. h x \<le> p x" ..
+ and hp: "\<forall>x \<in> H. h x \<le> p x" unfolding M_def ..
-- {* @{text g} is a norm-preserving extension of @{text f}, in other words: *}
-- {* @{text g} is the graph of some linear form @{text h} defined on a subspace @{text H} of @{text E}, *}
-- {* and @{text h} is an extension of @{text f} that is again bounded by @{text p}. \skp *}
@@ -213,14 +217,15 @@
proof
assume eq: "graph H h = graph H' h'"
have "x' \<in> H'"
- proof (unfold H'_def, rule)
+ unfolding H'_def
+ proof
from H show "0 \<in> H" by (rule vectorspace.zero)
from x'E show "x' \<in> lin x'" by (rule x_lin_x)
from x'E show "x' = 0 + x'" by simp
qed
- hence "(x', h' x') \<in> graph H' h'" ..
+ then have "(x', h' x') \<in> graph H' h'" ..
with eq have "(x', h' x') \<in> graph H h" by (simp only:)
- hence "x' \<in> H" ..
+ then have "x' \<in> H" ..
with `x' \<notin> H` show False by contradiction
qed
with g_rep show ?thesis by simp
@@ -252,7 +257,7 @@
by (simp add: Let_def)
also have "(x, 0) =
(SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H)"
- using E HE
+ using E HE
proof (rule decomp_H'_H [symmetric])
from FH x show "x \<in> H" ..
from x' show "x' \<noteq> 0" .
@@ -274,7 +279,7 @@
qed
ultimately show ?thesis ..
qed
- hence "\<not> (\<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x)" by simp
+ then have "\<not> (\<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x)" by simp
-- {* So the graph @{text g} of @{text h} cannot be maximal. Contradiction! \skp *}
with gx show "H = E" by contradiction
qed
@@ -321,12 +326,8 @@
interpret subspace [F E] by fact
interpret linearform [F f] by fact
interpret seminorm [E p] by fact
-(* note E = `vectorspace E`
- note FE = `subspace F E`
- note sn = `seminorm E p`
- note lf = `linearform F f`
-*) have "\<exists>g. linearform E g \<and> (\<forall>x \<in> F. g x = f x) \<and> (\<forall>x \<in> E. g x \<le> p x)"
- using E FE sn lf
+ have "\<exists>g. linearform E g \<and> (\<forall>x \<in> F. g x = f x) \<and> (\<forall>x \<in> E. g x \<le> p x)"
+ using E FE sn lf
proof (rule HahnBanach)
show "\<forall>x \<in> F. f x \<le> p x"
using FE E sn lf and fp by (rule abs_ineq_iff [THEN iffD1])
@@ -334,7 +335,7 @@
then obtain g where lg: "linearform E g" and *: "\<forall>x \<in> F. g x = f x"
and **: "\<forall>x \<in> E. g x \<le> p x" by blast
have "\<forall>x \<in> E. \<bar>g x\<bar> \<le> p x"
- using _ E sn lg **
+ using _ E sn lg **
proof (rule abs_ineq_iff [THEN iffD2])
show "E \<unlhd> E" ..
qed
@@ -384,10 +385,10 @@
have q: "seminorm E p"
proof
fix x y a assume x: "x \<in> E" and y: "y \<in> E"
-
+
txt {* @{text p} is positive definite: *}
- have "0 \<le> \<parallel>f\<parallel>\<hyphen>F" by (rule ge_zero)
- moreover from x have "0 \<le> \<parallel>x\<parallel>" ..
+ 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"
by (simp add: p_def zero_le_mult_iff)
@@ -422,9 +423,9 @@
have "\<forall>x \<in> F. \<bar>f x\<bar> \<le> p x"
proof
fix x assume "x \<in> F"
- from this and `continuous F norm f`
+ with `continuous F norm f` and linearform
show "\<bar>f x\<bar> \<le> p x"
- by (unfold p_def) (rule normed_vectorspace_with_fn_norm.fn_norm_le_cong
+ unfolding p_def by (rule normed_vectorspace_with_fn_norm.fn_norm_le_cong
[OF normed_vectorspace_with_fn_norm.intro,
OF F_norm, folded B_def fn_norm_def])
qed
@@ -435,9 +436,9 @@
some function @{text g} on the whole vector space @{text E}. *}
with E FE linearform q obtain g where
- linearformE: "linearform E g"
- and a: "\<forall>x \<in> F. g x = f x"
- and b: "\<forall>x \<in> E. \<bar>g x\<bar> \<le> p x"
+ linearformE: "linearform E g"
+ and a: "\<forall>x \<in> F. g x = f x"
+ and b: "\<forall>x \<in> E. \<bar>g x\<bar> \<le> p x"
by (rule abs_HahnBanach [elim_format]) iprover
txt {* We furthermore have to show that @{text g} is also continuous: *}
@@ -489,7 +490,7 @@
proof
fix x assume x: "x \<in> F"
from a x have "g x = f x" ..
- hence "\<bar>f x\<bar> = \<bar>g x\<bar>" by (simp only:)
+ then have "\<bar>f x\<bar> = \<bar>g x\<bar>" by (simp only:)
also from g_cont
have "\<dots> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>"
proof (rule fn_norm_le_cong [of g, folded B_def fn_norm_def])
@@ -500,7 +501,6 @@
show "0 \<le> \<parallel>g\<parallel>\<hyphen>E"
using g_cont
by (rule fn_norm_ge_zero [of g, folded B_def fn_norm_def])
- next
show "continuous F norm f" by fact
qed
qed
--- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Tue Jul 15 16:50:09 2008 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Tue Jul 15 19:39:37 2008 +0200
@@ -5,7 +5,9 @@
header {* Extending non-maximal functions *}
-theory HahnBanachExtLemmas imports FunctionNorm begin
+theory HahnBanachExtLemmas
+imports FunctionNorm
+begin
text {*
In this section the following context is presumed. Let @{text E} be
@@ -98,7 +100,8 @@
proof -
interpret linearform [H h] by fact
interpret vectorspace [E] by fact
- show ?thesis proof
+ show ?thesis
+ proof
note E = `vectorspace E`
have H': "vectorspace H'"
proof (unfold H'_def)
@@ -116,7 +119,7 @@
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"
- by (unfold H'_def sum_def lin_def) blast
+ 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') txt_raw {* \label{decomp-H-use} *}
@@ -154,9 +157,9 @@
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"
+ 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"
- by (unfold H'_def sum_def lin_def) blast
+ 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')
@@ -204,15 +207,16 @@
interpret subspace [H E] by fact
interpret seminorm [E p] by fact
interpret linearform [H h] by fact
- show ?thesis proof
+ show ?thesis
+ proof
fix x assume x': "x \<in> H'"
show "h' x \<le> p x"
proof -
from a' have a1: "\<forall>ya \<in> H. - p (ya + x0) - h ya \<le> xi"
and a2: "\<forall>ya \<in> H. xi \<le> p (ya + x0) - h ya" by auto
from x' obtain y a where
- x_rep: "x = y + a \<cdot> x0" and y: "y \<in> H"
- by (unfold H'_def sum_def lin_def) blast
+ x_rep: "x = y + a \<cdot> x0" and y: "y \<in> H"
+ 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
@@ -228,7 +232,7 @@
next
txt {* In the case @{text "a < 0"}, we use @{text "a\<^sub>1"}
with @{text ya} taken as @{text "y / a"}: *}
- assume lz: "a < 0" hence nz: "a \<noteq> 0" by simp
+ assume lz: "a < 0" then have nz: "a \<noteq> 0" by simp
from a1 ay
have "- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y) \<le> xi" ..
with lz have "a * xi \<le>
@@ -250,13 +254,13 @@
next
txt {* In the case @{text "a > 0"}, we use @{text "a\<^sub>2"}
with @{text ya} taken as @{text "y / a"}: *}
- assume gz: "0 < a" hence nz: "a \<noteq> 0" by simp
+ assume gz: "0 < a" then have nz: "a \<noteq> 0" by simp
from a2 ay
have "xi \<le> p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y)" ..
with gz have "a * xi \<le>
a * (p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))"
by simp
- also have "... = a * p (inverse a \<cdot> y + x0) - a * h (inverse a \<cdot> y)"
+ also have "\<dots> = a * p (inverse a \<cdot> y + x0) - a * h (inverse a \<cdot> y)"
by (simp add: right_diff_distrib)
also from gz x0 y'
have "a * p (inverse a \<cdot> y + x0) = p (a \<cdot> (inverse a \<cdot> y + x0))"
--- a/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy Tue Jul 15 16:50:09 2008 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy Tue Jul 15 19:39:37 2008 +0200
@@ -5,7 +5,9 @@
header {* The supremum w.r.t.~the function order *}
-theory HahnBanachSupLemmas imports FunctionNorm ZornLemma begin
+theory HahnBanachSupLemmas
+imports FunctionNorm ZornLemma
+begin
text {*
This section contains some lemmas that will be used in the proof of
@@ -132,7 +134,7 @@
proof
assume ?case1
have "(x, h x) \<in> graph H'' h''" by fact
- also have "... \<subseteq> graph H' h'" by fact
+ also have "\<dots> \<subseteq> graph H' h'" by fact
finally have xh:"(x, h x) \<in> graph H' h'" .
then have "x \<in> H'" ..
moreover from y_hy have "y \<in> H'" ..
@@ -171,11 +173,11 @@
from G1 c have "G1 \<in> M" ..
then obtain H1 h1 where G1_rep: "G1 = graph H1 h1"
- by (unfold M_def) blast
+ unfolding M_def by blast
from G2 c have "G2 \<in> M" ..
then obtain H2 h2 where G2_rep: "G2 = graph H2 h2"
- by (unfold M_def) blast
+ unfolding M_def by blast
txt {* @{text "G\<^sub>1"} is contained in @{text "G\<^sub>2"}
or vice versa, since both @{text "G\<^sub>1"} and @{text
@@ -186,18 +188,18 @@
proof
assume ?case1
with xy' G2_rep have "(x, y) \<in> graph H2 h2" by blast
- hence "y = h2 x" ..
+ then have "y = h2 x" ..
also
from xz' G2_rep have "(x, z) \<in> graph H2 h2" by (simp only:)
- hence "z = h2 x" ..
+ then have "z = h2 x" ..
finally show ?thesis .
next
assume ?case2
with xz' G1_rep have "(x, z) \<in> graph H1 h1" by blast
- hence "z = h1 x" ..
+ then have "z = h1 x" ..
also
from xy' G1_rep have "(x, y) \<in> graph H1 h1" by (simp only:)
- hence "y = h1 x" ..
+ then have "y = h1 x" ..
finally show ?thesis ..
qed
qed
--- a/src/HOL/Real/HahnBanach/Linearform.thy Tue Jul 15 16:50:09 2008 +0200
+++ b/src/HOL/Real/HahnBanach/Linearform.thy Tue Jul 15 19:39:37 2008 +0200
@@ -5,7 +5,9 @@
header {* Linearforms *}
-theory Linearform imports VectorSpace begin
+theory Linearform
+imports VectorSpace
+begin
text {*
A \emph{linear form} is a function on a vector space into the reals
@@ -25,9 +27,9 @@
proof -
interpret vectorspace [V] by fact
assume x: "x \<in> V"
- hence "f (- x) = f ((- 1) \<cdot> x)" by (simp add: negate_eq1)
- also from x have "... = (- 1) * (f x)" by (rule mult)
- also from x have "... = - (f x)" by simp
+ then have "f (- x) = f ((- 1) \<cdot> x)" by (simp add: negate_eq1)
+ also from x have "\<dots> = (- 1) * (f x)" by (rule mult)
+ also from x have "\<dots> = - (f x)" by simp
finally show ?thesis .
qed
@@ -37,8 +39,8 @@
proof -
interpret vectorspace [V] by fact
assume x: "x \<in> V" and y: "y \<in> V"
- hence "x - y = x + - y" by (rule diff_eq1)
- also have "f ... = f x + f (- y)" by (rule add) (simp_all add: x y)
+ then have "x - y = x + - y" by (rule diff_eq1)
+ also have "f \<dots> = f x + f (- y)" by (rule add) (simp_all add: x y)
also have "f (- y) = - f y" using `vectorspace V` y by (rule neg)
finally show ?thesis by simp
qed
--- a/src/HOL/Real/HahnBanach/NormedSpace.thy Tue Jul 15 16:50:09 2008 +0200
+++ b/src/HOL/Real/HahnBanach/NormedSpace.thy Tue Jul 15 19:39:37 2008 +0200
@@ -5,7 +5,9 @@
header {* Normed vector spaces *}
-theory NormedSpace imports Subspace begin
+theory NormedSpace
+imports Subspace
+begin
subsection {* Quasinorms *}
@@ -32,7 +34,7 @@
proof -
interpret vectorspace [V] by fact
assume x: "x \<in> V" and y: "y \<in> V"
- hence "x - y = x + - 1 \<cdot> y"
+ then have "x - y = x + - 1 \<cdot> y"
by (simp add: diff_eq2 negate_eq2a)
also from x y have "\<parallel>\<dots>\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>- 1 \<cdot> y\<parallel>"
by (simp add: subadditive)
@@ -48,7 +50,7 @@
proof -
interpret vectorspace [V] by fact
assume x: "x \<in> V"
- hence "- x = - 1 \<cdot> x" by (simp only: negate_eq1)
+ then have "- x = - 1 \<cdot> x" by (simp only: negate_eq1)
also from x have "\<parallel>\<dots>\<parallel> = \<bar>- 1\<bar> * \<parallel>x\<parallel>"
by (rule abs_homogenous)
also have "\<dots> = \<parallel>x\<parallel>" by simp
@@ -103,7 +105,8 @@
proof -
interpret subspace [F E] by fact
interpret normed_vectorspace [E norm] by fact
- show ?thesis proof
+ show ?thesis
+ proof
show "vectorspace F" by (rule vectorspace) unfold_locales
next
have "NormedSpace.norm E norm" by unfold_locales
--- a/src/HOL/Real/HahnBanach/Subspace.thy Tue Jul 15 16:50:09 2008 +0200
+++ b/src/HOL/Real/HahnBanach/Subspace.thy Tue Jul 15 19:39:37 2008 +0200
@@ -5,8 +5,9 @@
header {* Subspaces *}
-theory Subspace imports VectorSpace begin
-
+theory Subspace
+imports VectorSpace
+begin
subsection {* Definition *}
@@ -42,10 +43,11 @@
lemma (in subspace) diff_closed [iff]:
assumes "vectorspace V"
- shows "x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x - y \<in> U" (is "PROP ?P")
+ assumes x: "x \<in> U" and y: "y \<in> U"
+ shows "x - y \<in> U"
proof -
interpret vectorspace [V] by fact
- show "PROP ?P" by (simp add: diff_eq1 negate_eq1)
+ from x y show ?thesis by (simp add: diff_eq1 negate_eq1)
qed
text {*
@@ -61,17 +63,18 @@
interpret vectorspace [V] by fact
have "U \<noteq> {}" by (rule U_V.non_empty)
then obtain x where x: "x \<in> U" by blast
- hence "x \<in> V" .. hence "0 = x - x" by simp
- also from `vectorspace V` x x have "... \<in> U" by (rule U_V.diff_closed)
+ then have "x \<in> V" .. then have "0 = x - x" by simp
+ also from `vectorspace V` x x have "\<dots> \<in> U" by (rule U_V.diff_closed)
finally show ?thesis .
qed
lemma (in subspace) neg_closed [iff]:
assumes "vectorspace V"
- shows "x \<in> U \<Longrightarrow> - x \<in> U" (is "PROP ?P")
+ assumes x: "x \<in> U"
+ shows "- x \<in> U"
proof -
interpret vectorspace [V] by fact
- show "PROP ?P" by (simp add: negate_eq1)
+ from x show ?thesis by (simp add: negate_eq1)
qed
text {* \medskip Further derived laws: every subspace is a vector space. *}
@@ -81,7 +84,8 @@
shows "vectorspace U"
proof -
interpret vectorspace [V] by fact
- show ?thesis proof
+ show ?thesis
+ proof
show "U \<noteq> {}" ..
fix x y z assume x: "x \<in> U" and y: "y \<in> U" and z: "z \<in> U"
fix a b :: real
@@ -144,14 +148,13 @@
"lin x = {a \<cdot> x | a. True}"
lemma linI [intro]: "y = a \<cdot> x \<Longrightarrow> y \<in> lin x"
- by (unfold lin_def) blast
+ unfolding lin_def by blast
lemma linI' [iff]: "a \<cdot> x \<in> lin x"
- by (unfold lin_def) blast
+ unfolding lin_def by blast
-lemma linE [elim]:
- "x \<in> lin v \<Longrightarrow> (\<And>a::real. x = a \<cdot> v \<Longrightarrow> C) \<Longrightarrow> C"
- by (unfold lin_def) blast
+lemma linE [elim]: "x \<in> lin v \<Longrightarrow> (\<And>a::real. x = a \<cdot> v \<Longrightarrow> C) \<Longrightarrow> C"
+ unfolding lin_def by blast
text {* Every vector is contained in its linear closure. *}
@@ -159,7 +162,7 @@
lemma (in vectorspace) x_lin_x [iff]: "x \<in> V \<Longrightarrow> x \<in> lin x"
proof -
assume "x \<in> V"
- hence "x = 1 \<cdot> x" by simp
+ then have "x = 1 \<cdot> x" by simp
also have "\<dots> \<in> lin x" ..
finally show ?thesis .
qed
@@ -167,7 +170,7 @@
lemma (in vectorspace) "0_lin_x" [iff]: "x \<in> V \<Longrightarrow> 0 \<in> lin x"
proof
assume "x \<in> V"
- thus "0 = 0 \<cdot> x" by simp
+ then show "0 = 0 \<cdot> x" by simp
qed
text {* Any linear closure is a subspace. *}
@@ -176,7 +179,7 @@
"x \<in> V \<Longrightarrow> lin x \<unlhd> V"
proof
assume x: "x \<in> V"
- thus "lin x \<noteq> {}" by (auto simp add: x_lin_x)
+ then show "lin x \<noteq> {}" by (auto simp add: x_lin_x)
show "lin x \<subseteq> V"
proof
fix x' assume "x' \<in> lin x"
@@ -224,22 +227,27 @@
set of all sums of elements from @{text U} and @{text V}.
*}
-instance "fun" :: (type, type) plus ..
+instantiation "fun" :: (type, type) plus
+begin
-defs (overloaded)
- sum_def: "U + V \<equiv> {u + v | u v. u \<in> U \<and> v \<in> V}"
+definition
+ sum_def: "plus_fun U V = {u + v | u v. u \<in> U \<and> v \<in> V}" (* FIXME not fully general!? *)
+
+instance ..
+
+end
lemma sumE [elim]:
"x \<in> U + V \<Longrightarrow> (\<And>u v. x = u + v \<Longrightarrow> u \<in> U \<Longrightarrow> v \<in> V \<Longrightarrow> C) \<Longrightarrow> C"
- by (unfold sum_def) blast
+ unfolding sum_def by blast
lemma sumI [intro]:
"u \<in> U \<Longrightarrow> v \<in> V \<Longrightarrow> x = u + v \<Longrightarrow> x \<in> U + V"
- by (unfold sum_def) blast
+ unfolding sum_def by blast
lemma sumI' [intro]:
"u \<in> U \<Longrightarrow> v \<in> V \<Longrightarrow> u + v \<in> U + V"
- by (unfold sum_def) blast
+ unfolding sum_def by blast
text {* @{text U} is a subspace of @{text "U + V"}. *}
@@ -249,7 +257,8 @@
proof -
interpret vectorspace [U] by fact
interpret vectorspace [V] by fact
- show ?thesis proof
+ show ?thesis
+ proof
show "U \<noteq> {}" ..
show "U \<subseteq> U + V"
proof
@@ -259,7 +268,7 @@
with x show "x \<in> U + V" by simp
qed
fix x y assume x: "x \<in> U" and "y \<in> U"
- thus "x + y \<in> U" by simp
+ then show "x + y \<in> U" by simp
from x show "\<And>a. a \<cdot> x \<in> U" by simp
qed
qed
@@ -273,14 +282,15 @@
interpret subspace [U E] by fact
interpret vectorspace [E] by fact
interpret subspace [V E] by fact
- show ?thesis proof
+ show ?thesis
+ proof
have "0 \<in> U + V"
proof
show "0 \<in> U" using `vectorspace E` ..
show "0 \<in> V" using `vectorspace E` ..
show "(0::'a) = 0 + 0" by simp
qed
- thus "U + V \<noteq> {}" by blast
+ then show "U + V \<noteq> {}" by blast
show "U + V \<subseteq> E"
proof
fix x assume "x \<in> U + V"
@@ -299,14 +309,14 @@
and "vx + vy \<in> V"
and "x + y = (ux + uy) + (vx + vy)"
using x y by (simp_all add: add_ac)
- thus ?thesis ..
+ then show ?thesis ..
qed
fix a show "a \<cdot> x \<in> U + V"
proof -
from x obtain u v where "x = u + v" and "u \<in> U" and "v \<in> V" ..
- hence "a \<cdot> u \<in> U" and "a \<cdot> v \<in> V"
+ then have "a \<cdot> u \<in> U" and "a \<cdot> v \<in> V"
and "a \<cdot> x = (a \<cdot> u) + (a \<cdot> v)" by (simp_all add: distrib)
- thus ?thesis ..
+ then show ?thesis ..
qed
qed
qed
@@ -339,7 +349,8 @@
interpret vectorspace [E] by fact
interpret subspace [U E] by fact
interpret subspace [V E] by fact
- show ?thesis proof
+ show ?thesis
+ proof
have U: "vectorspace U" (* FIXME: use interpret *)
using `subspace U E` `vectorspace E` by (rule subspace.vectorspace)
have V: "vectorspace V"
@@ -386,7 +397,8 @@
proof -
interpret vectorspace [E] by fact
interpret subspace [H E] by fact
- show ?thesis proof
+ show ?thesis
+ proof
have c: "y1 = y2 \<and> a1 \<cdot> x' = a2 \<cdot> x'"
proof (rule decomp)
show "a1 \<cdot> x' \<in> lin x'" ..
@@ -409,7 +421,7 @@
with a and x' have "x' \<in> H" by (simp add: mult_assoc2)
with `x' \<notin> H` show ?thesis by contradiction
qed
- thus "x \<in> {0}" ..
+ then show "x \<in> {0}" ..
qed
show "{0} \<subseteq> H \<inter> lin x'"
proof -
@@ -420,7 +432,7 @@
qed
show "lin x' \<unlhd> E" using `x' \<in> E` ..
qed (rule `vectorspace E`, rule `subspace H E`, rule y1, rule y2, rule eq)
- thus "y1 = y2" ..
+ then show "y1 = y2" ..
from c have "a1 \<cdot> x' = a2 \<cdot> x'" ..
with x' show "a1 = a2" by (simp add: mult_right_cancel)
qed
@@ -441,7 +453,8 @@
proof -
interpret vectorspace [E] by fact
interpret subspace [H E] by fact
- show ?thesis proof (rule, simp_all only: split_paired_all split_conv)
+ show ?thesis
+ proof (rule, simp_all only: split_paired_all split_conv)
from t x' show "t = t + 0 \<cdot> x' \<and> t \<in> H" by simp
fix y and a assume ya: "t = y + a \<cdot> x' \<and> y \<in> H"
have "y = t \<and> a = 0"
@@ -490,10 +503,10 @@
from xp and xq show "fst p + snd p \<cdot> x' = fst q + snd q \<cdot> x'"
by simp
qed (rule `vectorspace E`, rule `subspace H E`, (rule x')+)
- thus ?thesis by (cases p, cases q) simp
+ then show ?thesis by (cases p, cases q) simp
qed
qed
- hence eq: "(SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H) = (y, a)"
+ then have eq: "(SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H) = (y, a)"
by (rule some1_equality) (simp add: x y)
with h'_def show "h' x = h y + a * xi" by (simp add: Let_def)
qed
--- a/src/HOL/Real/HahnBanach/VectorSpace.thy Tue Jul 15 16:50:09 2008 +0200
+++ b/src/HOL/Real/HahnBanach/VectorSpace.thy Tue Jul 15 19:39:37 2008 +0200
@@ -5,7 +5,9 @@
header {* Vector spaces *}
-theory VectorSpace imports Real Bounds Zorn begin
+theory VectorSpace
+imports Real Bounds Zorn
+begin
subsection {* Signature *}
@@ -71,10 +73,10 @@
"x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> x + (y + z) = y + (x + z)"
proof -
assume xyz: "x \<in> V" "y \<in> V" "z \<in> V"
- hence "x + (y + z) = (x + y) + z"
+ then have "x + (y + z) = (x + y) + z"
by (simp only: add_assoc)
- also from xyz have "... = (y + x) + z" by (simp only: add_commute)
- also from xyz have "... = y + (x + z)" by (simp only: add_assoc)
+ also from xyz have "\<dots> = (y + x) + z" by (simp only: add_commute)
+ also from xyz have "\<dots> = y + (x + z)" by (simp only: add_assoc)
finally show ?thesis .
qed
@@ -89,7 +91,7 @@
proof -
from non_empty obtain x where x: "x \<in> V" by blast
then have "0 = x - x" by (rule diff_self [symmetric])
- also from x x have "... \<in> V" by (rule diff_closed)
+ also from x x have "\<dots> \<in> V" by (rule diff_closed)
finally show ?thesis .
qed
@@ -98,7 +100,7 @@
proof -
assume x: "x \<in> V"
from this and zero have "x + 0 = 0 + x" by (rule add_commute)
- also from x have "... = x" by (rule add_zero_left)
+ also from x have "\<dots> = x" by (rule add_zero_left)
finally show ?thesis .
qed
@@ -116,11 +118,11 @@
assume x: "x \<in> V"
have " (a - b) \<cdot> x = (a + - b) \<cdot> x"
by (simp add: real_diff_def)
- also from x have "... = a \<cdot> x + (- b) \<cdot> x"
+ also from x have "\<dots> = a \<cdot> x + (- b) \<cdot> x"
by (rule add_mult_distrib2)
- also from x have "... = a \<cdot> x + - (b \<cdot> x)"
+ also from x have "\<dots> = a \<cdot> x + - (b \<cdot> x)"
by (simp add: negate_eq1 mult_assoc2)
- also from x have "... = a \<cdot> x - (b \<cdot> x)"
+ also from x have "\<dots> = a \<cdot> x - (b \<cdot> x)"
by (simp add: diff_eq1)
finally show ?thesis .
qed
@@ -137,13 +139,13 @@
proof -
assume x: "x \<in> V"
have "0 \<cdot> x = (1 - 1) \<cdot> x" by simp
- also have "... = (1 + - 1) \<cdot> x" by simp
- also from x have "... = 1 \<cdot> x + (- 1) \<cdot> x"
+ also have "\<dots> = (1 + - 1) \<cdot> x" by simp
+ also from x have "\<dots> = 1 \<cdot> x + (- 1) \<cdot> x"
by (rule add_mult_distrib2)
- also from x have "... = x + (- 1) \<cdot> x" by simp
- also from x have "... = x + - x" by (simp add: negate_eq2a)
- also from x have "... = x - x" by (simp add: diff_eq2)
- also from x have "... = 0" by simp
+ also from x have "\<dots> = x + (- 1) \<cdot> x" by simp
+ also from x have "\<dots> = x + - x" by (simp add: negate_eq2a)
+ also from x have "\<dots> = x - x" by (simp add: diff_eq2)
+ also from x have "\<dots> = 0" by simp
finally show ?thesis .
qed
@@ -151,9 +153,9 @@
"a \<cdot> 0 = (0::'a)"
proof -
have "a \<cdot> 0 = a \<cdot> (0 - (0::'a))" by simp
- also have "... = a \<cdot> 0 - a \<cdot> 0"
+ also have "\<dots> = a \<cdot> 0 - a \<cdot> 0"
by (rule diff_mult_distrib1) simp_all
- also have "... = 0" by simp
+ also have "\<dots> = 0" by simp
finally show ?thesis .
qed
@@ -165,8 +167,8 @@
"x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> - x + y = y - x"
proof -
assume xy: "x \<in> V" "y \<in> V"
- hence "- x + y = y + - x" by (simp add: add_commute)
- also from xy have "... = y - x" by (simp add: diff_eq1)
+ then have "- x + y = y + - x" by (simp add: add_commute)
+ also from xy have "\<dots> = y - x" by (simp add: diff_eq1)
finally show ?thesis .
qed
@@ -193,7 +195,7 @@
{
from x have "x = - (- x)" by (simp add: minus_minus)
also assume "- x = 0"
- also have "- ... = 0" by (rule minus_zero)
+ also have "- \<dots> = 0" by (rule minus_zero)
finally show "x = 0" .
next
assume "x = 0"
@@ -227,13 +229,13 @@
assume x: "x \<in> V" and y: "y \<in> V" and z: "z \<in> V"
{
from y have "y = 0 + y" by simp
- also from x y have "... = (- x + x) + y" by simp
- also from x y have "... = - x + (x + y)"
+ also from x y have "\<dots> = (- x + x) + y" by simp
+ also from x y have "\<dots> = - x + (x + y)"
by (simp add: add_assoc neg_closed)
also assume "x + y = x + z"
also from x z have "- x + (x + z) = - x + x + z"
by (simp add: add_assoc [symmetric] neg_closed)
- also from x z have "... = z" by simp
+ also from x z have "\<dots> = z" by simp
finally show "y = z" .
next
assume "y = z"
@@ -260,9 +262,9 @@
assume a: "a \<noteq> 0"
assume x: "x \<in> V" "x \<noteq> 0" and ax: "a \<cdot> x = 0"
from x a have "x = (inverse a * a) \<cdot> x" by simp
- also from `x \<in> V` have "... = inverse a \<cdot> (a \<cdot> x)" by (rule mult_assoc)
- also from ax have "... = inverse a \<cdot> 0" by simp
- also have "... = 0" by simp
+ also from `x \<in> V` have "\<dots> = inverse a \<cdot> (a \<cdot> x)" by (rule mult_assoc)
+ also from ax have "\<dots> = inverse a \<cdot> 0" by simp
+ also have "\<dots> = 0" by simp
finally have "x = 0" .
with `x \<noteq> 0` show "a = 0" by contradiction
qed
@@ -272,11 +274,11 @@
proof
assume x: "x \<in> V" and y: "y \<in> V" and a: "a \<noteq> 0"
from x have "x = 1 \<cdot> x" by simp
- also from a have "... = (inverse a * a) \<cdot> x" by simp
- also from x have "... = inverse a \<cdot> (a \<cdot> x)"
+ also from a have "\<dots> = (inverse a * a) \<cdot> x" by simp
+ also from x have "\<dots> = inverse a \<cdot> (a \<cdot> x)"
by (simp only: mult_assoc)
also assume "a \<cdot> x = a \<cdot> y"
- also from a y have "inverse a \<cdot> ... = y"
+ also from a y have "inverse a \<cdot> \<dots> = y"
by (simp add: mult_assoc2)
finally show "x = y" .
next
@@ -295,7 +297,7 @@
with x have "a \<cdot> x - b \<cdot> x = 0" by simp
finally have "(a - b) \<cdot> x = 0" .
with x neq have "a - b = 0" by (rule mult_zero_uniq)
- thus "a = b" by simp
+ then show "a = b" by simp
next
assume "a = b"
then show "a \<cdot> x = b \<cdot> x" by (simp only:)
@@ -308,24 +310,24 @@
assume x: "x \<in> V" and y: "y \<in> V" and z: "z \<in> V"
{
assume "x = z - y"
- hence "x + y = z - y + y" by simp
- also from y z have "... = z + - y + y"
+ then have "x + y = z - y + y" by simp
+ also from y z have "\<dots> = z + - y + y"
by (simp add: diff_eq1)
- also have "... = z + (- y + y)"
+ also have "\<dots> = z + (- y + y)"
by (rule add_assoc) (simp_all add: y z)
- also from y z have "... = z + 0"
+ also from y z have "\<dots> = z + 0"
by (simp only: add_minus_left)
- also from z have "... = z"
+ also from z have "\<dots> = z"
by (simp only: add_zero_right)
finally show "x + y = z" .
next
assume "x + y = z"
- hence "z - y = (x + y) - y" by simp
- also from x y have "... = x + y + - y"
+ then have "z - y = (x + y) - y" by simp
+ also from x y have "\<dots> = x + y + - y"
by (simp add: diff_eq1)
- also have "... = x + (y + - y)"
+ also have "\<dots> = x + (y + - y)"
by (rule add_assoc) (simp_all add: x y)
- also from x y have "... = x" by simp
+ also from x y have "\<dots> = x" by simp
finally show "x = z - y" ..
}
qed
@@ -335,7 +337,7 @@
proof -
assume x: "x \<in> V" and y: "y \<in> V"
from x y have "x = (- y + y) + x" by simp
- also from x y have "... = - y + (x + y)" by (simp add: add_ac)
+ also from x y have "\<dots> = - y + (x + y)" by (simp add: add_ac)
also assume "x + y = 0"
also from y have "- y + 0 = - y" by simp
finally show "x = - y" .
@@ -360,13 +362,13 @@
and eq: "a + b = c + d"
then have "- c + (a + b) = - c + (c + d)"
by (simp add: add_left_cancel)
- also have "... = d" using `c \<in> V` `d \<in> V` by (rule minus_add_cancel)
+ also have "\<dots> = d" using `c \<in> V` `d \<in> V` by (rule minus_add_cancel)
finally have eq: "- c + (a + b) = d" .
from vs have "a - c = (- c + (a + b)) + - b"
by (simp add: add_ac diff_eq1)
- also from vs eq have "... = d + - b"
+ also from vs eq have "\<dots> = d + - b"
by (simp add: add_right_cancel)
- also from vs have "... = d - b" by (simp add: diff_eq2)
+ also from vs have "\<dots> = d - b" by (simp add: diff_eq2)
finally show "a - c = d - b" .
qed
@@ -377,7 +379,7 @@
assume vs: "x \<in> V" "y \<in> V" "z \<in> V" "u \<in> V"
{
from vs have "x + z = - y + y + (x + z)" by simp
- also have "... = - y + (y + (x + z))"
+ also have "\<dots> = - y + (y + (x + z))"
by (rule add_assoc) (simp_all add: vs)
also from vs have "y + (x + z) = x + (y + z)"
by (simp add: add_ac)
@@ -404,10 +406,10 @@
with vs show "x = - z" by (simp add: add_minus_eq_minus)
next
assume eq: "x = - z"
- hence "x + (y + z) = - z + (y + z)" by simp
- also have "... = y + (- z + z)"
+ then have "x + (y + z) = - z + (y + z)" by simp
+ also have "\<dots> = y + (- z + z)"
by (rule add_left_commute) (simp_all add: vs)
- also from vs have "... = y" by simp
+ also from vs have "\<dots> = y" by simp
finally show "x + (y + z) = y" .
}
qed
--- a/src/HOL/Real/HahnBanach/ZornLemma.thy Tue Jul 15 16:50:09 2008 +0200
+++ b/src/HOL/Real/HahnBanach/ZornLemma.thy Tue Jul 15 19:39:37 2008 +0200
@@ -5,7 +5,9 @@
header {* Zorn's Lemma *}
-theory ZornLemma imports Zorn begin
+theory ZornLemma
+imports Zorn
+begin
text {*
Zorn's Lemmas states: if every linear ordered subset of an ordered
@@ -23,8 +25,6 @@
and aS: "a \<in> S"
shows "\<exists>y \<in> S. \<forall>z \<in> S. y \<subseteq> z \<longrightarrow> y = z"
proof (rule Zorn_Lemma2)
- txt_raw {* \footnote{See
- \url{http://isabelle.in.tum.de/library/HOL/HOL-Complex/Zorn.html}} \isanewline *}
show "\<forall>c \<in> chain S. \<exists>y \<in> S. \<forall>z \<in> c. z \<subseteq> y"
proof
fix c assume "c \<in> chain S"
@@ -32,22 +32,22 @@
proof cases
txt {* If @{text c} is an empty chain, then every element in
- @{text S} is an upper bound of @{text c}. *}
+ @{text S} is an upper bound of @{text c}. *}
assume "c = {}"
with aS show ?thesis by fast
txt {* If @{text c} is non-empty, then @{text "\<Union>c"} is an upper
- bound of @{text c}, lying in @{text S}. *}
+ bound of @{text c}, lying in @{text S}. *}
next
- assume c: "c \<noteq> {}"
+ assume "c \<noteq> {}"
show ?thesis
proof
show "\<forall>z \<in> c. z \<subseteq> \<Union>c" by fast
show "\<Union>c \<in> S"
proof (rule r)
- from c show "\<exists>x. x \<in> c" by fast
+ from `c \<noteq> {}` show "\<exists>x. x \<in> c" by fast
show "c \<in> chain S" by fact
qed
qed