--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy Wed Jun 13 19:14:51 2007 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy Thu Jun 14 00:22:45 2007 +0200
@@ -30,7 +30,7 @@
assumes r: "\<And>x. x \<in> V \<Longrightarrow> \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>"
shows "continuous V norm f"
proof
- show "linearform V f" .
+ show "linearform V f" by fact
from r have "\<exists>c. \<forall>x\<in>V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" by blast
then show "continuous_axioms V norm f" ..
qed
@@ -138,7 +138,7 @@
note y_rep
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 show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..
+ 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)
@@ -164,7 +164,8 @@
shows "b \<le> \<parallel>f\<parallel>\<hyphen>V"
proof -
have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
- by (unfold B_def fn_norm_def) (rule fn_norm_works)
+ unfolding B_def fn_norm_def
+ using `continuous V norm f` by (rule fn_norm_works)
from this and b show ?thesis ..
qed
@@ -174,7 +175,8 @@
shows "\<parallel>f\<parallel>\<hyphen>V \<le> y"
proof -
have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
- by (unfold B_def fn_norm_def) (rule fn_norm_works)
+ unfolding B_def fn_norm_def
+ using `continuous V norm f` by (rule fn_norm_works)
from this and b show ?thesis ..
qed
@@ -188,7 +190,8 @@
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)"
- by (unfold B_def fn_norm_def) (rule fn_norm_works)
+ 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 ..
qed
@@ -210,8 +213,9 @@
also have "f 0 = 0" by rule unfold_locales
also have "\<bar>\<dots>\<bar> = 0" by simp
also have a: "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
- by (unfold B_def fn_norm_def) (rule fn_norm_ge_zero)
- have "0 \<le> norm x" ..
+ unfolding B_def fn_norm_def
+ using `continuous V norm f` by (rule fn_norm_ge_zero)
+ from x have "0 \<le> norm x" ..
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
@@ -223,8 +227,8 @@
from x show "0 \<le> \<parallel>x\<parallel>" ..
from x and neq have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<in> B V f"
by (auto simp add: B_def real_divide_def)
- then show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V"
- by (unfold B_def fn_norm_def) (rule fn_norm_ub)
+ with `continuous V norm f` show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V"
+ unfolding B_def fn_norm_def by (rule fn_norm_ub)
qed
finally show ?thesis .
qed
@@ -255,7 +259,7 @@
note b_rep
also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>"
proof (rule mult_right_mono)
- have "0 < \<parallel>x\<parallel>" ..
+ have "0 < \<parallel>x\<parallel>" using x x_neq ..
then show "0 \<le> inverse \<parallel>x\<parallel>" by simp
from ineq and x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..
qed
--- a/src/HOL/Real/HahnBanach/FunctionOrder.thy Wed Jun 13 19:14:51 2007 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy Thu Jun 14 00:22:45 2007 +0200
@@ -82,13 +82,13 @@
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 !? *)
- fix a b assume "(a, b) \<in> g"
- show "(a, SOME y. (a, y) \<in> g) \<in> g" by (rule someI2)
- show "\<exists>y. (a, y) \<in> g" ..
- show "b = (SOME y. (a, y) \<in> g)"
+ 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" ..
+ from g show "b = (SOME y. (a, y) \<in> g)"
proof (rule some_equality [symmetric])
fix y assume "(a, y) \<in> g"
- show "y = b" by (rule uniq)
+ with g show "y = b" by (rule uniq)
qed
qed
--- a/src/HOL/Real/HahnBanach/HahnBanach.thy Wed Jun 13 19:14:51 2007 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy Thu Jun 14 00:22:45 2007 +0200
@@ -62,8 +62,9 @@
proof -
def M \<equiv> "norm_pres_extensions E p F f"
hence M: "M = \<dots>" by (simp only:)
- have E: "vectorspace E" .
- have F: "vectorspace F" ..
+ note E = `vectorspace E`
+ then have F: "vectorspace F" ..
+ note FE = `F \<unlhd> E`
{
fix c assume cM: "c \<in> chain M" and ex: "\<exists>x. x \<in> c"
have "\<Union>c \<in> M"
@@ -80,9 +81,9 @@
qed
moreover from M cM a have "linearform ?H ?h"
by (rule sup_lf)
- moreover from a M cM ex have "?H \<unlhd> E"
+ moreover from a M cM ex FE E have "?H \<unlhd> E"
by (rule sup_subE)
- moreover from a M cM ex have "F \<unlhd> ?H"
+ 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)
@@ -102,14 +103,14 @@
-- {* We show that @{text M} is non-empty: *}
show "graph F f \<in> M"
proof (unfold M_def, rule norm_pres_extensionI2)
- show "linearform F f" .
- show "F \<unlhd> E" .
+ show "linearform F f" by fact
+ show "F \<unlhd> E" by fact
from F show "F \<unlhd> F" by (rule vectorspace.subspace_refl)
show "graph F f \<subseteq> graph F f" ..
- show "\<forall>x\<in>F. f x \<le> p x" .
+ show "\<forall>x\<in>F. f x \<le> p x" by fact
qed
qed
- then obtain g where gM: "g \<in> M" and "\<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x"
+ 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
g_rep: "g = graph H h"
@@ -120,7 +121,7 @@
-- {* @{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 *}
- from HE have H: "vectorspace H"
+ from HE E have H: "vectorspace H"
by (rule subspace.vectorspace)
have HE_eq: "H = E"
@@ -139,7 +140,7 @@
proof
assume "x' = 0"
with H have "x' \<in> H" by (simp only: vectorspace.zero)
- then show False by contradiction
+ with `x' \<notin> H` show False by contradiction
qed
qed
@@ -147,12 +148,12 @@
-- {* Define @{text H'} as the direct sum of @{text H} and the linear closure of @{text x'}. \skp *}
have HH': "H \<unlhd> H'"
proof (unfold H'_def)
- have "vectorspace (lin x')" ..
+ from x'E have "vectorspace (lin x')" ..
with H show "H \<unlhd> H + lin x'" ..
qed
obtain xi where
- "\<forall>y \<in> H. - p (y + x') - h y \<le> xi
+ xi: "\<forall>y \<in> H. - p (y + x') - h y \<le> xi
\<and> xi \<le> p (y + x') - h y"
-- {* Pick a real number @{text \<xi>} that fulfills certain inequations; this will *}
-- {* be used to establish that @{text h'} is a norm-preserving extension of @{text h}.
@@ -178,7 +179,7 @@
finally have "h v - h u \<le> p (v + x') + p (u + x')" .
then show "- p (u + x') - h u \<le> p (v + x') - h v" by simp
qed
- then show ?thesis ..
+ then show thesis by (blast intro: that)
qed
def h' \<equiv> "\<lambda>x. let (y, a) =
@@ -193,8 +194,8 @@
have "graph H h \<subseteq> graph H' h'"
proof (rule graph_extI)
fix t assume t: "t \<in> H"
- have "(SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H) = (t, 0)"
- by (rule decomp_H'_H)
+ from E HE t have "(SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H) = (t, 0)"
+ using `x' \<notin> H` `x' \<in> E` `x' \<noteq> 0` by (rule decomp_H'_H)
with h'_def show "h t = h' t" by (simp add: Let_def)
next
from HH' show "H \<subseteq> H'" ..
@@ -216,7 +217,7 @@
hence "(x', h' x') \<in> graph H' h'" ..
with eq have "(x', h' x') \<in> graph H h" by (simp only:)
hence "x' \<in> H" ..
- thus False by contradiction
+ with `x' \<notin> H` show False by contradiction
qed
with g_rep show ?thesis by simp
qed
@@ -226,15 +227,17 @@
proof (unfold M_def)
show "graph H' h' \<in> norm_pres_extensions E p F f"
proof (rule norm_pres_extensionI2)
- show "linearform H' h'" by (rule h'_lf)
+ show "linearform H' h'"
+ using h'_def H'_def HE linearform `x' \<notin> H` `x' \<in> E` `x' \<noteq> 0` E
+ by (rule h'_lf)
show "H' \<unlhd> E"
- proof (unfold H'_def, rule)
- show "H \<unlhd> E" .
- show "vectorspace E" .
+ unfolding H'_def
+ proof
+ show "H \<unlhd> E" by fact
+ show "vectorspace E" by fact
from x'E show "lin x' \<unlhd> E" ..
qed
- have "F \<unlhd> H" .
- from H this HH' show FH': "F \<unlhd> H'"
+ from H `F \<unlhd> H` HH' show FH': "F \<unlhd> H'"
by (rule vectorspace.subspace_trans)
show "graph F f \<subseteq> graph H' h'"
proof (rule graph_extI)
@@ -245,9 +248,12 @@
by (simp add: Let_def)
also have "(x, 0) =
(SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H)"
+ using E HE
proof (rule decomp_H'_H [symmetric])
from FH x show "x \<in> H" ..
from x' show "x' \<noteq> 0" .
+ show "x' \<notin> H" by fact
+ show "x' \<in> E" by fact
qed
also have
"(let (y, a) = (SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H)
@@ -256,14 +262,17 @@
next
from FH' show "F \<subseteq> H'" ..
qed
- show "\<forall>x \<in> H'. h' x \<le> p x" by (rule h'_norm_pres)
+ show "\<forall>x \<in> H'. h' x \<le> p x"
+ using h'_def H'_def `x' \<notin> H` `x' \<in> E` `x' \<noteq> 0` E HE
+ `seminorm E p` linearform and hp xi
+ by (rule h'_norm_pres)
qed
qed
ultimately show ?thesis ..
qed
hence "\<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 *}
- then show "H = E" by contradiction
+ with gx show "H = E" by contradiction
qed
from HE_eq and linearform have "linearform E h"
@@ -303,19 +312,24 @@
\<and> (\<forall>x \<in> F. g x = f x)
\<and> (\<forall>x \<in> E. \<bar>g x\<bar> \<le> p x)"
proof -
- 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)"
+ 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
proof (rule HahnBanach)
show "\<forall>x \<in> F. f x \<le> p x"
- by (rule abs_ineq_iff [THEN iffD1])
+ using FE E sn lf and fp by (rule abs_ineq_iff [THEN iffD1])
qed
- then obtain g where * : "linearform E g" "\<forall>x \<in> F. g x = f x"
- and "\<forall>x \<in> E. g x \<le> p x" by blast
+ 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 **
proof (rule abs_ineq_iff [THEN iffD2])
show "E \<unlhd> E" ..
qed
- with * show ?thesis by blast
+ with lg * show ?thesis by blast
qed
@@ -336,14 +350,14 @@
proof -
have E: "vectorspace E" by unfold_locales
have E_norm: "normed_vectorspace E norm" by rule unfold_locales
- have FE: "F \<unlhd> E" .
+ note FE = `F \<unlhd> E`
have F: "vectorspace F" by rule unfold_locales
- have linearform: "linearform F f" .
+ note linearform = `linearform F f`
have F_norm: "normed_vectorspace F norm"
- by (rule subspace_normed_vs)
+ using FE E_norm by (rule subspace_normed_vs)
have ge_zero: "0 \<le> \<parallel>f\<parallel>\<hyphen>F"
by (rule normed_vectorspace.fn_norm_ge_zero
- [OF F_norm (* continuous.intro*), folded B_def fn_norm_def])
+ [OF F_norm `continuous F norm f`, folded B_def fn_norm_def])
txt {* We define a function @{text p} on @{text E} as follows:
@{text "p x = \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"} *}
def p \<equiv> "\<lambda>x. \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>"
@@ -390,6 +404,7 @@
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`
show "\<bar>f x\<bar> \<le> p x"
by (unfold p_def) (rule normed_vectorspace.fn_norm_le_cong
[OF F_norm, folded B_def fn_norm_def])
@@ -452,7 +467,7 @@
show "\<forall>x \<in> F. \<bar>f x\<bar> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>"
proof
fix x assume x: "x \<in> F"
- from a have "g x = f x" ..
+ from a x have "g x = f x" ..
hence "\<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>"
@@ -465,7 +480,7 @@
using g_cont
by (rule fn_norm_ge_zero [of g, folded B_def fn_norm_def])
next
- show "continuous F norm f" .
+ show "continuous F norm f" by fact
qed
qed
with linearformE a g_cont show ?thesis by blast
--- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Wed Jun 13 19:14:51 2007 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Thu Jun 14 00:22:45 2007 +0200
@@ -96,11 +96,12 @@
includes vectorspace E
shows "linearform H' h'"
proof
+ note E = `vectorspace E`
have H': "vectorspace H'"
proof (unfold H'_def)
- have "x0 \<in> E" .
- then have "lin x0 \<unlhd> E" ..
- with HE show "vectorspace (H + lin x0)" ..
+ from `x0 \<in> E`
+ 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'"
@@ -114,7 +115,7 @@
and x2_rep: "x2 = y2 + a2 \<cdot> x0" and y2: "y2 \<in> H"
by (unfold H'_def sum_def lin_def) blast
- have ya: "y1 + y2 = y \<and> a1 + a2 = a" using _ HE _ y x0
+ have ya: "y1 + y2 = y \<and> a1 + a2 = a" using E HE _ y x0
proof (rule decomp_H') txt_raw {* \label{decomp-H-use} *}
from HE y1 y2 show "y1 + y2 \<in> H"
by (rule subspace.add_closed)
@@ -126,7 +127,7 @@
finally show "(y1 + y2) + (a1 + a2) \<cdot> x0 = y + a \<cdot> x0" .
qed
- from h'_def x1x2 _ HE y x0
+ 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"
@@ -135,10 +136,10 @@
by simp
also have "\<dots> + (a1 + a2) * xi = (h y1 + a1 * xi) + (h y2 + a2 * xi)"
by (simp add: left_distrib)
- also from h'_def x1_rep _ HE y1 x0
+ 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 _ HE y2 x0
+ 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 .
@@ -154,7 +155,7 @@
and x1_rep: "x1 = y1 + a1 \<cdot> x0" and y1: "y1 \<in> H"
by (unfold H'_def sum_def lin_def) blast
- have ya: "c \<cdot> y1 = y \<and> c * a1 = a" using _ HE _ y x0
+ 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)
@@ -166,7 +167,7 @@
finally show "c \<cdot> y1 + (c * a1) \<cdot> x0 = y + a \<cdot> x0" .
qed
- from h'_def cx1_rep _ HE y x0 have "h' (c \<cdot> x1) = h y + a * xi"
+ 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)
@@ -174,7 +175,7 @@
by simp
also have "\<dots> + (c * a1) * xi = c * (h y1 + a1 * xi)"
by (simp only: right_distrib)
- also from h'_def x1_rep _ HE y1 x0 have "h y1 + a1 * xi = h' x1"
+ 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
@@ -195,6 +196,8 @@
and a': "\<forall>y \<in> H. - p (y + x0) - h y \<le> xi \<and> xi \<le> p (y + x0) - h y"
shows "\<forall>x \<in> H'. h' x \<le> p x"
proof
+ note E = `vectorspace E`
+ note HE = `subspace H E`
fix x assume x': "x \<in> H'"
show "h' x \<le> p x"
proof -
@@ -206,7 +209,7 @@
from y have y': "y \<in> E" ..
from y have ay: "inverse a \<cdot> y \<in> H" by simp
- from h'_def x_rep _ _ y x0 have "h' x = h y + a * xi"
+ 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)"
proof (rule linorder_cases)
--- a/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy Wed Jun 13 19:14:51 2007 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy Thu Jun 14 00:22:45 2007 +0200
@@ -126,13 +126,13 @@
@{text x} and @{text y} are contained in the greater
one. \label{cases1}*}
- from cM have "graph H'' h'' \<subseteq> graph H' h' \<or> graph H' h' \<subseteq> graph H'' h''"
+ from cM c'' c' have "graph H'' h'' \<subseteq> graph H' h' \<or> graph H' h' \<subseteq> graph H'' h''"
(is "?case1 \<or> ?case2") ..
then show ?thesis
proof
assume ?case1
- have "(x, h x) \<in> graph H'' h''" .
- also have "... \<subseteq> graph H' h'" .
+ have "(x, h x) \<in> graph H'' h''" by fact
+ also have "... \<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'" ..
@@ -143,8 +143,8 @@
assume ?case2
from x_hx have "x \<in> H''" ..
moreover {
- from y_hy have "(y, h y) \<in> graph H' h'" .
- also have "\<dots> \<subseteq> graph H'' h''" .
+ have "(y, h y) \<in> graph H' h'" by (rule y_hy)
+ also have "\<dots> \<subseteq> graph H'' h''" by fact
finally have "(y, h y) \<in> graph H'' h''" .
} then have "y \<in> H''" ..
moreover from cM u and c'' have "graph H'' h'' \<subseteq> graph H h"
@@ -402,7 +402,7 @@
includes subspace H E + vectorspace E + seminorm E p + linearform H h
shows "(\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x) = (\<forall>x \<in> H. h x \<le> p x)" (is "?L = ?R")
proof
- have H: "vectorspace H" ..
+ have H: "vectorspace H" using `vectorspace E` ..
{
assume l: ?L
show ?R
@@ -419,12 +419,13 @@
fix x assume x: "x \<in> H"
show "\<And>a b :: real. - a \<le> b \<Longrightarrow> b \<le> a \<Longrightarrow> \<bar>b\<bar> \<le> a"
by arith
- have "linearform H h" .
- from this H x have "- h x = h (- x)" by (rule linearform.neg [symmetric])
+ from `linearform H h` 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 `seminorm E p` `vectorspace E`
proof (rule seminorm.minus)
from x show "x \<in> E" ..
qed
--- a/src/HOL/Real/HahnBanach/Linearform.thy Wed Jun 13 19:14:51 2007 +0200
+++ b/src/HOL/Real/HahnBanach/Linearform.thy Thu Jun 14 00:22:45 2007 +0200
@@ -36,7 +36,7 @@
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)
- also from _ y have "f (- y) = - f y" by (rule neg)
+ also have "f (- y) = - f y" using `vectorspace V` y by (rule neg)
finally show ?thesis by simp
qed
@@ -47,7 +47,7 @@
shows "f 0 = 0"
proof -
have "f 0 = f (0 - 0)" by simp
- also have "\<dots> = f 0 - f 0" by (rule diff) simp_all
+ also have "\<dots> = f 0 - f 0" using `vectorspace V` by (rule diff) simp_all
also have "\<dots> = 0" by simp
finally show ?thesis .
qed
--- a/src/HOL/Real/HahnBanach/Subspace.thy Wed Jun 13 19:14:51 2007 +0200
+++ b/src/HOL/Real/HahnBanach/Subspace.thy Thu Jun 14 00:22:45 2007 +0200
@@ -58,7 +58,7 @@
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 have "... \<in> U" by (rule U_V.diff_closed)
+ also from `vectorspace V` x x have "... \<in> U" by (rule U_V.diff_closed)
finally show ?thesis .
qed
@@ -198,8 +198,14 @@
text {* Any linear closure is a vector space. *}
lemma (in vectorspace) lin_vectorspace [intro]:
- "x \<in> V \<Longrightarrow> vectorspace (lin x)"
- by (rule subspace.vectorspace) (rule lin_subspace)
+ assumes "x \<in> V"
+ shows "vectorspace (lin x)"
+proof -
+ from `x \<in> V` have "subspace (lin x) V"
+ by (rule lin_subspace)
+ from this and `vectorspace V` show ?thesis
+ by (rule subspace.vectorspace)
+qed
subsection {* Sum of two vectorspaces *}
@@ -253,19 +259,17 @@
proof
have "0 \<in> U + V"
proof
- show "0 \<in> U" ..
- show "0 \<in> V" ..
+ 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
show "U + V \<subseteq> E"
proof
fix x assume "x \<in> U + V"
- then obtain u v where x: "x = u + v" and
- u: "u \<in> U" and v: "v \<in> V" ..
- have "U \<unlhd> E" . with u have "u \<in> E" ..
- moreover have "V \<unlhd> E" . with v have "v \<in> E" ..
- ultimately show "x \<in> E" using x by simp
+ then obtain u v where "x = u + v" and
+ "u \<in> U" and "v \<in> V" ..
+ then show "x \<in> E" by simp
qed
fix x y assume x: "x \<in> U + V" and y: "y \<in> U + V"
show "x + y \<in> U + V"
@@ -314,8 +318,10 @@
and sum: "u1 + v1 = u2 + v2"
shows "u1 = u2 \<and> v1 = v2"
proof
- have U: "vectorspace U" by (rule subspace.vectorspace)
- have V: "vectorspace V" by (rule subspace.vectorspace)
+ have U: "vectorspace U"
+ using `subspace U E` `vectorspace E` by (rule subspace.vectorspace)
+ have V: "vectorspace V"
+ using `subspace V E` `vectorspace E` by (rule subspace.vectorspace)
from u1 u2 v1 v2 and sum have eq: "u1 - u2 = v2 - v1"
by (simp add: add_diff_swap)
from u1 u2 have u: "u1 - u2 \<in> U"
@@ -327,15 +333,15 @@
show "u1 = u2"
proof (rule add_minus_eq)
- show "u1 \<in> E" ..
- show "u2 \<in> E" ..
- from u u' and direct show "u1 - u2 = 0" by force
+ from u1 show "u1 \<in> E" ..
+ from u2 show "u2 \<in> E" ..
+ from u u' and direct show "u1 - u2 = 0" by blast
qed
show "v1 = v2"
proof (rule add_minus_eq [symmetric])
- show "v1 \<in> E" ..
- show "v2 \<in> E" ..
- from v v' and direct show "v2 - v1 = 0" by force
+ from v1 show "v1 \<in> E" ..
+ from v2 show "v2 \<in> E" ..
+ from v v' and direct show "v2 - v1 = 0" by blast
qed
qed
@@ -375,19 +381,19 @@
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)
- thus ?thesis by contradiction
+ with `x' \<notin> H` show ?thesis by contradiction
qed
thus "x \<in> {0}" ..
qed
show "{0} \<subseteq> H \<inter> lin x'"
proof -
- have "0 \<in> H" ..
- moreover have "0 \<in> lin x'" ..
+ have "0 \<in> H" using `vectorspace E` ..
+ moreover have "0 \<in> lin x'" using `x' \<in> E` ..
ultimately show ?thesis by blast
qed
qed
- show "lin x' \<unlhd> E" ..
- 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" ..
from c have "a1 \<cdot> x' = a2 \<cdot> x'" ..
with x' show "a1 = a2" by (simp add: mult_right_cancel)
@@ -412,7 +418,7 @@
proof (rule decomp_H')
from ya x' show "y + a \<cdot> x' = t + 0 \<cdot> x'" by simp
from ya show "y \<in> H" ..
- qed
+ qed (rule `vectorspace E`, rule `subspace H E`, rule t, (rule x')+)
with t x' show "(y, a) = (y + a \<cdot> x', 0)" by simp
qed
@@ -450,7 +456,7 @@
from xq show "fst q \<in> H" ..
from xp and xq show "fst p + snd p \<cdot> x' = fst q + snd q \<cdot> x'"
by simp
- qed
+ qed (rule `vectorspace E`, rule `subspace H E`, (rule x')+)
thus ?thesis by (cases p, cases q) simp
qed
qed
--- a/src/HOL/Real/HahnBanach/VectorSpace.thy Wed Jun 13 19:14:51 2007 +0200
+++ b/src/HOL/Real/HahnBanach/VectorSpace.thy Thu Jun 14 00:22:45 2007 +0200
@@ -89,7 +89,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 have "... \<in> V" by (rule diff_closed)
+ also from x x have "... \<in> V" by (rule diff_closed)
finally show ?thesis .
qed
@@ -116,7 +116,7 @@
assume x: "x \<in> V"
have " (a - b) \<cdot> x = (a + - b) \<cdot> x"
by (simp add: real_diff_def)
- also have "... = a \<cdot> x + (- b) \<cdot> x"
+ also from x have "... = a \<cdot> x + (- b) \<cdot> x"
by (rule add_mult_distrib2)
also from x have "... = a \<cdot> x + - (b \<cdot> x)"
by (simp add: negate_eq1 mult_assoc2)
@@ -138,7 +138,7 @@
assume x: "x \<in> V"
have "0 \<cdot> x = (1 - 1) \<cdot> x" by simp
also have "... = (1 + - 1) \<cdot> x" by simp
- also have "... = 1 \<cdot> x + (- 1) \<cdot> x"
+ also from x have "... = 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)
@@ -260,11 +260,11 @@
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 have "... = inverse a \<cdot> (a \<cdot> x)" by (rule mult_assoc)
+ 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
finally have "x = 0" .
- thus "a = 0" by contradiction
+ with `x \<noteq> 0` show "a = 0" by contradiction
qed
lemma (in vectorspace) mult_left_cancel:
@@ -360,7 +360,7 @@
and eq: "a + b = c + d"
then have "- c + (a + b) = - c + (c + d)"
by (simp add: add_left_cancel)
- also have "... = d" by (rule minus_add_cancel)
+ also have "... = 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)
--- a/src/HOL/Real/HahnBanach/ZornLemma.thy Wed Jun 13 19:14:51 2007 +0200
+++ b/src/HOL/Real/HahnBanach/ZornLemma.thy Thu Jun 14 00:22:45 2007 +0200
@@ -48,6 +48,7 @@
show "\<Union>c \<in> S"
proof (rule r)
from c show "\<exists>x. x \<in> c" by fast
+ show "c \<in> chain S" by fact
qed
qed
qed