- xsymbols for
\<noteq> \<notin> \<in> \<exists> \<forall>
\<and> \<inter> \<union> \<Union>
- vector space type of {plus, minus, zero}, overload 0 in vector space
- syntax |.| and ||.||
--- a/src/HOL/Real/HahnBanach/Aux.thy Sun Jul 16 21:00:32 2000 +0200
+++ b/src/HOL/Real/HahnBanach/Aux.thy Mon Jul 17 13:58:18 2000 +0200
@@ -17,22 +17,22 @@
text_raw {* \medskip *}
text{* Lemmas about sets. *}
-lemma Int_singletonD: "[| A Int B = {v}; x:A; x:B |] ==> x = v"
+lemma Int_singletonD: "[| A \<inter> B = {v}; x \<in> A; x \<in> B |] ==> x = v"
by (fast elim: equalityE)
-lemma set_less_imp_diff_not_empty: "H < E ==> EX x0:E. x0 ~: H"
+lemma set_less_imp_diff_not_empty: "H < E ==> \<exists>x0 \<in> E. x0 \<notin> H"
by (force simp add: psubset_eq)
text_raw {* \medskip *}
text{* Some lemmas about orders. *}
-lemma lt_imp_not_eq: "x < (y::'a::order) ==> x ~= y"
+lemma lt_imp_not_eq: "x < (y::'a::order) ==> x \<noteq> y"
by (rule order_less_le[RS iffD1, RS conjunct2])
lemma le_noteq_imp_less:
- "[| x <= (r::'a::order); x ~= r |] ==> x < r"
+ "[| x <= (r::'a::order); x \<noteq> r |] ==> x < r"
proof -
- assume "x <= (r::'a::order)" and ne:"x ~= r"
+ assume "x <= r" and ne:"x \<noteq> r"
hence "x < r | x = r" by (simp add: order_le_less)
with ne show ?thesis by simp
qed
@@ -116,10 +116,10 @@
thus ?thesis; by simp;
qed;
-lemma real_mult_inv_right1: "x ~= #0 ==> x*rinv(x) = #1"
+lemma real_mult_inv_right1: "x \<noteq> #0 ==> x*rinv(x) = #1"
by simp
-lemma real_mult_inv_left1: "x ~= #0 ==> rinv(x)*x = #1"
+lemma real_mult_inv_left1: "x \<noteq> #0 ==> rinv(x) * x = #1"
by simp
lemma real_le_mult_order1a:
--- a/src/HOL/Real/HahnBanach/Bounds.thy Sun Jul 16 21:00:32 2000 +0200
+++ b/src/HOL/Real/HahnBanach/Bounds.thy Mon Jul 17 13:58:18 2000 +0200
@@ -11,13 +11,13 @@
constdefs
is_LowerBound :: "('a::order) set => 'a set => 'a => bool"
- "is_LowerBound A B == \<lambda>x. x:A & (ALL y:B. x <= y)"
+ "is_LowerBound A B == \<lambda>x. x \<in> A \<and> (\<forall>y \<in> B. x <= y)"
LowerBounds :: "('a::order) set => 'a set => 'a set"
"LowerBounds A B == Collect (is_LowerBound A B)"
is_UpperBound :: "('a::order) set => 'a set => 'a => bool"
- "is_UpperBound A B == \<lambda>x. x:A & (ALL y:B. y <= x)"
+ "is_UpperBound A B == \<lambda>x. x \<in> A \<and> (\<forall> y \<in> B. y <= x)"
UpperBounds :: "('a::order) set => 'a set => 'a set"
"UpperBounds A B == Collect (is_UpperBound A B)"
@@ -70,7 +70,7 @@
text {*
A supremum\footnote{The definition of the supremum is based on one in
\url{http://isabelle.in.tum.de/library/HOL/HOL-Real/Lubs.html}} of
- an ordered set $B$ w.~r.~t.~$A$ is defined as a least upper bound of
+ an ordered set $B$ w.~r.~.~ $A$ is defined as a least upper bound of
$B$, which lies in $A$.
*}
@@ -86,7 +86,7 @@
(*<*)
constdefs
is_Inf :: "('a::order) set => 'a set => 'a => bool"
- "is_Inf A B x == x:A & is_Greatest (LowerBounds A B) x"
+ "is_Inf A B x == x \<in> A \<and> is_Greatest (LowerBounds A B) x"
Inf :: "('a::order) set => 'a set => 'a"
"Inf A B == Eps (is_Inf A B)"
@@ -115,16 +115,16 @@
text {* The supremum $B$ is an upper bound for $B$. *}
-lemma sup_ub: "y:B ==> is_Sup A B s ==> y <= s"
+lemma sup_ub: "y \<in> B ==> is_Sup A B s ==> y <= s"
by (unfold is_Sup_def, rule isLubD2)
text{* The supremum of a non-empty set $B$ is greater
than a lower bound of $B$. *}
lemma sup_ub1:
- "[| ALL y:B. a <= y; is_Sup A B s; x:B |] ==> a <= s"
+ "[| \<forall> y \<in> B. a <= y; is_Sup A B s; x \<in> B |] ==> a <= s"
proof -
- assume "ALL y:B. a <= y" "is_Sup A B s" "x:B"
+ assume "\<forall> y \<in> B. a <= y" "is_Sup A B s" "x \<in> B"
have "a <= x" by (rule bspec)
also have "x <= s" by (rule sup_ub)
finally show "a <= s" .
--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy Sun Jul 16 21:00:32 2000 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy Mon Jul 17 13:58:18 2000 +0200
@@ -18,16 +18,16 @@
constdefs
is_continuous ::
- "['a::{minus, plus} set, 'a => real, 'a => real] => bool"
+ "['a::{plus, minus, zero} set, 'a => real, 'a => real] => bool"
"is_continuous V norm f ==
- is_linearform V f & (EX c. ALL x:V. abs (f x) <= c * norm x)"
+ is_linearform V f \<and> (\<exists>c. \<forall>x \<in> V. |f x| <= c * norm x)"
lemma continuousI [intro]:
- "[| is_linearform V f; !! x. x:V ==> abs (f x) <= c * norm x |]
+ "[| is_linearform V f; !! x. x \<in> V ==> |f x| <= c * norm x |]
==> is_continuous V norm f"
proof (unfold is_continuous_def, intro exI conjI ballI)
- assume r: "!! x. x:V ==> abs (f x) <= c * norm x"
- fix x assume "x:V" show "abs (f x) <= c * norm x" by (rule r)
+ assume r: "!! x. x \<in> V ==> |f x| <= c * norm x"
+ fix x assume "x \<in> V" show "|f x| <= c * norm x" by (rule r)
qed
lemma continuous_linearform [intro??]:
@@ -36,7 +36,7 @@
lemma continuous_bounded [intro??]:
"is_continuous V norm f
- ==> EX c. ALL x:V. abs (f x) <= c * norm x"
+ ==> \<exists>c. \<forall>x \<in> V. |f x| <= c * norm x"
by (unfold is_continuous_def) force
subsection{* The norm of a linear form *}
@@ -59,14 +59,14 @@
Thus we define the set $B$ the supremum is taken from as
\[
-\{ 0 \} \Un \left\{ \frac{|f\ap x|}{\norm x} \dt x\neq \zero \And x\in F\right\}
+\{ 0 \} \Union \left\{ \frac{|f\ap x|}{\norm x} \dt x\neq \zero \And x\in F\right\}
\]
*}
constdefs
- B :: "[ 'a set, 'a => real, 'a => real ] => real set"
+ B :: "[ 'a set, 'a => real, 'a::{plus, minus, zero} => real ] => real set"
"B V norm f ==
- {#0} Un {abs (f x) * rinv (norm x) | x. x ~= 00 & x:V}"
+ {#0} \<union> {|f x| * rinv (norm x) | x. x \<noteq> 0 \<and> x \<in> V}"
text{* $n$ is the function norm of $f$, iff
$n$ is the supremum of $B$.
@@ -74,17 +74,20 @@
constdefs
is_function_norm ::
- " ['a set, 'a => real, 'a => real] => real => bool"
- "is_function_norm V norm f fn == is_Sup UNIV (B V norm f) fn"
+ " ['a::{minus,plus,zero} => real, 'a set, 'a => real] => real => bool"
+ "is_function_norm f V norm fn == is_Sup UNIV (B V norm f) fn"
text{* $\idt{function{\dsh}norm}$ is equal to the supremum of $B$,
if the supremum exists. Otherwise it is undefined. *}
constdefs
- function_norm :: " ['a set, 'a => real, 'a => real] => real"
- "function_norm V norm f == Sup UNIV (B V norm f)"
+ function_norm :: " ['a::{minus,plus,zero} => real, 'a set, 'a => real] => real"
+ "function_norm f V norm == Sup UNIV (B V norm f)"
-lemma B_not_empty: "#0 : B V norm f"
+syntax
+ function_norm :: " ['a => real, 'a set, 'a => real] => real" ("\<parallel>_\<parallel>_,_")
+
+lemma B_not_empty: "#0 \<in> B V norm f"
by (unfold B_def, force)
text {* The following lemma states that every continuous linear form
@@ -92,35 +95,35 @@
lemma ex_fnorm [intro??]:
"[| is_normed_vectorspace V norm; is_continuous V norm f|]
- ==> is_function_norm V norm f (function_norm V norm f)"
+ ==> is_function_norm f V norm \<parallel>f\<parallel>V,norm"
proof (unfold function_norm_def is_function_norm_def
is_continuous_def Sup_def, elim conjE, rule selectI2EX)
assume "is_normed_vectorspace V norm"
assume "is_linearform V f"
- and e: "EX c. ALL x:V. abs (f x) <= c * norm x"
+ and e: "\<exists>c. \<forall>x \<in> V. |f x| <= c * norm x"
txt {* The existence of the supremum is shown using the
completeness of the reals. Completeness means, that
every non-empty bounded set of reals has a
supremum. *}
- show "EX a. is_Sup UNIV (B V norm f) a"
+ show "\<exists>a. is_Sup UNIV (B V norm f) a"
proof (unfold is_Sup_def, rule reals_complete)
txt {* First we have to show that $B$ is non-empty: *}
- show "EX X. X : B V norm f"
+ show "\<exists>X. X \<in> B V norm f"
proof (intro exI)
- show "#0 : (B V norm f)" by (unfold B_def, force)
+ show "#0 \<in> (B V norm f)" by (unfold B_def, force)
qed
txt {* Then we have to show that $B$ is bounded: *}
- from e show "EX Y. isUb UNIV (B V norm f) Y"
+ from e show "\<exists>Y. isUb UNIV (B V norm f) Y"
proof
txt {* We know that $f$ is bounded by some value $c$. *}
- fix c assume a: "ALL x:V. abs (f x) <= c * norm x"
+ fix c assume a: "\<forall>x \<in> V. |f x| <= c * norm x"
def b == "max c #0"
show "?thesis"
@@ -141,7 +144,7 @@
next
fix x y
- assume "x:V" "x ~= 00" (***
+ assume "x \<in> V" "x \<noteq> 0" (***
have ge: "#0 <= rinv (norm x)";
by (rule real_less_imp_le, rule real_rinv_gt_zero,
@@ -152,11 +155,11 @@
show "#0 < norm x"; ..;
qed;
qed; *** )
- have nz: "norm x ~= #0"
+ have nz: "norm x \<noteq> #0"
by (rule not_sym, rule lt_imp_not_eq,
rule normed_vs_norm_gt_zero) (***
proof (rule not_sym);
- show "#0 ~= norm x";
+ show "#0 \<noteq> norm x";
proof (rule lt_imp_not_eq);
show "#0 < norm x"; ..;
qed;
@@ -165,19 +168,19 @@
txt {* The thesis follows by a short calculation using the
fact that $f$ is bounded. *}
- assume "y = abs (f x) * rinv (norm x)"
+ assume "y = |f x| * rinv (norm x)"
also have "... <= c * norm x * rinv (norm x)"
proof (rule real_mult_le_le_mono2)
show "#0 <= rinv (norm x)"
by (rule real_less_imp_le, rule real_rinv_gt_zero1,
rule normed_vs_norm_gt_zero)
- from a show "abs (f x) <= c * norm x" ..
+ from a show "|f x| <= c * norm x" ..
qed
also have "... = c * (norm x * rinv (norm x))"
by (rule real_mult_assoc)
also have "(norm x * rinv (norm x)) = (#1::real)"
proof (rule real_mult_inv_right1)
- show nz: "norm x ~= #0"
+ show nz: "norm x \<noteq> #0"
by (rule not_sym, rule lt_imp_not_eq,
rule normed_vs_norm_gt_zero)
qed
@@ -191,8 +194,8 @@
text {* The norm of a continuous function is always $\geq 0$. *}
lemma fnorm_ge_zero [intro??]:
- "[| is_continuous V norm f; is_normed_vectorspace V norm|]
- ==> #0 <= function_norm V norm f"
+ "[| is_continuous V norm f; is_normed_vectorspace V norm |]
+ ==> #0 <= \<parallel>f\<parallel>V,norm"
proof -
assume c: "is_continuous V norm f"
and n: "is_normed_vectorspace V norm"
@@ -203,14 +206,14 @@
show ?thesis
proof (unfold function_norm_def, rule sup_ub1)
- show "ALL x:(B V norm f). #0 <= x"
+ show "\<forall>x \<in> (B V norm f). #0 <= x"
proof (intro ballI, unfold B_def,
elim UnE singletonE CollectE exE conjE)
fix x r
- assume "x : V" "x ~= 00"
- and r: "r = abs (f x) * rinv (norm x)"
+ assume "x \<in> V" "x \<noteq> 0"
+ and r: "r = |f x| * rinv (norm x)"
- have ge: "#0 <= abs (f x)" by (simp! only: abs_ge_zero)
+ have ge: "#0 <= |f x|" by (simp! only: abs_ge_zero)
have "#0 <= rinv (norm x)"
by (rule real_less_imp_le, rule real_rinv_gt_zero1, rule)(***
proof (rule real_less_imp_le);
@@ -225,13 +228,13 @@
txt {* Since $f$ is continuous the function norm exists: *}
- have "is_function_norm V norm f (function_norm V norm f)" ..
+ have "is_function_norm f V norm \<parallel>f\<parallel>V,norm" ..
thus "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"
by (unfold is_function_norm_def function_norm_def)
txt {* $B$ is non-empty by construction: *}
- show "#0 : B V norm f" by (rule B_not_empty)
+ show "#0 \<in> B V norm f" by (rule B_not_empty)
qed
qed
@@ -242,13 +245,12 @@
*}
lemma norm_fx_le_norm_f_norm_x:
- "[| is_normed_vectorspace V norm; x:V; is_continuous V norm f |]
- ==> abs (f x) <= function_norm V norm f * norm x"
+ "[| is_continuous V norm f; is_normed_vectorspace V norm; x \<in> V |]
+ ==> |f x| <= \<parallel>f\<parallel>V,norm * norm x"
proof -
- assume "is_normed_vectorspace V norm" "x:V"
+ assume "is_normed_vectorspace V norm" "x \<in> V"
and c: "is_continuous V norm f"
have v: "is_vectorspace V" ..
- assume "x:V"
txt{* The proof is by case analysis on $x$. *}
@@ -259,22 +261,22 @@
from the linearity of $f$: for every linear function
holds $f\ap \zero = 0$. *}
- assume "x = 00"
- have "abs (f x) = abs (f 00)" by (simp!)
- also from v continuous_linearform have "f 00 = #0" ..
+ assume "x = 0"
+ have "|f x| = |f 0|" by (simp!)
+ also from v continuous_linearform have "f 0 = #0" ..
also note abs_zero
- also have "#0 <= function_norm V norm f * norm x"
+ also have "#0 <= \<parallel>f\<parallel>V,norm * norm x"
proof (rule real_le_mult_order1a)
- show "#0 <= function_norm V norm f" ..
+ show "#0 <= \<parallel>f\<parallel>V,norm" ..
show "#0 <= norm x" ..
qed
finally
- show "abs (f x) <= function_norm V norm f * norm x" .
+ show "|f x| <= \<parallel>f\<parallel>V,norm * norm x" .
next
- assume "x ~= 00"
+ assume "x \<noteq> 0"
have n: "#0 <= norm x" ..
- have nz: "norm x ~= #0"
+ have nz: "norm x \<noteq> #0"
proof (rule lt_imp_not_eq [RS not_sym])
show "#0 < norm x" ..
qed
@@ -282,28 +284,28 @@
txt {* For the case $x\neq \zero$ we derive the following
fact from the definition of the function norm:*}
- have l: "abs (f x) * rinv (norm x) <= function_norm V norm f"
+ have l: "|f x| * rinv (norm x) <= \<parallel>f\<parallel>V,norm"
proof (unfold function_norm_def, rule sup_ub)
from ex_fnorm [OF _ c]
show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"
by (simp! add: is_function_norm_def function_norm_def)
- show "abs (f x) * rinv (norm x) : B V norm f"
+ show "|f x| * rinv (norm x) \<in> B V norm f"
by (unfold B_def, intro UnI2 CollectI exI [of _ x]
conjI, simp)
qed
txt {* The thesis now follows by a short calculation: *}
- have "abs (f x) = abs (f x) * (#1::real)" by (simp!)
- also from nz have "(#1::real) = rinv (norm x) * norm x"
+ have "|f x| = |f x| * #1" by (simp!)
+ also from nz have "#1 = rinv (norm x) * norm x"
by (rule real_mult_inv_left1 [RS sym])
also
- have "abs (f x) * ... = abs (f x) * rinv (norm x) * norm x"
- by (simp! add: real_mult_assoc [of "abs (f x)"])
- also have "... <= function_norm V norm f * norm x"
+ have "|f x| * ... = |f x| * rinv (norm x) * norm x"
+ by (simp! add: real_mult_assoc)
+ also have "... <= \<parallel>f\<parallel>V,norm * norm x"
by (rule real_mult_le_le_mono2 [OF n l])
finally
- show "abs (f x) <= function_norm V norm f * norm x" .
+ show "|f x| <= \<parallel>f\<parallel>V,norm * norm x" .
qed
qed
@@ -315,13 +317,13 @@
*}
lemma fnorm_le_ub:
- "[| is_normed_vectorspace V norm; is_continuous V norm f;
- ALL x:V. abs (f x) <= c * norm x; #0 <= c |]
- ==> function_norm V norm f <= c"
+ "[| is_continuous V norm f; is_normed_vectorspace V norm;
+ \<forall>x \<in> V. |f x| <= c * norm x; #0 <= c |]
+ ==> \<parallel>f\<parallel>V,norm <= c"
proof (unfold function_norm_def)
assume "is_normed_vectorspace V norm"
assume c: "is_continuous V norm f"
- assume fb: "ALL x:V. abs (f x) <= c * norm x"
+ assume fb: "\<forall>x \<in> V. |f x| <= c * norm x"
and "#0 <= c"
txt {* Suppose the inequation holds for some $c\geq 0$.
@@ -336,12 +338,12 @@
show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"
by (simp! add: is_function_norm_def function_norm_def)
- txt {* $c$ is an upper bound of $B$, i.~e.~every
+ txt {* $c$ is an upper bound of $B$, i.e. every
$y\in B$ is less than $c$. *}
show "isUb UNIV (B V norm f) c"
proof (intro isUbI setleI ballI)
- fix y assume "y: B V norm f"
+ fix y assume "y \<in> B V norm f"
thus le: "y <= c"
proof (unfold B_def, elim UnE CollectE exE conjE singletonE)
@@ -356,14 +358,14 @@
next
fix x
- assume "x : V" "x ~= 00"
+ assume "x \<in> V" "x \<noteq> 0"
have lz: "#0 < norm x"
by (simp! add: normed_vs_norm_gt_zero)
- have nz: "norm x ~= #0"
+ have nz: "norm x \<noteq> #0"
proof (rule not_sym)
- from lz show "#0 ~= norm x"
+ from lz show "#0 \<noteq> norm x"
by (simp! add: order_less_imp_not_eq)
qed
@@ -372,10 +374,10 @@
hence rinv_gez: "#0 <= rinv (norm x)"
by (rule real_less_imp_le)
- assume "y = abs (f x) * rinv (norm x)"
+ assume "y = |f x| * rinv (norm x)"
also from rinv_gez have "... <= c * norm x * rinv (norm x)"
proof (rule real_mult_le_le_mono2)
- show "abs (f x) <= c * norm x" by (rule bspec)
+ show "|f x| <= c * norm x" by (rule bspec)
qed
also have "... <= c" by (simp add: nz real_mult_assoc)
finally show ?thesis .
--- a/src/HOL/Real/HahnBanach/FunctionOrder.thy Sun Jul 16 21:00:32 2000 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy Mon Jul 17 13:58:18 2000 +0200
@@ -12,7 +12,7 @@
text{* We define the \emph{graph} of a (real) function $f$ with
domain $F$ as the set
\[
-\{(x, f\ap x). \ap x:F\}
+\{(x, f\ap x). \ap x \in F\}
\]
So we are modeling partial functions by specifying the domain and
the mapping function. We use the term ``function'' also for its graph.
@@ -22,18 +22,18 @@
constdefs
graph :: "['a set, 'a => real] => 'a graph "
- "graph F f == {(x, f x) | x. x:F}"
+ "graph F f == {(x, f x) | x. x \<in> F}"
-lemma graphI [intro??]: "x:F ==> (x, f x) : graph F f"
+lemma graphI [intro??]: "x \<in> F ==> (x, f x) \<in> graph F f"
by (unfold graph_def, intro CollectI exI) force
-lemma graphI2 [intro??]: "x:F ==> EX t: (graph F f). t = (x, f x)"
+lemma graphI2 [intro??]: "x \<in> F ==> \<exists>t\<in> (graph F f). t = (x, f x)"
by (unfold graph_def, force)
-lemma graphD1 [intro??]: "(x, y): graph F f ==> x:F"
+lemma graphD1 [intro??]: "(x, y) \<in> graph F f ==> x \<in> F"
by (unfold graph_def, elim CollectE exE) force
-lemma graphD2 [intro??]: "(x, y): graph H h ==> y = h x"
+lemma graphD2 [intro??]: "(x, y) \<in> graph H h ==> y = h x"
by (unfold graph_def, elim CollectE exE) force
subsection {* Functions ordered by domain extension *}
@@ -42,12 +42,12 @@
$h$ is a subset of the graph of $h'$.*}
lemma graph_extI:
- "[| !! x. x: H ==> h x = h' x; H <= H'|]
+ "[| !! x. x \<in> H ==> h x = h' x; H <= H'|]
==> graph H h <= graph H' h'"
by (unfold graph_def, force)
lemma graph_extD1 [intro??]:
- "[| graph H h <= graph H' h'; x:H |] ==> h x = h' x"
+ "[| graph H h <= graph H' h'; x \<in> H |] ==> h x = h' x"
by (unfold graph_def, force)
lemma graph_extD2 [intro??]:
@@ -61,10 +61,10 @@
constdefs
domain :: "'a graph => 'a set"
- "domain g == {x. EX y. (x, y):g}"
+ "domain g == {x. \<exists>y. (x, y) \<in> g}"
funct :: "'a graph => ('a => real)"
- "funct g == \<lambda>x. (SOME y. (x, y):g)"
+ "funct g == \<lambda>x. (SOME y. (x, y) \<in> g)"
(*text{* The equations
\begin{matharray}
@@ -78,16 +78,16 @@
if the relation induced by $g$ is unique. *}
lemma graph_domain_funct:
- "(!!x y z. (x, y):g ==> (x, z):g ==> z = y)
+ "(!!x y z. (x, y) \<in> g ==> (x, z) \<in> g ==> z = y)
==> graph (domain g) (funct g) = g"
proof (unfold domain_def funct_def graph_def, auto)
- fix a b assume "(a, b) : g"
- show "(a, SOME y. (a, y) : g) : g" by (rule selectI2)
- show "EX y. (a, y) : g" ..
- assume uniq: "!!x y z. (x, y):g ==> (x, z):g ==> z = y"
- show "b = (SOME y. (a, y) : g)"
+ fix a b assume "(a, b) \<in> g"
+ show "(a, SOME y. (a, y) \<in> g) \<in> g" by (rule selectI2)
+ show "\<exists>y. (a, y) \<in> g" ..
+ assume uniq: "!!x y z. (x, y) \<in> g ==> (x, z) \<in> g ==> z = y"
+ show "b = (SOME y. (a, y) \<in> g)"
proof (rule select_equality [RS sym])
- fix y assume "(a, y):g" show "y = b" by (rule uniq)
+ fix y assume "(a, y) \<in> g" show "y = b" by (rule uniq)
qed
qed
@@ -102,40 +102,40 @@
constdefs
norm_pres_extensions ::
- "['a::{minus, plus} set, 'a => real, 'a set, 'a => real]
+ "['a::{plus, minus, zero} set, 'a => real, 'a set, 'a => real]
=> 'a graph set"
"norm_pres_extensions E p F f
- == {g. EX H h. graph H h = g
- & is_linearform H h
- & is_subspace H E
- & is_subspace F H
- & graph F f <= graph H h
- & (ALL x:H. h x <= p x)}"
+ == {g. \<exists>H h. graph H h = g
+ \<and> is_linearform H h
+ \<and> is_subspace H E
+ \<and> is_subspace F H
+ \<and> graph F f <= graph H h
+ \<and> (\<forall>x \<in> H. h x <= p x)}"
lemma norm_pres_extension_D:
- "g : norm_pres_extensions E p F f
- ==> EX H h. graph H h = g
- & is_linearform H h
- & is_subspace H E
- & is_subspace F H
- & graph F f <= graph H h
- & (ALL x:H. h x <= p x)"
+ "g \<in> norm_pres_extensions E p F f
+ ==> \<exists>H h. graph H h = g
+ \<and> is_linearform H h
+ \<and> is_subspace H E
+ \<and> is_subspace F H
+ \<and> graph F f <= graph H h
+ \<and> (\<forall>x \<in> H. h x <= p x)"
by (unfold norm_pres_extensions_def) force
lemma norm_pres_extensionI2 [intro]:
"[| is_linearform H h; is_subspace H E; is_subspace F H;
- graph F f <= graph H h; ALL x:H. h x <= p x |]
- ==> (graph H h : norm_pres_extensions E p F f)"
+ graph F f <= graph H h; \<forall>x \<in> H. h x <= p x |]
+ ==> (graph H h \<in> norm_pres_extensions E p F f)"
by (unfold norm_pres_extensions_def) force
lemma norm_pres_extensionI [intro]:
- "EX H h. graph H h = g
- & is_linearform H h
- & is_subspace H E
- & is_subspace F H
- & graph F f <= graph H h
- & (ALL x:H. h x <= p x)
- ==> g: norm_pres_extensions E p F f"
+ "\<exists>H h. graph H h = g
+ \<and> is_linearform H h
+ \<and> is_subspace H E
+ \<and> is_subspace F H
+ \<and> graph F f <= graph H h
+ \<and> (\<forall>x \<in> H. h x <= p x)
+ ==> g\<in> norm_pres_extensions E p F f"
by (unfold norm_pres_extensions_def) force
end
\ No newline at end of file
--- a/src/HOL/Real/HahnBanach/HahnBanach.thy Sun Jul 16 21:00:32 2000 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy Mon Jul 17 13:58:18 2000 +0200
@@ -1,123 +1,182 @@
-theory HahnBanach = HahnBanachLemmas: text_raw {* \smallskip\\ *} (* from ~/Pub/TYPES99/HB/HahnBanach.thy *)
+(* Title: HOL/Real/HahnBanach/HahnBanach.thy
+ ID: $Id$
+ Author: Gertrud Bauer, TU Munich
+*)
+
+header {* The Hahn-Banach Theorem *}
+
+theory HahnBanach = HahnBanachLemmas:
+
+text {*
+ We present the proof of two different versions of the Hahn-Banach
+ Theorem, closely following \cite[\S36]{Heuser:1986}.
+*}
+
+subsection {* The Hahn-Banach Theorem for vector spaces *}
+
+text {*
+{\bf Hahn-Banach Theorem.}\quad
+ Let $F$ be a subspace of a real vector space $E$, let $p$ be a semi-norm on
+ $E$, and $f$ be a linear form defined on $F$ such that $f$ is bounded by
+ $p$, i.e. $\All {x\in F} f\ap x \leq p\ap x$. Then $f$ can be extended to
+ a linear form $h$ on $E$ such that $h$ is norm-preserving, i.e. $h$ is also
+ bounded by $p$.
+
+\bigskip
+{\bf Proof Sketch.}
+\begin{enumerate}
+\item Define $M$ as the set of norm-preserving extensions of $f$ to subspaces
+ of $E$. The linear forms in $M$ are ordered by domain extension.
+\item We show that every non-empty chain in $M$ has an upper bound in $M$.
+\item With Zorn's Lemma we conclude that there is a maximal function $g$ in
+ $M$.
+\item The domain $H$ of $g$ is the whole space $E$, as shown by classical
+ contradiction:
+\begin{itemize}
+\item Assuming $g$ is not defined on whole $E$, it can still be extended in a
+ norm-preserving way to a super-space $H'$ of $H$.
+\item Thus $g$ can not be maximal. Contradiction!
+\end{itemize}
+\end{enumerate}
+\bigskip
+*}
+
+(*
+text {* {\bf Theorem.} Let $f$ be a linear form defined on a subspace
+ $F$ of a real vector space $E$, such that $f$ is bounded by a seminorm
+ $p$.
+
+ Then $f$ can be extended to a linear form $h$ on $E$ that is again
+ bounded by $p$.
+
+ \bigskip{\bf Proof Outline.}
+ First we define the set $M$ of all norm-preserving extensions of $f$.
+ We show that every chain in $M$ has an upper bound in $M$.
+ With Zorn's lemma we can conclude that $M$ has a maximal element $g$.
+ We further show by contradiction that the domain $H$ of $g$ is the whole
+ vector space $E$.
+ If $H \neq E$, then $g$ can be extended in
+ a norm-preserving way to a greater vector space $H_0$.
+ So $g$ cannot be maximal in $M$.
+ \bigskip
+*}
+*)
theorem HahnBanach:
- "is_vectorspace E \\<Longrightarrow> is_subspace F E \\<Longrightarrow> is_seminorm E p
- \\<Longrightarrow> is_linearform F f \\<Longrightarrow> \\<forall>x \\<in> F. f x \\<le> p x
- \\<Longrightarrow> \\<exists>h. is_linearform E h \\<and> (\\<forall>x \\<in> F. h x = f x) \\<and> (\\<forall>x \\<in> E. h x \\<le> p x)"
+ "[| is_vectorspace E; is_subspace F E; is_seminorm E p;
+ is_linearform F f; \<forall>x \<in> F. f x \<le> p x |]
+ ==> \<exists>h. is_linearform E h \<and> (\<forall>x \<in> F. h x = f x) \<and> (\<forall>x \<in> E. h x \<le> p x)"
-- {* Let $E$ be a vector space, $F$ a subspace of $E$, $p$ a seminorm on $E$, *}
-- {* and $f$ a linear form on $F$ such that $f$ is bounded by $p$, *}
-- {* then $f$ can be extended to a linear form $h$ on $E$ in a norm-preserving way. \skp *}
proof -
assume "is_vectorspace E" "is_subspace F E" "is_seminorm E p"
- and "is_linearform F f" "\\<forall>x \\<in> F. f x \\<le> p x"
+ and "is_linearform F f" "\<forall>x \<in> F. f x \<le> p x"
-- {* Assume the context of the theorem. \skp *}
def M == "norm_pres_extensions E p F f"
-- {* Define $M$ as the set of all norm-preserving extensions of $F$. \skp *}
{
- fix c assume "c \\<in> chain M" "\\<exists>x. x \\<in> c"
- have "\\<Union>c \\<in> M"
- txt {* Show that every non-empty chain $c$ of $M$ has an upper bound in $M$: *}
- txt {* $\Union c$ is greater than any element of the chain $c$, so it suffices to show $\Union c \in M$. *}
+ fix c assume "c \<in> chain M" "\<exists>x. x \<in> c"
+ have "\<Union> c \<in> M"
+ -- {* Show that every non-empty chain $c$ of $M$ has an upper bound in $M$: *}
+ -- {* $\Union c$ is greater than any element of the chain $c$, so it suffices to show $\Union c \in M$. *}
proof (unfold M_def, rule norm_pres_extensionI)
- show "\\<exists> H h. graph H h = \\<Union> c
- & is_linearform H h
- & is_subspace H E
- & is_subspace F H
- & graph F f \\<subseteq> graph H h
- & (\\<forall> x \\<in> H. h x \\<le> p x)"
+ show "\<exists>H h. graph H h = \<Union> c
+ \<and> is_linearform H h
+ \<and> is_subspace H E
+ \<and> is_subspace F H
+ \<and> graph F f \<subseteq> graph H h
+ \<and> (\<forall>x \<in> H. h x \<le> p x)"
proof (intro exI conjI)
- let ?H = "domain (\\<Union> c)"
- let ?h = "funct (\\<Union> c)"
+ let ?H = "domain (\<Union> c)"
+ let ?h = "funct (\<Union> c)"
- show a: "graph ?H ?h = \\<Union> c"
+ show a: "graph ?H ?h = \<Union> c"
proof (rule graph_domain_funct)
- fix x y z assume "(x, y) \\<in> \\<Union> c" "(x, z) \\<in> \\<Union> c"
+ fix x y z assume "(x, y) \<in> \<Union> c" "(x, z) \<in> \<Union> c"
show "z = y" by (rule sup_definite)
qed
show "is_linearform ?H ?h"
by (simp! add: sup_lf a)
- show "is_subspace ?H E" thm sup_subE [OF _ _ _ a]
- by (rule sup_subE [OF _ _ _ a]) (simp !)+
- (* FIXME by (rule sup_subE, rule a) (simp!)+; *)
+ show "is_subspace ?H E"
+ by (rule sup_subE, rule a) (simp!)+
show "is_subspace F ?H"
- by (rule sup_supF [OF _ _ _ a]) (simp!)+
- (* FIXME by (rule sup_supF, rule a) (simp!)+ *)
- show "graph F f \\<subseteq> graph ?H ?h"
- by (rule sup_ext [OF _ _ _ a]) (simp!)+
- (* FIXME by (rule sup_ext, rule a) (simp!)+*)
- show "\\<forall>x \\<in> ?H. ?h x \\<le> p x"
- by (rule sup_norm_pres [OF _ _ a]) (simp!)+
- (* FIXME by (rule sup_norm_pres, rule a) (simp!)+ *)
+ by (rule sup_supF, rule a) (simp!)+
+ show "graph F f \<subseteq> graph ?H ?h"
+ by (rule sup_ext, rule a) (simp!)+
+ show "\<forall>x \<in> ?H. ?h x \<le> p x"
+ by (rule sup_norm_pres, rule a) (simp!)+
qed
qed
}
- hence "\\<exists>g \\<in> M. \\<forall>x \\<in> M. g \\<subseteq> x \\<longrightarrow> g = x"
- txt {* With Zorn's Lemma we can conclude that there is a maximal element in $M$.\skp *}
+ hence "\<exists>g \<in> M. \<forall>x \<in> M. g \<subseteq> x --> g = x"
+ -- {* With Zorn's Lemma we can conclude that there is a maximal element in $M$.\skp *}
proof (rule Zorn's_Lemma)
- txt {* We show that $M$ is non-empty: *}
- have "graph F f \\<in> norm_pres_extensions E p F f"
+ -- {* We show that $M$ is non-empty: *}
+ have "graph F f \<in> norm_pres_extensions E p F f"
proof (rule norm_pres_extensionI2)
have "is_vectorspace F" ..
thus "is_subspace F F" ..
qed (blast!)+
- thus "graph F f \\<in> M" by (simp!)
+ thus "graph F f \<in> M" by (simp!)
qed
thus ?thesis
proof
- fix g assume "g \\<in> M" "\\<forall>x \\<in> M. g \\<subseteq> x \\<longrightarrow> g = x"
+ fix g assume "g \<in> M" "\<forall>x \<in> M. g \<subseteq> x --> g = x"
-- {* We consider such a maximal element $g \in M$. \skp *}
show ?thesis
obtain H h where "graph H h = g" "is_linearform H h"
- "is_subspace H E" "is_subspace F H" "graph F f \\<subseteq> graph H h"
- "\\<forall>x \\<in> H. h x \\<le> p x"
- txt {* $g$ is a norm-preserving extension of $f$, in other words: *}
- txt {* $g$ is the graph of some linear form $h$ defined on a subspace $H$ of $E$, *}
- txt {* and $h$ is an extension of $f$ that is again bounded by $p$. \skp *}
+ "is_subspace H E" "is_subspace F H" "graph F f \<subseteq> graph H h"
+ "\<forall>x \<in> H. h x \<le> p x"
+ -- {* $g$ is a norm-preserving extension of $f$, in other words: *}
+ -- {* $g$ is the graph of some linear form $h$ defined on a subspace $H$ of $E$, *}
+ -- {* and $h$ is an extension of $f$ that is again bounded by $p$. \skp *}
proof -
- have "\\<exists> H h. graph H h = g & is_linearform H h
- & is_subspace H E & is_subspace F H
- & graph F f \\<subseteq> graph H h
- & (\\<forall>x \\<in> H. h x \\<le> p x)" by (simp! add: norm_pres_extension_D)
+ have "\<exists> H h. graph H h = g \<and> is_linearform H h
+ \<and> is_subspace H E \<and> is_subspace F H
+ \<and> graph F f \<subseteq> graph H h
+ \<and> (\<forall>x \<in> H. h x \<le> p x)" by (simp! add: norm_pres_extension_D)
thus ?thesis by (elim exE conjE) rule
qed
have h: "is_vectorspace H" ..
have "H = E"
-- {* We show that $h$ is defined on whole $E$ by classical contradiction. \skp *}
proof (rule classical)
- assume "H \\<noteq> E"
+ assume "H \<noteq> E"
-- {* Assume $h$ is not defined on whole $E$. Then show that $h$ can be extended *}
-- {* in a norm-preserving way to a function $h'$ with the graph $g'$. \skp *}
- have "\\<exists>g' \\<in> M. g \\<subseteq> g' \\<and> g \\<noteq> g'"
- obtain x' where "x' \\<in> E" "x' \\<notin> H"
- txt {* Pick $x' \in E \setminus H$. \skp *}
+ have "\<exists>g' \<in> M. g \<subseteq> g' \<and> g \<noteq> g'"
+ obtain x' where "x' \<in> E" "x' \<notin> H"
+ -- {* Pick $x' \in E \setminus H$. \skp *}
proof -
- have "\\<exists>x' \\<in> E. x' \\<notin> H"
+ have "\<exists>x' \<in> E. x' \<notin> H"
proof (rule set_less_imp_diff_not_empty)
- have "H \\<subseteq> E" ..
- thus "H \\<subset> E" ..
+ have "H \<subseteq> E" ..
+ thus "H \<subset> E" ..
qed
thus ?thesis by blast
qed
- have x': "x' \\<noteq> \<zero>"
+ have x': "x' \<noteq> 0"
proof (rule classical)
- presume "x' = \<zero>"
- with h have "x' \\<in> H" by simp
+ presume "x' = 0"
+ with h have "x' \<in> H" by simp
thus ?thesis by contradiction
qed blast
def H' == "H + lin x'"
-- {* Define $H'$ as the direct sum of $H$ and the linear closure of $x'$. \skp *}
show ?thesis
- obtain xi where "\\<forall>y \\<in> H. - p (y + x') - h y \\<le> xi
- \\<and> xi \\<le> p (y + x') - h y"
- txt {* Pick a real number $\xi$ that fulfills certain inequations; this will *}
- txt {* be used to establish that $h'$ is a norm-preserving extension of $h$. \skp *}
+ obtain xi where "\<forall>y \<in> H. - p (y + x') - h y \<le> xi
+ \<and> xi \<le> p (y + x') - h y"
+ -- {* Pick a real number $\xi$ that fulfills certain inequations; this will *}
+ -- {* be used to establish that $h'$ is a norm-preserving extension of $h$.
+ \label{ex-xi-use}\skp *}
proof -
- from h have "EX xi. ALL y:H. - p (y + x') - h y <= xi
- & xi <= p (y + x') - h y"
+ from h have "\<exists>xi. \<forall>y \<in> H. - p (y + x') - h y <= xi
+ \<and> xi <= p (y + x') - h y"
proof (rule ex_xi)
- fix u v assume "u:H" "v:H"
+ fix u v assume "u \<in> H" "v \<in> H"
from h have "h v - h u = h (v - u)"
by (simp! add: linearform_diff)
also have "... <= p (v - u)"
@@ -138,25 +197,25 @@
thus ?thesis by rule rule
qed
- def h' == "\\<lambda>x. let (y,a) = \\<epsilon>(y,a). x = y + a \<prod> x' \\<and> y \\<in> H
+ def h' == "\<lambda>x. let (y,a) = SOME (y,a). x = y + a \<cdot> x' \<and> y \<in> H
in (h y) + a * xi"
-- {* Define the extension $h'$ of $h$ to $H'$ using $\xi$. \skp *}
show ?thesis
proof
- show "g \\<subseteq> graph H' h' \\<and> g \\<noteq> graph H' h'"
- txt {* Show that $h'$ is an extension of $h$ \dots \skp *}
-proof
- show "g \\<subseteq> graph H' h'"
+ show "g \<subseteq> graph H' h' \<and> g \<noteq> graph H' h'"
+ -- {* Show that $h'$ is an extension of $h$ \dots \skp *}
+ proof
+ show "g \<subseteq> graph H' h'"
proof -
- have "graph H h \\<subseteq> graph H' h'"
+ have "graph H h \<subseteq> graph H' h'"
proof (rule graph_extI)
- fix t assume "t \\<in> H"
- have "(SOME (y, a). t = y + a \<prod> x' & y \\<in> H)
- = (t, #0)"
- by (rule decomp_H0_H [OF _ _ _ _ _ x'])
+ fix t assume "t \<in> H"
+ have "(SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H)
+ = (t, #0)"
+ by (rule decomp_H'_H) (assumption+, rule x');
thus "h t = h' t" by (simp! add: Let_def)
next
- show "H \\<subseteq> H'"
+ show "H \<subseteq> H'"
proof (rule subspace_subset)
show "is_subspace H H'"
proof (unfold H'_def, rule subspace_vs_sum1)
@@ -167,33 +226,33 @@
qed
thus ?thesis by (simp!)
qed
- show "g \\<noteq> graph H' h'"
+ show "g \<noteq> graph H' h'"
proof -
- have "graph H h \\<noteq> graph H' h'"
+ have "graph H h \<noteq> graph H' h'"
proof
assume e: "graph H h = graph H' h'"
- have "x' \\<in> H'"
+ have "x' \<in> H'"
proof (unfold H'_def, rule vs_sumI)
- show "x' = \<zero> + x'" by (simp!)
- from h show "\<zero> \\<in> H" ..
- show "x' \\<in> lin x'" by (rule x_lin_x)
+ show "x' = 0 + x'" by (simp!)
+ from h show "0 \<in> H" ..
+ show "x' \<in> lin x'" by (rule x_lin_x)
qed
- hence "(x', h' x') \\<in> graph H' h'" ..
- with e have "(x', h' x') \\<in> graph H h" by simp
- hence "x' \\<in> H" ..
+ hence "(x', h' x') \<in> graph H' h'" ..
+ with e have "(x', h' x') \<in> graph H h" by simp
+ hence "x' \<in> H" ..
thus False by contradiction
qed
thus ?thesis by (simp!)
qed
qed
- show "graph H' h' \\<in> M"
- txt {* and $h'$ is norm-preserving. \skp *}
+ show "graph H' h' \<in> M"
+ -- {* and $h'$ is norm-preserving. \skp *}
proof -
- have "graph H' h' \\<in> norm_pres_extensions E p F f"
+ have "graph H' h' \<in> norm_pres_extensions E p F f"
proof (rule norm_pres_extensionI2)
show "is_linearform H' h'"
- by (rule h0_lf [OF _ _ _ _ _ _ x']) (simp!)+
- show "is_subspace H' E"
+ by (rule h'_lf) (simp! add: x')+
+ show "is_subspace H' E"
by (unfold H'_def) (rule vs_sum_subspace [OF _ lin_subspace])
have "is_subspace F H" .
also from h lin_vs
@@ -201,49 +260,259 @@
finally (subspace_trans [OF _ h])
show f_h': "is_subspace F H'" .
- show "graph F f \\<subseteq> graph H' h'"
+ show "graph F f \<subseteq> graph H' h'"
proof (rule graph_extI)
- fix x assume "x \\<in> F"
+ fix x assume "x \<in> F"
have "f x = h x" ..
also have " ... = h x + #0 * xi" by simp
also have "... = (let (y,a) = (x, #0) in h y + a * xi)"
by (simp add: Let_def)
also have
- "(x, #0) = (SOME (y, a). x = y + a (*) x' & y \\<in> H)"
- by (rule decomp_H0_H [RS sym, OF _ _ _ _ _ x']) (simp!)+
+ "(x, #0) = (SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H)"
+ proof (rule decomp_H'_H [RS sym]) qed (simp! add: x')+
also have
- "(let (y,a) = (SOME (y,a). x = y + a (*) x' & y \\<in> H)
+ "(let (y,a) = (SOME (y,a). x = y + a \<cdot> x' \<and> y \<in> H)
in h y + a * xi)
= h' x" by (simp!)
finally show "f x = h' x" .
next
- from f_h' show "F \\<subseteq> H'" ..
+ from f_h' show "F \<subseteq> H'" ..
qed
- show "\\<forall>x \\<in> H'. h' x \\<le> p x"
- by (rule h0_norm_pres [OF _ _ _ _ x'])
+ show "\<forall>x \<in> H'. h' x \<le> p x"
+ by (rule h'_norm_pres) (assumption+, rule x')
qed
- thus "graph H' h' \\<in> M" by (simp!)
+ thus "graph H' h' \<in> M" by (simp!)
qed
qed
qed
qed
- hence "\\<not>(\\<forall>x \\<in> M. g \\<subseteq> x \\<longrightarrow> g = x)" by simp
+ hence "\<not> (\<forall>x \<in> M. g \<subseteq> x --> g = x)" by simp
-- {* So the graph $g$ of $h$ cannot be maximal. Contradiction! \skp *}
thus "H = E" by contradiction
qed
- thus "\\<exists>h. is_linearform E h \\<and> (\\<forall>x \\<in> F. h x = f x)
- \\<and> (\\<forall>x \\<in> E. h x \\<le> p x)"
+ thus "\<exists>h. is_linearform E h \<and> (\<forall>x \<in> F. h x = f x)
+ \<and> (\<forall>x \<in> E. h x \<le> p x)"
proof (intro exI conjI)
assume eq: "H = E"
from eq show "is_linearform E h" by (simp!)
- show "\\<forall>x \\<in> F. h x = f x"
+ show "\<forall>x \<in> F. h x = f x"
proof (intro ballI, rule sym)
- fix x assume "x \\<in> F" show "f x = h x " ..
+ fix x assume "x \<in> F" show "f x = h x " ..
qed
- from eq show "\\<forall>x \\<in> E. h x \\<le> p x" by (force!)
+ from eq show "\<forall>x \<in> E. h x \<le> p x" by (force!)
qed
qed
qed
-qed text_raw {* \smallskip\\ *}
+qed
+
+
+
+subsection {* Alternative formulation *}
+
+text {* The following alternative formulation of the Hahn-Banach
+Theorem\label{abs-HahnBanach} uses the fact that for a real linear form
+$f$ and a seminorm $p$ the
+following inequations are equivalent:\footnote{This was shown in lemma
+$\idt{abs{\dsh}ineq{\dsh}iff}$ (see page \pageref{abs-ineq-iff}).}
+\begin{matharray}{ll}
+\forall x\in H.\ap |h\ap x|\leq p\ap x& {\rm and}\\
+\forall x\in H.\ap h\ap x\leq p\ap x\\
+\end{matharray}
+*}
+
+theorem abs_HahnBanach:
+ "[| is_vectorspace E; is_subspace F E; is_linearform F f;
+ is_seminorm E p; \<forall>x \<in> F. |f x| <= p x |]
+ ==> \<exists>g. is_linearform E g \<and> (\<forall>x \<in> F. g x = f x)
+ \<and> (\<forall>x \<in> E. |g x| <= p x)"
+proof -
+ assume "is_vectorspace E" "is_subspace F E" "is_seminorm E p"
+ "is_linearform F f" "\<forall>x \<in> F. |f x| <= p x"
+ have "\<forall>x \<in> F. f x <= p x" by (rule abs_ineq_iff [RS iffD1])
+ hence "\<exists>g. is_linearform E g \<and> (\<forall>x \<in> F. g x = f x)
+ \<and> (\<forall>x \<in> E. g x <= p x)"
+ by (simp! only: HahnBanach)
+ thus ?thesis
+ proof (elim exE conjE)
+ fix g assume "is_linearform E g" "\<forall>x \<in> F. g x = f x"
+ "\<forall>x \<in> E. g x <= p x"
+ hence "\<forall>x \<in> E. |g x| <= p x"
+ by (simp! add: abs_ineq_iff [OF subspace_refl])
+ thus ?thesis by (intro exI conjI)
+ qed
+qed
+
+subsection {* The Hahn-Banach Theorem for normed spaces *}
+
+text {* Every continuous linear form $f$ on a subspace $F$ of a
+norm space $E$, can be extended to a continuous linear form $g$ on
+$E$ such that $\fnorm{f} = \fnorm {g}$. *}
+
+theorem norm_HahnBanach:
+ "[| is_normed_vectorspace E norm; is_subspace F E;
+ is_linearform F f; is_continuous F norm f |]
+ ==> \<exists>g. is_linearform E g
+ \<and> is_continuous E norm g
+ \<and> (\<forall>x \<in> F. g x = f x)
+ \<and> \<parallel>g\<parallel>E,norm = \<parallel>f\<parallel>F,norm"
+proof -
+ assume e_norm: "is_normed_vectorspace E norm"
+ assume f: "is_subspace F E" "is_linearform F f"
+ assume f_cont: "is_continuous F norm f"
+ have e: "is_vectorspace E" ..
+ hence f_norm: "is_normed_vectorspace F norm" ..
+
+ txt{* We define a function $p$ on $E$ as follows:
+ \begin{matharray}{l}
+ p \: x = \fnorm f \cdot \norm x\\
+ \end{matharray}
+ *}
+
+ def p == "\<lambda>x. \<parallel>f\<parallel>F,norm * norm x"
+
+ txt{* $p$ is a seminorm on $E$: *}
+
+ have q: "is_seminorm E p"
+ proof
+ fix x y a assume "x \<in> E" "y \<in> E"
+
+ txt{* $p$ is positive definite: *}
+
+ show "#0 <= p x"
+ proof (unfold p_def, rule real_le_mult_order1a) thm fnorm_ge_zero
+ from f_cont f_norm show "#0 <= \<parallel>f\<parallel>F,norm" ..
+ show "#0 <= norm x" ..
+ qed
+
+ txt{* $p$ is absolutely homogenous: *}
+
+ show "p (a \<cdot> x) = |a| * p x"
+ proof -
+ have "p (a \<cdot> x) = \<parallel>f\<parallel>F,norm * norm (a \<cdot> x)"
+ by (simp!)
+ also have "norm (a \<cdot> x) = |a| * norm x"
+ by (rule normed_vs_norm_abs_homogenous)
+ also have "\<parallel>f\<parallel>F,norm * ( |a| * norm x )
+ = |a| * (\<parallel>f\<parallel>F,norm * norm x)"
+ by (simp! only: real_mult_left_commute)
+ also have "... = |a| * p x" by (simp!)
+ finally show ?thesis .
+ qed
+
+ txt{* Furthermore, $p$ is subadditive: *}
+
+ show "p (x + y) <= p x + p y"
+ proof -
+ have "p (x + y) = \<parallel>f\<parallel>F,norm * norm (x + y)"
+ by (simp!)
+ also
+ have "... <= \<parallel>f\<parallel>F,norm * (norm x + norm y)"
+ proof (rule real_mult_le_le_mono1a)
+ from f_cont f_norm show "#0 <= \<parallel>f\<parallel>F,norm" ..
+ show "norm (x + y) <= norm x + norm y" ..
+ qed
+ also have "... = \<parallel>f\<parallel>F,norm * norm x
+ + \<parallel>f\<parallel>F,norm * norm y"
+ by (simp! only: real_add_mult_distrib2)
+ finally show ?thesis by (simp!)
+ qed
+ qed
+
+ txt{* $f$ is bounded by $p$. *}
+
+ have "\<forall>x \<in> F. |f x| <= p x"
+ proof
+ fix x assume "x \<in> F"
+ from f_norm show "|f x| <= p x"
+ by (simp! add: norm_fx_le_norm_f_norm_x)
+ qed
+
+ txt{* Using the fact that $p$ is a seminorm and
+ $f$ is bounded by $p$ we can apply the Hahn-Banach Theorem
+ for real vector spaces.
+ So $f$ can be extended in a norm-preserving way to some function
+ $g$ on the whole vector space $E$. *}
+
+ with e f q
+ have "\<exists>g. is_linearform E g \<and> (\<forall>x \<in> F. g x = f x)
+ \<and> (\<forall>x \<in> E. |g x| <= p x)"
+ by (simp! add: abs_HahnBanach)
+
+ thus ?thesis
+ proof (elim exE conjE)
+ fix g
+ assume "is_linearform E g" and a: "\<forall>x \<in> F. g x = f x"
+ and b: "\<forall>x \<in> E. |g x| <= p x"
+
+ show "\<exists>g. is_linearform E g
+ \<and> is_continuous E norm g
+ \<and> (\<forall>x \<in> F. g x = f x)
+ \<and> \<parallel>g\<parallel>E,norm = \<parallel>f\<parallel>F,norm"
+ proof (intro exI conjI)
+
+ txt{* We furthermore have to show that
+ $g$ is also continuous: *}
+
+ show g_cont: "is_continuous E norm g"
+ proof
+ fix x assume "x \<in> E"
+ with b show "|g x| <= \<parallel>f\<parallel>F,norm * norm x"
+ by (simp add: p_def)
+ qed
+
+ txt {* To complete the proof, we show that
+ $\fnorm g = \fnorm f$. \label{order_antisym} *}
+
+ show "\<parallel>g\<parallel>E,norm = \<parallel>f\<parallel>F,norm"
+ (is "?L = ?R")
+ proof (rule order_antisym)
+
+ txt{* First we show $\fnorm g \leq \fnorm f$. The function norm
+ $\fnorm g$ is defined as the smallest $c\in\bbbR$ such that
+ \begin{matharray}{l}
+ \All {x\in E} {|g\ap x| \leq c \cdot \norm x}
+ \end{matharray}
+ Furthermore holds
+ \begin{matharray}{l}
+ \All {x\in E} {|g\ap x| \leq \fnorm f \cdot \norm x}
+ \end{matharray}
+ *}
+
+ have "\<forall>x \<in> E. |g x| <= \<parallel>f\<parallel>F,norm * norm x"
+ proof
+ fix x assume "x \<in> E"
+ show "|g x| <= \<parallel>f\<parallel>F,norm * norm x"
+ by (simp!)
+ qed
+
+ with g_cont e_norm show "?L <= ?R"
+ proof (rule fnorm_le_ub)
+ from f_cont f_norm show "#0 <= \<parallel>f\<parallel>F,norm" ..
+ qed
+
+ txt{* The other direction is achieved by a similar
+ argument. *}
+
+ have "\<forall>x \<in> F. |f x| <= \<parallel>g\<parallel>E,norm * norm x"
+ proof
+ fix x assume "x \<in> F"
+ from a have "g x = f x" ..
+ hence "|f x| = |g x|" by simp
+ also from g_cont
+ have "... <= \<parallel>g\<parallel>E,norm * norm x"
+ proof (rule norm_fx_le_norm_f_norm_x)
+ show "x \<in> E" ..
+ qed
+ finally show "|f x| <= \<parallel>g\<parallel>E,norm * norm x" .
+ qed
+ thus "?R <= ?L"
+ proof (rule fnorm_le_ub [OF f_cont f_norm])
+ from g_cont show "#0 <= \<parallel>g\<parallel>E,norm" ..
+ qed
+ qed
+ qed
+ qed
+qed
+
end
\ No newline at end of file
--- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Sun Jul 16 21:00:32 2000 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Mon Jul 17 13:58:18 2000 +0200
@@ -35,51 +35,51 @@
\end{matharray} *};
lemma ex_xi:
- "[| is_vectorspace F; !! u v. [| u:F; v:F |] ==> a u <= b v |]
- ==> EX (xi::real). ALL y:F. a y <= xi & xi <= b y";
+ "[| is_vectorspace F; !! u v. [| u \<in> F; v \<in> F |] ==> a u <= b v |]
+ ==> \<exists>xi::real. \<forall>y \<in> F. a y <= xi \<and> xi <= b y";
proof -;
assume vs: "is_vectorspace F";
- assume r: "(!! u v. [| u:F; v:F |] ==> a u <= (b v::real))";
+ assume r: "(!! u v. [| u \<in> F; v \<in> F |] ==> a u <= (b v::real))";
txt {* From the completeness of the reals follows:
The set $S = \{a\: u\dt\: u\in F\}$ has a supremum, if
it is non-empty and has an upper bound. *};
- let ?S = "{a u :: real | u. u:F}";
+ let ?S = "{a u :: real | u. u \<in> F}";
- have "EX xi. isLub UNIV ?S xi";
+ have "\<exists>xi. isLub UNIV ?S xi";
proof (rule reals_complete);
txt {* The set $S$ is non-empty, since $a\ap\zero \in S$: *};
- from vs; have "a \<zero> : ?S"; by force;
- thus "EX X. X : ?S"; ..;
+ from vs; have "a 0 \<in> ?S"; by force;
+ thus "\<exists>X. X \<in> ?S"; ..;
txt {* $b\ap \zero$ is an upper bound of $S$: *};
- show "EX Y. isUb UNIV ?S Y";
+ show "\<exists>Y. isUb UNIV ?S Y";
proof;
- show "isUb UNIV ?S (b \<zero>)";
+ show "isUb UNIV ?S (b 0)";
proof (intro isUbI setleI ballI);
- show "b \<zero> : UNIV"; ..;
+ show "b 0 \<in> UNIV"; ..;
next;
txt {* Every element $y\in S$ is less than $b\ap \zero$: *};
- fix y; assume y: "y : ?S";
- from y; have "EX u:F. y = a u"; by fast;
- thus "y <= b \<zero>";
+ fix y; assume y: "y \<in> ?S";
+ from y; have "\<exists>u \<in> F. y = a u"; by fast;
+ thus "y <= b 0";
proof;
- fix u; assume "u:F";
+ fix u; assume "u \<in> F";
assume "y = a u";
- also; have "a u <= b \<zero>"; by (rule r) (simp!)+;
+ also; have "a u <= b 0"; by (rule r) (simp!)+;
finally; show ?thesis; .;
qed;
qed;
qed;
qed;
- thus "EX xi. ALL y:F. a y <= xi & xi <= b y";
+ thus "\<exists>xi. \<forall>y \<in> F. a y <= xi \<and> xi <= b y";
proof (elim exE);
fix xi; assume "isLub UNIV ?S xi";
show ?thesis;
@@ -87,7 +87,7 @@
txt {* For all $y\in F$ holds $a\ap y \leq \xi$: *};
- fix y; assume y: "y:F";
+ fix y; assume y: "y \<in> F";
show "a y <= xi";
proof (rule isUbD);
show "isUb UNIV ?S xi"; ..;
@@ -96,17 +96,17 @@
txt {* For all $y\in F$ holds $\xi\leq b\ap y$: *};
- fix y; assume "y:F";
+ fix y; assume "y \<in> F";
show "xi <= b y";
proof (intro isLub_le_isUb isUbI setleI);
- show "b y : UNIV"; ..;
- show "ALL ya : ?S. ya <= b y";
+ show "b y \<in> UNIV"; ..;
+ show "\<forall>ya \<in> ?S. ya <= b y";
proof;
- fix au; assume au: "au : ?S ";
- hence "EX u:F. au = a u"; by fast;
+ fix au; assume au: "au \<in> ?S ";
+ hence "\<exists>u \<in> F. au = a u"; by fast;
thus "au <= b y";
proof;
- fix u; assume "u:F"; assume "au = a u";
+ fix u; assume "u \<in> F"; assume "au = a u";
also; have "... <= b y"; by (rule r);
finally; show ?thesis; .;
qed;
@@ -120,63 +120,63 @@
$h_0\ap x = h\ap y + a\cdot \xi$ where $x = y + a\mult \xi$
is a linear extension of $h$ to $H_0$. *};
-lemma h0_lf:
- "[| h0 == (\\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<prod> x0 & y:H
+lemma h'_lf:
+ "[| h' == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H
in h y + a * xi);
- H0 == H + lin x0; is_subspace H E; is_linearform H h; x0 ~: H;
- x0 : E; x0 ~= \<zero>; is_vectorspace E |]
- ==> is_linearform H0 h0";
+ H' == H + lin x0; is_subspace H E; is_linearform H h; x0 \<notin> H;
+ x0 \<in> E; x0 \<noteq> 0; is_vectorspace E |]
+ ==> is_linearform H' h'";
proof -;
- assume h0_def:
- "h0 == (\\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<prod> x0 & y:H
+ assume h'_def:
+ "h' == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H
in h y + a * xi)"
- and H0_def: "H0 == H + lin x0"
- and vs: "is_subspace H E" "is_linearform H h" "x0 ~: H"
- "x0 ~= \<zero>" "x0 : E" "is_vectorspace E";
+ and H'_def: "H' == H + lin x0"
+ and vs: "is_subspace H E" "is_linearform H h" "x0 \<notin> H"
+ "x0 \<noteq> 0" "x0 \<in> E" "is_vectorspace E";
- have h0: "is_vectorspace H0";
- proof (unfold H0_def, rule vs_sum_vs);
+ have h': "is_vectorspace H'";
+ proof (unfold H'_def, rule vs_sum_vs);
show "is_subspace (lin x0) E"; ..;
qed;
show ?thesis;
proof;
- fix x1 x2; assume x1: "x1 : H0" and x2: "x2 : H0";
+ fix x1 x2; assume x1: "x1 \<in> H'" and x2: "x2 \<in> H'";
txt{* We now have to show that $h_0$ is additive, i.~e.\
$h_0 \ap (x_1\plus x_2) = h_0\ap x_1 + h_0\ap x_2$
for $x_1, x_2\in H$. *};
- have x1x2: "x1 + x2 : H0";
- by (rule vs_add_closed, rule h0);
+ have x1x2: "x1 + x2 \<in> H'";
+ by (rule vs_add_closed, rule h');
from x1;
- have ex_x1: "EX y1 a1. x1 = y1 + a1 \<prod> x0 & y1 : H";
- by (unfold H0_def vs_sum_def lin_def) fast;
+ have ex_x1: "\<exists> y1 a1. x1 = y1 + a1 \<cdot> x0 \<and> y1 \<in> H";
+ by (unfold H'_def vs_sum_def lin_def) fast;
from x2;
- have ex_x2: "EX y2 a2. x2 = y2 + a2 \<prod> x0 & y2 : H";
- by (unfold H0_def vs_sum_def lin_def) fast;
+ have ex_x2: "\<exists> y2 a2. x2 = y2 + a2 \<cdot> x0 \<and> y2 \<in> H";
+ by (unfold H'_def vs_sum_def lin_def) fast;
from x1x2;
- have ex_x1x2: "EX y a. x1 + x2 = y + a \<prod> x0 & y : H";
- by (unfold H0_def vs_sum_def lin_def) fast;
+ have ex_x1x2: "\<exists> y a. x1 + x2 = y + a \<cdot> x0 \<and> y \<in> H";
+ by (unfold H'_def vs_sum_def lin_def) fast;
from ex_x1 ex_x2 ex_x1x2;
- show "h0 (x1 + x2) = h0 x1 + h0 x2";
+ show "h' (x1 + x2) = h' x1 + h' x2";
proof (elim exE conjE);
fix y1 y2 y a1 a2 a;
- assume y1: "x1 = y1 + a1 \<prod> x0" and y1': "y1 : H"
- and y2: "x2 = y2 + a2 \<prod> x0" and y2': "y2 : H"
- and y: "x1 + x2 = y + a \<prod> x0" and y': "y : H";
+ assume y1: "x1 = y1 + a1 \<cdot> x0" and y1': "y1 \<in> H"
+ and y2: "x2 = y2 + a2 \<cdot> x0" and y2': "y2 \<in> H"
+ and y: "x1 + x2 = y + a \<cdot> x0" and y': "y \<in> H";
- have ya: "y1 + y2 = y & a1 + a2 = a";
- proof (rule decomp_H0);;
- txt_raw {* \label{decomp-H0-use} *};;
- show "y1 + y2 + (a1 + a2) \<prod> x0 = y + a \<prod> x0";
+ have ya: "y1 + y2 = y \<and> a1 + a2 = a";
+ proof (rule decomp_H');;
+ txt_raw {* \label{decomp-H-use} *};;
+ show "y1 + y2 + (a1 + a2) \<cdot> x0 = y + a \<cdot> x0";
by (simp! add: vs_add_mult_distrib2 [of E]);
- show "y1 + y2 : H"; ..;
+ show "y1 + y2 \<in> H"; ..;
qed;
- have "h0 (x1 + x2) = h y + a * xi";
- by (rule h0_definite);
+ have "h' (x1 + x2) = h y + a * xi";
+ by (rule h'_definite);
also; have "... = h (y1 + y2) + (a1 + a2) * xi";
by (simp add: ya);
also; from vs y1' y2';
@@ -185,10 +185,10 @@
real_add_mult_distrib);
also; have "... = (h y1 + a1 * xi) + (h y2 + a2 * xi)";
by simp;
- also; have "h y1 + a1 * xi = h0 x1";
- by (rule h0_definite [RS sym]);
- also; have "h y2 + a2 * xi = h0 x2";
- by (rule h0_definite [RS sym]);
+ also; have "h y1 + a1 * xi = h' x1";
+ by (rule h'_definite [RS sym]);
+ also; have "h y2 + a2 * xi = h' x2";
+ by (rule h'_definite [RS sym]);
finally; show ?thesis; .;
qed;
@@ -198,39 +198,39 @@
*};
next;
- fix c x1; assume x1: "x1 : H0";
- have ax1: "c \<prod> x1 : H0";
- by (rule vs_mult_closed, rule h0);
- from x1; have ex_x: "!! x. x: H0
- ==> EX y a. x = y + a \<prod> x0 & y : H";
- by (unfold H0_def vs_sum_def lin_def) fast;
+ fix c x1; assume x1: "x1 \<in> H'";
+ have ax1: "c \<cdot> x1 \<in> H'";
+ by (rule vs_mult_closed, rule h');
+ from x1; have ex_x: "!! x. x\<in> H'
+ ==> \<exists> y a. x = y + a \<cdot> x0 \<and> y \<in> H";
+ by (unfold H'_def vs_sum_def lin_def) fast;
- from x1; have ex_x1: "EX y1 a1. x1 = y1 + a1 \<prod> x0 & y1 : H";
- by (unfold H0_def vs_sum_def lin_def) fast;
- with ex_x [of "c \<prod> x1", OF ax1];
- show "h0 (c \<prod> x1) = c * (h0 x1)";
+ from x1; have ex_x1: "\<exists> y1 a1. x1 = y1 + a1 \<cdot> x0 \<and> y1 \<in> H";
+ by (unfold H'_def vs_sum_def lin_def) fast;
+ with ex_x [of "c \<cdot> x1", OF ax1];
+ show "h' (c \<cdot> x1) = c * (h' x1)";
proof (elim exE conjE);
fix y1 y a1 a;
- assume y1: "x1 = y1 + a1 \<prod> x0" and y1': "y1 : H"
- and y: "c \<prod> x1 = y + a \<prod> x0" and y': "y : H";
+ assume y1: "x1 = y1 + a1 \<cdot> x0" and y1': "y1 \<in> H"
+ and y: "c \<cdot> x1 = y + a \<cdot> x0" and y': "y \<in> H";
- have ya: "c \<prod> y1 = y & c * a1 = a";
- proof (rule decomp_H0);
- show "c \<prod> y1 + (c * a1) \<prod> x0 = y + a \<prod> x0";
- by (simp! add: add: vs_add_mult_distrib1);
- show "c \<prod> y1 : H"; ..;
+ have ya: "c \<cdot> y1 = y \<and> c * a1 = a";
+ proof (rule decomp_H');
+ show "c \<cdot> y1 + (c * a1) \<cdot> x0 = y + a \<cdot> x0";
+ by (simp! add: vs_add_mult_distrib1);
+ show "c \<cdot> y1 \<in> H"; ..;
qed;
- have "h0 (c \<prod> x1) = h y + a * xi";
- by (rule h0_definite);
- also; have "... = h (c \<prod> y1) + (c * a1) * xi";
+ have "h' (c \<cdot> x1) = h y + a * xi";
+ by (rule h'_definite);
+ also; have "... = h (c \<cdot> y1) + (c * a1) * xi";
by (simp add: ya);
also; from vs y1'; have "... = c * h y1 + c * a1 * xi";
by (simp add: linearform_mult [of H]);
also; from vs y1'; have "... = c * (h y1 + a1 * xi)";
by (simp add: real_add_mult_distrib2 real_mult_assoc);
- also; have "h y1 + a1 * xi = h0 x1";
- by (rule h0_definite [RS sym]);
+ also; have "h y1 + a1 * xi = h' x1";
+ by (rule h'_definite [RS sym]);
finally; show ?thesis; .;
qed;
qed;
@@ -239,40 +239,40 @@
text{* \medskip The linear extension $h_0$ of $h$
is bounded by the seminorm $p$. *};
-lemma h0_norm_pres:
- "[| h0 == (\\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<prod> x0 & y:H
+lemma h'_norm_pres:
+ "[| h' == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H
in h y + a * xi);
- H0 == H + lin x0; x0 ~: H; x0 : E; x0 ~= \<zero>; is_vectorspace E;
- is_subspace H E; is_seminorm E p; is_linearform H h; ALL y:H. h y <= p y;
- ALL y:H. - p (y + x0) - h y <= xi & xi <= p (y + x0) - h y |]
- ==> ALL x:H0. h0 x <= p x";
+ H' == H + lin x0; x0 \<notin> H; x0 \<in> E; x0 \<noteq> 0; is_vectorspace E;
+ is_subspace H E; is_seminorm E p; is_linearform H h; \<forall>y \<in> H. h y <= p y;
+ \<forall>y \<in> H. - p (y + x0) - h y <= xi \<and> xi <= p (y + x0) - h y |]
+ ==> \<forall> x \<in> H'. h' x <= p x";
proof;
- assume h0_def:
- "h0 == (\\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<prod> x0 & y:H
+ assume h'_def:
+ "h' == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H
in (h y) + a * xi)"
- and H0_def: "H0 == H + lin x0"
- and vs: "x0 ~: H" "x0 : E" "x0 ~= \<zero>" "is_vectorspace E"
+ and H'_def: "H' == H + lin x0"
+ and vs: "x0 \<notin> H" "x0 \<in> E" "x0 \<noteq> 0" "is_vectorspace E"
"is_subspace H E" "is_seminorm E p" "is_linearform H h"
- and a: "ALL y:H. h y <= p y";
- presume a1: "ALL ya:H. - p (ya + x0) - h ya <= xi";
- presume a2: "ALL ya:H. xi <= p (ya + x0) - h ya";
- fix x; assume "x : H0";
+ and a: "\<forall>y \<in> H. h y <= p y";
+ presume a1: "\<forall>ya \<in> H. - p (ya + x0) - h ya <= xi";
+ presume a2: "\<forall>ya \<in> H. xi <= p (ya + x0) - h ya";
+ fix x; assume "x \<in> H'";
have ex_x:
- "!! x. x : H0 ==> EX y a. x = y + a \<prod> x0 & y : H";
- by (unfold H0_def vs_sum_def lin_def) fast;
- have "EX y a. x = y + a \<prod> x0 & y : H";
+ "!! x. x \<in> H' ==> \<exists>y a. x = y + a \<cdot> x0 \<and> y \<in> H";
+ by (unfold H'_def vs_sum_def lin_def) fast;
+ have "\<exists>y a. x = y + a \<cdot> x0 \<and> y \<in> H";
by (rule ex_x);
- thus "h0 x <= p x";
+ thus "h' x <= p x";
proof (elim exE conjE);
- fix y a; assume x: "x = y + a \<prod> x0" and y: "y : H";
- have "h0 x = h y + a * xi";
- by (rule h0_definite);
+ fix y a; assume x: "x = y + a \<cdot> x0" and y: "y \<in> H";
+ have "h' x = h y + a * xi";
+ by (rule h'_definite);
txt{* Now we show
$h\ap y + a \cdot \xi\leq p\ap (y\plus a \mult x_0)$
by case analysis on $a$. \label{linorder_linear_split}*};
- also; have "... <= p (y + a \<prod> x0)";
+ also; have "... <= p (y + a \<cdot> x0)";
proof (rule linorder_linear_split);
assume z: "a = #0";
@@ -282,29 +282,29 @@
taken as $y/a$: *};
next;
- assume lz: "a < #0"; hence nz: "a ~= #0"; by simp;
+ assume lz: "a < #0"; hence nz: "a \<noteq> #0"; by simp;
from a1;
- have "- p (rinv a \<prod> y + x0) - h (rinv a \<prod> y) <= xi";
+ have "- p (rinv a \<cdot> y + x0) - h (rinv a \<cdot> y) <= xi";
by (rule bspec) (simp!);
txt {* The thesis for this case now follows by a short
calculation. *};
hence "a * xi
- <= a * (- p (rinv a \<prod> y + x0) - h (rinv a \<prod> y))";
+ <= a * (- p (rinv a \<cdot> y + x0) - h (rinv a \<cdot> y))";
by (rule real_mult_less_le_anti [OF lz]);
- also; have "... = - a * (p (rinv a \<prod> y + x0))
- - a * (h (rinv a \<prod> y))";
+ also; have "... = - a * (p (rinv a \<cdot> y + x0))
+ - a * (h (rinv a \<cdot> y))";
by (rule real_mult_diff_distrib);
- also; from lz vs y; have "- a * (p (rinv a \<prod> y + x0))
- = p (a \<prod> (rinv a \<prod> y + x0))";
+ also; from lz vs y; have "- a * (p (rinv a \<cdot> y + x0))
+ = p (a \<cdot> (rinv a \<cdot> y + x0))";
by (simp add: seminorm_abs_homogenous abs_minus_eqI2);
- also; from nz vs y; have "... = p (y + a \<prod> x0)";
+ also; from nz vs y; have "... = p (y + a \<cdot> x0)";
by (simp add: vs_add_mult_distrib1);
- also; from nz vs y; have "a * (h (rinv a \<prod> y)) = h y";
+ also; from nz vs y; have "a * (h (rinv a \<cdot> y)) = h y";
by (simp add: linearform_mult [RS sym]);
- finally; have "a * xi <= p (y + a \<prod> x0) - h y"; .;
+ finally; have "a * xi <= p (y + a \<cdot> x0) - h y"; .;
- hence "h y + a * xi <= h y + p (y + a \<prod> x0) - h y";
+ hence "h y + a * xi <= h y + p (y + a \<cdot> x0) - h y";
by (simp add: real_add_left_cancel_le);
thus ?thesis; by simp;
@@ -312,32 +312,32 @@
taken as $y/a$: *};
next;
- assume gz: "#0 < a"; hence nz: "a ~= #0"; by simp;
+ assume gz: "#0 < a"; hence nz: "a \<noteq> #0"; by simp;
from a2;
- have "xi <= p (rinv a \<prod> y + x0) - h (rinv a \<prod> y)";
+ have "xi <= p (rinv a \<cdot> y + x0) - h (rinv a \<cdot> y)";
by (rule bspec) (simp!);
txt {* The thesis for this case follows by a short
calculation: *};
with gz; have "a * xi
- <= a * (p (rinv a \<prod> y + x0) - h (rinv a \<prod> y))";
+ <= a * (p (rinv a \<cdot> y + x0) - h (rinv a \<cdot> y))";
by (rule real_mult_less_le_mono);
- also; have "... = a * p (rinv a \<prod> y + x0)
- - a * h (rinv a \<prod> y)";
+ also; have "... = a * p (rinv a \<cdot> y + x0)
+ - a * h (rinv a \<cdot> y)";
by (rule real_mult_diff_distrib2);
also; from gz vs y;
- have "a * p (rinv a \<prod> y + x0)
- = p (a \<prod> (rinv a \<prod> y + x0))";
+ have "a * p (rinv a \<cdot> y + x0)
+ = p (a \<cdot> (rinv a \<cdot> y + x0))";
by (simp add: seminorm_abs_homogenous abs_eqI2);
also; from nz vs y;
- have "... = p (y + a \<prod> x0)";
+ have "... = p (y + a \<cdot> x0)";
by (simp add: vs_add_mult_distrib1);
- also; from nz vs y; have "a * h (rinv a \<prod> y) = h y";
+ also; from nz vs y; have "a * h (rinv a \<cdot> y) = h y";
by (simp add: linearform_mult [RS sym]);
- finally; have "a * xi <= p (y + a \<prod> x0) - h y"; .;
+ finally; have "a * xi <= p (y + a \<cdot> x0) - h y"; .;
- hence "h y + a * xi <= h y + (p (y + a \<prod> x0) - h y)";
+ hence "h y + a * xi <= h y + (p (y + a \<cdot> x0) - h y)";
by (simp add: real_add_left_cancel_le);
thus ?thesis; by simp;
qed;
@@ -346,4 +346,4 @@
qed;
qed blast+;
-end;
\ No newline at end of file
+end;
--- a/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy Sun Jul 16 21:00:32 2000 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy Mon Jul 17 13:58:18 2000 +0200
@@ -7,8 +7,6 @@
theory HahnBanachSupLemmas = FunctionNorm + ZornLemma:
-
-
text{* This section contains some lemmas that will be used in the
proof of the Hahn-Banach Theorem.
In this section the following context is presumed.
@@ -20,7 +18,6 @@
i.e.\ the supremum of the chain $c$.
*}
-
text{* Let $c$ be a chain of norm-preserving extensions of the
function $f$ and let $\idt{graph}\ap H\ap h$ be the supremum of $c$.
Every element in $H$ is member of
@@ -28,38 +25,38 @@
lemma some_H'h't:
"[| M = norm_pres_extensions E p F f; c \<in> chain M;
- graph H h = Union c; x \\<in> H |]
- ==> \\<exists> H' h'. graph H' h' \<in> c & (x, h x) \<in> graph H' h'
- & is_linearform H' h' & is_subspace H' E
- & is_subspace F H' & graph F f \\<subseteq> graph H' h'
- & (\\<forall>x \\<in> H'. h' x \\<le> p x)"
+ graph H h = \<Union> c; x \<in> H |]
+ ==> \<exists>H' h'. graph H' h' \<in> c \<and> (x, h x) \<in> graph H' h'
+ \<and> is_linearform H' h' \<and> is_subspace H' E
+ \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h'
+ \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
proof -
assume m: "M = norm_pres_extensions E p F f" and "c \<in> chain M"
- and u: "graph H h = Union c" "x \\<in> H"
+ and u: "graph H h = \<Union> c" "x \<in> H"
have h: "(x, h x) \<in> graph H h" ..
- with u have "(x, h x) \<in> Union c" by simp
- hence ex1: "\<exists> g \\<in> c. (x, h x) \<in> g"
+ with u have "(x, h x) \<in> \<Union> c" by simp
+ hence ex1: "\<exists>g \<in> c. (x, h x) \<in> g"
by (simp only: Union_iff)
thus ?thesis
proof (elim bexE)
- fix g assume g: "g \\<in> c" "(x, h x) \\<in> g"
- have "c \\<subseteq> M" by (rule chainD2)
- hence "g \\<in> M" ..
+ fix g assume g: "g \<in> c" "(x, h x) \<in> g"
+ have "c \<subseteq> M" by (rule chainD2)
+ hence "g \<in> M" ..
hence "g \<in> norm_pres_extensions E p F f" by (simp only: m)
- hence "\<exists> H' h'. graph H' h' = g
- & is_linearform H' h'
- & is_subspace H' E
- & is_subspace F H'
- & graph F f \\<subseteq> graph H' h'
- & (\<forall>x \\<in> H'. h' x \\<le> p x)"
+ hence "\<exists>H' h'. graph H' h' = g
+ \<and> is_linearform H' h'
+ \<and> is_subspace H' E
+ \<and> is_subspace F H'
+ \<and> graph F f \<subseteq> graph H' h'
+ \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
by (rule norm_pres_extension_D)
thus ?thesis
proof (elim exE conjE)
fix H' h'
assume "graph H' h' = g" "is_linearform H' h'"
"is_subspace H' E" "is_subspace F H'"
- "graph F f \\<subseteq> graph H' h'" "\<forall>x \\<in> H'. h' x \\<le> p x"
+ "graph F f \<subseteq> graph H' h'" "\<forall>x \<in> H'. h' x \<le> p x"
show ?thesis
proof (intro exI conjI)
show "graph H' h' \<in> c" by (simp!)
@@ -78,28 +75,28 @@
lemma some_H'h':
"[| M = norm_pres_extensions E p F f; c \<in> chain M;
- graph H h = Union c; x \\<in> H |]
- ==> \<exists> H' h'. x \\<in> H' & graph H' h' \\<subseteq> graph H h
- & is_linearform H' h' & is_subspace H' E & is_subspace F H'
- & graph F f \\<subseteq> graph H' h' & (\<forall>x \\<in> H'. h' x \\<le> p x)"
+ graph H h = \<Union> c; x \<in> H |]
+ ==> \<exists>H' h'. x \<in> H' \<and> graph H' h' \<subseteq> graph H h
+ \<and> is_linearform H' h' \<and> is_subspace H' E \<and> is_subspace F H'
+ \<and> graph F f \<subseteq> graph H' h' \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
proof -
assume "M = norm_pres_extensions E p F f" and cM: "c \<in> chain M"
- and u: "graph H h = Union c" "x \\<in> H"
+ and u: "graph H h = \<Union> c" "x \<in> H"
- have "\<exists> H' h'. graph H' h' \<in> c & (x, h x) \<in> graph H' h'
- & is_linearform H' h' & is_subspace H' E
- & is_subspace F H' & graph F f \\<subseteq> graph H' h'
- & (\<forall> x \\<in> H'. h' x \\<le> p x)"
+ have "\<exists>H' h'. graph H' h' \<in> c \<and> (x, h x) \<in> graph H' h'
+ \<and> is_linearform H' h' \<and> is_subspace H' E
+ \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h'
+ \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
by (rule some_H'h't)
thus ?thesis
proof (elim exE conjE)
fix H' h' assume "(x, h x) \<in> graph H' h'" "graph H' h' \<in> c"
"is_linearform H' h'" "is_subspace H' E" "is_subspace F H'"
- "graph F f \\<subseteq> graph H' h'" "\<forall> x\<in>H'. h' x \\<le> p x"
+ "graph F f \<subseteq> graph H' h'" "\<forall>x \<in> H'. h' x \<le> p x"
show ?thesis
proof (intro exI conjI)
- show "x\<in>H'" by (rule graphD1)
- from cM u show "graph H' h' \\<subseteq> graph H h"
+ show "x \<in> H'" by (rule graphD1)
+ from cM u show "graph H' h' \<subseteq> graph H h"
by (simp! only: chain_ball_Union_upper)
qed
qed
@@ -111,48 +108,48 @@
$h'$, such that $h$ extends $h'$. *}
lemma some_H'h'2:
- "[| M = norm_pres_extensions E p F f; c\<in> chain M;
- graph H h = Union c; x\<in>H; y\<in>H |]
- ==> \<exists> H' h'. x\<in>H' & y\<in>H' & graph H' h' \\<subseteq> graph H h
- & is_linearform H' h' & is_subspace H' E & is_subspace F H'
- & graph F f \\<subseteq> graph H' h' & (\<forall> x\<in>H'. h' x \\<le> p x)"
+ "[| M = norm_pres_extensions E p F f; c \<in> chain M;
+ graph H h = \<Union> c; x \<in> H; y \<in> H |]
+ ==> \<exists>H' h'. x \<in> H' \<and> y \<in> H' \<and> graph H' h' \<subseteq> graph H h
+ \<and> is_linearform H' h' \<and> is_subspace H' E \<and> is_subspace F H'
+ \<and> graph F f \<subseteq> graph H' h' \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
proof -
- assume "M = norm_pres_extensions E p F f" "c\<in> chain M"
- "graph H h = Union c" "x\<in>H" "y\<in>H"
+ assume "M = norm_pres_extensions E p F f" "c \<in> chain M"
+ "graph H h = \<Union> c" "x \<in> H" "y \<in> H"
txt {* $x$ is in the domain $H'$ of some function $h'$,
such that $h$ extends $h'$. *}
- have e1: "\<exists> H' h'. graph H' h' \<in> c & (x, h x) \<in> graph H' h'
- & is_linearform H' h' & is_subspace H' E
- & is_subspace F H' & graph F f \\<subseteq> graph H' h'
- & (\<forall> x\<in>H'. h' x \\<le> p x)"
+ have e1: "\<exists>H' h'. graph H' h' \<in> c \<and> (x, h x) \<in> graph H' h'
+ \<and> is_linearform H' h' \<and> is_subspace H' E
+ \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h'
+ \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
by (rule some_H'h't)
txt {* $y$ is in the domain $H''$ of some function $h''$,
such that $h$ extends $h''$. *}
- have e2: "\<exists> H'' h''. graph H'' h'' \<in> c & (y, h y) \<in> graph H'' h''
- & is_linearform H'' h'' & is_subspace H'' E
- & is_subspace F H'' & graph F f \\<subseteq> graph H'' h''
- & (\<forall> x\<in>H''. h'' x \\<le> p x)"
+ have e2: "\<exists>H'' h''. graph H'' h'' \<in> c \<and> (y, h y) \<in> graph H'' h''
+ \<and> is_linearform H'' h'' \<and> is_subspace H'' E
+ \<and> is_subspace F H'' \<and> graph F f \<subseteq> graph H'' h''
+ \<and> (\<forall>x \<in> H''. h'' x \<le> p x)"
by (rule some_H'h't)
from e1 e2 show ?thesis
proof (elim exE conjE)
- fix H' h' assume "(y, h y)\<in> graph H' h'" "graph H' h' \<in> c"
+ fix H' h' assume "(y, h y) \<in> graph H' h'" "graph H' h' \<in> c"
"is_linearform H' h'" "is_subspace H' E" "is_subspace F H'"
- "graph F f \\<subseteq> graph H' h'" "\<forall> x\<in>H'. h' x \\<le> p x"
+ "graph F f \<subseteq> graph H' h'" "\<forall>x \<in> H'. h' x \<le> p x"
- fix H'' h'' assume "(x, h x)\<in> graph H'' h''" "graph H'' h'' \<in> c"
+ fix H'' h'' assume "(x, h x) \<in> graph H'' h''" "graph H'' h'' \<in> c"
"is_linearform H'' h''" "is_subspace H'' E" "is_subspace F H''"
- "graph F f \\<subseteq> graph H'' h''" "\<forall> x\<in>H''. h'' x \\<le> p x"
+ "graph F f \<subseteq> graph H'' h''" "\<forall>x \<in> H''. h'' x \<le> p x"
txt {* Since both $h'$ and $h''$ are elements of the chain,
$h''$ is an extension of $h'$ or vice versa. Thus both
$x$ and $y$ are contained in the greater one. \label{cases1}*}
- have "graph H'' h'' \\<subseteq> graph H' h' | graph H' h' \\<subseteq> graph H'' h''"
+ have "graph H'' h'' \<subseteq> graph H' h' | graph H' h' \<subseteq> graph H'' h''"
(is "?case1 | ?case2")
by (rule chainD)
thus ?thesis
@@ -161,23 +158,23 @@
show ?thesis
proof (intro exI conjI)
have "(x, h x) \<in> graph H'' h''" .
- also have "... \\<subseteq> graph H' h'" .
- finally have xh\<in> "(x, h x)\<in> graph H' h'" .
- thus x: "x\<in>H'" ..
- show y: "y\<in>H'" ..
- show "graph H' h' \\<subseteq> graph H h"
+ also have "... \<subseteq> graph H' h'" .
+ finally have xh:"(x, h x) \<in> graph H' h'" .
+ thus x: "x \<in> H'" ..
+ show y: "y \<in> H'" ..
+ show "graph H' h' \<subseteq> graph H h"
by (simp! only: chain_ball_Union_upper)
qed
next
assume ?case2
show ?thesis
proof (intro exI conjI)
- show x: "x\<in>H''" ..
+ show x: "x \<in> H''" ..
have "(y, h y) \<in> graph H' h'" by (simp!)
- also have "... \\<subseteq> graph H'' h''" .
- finally have yh: "(y, h y)\<in> graph H'' h''" .
- thus y: "y\<in>H''" ..
- show "graph H'' h'' \\<subseteq> graph H h"
+ also have "... \<subseteq> graph H'' h''" .
+ finally have yh: "(y, h y) \<in> graph H'' h''" .
+ thus y: "y \<in> H''" ..
+ show "graph H'' h'' \<subseteq> graph H h"
by (simp! only: chain_ball_Union_upper)
qed
qed
@@ -187,14 +184,14 @@
text{* \medskip The relation induced by the graph of the supremum
-of a chain $c$ is definite, i.~e.~it is the graph of a function. *}
+of a chain $c$ is definite, i.~e.~t is the graph of a function. *}
lemma sup_definite:
"[| M == norm_pres_extensions E p F f; c \<in> chain M;
- (x, y) \<in> Union c; (x, z) \<in> Union c |] ==> z = y"
+ (x, y) \<in> \<Union> c; (x, z) \<in> \<Union> c |] ==> z = y"
proof -
- assume "c\<in>chain M" "M == norm_pres_extensions E p F f"
- "(x, y) \<in> Union c" "(x, z) \<in> Union c"
+ assume "c \<in> chain M" "M == norm_pres_extensions E p F f"
+ "(x, y) \<in> \<Union> c" "(x, z) \<in> \<Union> c"
thus ?thesis
proof (elim UnionE chainE2)
@@ -203,7 +200,7 @@
both $G_1$ and $G_2$ are members of $c$.*}
fix G1 G2 assume
- "(x, y) \<in> G1" "G1 \<in> c" "(x, z) \<in> G2" "G2 \<in> c" "c \\<subseteq> M"
+ "(x, y) \<in> G1" "G1 \<in> c" "(x, z) \<in> G2" "G2 \<in> c" "c \<subseteq> M"
have "G1 \<in> M" ..
hence e1: "\<exists> H1 h1. graph H1 h1 = G1"
@@ -219,7 +216,7 @@
txt{* $G_1$ is contained in $G_2$ or vice versa,
since both $G_1$ and $G_2$ are members of $c$. \label{cases2}*}
- have "G1 \\<subseteq> G2 | G2 \\<subseteq> G1" (is "?case1 | ?case2") ..
+ have "G1 \<subseteq> G2 | G2 \<subseteq> G1" (is "?case1 | ?case2") ..
thus ?thesis
proof
assume ?case1
@@ -247,27 +244,27 @@
function $h'$ is linear by construction of $M$. *}
lemma sup_lf:
- "[| M = norm_pres_extensions E p F f; c\<in> chain M;
- graph H h = Union c |] ==> is_linearform H h"
+ "[| M = norm_pres_extensions E p F f; c \<in> chain M;
+ graph H h = \<Union> c |] ==> is_linearform H h"
proof -
- assume "M = norm_pres_extensions E p F f" "c\<in> chain M"
- "graph H h = Union c"
+ assume "M = norm_pres_extensions E p F f" "c \<in> chain M"
+ "graph H h = \<Union> c"
show "is_linearform H h"
proof
fix x y assume "x \<in> H" "y \<in> H"
- have "\<exists> H' h'. x\<in>H' & y\<in>H' & graph H' h' \\<subseteq> graph H h
- & is_linearform H' h' & is_subspace H' E
- & is_subspace F H' & graph F f \\<subseteq> graph H' h'
- & (\<forall> x\<in>H'. h' x \\<le> p x)"
+ have "\<exists>H' h'. x \<in> H' \<and> y \<in> H' \<and> graph H' h' \<subseteq> graph H h
+ \<and> is_linearform H' h' \<and> is_subspace H' E
+ \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h'
+ \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
by (rule some_H'h'2)
txt {* We have to show that $h$ is additive. *}
thus "h (x + y) = h x + h y"
proof (elim exE conjE)
- fix H' h' assume "x\<in>H'" "y\<in>H'"
- and b: "graph H' h' \\<subseteq> graph H h"
+ fix H' h' assume "x \<in> H'" "y \<in> H'"
+ and b: "graph H' h' \<subseteq> graph H h"
and "is_linearform H' h'" "is_subspace H' E"
have "h' (x + y) = h' x + h' y"
by (rule linearform_add)
@@ -279,24 +276,24 @@
qed
next
fix a x assume "x \<in> H"
- have "\<exists> H' h'. x\<in>H' & graph H' h' \\<subseteq> graph H h
- & is_linearform H' h' & is_subspace H' E
- & is_subspace F H' & graph F f \\<subseteq> graph H' h'
- & (\<forall> x\<in>H'. h' x \\<le> p x)"
+ have "\<exists> H' h'. x \<in> H' \<and> graph H' h' \<subseteq> graph H h
+ \<and> is_linearform H' h' \<and> is_subspace H' E
+ \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h'
+ \<and> (\<forall> x \<in> H'. h' x \<le> p x)"
by (rule some_H'h')
txt{* We have to show that $h$ is multiplicative. *}
- thus "h (a \<prod> x) = a * h x"
+ thus "h (a \<cdot> x) = a * h x"
proof (elim exE conjE)
- fix H' h' assume "x\<in>H'"
- and b: "graph H' h' \\<subseteq> graph H h"
+ fix H' h' assume "x \<in> H'"
+ and b: "graph H' h' \<subseteq> graph H h"
and "is_linearform H' h'" "is_subspace H' E"
- have "h' (a \<prod> x) = a * h' x"
+ have "h' (a \<cdot> x) = a * h' x"
by (rule linearform_mult)
also have "h' x = h x" ..
- also have "a \<prod> x \<in> H'" ..
- with b have "h' (a \<prod> x) = h (a \<prod> x)" ..
+ also have "a \<cdot> x \<in> H'" ..
+ with b have "h' (a \<cdot> x) = h (a \<cdot> x)" ..
finally show ?thesis .
qed
qed
@@ -309,34 +306,34 @@
for every element of the chain.*}
lemma sup_ext:
- "[| M = norm_pres_extensions E p F f; c\<in> chain M; \<exists> x. x\<in>c;
- graph H h = Union c |] ==> graph F f \\<subseteq> graph H h"
+ "[| graph H h = \<Union> c; M = norm_pres_extensions E p F f;
+ c \<in> chain M; \<exists>x. x \<in> c |] ==> graph F f \<subseteq> graph H h"
proof -
- assume "M = norm_pres_extensions E p F f" "c\<in> chain M"
- "graph H h = Union c"
- assume "\<exists> x. x\<in>c"
+ assume "M = norm_pres_extensions E p F f" "c \<in> chain M"
+ "graph H h = \<Union> c"
+ assume "\<exists>x. x \<in> c"
thus ?thesis
proof
- fix x assume "x\<in>c"
- have "c \\<subseteq> M" by (rule chainD2)
- hence "x\<in>M" ..
+ fix x assume "x \<in> c"
+ have "c \<subseteq> M" by (rule chainD2)
+ hence "x \<in> M" ..
hence "x \<in> norm_pres_extensions E p F f" by (simp!)
- hence "\<exists> G g. graph G g = x
- & is_linearform G g
- & is_subspace G E
- & is_subspace F G
- & graph F f \\<subseteq> graph G g
- & (\<forall> x\<in>G. g x \\<le> p x)"
+ hence "\<exists>G g. graph G g = x
+ \<and> is_linearform G g
+ \<and> is_subspace G E
+ \<and> is_subspace F G
+ \<and> graph F f \<subseteq> graph G g
+ \<and> (\<forall>x \<in> G. g x \<le> p x)"
by (simp! add: norm_pres_extension_D)
thus ?thesis
proof (elim exE conjE)
- fix G g assume "graph F f \\<subseteq> graph G g"
+ fix G g assume "graph F f \<subseteq> graph G g"
also assume "graph G g = x"
also have "... \<in> c" .
- hence "x \\<subseteq> Union c" by fast
- also have [RS sym]: "graph H h = Union c" .
+ hence "x \<subseteq> \<Union> c" by fast
+ also have [RS sym]: "graph H h = \<Union> c" .
finally show ?thesis .
qed
qed
@@ -348,30 +345,30 @@
vector space. *}
lemma sup_supF:
- "[| M = norm_pres_extensions E p F f; c\<in> chain M; \<exists> x. x\<in>c;
- graph H h = Union c; is_subspace F E; is_vectorspace E |]
+ "[| graph H h = \<Union> c; M = norm_pres_extensions E p F f;
+ c \<in> chain M; \<exists>x. x \<in> c; is_subspace F E; is_vectorspace E |]
==> is_subspace F H"
proof -
- assume "M = norm_pres_extensions E p F f" "c\<in> chain M" "\<exists> x. x\<in>c"
- "graph H h = Union c" "is_subspace F E" "is_vectorspace E"
+ assume "M = norm_pres_extensions E p F f" "c \<in> chain M" "\<exists>x. x \<in> c"
+ "graph H h = \<Union> c" "is_subspace F E" "is_vectorspace E"
show ?thesis
proof
- show "\<zero> \<in> F" ..
- show "F \\<subseteq> H"
+ show "0 \<in> F" ..
+ show "F \<subseteq> H"
proof (rule graph_extD2)
- show "graph F f \\<subseteq> graph H h"
+ show "graph F f \<subseteq> graph H h"
by (rule sup_ext)
qed
- show "\<forall> x\<in>F. \<forall> y\<in>F. x + y \<in> F"
+ show "\<forall>x \<in> F. \<forall>y \<in> F. x + y \<in> F"
proof (intro ballI)
- fix x y assume "x\<in>F" "y\<in>F"
+ fix x y assume "x \<in> F" "y \<in> F"
show "x + y \<in> F" by (simp!)
qed
- show "\<forall> x\<in>F. \<forall> a. a \<prod> x \<in> F"
+ show "\<forall>x \<in> F. \<forall>a. a \<cdot> x \<in> F"
proof (intro ballI allI)
fix x a assume "x\<in>F"
- show "a \<prod> x \<in> F" by (simp!)
+ show "a \<cdot> x \<in> F" by (simp!)
qed
qed
qed
@@ -380,78 +377,78 @@
of $E$. *}
lemma sup_subE:
- "[| M = norm_pres_extensions E p F f; c\<in> chain M; \<exists> x. x\<in>c;
- graph H h = Union c; is_subspace F E; is_vectorspace E |]
+ "[| graph H h = \<Union> c; M = norm_pres_extensions E p F f;
+ c \<in> chain M; \<exists>x. x \<in> c; is_subspace F E; is_vectorspace E |]
==> is_subspace H E"
proof -
- assume "M = norm_pres_extensions E p F f" "c\<in> chain M" "\<exists> x. x\<in>c"
- "graph H h = Union c" "is_subspace F E" "is_vectorspace E"
+ assume "M = norm_pres_extensions E p F f" "c \<in> chain M" "\<exists>x. x \<in> c"
+ "graph H h = \<Union> c" "is_subspace F E" "is_vectorspace E"
show ?thesis
proof
txt {* The $\zero$ element is in $H$, as $F$ is a subset
of $H$: *}
- have "\<zero> \<in> F" ..
+ have "0 \<in> F" ..
also have "is_subspace F H" by (rule sup_supF)
- hence "F \\<subseteq> H" ..
- finally show "\<zero> \<in> H" .
+ hence "F \<subseteq> H" ..
+ finally show "0 \<in> H" .
txt{* $H$ is a subset of $E$: *}
- show "H \\<subseteq> E"
+ show "H \<subseteq> E"
proof
- fix x assume "x\<in>H"
- have "\<exists> H' h'. x\<in>H' & graph H' h' \\<subseteq> graph H h
- & is_linearform H' h' & is_subspace H' E
- & is_subspace F H' & graph F f \\<subseteq> graph H' h'
- & (\<forall> x\<in>H'. h' x \\<le> p x)"
+ fix x assume "x \<in> H"
+ have "\<exists>H' h'. x \<in> H' \<and> graph H' h' \<subseteq> graph H h
+ \<and> is_linearform H' h' \<and> is_subspace H' E
+ \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h'
+ \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
by (rule some_H'h')
- thus "x\<in>E"
+ thus "x \<in> E"
proof (elim exE conjE)
- fix H' h' assume "x\<in>H'" "is_subspace H' E"
- have "H' \\<subseteq> E" ..
- thus "x\<in>E" ..
+ fix H' h' assume "x \<in> H'" "is_subspace H' E"
+ have "H' \<subseteq> E" ..
+ thus "x \<in> E" ..
qed
qed
txt{* $H$ is closed under addition: *}
- show "\<forall> x\<in>H. \<forall> y\<in>H. x + y \<in> H"
+ show "\<forall>x \<in> H. \<forall>y \<in> H. x + y \<in> H"
proof (intro ballI)
- fix x y assume "x\<in>H" "y\<in>H"
- have "\<exists> H' h'. x\<in>H' & y\<in>H' & graph H' h' \\<subseteq> graph H h
- & is_linearform H' h' & is_subspace H' E
- & is_subspace F H' & graph F f \\<subseteq> graph H' h'
- & (\<forall> x\<in>H'. h' x \\<le> p x)"
+ fix x y assume "x \<in> H" "y \<in> H"
+ have "\<exists>H' h'. x \<in> H' \<and> y \<in> H' \<and> graph H' h' \<subseteq> graph H h
+ \<and> is_linearform H' h' \<and> is_subspace H' E
+ \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h'
+ \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
by (rule some_H'h'2)
thus "x + y \<in> H"
proof (elim exE conjE)
fix H' h'
- assume "x\<in>H'" "y\<in>H'" "is_subspace H' E"
- "graph H' h' \\<subseteq> graph H h"
+ assume "x \<in> H'" "y \<in> H'" "is_subspace H' E"
+ "graph H' h' \<subseteq> graph H h"
have "x + y \<in> H'" ..
- also have "H' \\<subseteq> H" ..
+ also have "H' \<subseteq> H" ..
finally show ?thesis .
qed
qed
txt{* $H$ is closed under scalar multiplication: *}
- show "\<forall> x\<in>H. \<forall> a. a \<prod> x \<in> H"
+ show "\<forall>x \<in> H. \<forall>a. a \<cdot> x \<in> H"
proof (intro ballI allI)
- fix x a assume "x\<in>H"
- have "\<exists> H' h'. x\<in>H' & graph H' h' \\<subseteq> graph H h
- & is_linearform H' h' & is_subspace H' E
- & is_subspace F H' & graph F f \\<subseteq> graph H' h'
- & (\<forall> x\<in>H'. h' x \\<le> p x)"
+ fix x a assume "x \<in> H"
+ have "\<exists>H' h'. x \<in> H' \<and> graph H' h' \<subseteq> graph H h
+ \<and> is_linearform H' h' \<and> is_subspace H' E
+ \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h'
+ \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
by (rule some_H'h')
- thus "a \<prod> x \<in> H"
+ thus "a \<cdot> x \<in> H"
proof (elim exE conjE)
fix H' h'
- assume "x\<in>H'" "is_subspace H' E" "graph H' h' \\<subseteq> graph H h"
- have "a \<prod> x \<in> H'" ..
- also have "H' \\<subseteq> H" ..
+ assume "x \<in> H'" "is_subspace H' E" "graph H' h' \<subseteq> graph H h"
+ have "a \<cdot> x \<in> H'" ..
+ also have "H' \<subseteq> H" ..
finally show ?thesis .
qed
qed
@@ -463,24 +460,24 @@
bounded by $p$.
*}
-lemma sup_norm_pres\<in>
- "[| M = norm_pres_extensions E p F f; c\<in> chain M;
- graph H h = Union c |] ==> \<forall> x\<in>H. h x \\<le> p x"
+lemma sup_norm_pres:
+ "[| graph H h = \<Union> c; M = norm_pres_extensions E p F f; c \<in> chain M |]
+ ==> \<forall> x \<in> H. h x \<le> p x"
proof
- assume "M = norm_pres_extensions E p F f" "c\<in> chain M"
- "graph H h = Union c"
- fix x assume "x\<in>H"
- have "\\<exists> H' h'. x\<in>H' & graph H' h' \\<subseteq> graph H h
- & is_linearform H' h' & is_subspace H' E & is_subspace F H'
- & graph F f \\<subseteq> graph H' h' & (\<forall> x\<in>H'. h' x \\<le> p x)"
+ assume "M = norm_pres_extensions E p F f" "c \<in> chain M"
+ "graph H h = \<Union> c"
+ fix x assume "x \<in> H"
+ have "\<exists>H' h'. x \<in> H' \<and> graph H' h' \<subseteq> graph H h
+ \<and> is_linearform H' h' \<and> is_subspace H' E \<and> is_subspace F H'
+ \<and> graph F f \<subseteq> graph H' h' \<and> (\<forall> x \<in> H'. h' x \<le> p x)"
by (rule some_H'h')
- thus "h x \\<le> p x"
+ thus "h x \<le> p x"
proof (elim exE conjE)
fix H' h'
- assume "x\<in> H'" "graph H' h' \\<subseteq> graph H h"
- and a: "\<forall> x\<in> H'. h' x \\<le> p x"
+ assume "x \<in> H'" "graph H' h' \<subseteq> graph H h"
+ and a: "\<forall>x \<in> H'. h' x \<le> p x"
have [RS sym]: "h' x = h x" ..
- also from a have "h' x \\<le> p x " ..
+ also from a have "h' x \<le> p x " ..
finally show ?thesis .
qed
qed
@@ -499,7 +496,7 @@
lemma abs_ineq_iff:
"[| is_subspace H E; is_vectorspace E; is_seminorm E p;
is_linearform H h |]
- ==> (\<forall> x\<in>H. abs (h x) \\<le> p x) = (\<forall> x\<in>H. h x \\<le> p x)"
+ ==> (\<forall>x \<in> H. |h x| \<le> p x) = (\<forall>x \<in> H. h x \<le> p x)"
(concl is "?L = ?R")
proof -
assume "is_subspace H E" "is_vectorspace E" "is_seminorm E p"
@@ -510,28 +507,28 @@
assume l: ?L
show ?R
proof
- fix x assume x: "x\<in>H"
- have "h x \\<le> abs (h x)" by (rule abs_ge_self)
- also from l have "... \\<le> p x" ..
- finally show "h x \\<le> p x" .
+ fix x assume x: "x \<in> H"
+ have "h x \<le> |h x|" by (rule abs_ge_self)
+ also from l have "... \<le> p x" ..
+ finally show "h x \<le> p x" .
qed
next
assume r: ?R
show ?L
proof
- fix x assume "x\<in>H"
- show "!! a b \<in>: real. [| - a \\<le> b; b \\<le> a |] ==> abs b \\<le> a"
+ fix x assume "x \<in> H"
+ show "!! a b :: real. [| - a \<le> b; b \<le> a |] ==> |b| \<le> a"
by arith
- show "- p x \\<le> h x"
+ show "- p x \<le> h x"
proof (rule real_minus_le)
from h have "- h x = h (- x)"
by (rule linearform_neg [RS sym])
- also from r have "... \\<le> p (- x)" by (simp!)
+ also from r have "... \<le> p (- x)" by (simp!)
also have "... = p x"
by (rule seminorm_minus [OF _ subspace_subsetD])
- finally show "- h x \\<le> p x" .
+ finally show "- h x \<le> p x" .
qed
- from r show "h x \\<le> p x" ..
+ from r show "h x \<le> p x" ..
qed
qed
qed
--- a/src/HOL/Real/HahnBanach/Linearform.thy Sun Jul 16 21:00:32 2000 +0200
+++ b/src/HOL/Real/HahnBanach/Linearform.thy Mon Jul 17 13:58:18 2000 +0200
@@ -11,41 +11,41 @@
space into the reals that is additive and multiplicative. *}
constdefs
- is_linearform :: "['a::{minus, plus} set, 'a => real] => bool"
+ is_linearform :: "['a::{plus, minus, zero} set, 'a => real] => bool"
"is_linearform V f ==
- (ALL x: V. ALL y: V. f (x + y) = f x + f y) &
- (ALL x: V. ALL a. f (a (*) x) = a * (f x))"
+ (\<forall>x \<in> V. \<forall>y \<in> V. f (x + y) = f x + f y) \<and>
+ (\<forall>x \<in> V. \<forall>a. f (a \<cdot> x) = a * (f x))"
lemma is_linearformI [intro]:
- "[| !! x y. [| x : V; y : V |] ==> f (x + y) = f x + f y;
- !! x c. x : V ==> f (c (*) x) = c * f x |]
+ "[| !! x y. [| x \<in> V; y \<in> V |] ==> f (x + y) = f x + f y;
+ !! x c. x \<in> V ==> f (c \<cdot> x) = c * f x |]
==> is_linearform V f"
by (unfold is_linearform_def) force
lemma linearform_add [intro??]:
- "[| is_linearform V f; x:V; y:V |] ==> f (x + y) = f x + f y"
+ "[| is_linearform V f; x \<in> V; y \<in> V |] ==> f (x + y) = f x + f y"
by (unfold is_linearform_def) fast
lemma linearform_mult [intro??]:
- "[| is_linearform V f; x:V |] ==> f (a (*) x) = a * (f x)"
+ "[| is_linearform V f; x \<in> V |] ==> f (a \<cdot> x) = a * (f x)"
by (unfold is_linearform_def) fast
lemma linearform_neg [intro??]:
- "[| is_vectorspace V; is_linearform V f; x:V|]
+ "[| is_vectorspace V; is_linearform V f; x \<in> V|]
==> f (- x) = - f x"
proof -
- assume "is_linearform V f" "is_vectorspace V" "x:V"
- have "f (- x) = f ((- #1) (*) x)" by (simp! add: negate_eq1)
+ assume "is_linearform V f" "is_vectorspace V" "x \<in> V"
+ have "f (- x) = f ((- #1) \<cdot> x)" by (simp! add: negate_eq1)
also have "... = (- #1) * (f x)" by (rule linearform_mult)
also have "... = - (f x)" by (simp!)
finally show ?thesis .
qed
lemma linearform_diff [intro??]:
- "[| is_vectorspace V; is_linearform V f; x:V; y:V |]
+ "[| is_vectorspace V; is_linearform V f; x \<in> V; y \<in> V |]
==> f (x - y) = f x - f y"
proof -
- assume "is_vectorspace V" "is_linearform V f" "x:V" "y:V"
+ assume "is_vectorspace V" "is_linearform V f" "x \<in> V" "y \<in> V"
have "f (x - y) = f (x + - y)" by (simp! only: diff_eq1)
also have "... = f x + f (- y)"
by (rule linearform_add) (simp!)+
@@ -56,14 +56,14 @@
text{* Every linear form yields $0$ for the $\zero$ vector.*}
lemma linearform_zero [intro??, simp]:
- "[| is_vectorspace V; is_linearform V f |] ==> f 00 = #0"
+ "[| is_vectorspace V; is_linearform V f |] ==> f 0 = #0"
proof -
assume "is_vectorspace V" "is_linearform V f"
- have "f 00 = f (00 - 00)" by (simp!)
- also have "... = f 00 - f 00"
+ have "f 0 = f (0 - 0)" by (simp!)
+ also have "... = f 0 - f 0"
by (rule linearform_diff) (simp!)+
also have "... = #0" by simp
- finally show "f 00 = #0" .
+ finally show "f 0 = #0" .
qed
end
\ No newline at end of file
--- a/src/HOL/Real/HahnBanach/NormedSpace.thy Sun Jul 16 21:00:32 2000 +0200
+++ b/src/HOL/Real/HahnBanach/NormedSpace.thy Mon Jul 17 13:58:18 2000 +0200
@@ -7,6 +7,8 @@
theory NormedSpace = Subspace:
+syntax
+ abs :: "real \<Rightarrow> real" ("|_|")
subsection {* Quasinorms *}
@@ -15,57 +17,57 @@
definite, absolute homogenous and subadditive. *}
constdefs
- is_seminorm :: "['a::{plus, minus} set, 'a => real] => bool"
- "is_seminorm V norm == ALL x: V. ALL y:V. ALL a.
+ is_seminorm :: "['a::{plus, minus, zero} set, 'a => real] => bool"
+ "is_seminorm V norm == \<forall>x \<in> V. \<forall>y \<in> V. \<forall>a.
#0 <= norm x
- & norm (a (*) x) = (abs a) * (norm x)
- & norm (x + y) <= norm x + norm y"
+ \<and> norm (a \<cdot> x) = |a| * norm x
+ \<and> norm (x + y) <= norm x + norm y"
lemma is_seminormI [intro]:
- "[| !! x y a. [| x:V; y:V|] ==> #0 <= norm x;
- !! x a. x:V ==> norm (a (*) x) = (abs a) * (norm x);
- !! x y. [|x:V; y:V |] ==> norm (x + y) <= norm x + norm y |]
+ "[| !! x y a. [| x \<in> V; y \<in> V|] ==> #0 <= norm x;
+ !! x a. x \<in> V ==> norm (a \<cdot> x) = |a| * norm x;
+ !! x y. [|x \<in> V; y \<in> V |] ==> norm (x + y) <= norm x + norm y |]
==> is_seminorm V norm"
by (unfold is_seminorm_def, force)
lemma seminorm_ge_zero [intro??]:
- "[| is_seminorm V norm; x:V |] ==> #0 <= norm x"
+ "[| is_seminorm V norm; x \<in> V |] ==> #0 <= norm x"
by (unfold is_seminorm_def, force)
lemma seminorm_abs_homogenous:
- "[| is_seminorm V norm; x:V |]
- ==> norm (a (*) x) = (abs a) * (norm x)"
+ "[| is_seminorm V norm; x \<in> V |]
+ ==> norm (a \<cdot> x) = |a| * norm x"
by (unfold is_seminorm_def, force)
lemma seminorm_subadditive:
- "[| is_seminorm V norm; x:V; y:V |]
+ "[| is_seminorm V norm; x \<in> V; y \<in> V |]
==> norm (x + y) <= norm x + norm y"
by (unfold is_seminorm_def, force)
lemma seminorm_diff_subadditive:
- "[| is_seminorm V norm; x:V; y:V; is_vectorspace V |]
+ "[| is_seminorm V norm; x \<in> V; y \<in> V; is_vectorspace V |]
==> norm (x - y) <= norm x + norm y"
proof -
- assume "is_seminorm V norm" "x:V" "y:V" "is_vectorspace V"
- have "norm (x - y) = norm (x + - #1 (*) y)"
+ assume "is_seminorm V norm" "x \<in> V" "y \<in> V" "is_vectorspace V"
+ have "norm (x - y) = norm (x + - #1 \<cdot> y)"
by (simp! add: diff_eq2 negate_eq2a)
- also have "... <= norm x + norm (- #1 (*) y)"
+ also have "... <= norm x + norm (- #1 \<cdot> y)"
by (simp! add: seminorm_subadditive)
- also have "norm (- #1 (*) y) = abs (- #1) * norm y"
+ also have "norm (- #1 \<cdot> y) = |- #1| * norm y"
by (rule seminorm_abs_homogenous)
- also have "abs (- #1) = (#1::real)" by (rule abs_minus_one)
+ also have "|- #1| = (#1::real)" by (rule abs_minus_one)
finally show "norm (x - y) <= norm x + norm y" by simp
qed
lemma seminorm_minus:
- "[| is_seminorm V norm; x:V; is_vectorspace V |]
+ "[| is_seminorm V norm; x \<in> V; is_vectorspace V |]
==> norm (- x) = norm x"
proof -
- assume "is_seminorm V norm" "x:V" "is_vectorspace V"
- have "norm (- x) = norm (- #1 (*) x)" by (simp! only: negate_eq1)
- also have "... = abs (- #1) * norm x"
+ assume "is_seminorm V norm" "x \<in> V" "is_vectorspace V"
+ have "norm (- x) = norm (- #1 \<cdot> x)" by (simp! only: negate_eq1)
+ also have "... = |- #1| * norm x"
by (rule seminorm_abs_homogenous)
- also have "abs (- #1) = (#1::real)" by (rule abs_minus_one)
+ also have "|- #1| = (#1::real)" by (rule abs_minus_one)
finally show "norm (- x) = norm x" by simp
qed
@@ -76,24 +78,24 @@
$\zero$ vector to $0$. *}
constdefs
- is_norm :: "['a::{minus, plus} set, 'a => real] => bool"
- "is_norm V norm == ALL x: V. is_seminorm V norm
- & (norm x = #0) = (x = 00)"
+ is_norm :: "['a::{plus, minus, zero} set, 'a => real] => bool"
+ "is_norm V norm == \<forall>x \<in> V. is_seminorm V norm
+ \<and> (norm x = #0) = (x = 0)"
lemma is_normI [intro]:
- "ALL x: V. is_seminorm V norm & (norm x = #0) = (x = 00)
+ "\<forall>x \<in> V. is_seminorm V norm \<and> (norm x = #0) = (x = 0)
==> is_norm V norm" by (simp only: is_norm_def)
lemma norm_is_seminorm [intro??]:
- "[| is_norm V norm; x:V |] ==> is_seminorm V norm"
+ "[| is_norm V norm; x \<in> V |] ==> is_seminorm V norm"
by (unfold is_norm_def, force)
lemma norm_zero_iff:
- "[| is_norm V norm; x:V |] ==> (norm x = #0) = (x = 00)"
+ "[| is_norm V norm; x \<in> V |] ==> (norm x = #0) = (x = 0)"
by (unfold is_norm_def, force)
lemma norm_ge_zero [intro??]:
- "[|is_norm V norm; x:V |] ==> #0 <= norm x"
+ "[|is_norm V norm; x \<in> V |] ==> #0 <= norm x"
by (unfold is_norm_def is_seminorm_def, force)
@@ -104,10 +106,9 @@
constdefs
is_normed_vectorspace ::
- "['a::{plus, minus} set, 'a => real] => bool"
+ "['a::{plus, minus, zero} set, 'a => real] => bool"
"is_normed_vectorspace V norm ==
- is_vectorspace V &
- is_norm V norm"
+ is_vectorspace V \<and> is_norm V norm"
lemma normed_vsI [intro]:
"[| is_vectorspace V; is_norm V norm |]
@@ -123,32 +124,32 @@
by (unfold is_normed_vectorspace_def, elim conjE)
lemma normed_vs_norm_ge_zero [intro??]:
- "[| is_normed_vectorspace V norm; x:V |] ==> #0 <= norm x"
+ "[| is_normed_vectorspace V norm; x \<in> V |] ==> #0 <= norm x"
by (unfold is_normed_vectorspace_def, rule, elim conjE)
lemma normed_vs_norm_gt_zero [intro??]:
- "[| is_normed_vectorspace V norm; x:V; x ~= 00 |] ==> #0 < norm x"
+ "[| is_normed_vectorspace V norm; x \<in> V; x \<noteq> 0 |] ==> #0 < norm x"
proof (unfold is_normed_vectorspace_def, elim conjE)
- assume "x : V" "x ~= 00" "is_vectorspace V" "is_norm V norm"
+ assume "x \<in> V" "x \<noteq> 0" "is_vectorspace V" "is_norm V norm"
have "#0 <= norm x" ..
- also have "#0 ~= norm x"
+ also have "#0 \<noteq> norm x"
proof
presume "norm x = #0"
- also have "?this = (x = 00)" by (rule norm_zero_iff)
- finally have "x = 00" .
+ also have "?this = (x = 0)" by (rule norm_zero_iff)
+ finally have "x = 0" .
thus "False" by contradiction
qed (rule sym)
finally show "#0 < norm x" .
qed
lemma normed_vs_norm_abs_homogenous [intro??]:
- "[| is_normed_vectorspace V norm; x:V |]
- ==> norm (a (*) x) = (abs a) * (norm x)"
+ "[| is_normed_vectorspace V norm; x \<in> V |]
+ ==> norm (a \<cdot> x) = |a| * norm x"
by (rule seminorm_abs_homogenous, rule norm_is_seminorm,
rule normed_vs_norm)
lemma normed_vs_norm_subadditive [intro??]:
- "[| is_normed_vectorspace V norm; x:V; y:V |]
+ "[| is_normed_vectorspace V norm; x \<in> V; y \<in> V |]
==> norm (x + y) <= norm x + norm y"
by (rule seminorm_subadditive, rule norm_is_seminorm,
rule normed_vs_norm)
@@ -157,7 +158,7 @@
normed vectorspace.*}
lemma subspace_normed_vs [intro??]:
- "[| is_subspace F E; is_vectorspace E;
+ "[| is_vectorspace E; is_subspace F E;
is_normed_vectorspace E norm |] ==> is_normed_vectorspace F norm"
proof (rule normed_vsI)
assume "is_subspace F E" "is_vectorspace E"
@@ -167,15 +168,15 @@
proof (intro is_normI ballI conjI)
show "is_seminorm F norm"
proof
- fix x y a presume "x : E"
+ fix x y a presume "x \<in> E"
show "#0 <= norm x" ..
- show "norm (a (*) x) = abs a * norm x" ..
- presume "y : E"
+ show "norm (a \<cdot> x) = |a| * norm x" ..
+ presume "y \<in> E"
show "norm (x + y) <= norm x + norm y" ..
qed (simp!)+
- fix x assume "x : F"
- show "(norm x = #0) = (x = 00)"
+ fix x assume "x \<in> F"
+ show "(norm x = #0) = (x = 0)"
proof (rule norm_zero_iff)
show "is_norm E norm" ..
qed (simp!)
--- a/src/HOL/Real/HahnBanach/Subspace.thy Sun Jul 16 21:00:32 2000 +0200
+++ b/src/HOL/Real/HahnBanach/Subspace.thy Mon Jul 17 13:58:18 2000 +0200
@@ -16,39 +16,39 @@
scalar multiplication. *}
constdefs
- is_subspace :: "['a::{minus, plus} set, 'a set] => bool"
- "is_subspace U V == U ~= {} & U <= V
- & (ALL x:U. ALL y:U. ALL a. x + y : U & a (*) x : U)"
+ is_subspace :: "['a::{plus, minus, zero} set, 'a set] => bool"
+ "is_subspace U V == U \<noteq> {} \<and> U <= V
+ \<and> (\<forall>x \<in> U. \<forall>y \<in> U. \<forall>a. x + y \<in> U \<and> a \<cdot> x\<in> U)"
lemma subspaceI [intro]:
- "[| 00 : U; U <= V; ALL x:U. ALL y:U. (x + y : U);
- ALL x:U. ALL a. a (*) x : U |]
+ "[| 0 \<in> U; U <= V; \<forall>x \<in> U. \<forall>y \<in> U. (x + y \<in> U);
+ \<forall>x \<in> U. \<forall>a. a \<cdot> x \<in> U |]
==> is_subspace U V"
proof (unfold is_subspace_def, intro conjI)
- assume "00 : U" thus "U ~= {}" by fast
+ assume "0 \<in> U" thus "U \<noteq> {}" by fast
qed (simp+)
-lemma subspace_not_empty [intro??]: "is_subspace U V ==> U ~= {}"
+lemma subspace_not_empty [intro??]: "is_subspace U V ==> U \<noteq> {}"
by (unfold is_subspace_def) simp
lemma subspace_subset [intro??]: "is_subspace U V ==> U <= V"
by (unfold is_subspace_def) simp
lemma subspace_subsetD [simp, intro??]:
- "[| is_subspace U V; x:U |] ==> x:V"
+ "[| is_subspace U V; x \<in> U |] ==> x \<in> V"
by (unfold is_subspace_def) force
lemma subspace_add_closed [simp, intro??]:
- "[| is_subspace U V; x:U; y:U |] ==> x + y : U"
+ "[| is_subspace U V; x \<in> U; y \<in> U |] ==> x + y \<in> U"
by (unfold is_subspace_def) simp
lemma subspace_mult_closed [simp, intro??]:
- "[| is_subspace U V; x:U |] ==> a (*) x : U"
+ "[| is_subspace U V; x \<in> U |] ==> a \<cdot> x \<in> U"
by (unfold is_subspace_def) simp
lemma subspace_diff_closed [simp, intro??]:
- "[| is_subspace U V; is_vectorspace V; x:U; y:U |]
- ==> x - y : U"
+ "[| is_subspace U V; is_vectorspace V; x \<in> U; y \<in> U |]
+ ==> x - y \<in> U"
by (simp! add: diff_eq1 negate_eq1)
text {* Similar as for linear spaces, the existence of the
@@ -56,23 +56,23 @@
of the carrier set and by vector space laws.*}
lemma zero_in_subspace [intro??]:
- "[| is_subspace U V; is_vectorspace V |] ==> 00 : U"
+ "[| is_subspace U V; is_vectorspace V |] ==> 0 \<in> U"
proof -
assume "is_subspace U V" and v: "is_vectorspace V"
- have "U ~= {}" ..
- hence "EX x. x:U" by force
+ have "U \<noteq> {}" ..
+ hence "\<exists>x. x \<in> U" by force
thus ?thesis
proof
- fix x assume u: "x:U"
- hence "x:V" by (simp!)
- with v have "00 = x - x" by (simp!)
- also have "... : U" by (rule subspace_diff_closed)
+ fix x assume u: "x \<in> U"
+ hence "x \<in> V" by (simp!)
+ with v have "0 = x - x" by (simp!)
+ also have "... \<in> U" by (rule subspace_diff_closed)
finally show ?thesis .
qed
qed
lemma subspace_neg_closed [simp, intro??]:
- "[| is_subspace U V; is_vectorspace V; x:U |] ==> - x : U"
+ "[| is_subspace U V; is_vectorspace V; x \<in> U |] ==> - x \<in> U"
by (simp add: negate_eq1)
text_raw {* \medskip *}
@@ -84,11 +84,11 @@
assume "is_subspace U V" "is_vectorspace V"
show ?thesis
proof
- show "00 : U" ..
- show "ALL x:U. ALL a. a (*) x : U" by (simp!)
- show "ALL x:U. ALL y:U. x + y : U" by (simp!)
- show "ALL x:U. - x = -#1 (*) x" by (simp! add: negate_eq1)
- show "ALL x:U. ALL y:U. x - y = x + - y"
+ show "0 \<in> U" ..
+ show "\<forall>x \<in> U. \<forall>a. a \<cdot> x \<in> U" by (simp!)
+ show "\<forall>x \<in> U. \<forall>y \<in> U. x + y \<in> U" by (simp!)
+ show "\<forall>x \<in> U. - x = -#1 \<cdot> x" by (simp! add: negate_eq1)
+ show "\<forall>x \<in> U. \<forall>y \<in> U. x - y = x + - y"
by (simp! add: diff_eq1)
qed (simp! add: vs_add_mult_distrib1 vs_add_mult_distrib2)+
qed
@@ -98,10 +98,10 @@
lemma subspace_refl [intro]: "is_vectorspace V ==> is_subspace V V"
proof
assume "is_vectorspace V"
- show "00 : V" ..
+ show "0 \<in> V" ..
show "V <= V" ..
- show "ALL x:V. ALL y:V. x + y : V" by (simp!)
- show "ALL x:V. ALL a. a (*) x : V" by (simp!)
+ show "\<forall>x \<in> V. \<forall>y \<in> V. x + y \<in> V" by (simp!)
+ show "\<forall>x \<in> V. \<forall>a. a \<cdot> x \<in> V" by (simp!)
qed
text {* The subspace relation is transitive. *}
@@ -111,22 +111,22 @@
==> is_subspace U W"
proof
assume "is_subspace U V" "is_subspace V W" "is_vectorspace V"
- show "00 : U" ..
+ show "0 \<in> U" ..
have "U <= V" ..
also have "V <= W" ..
finally show "U <= W" .
- show "ALL x:U. ALL y:U. x + y : U"
+ show "\<forall>x \<in> U. \<forall>y \<in> U. x + y \<in> U"
proof (intro ballI)
- fix x y assume "x:U" "y:U"
- show "x + y : U" by (simp!)
+ fix x y assume "x \<in> U" "y \<in> U"
+ show "x + y \<in> U" by (simp!)
qed
- show "ALL x:U. ALL a. a (*) x : U"
+ show "\<forall>x \<in> U. \<forall>a. a \<cdot> x \<in> U"
proof (intro ballI allI)
- fix x a assume "x:U"
- show "a (*) x : U" by (simp!)
+ fix x a assume "x \<in> U"
+ show "a \<cdot> x \<in> U" by (simp!)
qed
qed
@@ -138,60 +138,60 @@
scalar multiples of $x$. *}
constdefs
- lin :: "'a => 'a set"
- "lin x == {a (*) x | a. True}"
+ lin :: "('a::{minus,plus,zero}) => 'a set"
+ "lin x == {a \<cdot> x | a. True}"
-lemma linD: "x : lin v = (EX a::real. x = a (*) v)"
+lemma linD: "x \<in> lin v = (\<exists>a::real. x = a \<cdot> v)"
by (unfold lin_def) fast
-lemma linI [intro??]: "a (*) x0 : lin x0"
+lemma linI [intro??]: "a \<cdot> x0 \<in> lin x0"
by (unfold lin_def) fast
text {* Every vector is contained in its linear closure. *}
-lemma x_lin_x: "[| is_vectorspace V; x:V |] ==> x : lin x"
+lemma x_lin_x: "[| is_vectorspace V; x \<in> V |] ==> x \<in> lin x"
proof (unfold lin_def, intro CollectI exI conjI)
- assume "is_vectorspace V" "x:V"
- show "x = #1 (*) x" by (simp!)
+ assume "is_vectorspace V" "x \<in> V"
+ show "x = #1 \<cdot> x" by (simp!)
qed simp
text {* Any linear closure is a subspace. *}
lemma lin_subspace [intro??]:
- "[| is_vectorspace V; x:V |] ==> is_subspace (lin x) V"
+ "[| is_vectorspace V; x \<in> V |] ==> is_subspace (lin x) V"
proof
- assume "is_vectorspace V" "x:V"
- show "00 : lin x"
+ assume "is_vectorspace V" "x \<in> V"
+ show "0 \<in> lin x"
proof (unfold lin_def, intro CollectI exI conjI)
- show "00 = (#0::real) (*) x" by (simp!)
+ show "0 = (#0::real) \<cdot> x" by (simp!)
qed simp
show "lin x <= V"
proof (unfold lin_def, intro subsetI, elim CollectE exE conjE)
- fix xa a assume "xa = a (*) x"
- show "xa:V" by (simp!)
+ fix xa a assume "xa = a \<cdot> x"
+ show "xa \<in> V" by (simp!)
qed
- show "ALL x1 : lin x. ALL x2 : lin x. x1 + x2 : lin x"
+ show "\<forall>x1 \<in> lin x. \<forall>x2 \<in> lin x. x1 + x2 \<in> lin x"
proof (intro ballI)
- fix x1 x2 assume "x1 : lin x" "x2 : lin x"
- thus "x1 + x2 : lin x"
+ fix x1 x2 assume "x1 \<in> lin x" "x2 \<in> lin x"
+ thus "x1 + x2 \<in> lin x"
proof (unfold lin_def, elim CollectE exE conjE,
intro CollectI exI conjI)
- fix a1 a2 assume "x1 = a1 (*) x" "x2 = a2 (*) x"
- show "x1 + x2 = (a1 + a2) (*) x"
+ fix a1 a2 assume "x1 = a1 \<cdot> x" "x2 = a2 \<cdot> x"
+ show "x1 + x2 = (a1 + a2) \<cdot> x"
by (simp! add: vs_add_mult_distrib2)
qed simp
qed
- show "ALL xa:lin x. ALL a. a (*) xa : lin x"
+ show "\<forall>xa \<in> lin x. \<forall>a. a \<cdot> xa \<in> lin x"
proof (intro ballI allI)
- fix x1 a assume "x1 : lin x"
- thus "a (*) x1 : lin x"
+ fix x1 a assume "x1 \<in> lin x"
+ thus "a \<cdot> x1 \<in> lin x"
proof (unfold lin_def, elim CollectE exE conjE,
intro CollectI exI conjI)
- fix a1 assume "x1 = a1 (*) x"
- show "a (*) x1 = (a * a1) (*) x" by (simp!)
+ fix a1 assume "x1 = a1 \<cdot> x"
+ show "a \<cdot> x1 = (a * a1) \<cdot> x" by (simp!)
qed simp
qed
qed
@@ -199,9 +199,9 @@
text {* Any linear closure is a vector space. *}
lemma lin_vs [intro??]:
- "[| is_vectorspace V; x:V |] ==> is_vectorspace (lin x)"
+ "[| is_vectorspace V; x \<in> V |] ==> is_vectorspace (lin x)"
proof (rule subspace_vs)
- assume "is_vectorspace V" "x:V"
+ assume "is_vectorspace V" "x \<in> V"
show "is_subspace (lin x) V" ..
qed
@@ -215,22 +215,22 @@
instance set :: (plus) plus by intro_classes
defs vs_sum_def:
- "U + V == {u + v | u v. u:U & v:V}" (***
+ "U + V == {u + v | u v. u \<in> U \<and> v \<in> V}" (***
constdefs
vs_sum ::
- "['a::{minus, plus} set, 'a set] => 'a set" (infixl "+" 65)
- "vs_sum U V == {x. EX u:U. EX v:V. x = u + v}";
+ "['a::{plus, minus, zero} set, 'a set] => 'a set" (infixl "+" 65)
+ "vs_sum U V == {x. \<exists>u \<in> U. \<exists>v \<in> V. x = u + v}";
***)
lemma vs_sumD:
- "x: U + V = (EX u:U. EX v:V. x = u + v)"
+ "x \<in> U + V = (\<exists>u \<in> U. \<exists>v \<in> V. x = u + v)"
by (unfold vs_sum_def) fast
lemmas vs_sumE = vs_sumD [RS iffD1, elimify]
lemma vs_sumI [intro??]:
- "[| x:U; y:V; t= x + y |] ==> t : U + V"
+ "[| x \<in> U; y \<in> V; t= x + y |] ==> t \<in> U + V"
by (unfold vs_sum_def) fast
text{* $U$ is a subspace of $U + V$. *}
@@ -240,20 +240,20 @@
==> is_subspace U (U + V)"
proof
assume "is_vectorspace U" "is_vectorspace V"
- show "00 : U" ..
+ show "0 \<in> U" ..
show "U <= U + V"
proof (intro subsetI vs_sumI)
- fix x assume "x:U"
- show "x = x + 00" by (simp!)
- show "00 : V" by (simp!)
+ fix x assume "x \<in> U"
+ show "x = x + 0" by (simp!)
+ show "0 \<in> V" by (simp!)
qed
- show "ALL x:U. ALL y:U. x + y : U"
+ show "\<forall>x \<in> U. \<forall>y \<in> U. x + y \<in> U"
proof (intro ballI)
- fix x y assume "x:U" "y:U" show "x + y : U" by (simp!)
+ fix x y assume "x \<in> U" "y \<in> U" show "x + y \<in> U" by (simp!)
qed
- show "ALL x:U. ALL a. a (*) x : U"
+ show "\<forall>x \<in> U. \<forall>a. a \<cdot> x \<in> U"
proof (intro ballI allI)
- fix x a assume "x:U" show "a (*) x : U" by (simp!)
+ fix x a assume "x \<in> U" show "a \<cdot> x \<in> U" by (simp!)
qed
qed
@@ -264,38 +264,38 @@
==> is_subspace (U + V) E"
proof
assume "is_subspace U E" "is_subspace V E" "is_vectorspace E"
- show "00 : U + V"
+ show "0 \<in> U + V"
proof (intro vs_sumI)
- show "00 : U" ..
- show "00 : V" ..
- show "(00::'a) = 00 + 00" by (simp!)
+ show "0 \<in> U" ..
+ show "0 \<in> V" ..
+ show "(0::'a) = 0 + 0" by (simp!)
qed
show "U + V <= E"
proof (intro subsetI, elim vs_sumE bexE)
- fix x u v assume "u : U" "v : V" "x = u + v"
- show "x:E" by (simp!)
+ fix x u v assume "u \<in> U" "v \<in> V" "x = u + v"
+ show "x \<in> E" by (simp!)
qed
- show "ALL x: U + V. ALL y: U + V. x + y : U + V"
+ show "\<forall>x \<in> U + V. \<forall>y \<in> U + V. x + y \<in> U + V"
proof (intro ballI)
- fix x y assume "x : U + V" "y : U + V"
- thus "x + y : U + V"
+ fix x y assume "x \<in> U + V" "y \<in> U + V"
+ thus "x + y \<in> U + V"
proof (elim vs_sumE bexE, intro vs_sumI)
fix ux vx uy vy
- assume "ux : U" "vx : V" "x = ux + vx"
- and "uy : U" "vy : V" "y = uy + vy"
+ assume "ux \<in> U" "vx \<in> V" "x = ux + vx"
+ and "uy \<in> U" "vy \<in> V" "y = uy + vy"
show "x + y = (ux + uy) + (vx + vy)" by (simp!)
qed (simp!)+
qed
- show "ALL x : U + V. ALL a. a (*) x : U + V"
+ show "\<forall>x \<in> U + V. \<forall>a. a \<cdot> x \<in> U + V"
proof (intro ballI allI)
- fix x a assume "x : U + V"
- thus "a (*) x : U + V"
+ fix x a assume "x \<in> U + V"
+ thus "a \<cdot> x \<in> U + V"
proof (elim vs_sumE bexE, intro vs_sumI)
- fix a x u v assume "u : U" "v : V" "x = u + v"
- show "a (*) x = (a (*) u) + (a (*) v)"
+ fix a x u v assume "u \<in> U" "v \<in> V" "x = u + v"
+ show "a \<cdot> x = (a \<cdot> u) + (a \<cdot> v)"
by (simp! add: vs_add_mult_distrib1)
qed (simp!)+
qed
@@ -323,154 +323,154 @@
lemma decomp:
"[| is_vectorspace E; is_subspace U E; is_subspace V E;
- U Int V = {00}; u1:U; u2:U; v1:V; v2:V; u1 + v1 = u2 + v2 |]
- ==> u1 = u2 & v1 = v2"
+ U \<inter> V = {0}; u1 \<in> U; u2 \<in> U; v1 \<in> V; v2 \<in> V; u1 + v1 = u2 + v2 |]
+ ==> u1 = u2 \<and> v1 = v2"
proof
assume "is_vectorspace E" "is_subspace U E" "is_subspace V E"
- "U Int V = {00}" "u1:U" "u2:U" "v1:V" "v2:V"
+ "U \<inter> V = {0}" "u1 \<in> U" "u2 \<in> U" "v1 \<in> V" "v2 \<in> V"
"u1 + v1 = u2 + v2"
have eq: "u1 - u2 = v2 - v1" by (simp! add: vs_add_diff_swap)
- have u: "u1 - u2 : U" by (simp!)
- with eq have v': "v2 - v1 : U" by simp
- have v: "v2 - v1 : V" by (simp!)
- with eq have u': "u1 - u2 : V" by simp
+ have u: "u1 - u2 \<in> U" by (simp!)
+ with eq have v': "v2 - v1 \<in> U" by simp
+ have v: "v2 - v1 \<in> V" by (simp!)
+ with eq have u': "u1 - u2 \<in> V" by simp
show "u1 = u2"
proof (rule vs_add_minus_eq)
- show "u1 - u2 = 00" by (rule Int_singletonD [OF _ u u'])
- show "u1 : E" ..
- show "u2 : E" ..
+ show "u1 - u2 = 0" by (rule Int_singletonD [OF _ u u'])
+ show "u1 \<in> E" ..
+ show "u2 \<in> E" ..
qed
show "v1 = v2"
proof (rule vs_add_minus_eq [RS sym])
- show "v2 - v1 = 00" by (rule Int_singletonD [OF _ v' v])
- show "v1 : E" ..
- show "v2 : E" ..
+ show "v2 - v1 = 0" by (rule Int_singletonD [OF _ v' v])
+ show "v1 \<in> E" ..
+ show "v2 \<in> E" ..
qed
qed
text {* An application of the previous lemma will be used in the proof
-of the Hahn-Banach Theorem (see page \pageref{decomp-H0-use}): for any
+of the Hahn-Banach Theorem (see page \pageref{decomp-H-use}): for any
element $y + a \mult x_0$ of the direct sum of a vectorspace $H$ and
the linear closure of $x_0$ the components $y \in H$ and $a$ are
uniquely determined. *}
-lemma decomp_H0:
- "[| is_vectorspace E; is_subspace H E; y1 : H; y2 : H;
- x0 ~: H; x0 : E; x0 ~= 00; y1 + a1 (*) x0 = y2 + a2 (*) x0 |]
- ==> y1 = y2 & a1 = a2"
+lemma decomp_H':
+ "[| is_vectorspace E; is_subspace H E; y1 \<in> H; y2 \<in> H;
+ x' \<notin> H; x' \<in> E; x' \<noteq> 0; y1 + a1 \<cdot> x' = y2 + a2 \<cdot> x' |]
+ ==> y1 = y2 \<and> a1 = a2"
proof
assume "is_vectorspace E" and h: "is_subspace H E"
- and "y1 : H" "y2 : H" "x0 ~: H" "x0 : E" "x0 ~= 00"
- "y1 + a1 (*) x0 = y2 + a2 (*) x0"
+ and "y1 \<in> H" "y2 \<in> H" "x' \<notin> H" "x' \<in> E" "x' \<noteq> 0"
+ "y1 + a1 \<cdot> x' = y2 + a2 \<cdot> x'"
- have c: "y1 = y2 & a1 (*) x0 = a2 (*) x0"
+ have c: "y1 = y2 \<and> a1 \<cdot> x' = a2 \<cdot> x'"
proof (rule decomp)
- show "a1 (*) x0 : lin x0" ..
- show "a2 (*) x0 : lin x0" ..
- show "H Int (lin x0) = {00}"
+ show "a1 \<cdot> x' \<in> lin x'" ..
+ show "a2 \<cdot> x' \<in> lin x'" ..
+ show "H \<inter> (lin x') = {0}"
proof
- show "H Int lin x0 <= {00}"
+ show "H \<inter> lin x' <= {0}"
proof (intro subsetI, elim IntE, rule singleton_iff[RS iffD2])
- fix x assume "x:H" "x : lin x0"
- thus "x = 00"
+ fix x assume "x \<in> H" "x \<in> lin x'"
+ thus "x = 0"
proof (unfold lin_def, elim CollectE exE conjE)
- fix a assume "x = a (*) x0"
+ fix a assume "x = a \<cdot> x'"
show ?thesis
proof cases
assume "a = (#0::real)" show ?thesis by (simp!)
next
- assume "a ~= (#0::real)"
- from h have "rinv a (*) a (*) x0 : H"
+ assume "a \<noteq> (#0::real)"
+ from h have "rinv a \<cdot> a \<cdot> x' \<in> H"
by (rule subspace_mult_closed) (simp!)
- also have "rinv a (*) a (*) x0 = x0" by (simp!)
- finally have "x0 : H" .
+ also have "rinv a \<cdot> a \<cdot> x' = x'" by (simp!)
+ finally have "x' \<in> H" .
thus ?thesis by contradiction
qed
qed
qed
- show "{00} <= H Int lin x0"
+ show "{0} <= H \<inter> lin x'"
proof -
- have "00: H Int lin x0"
+ have "0 \<in> H \<inter> lin x'"
proof (rule IntI)
- show "00:H" ..
- from lin_vs show "00 : lin x0" ..
+ show "0 \<in> H" ..
+ from lin_vs show "0 \<in> lin x'" ..
qed
thus ?thesis by simp
qed
qed
- show "is_subspace (lin x0) E" ..
+ show "is_subspace (lin x') E" ..
qed
from c show "y1 = y2" by simp
show "a1 = a2"
proof (rule vs_mult_right_cancel [RS iffD1])
- from c show "a1 (*) x0 = a2 (*) x0" by simp
+ from c show "a1 \<cdot> x' = a2 \<cdot> x'" by simp
qed
qed
-text {* Since for any element $y + a \mult x_0$ of the direct sum
-of a vectorspace $H$ and the linear closure of $x_0$ the components
+text {* Since for any element $y + a \mult x'$ of the direct sum
+of a vectorspace $H$ and the linear closure of $x'$ the components
$y\in H$ and $a$ are unique, it follows from $y\in H$ that
$a = 0$.*}
-lemma decomp_H0_H:
- "[| is_vectorspace E; is_subspace H E; t:H; x0 ~: H; x0:E;
- x0 ~= 00 |]
- ==> (SOME (y, a). t = y + a (*) x0 & y : H) = (t, (#0::real))"
+lemma decomp_H'_H:
+ "[| is_vectorspace E; is_subspace H E; t \<in> H; x' \<notin> H; x' \<in> E;
+ x' \<noteq> 0 |]
+ ==> (SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H) = (t, (#0::real))"
proof (rule, unfold split_tupled_all)
- assume "is_vectorspace E" "is_subspace H E" "t:H" "x0 ~: H" "x0:E"
- "x0 ~= 00"
+ assume "is_vectorspace E" "is_subspace H E" "t \<in> H" "x' \<notin> H" "x' \<in> E"
+ "x' \<noteq> 0"
have h: "is_vectorspace H" ..
- fix y a presume t1: "t = y + a (*) x0" and "y:H"
- have "y = t & a = (#0::real)"
- by (rule decomp_H0) (assumption | (simp!))+
+ fix y a presume t1: "t = y + a \<cdot> x'" and "y \<in> H"
+ have "y = t \<and> a = (#0::real)"
+ by (rule decomp_H') (assumption | (simp!))+
thus "(y, a) = (t, (#0::real))" by (simp!)
qed (simp!)+
-text {* The components $y\in H$ and $a$ in $y \plus a \mult x_0$
-are unique, so the function $h_0$ defined by
-$h_0 (y \plus a \mult x_0) = h y + a \cdot \xi$ is definite. *}
+text {* The components $y\in H$ and $a$ in $y \plus a \mult x'$
+are unique, so the function $h'$ defined by
+$h' (y \plus a \mult x') = h y + a \cdot \xi$ is definite. *}
-lemma h0_definite:
- "[| h0 == (\\<lambda>x. let (y, a) = SOME (y, a). (x = y + a (*) x0 & y:H)
+lemma h'_definite:
+ "[| h' == (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a \<cdot> x' \<and> y \<in> H)
in (h y) + a * xi);
- x = y + a (*) x0; is_vectorspace E; is_subspace H E;
- y:H; x0 ~: H; x0:E; x0 ~= 00 |]
- ==> h0 x = h y + a * xi"
+ x = y + a \<cdot> x'; is_vectorspace E; is_subspace H E;
+ y \<in> H; x' \<notin> H; x' \<in> E; x' \<noteq> 0 |]
+ ==> h' x = h y + a * xi"
proof -
assume
- "h0 == (\\<lambda>x. let (y, a) = SOME (y, a). (x = y + a (*) x0 & y:H)
+ "h' == (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a \<cdot> x' \<and> y \<in> H)
in (h y) + a * xi)"
- "x = y + a (*) x0" "is_vectorspace E" "is_subspace H E"
- "y:H" "x0 ~: H" "x0:E" "x0 ~= 00"
- have "x : H + (lin x0)"
+ "x = y + a \<cdot> x'" "is_vectorspace E" "is_subspace H E"
+ "y \<in> H" "x' \<notin> H" "x' \<in> E" "x' \<noteq> 0"
+ have "x \<in> H + (lin x')"
by (simp! add: vs_sum_def lin_def) force+
- have "EX! xa. ((\\<lambda>(y, a). x = y + a (*) x0 & y:H) xa)"
+ have "\<exists>! xa. ((\<lambda>(y, a). x = y + a \<cdot> x' \<and> y \<in> H) xa)"
proof
- show "EX xa. ((\\<lambda>(y, a). x = y + a (*) x0 & y:H) xa)"
+ show "\<exists>xa. ((\<lambda>(y, a). x = y + a \<cdot> x' \<and> y \<in> H) xa)"
by (force!)
next
fix xa ya
- assume "(\\<lambda>(y,a). x = y + a (*) x0 & y : H) xa"
- "(\\<lambda>(y,a). x = y + a (*) x0 & y : H) ya"
+ assume "(\<lambda>(y,a). x = y + a \<cdot> x' \<and> y \<in> H) xa"
+ "(\<lambda>(y,a). x = y + a \<cdot> x' \<and> y \<in> H) ya"
show "xa = ya"
proof -
- show "fst xa = fst ya & snd xa = snd ya ==> xa = ya"
+ show "fst xa = fst ya \<and> snd xa = snd ya ==> xa = ya"
by (simp add: Pair_fst_snd_eq)
- have x: "x = fst xa + snd xa (*) x0 & fst xa : H"
+ have x: "x = fst xa + snd xa \<cdot> x' \<and> fst xa \<in> H"
by (force!)
- have y: "x = fst ya + snd ya (*) x0 & fst ya : H"
+ have y: "x = fst ya + snd ya \<cdot> x' \<and> fst ya \<in> H"
by (force!)
- from x y show "fst xa = fst ya & snd xa = snd ya"
- by (elim conjE) (rule decomp_H0, (simp!)+)
+ from x y show "fst xa = fst ya \<and> snd xa = snd ya"
+ by (elim conjE) (rule decomp_H', (simp!)+)
qed
qed
- hence eq: "(SOME (y, a). x = y + a (*) x0 & y:H) = (y, a)"
+ hence eq: "(SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H) = (y, a)"
by (rule select1_equality) (force!)
- thus "h0 x = h y + a * xi" by (simp! add: Let_def)
+ thus "h' x = h y + a * xi" by (simp! add: Let_def)
qed
end
\ No newline at end of file
--- a/src/HOL/Real/HahnBanach/VectorSpace.thy Sun Jul 16 21:00:32 2000 +0200
+++ b/src/HOL/Real/HahnBanach/VectorSpace.thy Mon Jul 17 13:58:18 2000 +0200
@@ -15,24 +15,11 @@
element $\zero$ is defined. *}
consts
- prod :: "[real, 'a] => 'a" (infixr "'(*')" 70)
- zero :: 'a ("00")
+ prod :: "[real, 'a::{plus, minus, zero}] => 'a" (infixr "'(*')" 70)
syntax (symbols)
- prod :: "[real, 'a] => 'a" (infixr "\<prod>" 70)
- zero :: 'a ("\<zero>")
-
-(* text {* The unary and binary minus can be considered as
-abbreviations: *}
-*)
+ prod :: "[real, 'a] => 'a" (infixr "\<cdot>" 70)
-(***
-constdefs
- negate :: "'a => 'a" ("- _" [100] 100)
- "- x == (- #1) ( * ) x"
- diff :: "'a => 'a => 'a" (infixl "-" 68)
- "x - y == x + - y";
-***)
subsection {* Vector space laws *}
@@ -47,43 +34,43 @@
*}
constdefs
- is_vectorspace :: "('a::{plus,minus}) set => bool"
- "is_vectorspace V == V ~= {}
- & (ALL x:V. ALL y:V. ALL z:V. ALL a b.
- x + y : V
- & a (*) x : V
- & (x + y) + z = x + (y + z)
- & x + y = y + x
- & x - x = 00
- & 00 + x = x
- & a (*) (x + y) = a (*) x + a (*) y
- & (a + b) (*) x = a (*) x + b (*) x
- & (a * b) (*) x = a (*) b (*) x
- & #1 (*) x = x
- & - x = (- #1) (*) x
- & x - y = x + - y)"
+ is_vectorspace :: "('a::{plus, minus, zero}) set => bool"
+ "is_vectorspace V == V \<noteq> {}
+ \<and> (\<forall>x \<in> V. \<forall>y \<in> V. \<forall>z \<in> V. \<forall>a b.
+ x + y \<in> V
+ \<and> a \<cdot> x \<in> V
+ \<and> (x + y) + z = x + (y + z)
+ \<and> x + y = y + x
+ \<and> x - x = 0
+ \<and> 0 + x = x
+ \<and> a \<cdot> (x + y) = a \<cdot> x + a \<cdot> y
+ \<and> (a + b) \<cdot> x = a \<cdot> x + b \<cdot> x
+ \<and> (a * b) \<cdot> x = a \<cdot> b \<cdot> x
+ \<and> #1 \<cdot> x = x
+ \<and> - x = (- #1) \<cdot> x
+ \<and> x - y = x + - y)"
text_raw {* \medskip *}
text {* The corresponding introduction rule is:*}
lemma vsI [intro]:
- "[| 00:V;
- ALL x:V. ALL y:V. x + y : V;
- ALL x:V. ALL a. a (*) x : V;
- ALL x:V. ALL y:V. ALL z:V. (x + y) + z = x + (y + z);
- ALL x:V. ALL y:V. x + y = y + x;
- ALL x:V. x - x = 00;
- ALL x:V. 00 + x = x;
- ALL x:V. ALL y:V. ALL a. a (*) (x + y) = a (*) x + a (*) y;
- ALL x:V. ALL a b. (a + b) (*) x = a (*) x + b (*) x;
- ALL x:V. ALL a b. (a * b) (*) x = a (*) b (*) x;
- ALL x:V. #1 (*) x = x;
- ALL x:V. - x = (- #1) (*) x;
- ALL x:V. ALL y:V. x - y = x + - y |] ==> is_vectorspace V"
+ "[| 0 \<in> V;
+ \<forall>x \<in> V. \<forall>y \<in> V. x + y \<in> V;
+ \<forall>x \<in> V. \<forall>a. a \<cdot> x \<in> V;
+ \<forall>x \<in> V. \<forall>y \<in> V. \<forall>z \<in> V. (x + y) + z = x + (y + z);
+ \<forall>x \<in> V. \<forall>y \<in> V. x + y = y + x;
+ \<forall>x \<in> V. x - x = 0;
+ \<forall>x \<in> V. 0 + x = x;
+ \<forall>x \<in> V. \<forall>y \<in> V. \<forall>a. a \<cdot> (x + y) = a \<cdot> x + a \<cdot> y;
+ \<forall>x \<in> V. \<forall>a b. (a + b) \<cdot> x = a \<cdot> x + b \<cdot> x;
+ \<forall>x \<in> V. \<forall>a b. (a * b) \<cdot> x = a \<cdot> b \<cdot> x;
+ \<forall>x \<in> V. #1 \<cdot> x = x;
+ \<forall>x \<in> V. - x = (- #1) \<cdot> x;
+ \<forall>x \<in> V. \<forall>y \<in> V. x - y = x + - y |] ==> is_vectorspace V"
proof (unfold is_vectorspace_def, intro conjI ballI allI)
fix x y z
- assume "x:V" "y:V" "z:V"
- "ALL x:V. ALL y:V. ALL z:V. x + y + z = x + (y + z)"
+ assume "x \<in> V" "y \<in> V" "z \<in> V"
+ "\<forall>x \<in> V. \<forall>y \<in> V. \<forall>z \<in> V. x + y + z = x + (y + z)"
thus "x + y + z = x + (y + z)" by (elim bspec[elimify])
qed force+
@@ -91,58 +78,58 @@
text {* The corresponding destruction rules are: *}
lemma negate_eq1:
- "[| is_vectorspace V; x:V |] ==> - x = (- #1) (*) x"
+ "[| is_vectorspace V; x \<in> V |] ==> - x = (- #1) \<cdot> x"
by (unfold is_vectorspace_def) simp
lemma diff_eq1:
- "[| is_vectorspace V; x:V; y:V |] ==> x - y = x + - y"
+ "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> x - y = x + - y"
by (unfold is_vectorspace_def) simp
lemma negate_eq2:
- "[| is_vectorspace V; x:V |] ==> (- #1) (*) x = - x"
+ "[| is_vectorspace V; x \<in> V |] ==> (- #1) \<cdot> x = - x"
by (unfold is_vectorspace_def) simp
lemma negate_eq2a:
- "[| is_vectorspace V; x:V |] ==> #-1 (*) x = - x"
+ "[| is_vectorspace V; x \<in> V |] ==> #-1 \<cdot> x = - x"
by (unfold is_vectorspace_def) simp
lemma diff_eq2:
- "[| is_vectorspace V; x:V; y:V |] ==> x + - y = x - y"
+ "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> x + - y = x - y"
by (unfold is_vectorspace_def) simp
-lemma vs_not_empty [intro??]: "is_vectorspace V ==> (V ~= {})"
+lemma vs_not_empty [intro??]: "is_vectorspace V ==> (V \<noteq> {})"
by (unfold is_vectorspace_def) simp
lemma vs_add_closed [simp, intro??]:
- "[| is_vectorspace V; x:V; y:V |] ==> x + y : V"
+ "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> x + y \<in> V"
by (unfold is_vectorspace_def) simp
lemma vs_mult_closed [simp, intro??]:
- "[| is_vectorspace V; x:V |] ==> a (*) x : V"
+ "[| is_vectorspace V; x \<in> V |] ==> a \<cdot> x \<in> V"
by (unfold is_vectorspace_def) simp
lemma vs_diff_closed [simp, intro??]:
- "[| is_vectorspace V; x:V; y:V |] ==> x - y : V"
+ "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> x - y \<in> V"
by (simp add: diff_eq1 negate_eq1)
lemma vs_neg_closed [simp, intro??]:
- "[| is_vectorspace V; x:V |] ==> - x : V"
+ "[| is_vectorspace V; x \<in> V |] ==> - x \<in> V"
by (simp add: negate_eq1)
lemma vs_add_assoc [simp]:
- "[| is_vectorspace V; x:V; y:V; z:V |]
+ "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V |]
==> (x + y) + z = x + (y + z)"
by (unfold is_vectorspace_def) fast
lemma vs_add_commute [simp]:
- "[| is_vectorspace V; x:V; y:V |] ==> y + x = x + y"
+ "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> y + x = x + y"
by (unfold is_vectorspace_def) simp
lemma vs_add_left_commute [simp]:
- "[| is_vectorspace V; x:V; y:V; z:V |]
+ "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V |]
==> x + (y + z) = y + (x + z)"
proof -
- assume "is_vectorspace V" "x:V" "y:V" "z:V"
+ assume "is_vectorspace V" "x \<in> V" "y \<in> V" "z \<in> V"
hence "x + (y + z) = (x + y) + z"
by (simp only: vs_add_assoc)
also have "... = (y + x) + z" by (simp! only: vs_add_commute)
@@ -153,78 +140,78 @@
theorems vs_add_ac = vs_add_assoc vs_add_commute vs_add_left_commute
lemma vs_diff_self [simp]:
- "[| is_vectorspace V; x:V |] ==> x - x = 00"
+ "[| is_vectorspace V; x \<in> V |] ==> x - x = 0"
by (unfold is_vectorspace_def) simp
text {* The existence of the zero element of a vector space
follows from the non-emptiness of carrier set. *}
-lemma zero_in_vs [simp, intro]: "is_vectorspace V ==> 00:V"
+lemma zero_in_vs [simp, intro]: "is_vectorspace V ==> 0 \<in> V"
proof -
assume "is_vectorspace V"
- have "V ~= {}" ..
- hence "EX x. x:V" by force
+ have "V \<noteq> {}" ..
+ hence "\<exists>x. x \<in> V" by force
thus ?thesis
proof
- fix x assume "x:V"
- have "00 = x - x" by (simp!)
- also have "... : V" by (simp! only: vs_diff_closed)
+ fix x assume "x \<in> V"
+ have "0 = x - x" by (simp!)
+ also have "... \<in> V" by (simp! only: vs_diff_closed)
finally show ?thesis .
qed
qed
lemma vs_add_zero_left [simp]:
- "[| is_vectorspace V; x:V |] ==> 00 + x = x"
+ "[| is_vectorspace V; x \<in> V |] ==> 0 + x = x"
by (unfold is_vectorspace_def) simp
lemma vs_add_zero_right [simp]:
- "[| is_vectorspace V; x:V |] ==> x + 00 = x"
+ "[| is_vectorspace V; x \<in> V |] ==> x + 0 = x"
proof -
- assume "is_vectorspace V" "x:V"
- hence "x + 00 = 00 + x" by simp
+ assume "is_vectorspace V" "x \<in> V"
+ hence "x + 0 = 0 + x" by simp
also have "... = x" by (simp!)
finally show ?thesis .
qed
lemma vs_add_mult_distrib1:
- "[| is_vectorspace V; x:V; y:V |]
- ==> a (*) (x + y) = a (*) x + a (*) y"
+ "[| is_vectorspace V; x \<in> V; y \<in> V |]
+ ==> a \<cdot> (x + y) = a \<cdot> x + a \<cdot> y"
by (unfold is_vectorspace_def) simp
lemma vs_add_mult_distrib2:
- "[| is_vectorspace V; x:V |]
- ==> (a + b) (*) x = a (*) x + b (*) x"
+ "[| is_vectorspace V; x \<in> V |]
+ ==> (a + b) \<cdot> x = a \<cdot> x + b \<cdot> x"
by (unfold is_vectorspace_def) simp
lemma vs_mult_assoc:
- "[| is_vectorspace V; x:V |] ==> (a * b) (*) x = a (*) (b (*) x)"
+ "[| is_vectorspace V; x \<in> V |] ==> (a * b) \<cdot> x = a \<cdot> (b \<cdot> x)"
by (unfold is_vectorspace_def) simp
lemma vs_mult_assoc2 [simp]:
- "[| is_vectorspace V; x:V |] ==> a (*) b (*) x = (a * b) (*) x"
+ "[| is_vectorspace V; x \<in> V |] ==> a \<cdot> b \<cdot> x = (a * b) \<cdot> x"
by (simp only: vs_mult_assoc)
lemma vs_mult_1 [simp]:
- "[| is_vectorspace V; x:V |] ==> #1 (*) x = x"
+ "[| is_vectorspace V; x \<in> V |] ==> #1 \<cdot> x = x"
by (unfold is_vectorspace_def) simp
lemma vs_diff_mult_distrib1:
- "[| is_vectorspace V; x:V; y:V |]
- ==> a (*) (x - y) = a (*) x - a (*) y"
+ "[| is_vectorspace V; x \<in> V; y \<in> V |]
+ ==> a \<cdot> (x - y) = a \<cdot> x - a \<cdot> y"
by (simp add: diff_eq1 negate_eq1 vs_add_mult_distrib1)
lemma vs_diff_mult_distrib2:
- "[| is_vectorspace V; x:V |]
- ==> (a - b) (*) x = a (*) x - (b (*) x)"
+ "[| is_vectorspace V; x \<in> V |]
+ ==> (a - b) \<cdot> x = a \<cdot> x - (b \<cdot> x)"
proof -
- assume "is_vectorspace V" "x:V"
- have " (a - b) (*) x = (a + - b) (*) x"
+ assume "is_vectorspace V" "x \<in> V"
+ have " (a - b) \<cdot> x = (a + - b) \<cdot> x"
by (unfold real_diff_def, simp)
- also have "... = a (*) x + (- b) (*) x"
+ also have "... = a \<cdot> x + (- b) \<cdot> x"
by (rule vs_add_mult_distrib2)
- also have "... = a (*) x + - (b (*) x)"
+ also have "... = a \<cdot> x + - (b \<cdot> x)"
by (simp! add: negate_eq1)
- also have "... = a (*) x - (b (*) x)"
+ also have "... = a \<cdot> x - (b \<cdot> x)"
by (simp! add: diff_eq1)
finally show ?thesis .
qed
@@ -234,40 +221,40 @@
text{* Further derived laws: *}
lemma vs_mult_zero_left [simp]:
- "[| is_vectorspace V; x:V |] ==> #0 (*) x = 00"
+ "[| is_vectorspace V; x \<in> V |] ==> #0 \<cdot> x = 0"
proof -
- assume "is_vectorspace V" "x:V"
- have "#0 (*) x = (#1 - #1) (*) x" by simp
- also have "... = (#1 + - #1) (*) x" by simp
- also have "... = #1 (*) x + (- #1) (*) x"
+ assume "is_vectorspace V" "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"
by (rule vs_add_mult_distrib2)
- also have "... = x + (- #1) (*) x" by (simp!)
+ also have "... = x + (- #1) \<cdot> x" by (simp!)
also have "... = x + - x" by (simp! add: negate_eq2a)
also have "... = x - x" by (simp! add: diff_eq2)
- also have "... = 00" by (simp!)
+ also have "... = 0" by (simp!)
finally show ?thesis .
qed
lemma vs_mult_zero_right [simp]:
- "[| is_vectorspace (V:: 'a::{plus, minus} set) |]
- ==> a (*) 00 = (00::'a)"
+ "[| is_vectorspace (V:: 'a::{plus, minus, zero} set) |]
+ ==> a \<cdot> 0 = (0::'a)"
proof -
assume "is_vectorspace V"
- have "a (*) 00 = a (*) (00 - (00::'a))" by (simp!)
- also have "... = a (*) 00 - a (*) 00"
+ have "a \<cdot> 0 = a \<cdot> (0 - (0::'a))" by (simp!)
+ also have "... = a \<cdot> 0 - a \<cdot> 0"
by (rule vs_diff_mult_distrib1) (simp!)+
- also have "... = 00" by (simp!)
+ also have "... = 0" by (simp!)
finally show ?thesis .
qed
lemma vs_minus_mult_cancel [simp]:
- "[| is_vectorspace V; x:V |] ==> (- a) (*) - x = a (*) x"
+ "[| is_vectorspace V; x \<in> V |] ==> (- a) \<cdot> - x = a \<cdot> x"
by (simp add: negate_eq1)
lemma vs_add_minus_left_eq_diff:
- "[| is_vectorspace V; x:V; y:V |] ==> - x + y = y - x"
+ "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> - x + y = y - x"
proof -
- assume "is_vectorspace V" "x:V" "y:V"
+ assume "is_vectorspace V" "x \<in> V" "y \<in> V"
have "- x + y = y + - x"
by (simp! add: vs_add_commute [RS sym, of V "- x"])
also have "... = y - x" by (simp! add: diff_eq1)
@@ -275,63 +262,63 @@
qed
lemma vs_add_minus [simp]:
- "[| is_vectorspace V; x:V |] ==> x + - x = 00"
+ "[| is_vectorspace V; x \<in> V |] ==> x + - x = 0"
by (simp! add: diff_eq2)
lemma vs_add_minus_left [simp]:
- "[| is_vectorspace V; x:V |] ==> - x + x = 00"
+ "[| is_vectorspace V; x \<in> V |] ==> - x + x = 0"
by (simp! add: diff_eq2)
lemma vs_minus_minus [simp]:
- "[| is_vectorspace V; x:V |] ==> - (- x) = x"
+ "[| is_vectorspace V; x \<in> V |] ==> - (- x) = x"
by (simp add: negate_eq1)
lemma vs_minus_zero [simp]:
- "is_vectorspace (V::'a::{minus, plus} set) ==> - (00::'a) = 00"
+ "is_vectorspace (V::'a::{plus, minus, zero} set) ==> - (0::'a) = 0"
by (simp add: negate_eq1)
lemma vs_minus_zero_iff [simp]:
- "[| is_vectorspace V; x:V |] ==> (- x = 00) = (x = 00)"
+ "[| is_vectorspace V; x \<in> V |] ==> (- x = 0) = (x = 0)"
(concl is "?L = ?R")
proof -
- assume "is_vectorspace V" "x:V"
+ assume "is_vectorspace V" "x \<in> V"
show "?L = ?R"
proof
have "x = - (- x)" by (rule vs_minus_minus [RS sym])
also assume ?L
- also have "- ... = 00" by (rule vs_minus_zero)
+ also have "- ... = 0" by (rule vs_minus_zero)
finally show ?R .
qed (simp!)
qed
lemma vs_add_minus_cancel [simp]:
- "[| is_vectorspace V; x:V; y:V |] ==> x + (- x + y) = y"
+ "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> x + (- x + y) = y"
by (simp add: vs_add_assoc [RS sym] del: vs_add_commute)
lemma vs_minus_add_cancel [simp]:
- "[| is_vectorspace V; x:V; y:V |] ==> - x + (x + y) = y"
+ "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> - x + (x + y) = y"
by (simp add: vs_add_assoc [RS sym] del: vs_add_commute)
lemma vs_minus_add_distrib [simp]:
- "[| is_vectorspace V; x:V; y:V |]
+ "[| is_vectorspace V; x \<in> V; y \<in> V |]
==> - (x + y) = - x + - y"
by (simp add: negate_eq1 vs_add_mult_distrib1)
lemma vs_diff_zero [simp]:
- "[| is_vectorspace V; x:V |] ==> x - 00 = x"
+ "[| is_vectorspace V; x \<in> V |] ==> x - 0 = x"
by (simp add: diff_eq1)
lemma vs_diff_zero_right [simp]:
- "[| is_vectorspace V; x:V |] ==> 00 - x = - x"
+ "[| is_vectorspace V; x \<in> V |] ==> 0 - x = - x"
by (simp add:diff_eq1)
lemma vs_add_left_cancel:
- "[| is_vectorspace V; x:V; y:V; z:V |]
+ "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V |]
==> (x + y = x + z) = (y = z)"
(concl is "?L = ?R")
proof
- assume "is_vectorspace V" "x:V" "y:V" "z:V"
- have "y = 00 + y" by (simp!)
+ assume "is_vectorspace V" "x \<in> V" "y \<in> V" "z \<in> V"
+ have "y = 0 + y" by (simp!)
also have "... = - x + x + y" by (simp!)
also have "... = - x + (x + y)"
by (simp! only: vs_add_assoc vs_neg_closed)
@@ -343,68 +330,67 @@
qed force
lemma vs_add_right_cancel:
- "[| is_vectorspace V; x:V; y:V; z:V |]
+ "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V |]
==> (y + x = z + x) = (y = z)"
by (simp only: vs_add_commute vs_add_left_cancel)
lemma vs_add_assoc_cong:
- "[| is_vectorspace V; x:V; y:V; x':V; y':V; z:V |]
+ "[| is_vectorspace V; x \<in> V; y \<in> V; x' \<in> V; y' \<in> V; z \<in> V |]
==> x + y = x' + y' ==> x + (y + z) = x' + (y' + z)"
by (simp only: vs_add_assoc [RS sym])
lemma vs_mult_left_commute:
- "[| is_vectorspace V; x:V; y:V; z:V |]
- ==> x (*) y (*) z = y (*) x (*) z"
+ "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V |]
+ ==> x \<cdot> y \<cdot> z = y \<cdot> x \<cdot> z"
by (simp add: real_mult_commute)
-lemma vs_mult_zero_uniq :
- "[| is_vectorspace V; x:V; a (*) x = 00; x ~= 00 |] ==> a = #0"
+lemma vs_mult_zero_uniq:
+ "[| is_vectorspace V; x \<in> V; a \<cdot> x = 0; x \<noteq> 0 |] ==> a = #0"
proof (rule classical)
- assume "is_vectorspace V" "x:V" "a (*) x = 00" "x ~= 00"
- assume "a ~= #0"
- have "x = (rinv a * a) (*) x" by (simp!)
- also have "... = rinv a (*) (a (*) x)" by (rule vs_mult_assoc)
- also have "... = rinv a (*) 00" by (simp!)
- also have "... = 00" by (simp!)
- finally have "x = 00" .
+ assume "is_vectorspace V" "x \<in> V" "a \<cdot> x = 0" "x \<noteq> 0"
+ assume "a \<noteq> #0"
+ have "x = (rinv a * a) \<cdot> x" by (simp!)
+ also have "... = rinv a \<cdot> (a \<cdot> x)" by (rule vs_mult_assoc)
+ also have "... = rinv a \<cdot> 0" by (simp!)
+ also have "... = 0" by (simp!)
+ finally have "x = 0" .
thus "a = #0" by contradiction
qed
lemma vs_mult_left_cancel:
- "[| is_vectorspace V; x:V; y:V; a ~= #0 |] ==>
- (a (*) x = a (*) y) = (x = y)"
+ "[| is_vectorspace V; x \<in> V; y \<in> V; a \<noteq> #0 |] ==>
+ (a \<cdot> x = a \<cdot> y) = (x = y)"
(concl is "?L = ?R")
proof
- assume "is_vectorspace V" "x:V" "y:V" "a ~= #0"
- have "x = #1 (*) x" by (simp!)
- also have "... = (rinv a * a) (*) x" by (simp!)
- also have "... = rinv a (*) (a (*) x)"
+ assume "is_vectorspace V" "x \<in> V" "y \<in> V" "a \<noteq> #0"
+ have "x = #1 \<cdot> x" by (simp!)
+ also have "... = (rinv a * a) \<cdot> x" by (simp!)
+ also have "... = rinv a \<cdot> (a \<cdot> x)"
by (simp! only: vs_mult_assoc)
also assume ?L
- also have "rinv a (*) ... = y" by (simp!)
+ also have "rinv a \<cdot> ... = y" by (simp!)
finally show ?R .
qed simp
lemma vs_mult_right_cancel: (*** forward ***)
- "[| is_vectorspace V; x:V; x ~= 00 |]
- ==> (a (*) x = b (*) x) = (a = b)" (concl is "?L = ?R")
+ "[| is_vectorspace V; x \<in> V; x \<noteq> 0 |]
+ ==> (a \<cdot> x = b \<cdot> x) = (a = b)" (concl is "?L = ?R")
proof
- assume "is_vectorspace V" "x:V" "x ~= 00"
- have "(a - b) (*) x = a (*) x - b (*) x"
+ assume "is_vectorspace V" "x \<in> V" "x \<noteq> 0"
+ have "(a - b) \<cdot> x = a \<cdot> x - b \<cdot> x"
by (simp! add: vs_diff_mult_distrib2)
- also assume ?L hence "a (*) x - b (*) x = 00" by (simp!)
- finally have "(a - b) (*) x = 00" .
+ also assume ?L hence "a \<cdot> x - b \<cdot> x = 0" by (simp!)
+ finally have "(a - b) \<cdot> x = 0" .
hence "a - b = #0" by (simp! add: vs_mult_zero_uniq)
thus "a = b" by (rule real_add_minus_eq)
qed simp (***
-backward :
lemma vs_mult_right_cancel:
- "[| is_vectorspace V; x:V; x ~= 00 |] ==>
+ "[| is_vectorspace V; x:V; x \<noteq> 0 |] ==>
(a ( * ) x = b ( * ) x) = (a = b)"
(concl is "?L = ?R");
proof;
- assume "is_vectorspace V" "x:V" "x ~= 00";
+ assume "is_vectorspace V" "x:V" "x \<noteq> 0";
assume l: ?L;
show "a = b";
proof (rule real_add_minus_eq);
@@ -412,8 +398,8 @@
proof (rule vs_mult_zero_uniq);
have "(a - b) ( * ) x = a ( * ) x - b ( * ) x";
by (simp! add: vs_diff_mult_distrib2);
- also; from l; have "a ( * ) x - b ( * ) x = 00"; by (simp!);
- finally; show "(a - b) ( * ) x = 00"; .;
+ also; from l; have "a ( * ) x - b ( * ) x = 0"; by (simp!);
+ finally; show "(a - b) ( * ) x = 0"; .;
qed;
qed;
next;
@@ -423,11 +409,11 @@
**)
lemma vs_eq_diff_eq:
- "[| is_vectorspace V; x:V; y:V; z:V |] ==>
+ "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V |] ==>
(x = z - y) = (x + y = z)"
(concl is "?L = ?R" )
proof -
- assume vs: "is_vectorspace V" "x:V" "y:V" "z:V"
+ assume vs: "is_vectorspace V" "x \<in> V" "y \<in> V" "z \<in> V"
show "?L = ?R"
proof
assume ?L
@@ -435,7 +421,7 @@
also have "... = z + - y + y" by (simp! add: diff_eq1)
also have "... = z + (- y + y)"
by (rule vs_add_assoc) (simp!)+
- also from vs have "... = z + 00"
+ also from vs have "... = z + 0"
by (simp only: vs_add_minus_left)
also from vs have "... = z" by (simp only: vs_add_zero_right)
finally show ?R .
@@ -452,32 +438,32 @@
qed
lemma vs_add_minus_eq_minus:
- "[| is_vectorspace V; x:V; y:V; x + y = 00 |] ==> x = - y"
+ "[| is_vectorspace V; x \<in> V; y \<in> V; x + y = 0 |] ==> x = - y"
proof -
- assume "is_vectorspace V" "x:V" "y:V"
+ assume "is_vectorspace V" "x \<in> V" "y \<in> V"
have "x = (- y + y) + x" by (simp!)
also have "... = - y + (x + y)" by (simp!)
- also assume "x + y = 00"
- also have "- y + 00 = - y" by (simp!)
+ also assume "x + y = 0"
+ also have "- y + 0 = - y" by (simp!)
finally show "x = - y" .
qed
lemma vs_add_minus_eq:
- "[| is_vectorspace V; x:V; y:V; x - y = 00 |] ==> x = y"
+ "[| is_vectorspace V; x \<in> V; y \<in> V; x - y = 0 |] ==> x = y"
proof -
- assume "is_vectorspace V" "x:V" "y:V" "x - y = 00"
- assume "x - y = 00"
- hence e: "x + - y = 00" by (simp! add: diff_eq1)
+ assume "is_vectorspace V" "x \<in> V" "y \<in> V" "x - y = 0"
+ assume "x - y = 0"
+ hence e: "x + - y = 0" by (simp! add: diff_eq1)
with _ _ _ have "x = - (- y)"
by (rule vs_add_minus_eq_minus) (simp!)+
thus "x = y" by (simp!)
qed
lemma vs_add_diff_swap:
- "[| is_vectorspace V; a:V; b:V; c:V; d:V; a + b = c + d |]
+ "[| is_vectorspace V; a \<in> V; b \<in> V; c \<in> V; d \<in> V; a + b = c + d |]
==> a - c = d - b"
proof -
- assume vs: "is_vectorspace V" "a:V" "b:V" "c:V" "d:V"
+ assume vs: "is_vectorspace V" "a \<in> V" "b \<in> V" "c \<in> V" "d \<in> V"
and eq: "a + b = c + d"
have "- c + (a + b) = - c + (c + d)"
by (simp! add: vs_add_left_cancel)
@@ -487,16 +473,16 @@
by (simp add: vs_add_ac diff_eq1)
also from eq have "... = d + - b"
by (simp! add: vs_add_right_cancel)
- also have "... = d - b" by (simp! add : diff_eq2)
+ also have "... = d - b" by (simp! add: diff_eq2)
finally show "a - c = d - b" .
qed
lemma vs_add_cancel_21:
- "[| is_vectorspace V; x:V; y:V; z:V; u:V |]
+ "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V; u \<in> V |]
==> (x + (y + z) = y + u) = ((x + z) = u)"
(concl is "?L = ?R")
proof -
- assume "is_vectorspace V" "x:V" "y:V""z:V" "u:V"
+ assume "is_vectorspace V" "x \<in> V" "y \<in> V" "z \<in> V" "u \<in> V"
show "?L = ?R"
proof
have "x + z = - y + y + (x + z)" by (simp!)
@@ -510,20 +496,20 @@
qed
lemma vs_add_cancel_end:
- "[| is_vectorspace V; x:V; y:V; z:V |]
+ "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V |]
==> (x + (y + z) = y) = (x = - z)"
(concl is "?L = ?R" )
proof -
- assume "is_vectorspace V" "x:V" "y:V" "z:V"
+ assume "is_vectorspace V" "x \<in> V" "y \<in> V" "z \<in> V"
show "?L = ?R"
proof
assume l: ?L
- have "x + z = 00"
+ have "x + z = 0"
proof (rule vs_add_left_cancel [RS iffD1])
have "y + (x + z) = x + (y + z)" by (simp!)
also note l
- also have "y = y + 00" by (simp!)
- finally show "y + (x + z) = y + 00" .
+ also have "y = y + 0" by (simp!)
+ finally show "y + (x + z) = y + 0" .
qed (simp!)+
thus "x = - z" by (simp! add: vs_add_minus_eq_minus)
next