--- a/src/HOL/Real/HahnBanach/Aux.thy Mon Jul 17 15:06:08 2000 +0200
+++ b/src/HOL/Real/HahnBanach/Aux.thy Mon Jul 17 18:17:54 2000 +0200
@@ -17,22 +17,22 @@
text_raw {* \medskip *}
text{* Lemmas about sets. *}
-lemma Int_singletonD: "[| A \<inter> B = {v}; x \<in> A; x \<in> 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 ==> \<exists>x0 \<in> E. x0 \<notin> H"
- by (force simp add: psubset_eq)
+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 \<noteq> y"
- by (rule order_less_le[RS iffD1, RS conjunct2])
+lemma lt_imp_not_eq: "x < (y::'a::order) ==> x \\<noteq> y"
+ by (simp add: order_less_le)
lemma le_noteq_imp_less:
- "[| x <= (r::'a::order); x \<noteq> r |] ==> x < r"
+ "[| x <= (r::'a::order); x \\<noteq> r |] ==> x < r"
proof -
- assume "x <= r" and ne:"x \<noteq> 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 \<noteq> #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 \<noteq> #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 Mon Jul 17 15:06:08 2000 +0200
+++ b/src/HOL/Real/HahnBanach/Bounds.thy Mon Jul 17 18:17:54 2000 +0200
@@ -11,13 +11,13 @@
constdefs
is_LowerBound :: "('a::order) set => 'a set => 'a => bool"
- "is_LowerBound A B == \<lambda>x. x \<in> A \<and> (\<forall>y \<in> 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 \<in> A \<and> (\<forall> y \<in> 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)"
@@ -33,9 +33,9 @@
("(3LOWER'_BOUNDS _./ _)" 10)
translations
- "UPPER_BOUNDS x:A. P" == "UpperBounds A (Collect (\<lambda>x. P))"
+ "UPPER_BOUNDS x:A. P" == "UpperBounds A (Collect (\\<lambda>x. P))"
"UPPER_BOUNDS x. P" == "UPPER_BOUNDS x:UNIV. P"
- "LOWER_BOUNDS x:A. P" == "LowerBounds A (Collect (\<lambda>x. P))"
+ "LOWER_BOUNDS x:A. P" == "LowerBounds A (Collect (\\<lambda>x. P))"
"LOWER_BOUNDS x. P" == "LOWER_BOUNDS x:UNIV. P"
@@ -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.~.~ $A$ is defined as a least upper bound of
+ an ordered set $B$ w.~r.~t. $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 \<in> A \<and> 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)"
@@ -102,9 +102,9 @@
("(3INF _./ _)" 10)
translations
- "SUP x:A. P" == "Sup A (Collect (\<lambda>x. P))"
+ "SUP x:A. P" == "Sup A (Collect (\\<lambda>x. P))"
"SUP x. P" == "SUP x:UNIV. P"
- "INF x:A. P" == "Inf A (Collect (\<lambda>x. P))"
+ "INF x:A. P" == "Inf A (Collect (\\<lambda>x. P))"
"INF x. P" == "INF x:UNIV. P"
(*>*)
text{* The supremum of $B$ is less than any upper bound
@@ -115,16 +115,16 @@
text {* The supremum $B$ is an upper bound for $B$. *}
-lemma sup_ub: "y \<in> 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:
- "[| \<forall> y \<in> B. a <= y; is_Sup A B s; x \<in> B |] ==> a <= s"
+ "[| \\<forall>y \\<in> B. a <= y; is_Sup A B s; x \\<in> B |] ==> a <= s"
proof -
- assume "\<forall> y \<in> B. a <= y" "is_Sup A B s" "x \<in> 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 Mon Jul 17 15:06:08 2000 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy Mon Jul 17 18:17:54 2000 +0200
@@ -20,14 +20,14 @@
is_continuous ::
"['a::{plus, minus, zero} set, 'a => real, 'a => real] => bool"
"is_continuous V norm f ==
- is_linearform V f \<and> (\<exists>c. \<forall>x \<in> V. |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 \<in> V ==> |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 \<in> V ==> |f x| <= c * norm x"
- fix x assume "x \<in> V" show "|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
- ==> \<exists>c. \<forall>x \<in> V. |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 *}
@@ -66,7 +66,7 @@
constdefs
B :: "[ 'a set, 'a => real, 'a::{plus, minus, zero} => real ] => real set"
"B V norm f ==
- {#0} \<union> {|f x| * rinv (norm x) | x. x \<noteq> 0 \<and> x \<in> 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$.
@@ -85,9 +85,9 @@
"function_norm f V norm == Sup UNIV (B V norm f)"
syntax
- function_norm :: " ['a => real, 'a set, 'a => real] => real" ("\<parallel>_\<parallel>_,_")
+ function_norm :: " ['a => real, 'a set, 'a => real] => real" ("\\<parallel>_\\<parallel>_,_")
-lemma B_not_empty: "#0 \<in> B V norm f"
+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
@@ -95,35 +95,35 @@
lemma ex_fnorm [intro??]:
"[| is_normed_vectorspace V norm; is_continuous V norm f|]
- ==> is_function_norm f V norm \<parallel>f\<parallel>V,norm"
+ ==> 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: "\<exists>c. \<forall>x \<in> V. |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 "\<exists>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 "\<exists>X. X \<in> B V norm f"
+ show "\\<exists>X. X \\<in> B V norm f"
proof (intro exI)
- show "#0 \<in> (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 "\<exists>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: "\<forall>x \<in> V. |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"
@@ -133,7 +133,7 @@
txt{* To proof the thesis, we have to show that there is
some constant $b$, such that $y \leq b$ for all $y\in B$.
Due to the definition of $B$ there are two cases for
- $y\in B$. If $y = 0$ then $y \leq idt{max}\ap c\ap 0$: *}
+ $y\in B$. If $y = 0$ then $y \leq \idt{max}\ap c\ap 0$: *}
fix y assume "y = (#0::real)"
show "y <= b" by (simp! add: le_max2)
@@ -144,7 +144,7 @@
next
fix x y
- assume "x \<in> V" "x \<noteq> 0" (***
+ assume "x \\<in> V" "x \\<noteq> 0" (***
have ge: "#0 <= rinv (norm x)";
by (rule real_less_imp_le, rule real_rinv_gt_zero,
@@ -155,11 +155,11 @@
show "#0 < norm x"; ..;
qed;
qed; *** )
- have nz: "norm x \<noteq> #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 \<noteq> norm x";
+ show "#0 \\<noteq> norm x";
proof (rule lt_imp_not_eq);
show "#0 < norm x"; ..;
qed;
@@ -180,7 +180,7 @@
by (rule real_mult_assoc)
also have "(norm x * rinv (norm x)) = (#1::real)"
proof (rule real_mult_inv_right1)
- show nz: "norm x \<noteq> #0"
+ show nz: "norm x \\<noteq> #0"
by (rule not_sym, rule lt_imp_not_eq,
rule normed_vs_norm_gt_zero)
qed
@@ -195,7 +195,7 @@
lemma fnorm_ge_zero [intro??]:
"[| is_continuous V norm f; is_normed_vectorspace V norm |]
- ==> #0 <= \<parallel>f\<parallel>V,norm"
+ ==> #0 <= \\<parallel>f\\<parallel>V,norm"
proof -
assume c: "is_continuous V norm f"
and n: "is_normed_vectorspace V norm"
@@ -206,11 +206,11 @@
show ?thesis
proof (unfold function_norm_def, rule sup_ub1)
- show "\<forall>x \<in> (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 \<in> V" "x \<noteq> 0"
+ assume "x \\<in> V" "x \\<noteq> 0"
and r: "r = |f x| * rinv (norm x)"
have ge: "#0 <= |f x|" by (simp! only: abs_ge_zero)
@@ -228,13 +228,13 @@
txt {* Since $f$ is continuous the function norm exists: *}
- have "is_function_norm f V norm \<parallel>f\<parallel>V,norm" ..
+ 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 \<in> B V norm f" by (rule B_not_empty)
+ show "#0 \\<in> B V norm f" by (rule B_not_empty)
qed
qed
@@ -245,10 +245,10 @@
*}
lemma norm_fx_le_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"
+ "[| 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 \<in> V"
+ assume "is_normed_vectorspace V norm" "x \\<in> V"
and c: "is_continuous V norm f"
have v: "is_vectorspace V" ..
@@ -265,31 +265,29 @@
have "|f x| = |f 0|" by (simp!)
also from v continuous_linearform have "f 0 = #0" ..
also note abs_zero
- also have "#0 <= \<parallel>f\<parallel>V,norm * norm x"
+ also have "#0 <= \\<parallel>f\\<parallel>V,norm * norm x"
proof (rule real_le_mult_order1a)
- show "#0 <= \<parallel>f\<parallel>V,norm" ..
+ show "#0 <= \\<parallel>f\\<parallel>V,norm" ..
show "#0 <= norm x" ..
qed
finally
- show "|f x| <= \<parallel>f\<parallel>V,norm * norm x" .
+ show "|f x| <= \\<parallel>f\\<parallel>V,norm * norm x" .
next
- assume "x \<noteq> 0"
- have n: "#0 <= norm x" ..
- have nz: "norm x \<noteq> #0"
- proof (rule lt_imp_not_eq [RS not_sym])
- show "#0 < norm x" ..
- qed
+ assume "x \\<noteq> 0"
+ have n: "#0 < norm x" ..
+ hence nz: "norm x \\<noteq> #0"
+ by (simp only: lt_imp_not_eq)
txt {* For the case $x\neq \zero$ we derive the following
fact from the definition of the function norm:*}
- have l: "|f x| * rinv (norm x) <= \<parallel>f\<parallel>V,norm"
+ 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 "|f x| * rinv (norm x) \<in> 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
@@ -298,14 +296,12 @@
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 "|f x| * ... = |f x| * rinv (norm x) * norm x"
+ by (simp add: real_mult_inv_left1)
+ also 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 "|f x| <= \<parallel>f\<parallel>V,norm * norm x" .
+ also from n l have "... <= \\<parallel>f\\<parallel>V,norm * norm x"
+ by (simp add: real_mult_le_le_mono2)
+ finally show "|f x| <= \\<parallel>f\\<parallel>V,norm * norm x" .
qed
qed
@@ -318,13 +314,13 @@
lemma fnorm_le_ub:
"[| 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"
+ \\<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: "\<forall>x \<in> V. |f x| <= c * norm x"
- and "#0 <= c"
+ assume fb: "\\<forall>x \\<in> V. |f x| <= c * norm x"
+ and "#0 <= c"
txt {* Suppose the inequation holds for some $c\geq 0$.
If $c$ is an upper bound of $B$, then $c$ is greater
@@ -343,7 +339,7 @@
show "isUb UNIV (B V norm f) c"
proof (intro isUbI setleI ballI)
- fix y assume "y \<in> 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)
@@ -358,14 +354,14 @@
next
fix x
- assume "x \<in> V" "x \<noteq> 0"
+ assume "x \\<in> V" "x \\<noteq> 0"
have lz: "#0 < norm x"
by (simp! add: normed_vs_norm_gt_zero)
- have nz: "norm x \<noteq> #0"
+ have nz: "norm x \\<noteq> #0"
proof (rule not_sym)
- from lz show "#0 \<noteq> norm x"
+ from lz show "#0 \\<noteq> norm x"
by (simp! add: order_less_imp_not_eq)
qed
--- a/src/HOL/Real/HahnBanach/FunctionOrder.thy Mon Jul 17 15:06:08 2000 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy Mon Jul 17 18:17:54 2000 +0200
@@ -22,18 +22,18 @@
constdefs
graph :: "['a set, 'a => real] => 'a graph "
- "graph F f == {(x, f x) | x. x \<in> F}"
+ "graph F f == {(x, f x) | x. x \\<in> F}"
-lemma graphI [intro??]: "x \<in> F ==> (x, f x) \<in> 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 \<in> F ==> \<exists>t\<in> (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) \<in> graph F f ==> x \<in> 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) \<in> 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 \<in> 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 \<in> 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,33 +61,26 @@
constdefs
domain :: "'a graph => 'a set"
- "domain g == {x. \<exists>y. (x, y) \<in> g}"
+ "domain g == {x. \\<exists>y. (x, y) \\<in> g}"
funct :: "'a graph => ('a => real)"
- "funct g == \<lambda>x. (SOME y. (x, y) \<in> g)"
+ "funct g == \\<lambda>x. (SOME y. (x, y) \\<in> g)"
-(*text{* The equations
-\begin{matharray}
-\idt{domain} graph F f = F {\rm and}\\
-\idt{funct} graph F f = f
-\end{matharray}
-hold, but are not proved here.
-*}*)
text {* The following lemma states that $g$ is the graph of a function
if the relation induced by $g$ is unique. *}
lemma graph_domain_funct:
- "(!!x y z. (x, y) \<in> g ==> (x, z) \<in> 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) \<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)"
+ 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) \<in> g" show "y = b" by (rule uniq)
+ fix y assume "(a, y) \\<in> g" show "y = b" by (rule uniq)
qed
qed
@@ -105,37 +98,37 @@
"['a::{plus, minus, zero} set, 'a => real, 'a set, 'a => real]
=> 'a graph set"
"norm_pres_extensions E p F f
- == {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)}"
+ == {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 \<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)"
+ "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; \<forall>x \<in> H. h x <= p x |]
- ==> (graph H h \<in> 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]:
- "\<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"
+ "\\<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 Mon Jul 17 15:06:08 2000 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy Mon Jul 17 18:17:54 2000 +0200
@@ -64,36 +64,37 @@
theorem HahnBanach:
"[| 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)"
+ is_linearform F f; \\<forall>x \\<in> F. f x <= p x |]
+ ==> \\<exists>h. is_linearform E h \\<and> (\\<forall>x \\<in> F. h x = f x)
+ \\<and> (\\<forall>x \\<in> E. h x <= 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 <= 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"
+ 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
- \<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)"
+ 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 <= 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"
@@ -102,81 +103,82 @@
by (rule sup_subE, rule a) (simp!)+
show "is_subspace F ?H"
by (rule sup_supF, rule a) (simp!)+
- show "graph F f \<subseteq> graph ?H ?h"
+ 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"
+ show "\\<forall>x \\<in> ?H. ?h x <= p x"
by (rule sup_norm_pres, rule a) (simp!)+
qed
qed
}
- hence "\<exists>g \<in> M. \<forall>x \<in> M. g \<subseteq> x --> g = x"
+ 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)
-- {* We show that $M$ is non-empty: *}
- have "graph F f \<in> norm_pres_extensions E p F f"
+ 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 --> 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"
+ "is_subspace H E" "is_subspace F H" "graph F f \\<subseteq> graph H h"
+ "\\<forall>x \\<in> H. h x <= 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 \<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)
+ 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 <= 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"
+ 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> 0"
+ have x': "x' \\<noteq> 0"
proof (rule classical)
presume "x' = 0"
- with h have "x' \<in> H" by simp
+ 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"
+ obtain xi where "\\<forall>y \\<in> H. - p (y + x') - h y <= xi
+ \\<and> xi <= 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 "\<exists>xi. \<forall>y \<in> H. - p (y + x') - h y <= xi
- \<and> 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 \<in> H" "v \<in> 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)"
@@ -197,25 +199,25 @@
thus ?thesis by rule rule
qed
- def h' == "\<lambda>x. let (y,a) = SOME (y,a). x = y + a \<cdot> 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'"
+ 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'"
+ 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 \<cdot> x' \<and> y \<in> H)
+ 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)
@@ -226,81 +228,82 @@
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' = 0 + x'" by (simp!)
- from h show "0 \<in> H" ..
- show "x' \<in> lin x'" by (rule x_lin_x)
+ 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"
+ 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 h'_lf) (simp! add: x')+
show "is_subspace H' E"
- by (unfold H'_def) (rule vs_sum_subspace [OF _ lin_subspace])
+ by (unfold H'_def)
+ (rule vs_sum_subspace [OF _ lin_subspace])
have "is_subspace F H" .
also from h lin_vs
have [fold H'_def]: "is_subspace H (H + lin x')" ..
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)"
+ 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 \<cdot> x' \<and> y \<in> H)"
- proof (rule decomp_H'_H [RS sym]) qed (simp! add: x')+
+ "(x, #0) = (SOME (y, a). x = y + a \\<cdot> x' \\<and> y \\<in> H)"
+ by (rule decomp_H'_H [RS sym]) (simp! add: x')+
also have
- "(let (y,a) = (SOME (y,a). x = y + a \<cdot> x' \<and> y \<in> H)
- in h y + a * xi)
- = h' x" by (simp!)
+ "(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"
+ show "\\<forall>x \\<in> H'. h' x <= 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 --> 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 <= 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 <= p x" by (force!)
qed
qed
qed
@@ -323,21 +326,21 @@
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)"
+ 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)"
+ "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"
+ 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
@@ -352,10 +355,10 @@
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"
+ ==> \\<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"
@@ -369,32 +372,32 @@
\end{matharray}
*}
- def p == "\<lambda>x. \<parallel>f\<parallel>F,norm * norm x"
+ 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"
+ 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" ..
+ proof (unfold p_def, rule real_le_mult_order1a)
+ 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"
+ show "p (a \\<cdot> x) = |a| * p x"
proof -
- have "p (a \<cdot> x) = \<parallel>f\<parallel>F,norm * norm (a \<cdot> x)"
+ 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"
+ 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)"
+ 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 .
@@ -404,16 +407,16 @@
show "p (x + y) <= p x + p y"
proof -
- have "p (x + y) = \<parallel>f\<parallel>F,norm * norm (x + y)"
+ 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)"
+ 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" ..
+ 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"
+ 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
@@ -421,9 +424,9 @@
txt{* $f$ is bounded by $p$. *}
- have "\<forall>x \<in> F. |f x| <= p x"
+ have "\\<forall>x \\<in> F. |f x| <= p x"
proof
- fix x assume "x \<in> F"
+ 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
@@ -435,20 +438,20 @@
$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)"
+ 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"
+ 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"
+ 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
@@ -456,15 +459,15 @@
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"
+ 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"
+ show "\\<parallel>g\\<parallel>E,norm = \\<parallel>f\\<parallel>F,norm"
(is "?L = ?R")
proof (rule order_antisym)
@@ -479,36 +482,36 @@
\end{matharray}
*}
- have "\<forall>x \<in> E. |g x| <= \<parallel>f\<parallel>F,norm * norm x"
+ 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"
+ 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" ..
+ 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"
+ have "\\<forall>x \\<in> F. |f x| <= \\<parallel>g\\<parallel>E,norm * norm x"
proof
- fix x assume "x \<in> F"
+ 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"
+ have "... <= \\<parallel>g\\<parallel>E,norm * norm x"
proof (rule norm_fx_le_norm_f_norm_x)
- show "x \<in> E" ..
+ show "x \\<in> E" ..
qed
- finally show "|f x| <= \<parallel>g\<parallel>E,norm * norm x" .
+ 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" ..
+ from g_cont show "#0 <= \\<parallel>g\\<parallel>E,norm" ..
qed
qed
qed
--- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Mon Jul 17 15:06:08 2000 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Mon Jul 17 18:17:54 2000 +0200
@@ -13,12 +13,12 @@
function on $F$. We consider a subspace $H$ of $E$ that is a
superspace of $F$ and a linear form $h$ on $H$. $H$ is a not equal
to $E$ and $x_0$ is an element in $E \backslash H$.
-$H$ is extended to the direct sum $H_0 = H + \idt{lin}\ap x_0$, so for
-any $x\in H_0$ the decomposition of $x = y + a \mult x$
-with $y\in H$ is unique. $h_0$ is defined on $H_0$ by
-$h_0\ap x = h\ap y + a \cdot \xi$ for a certain $\xi$.
+$H$ is extended to the direct sum $H' = H + \idt{lin}\ap x_0$, so for
+any $x\in H'$ the decomposition of $x = y + a \mult x$
+with $y\in H$ is unique. $h'$ is defined on $H'$ by
+$h'\ap x = h\ap y + a \cdot \xi$ for a certain $\xi$.
-Subsequently we show some properties of this extension $h_0$ of $h$.
+Subsequently we show some properties of this extension $h'$ of $h$.
*};
@@ -35,42 +35,42 @@
\end{matharray} *};
lemma ex_xi:
- "[| 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";
+ "[| 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 \<in> F; v \<in> 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 \<in> F}";
+ let ?S = "{a u :: real | u. u \\<in> F}";
- have "\<exists>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 0 \<in> ?S"; by force;
- thus "\<exists>X. X \<in> ?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 "\<exists>Y. isUb UNIV ?S Y";
+ show "\\<exists>Y. isUb UNIV ?S Y";
proof;
show "isUb UNIV ?S (b 0)";
proof (intro isUbI setleI ballI);
- show "b 0 \<in> UNIV"; ..;
+ show "b 0 \\<in> UNIV"; ..;
next;
txt {* Every element $y\in S$ is less than $b\ap \zero$: *};
- fix y; assume y: "y \<in> ?S";
- from y; have "\<exists>u \<in> F. y = a u"; by fast;
+ 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 \<in> F";
+ fix u; assume "u \\<in> F";
assume "y = a u";
also; have "a u <= b 0"; by (rule r) (simp!)+;
finally; show ?thesis; .;
@@ -79,7 +79,7 @@
qed;
qed;
- thus "\<exists>xi. \<forall>y \<in> F. a y <= xi \<and> 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 \<in> 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 \<in> F";
+ fix y; assume "y \\<in> F";
show "xi <= b y";
proof (intro isLub_le_isUb isUbI setleI);
- show "b y \<in> UNIV"; ..;
- show "\<forall>ya \<in> ?S. ya <= b y";
+ show "b y \\<in> UNIV"; ..;
+ show "\\<forall>ya \\<in> ?S. ya <= b y";
proof;
- fix au; assume au: "au \<in> ?S ";
- hence "\<exists>u \<in> 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 \<in> 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;
@@ -116,23 +116,23 @@
qed;
qed;
-text{* \medskip The function $h_0$ is defined as a
-$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$. *};
+text{* \medskip The function $h'$ is defined as a
+$h'\ap x = h\ap y + a\cdot \xi$ where $x = y + a\mult \xi$
+is a linear extension of $h$ to $H'$. *};
lemma h'_lf:
- "[| h' == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H
+ "[| h' == (\\<lambda>x. let (y, a) = SOME (y, a). x = y + a \\<cdot> x0 \\<and> y \\<in> H
in h y + a * xi);
- H' == H + lin x0; is_subspace H E; is_linearform H h; x0 \<notin> H;
- x0 \<in> E; x0 \<noteq> 0; is_vectorspace E |]
+ 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 h'_def:
- "h' == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H
+ "h' == (\\<lambda>x. let (y, a) = SOME (y, a). x = y + a \\<cdot> x0 \\<and> y \\<in> H
in h y + a * xi)"
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";
+ and vs: "is_subspace H E" "is_linearform H h" "x0 \\<notin> H"
+ "x0 \\<noteq> 0" "x0 \\<in> E" "is_vectorspace E";
have h': "is_vectorspace H'";
proof (unfold H'_def, rule vs_sum_vs);
@@ -141,38 +141,37 @@
show ?thesis;
proof;
- fix x1 x2; assume x1: "x1 \<in> H'" and x2: "x2 \<in> H'";
+ 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$
+ txt{* We now have to show that $h'$ is additive, i.~e.\
+ $h' \ap (x_1\plus x_2) = h'\ap x_1 + h'\ap x_2$
for $x_1, x_2\in H$. *};
- have x1x2: "x1 + x2 \<in> H'";
+ have x1x2: "x1 + x2 \\<in> H'";
by (rule vs_add_closed, rule h');
from x1;
- have ex_x1: "\<exists> y1 a1. x1 = y1 + a1 \<cdot> x0 \<and> y1 \<in> H";
+ 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: "\<exists> y2 a2. x2 = y2 + a2 \<cdot> x0 \<and> y2 \<in> H";
+ 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: "\<exists> y a. x1 + x2 = y + a \<cdot> x0 \<and> y \<in> H";
+ 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 "h' (x1 + x2) = h' x1 + h' x2";
proof (elim exE conjE);
fix y1 y2 y a1 a2 a;
- 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 \<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";
+ 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";
+ txt {* \label{decomp-H-use}*}
+ have ya: "y1 + y2 = y \\<and> a1 + a2 = a";
+ proof (rule decomp_H')
+ show "y1 + y2 + (a1 + a2) \\<cdot> x0 = y + a \\<cdot> x0";
by (simp! add: vs_add_mult_distrib2 [of E]);
- show "y1 + y2 \<in> H"; ..;
+ show "y1 + y2 \\<in> H"; ..;
qed;
have "h' (x1 + x2) = h y + a * xi";
@@ -185,45 +184,45 @@
real_add_mult_distrib);
also; have "... = (h y1 + a1 * xi) + (h y2 + a2 * xi)";
by simp;
- also; have "h y1 + a1 * xi = h' x1";
+ 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;
- txt{* We further have to show that $h_0$ is multiplicative,
- i.~e.\ $h_0\ap (c \mult x_1) = c \cdot h_0\ap x_1$
+ txt{* We further have to show that $h'$ is multiplicative,
+ i.~e.\ $h'\ap (c \mult x_1) = c \cdot h'\ap x_1$
for $x\in H$ and $c\in \bbbR$.
*};
next;
- fix c x1; assume x1: "x1 \<in> H'";
- have ax1: "c \<cdot> x1 \<in> H'";
+ 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";
+ 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: "\<exists> y1 a1. x1 = y1 + a1 \<cdot> x0 \<and> y1 \<in> H";
+ 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)";
+ 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 \<cdot> x0" and y1': "y1 \<in> H"
- and y: "c \<cdot> x1 = y + a \<cdot> x0" and y': "y \<in> 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 \<cdot> y1 = y \<and> c * a1 = a";
+ 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";
+ 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"; ..;
+ show "c \\<cdot> y1 \\<in> H"; ..;
qed;
- have "h' (c \<cdot> x1) = h y + a * xi";
+ have "h' (c \\<cdot> x1) = h y + a * xi";
by (rule h'_definite);
- also; have "... = h (c \<cdot> y1) + (c * a1) * xi";
+ 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]);
@@ -236,35 +235,36 @@
qed;
qed;
-text{* \medskip The linear extension $h_0$ of $h$
+text{* \medskip The linear extension $h'$ of $h$
is bounded by the seminorm $p$. *};
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);
- 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";
+ "[| h' == (\\<lambda>x. let (y, a) = SOME (y, a). x = y + a \\<cdot> x0 \\<and> y \\<in> H
+ in h y + a * xi);
+ 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 h'_def:
- "h' == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H
+ "h' == (\\<lambda>x. let (y, a) = SOME (y, a). x = y + a \\<cdot> x0 \\<and> y \\<in> H
in (h y) + a * xi)"
and H'_def: "H' == H + lin x0"
- and vs: "x0 \<notin> H" "x0 \<in> E" "x0 \<noteq> 0" "is_vectorspace E"
+ 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: "\<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'";
+ 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 \<in> H' ==> \<exists>y a. x = y + a \<cdot> x0 \<and> y \<in> 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";
+ have "\\<exists>y a. x = y + a \\<cdot> x0 \\<and> y \\<in> H";
by (rule ex_x);
thus "h' x <= p x";
proof (elim exE conjE);
- fix y a; assume x: "x = y + a \<cdot> x0" and y: "y \<in> H";
+ 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);
@@ -272,7 +272,7 @@
$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 \<cdot> x0)";
+ also; have "... <= p (y + a \\<cdot> x0)";
proof (rule linorder_linear_split);
assume z: "a = #0";
@@ -282,29 +282,28 @@
taken as $y/a$: *};
next;
- assume lz: "a < #0"; hence nz: "a \<noteq> #0"; by simp;
+ assume lz: "a < #0"; hence nz: "a \\<noteq> #0"; by simp;
from a1;
- have "- p (rinv a \<cdot> y + x0) - h (rinv a \<cdot> 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 \<cdot> y + x0) - h (rinv a \<cdot> y))";
+ hence "a * xi <= 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 \<cdot> y + x0))
- - a * (h (rinv a \<cdot> 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 \<cdot> y + x0))
- = p (a \<cdot> (rinv a \<cdot> 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 \<cdot> 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 \<cdot> 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 \<cdot> x0) - h y"; .;
+ finally; have "a * xi <= p (y + a \\<cdot> x0) - h y"; .;
- hence "h y + a * xi <= h y + p (y + a \<cdot> 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 +311,28 @@
taken as $y/a$: *};
next;
- assume gz: "#0 < a"; hence nz: "a \<noteq> #0"; by simp;
- from a2;
- have "xi <= p (rinv a \<cdot> y + x0) - h (rinv a \<cdot> y)";
+ assume gz: "#0 < a"; hence nz: "a \\<noteq> #0"; by simp;
+ from a2; 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 \<cdot> y + x0) - h (rinv a \<cdot> y))";
+ with gz;
+ have "a * xi <= 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 \<cdot> y + x0)
- - a * h (rinv a \<cdot> 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 \<cdot> y + x0)
- = p (a \<cdot> (rinv a \<cdot> 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 \<cdot> 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 \<cdot> 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 \<cdot> x0) - h y"; .;
+ finally; have "a * xi <= p (y + a \\<cdot> x0) - h y"; .;
- hence "h y + a * xi <= h y + (p (y + a \<cdot> 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;
--- a/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy Mon Jul 17 15:06:08 2000 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy Mon Jul 17 18:17:54 2000 +0200
@@ -24,43 +24,43 @@
one of the elements of the chain. *}
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 \<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)"
+ "[| 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 \\<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 <= 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"
+ 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"
- 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"
+ 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"
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" ..
- hence "g \<in> norm_pres_extensions E p F f" by (simp only: m)
- 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)"
+ 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
+ \\<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 <= 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 <= p x"
show ?thesis
proof (intro exI conjI)
- show "graph H' h' \<in> c" by (simp!)
- show "(x, h x) \<in> graph H' h'" by (simp!)
+ show "graph H' h' \\<in> c" by (simp!)
+ show "(x, h x) \\<in> graph H' h'" by (simp!)
qed
qed
qed
@@ -74,29 +74,29 @@
*}
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' \<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)"
+ "[| 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' \\<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 <= 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"
+ 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"
- 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)"
+ 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 <= 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"
+ 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 <= 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
@@ -108,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' \<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)"
+ "[| 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 <= 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 \<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)"
+ 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 <= 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 \<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)"
+ 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 <= 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 <= 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 <= 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
@@ -157,24 +157,24 @@
assume ?case1
show ?thesis
proof (intro exI conjI)
- have "(x, h x) \<in> 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"
+ have "(x, h x) \\<in> 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''" ..
- 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"
+ 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"
by (simp! only: chain_ball_Union_upper)
qed
qed
@@ -187,11 +187,11 @@
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"
+ "[| M == norm_pres_extensions E p F f; c \\<in> chain M;
+ (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)
@@ -200,13 +200,13 @@
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"
+ have "G1 \\<in> M" ..
+ hence e1: "\\<exists>H1 h1. graph H1 h1 = G1"
by (force! dest: norm_pres_extension_D)
- have "G2 \<in> M" ..
- hence e2: "\<exists> H2 h2. graph H2 h2 = G2"
+ have "G2 \\<in> M" ..
+ hence e2: "\\<exists>H2 h2. graph H2 h2 = G2"
by (force! dest: norm_pres_extension_D)
from e1 e2 show ?thesis
proof (elim exE)
@@ -216,20 +216,20 @@
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
- have "(x, y) \<in> graph H2 h2" by (force!)
+ have "(x, y) \\<in> graph H2 h2" by (force!)
hence "y = h2 x" ..
- also have "(x, z) \<in> graph H2 h2" by (simp!)
+ also have "(x, z) \\<in> graph H2 h2" by (simp!)
hence "z = h2 x" ..
finally show ?thesis .
next
assume ?case2
- have "(x, y) \<in> graph H1 h1" by (simp!)
+ have "(x, y) \\<in> graph H1 h1" by (simp!)
hence "y = h1 x" ..
- also have "(x, z) \<in> graph H1 h1" by (force!)
+ also have "(x, z) \\<in> graph H1 h1" by (force!)
hence "z = h1 x" ..
finally show ?thesis .
qed
@@ -244,56 +244,56 @@
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' \<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)"
+ 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 <= 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)
also have "h' x = h x" ..
also have "h' y = h y" ..
- also have "x + y \<in> H'" ..
+ also have "x + y \\<in> H'" ..
with b have "h' (x + y) = h (x + y)" ..
finally show ?thesis .
qed
next
- fix a 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)"
+ fix a 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 <= p x)"
by (rule some_H'h')
txt{* We have to show that $h$ is multiplicative. *}
- thus "h (a \<cdot> 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 \<cdot> 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 \<cdot> x \<in> H'" ..
- with b have "h' (a \<cdot> x) = h (a \<cdot> x)" ..
+ also have "a \\<cdot> x \\<in> H'" ..
+ with b have "h' (a \\<cdot> x) = h (a \\<cdot> x)" ..
finally show ?thesis .
qed
qed
@@ -306,34 +306,34 @@
for every element of the chain.*}
lemma sup_ext:
- "[| 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"
+ "[| 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" ..
- hence "x \<in> norm_pres_extensions E p F f" by (simp!)
+ 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
- \<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)"
+ 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 <= 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" .
+ also have "... \\<in> c" .
+ hence "x \\<subseteq> \\<Union> c" by fast
+ also have [RS sym]: "graph H h = \\<Union> c" .
finally show ?thesis .
qed
qed
@@ -345,30 +345,30 @@
vector space. *}
lemma sup_supF:
- "[| 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 |]
+ "[| 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 "0 \<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"
- show "x + y \<in> F" by (simp!)
+ 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 \<cdot> 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 \<cdot> x \<in> F" by (simp!)
+ fix x a assume "x\\<in>F"
+ show "a \\<cdot> x \\<in> F" by (simp!)
qed
qed
qed
@@ -377,78 +377,78 @@
of $E$. *}
lemma sup_subE:
- "[| 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 |]
+ "[| 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 "0 \<in> F" ..
+ have "0 \\<in> F" ..
also have "is_subspace F H" by (rule sup_supF)
- hence "F \<subseteq> H" ..
- finally show "0 \<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' \<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)"
+ 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 <= 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' \<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)"
+ 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 <= p x)"
by (rule some_H'h'2)
- thus "x + y \<in> H"
+ 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"
- have "x + y \<in> H'" ..
- also have "H' \<subseteq> 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" ..
finally show ?thesis .
qed
qed
txt{* $H$ is closed under scalar multiplication: *}
- show "\<forall>x \<in> H. \<forall>a. a \<cdot> 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' \<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)"
+ 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 <= p x)"
by (rule some_H'h')
- thus "a \<cdot> 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 \<cdot> 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
@@ -461,23 +461,23 @@
*}
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"
+ "[| graph H h = \\<Union> c; M = norm_pres_extensions E p F f;
+ c \\<in> chain M |] ==> \\<forall>x \\<in> H. h x <= 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' \<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)"
+ 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 <= p x)"
by (rule some_H'h')
- thus "h x \<le> p x"
+ thus "h x <= 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 <= p x"
have [RS sym]: "h' x = h x" ..
- also from a have "h' x \<le> p x " ..
+ also from a have "h' x <= p x " ..
finally show ?thesis .
qed
qed
@@ -496,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. |h x| \<le> p x) = (\<forall>x \<in> H. h x \<le> p x)"
+ ==> (\\<forall>x \\<in> H. |h x| <= p x) = (\\<forall>x \\<in> H. h x <= p x)"
(concl is "?L = ?R")
proof -
assume "is_subspace H E" "is_vectorspace E" "is_seminorm E p"
@@ -507,31 +507,32 @@
assume l: ?L
show ?R
proof
- 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" .
+ fix x assume x: "x \\<in> H"
+ have "h x <= |h x|" by (rule abs_ge_self)
+ also from l have "... <= p x" ..
+ finally show "h x <= p x" .
qed
next
assume r: ?R
show ?L
proof
- fix x assume "x \<in> H"
- show "!! a b :: real. [| - a \<le> b; b \<le> a |] ==> |b| \<le> a"
+ fix x assume "x \\<in> H"
+ show "!! a b :: real. [| - a <= b; b <= a |] ==> |b| <= a"
by arith
- show "- p x \<le> h x"
+ show "- p x <= h x"
proof (rule real_minus_le)
- from h have "- h x = h (- x)"
+ 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 "... <= p (- x)" by (simp!)
also have "... = p x"
- by (rule seminorm_minus [OF _ subspace_subsetD])
- finally show "- h x \<le> p x" .
+ proof (rule seminorm_minus)
+ show "x \\<in> E" ..
+ qed
+ finally show "- h x <= p x" .
qed
- from r show "h x \<le> p x" ..
+ from r show "h x <= p x" ..
qed
qed
qed
-
end
\ No newline at end of file
--- a/src/HOL/Real/HahnBanach/VectorSpace.thy Mon Jul 17 15:06:08 2000 +0200
+++ b/src/HOL/Real/HahnBanach/VectorSpace.thy Mon Jul 17 18:17:54 2000 +0200
@@ -10,15 +10,14 @@
subsection {* Signature *}
text {* For the definition of real vector spaces a type $\alpha$
-of the sort $\{ \idt{plus}, \idt{minus}\}$ is considered, on which a
-real scalar multiplication $\mult$, and a zero
-element $\zero$ is defined. *}
+of the sort $\{ \idt{plus}, \idt{minus}, \idt{zero}\}$ is considered, on which a
+real scalar multiplication $\mult$ is defined. *}
consts
- prod :: "[real, 'a::{plus, minus, zero}] => 'a" (infixr "'(*')" 70)
+ prod :: "[real, 'a::{plus, minus, zero}] => 'a" (infixr "'(*')" 70)
syntax (symbols)
- prod :: "[real, 'a] => 'a" (infixr "\<cdot>" 70)
+ prod :: "[real, 'a] => 'a" (infixr "\\<cdot>" 70)
subsection {* Vector space laws *}
@@ -27,7 +26,7 @@
$\alpha$ with the following vector space laws: The set $V$ is closed
under addition and scalar multiplication, addition is associative
and commutative; $\minus x$ is the inverse of $x$ w.~r.~t.~addition
- and $\zero$ is the neutral element of addition. Addition and
+ and $0$ is the neutral element of addition. Addition and
multiplication are distributive; scalar multiplication is
associative and the real number $1$ is the neutral element of scalar
multiplication.
@@ -35,42 +34,42 @@
constdefs
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)"
+ "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]:
- "[| 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"
+ "[| 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 \<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)"
+ 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+
@@ -78,58 +77,58 @@
text {* The corresponding destruction rules are: *}
lemma negate_eq1:
- "[| is_vectorspace V; x \<in> V |] ==> - x = (- #1) \<cdot> x"
+ "[| is_vectorspace V; x \\<in> V |] ==> - x = (- #1) \\<cdot> x"
by (unfold is_vectorspace_def) simp
lemma diff_eq1:
- "[| is_vectorspace V; x \<in> V; y \<in> 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 \<in> V |] ==> (- #1) \<cdot> 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 \<in> V |] ==> #-1 \<cdot> 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 \<in> V; y \<in> 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 \<noteq> {})"
+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 \<in> V; y \<in> V |] ==> x + y \<in> 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 \<in> V |] ==> a \<cdot> x \<in> 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 \<in> V; y \<in> V |] ==> x - y \<in> 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 \<in> V |] ==> - x \<in> V"
+ "[| is_vectorspace V; x \\<in> V |] ==> - x \\<in> V"
by (simp add: negate_eq1)
lemma vs_add_assoc [simp]:
- "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> 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 \<in> V; y \<in> 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 \<in> V; y \<in> V; z \<in> 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 \<in> V" "y \<in> V" "z \<in> 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)
@@ -140,78 +139,78 @@
theorems vs_add_ac = vs_add_assoc vs_add_commute vs_add_left_commute
lemma vs_diff_self [simp]:
- "[| is_vectorspace V; x \<in> V |] ==> x - x = 0"
+ "[| 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 ==> 0 \<in> V"
+lemma zero_in_vs [simp, intro]: "is_vectorspace V ==> 0 \\<in> V"
proof -
assume "is_vectorspace V"
- have "V \<noteq> {}" ..
- hence "\<exists>x. x \<in> V" by force
+ have "V \\<noteq> {}" ..
+ hence "\\<exists>x. x \\<in> V" by force
thus ?thesis
proof
- fix x assume "x \<in> V"
+ fix x assume "x \\<in> V"
have "0 = x - x" by (simp!)
- also have "... \<in> V" by (simp! only: vs_diff_closed)
+ 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 \<in> V |] ==> 0 + 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 \<in> V |] ==> x + 0 = x"
+ "[| is_vectorspace V; x \\<in> V |] ==> x + 0 = x"
proof -
- assume "is_vectorspace V" "x \<in> V"
+ 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 \<in> V; y \<in> V |]
- ==> a \<cdot> (x + y) = a \<cdot> x + a \<cdot> 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 \<in> V |]
- ==> (a + b) \<cdot> x = a \<cdot> x + b \<cdot> 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 \<in> V |] ==> (a * b) \<cdot> x = a \<cdot> (b \<cdot> 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 \<in> V |] ==> a \<cdot> b \<cdot> x = (a * b) \<cdot> 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 \<in> V |] ==> #1 \<cdot> 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 \<in> V; y \<in> V |]
- ==> a \<cdot> (x - y) = a \<cdot> x - a \<cdot> 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 \<in> V |]
- ==> (a - b) \<cdot> x = a \<cdot> x - (b \<cdot> x)"
+ "[| is_vectorspace V; x \\<in> V |]
+ ==> (a - b) \\<cdot> x = a \\<cdot> x - (b \\<cdot> x)"
proof -
- assume "is_vectorspace V" "x \<in> V"
- have " (a - b) \<cdot> x = (a + - b) \<cdot> 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 \<cdot> x + (- b) \<cdot> x"
+ also have "... = a \\<cdot> x + (- b) \\<cdot> x"
by (rule vs_add_mult_distrib2)
- also have "... = a \<cdot> x + - (b \<cdot> x)"
+ also have "... = a \\<cdot> x + - (b \\<cdot> x)"
by (simp! add: negate_eq1)
- also have "... = a \<cdot> x - (b \<cdot> x)"
+ also have "... = a \\<cdot> x - (b \\<cdot> x)"
by (simp! add: diff_eq1)
finally show ?thesis .
qed
@@ -221,14 +220,14 @@
text{* Further derived laws: *}
lemma vs_mult_zero_left [simp]:
- "[| is_vectorspace V; x \<in> V |] ==> #0 \<cdot> x = 0"
+ "[| is_vectorspace V; x \\<in> V |] ==> #0 \\<cdot> x = 0"
proof -
- 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"
+ 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) \<cdot> 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 "... = 0" by (simp!)
@@ -237,40 +236,40 @@
lemma vs_mult_zero_right [simp]:
"[| is_vectorspace (V:: 'a::{plus, minus, zero} set) |]
- ==> a \<cdot> 0 = (0::'a)"
+ ==> a \\<cdot> 0 = (0::'a)"
proof -
assume "is_vectorspace V"
- have "a \<cdot> 0 = a \<cdot> (0 - (0::'a))" by (simp!)
- also have "... = a \<cdot> 0 - a \<cdot> 0"
+ 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 "... = 0" by (simp!)
finally show ?thesis .
qed
lemma vs_minus_mult_cancel [simp]:
- "[| is_vectorspace V; x \<in> V |] ==> (- a) \<cdot> - x = a \<cdot> 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 \<in> V; y \<in> V |] ==> - x + y = y - x"
+ "[| is_vectorspace V; x \\<in> V; y \\<in> V |] ==> - x + y = y - x"
proof -
- 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"])
+ assume "is_vectorspace V" "x \\<in> V" "y \\<in> V"
+ hence "- x + y = y + - x"
+ by (simp add: vs_add_commute)
also have "... = y - x" by (simp! add: diff_eq1)
finally show ?thesis .
qed
lemma vs_add_minus [simp]:
- "[| is_vectorspace V; x \<in> V |] ==> x + - x = 0"
+ "[| is_vectorspace V; x \\<in> V |] ==> x + - x = 0"
by (simp! add: diff_eq2)
lemma vs_add_minus_left [simp]:
- "[| is_vectorspace V; x \<in> V |] ==> - x + x = 0"
+ "[| is_vectorspace V; x \\<in> V |] ==> - x + x = 0"
by (simp! add: diff_eq2)
lemma vs_minus_minus [simp]:
- "[| is_vectorspace V; x \<in> V |] ==> - (- x) = x"
+ "[| is_vectorspace V; x \\<in> V |] ==> - (- x) = x"
by (simp add: negate_eq1)
lemma vs_minus_zero [simp]:
@@ -278,13 +277,13 @@
by (simp add: negate_eq1)
lemma vs_minus_zero_iff [simp]:
- "[| is_vectorspace V; x \<in> V |] ==> (- x = 0) = (x = 0)"
+ "[| is_vectorspace V; x \\<in> V |] ==> (- x = 0) = (x = 0)"
(concl is "?L = ?R")
proof -
- assume "is_vectorspace V" "x \<in> V"
+ assume "is_vectorspace V" "x \\<in> V"
show "?L = ?R"
proof
- have "x = - (- x)" by (rule vs_minus_minus [RS sym])
+ have "x = - (- x)" by (simp! add: vs_minus_minus)
also assume ?L
also have "- ... = 0" by (rule vs_minus_zero)
finally show ?R .
@@ -292,105 +291,105 @@
qed
lemma vs_add_minus_cancel [simp]:
- "[| is_vectorspace V; x \<in> V; y \<in> 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 \<in> V; y \<in> 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 \<in> V; y \<in> 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 \<in> V |] ==> x - 0 = 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 \<in> V |] ==> 0 - 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 \<in> V; y \<in> V; z \<in> 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 \<in> V" "y \<in> V" "z \<in> V"
+ 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)
- also assume ?L
- also have "- x + ... = - x + x + z"
- by (rule vs_add_assoc [RS sym]) (simp!)+
+ also assume "x + y = x + z"
+ also have "- x + (x + z) = - x + x + z"
+ by (simp! only: vs_add_assoc[RS sym] vs_neg_closed)
also have "... = z" by (simp!)
finally show ?R .
qed force
lemma vs_add_right_cancel:
- "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> 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 \<in> V; y \<in> V; x' \<in> V; y' \<in> V; z \<in> 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 \<in> V; y \<in> V; z \<in> V |]
- ==> x \<cdot> y \<cdot> z = y \<cdot> x \<cdot> 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 \<in> V; a \<cdot> x = 0; x \<noteq> 0 |] ==> a = #0"
+ "[| is_vectorspace V; x \\<in> V; a \\<cdot> x = 0; x \\<noteq> 0 |] ==> a = #0"
proof (rule classical)
- 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!)
+ 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 \<in> V; y \<in> V; a \<noteq> #0 |] ==>
- (a \<cdot> x = a \<cdot> 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 \<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)"
+ 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 \<cdot> ... = 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 \<in> V; x \<noteq> 0 |]
- ==> (a \<cdot> x = b \<cdot> 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 \<in> V" "x \<noteq> 0"
- have "(a - b) \<cdot> x = a \<cdot> x - b \<cdot> 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 \<cdot> x - b \<cdot> x = 0" by (simp!)
- finally have "(a - b) \<cdot> x = 0" .
+ 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 (***
lemma vs_mult_right_cancel:
- "[| is_vectorspace V; x:V; x \<noteq> 0 |] ==>
+ "[| 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 \<noteq> 0";
+ assume "is_vectorspace V" "x:V" "x \\<noteq> 0";
assume l: ?L;
show "a = b";
proof (rule real_add_minus_eq);
@@ -409,11 +408,11 @@
**)
lemma vs_eq_diff_eq:
- "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> 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 \<in> V" "y \<in> V" "z \<in> V"
+ assume vs: "is_vectorspace V" "x \\<in> V" "y \\<in> V" "z \\<in> V"
show "?L = ?R"
proof
assume ?L
@@ -438,9 +437,9 @@
qed
lemma vs_add_minus_eq_minus:
- "[| is_vectorspace V; x \<in> V; y \<in> V; x + y = 0 |] ==> x = - y"
+ "[| is_vectorspace V; x \\<in> V; y \\<in> V; x + y = 0 |] ==> x = - y"
proof -
- assume "is_vectorspace V" "x \<in> V" "y \<in> 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 = 0"
@@ -449,9 +448,9 @@
qed
lemma vs_add_minus_eq:
- "[| is_vectorspace V; x \<in> V; y \<in> V; x - y = 0 |] ==> x = y"
+ "[| is_vectorspace V; x \\<in> V; y \\<in> V; x - y = 0 |] ==> x = y"
proof -
- assume "is_vectorspace V" "x \<in> V" "y \<in> V" "x - y = 0"
+ 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)"
@@ -460,10 +459,10 @@
qed
lemma vs_add_diff_swap:
- "[| is_vectorspace V; a \<in> V; b \<in> V; c \<in> V; d \<in> 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 \<in> V" "b \<in> V" "c \<in> V" "d \<in> 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)
@@ -478,11 +477,11 @@
qed
lemma vs_add_cancel_21:
- "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V; u \<in> 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 \<in> V" "y \<in> V" "z \<in> V" "u \<in> 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!)
@@ -496,11 +495,11 @@
qed
lemma vs_add_cancel_end:
- "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> 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 \<in> V" "y \<in> V" "z \<in> V"
+ assume "is_vectorspace V" "x \\<in> V" "y \\<in> V" "z \\<in> V"
show "?L = ?R"
proof
assume l: ?L
--- a/src/HOL/Real/HahnBanach/document/notation.tex Mon Jul 17 15:06:08 2000 +0200
+++ b/src/HOL/Real/HahnBanach/document/notation.tex Mon Jul 17 18:17:54 2000 +0200
@@ -31,10 +31,10 @@
\newcommand{\norm}[1]{\left\|#1\right\|}
\newcommand{\fnorm}[1]{\left\|#1\right\|}
-\newcommand{\zero}{\mathord{\mathbf 0}}
+\newcommand{\zero}{0}
\newcommand{\plus}{\mathbin{\mathbf +}}
\newcommand{\minus}{\mathbin{\mathbf -}}
-\newcommand{\mult}{\mathbin{\mathbf\odot}}
+\newcommand{\mult}{\cdot}
%%% Local Variables:
%%% mode: latex