# HG changeset patch # User bauerg # Date 963850674 -7200 # Node ID 21cfeae6659d933aeb0bf40a1e2a534b1d8541a8 # Parent 12f251a5a3b5d88f9588fe55fd0351d9140ff5a3 tuded presentation; diff -r 12f251a5a3b5 -r 21cfeae6659d src/HOL/Real/HahnBanach/Aux.thy --- 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 \ B = {v}; x \ A; x \ B |] ==> x = v" +lemma Int_singletonD: "[| A \\ B = {v}; x \\ A; x \\ B |] ==> x = v" by (fast elim: equalityE) -lemma set_less_imp_diff_not_empty: "H < E ==> \x0 \ E. x0 \ H" - by (force simp add: psubset_eq) +lemma set_less_imp_diff_not_empty: "H < E ==> \\x0 \\ E. x0 \\ H" + by (force simp add: psubset_eq) text_raw {* \medskip *} text{* Some lemmas about orders. *} -lemma lt_imp_not_eq: "x < (y::'a::order) ==> x \ y" - by (rule order_less_le[RS iffD1, RS conjunct2]) +lemma lt_imp_not_eq: "x < (y::'a::order) ==> x \\ y" + by (simp add: order_less_le) lemma le_noteq_imp_less: - "[| x <= (r::'a::order); x \ r |] ==> x < r" + "[| x <= (r::'a::order); x \\ r |] ==> x < r" proof - - assume "x <= r" and ne:"x \ r" + assume "x <= r" and ne:"x \\ r" hence "x < r | x = r" by (simp add: order_le_less) with ne show ?thesis by simp qed @@ -116,10 +116,10 @@ thus ?thesis; by simp; qed; -lemma real_mult_inv_right1: "x \ #0 ==> x*rinv(x) = #1" +lemma real_mult_inv_right1: "x \\ #0 ==> x*rinv(x) = #1" by simp -lemma real_mult_inv_left1: "x \ #0 ==> rinv(x) * x = #1" +lemma real_mult_inv_left1: "x \\ #0 ==> rinv(x) * x = #1" by simp lemma real_le_mult_order1a: diff -r 12f251a5a3b5 -r 21cfeae6659d src/HOL/Real/HahnBanach/Bounds.thy --- 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 == \x. x \ A \ (\y \ B. x <= y)" + "is_LowerBound A B == \\x. x \\ A \\ (\\y \\ 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 == \x. x \ A \ (\ y \ B. y <= x)" + "is_UpperBound A B == \\x. x \\ A \\ (\\y \\ 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 (\x. P))" + "UPPER_BOUNDS x:A. P" == "UpperBounds A (Collect (\\x. P))" "UPPER_BOUNDS x. P" == "UPPER_BOUNDS x:UNIV. P" - "LOWER_BOUNDS x:A. P" == "LowerBounds A (Collect (\x. P))" + "LOWER_BOUNDS x:A. P" == "LowerBounds A (Collect (\\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 \ A \ is_Greatest (LowerBounds A B) x" + "is_Inf A B x == x \\ A \\ 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 (\x. P))" + "SUP x:A. P" == "Sup A (Collect (\\x. P))" "SUP x. P" == "SUP x:UNIV. P" - "INF x:A. P" == "Inf A (Collect (\x. P))" + "INF x:A. P" == "Inf A (Collect (\\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 \ B ==> is_Sup A B s ==> y <= s" +lemma sup_ub: "y \\ 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: - "[| \ y \ B. a <= y; is_Sup A B s; x \ B |] ==> a <= s" + "[| \\y \\ B. a <= y; is_Sup A B s; x \\ B |] ==> a <= s" proof - - assume "\ y \ B. a <= y" "is_Sup A B s" "x \ B" + assume "\\y \\ B. a <= y" "is_Sup A B s" "x \\ B" have "a <= x" by (rule bspec) also have "x <= s" by (rule sup_ub) finally show "a <= s" . diff -r 12f251a5a3b5 -r 21cfeae6659d src/HOL/Real/HahnBanach/FunctionNorm.thy --- 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 \ (\c. \x \ V. |f x| <= c * norm x)" + is_linearform V f \\ (\\c. \\x \\ V. |f x| <= c * norm x)" lemma continuousI [intro]: - "[| is_linearform V f; !! x. x \ V ==> |f x| <= c * norm x |] + "[| is_linearform V f; !! x. x \\ V ==> |f x| <= c * norm x |] ==> is_continuous V norm f" proof (unfold is_continuous_def, intro exI conjI ballI) - assume r: "!! x. x \ V ==> |f x| <= c * norm x" - fix x assume "x \ V" show "|f x| <= c * norm x" by (rule r) + assume r: "!! x. x \\ V ==> |f x| <= c * norm x" + fix x assume "x \\ 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 - ==> \c. \x \ V. |f x| <= c * norm x" + ==> \\c. \\x \\ 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} \ {|f x| * rinv (norm x) | x. x \ 0 \ x \ V}" + {#0} \\ {|f x| * rinv (norm x) | x. x \\ 0 \\ x \\ 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" ("\_\_,_") + function_norm :: " ['a => real, 'a set, 'a => real] => real" ("\\_\\_,_") -lemma B_not_empty: "#0 \ B V norm f" +lemma B_not_empty: "#0 \\ 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 \f\V,norm" + ==> is_function_norm f V norm \\f\\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: "\c. \x \ V. |f x| <= c * norm x" + and e: "\\c. \\x \\ 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 "\a. is_Sup UNIV (B V norm f) a" + show "\\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 "\X. X \ B V norm f" + show "\\X. X \\ B V norm f" proof (intro exI) - show "#0 \ (B V norm f)" by (unfold B_def, force) + show "#0 \\ (B V norm f)" by (unfold B_def, force) qed txt {* Then we have to show that $B$ is bounded: *} - from e show "\Y. isUb UNIV (B V norm f) Y" + from e show "\\Y. isUb UNIV (B V norm f) Y" proof txt {* We know that $f$ is bounded by some value $c$. *} - fix c assume a: "\x \ V. |f x| <= c * norm x" + fix c assume a: "\\x \\ 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 \ V" "x \ 0" (*** + assume "x \\ V" "x \\ 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 \ #0" + have nz: "norm x \\ #0" by (rule not_sym, rule lt_imp_not_eq, rule normed_vs_norm_gt_zero) (*** proof (rule not_sym); - show "#0 \ norm x"; + show "#0 \\ 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 \ #0" + show nz: "norm x \\ #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 <= \f\V,norm" + ==> #0 <= \\f\\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 "\x \ (B V norm f). #0 <= x" + show "\\x \\ (B V norm f). #0 <= x" proof (intro ballI, unfold B_def, elim UnE singletonE CollectE exE conjE) fix x r - assume "x \ V" "x \ 0" + assume "x \\ V" "x \\ 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 \f\V,norm" .. + have "is_function_norm f V norm \\f\\V,norm" .. thus "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))" by (unfold is_function_norm_def function_norm_def) txt {* $B$ is non-empty by construction: *} - show "#0 \ B V norm f" by (rule B_not_empty) + show "#0 \\ 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 \ V |] - ==> |f x| <= \f\V,norm * norm x" + "[| is_continuous V norm f; is_normed_vectorspace V norm; x \\ V |] + ==> |f x| <= \\f\\V,norm * norm x" proof - - assume "is_normed_vectorspace V norm" "x \ V" + assume "is_normed_vectorspace V norm" "x \\ 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 <= \f\V,norm * norm x" + also have "#0 <= \\f\\V,norm * norm x" proof (rule real_le_mult_order1a) - show "#0 <= \f\V,norm" .. + show "#0 <= \\f\\V,norm" .. show "#0 <= norm x" .. qed finally - show "|f x| <= \f\V,norm * norm x" . + show "|f x| <= \\f\\V,norm * norm x" . next - assume "x \ 0" - have n: "#0 <= norm x" .. - have nz: "norm x \ #0" - proof (rule lt_imp_not_eq [RS not_sym]) - show "#0 < norm x" .. - qed + assume "x \\ 0" + have n: "#0 < norm x" .. + hence nz: "norm x \\ #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) <= \f\V,norm" + have l: "|f x| * rinv (norm x) <= \\f\\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) \ B V norm f" + show "|f x| * rinv (norm x) \\ 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 "... <= \f\V,norm * norm x" - by (rule real_mult_le_le_mono2 [OF n l]) - finally - show "|f x| <= \f\V,norm * norm x" . + also from n l have "... <= \\f\\V,norm * norm x" + by (simp add: real_mult_le_le_mono2) + finally show "|f x| <= \\f\\V,norm * norm x" . qed qed @@ -318,13 +314,13 @@ lemma fnorm_le_ub: "[| is_continuous V norm f; is_normed_vectorspace V norm; - \x \ V. |f x| <= c * norm x; #0 <= c |] - ==> \f\V,norm <= c" + \\x \\ V. |f x| <= c * norm x; #0 <= c |] + ==> \\f\\V,norm <= c" proof (unfold function_norm_def) assume "is_normed_vectorspace V norm" assume c: "is_continuous V norm f" - assume fb: "\x \ V. |f x| <= c * norm x" - and "#0 <= c" + assume fb: "\\x \\ 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 \ B V norm f" + fix y assume "y \\ 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 \ V" "x \ 0" + assume "x \\ V" "x \\ 0" have lz: "#0 < norm x" by (simp! add: normed_vs_norm_gt_zero) - have nz: "norm x \ #0" + have nz: "norm x \\ #0" proof (rule not_sym) - from lz show "#0 \ norm x" + from lz show "#0 \\ norm x" by (simp! add: order_less_imp_not_eq) qed diff -r 12f251a5a3b5 -r 21cfeae6659d src/HOL/Real/HahnBanach/FunctionOrder.thy --- 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 \ F}" + "graph F f == {(x, f x) | x. x \\ F}" -lemma graphI [intro??]: "x \ F ==> (x, f x) \ graph F f" +lemma graphI [intro??]: "x \\ F ==> (x, f x) \\ graph F f" by (unfold graph_def, intro CollectI exI) force -lemma graphI2 [intro??]: "x \ F ==> \t\ (graph F f). t = (x, f x)" +lemma graphI2 [intro??]: "x \\ F ==> \\t\\ (graph F f). t = (x, f x)" by (unfold graph_def, force) -lemma graphD1 [intro??]: "(x, y) \ graph F f ==> x \ F" +lemma graphD1 [intro??]: "(x, y) \\ graph F f ==> x \\ F" by (unfold graph_def, elim CollectE exE) force -lemma graphD2 [intro??]: "(x, y) \ graph H h ==> y = h x" +lemma graphD2 [intro??]: "(x, y) \\ graph H h ==> y = h x" by (unfold graph_def, elim CollectE exE) force subsection {* Functions ordered by domain extension *} @@ -42,12 +42,12 @@ $h$ is a subset of the graph of $h'$.*} lemma graph_extI: - "[| !! x. x \ H ==> h x = h' x; H <= H'|] + "[| !! x. x \\ H ==> h x = h' x; H <= H'|] ==> graph H h <= graph H' h'" by (unfold graph_def, force) lemma graph_extD1 [intro??]: - "[| graph H h <= graph H' h'; x \ H |] ==> h x = h' x" + "[| graph H h <= graph H' h'; x \\ 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. \y. (x, y) \ g}" + "domain g == {x. \\y. (x, y) \\ g}" funct :: "'a graph => ('a => real)" - "funct g == \x. (SOME y. (x, y) \ g)" + "funct g == \\x. (SOME y. (x, y) \\ 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) \ g ==> (x, z) \ g ==> z = y) + "(!!x y z. (x, y) \\ g ==> (x, z) \\ g ==> z = y) ==> graph (domain g) (funct g) = g" proof (unfold domain_def funct_def graph_def, auto) - fix a b assume "(a, b) \ g" - show "(a, SOME y. (a, y) \ g) \ g" by (rule selectI2) - show "\y. (a, y) \ g" .. - assume uniq: "!!x y z. (x, y) \ g ==> (x, z) \ g ==> z = y" - show "b = (SOME y. (a, y) \ g)" + fix a b assume "(a, b) \\ g" + show "(a, SOME y. (a, y) \\ g) \\ g" by (rule selectI2) + show "\\y. (a, y) \\ g" .. + assume uniq: "!!x y z. (x, y) \\ g ==> (x, z) \\ g ==> z = y" + show "b = (SOME y. (a, y) \\ g)" proof (rule select_equality [RS sym]) - fix y assume "(a, y) \ g" show "y = b" by (rule uniq) + fix y assume "(a, y) \\ 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. \H h. graph H h = g - \ is_linearform H h - \ is_subspace H E - \ is_subspace F H - \ graph F f <= graph H h - \ (\x \ H. h x <= p x)}" + == {g. \\H h. graph H h = g + \\ is_linearform H h + \\ is_subspace H E + \\ is_subspace F H + \\ graph F f <= graph H h + \\ (\\x \\ H. h x <= p x)}" lemma norm_pres_extension_D: - "g \ norm_pres_extensions E p F f - ==> \H h. graph H h = g - \ is_linearform H h - \ is_subspace H E - \ is_subspace F H - \ graph F f <= graph H h - \ (\x \ H. h x <= p x)" + "g \\ norm_pres_extensions E p F f + ==> \\H h. graph H h = g + \\ is_linearform H h + \\ is_subspace H E + \\ is_subspace F H + \\ graph F f <= graph H h + \\ (\\x \\ 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; \x \ H. h x <= p x |] - ==> (graph H h \ norm_pres_extensions E p F f)" + graph F f <= graph H h; \\x \\ H. h x <= p x |] + ==> (graph H h \\ norm_pres_extensions E p F f)" by (unfold norm_pres_extensions_def) force lemma norm_pres_extensionI [intro]: - "\H h. graph H h = g - \ is_linearform H h - \ is_subspace H E - \ is_subspace F H - \ graph F f <= graph H h - \ (\x \ H. h x <= p x) - ==> g\ norm_pres_extensions E p F f" + "\\H h. graph H h = g + \\ is_linearform H h + \\ is_subspace H E + \\ is_subspace F H + \\ graph F f <= graph H h + \\ (\\x \\ H. h x <= p x) + ==> g \\ norm_pres_extensions E p F f" by (unfold norm_pres_extensions_def) force end \ No newline at end of file diff -r 12f251a5a3b5 -r 21cfeae6659d src/HOL/Real/HahnBanach/HahnBanach.thy --- 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; \x \ F. f x \ p x |] - ==> \h. is_linearform E h \ (\x \ F. h x = f x) \ (\x \ E. h x \ p x)" + is_linearform F f; \\x \\ F. f x <= p x |] + ==> \\h. is_linearform E h \\ (\\x \\ F. h x = f x) + \\ (\\x \\ 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" "\x \ F. f x \ p x" + and "is_linearform F f" "\\x \\ 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 \ chain M" "\x. x \ c" - have "\ c \ M" + fix c assume "c \\ chain M" "\\x. x \\ c" + have "\\ c \\ 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 "\H h. graph H h = \ c - \ is_linearform H h - \ is_subspace H E - \ is_subspace F H - \ graph F f \ graph H h - \ (\x \ H. h x \ p x)" + show "\\H h. graph H h = \\ c + \\ is_linearform H h + \\ is_subspace H E + \\ is_subspace F H + \\ graph F f \\ graph H h + \\ (\\x \\ H. h x <= p x)" proof (intro exI conjI) - let ?H = "domain (\ c)" - let ?h = "funct (\ c)" + let ?H = "domain (\\ c)" + let ?h = "funct (\\ c)" - show a: "graph ?H ?h = \ c" + show a: "graph ?H ?h = \\ c" proof (rule graph_domain_funct) - fix x y z assume "(x, y) \ \ c" "(x, z) \ \ c" + fix x y z assume "(x, y) \\ \\ c" "(x, z) \\ \\ 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 \ graph ?H ?h" + show "graph F f \\ graph ?H ?h" by (rule sup_ext, rule a) (simp!)+ - show "\x \ ?H. ?h x \ p x" + show "\\x \\ ?H. ?h x <= p x" by (rule sup_norm_pres, rule a) (simp!)+ qed qed } - hence "\g \ M. \x \ M. g \ x --> g = x" + hence "\\g \\ M. \\x \\ M. g \\ 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 \ norm_pres_extensions E p F f" + have "graph F f \\ 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 \ M" by (simp!) + thus "graph F f \\ M" by (simp!) qed thus ?thesis proof - fix g assume "g \ M" "\x \ M. g \ x --> g = x" + fix g assume "g \\ M" "\\x \\ M. g \\ 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 \ graph H h" - "\x \ H. h x \ p x" + "is_subspace H E" "is_subspace F H" "graph F f \\ graph H h" + "\\x \\ 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 "\ H h. graph H h = g \ is_linearform H h - \ is_subspace H E \ is_subspace F H - \ graph F f \ graph H h - \ (\x \ H. h x \ p x)" by (simp! add: norm_pres_extension_D) + have "\\H h. graph H h = g \\ is_linearform H h + \\ is_subspace H E \\ is_subspace F H + \\ graph F f \\ graph H h + \\ (\\x \\ 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 \ E" + assume "H \\ 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 "\g' \ M. g \ g' \ g \ g'" - obtain x' where "x' \ E" "x' \ H" + have "\\g' \\ M. g \\ g' \\ g \\ g'" + obtain x' where "x' \\ E" "x' \\ H" -- {* Pick $x' \in E \setminus H$. \skp *} proof - - have "\x' \ E. x' \ H" + have "\\x' \\ E. x' \\ H" proof (rule set_less_imp_diff_not_empty) - have "H \ E" .. - thus "H \ E" .. + have "H \\ E" .. + thus "H \\ E" .. qed thus ?thesis by blast qed - have x': "x' \ 0" + have x': "x' \\ 0" proof (rule classical) presume "x' = 0" - with h have "x' \ H" by simp + with h have "x' \\ 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 "\y \ H. - p (y + x') - h y \ xi - \ xi \ p (y + x') - h y" + obtain xi where "\\y \\ H. - p (y + x') - h y <= xi + \\ 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 "\xi. \y \ H. - p (y + x') - h y <= xi - \ xi <= p (y + x') - h y" + from h have "\\xi. \\y \\ H. - p (y + x') - h y <= xi + \\ xi <= p (y + x') - h y" proof (rule ex_xi) - fix u v assume "u \ H" "v \ H" + fix u v assume "u \\ H" "v \\ 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' == "\x. let (y,a) = SOME (y,a). x = y + a \ x' \ y \ H + def h' == "\\x. let (y,a) = SOME (y,a). x = y + a \\ x' \\ y \\ H in (h y) + a * xi" -- {* Define the extension $h'$ of $h$ to $H'$ using $\xi$. \skp *} show ?thesis proof - show "g \ graph H' h' \ g \ graph H' h'" + show "g \\ graph H' h' \\ g \\ graph H' h'" -- {* Show that $h'$ is an extension of $h$ \dots \skp *} proof - show "g \ graph H' h'" + show "g \\ graph H' h'" proof - - have "graph H h \ graph H' h'" + have "graph H h \\ graph H' h'" proof (rule graph_extI) - fix t assume "t \ H" - have "(SOME (y, a). t = y + a \ x' \ y \ H) + fix t assume "t \\ H" + have "(SOME (y, a). t = y + a \\ x' \\ y \\ H) = (t, #0)" by (rule decomp_H'_H) (assumption+, rule x'); thus "h t = h' t" by (simp! add: Let_def) next - show "H \ H'" + show "H \\ 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 \ graph H' h'" + show "g \\ graph H' h'" proof - - have "graph H h \ graph H' h'" + have "graph H h \\ graph H' h'" proof assume e: "graph H h = graph H' h'" - have "x' \ H'" + have "x' \\ H'" proof (unfold H'_def, rule vs_sumI) show "x' = 0 + x'" by (simp!) - from h show "0 \ H" .. - show "x' \ lin x'" by (rule x_lin_x) + from h show "0 \\ H" .. + show "x' \\ lin x'" by (rule x_lin_x) qed - hence "(x', h' x') \ graph H' h'" .. - with e have "(x', h' x') \ graph H h" by simp - hence "x' \ H" .. + hence "(x', h' x') \\ graph H' h'" .. + with e have "(x', h' x') \\ graph H h" by simp + hence "x' \\ H" .. thus False by contradiction qed thus ?thesis by (simp!) qed qed - show "graph H' h' \ M" + show "graph H' h' \\ M" -- {* and $h'$ is norm-preserving. \skp *} proof - - have "graph H' h' \ norm_pres_extensions E p F f" + have "graph H' h' \\ 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 \ graph H' h'" + show "graph F f \\ graph H' h'" proof (rule graph_extI) - fix x assume "x \ F" + fix x assume "x \\ 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 \ x' \ y \ H)" - proof (rule decomp_H'_H [RS sym]) qed (simp! add: x')+ + "(x, #0) = (SOME (y, a). x = y + a \\ x' \\ y \\ H)" + by (rule decomp_H'_H [RS sym]) (simp! add: x')+ also have - "(let (y,a) = (SOME (y,a). x = y + a \ x' \ y \ H) - in h y + a * xi) - = h' x" by (simp!) + "(let (y,a) = (SOME (y,a). x = y + a \\ x' \\ y \\ H) + in h y + a * xi) = h' x" by (simp!) finally show "f x = h' x" . next - from f_h' show "F \ H'" .. + from f_h' show "F \\ H'" .. qed - show "\x \ H'. h' x \ p x" + show "\\x \\ H'. h' x <= p x" by (rule h'_norm_pres) (assumption+, rule x') qed - thus "graph H' h' \ M" by (simp!) + thus "graph H' h' \\ M" by (simp!) qed qed qed qed - hence "\ (\x \ M. g \ x --> g = x)" by simp + hence "\\ (\\x \\ M. g \\ x --> g = x)" by simp -- {* So the graph $g$ of $h$ cannot be maximal. Contradiction! \skp *} thus "H = E" by contradiction qed - thus "\h. is_linearform E h \ (\x \ F. h x = f x) - \ (\x \ E. h x \ p x)" + thus "\\h. is_linearform E h \\ (\\x \\ F. h x = f x) + \\ (\\x \\ E. h x <= p x)" proof (intro exI conjI) assume eq: "H = E" from eq show "is_linearform E h" by (simp!) - show "\x \ F. h x = f x" + show "\\x \\ F. h x = f x" proof (intro ballI, rule sym) - fix x assume "x \ F" show "f x = h x " .. + fix x assume "x \\ F" show "f x = h x " .. qed - from eq show "\x \ E. h x \ p x" by (force!) + from eq show "\\x \\ 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; \x \ F. |f x| <= p x |] - ==> \g. is_linearform E g \ (\x \ F. g x = f x) - \ (\x \ E. |g x| <= p x)" + is_seminorm E p; \\x \\ F. |f x| <= p x |] + ==> \\g. is_linearform E g \\ (\\x \\ F. g x = f x) + \\ (\\x \\ E. |g x| <= p x)" proof - assume "is_vectorspace E" "is_subspace F E" "is_seminorm E p" - "is_linearform F f" "\x \ F. |f x| <= p x" - have "\x \ F. f x <= p x" by (rule abs_ineq_iff [RS iffD1]) - hence "\g. is_linearform E g \ (\x \ F. g x = f x) - \ (\x \ E. g x <= p x)" + "is_linearform F f" "\\x \\ F. |f x| <= p x" + have "\\x \\ F. f x <= p x" by (rule abs_ineq_iff [RS iffD1]) + hence "\\g. is_linearform E g \\ (\\x \\ F. g x = f x) + \\ (\\x \\ E. g x <= p x)" by (simp! only: HahnBanach) thus ?thesis proof (elim exE conjE) - fix g assume "is_linearform E g" "\x \ F. g x = f x" - "\x \ E. g x <= p x" - hence "\x \ E. |g x| <= p x" + fix g assume "is_linearform E g" "\\x \\ F. g x = f x" + "\\x \\ E. g x <= p x" + hence "\\x \\ 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 |] - ==> \g. is_linearform E g - \ is_continuous E norm g - \ (\x \ F. g x = f x) - \ \g\E,norm = \f\F,norm" + ==> \\g. is_linearform E g + \\ is_continuous E norm g + \\ (\\x \\ F. g x = f x) + \\ \\g\\E,norm = \\f\\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 == "\x. \f\F,norm * norm x" + def p == "\\x. \\f\\F,norm * norm x" txt{* $p$ is a seminorm on $E$: *} have q: "is_seminorm E p" proof - fix x y a assume "x \ E" "y \ E" + fix x y a assume "x \\ E" "y \\ 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 <= \f\F,norm" .. + proof (unfold p_def, rule real_le_mult_order1a) + from f_cont f_norm show "#0 <= \\f\\F,norm" .. show "#0 <= norm x" .. qed txt{* $p$ is absolutely homogenous: *} - show "p (a \ x) = |a| * p x" + show "p (a \\ x) = |a| * p x" proof - - have "p (a \ x) = \f\F,norm * norm (a \ x)" + have "p (a \\ x) = \\f\\F,norm * norm (a \\ x)" by (simp!) - also have "norm (a \ x) = |a| * norm x" + also have "norm (a \\ x) = |a| * norm x" by (rule normed_vs_norm_abs_homogenous) - also have "\f\F,norm * ( |a| * norm x ) - = |a| * (\f\F,norm * norm x)" + also have "\\f\\F,norm * ( |a| * norm x ) + = |a| * (\\f\\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) = \f\F,norm * norm (x + y)" + have "p (x + y) = \\f\\F,norm * norm (x + y)" by (simp!) also - have "... <= \f\F,norm * (norm x + norm y)" + have "... <= \\f\\F,norm * (norm x + norm y)" proof (rule real_mult_le_le_mono1a) - from f_cont f_norm show "#0 <= \f\F,norm" .. + from f_cont f_norm show "#0 <= \\f\\F,norm" .. show "norm (x + y) <= norm x + norm y" .. qed - also have "... = \f\F,norm * norm x - + \f\F,norm * norm y" + also have "... = \\f\\F,norm * norm x + + \\f\\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 "\x \ F. |f x| <= p x" + have "\\x \\ F. |f x| <= p x" proof - fix x assume "x \ F" + fix x assume "x \\ 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 "\g. is_linearform E g \ (\x \ F. g x = f x) - \ (\x \ E. |g x| <= p x)" + have "\\g. is_linearform E g \\ (\\x \\ F. g x = f x) + \\ (\\x \\ 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: "\x \ F. g x = f x" - and b: "\x \ E. |g x| <= p x" + assume "is_linearform E g" and a: "\\x \\ F. g x = f x" + and b: "\\x \\ E. |g x| <= p x" - show "\g. is_linearform E g - \ is_continuous E norm g - \ (\x \ F. g x = f x) - \ \g\E,norm = \f\F,norm" + show "\\g. is_linearform E g + \\ is_continuous E norm g + \\ (\\x \\ F. g x = f x) + \\ \\g\\E,norm = \\f\\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 \ E" - with b show "|g x| <= \f\F,norm * norm x" + fix x assume "x \\ E" + with b show "|g x| <= \\f\\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 "\g\E,norm = \f\F,norm" + show "\\g\\E,norm = \\f\\F,norm" (is "?L = ?R") proof (rule order_antisym) @@ -479,36 +482,36 @@ \end{matharray} *} - have "\x \ E. |g x| <= \f\F,norm * norm x" + have "\\x \\ E. |g x| <= \\f\\F,norm * norm x" proof - fix x assume "x \ E" - show "|g x| <= \f\F,norm * norm x" + fix x assume "x \\ E" + show "|g x| <= \\f\\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 <= \f\F,norm" .. + from f_cont f_norm show "#0 <= \\f\\F,norm" .. qed txt{* The other direction is achieved by a similar argument. *} - have "\x \ F. |f x| <= \g\E,norm * norm x" + have "\\x \\ F. |f x| <= \\g\\E,norm * norm x" proof - fix x assume "x \ F" + fix x assume "x \\ F" from a have "g x = f x" .. hence "|f x| = |g x|" by simp also from g_cont - have "... <= \g\E,norm * norm x" + have "... <= \\g\\E,norm * norm x" proof (rule norm_fx_le_norm_f_norm_x) - show "x \ E" .. + show "x \\ E" .. qed - finally show "|f x| <= \g\E,norm * norm x" . + finally show "|f x| <= \\g\\E,norm * norm x" . qed thus "?R <= ?L" proof (rule fnorm_le_ub [OF f_cont f_norm]) - from g_cont show "#0 <= \g\E,norm" .. + from g_cont show "#0 <= \\g\\E,norm" .. qed qed qed diff -r 12f251a5a3b5 -r 21cfeae6659d src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy --- 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 \ F; v \ F |] ==> a u <= b v |] - ==> \xi::real. \y \ F. a y <= xi \ xi <= b y"; + "[| is_vectorspace F; !! u v. [| u \\ F; v \\ F |] ==> a u <= b v |] + ==> \\xi::real. \\y \\ F. a y <= xi \\ xi <= b y"; proof -; assume vs: "is_vectorspace F"; - assume r: "(!! u v. [| u \ F; v \ F |] ==> a u <= (b v::real))"; + assume r: "(!! u v. [| u \\ F; v \\ F |] ==> a u <= (b v::real))"; txt {* From the completeness of the reals follows: The set $S = \{a\: u\dt\: u\in F\}$ has a supremum, if it is non-empty and has an upper bound. *}; - let ?S = "{a u :: real | u. u \ F}"; + let ?S = "{a u :: real | u. u \\ F}"; - have "\xi. isLub UNIV ?S xi"; + have "\\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 \ ?S"; by force; - thus "\X. X \ ?S"; ..; + from vs; have "a 0 \\ ?S"; by force; + thus "\\X. X \\ ?S"; ..; txt {* $b\ap \zero$ is an upper bound of $S$: *}; - show "\Y. isUb UNIV ?S Y"; + show "\\Y. isUb UNIV ?S Y"; proof; show "isUb UNIV ?S (b 0)"; proof (intro isUbI setleI ballI); - show "b 0 \ UNIV"; ..; + show "b 0 \\ UNIV"; ..; next; txt {* Every element $y\in S$ is less than $b\ap \zero$: *}; - fix y; assume y: "y \ ?S"; - from y; have "\u \ F. y = a u"; by fast; + fix y; assume y: "y \\ ?S"; + from y; have "\\u \\ F. y = a u"; by fast; thus "y <= b 0"; proof; - fix u; assume "u \ F"; + fix u; assume "u \\ 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 "\xi. \y \ F. a y <= xi \ xi <= b y"; + thus "\\xi. \\y \\ F. a y <= xi \\ xi <= b y"; proof (elim exE); fix xi; assume "isLub UNIV ?S xi"; show ?thesis; @@ -87,7 +87,7 @@ txt {* For all $y\in F$ holds $a\ap y \leq \xi$: *}; - fix y; assume y: "y \ F"; + fix y; assume y: "y \\ F"; show "a y <= xi"; proof (rule isUbD); show "isUb UNIV ?S xi"; ..; @@ -96,17 +96,17 @@ txt {* For all $y\in F$ holds $\xi\leq b\ap y$: *}; - fix y; assume "y \ F"; + fix y; assume "y \\ F"; show "xi <= b y"; proof (intro isLub_le_isUb isUbI setleI); - show "b y \ UNIV"; ..; - show "\ya \ ?S. ya <= b y"; + show "b y \\ UNIV"; ..; + show "\\ya \\ ?S. ya <= b y"; proof; - fix au; assume au: "au \ ?S "; - hence "\u \ F. au = a u"; by fast; + fix au; assume au: "au \\ ?S "; + hence "\\u \\ F. au = a u"; by fast; thus "au <= b y"; proof; - fix u; assume "u \ F"; assume "au = a u"; + fix u; assume "u \\ 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' == (\x. let (y, a) = SOME (y, a). x = y + a \ x0 \ y \ H + "[| h' == (\\x. let (y, a) = SOME (y, a). x = y + a \\ x0 \\ y \\ H in h y + a * xi); - H' == H + lin x0; is_subspace H E; is_linearform H h; x0 \ H; - x0 \ E; x0 \ 0; is_vectorspace E |] + H' == H + lin x0; is_subspace H E; is_linearform H h; x0 \\ H; + x0 \\ E; x0 \\ 0; is_vectorspace E |] ==> is_linearform H' h'"; proof -; assume h'_def: - "h' == (\x. let (y, a) = SOME (y, a). x = y + a \ x0 \ y \ H + "h' == (\\x. let (y, a) = SOME (y, a). x = y + a \\ x0 \\ y \\ H in h y + a * xi)" and H'_def: "H' == H + lin x0" - and vs: "is_subspace H E" "is_linearform H h" "x0 \ H" - "x0 \ 0" "x0 \ E" "is_vectorspace E"; + and vs: "is_subspace H E" "is_linearform H h" "x0 \\ H" + "x0 \\ 0" "x0 \\ 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 \ H'" and x2: "x2 \ H'"; + fix x1 x2; assume x1: "x1 \\ H'" and x2: "x2 \\ 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 \ H'"; + have x1x2: "x1 + x2 \\ H'"; by (rule vs_add_closed, rule h'); from x1; - have ex_x1: "\ y1 a1. x1 = y1 + a1 \ x0 \ y1 \ H"; + have ex_x1: "\\y1 a1. x1 = y1 + a1 \\ x0 \\ y1 \\ H"; by (unfold H'_def vs_sum_def lin_def) fast; from x2; - have ex_x2: "\ y2 a2. x2 = y2 + a2 \ x0 \ y2 \ H"; + have ex_x2: "\\y2 a2. x2 = y2 + a2 \\ x0 \\ y2 \\ H"; by (unfold H'_def vs_sum_def lin_def) fast; from x1x2; - have ex_x1x2: "\ y a. x1 + x2 = y + a \ x0 \ y \ H"; + have ex_x1x2: "\\y a. x1 + x2 = y + a \\ x0 \\ y \\ 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 \ x0" and y1': "y1 \ H" - and y2: "x2 = y2 + a2 \ x0" and y2': "y2 \ H" - and y: "x1 + x2 = y + a \ x0" and y': "y \ H"; - - have ya: "y1 + y2 = y \ a1 + a2 = a"; - proof (rule decomp_H');; - txt_raw {* \label{decomp-H-use} *};; - show "y1 + y2 + (a1 + a2) \ x0 = y + a \ x0"; + assume y1: "x1 = y1 + a1 \\ x0" and y1': "y1 \\ H" + and y2: "x2 = y2 + a2 \\ x0" and y2': "y2 \\ H" + and y: "x1 + x2 = y + a \\ x0" and y': "y \\ H"; + txt {* \label{decomp-H-use}*} + have ya: "y1 + y2 = y \\ a1 + a2 = a"; + proof (rule decomp_H') + show "y1 + y2 + (a1 + a2) \\ x0 = y + a \\ x0"; by (simp! add: vs_add_mult_distrib2 [of E]); - show "y1 + y2 \ H"; ..; + show "y1 + y2 \\ 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 \ H'"; - have ax1: "c \ x1 \ H'"; + fix c x1; assume x1: "x1 \\ H'"; + have ax1: "c \\ x1 \\ H'"; by (rule vs_mult_closed, rule h'); - from x1; have ex_x: "!! x. x\ H' - ==> \ y a. x = y + a \ x0 \ y \ H"; + from x1; + have ex_x: "!! x. x\\ H' ==> \\y a. x = y + a \\ x0 \\ y \\ H"; by (unfold H'_def vs_sum_def lin_def) fast; - from x1; have ex_x1: "\ y1 a1. x1 = y1 + a1 \ x0 \ y1 \ H"; + from x1; have ex_x1: "\\y1 a1. x1 = y1 + a1 \\ x0 \\ y1 \\ H"; by (unfold H'_def vs_sum_def lin_def) fast; - with ex_x [of "c \ x1", OF ax1]; - show "h' (c \ x1) = c * (h' x1)"; + with ex_x [of "c \\ x1", OF ax1]; + show "h' (c \\ x1) = c * (h' x1)"; proof (elim exE conjE); fix y1 y a1 a; - assume y1: "x1 = y1 + a1 \ x0" and y1': "y1 \ H" - and y: "c \ x1 = y + a \ x0" and y': "y \ H"; + assume y1: "x1 = y1 + a1 \\ x0" and y1': "y1 \\ H" + and y: "c \\ x1 = y + a \\ x0" and y': "y \\ H"; - have ya: "c \ y1 = y \ c * a1 = a"; + have ya: "c \\ y1 = y \\ c * a1 = a"; proof (rule decomp_H'); - show "c \ y1 + (c * a1) \ x0 = y + a \ x0"; + show "c \\ y1 + (c * a1) \\ x0 = y + a \\ x0"; by (simp! add: vs_add_mult_distrib1); - show "c \ y1 \ H"; ..; + show "c \\ y1 \\ H"; ..; qed; - have "h' (c \ x1) = h y + a * xi"; + have "h' (c \\ x1) = h y + a * xi"; by (rule h'_definite); - also; have "... = h (c \ y1) + (c * a1) * xi"; + also; have "... = h (c \\ 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' == (\x. let (y, a) = SOME (y, a). x = y + a \ x0 \ y \ H - in h y + a * xi); - H' == H + lin x0; x0 \ H; x0 \ E; x0 \ 0; is_vectorspace E; - is_subspace H E; is_seminorm E p; is_linearform H h; \y \ H. h y <= p y; - \y \ H. - p (y + x0) - h y <= xi \ xi <= p (y + x0) - h y |] - ==> \ x \ H'. h' x <= p x"; + "[| h' == (\\x. let (y, a) = SOME (y, a). x = y + a \\ x0 \\ y \\ H + in h y + a * xi); + H' == H + lin x0; x0 \\ H; x0 \\ E; x0 \\ 0; is_vectorspace E; + is_subspace H E; is_seminorm E p; is_linearform H h; + \\y \\ H. h y <= p y; + \\y \\ H. - p (y + x0) - h y <= xi \\ xi <= p (y + x0) - h y |] + ==> \\x \\ H'. h' x <= p x"; proof; assume h'_def: - "h' == (\x. let (y, a) = SOME (y, a). x = y + a \ x0 \ y \ H + "h' == (\\x. let (y, a) = SOME (y, a). x = y + a \\ x0 \\ y \\ H in (h y) + a * xi)" and H'_def: "H' == H + lin x0" - and vs: "x0 \ H" "x0 \ E" "x0 \ 0" "is_vectorspace E" + and vs: "x0 \\ H" "x0 \\ E" "x0 \\ 0" "is_vectorspace E" "is_subspace H E" "is_seminorm E p" "is_linearform H h" - and a: "\y \ H. h y <= p y"; - presume a1: "\ya \ H. - p (ya + x0) - h ya <= xi"; - presume a2: "\ya \ H. xi <= p (ya + x0) - h ya"; - fix x; assume "x \ H'"; + and a: "\\y \\ H. h y <= p y"; + presume a1: "\\ya \\ H. - p (ya + x0) - h ya <= xi"; + presume a2: "\\ya \\ H. xi <= p (ya + x0) - h ya"; + fix x; assume "x \\ H'"; have ex_x: - "!! x. x \ H' ==> \y a. x = y + a \ x0 \ y \ H"; + "!! x. x \\ H' ==> \\y a. x = y + a \\ x0 \\ y \\ H"; by (unfold H'_def vs_sum_def lin_def) fast; - have "\y a. x = y + a \ x0 \ y \ H"; + have "\\y a. x = y + a \\ x0 \\ y \\ H"; by (rule ex_x); thus "h' x <= p x"; proof (elim exE conjE); - fix y a; assume x: "x = y + a \ x0" and y: "y \ H"; + fix y a; assume x: "x = y + a \\ x0" and y: "y \\ 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 \ x0)"; + also; have "... <= p (y + a \\ 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 \ #0"; by simp; + assume lz: "a < #0"; hence nz: "a \\ #0"; by simp; from a1; - have "- p (rinv a \ y + x0) - h (rinv a \ y) <= xi"; + have "- p (rinv a \\ y + x0) - h (rinv a \\ 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 \ y + x0) - h (rinv a \ y))"; + hence "a * xi <= a * (- p (rinv a \\ y + x0) - h (rinv a \\ y))"; by (rule real_mult_less_le_anti [OF lz]); - also; have "... = - a * (p (rinv a \ y + x0)) - - a * (h (rinv a \ y))"; + also; + have "... = - a * (p (rinv a \\ y + x0)) - a * (h (rinv a \\ y))"; by (rule real_mult_diff_distrib); - also; from lz vs y; have "- a * (p (rinv a \ y + x0)) - = p (a \ (rinv a \ y + x0))"; + also; from lz vs y; + have "- a * (p (rinv a \\ y + x0)) = p (a \\ (rinv a \\ y + x0))"; by (simp add: seminorm_abs_homogenous abs_minus_eqI2); - also; from nz vs y; have "... = p (y + a \ x0)"; + also; from nz vs y; have "... = p (y + a \\ x0)"; by (simp add: vs_add_mult_distrib1); - also; from nz vs y; have "a * (h (rinv a \ y)) = h y"; + also; from nz vs y; have "a * (h (rinv a \\ y)) = h y"; by (simp add: linearform_mult [RS sym]); - finally; have "a * xi <= p (y + a \ x0) - h y"; .; + finally; have "a * xi <= p (y + a \\ x0) - h y"; .; - hence "h y + a * xi <= h y + p (y + a \ x0) - h y"; + hence "h y + a * xi <= h y + p (y + a \\ 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 \ #0"; by simp; - from a2; - have "xi <= p (rinv a \ y + x0) - h (rinv a \ y)"; + assume gz: "#0 < a"; hence nz: "a \\ #0"; by simp; + from a2; have "xi <= p (rinv a \\ y + x0) - h (rinv a \\ 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 \ y + x0) - h (rinv a \ y))"; + with gz; + have "a * xi <= a * (p (rinv a \\ y + x0) - h (rinv a \\ y))"; by (rule real_mult_less_le_mono); - also; have "... = a * p (rinv a \ y + x0) - - a * h (rinv a \ y)"; + also; have "... = a * p (rinv a \\ y + x0) - a * h (rinv a \\ y)"; by (rule real_mult_diff_distrib2); also; from gz vs y; - have "a * p (rinv a \ y + x0) - = p (a \ (rinv a \ y + x0))"; + have "a * p (rinv a \\ y + x0) = p (a \\ (rinv a \\ y + x0))"; by (simp add: seminorm_abs_homogenous abs_eqI2); - also; from nz vs y; - have "... = p (y + a \ x0)"; + also; from nz vs y; have "... = p (y + a \\ x0)"; by (simp add: vs_add_mult_distrib1); - also; from nz vs y; have "a * h (rinv a \ y) = h y"; + also; from nz vs y; have "a * h (rinv a \\ y) = h y"; by (simp add: linearform_mult [RS sym]); - finally; have "a * xi <= p (y + a \ x0) - h y"; .; + finally; have "a * xi <= p (y + a \\ x0) - h y"; .; - hence "h y + a * xi <= h y + (p (y + a \ x0) - h y)"; + hence "h y + a * xi <= h y + (p (y + a \\ x0) - h y)"; by (simp add: real_add_left_cancel_le); thus ?thesis; by simp; qed; diff -r 12f251a5a3b5 -r 21cfeae6659d src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy --- 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 \ chain M; - graph H h = \ c; x \ H |] - ==> \H' h'. graph H' h' \ c \ (x, h x) \ graph H' h' - \ is_linearform H' h' \ is_subspace H' E - \ is_subspace F H' \ graph F f \ graph H' h' - \ (\x \ H'. h' x \ p x)" + "[| M = norm_pres_extensions E p F f; c \\ chain M; + graph H h = \\ c; x \\ H |] + ==> \\H' h'. graph H' h' \\ c \\ (x, h x) \\ graph H' h' + \\ is_linearform H' h' \\ is_subspace H' E + \\ is_subspace F H' \\ graph F f \\ graph H' h' + \\ (\\x \\ H'. h' x <= p x)" proof - - assume m: "M = norm_pres_extensions E p F f" and "c \ chain M" - and u: "graph H h = \ c" "x \ H" + assume m: "M = norm_pres_extensions E p F f" and "c \\ chain M" + and u: "graph H h = \\ c" "x \\ H" - have h: "(x, h x) \ graph H h" .. - with u have "(x, h x) \ \ c" by simp - hence ex1: "\g \ c. (x, h x) \ g" + have h: "(x, h x) \\ graph H h" .. + with u have "(x, h x) \\ \\ c" by simp + hence ex1: "\\g \\ c. (x, h x) \\ g" by (simp only: Union_iff) thus ?thesis proof (elim bexE) - fix g assume g: "g \ c" "(x, h x) \ g" - have "c \ M" by (rule chainD2) - hence "g \ M" .. - hence "g \ norm_pres_extensions E p F f" by (simp only: m) - hence "\H' h'. graph H' h' = g - \ is_linearform H' h' - \ is_subspace H' E - \ is_subspace F H' - \ graph F f \ graph H' h' - \ (\x \ H'. h' x \ p x)" + fix g assume g: "g \\ c" "(x, h x) \\ g" + have "c \\ M" by (rule chainD2) + hence "g \\ M" .. + hence "g \\ norm_pres_extensions E p F f" by (simp only: m) + hence "\\H' h'. graph H' h' = g + \\ is_linearform H' h' + \\ is_subspace H' E + \\ is_subspace F H' + \\ graph F f \\ graph H' h' + \\ (\\x \\ 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 \ graph H' h'" "\x \ H'. h' x \ p x" + "graph F f \\ graph H' h'" "\\x \\ H'. h' x <= p x" show ?thesis proof (intro exI conjI) - show "graph H' h' \ c" by (simp!) - show "(x, h x) \ graph H' h'" by (simp!) + show "graph H' h' \\ c" by (simp!) + show "(x, h x) \\ 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 \ chain M; - graph H h = \ c; x \ H |] - ==> \H' h'. x \ H' \ graph H' h' \ graph H h - \ is_linearform H' h' \ is_subspace H' E \ is_subspace F H' - \ graph F f \ graph H' h' \ (\x \ H'. h' x \ p x)" + "[| M = norm_pres_extensions E p F f; c \\ chain M; + graph H h = \\ c; x \\ H |] + ==> \\H' h'. x \\ H' \\ graph H' h' \\ graph H h + \\ is_linearform H' h' \\ is_subspace H' E \\ is_subspace F H' + \\ graph F f \\ graph H' h' \\ (\\x \\ H'. h' x <= p x)" proof - - assume "M = norm_pres_extensions E p F f" and cM: "c \ chain M" - and u: "graph H h = \ c" "x \ H" + assume "M = norm_pres_extensions E p F f" and cM: "c \\ chain M" + and u: "graph H h = \\ c" "x \\ H" - have "\H' h'. graph H' h' \ c \ (x, h x) \ graph H' h' - \ is_linearform H' h' \ is_subspace H' E - \ is_subspace F H' \ graph F f \ graph H' h' - \ (\x \ H'. h' x \ p x)" + have "\\H' h'. graph H' h' \\ c \\ (x, h x) \\ graph H' h' + \\ is_linearform H' h' \\ is_subspace H' E + \\ is_subspace F H' \\ graph F f \\ graph H' h' + \\ (\\x \\ H'. h' x <= p x)" by (rule some_H'h't) thus ?thesis proof (elim exE conjE) - fix H' h' assume "(x, h x) \ graph H' h'" "graph H' h' \ c" + fix H' h' assume "(x, h x) \\ graph H' h'" "graph H' h' \\ c" "is_linearform H' h'" "is_subspace H' E" "is_subspace F H'" - "graph F f \ graph H' h'" "\x \ H'. h' x \ p x" + "graph F f \\ graph H' h'" "\\x \\ H'. h' x <= p x" show ?thesis proof (intro exI conjI) - show "x \ H'" by (rule graphD1) - from cM u show "graph H' h' \ graph H h" + show "x \\ H'" by (rule graphD1) + from cM u show "graph H' h' \\ 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 \ chain M; - graph H h = \ c; x \ H; y \ H |] - ==> \H' h'. x \ H' \ y \ H' \ graph H' h' \ graph H h - \ is_linearform H' h' \ is_subspace H' E \ is_subspace F H' - \ graph F f \ graph H' h' \ (\x \ H'. h' x \ p x)" + "[| M = norm_pres_extensions E p F f; c \\ chain M; + graph H h = \\ c; x \\ H; y \\ H |] + ==> \\H' h'. x \\ H' \\ y \\ H' \\ graph H' h' \\ graph H h + \\ is_linearform H' h' \\ is_subspace H' E \\ is_subspace F H' + \\ graph F f \\ graph H' h' \\ (\\x \\ H'. h' x <= p x)" proof - - assume "M = norm_pres_extensions E p F f" "c \ chain M" - "graph H h = \ c" "x \ H" "y \ H" + assume "M = norm_pres_extensions E p F f" "c \\ chain M" + "graph H h = \\ c" "x \\ H" "y \\ H" txt {* $x$ is in the domain $H'$ of some function $h'$, such that $h$ extends $h'$. *} - have e1: "\H' h'. graph H' h' \ c \ (x, h x) \ graph H' h' - \ is_linearform H' h' \ is_subspace H' E - \ is_subspace F H' \ graph F f \ graph H' h' - \ (\x \ H'. h' x \ p x)" + have e1: "\\H' h'. graph H' h' \\ c \\ (x, h x) \\ graph H' h' + \\ is_linearform H' h' \\ is_subspace H' E + \\ is_subspace F H' \\ graph F f \\ graph H' h' + \\ (\\x \\ 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: "\H'' h''. graph H'' h'' \ c \ (y, h y) \ graph H'' h'' - \ is_linearform H'' h'' \ is_subspace H'' E - \ is_subspace F H'' \ graph F f \ graph H'' h'' - \ (\x \ H''. h'' x \ p x)" + have e2: "\\H'' h''. graph H'' h'' \\ c \\ (y, h y) \\ graph H'' h'' + \\ is_linearform H'' h'' \\ is_subspace H'' E + \\ is_subspace F H'' \\ graph F f \\ graph H'' h'' + \\ (\\x \\ 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) \ graph H' h'" "graph H' h' \ c" + fix H' h' assume "(y, h y) \\ graph H' h'" "graph H' h' \\ c" "is_linearform H' h'" "is_subspace H' E" "is_subspace F H'" - "graph F f \ graph H' h'" "\x \ H'. h' x \ p x" + "graph F f \\ graph H' h'" "\\x \\ H'. h' x <= p x" - fix H'' h'' assume "(x, h x) \ graph H'' h''" "graph H'' h'' \ c" + fix H'' h'' assume "(x, h x) \\ graph H'' h''" "graph H'' h'' \\ c" "is_linearform H'' h''" "is_subspace H'' E" "is_subspace F H''" - "graph F f \ graph H'' h''" "\x \ H''. h'' x \ p x" + "graph F f \\ graph H'' h''" "\\x \\ 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'' \ graph H' h' | graph H' h' \ graph H'' h''" + have "graph H'' h'' \\ graph H' h' | graph H' h' \\ 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) \ graph H'' h''" . - also have "... \ graph H' h'" . - finally have xh:"(x, h x) \ graph H' h'" . - thus x: "x \ H'" .. - show y: "y \ H'" .. - show "graph H' h' \ graph H h" + have "(x, h x) \\ graph H'' h''" . + also have "... \\ graph H' h'" . + finally have xh:"(x, h x) \\ graph H' h'" . + thus x: "x \\ H'" .. + show y: "y \\ H'" .. + show "graph H' h' \\ graph H h" by (simp! only: chain_ball_Union_upper) qed next assume ?case2 show ?thesis proof (intro exI conjI) - show x: "x \ H''" .. - have "(y, h y) \ graph H' h'" by (simp!) - also have "... \ graph H'' h''" . - finally have yh: "(y, h y) \ graph H'' h''" . - thus y: "y \ H''" .. - show "graph H'' h'' \ graph H h" + show x: "x \\ H''" .. + have "(y, h y) \\ graph H' h'" by (simp!) + also have "... \\ graph H'' h''" . + finally have yh: "(y, h y) \\ graph H'' h''" . + thus y: "y \\ H''" .. + show "graph H'' h'' \\ 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 \ chain M; - (x, y) \ \ c; (x, z) \ \ c |] ==> z = y" + "[| M == norm_pres_extensions E p F f; c \\ chain M; + (x, y) \\ \\ c; (x, z) \\ \\ c |] ==> z = y" proof - - assume "c \ chain M" "M == norm_pres_extensions E p F f" - "(x, y) \ \ c" "(x, z) \ \ c" + assume "c \\ chain M" "M == norm_pres_extensions E p F f" + "(x, y) \\ \\ c" "(x, z) \\ \\ 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) \ G1" "G1 \ c" "(x, z) \ G2" "G2 \ c" "c \ M" + "(x, y) \\ G1" "G1 \\ c" "(x, z) \\ G2" "G2 \\ c" "c \\ M" - have "G1 \ M" .. - hence e1: "\ H1 h1. graph H1 h1 = G1" + have "G1 \\ M" .. + hence e1: "\\H1 h1. graph H1 h1 = G1" by (force! dest: norm_pres_extension_D) - have "G2 \ M" .. - hence e2: "\ H2 h2. graph H2 h2 = G2" + have "G2 \\ M" .. + hence e2: "\\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 \ G2 | G2 \ G1" (is "?case1 | ?case2") .. + have "G1 \\ G2 | G2 \\ G1" (is "?case1 | ?case2") .. thus ?thesis proof assume ?case1 - have "(x, y) \ graph H2 h2" by (force!) + have "(x, y) \\ graph H2 h2" by (force!) hence "y = h2 x" .. - also have "(x, z) \ graph H2 h2" by (simp!) + also have "(x, z) \\ graph H2 h2" by (simp!) hence "z = h2 x" .. finally show ?thesis . next assume ?case2 - have "(x, y) \ graph H1 h1" by (simp!) + have "(x, y) \\ graph H1 h1" by (simp!) hence "y = h1 x" .. - also have "(x, z) \ graph H1 h1" by (force!) + also have "(x, z) \\ 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 \ chain M; - graph H h = \ c |] ==> is_linearform H h" + "[| M = norm_pres_extensions E p F f; c \\ chain M; + graph H h = \\ c |] ==> is_linearform H h" proof - - assume "M = norm_pres_extensions E p F f" "c \ chain M" - "graph H h = \ c" + assume "M = norm_pres_extensions E p F f" "c \\ chain M" + "graph H h = \\ c" show "is_linearform H h" proof - fix x y assume "x \ H" "y \ H" - have "\H' h'. x \ H' \ y \ H' \ graph H' h' \ graph H h - \ is_linearform H' h' \ is_subspace H' E - \ is_subspace F H' \ graph F f \ graph H' h' - \ (\x \ H'. h' x \ p x)" + fix x y assume "x \\ H" "y \\ H" + have "\\H' h'. x \\ H' \\ y \\ H' \\ graph H' h' \\ graph H h + \\ is_linearform H' h' \\ is_subspace H' E + \\ is_subspace F H' \\ graph F f \\ graph H' h' + \\ (\\x \\ 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 \ H'" "y \ H'" - and b: "graph H' h' \ graph H h" + fix H' h' assume "x \\ H'" "y \\ H'" + and b: "graph H' h' \\ 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 \ H'" .. + also have "x + y \\ H'" .. with b have "h' (x + y) = h (x + y)" .. finally show ?thesis . qed next - fix a x assume "x \ H" - have "\ H' h'. x \ H' \ graph H' h' \ graph H h - \ is_linearform H' h' \ is_subspace H' E - \ is_subspace F H' \ graph F f \ graph H' h' - \ (\ x \ H'. h' x \ p x)" + fix a x assume "x \\ H" + have "\\H' h'. x \\ H' \\ graph H' h' \\ graph H h + \\ is_linearform H' h' \\ is_subspace H' E + \\ is_subspace F H' \\ graph F f \\ graph H' h' + \\ (\\x \\ H'. h' x <= p x)" by (rule some_H'h') txt{* We have to show that $h$ is multiplicative. *} - thus "h (a \ x) = a * h x" + thus "h (a \\ x) = a * h x" proof (elim exE conjE) - fix H' h' assume "x \ H'" - and b: "graph H' h' \ graph H h" + fix H' h' assume "x \\ H'" + and b: "graph H' h' \\ graph H h" and "is_linearform H' h'" "is_subspace H' E" - have "h' (a \ x) = a * h' x" + have "h' (a \\ x) = a * h' x" by (rule linearform_mult) also have "h' x = h x" .. - also have "a \ x \ H'" .. - with b have "h' (a \ x) = h (a \ x)" .. + also have "a \\ x \\ H'" .. + with b have "h' (a \\ x) = h (a \\ x)" .. finally show ?thesis . qed qed @@ -306,34 +306,34 @@ for every element of the chain.*} lemma sup_ext: - "[| graph H h = \ c; M = norm_pres_extensions E p F f; - c \ chain M; \x. x \ c |] ==> graph F f \ graph H h" + "[| graph H h = \\ c; M = norm_pres_extensions E p F f; + c \\ chain M; \\x. x \\ c |] ==> graph F f \\ graph H h" proof - - assume "M = norm_pres_extensions E p F f" "c \ chain M" - "graph H h = \ c" - assume "\x. x \ c" + assume "M = norm_pres_extensions E p F f" "c \\ chain M" + "graph H h = \\ c" + assume "\\x. x \\ c" thus ?thesis proof - fix x assume "x \ c" - have "c \ M" by (rule chainD2) - hence "x \ M" .. - hence "x \ norm_pres_extensions E p F f" by (simp!) + fix x assume "x \\ c" + have "c \\ M" by (rule chainD2) + hence "x \\ M" .. + hence "x \\ norm_pres_extensions E p F f" by (simp!) - hence "\G g. graph G g = x - \ is_linearform G g - \ is_subspace G E - \ is_subspace F G - \ graph F f \ graph G g - \ (\x \ G. g x \ p x)" + hence "\\G g. graph G g = x + \\ is_linearform G g + \\ is_subspace G E + \\ is_subspace F G + \\ graph F f \\ graph G g + \\ (\\x \\ 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 \ graph G g" + fix G g assume "graph F f \\ graph G g" also assume "graph G g = x" - also have "... \ c" . - hence "x \ \ c" by fast - also have [RS sym]: "graph H h = \ c" . + also have "... \\ c" . + hence "x \\ \\ c" by fast + also have [RS sym]: "graph H h = \\ c" . finally show ?thesis . qed qed @@ -345,30 +345,30 @@ vector space. *} lemma sup_supF: - "[| graph H h = \ c; M = norm_pres_extensions E p F f; - c \ chain M; \x. x \ c; is_subspace F E; is_vectorspace E |] + "[| graph H h = \\ c; M = norm_pres_extensions E p F f; + c \\ chain M; \\x. x \\ c; is_subspace F E; is_vectorspace E |] ==> is_subspace F H" proof - - assume "M = norm_pres_extensions E p F f" "c \ chain M" "\x. x \ c" - "graph H h = \ c" "is_subspace F E" "is_vectorspace E" + assume "M = norm_pres_extensions E p F f" "c \\ chain M" "\\x. x \\ c" + "graph H h = \\ c" "is_subspace F E" "is_vectorspace E" show ?thesis proof - show "0 \ F" .. - show "F \ H" + show "0 \\ F" .. + show "F \\ H" proof (rule graph_extD2) - show "graph F f \ graph H h" + show "graph F f \\ graph H h" by (rule sup_ext) qed - show "\x \ F. \y \ F. x + y \ F" + show "\\x \\ F. \\y \\ F. x + y \\ F" proof (intro ballI) - fix x y assume "x \ F" "y \ F" - show "x + y \ F" by (simp!) + fix x y assume "x \\ F" "y \\ F" + show "x + y \\ F" by (simp!) qed - show "\x \ F. \a. a \ x \ F" + show "\\x \\ F. \\a. a \\ x \\ F" proof (intro ballI allI) - fix x a assume "x\F" - show "a \ x \ F" by (simp!) + fix x a assume "x\\F" + show "a \\ x \\ F" by (simp!) qed qed qed @@ -377,78 +377,78 @@ of $E$. *} lemma sup_subE: - "[| graph H h = \ c; M = norm_pres_extensions E p F f; - c \ chain M; \x. x \ c; is_subspace F E; is_vectorspace E |] + "[| graph H h = \\ c; M = norm_pres_extensions E p F f; + c \\ chain M; \\x. x \\ c; is_subspace F E; is_vectorspace E |] ==> is_subspace H E" proof - - assume "M = norm_pres_extensions E p F f" "c \ chain M" "\x. x \ c" - "graph H h = \ c" "is_subspace F E" "is_vectorspace E" + assume "M = norm_pres_extensions E p F f" "c \\ chain M" "\\x. x \\ c" + "graph H h = \\ 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 \ F" .. + have "0 \\ F" .. also have "is_subspace F H" by (rule sup_supF) - hence "F \ H" .. - finally show "0 \ H" . + hence "F \\ H" .. + finally show "0 \\ H" . txt{* $H$ is a subset of $E$: *} - show "H \ E" + show "H \\ E" proof - fix x assume "x \ H" - have "\H' h'. x \ H' \ graph H' h' \ graph H h - \ is_linearform H' h' \ is_subspace H' E - \ is_subspace F H' \ graph F f \ graph H' h' - \ (\x \ H'. h' x \ p x)" + fix x assume "x \\ H" + have "\\H' h'. x \\ H' \\ graph H' h' \\ graph H h + \\ is_linearform H' h' \\ is_subspace H' E + \\ is_subspace F H' \\ graph F f \\ graph H' h' + \\ (\\x \\ H'. h' x <= p x)" by (rule some_H'h') - thus "x \ E" + thus "x \\ E" proof (elim exE conjE) - fix H' h' assume "x \ H'" "is_subspace H' E" - have "H' \ E" .. - thus "x \ E" .. + fix H' h' assume "x \\ H'" "is_subspace H' E" + have "H' \\ E" .. + thus "x \\ E" .. qed qed txt{* $H$ is closed under addition: *} - show "\x \ H. \y \ H. x + y \ H" + show "\\x \\ H. \\y \\ H. x + y \\ H" proof (intro ballI) - fix x y assume "x \ H" "y \ H" - have "\H' h'. x \ H' \ y \ H' \ graph H' h' \ graph H h - \ is_linearform H' h' \ is_subspace H' E - \ is_subspace F H' \ graph F f \ graph H' h' - \ (\x \ H'. h' x \ p x)" + fix x y assume "x \\ H" "y \\ H" + have "\\H' h'. x \\ H' \\ y \\ H' \\ graph H' h' \\ graph H h + \\ is_linearform H' h' \\ is_subspace H' E + \\ is_subspace F H' \\ graph F f \\ graph H' h' + \\ (\\x \\ H'. h' x <= p x)" by (rule some_H'h'2) - thus "x + y \ H" + thus "x + y \\ H" proof (elim exE conjE) fix H' h' - assume "x \ H'" "y \ H'" "is_subspace H' E" - "graph H' h' \ graph H h" - have "x + y \ H'" .. - also have "H' \ H" .. + assume "x \\ H'" "y \\ H'" "is_subspace H' E" + "graph H' h' \\ graph H h" + have "x + y \\ H'" .. + also have "H' \\ H" .. finally show ?thesis . qed qed txt{* $H$ is closed under scalar multiplication: *} - show "\x \ H. \a. a \ x \ H" + show "\\x \\ H. \\a. a \\ x \\ H" proof (intro ballI allI) - fix x a assume "x \ H" - have "\H' h'. x \ H' \ graph H' h' \ graph H h - \ is_linearform H' h' \ is_subspace H' E - \ is_subspace F H' \ graph F f \ graph H' h' - \ (\x \ H'. h' x \ p x)" + fix x a assume "x \\ H" + have "\\H' h'. x \\ H' \\ graph H' h' \\ graph H h + \\ is_linearform H' h' \\ is_subspace H' E + \\ is_subspace F H' \\ graph F f \\ graph H' h' + \\ (\\x \\ H'. h' x <= p x)" by (rule some_H'h') - thus "a \ x \ H" + thus "a \\ x \\ H" proof (elim exE conjE) fix H' h' - assume "x \ H'" "is_subspace H' E" "graph H' h' \ graph H h" - have "a \ x \ H'" .. - also have "H' \ H" .. + assume "x \\ H'" "is_subspace H' E" "graph H' h' \\ graph H h" + have "a \\ x \\ H'" .. + also have "H' \\ H" .. finally show ?thesis . qed qed @@ -461,23 +461,23 @@ *} lemma sup_norm_pres: - "[| graph H h = \ c; M = norm_pres_extensions E p F f; c \ chain M |] - ==> \ x \ H. h x \ p x" + "[| graph H h = \\ c; M = norm_pres_extensions E p F f; + c \\ chain M |] ==> \\x \\ H. h x <= p x" proof - assume "M = norm_pres_extensions E p F f" "c \ chain M" - "graph H h = \ c" - fix x assume "x \ H" - have "\H' h'. x \ H' \ graph H' h' \ graph H h - \ is_linearform H' h' \ is_subspace H' E \ is_subspace F H' - \ graph F f \ graph H' h' \ (\ x \ H'. h' x \ p x)" + assume "M = norm_pres_extensions E p F f" "c \\ chain M" + "graph H h = \\ c" + fix x assume "x \\ H" + have "\\H' h'. x \\ H' \\ graph H' h' \\ graph H h + \\ is_linearform H' h' \\ is_subspace H' E \\ is_subspace F H' + \\ graph F f \\ graph H' h' \\ (\\x \\ H'. h' x <= p x)" by (rule some_H'h') - thus "h x \ p x" + thus "h x <= p x" proof (elim exE conjE) fix H' h' - assume "x \ H'" "graph H' h' \ graph H h" - and a: "\x \ H'. h' x \ p x" + assume "x \\ H'" "graph H' h' \\ graph H h" + and a: "\\x \\ H'. h' x <= p x" have [RS sym]: "h' x = h x" .. - also from a have "h' x \ 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 |] - ==> (\x \ H. |h x| \ p x) = (\x \ H. h x \ p x)" + ==> (\\x \\ H. |h x| <= p x) = (\\x \\ 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 \ H" - have "h x \ |h x|" by (rule abs_ge_self) - also from l have "... \ p x" .. - finally show "h x \ p x" . + fix x assume x: "x \\ 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 \ H" - show "!! a b :: real. [| - a \ b; b \ a |] ==> |b| \ a" + fix x assume "x \\ H" + show "!! a b :: real. [| - a <= b; b <= a |] ==> |b| <= a" by arith - show "- p x \ 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 "... \ 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 \ p x" . + proof (rule seminorm_minus) + show "x \\ E" .. + qed + finally show "- h x <= p x" . qed - from r show "h x \ p x" .. + from r show "h x <= p x" .. qed qed qed - end \ No newline at end of file diff -r 12f251a5a3b5 -r 21cfeae6659d src/HOL/Real/HahnBanach/VectorSpace.thy --- 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 "\" 70) + prod :: "[real, 'a] => 'a" (infixr "\\" 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 \ {} - \ (\x \ V. \y \ V. \z \ V. \a b. - x + y \ V - \ a \ x \ V - \ (x + y) + z = x + (y + z) - \ x + y = y + x - \ x - x = 0 - \ 0 + x = x - \ a \ (x + y) = a \ x + a \ y - \ (a + b) \ x = a \ x + b \ x - \ (a * b) \ x = a \ b \ x - \ #1 \ x = x - \ - x = (- #1) \ x - \ x - y = x + - y)" + "is_vectorspace V == V \\ {} + \\ (\\x \\ V. \\y \\ V. \\z \\ V. \\a b. + x + y \\ V + \\ a \\ x \\ V + \\ (x + y) + z = x + (y + z) + \\ x + y = y + x + \\ x - x = 0 + \\ 0 + x = x + \\ a \\ (x + y) = a \\ x + a \\ y + \\ (a + b) \\ x = a \\ x + b \\ x + \\ (a * b) \\ x = a \\ b \\ x + \\ #1 \\ x = x + \\ - x = (- #1) \\ x + \\ x - y = x + - y)" text_raw {* \medskip *} text {* The corresponding introduction rule is:*} lemma vsI [intro]: - "[| 0 \ V; - \x \ V. \y \ V. x + y \ V; - \x \ V. \a. a \ x \ V; - \x \ V. \y \ V. \z \ V. (x + y) + z = x + (y + z); - \x \ V. \y \ V. x + y = y + x; - \x \ V. x - x = 0; - \x \ V. 0 + x = x; - \x \ V. \y \ V. \a. a \ (x + y) = a \ x + a \ y; - \x \ V. \a b. (a + b) \ x = a \ x + b \ x; - \x \ V. \a b. (a * b) \ x = a \ b \ x; - \x \ V. #1 \ x = x; - \x \ V. - x = (- #1) \ x; - \x \ V. \y \ V. x - y = x + - y |] ==> is_vectorspace V" + "[| 0 \\ V; + \\x \\ V. \\y \\ V. x + y \\ V; + \\x \\ V. \\a. a \\ x \\ V; + \\x \\ V. \\y \\ V. \\z \\ V. (x + y) + z = x + (y + z); + \\x \\ V. \\y \\ V. x + y = y + x; + \\x \\ V. x - x = 0; + \\x \\ V. 0 + x = x; + \\x \\ V. \\y \\ V. \\a. a \\ (x + y) = a \\ x + a \\ y; + \\x \\ V. \\a b. (a + b) \\ x = a \\ x + b \\ x; + \\x \\ V. \\a b. (a * b) \\ x = a \\ b \\ x; + \\x \\ V. #1 \\ x = x; + \\x \\ V. - x = (- #1) \\ x; + \\x \\ V. \\y \\ V. x - y = x + - y |] ==> is_vectorspace V" proof (unfold is_vectorspace_def, intro conjI ballI allI) fix x y z - assume "x \ V" "y \ V" "z \ V" - "\x \ V. \y \ V. \z \ V. x + y + z = x + (y + z)" + assume "x \\ V" "y \\ V" "z \\ V" + "\\x \\ V. \\y \\ V. \\z \\ 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 \ V |] ==> - x = (- #1) \ x" + "[| is_vectorspace V; x \\ V |] ==> - x = (- #1) \\ x" by (unfold is_vectorspace_def) simp lemma diff_eq1: - "[| is_vectorspace V; x \ V; y \ V |] ==> x - y = x + - y" + "[| is_vectorspace V; x \\ V; y \\ V |] ==> x - y = x + - y" by (unfold is_vectorspace_def) simp lemma negate_eq2: - "[| is_vectorspace V; x \ V |] ==> (- #1) \ x = - x" + "[| is_vectorspace V; x \\ V |] ==> (- #1) \\ x = - x" by (unfold is_vectorspace_def) simp lemma negate_eq2a: - "[| is_vectorspace V; x \ V |] ==> #-1 \ x = - x" + "[| is_vectorspace V; x \\ V |] ==> #-1 \\ x = - x" by (unfold is_vectorspace_def) simp lemma diff_eq2: - "[| is_vectorspace V; x \ V; y \ V |] ==> x + - y = x - y" + "[| is_vectorspace V; x \\ V; y \\ V |] ==> x + - y = x - y" by (unfold is_vectorspace_def) simp -lemma vs_not_empty [intro??]: "is_vectorspace V ==> (V \ {})" +lemma vs_not_empty [intro??]: "is_vectorspace V ==> (V \\ {})" by (unfold is_vectorspace_def) simp lemma vs_add_closed [simp, intro??]: - "[| is_vectorspace V; x \ V; y \ V |] ==> x + y \ V" + "[| is_vectorspace V; x \\ V; y \\ V |] ==> x + y \\ V" by (unfold is_vectorspace_def) simp lemma vs_mult_closed [simp, intro??]: - "[| is_vectorspace V; x \ V |] ==> a \ x \ V" + "[| is_vectorspace V; x \\ V |] ==> a \\ x \\ V" by (unfold is_vectorspace_def) simp lemma vs_diff_closed [simp, intro??]: - "[| is_vectorspace V; x \ V; y \ V |] ==> x - y \ V" + "[| is_vectorspace V; x \\ V; y \\ V |] ==> x - y \\ V" by (simp add: diff_eq1 negate_eq1) lemma vs_neg_closed [simp, intro??]: - "[| is_vectorspace V; x \ V |] ==> - x \ V" + "[| is_vectorspace V; x \\ V |] ==> - x \\ V" by (simp add: negate_eq1) lemma vs_add_assoc [simp]: - "[| is_vectorspace V; x \ V; y \ V; z \ V |] + "[| is_vectorspace V; x \\ V; y \\ V; z \\ V |] ==> (x + y) + z = x + (y + z)" by (unfold is_vectorspace_def) fast lemma vs_add_commute [simp]: - "[| is_vectorspace V; x \ V; y \ V |] ==> y + x = x + y" + "[| is_vectorspace V; x \\ V; y \\ V |] ==> y + x = x + y" by (unfold is_vectorspace_def) simp lemma vs_add_left_commute [simp]: - "[| is_vectorspace V; x \ V; y \ V; z \ V |] + "[| is_vectorspace V; x \\ V; y \\ V; z \\ V |] ==> x + (y + z) = y + (x + z)" proof - - assume "is_vectorspace V" "x \ V" "y \ V" "z \ V" + assume "is_vectorspace V" "x \\ V" "y \\ V" "z \\ 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 \ V |] ==> x - x = 0" + "[| is_vectorspace V; x \\ 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 \ V" +lemma zero_in_vs [simp, intro]: "is_vectorspace V ==> 0 \\ V" proof - assume "is_vectorspace V" - have "V \ {}" .. - hence "\x. x \ V" by force + have "V \\ {}" .. + hence "\\x. x \\ V" by force thus ?thesis proof - fix x assume "x \ V" + fix x assume "x \\ V" have "0 = x - x" by (simp!) - also have "... \ V" by (simp! only: vs_diff_closed) + also have "... \\ V" by (simp! only: vs_diff_closed) finally show ?thesis . qed qed lemma vs_add_zero_left [simp]: - "[| is_vectorspace V; x \ V |] ==> 0 + x = x" + "[| is_vectorspace V; x \\ V |] ==> 0 + x = x" by (unfold is_vectorspace_def) simp lemma vs_add_zero_right [simp]: - "[| is_vectorspace V; x \ V |] ==> x + 0 = x" + "[| is_vectorspace V; x \\ V |] ==> x + 0 = x" proof - - assume "is_vectorspace V" "x \ V" + assume "is_vectorspace V" "x \\ V" hence "x + 0 = 0 + x" by simp also have "... = x" by (simp!) finally show ?thesis . qed lemma vs_add_mult_distrib1: - "[| is_vectorspace V; x \ V; y \ V |] - ==> a \ (x + y) = a \ x + a \ y" + "[| is_vectorspace V; x \\ V; y \\ V |] + ==> a \\ (x + y) = a \\ x + a \\ y" by (unfold is_vectorspace_def) simp lemma vs_add_mult_distrib2: - "[| is_vectorspace V; x \ V |] - ==> (a + b) \ x = a \ x + b \ x" + "[| is_vectorspace V; x \\ V |] + ==> (a + b) \\ x = a \\ x + b \\ x" by (unfold is_vectorspace_def) simp lemma vs_mult_assoc: - "[| is_vectorspace V; x \ V |] ==> (a * b) \ x = a \ (b \ x)" + "[| is_vectorspace V; x \\ V |] ==> (a * b) \\ x = a \\ (b \\ x)" by (unfold is_vectorspace_def) simp lemma vs_mult_assoc2 [simp]: - "[| is_vectorspace V; x \ V |] ==> a \ b \ x = (a * b) \ x" + "[| is_vectorspace V; x \\ V |] ==> a \\ b \\ x = (a * b) \\ x" by (simp only: vs_mult_assoc) lemma vs_mult_1 [simp]: - "[| is_vectorspace V; x \ V |] ==> #1 \ x = x" + "[| is_vectorspace V; x \\ V |] ==> #1 \\ x = x" by (unfold is_vectorspace_def) simp lemma vs_diff_mult_distrib1: - "[| is_vectorspace V; x \ V; y \ V |] - ==> a \ (x - y) = a \ x - a \ y" + "[| is_vectorspace V; x \\ V; y \\ V |] + ==> a \\ (x - y) = a \\ x - a \\ y" by (simp add: diff_eq1 negate_eq1 vs_add_mult_distrib1) lemma vs_diff_mult_distrib2: - "[| is_vectorspace V; x \ V |] - ==> (a - b) \ x = a \ x - (b \ x)" + "[| is_vectorspace V; x \\ V |] + ==> (a - b) \\ x = a \\ x - (b \\ x)" proof - - assume "is_vectorspace V" "x \ V" - have " (a - b) \ x = (a + - b) \ x" + assume "is_vectorspace V" "x \\ V" + have " (a - b) \\ x = (a + - b) \\ x" by (unfold real_diff_def, simp) - also have "... = a \ x + (- b) \ x" + also have "... = a \\ x + (- b) \\ x" by (rule vs_add_mult_distrib2) - also have "... = a \ x + - (b \ x)" + also have "... = a \\ x + - (b \\ x)" by (simp! add: negate_eq1) - also have "... = a \ x - (b \ x)" + also have "... = a \\ x - (b \\ 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 \ V |] ==> #0 \ x = 0" + "[| is_vectorspace V; x \\ V |] ==> #0 \\ x = 0" proof - - assume "is_vectorspace V" "x \ V" - have "#0 \ x = (#1 - #1) \ x" by simp - also have "... = (#1 + - #1) \ x" by simp - also have "... = #1 \ x + (- #1) \ x" + assume "is_vectorspace V" "x \\ V" + have "#0 \\ x = (#1 - #1) \\ x" by simp + also have "... = (#1 + - #1) \\ x" by simp + also have "... = #1 \\ x + (- #1) \\ x" by (rule vs_add_mult_distrib2) - also have "... = x + (- #1) \ x" by (simp!) + also have "... = x + (- #1) \\ 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 \ 0 = (0::'a)" + ==> a \\ 0 = (0::'a)" proof - assume "is_vectorspace V" - have "a \ 0 = a \ (0 - (0::'a))" by (simp!) - also have "... = a \ 0 - a \ 0" + have "a \\ 0 = a \\ (0 - (0::'a))" by (simp!) + also have "... = a \\ 0 - a \\ 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 \ V |] ==> (- a) \ - x = a \ x" + "[| is_vectorspace V; x \\ V |] ==> (- a) \\ - x = a \\ x" by (simp add: negate_eq1) lemma vs_add_minus_left_eq_diff: - "[| is_vectorspace V; x \ V; y \ V |] ==> - x + y = y - x" + "[| is_vectorspace V; x \\ V; y \\ V |] ==> - x + y = y - x" proof - - assume "is_vectorspace V" "x \ V" "y \ V" - have "- x + y = y + - x" - by (simp! add: vs_add_commute [RS sym, of V "- x"]) + assume "is_vectorspace V" "x \\ V" "y \\ 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 \ V |] ==> x + - x = 0" + "[| is_vectorspace V; x \\ V |] ==> x + - x = 0" by (simp! add: diff_eq2) lemma vs_add_minus_left [simp]: - "[| is_vectorspace V; x \ V |] ==> - x + x = 0" + "[| is_vectorspace V; x \\ V |] ==> - x + x = 0" by (simp! add: diff_eq2) lemma vs_minus_minus [simp]: - "[| is_vectorspace V; x \ V |] ==> - (- x) = x" + "[| is_vectorspace V; x \\ 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 \ V |] ==> (- x = 0) = (x = 0)" + "[| is_vectorspace V; x \\ V |] ==> (- x = 0) = (x = 0)" (concl is "?L = ?R") proof - - assume "is_vectorspace V" "x \ V" + assume "is_vectorspace V" "x \\ 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 \ V; y \ V |] ==> x + (- x + y) = y" + "[| is_vectorspace V; x \\ V; y \\ V |] ==> x + (- x + y) = y" by (simp add: vs_add_assoc [RS sym] del: vs_add_commute) lemma vs_minus_add_cancel [simp]: - "[| is_vectorspace V; x \ V; y \ V |] ==> - x + (x + y) = y" + "[| is_vectorspace V; x \\ V; y \\ V |] ==> - x + (x + y) = y" by (simp add: vs_add_assoc [RS sym] del: vs_add_commute) lemma vs_minus_add_distrib [simp]: - "[| is_vectorspace V; x \ V; y \ V |] + "[| is_vectorspace V; x \\ V; y \\ V |] ==> - (x + y) = - x + - y" by (simp add: negate_eq1 vs_add_mult_distrib1) lemma vs_diff_zero [simp]: - "[| is_vectorspace V; x \ V |] ==> x - 0 = x" + "[| is_vectorspace V; x \\ V |] ==> x - 0 = x" by (simp add: diff_eq1) lemma vs_diff_zero_right [simp]: - "[| is_vectorspace V; x \ V |] ==> 0 - x = - x" + "[| is_vectorspace V; x \\ V |] ==> 0 - x = - x" by (simp add:diff_eq1) lemma vs_add_left_cancel: - "[| is_vectorspace V; x \ V; y \ V; z \ V |] + "[| is_vectorspace V; x \\ V; y \\ V; z \\ V |] ==> (x + y = x + z) = (y = z)" (concl is "?L = ?R") proof - assume "is_vectorspace V" "x \ V" "y \ V" "z \ V" + assume "is_vectorspace V" "x \\ V" "y \\ V" "z \\ 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 \ V; y \ V; z \ V |] + "[| is_vectorspace V; x \\ V; y \\ V; z \\ V |] ==> (y + x = z + x) = (y = z)" by (simp only: vs_add_commute vs_add_left_cancel) lemma vs_add_assoc_cong: - "[| is_vectorspace V; x \ V; y \ V; x' \ V; y' \ V; z \ V |] + "[| is_vectorspace V; x \\ V; y \\ V; x' \\ V; y' \\ V; z \\ V |] ==> x + y = x' + y' ==> x + (y + z) = x' + (y' + z)" by (simp only: vs_add_assoc [RS sym]) lemma vs_mult_left_commute: - "[| is_vectorspace V; x \ V; y \ V; z \ V |] - ==> x \ y \ z = y \ x \ z" + "[| is_vectorspace V; x \\ V; y \\ V; z \\ V |] + ==> x \\ y \\ z = y \\ x \\ z" by (simp add: real_mult_commute) lemma vs_mult_zero_uniq: - "[| is_vectorspace V; x \ V; a \ x = 0; x \ 0 |] ==> a = #0" + "[| is_vectorspace V; x \\ V; a \\ x = 0; x \\ 0 |] ==> a = #0" proof (rule classical) - assume "is_vectorspace V" "x \ V" "a \ x = 0" "x \ 0" - assume "a \ #0" - have "x = (rinv a * a) \ x" by (simp!) - also have "... = rinv a \ (a \ x)" by (rule vs_mult_assoc) - also have "... = rinv a \ 0" by (simp!) + assume "is_vectorspace V" "x \\ V" "a \\ x = 0" "x \\ 0" + assume "a \\ #0" + have "x = (rinv a * a) \\ x" by (simp!) + also have "... = rinv a \\ (a \\ x)" by (rule vs_mult_assoc) + also have "... = rinv a \\ 0" by (simp!) also have "... = 0" by (simp!) finally have "x = 0" . thus "a = #0" by contradiction qed lemma vs_mult_left_cancel: - "[| is_vectorspace V; x \ V; y \ V; a \ #0 |] ==> - (a \ x = a \ y) = (x = y)" + "[| is_vectorspace V; x \\ V; y \\ V; a \\ #0 |] ==> + (a \\ x = a \\ y) = (x = y)" (concl is "?L = ?R") proof - assume "is_vectorspace V" "x \ V" "y \ V" "a \ #0" - have "x = #1 \ x" by (simp!) - also have "... = (rinv a * a) \ x" by (simp!) - also have "... = rinv a \ (a \ x)" + assume "is_vectorspace V" "x \\ V" "y \\ V" "a \\ #0" + have "x = #1 \\ x" by (simp!) + also have "... = (rinv a * a) \\ x" by (simp!) + also have "... = rinv a \\ (a \\ x)" by (simp! only: vs_mult_assoc) also assume ?L - also have "rinv a \ ... = y" by (simp!) + also have "rinv a \\ ... = y" by (simp!) finally show ?R . qed simp lemma vs_mult_right_cancel: (*** forward ***) - "[| is_vectorspace V; x \ V; x \ 0 |] - ==> (a \ x = b \ x) = (a = b)" (concl is "?L = ?R") + "[| is_vectorspace V; x \\ V; x \\ 0 |] + ==> (a \\ x = b \\ x) = (a = b)" (concl is "?L = ?R") proof - assume "is_vectorspace V" "x \ V" "x \ 0" - have "(a - b) \ x = a \ x - b \ x" + assume "is_vectorspace V" "x \\ V" "x \\ 0" + have "(a - b) \\ x = a \\ x - b \\ x" by (simp! add: vs_diff_mult_distrib2) - also assume ?L hence "a \ x - b \ x = 0" by (simp!) - finally have "(a - b) \ x = 0" . + also assume ?L hence "a \\ x - b \\ x = 0" by (simp!) + finally have "(a - b) \\ 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 \ 0 |] ==> + "[| is_vectorspace V; x:V; x \\ 0 |] ==> (a ( * ) x = b ( * ) x) = (a = b)" (concl is "?L = ?R"); proof; - assume "is_vectorspace V" "x:V" "x \ 0"; + assume "is_vectorspace V" "x:V" "x \\ 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 \ V; y \ V; z \ V |] ==> + "[| is_vectorspace V; x \\ V; y \\ V; z \\ V |] ==> (x = z - y) = (x + y = z)" (concl is "?L = ?R" ) proof - - assume vs: "is_vectorspace V" "x \ V" "y \ V" "z \ V" + assume vs: "is_vectorspace V" "x \\ V" "y \\ V" "z \\ V" show "?L = ?R" proof assume ?L @@ -438,9 +437,9 @@ qed lemma vs_add_minus_eq_minus: - "[| is_vectorspace V; x \ V; y \ V; x + y = 0 |] ==> x = - y" + "[| is_vectorspace V; x \\ V; y \\ V; x + y = 0 |] ==> x = - y" proof - - assume "is_vectorspace V" "x \ V" "y \ V" + assume "is_vectorspace V" "x \\ V" "y \\ 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 \ V; y \ V; x - y = 0 |] ==> x = y" + "[| is_vectorspace V; x \\ V; y \\ V; x - y = 0 |] ==> x = y" proof - - assume "is_vectorspace V" "x \ V" "y \ V" "x - y = 0" + assume "is_vectorspace V" "x \\ V" "y \\ 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 \ V; b \ V; c \ V; d \ V; a + b = c + d |] + "[| is_vectorspace V; a \\ V; b \\ V; c \\ V; d \\ V; a + b = c + d |] ==> a - c = d - b" proof - - assume vs: "is_vectorspace V" "a \ V" "b \ V" "c \ V" "d \ V" + assume vs: "is_vectorspace V" "a \\ V" "b \\ V" "c \\ V" "d \\ 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 \ V; y \ V; z \ V; u \ V |] + "[| is_vectorspace V; x \\ V; y \\ V; z \\ V; u \\ V |] ==> (x + (y + z) = y + u) = ((x + z) = u)" (concl is "?L = ?R") proof - - assume "is_vectorspace V" "x \ V" "y \ V" "z \ V" "u \ V" + assume "is_vectorspace V" "x \\ V" "y \\ V" "z \\ V" "u \\ 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 \ V; y \ V; z \ V |] + "[| is_vectorspace V; x \\ V; y \\ V; z \\ V |] ==> (x + (y + z) = y) = (x = - z)" (concl is "?L = ?R" ) proof - - assume "is_vectorspace V" "x \ V" "y \ V" "z \ V" + assume "is_vectorspace V" "x \\ V" "y \\ V" "z \\ V" show "?L = ?R" proof assume l: ?L diff -r 12f251a5a3b5 -r 21cfeae6659d src/HOL/Real/HahnBanach/document/notation.tex --- 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