# HG changeset patch # User wenzelm # Date 960140369 -7200 # Node ID 371f023d3dbdc644093361e08eef06ec7226e01d # Parent ea4dc7603f0bfba5682f80671f80c8e09402d038 removed explicit terminator (";"); diff -r ea4dc7603f0b -r 371f023d3dbd src/HOL/Calculation.thy --- a/src/HOL/Calculation.thy Sun Jun 04 00:09:04 2000 +0200 +++ b/src/HOL/Calculation.thy Sun Jun 04 19:39:29 2000 +0200 @@ -6,54 +6,53 @@ list below later rules have priority. *) -theory Calculation = IntArith:; +theory Calculation = IntArith: -theorems [trans] = rev_mp mp; +theorems [trans] = rev_mp mp -theorem [trans]: "[| s = t; P t |] ==> P s"; (* = x x *) - by (rule ssubst); +theorem [trans]: "[| s = t; P t |] ==> P s" (* = x x *) + by (rule ssubst) -theorem [trans]: "[| P s; s = t |] ==> P t"; (* x = x *) - by (rule subst); +theorem [trans]: "[| P s; s = t |] ==> P t" (* x = x *) + by (rule subst) -theorems [trans] = dvd_trans; (* dvd dvd dvd *) +theorems [trans] = dvd_trans (* dvd dvd dvd *) -theorem [trans]: "[| c:A; A <= B |] ==> c:B"; - by (rule subsetD); +theorem [trans]: "[| c:A; A <= B |] ==> c:B" + by (rule subsetD) -theorem [trans]: "[| A <= B; c:A |] ==> c:B"; - by (rule subsetD); +theorem [trans]: "[| A <= B; c:A |] ==> c:B" + by (rule subsetD) -theorem [trans]: "[| x ~= y; (x::'a::order) <= y |] ==> x < y"; (* ~= <= < *) - by (simp! add: order_less_le); +theorem [trans]: "[| x ~= y; (x::'a::order) <= y |] ==> x < y" (* ~= <= < *) + by (simp! add: order_less_le) -theorem [trans]: "[| (x::'a::order) <= y; x ~= y |] ==> x < y"; (* <= ~= < *) - by (simp! add: order_less_le); +theorem [trans]: "[| (x::'a::order) <= y; x ~= y |] ==> x < y" (* <= ~= < *) + by (simp! add: order_less_le) -theorem [trans]: "[| (x::'a::order) < y; y < x |] ==> P"; (* < > P *) - by (rule order_less_asym); +theorem [trans]: "[| (x::'a::order) < y; y < x |] ==> P" (* < > P *) + by (rule order_less_asym) -theorems [trans] = order_less_trans; (* < < < *) -theorems [trans] = order_le_less_trans; (* <= < < *) -theorems [trans] = order_less_le_trans; (* < <= < *) -theorems [trans] = order_trans; (* <= <= <= *) -theorems [trans] = order_antisym; (* <= >= = *) +theorems [trans] = order_less_trans (* < < < *) +theorems [trans] = order_le_less_trans (* <= < < *) +theorems [trans] = order_less_le_trans (* < <= < *) +theorems [trans] = order_trans (* <= <= <= *) +theorems [trans] = order_antisym (* <= >= = *) -theorem [trans]: "[| x <= y; y = z |] ==> x <= z"; (* <= = <= *) - by (rule subst); +theorem [trans]: "[| x <= y; y = z |] ==> x <= z" (* <= = <= *) + by (rule subst) -theorem [trans]: "[| x = y; y <= z |] ==> x <= z"; (* = <= <= *) - by (rule ssubst); +theorem [trans]: "[| x = y; y <= z |] ==> x <= z" (* = <= <= *) + by (rule ssubst) -theorem [trans]: "[| x < y; y = z |] ==> x < z"; (* < = < *) - by (rule subst); +theorem [trans]: "[| x < y; y = z |] ==> x < z" (* < = < *) + by (rule subst) -theorem [trans]: "[| x = y; y < z |] ==> x < z"; (* = < < *) - by (rule ssubst); +theorem [trans]: "[| x = y; y < z |] ==> x < z" (* = < < *) + by (rule ssubst) theorems [trans] = trans (* = = = *) theorems [elim??] = sym - -end; +end diff -r ea4dc7603f0b -r 371f023d3dbd src/HOL/Numeral.thy --- a/src/HOL/Numeral.thy Sun Jun 04 00:09:04 2000 +0200 +++ b/src/HOL/Numeral.thy Sun Jun 04 19:39:29 2000 +0200 @@ -6,23 +6,23 @@ *) theory Numeral = Datatype -files "Tools/numeral_syntax.ML":; +files "Tools/numeral_syntax.ML": datatype bin = Pls | Min - | Bit bin bool (infixl "BIT" 90); + | Bit bin bool (infixl "BIT" 90) axclass - number < "term"; (*for numeric types: nat, int, real, ...*) + number < "term" (*for numeric types: nat, int, real, ...*) consts - number_of :: "bin => 'a::number"; + number_of :: "bin => 'a::number" syntax - "_Numeral" :: "xnum => 'a" ("_"); + "_Numeral" :: "xnum => 'a" ("_") -setup NumeralSyntax.setup; +setup NumeralSyntax.setup -end; +end diff -r ea4dc7603f0b -r 371f023d3dbd src/HOL/Real/HahnBanach/Aux.thy --- a/src/HOL/Real/HahnBanach/Aux.thy Sun Jun 04 00:09:04 2000 +0200 +++ b/src/HOL/Real/HahnBanach/Aux.thy Sun Jun 04 19:39:29 2000 +0200 @@ -3,161 +3,161 @@ Author: Gertrud Bauer, TU Munich *) -header {* Auxiliary theorems *}; +header {* Auxiliary theorems *} -theory Aux = Real + Zorn:; +theory Aux = Real + Zorn: text {* Some existing theorems are declared as extra introduction -or elimination rules, respectively. *}; +or elimination rules, respectively. *} -lemmas [intro??] = isLub_isUb; -lemmas [intro??] = chainD; -lemmas chainE2 = chainD2 [elimify]; +lemmas [intro??] = isLub_isUb +lemmas [intro??] = chainD +lemmas chainE2 = chainD2 [elimify] -text_raw {* \medskip *}; -text{* Lemmas about sets. *}; +text_raw {* \medskip *} +text{* Lemmas about sets. *} -lemma Int_singletonD: "[| A Int B = {v}; x:A; x:B |] ==> x = v"; - by (fast elim: equalityE); +lemma Int_singletonD: "[| A Int B = {v}; x:A; x:B |] ==> x = v" + by (fast elim: equalityE) -lemma set_less_imp_diff_not_empty: "H < E ==> EX x0:E. x0 ~: H"; - by (force simp add: psubset_eq); +lemma set_less_imp_diff_not_empty: "H < E ==> EX x0:E. x0 ~: H" + by (force simp add: psubset_eq) -text_raw {* \medskip *}; -text{* Some lemmas about orders. *}; +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 (rule order_less_le[RS iffD1, RS conjunct2]) lemma le_noteq_imp_less: - "[| x <= (r::'a::order); x ~= r |] ==> x < r"; -proof -; - assume "x <= (r::'a::order)" and ne:"x ~= r"; - hence "x < r | x = r"; by (simp add: order_le_less); - with ne; show ?thesis; by simp; -qed; + "[| x <= (r::'a::order); x ~= r |] ==> x < r" +proof - + assume "x <= (r::'a::order)" and ne:"x ~= r" + hence "x < r | x = r" by (simp add: order_le_less) + with ne show ?thesis by simp +qed -text_raw {* \medskip *}; -text {* Some lemmas about linear orders. *}; +text_raw {* \medskip *} +text {* Some lemmas about linear orders. *} theorem linorder_linear_split: -"[| x < a ==> Q; x = a ==> Q; a < (x::'a::linorder) ==> Q |] ==> Q"; - by (rule linorder_less_linear [of x a, elimify]) force+; +"[| x < a ==> Q; x = a ==> Q; a < (x::'a::linorder) ==> Q |] ==> Q" + by (rule linorder_less_linear [of x a, elimify]) force+ -lemma le_max1: "x <= max x (y::'a::linorder)"; - by (simp add: le_max_iff_disj[of x x y]); +lemma le_max1: "x <= max x (y::'a::linorder)" + by (simp add: le_max_iff_disj[of x x y]) -lemma le_max2: "y <= max x (y::'a::linorder)"; - by (simp add: le_max_iff_disj[of y x y]); +lemma le_max2: "y <= max x (y::'a::linorder)" + by (simp add: le_max_iff_disj[of y x y]) -text_raw {* \medskip *}; -text{* Some lemmas for the reals. *}; +text_raw {* \medskip *} +text{* Some lemmas for the reals. *} -lemma real_add_minus_eq: "x - y = (#0::real) ==> x = y"; - by simp; +lemma real_add_minus_eq: "x - y = (#0::real) ==> x = y" + by simp -lemma abs_minus_one: "abs (- (#1::real)) = #1"; - by simp; +lemma abs_minus_one: "abs (- (#1::real)) = #1" + by simp lemma real_mult_le_le_mono1a: - "[| (#0::real) <= z; x <= y |] ==> z * x <= z * y"; -proof -; - assume "(#0::real) <= z" "x <= y"; - hence "x < y | x = y"; by (force simp add: order_le_less); - thus ?thesis; - proof (elim disjE); - assume "x < y"; show ?thesis; by (rule real_mult_le_less_mono2) simp; - next; - assume "x = y"; thus ?thesis;; by simp; - qed; -qed; + "[| (#0::real) <= z; x <= y |] ==> z * x <= z * y" +proof - + assume "(#0::real) <= z" "x <= y" + hence "x < y | x = y" by (force simp add: order_le_less) + thus ?thesis + proof (elim disjE) + assume "x < y" show ?thesis by (rule real_mult_le_less_mono2) simp + next + assume "x = y" thus ?thesis by simp + qed +qed lemma real_mult_le_le_mono2: - "[| (#0::real) <= z; x <= y |] ==> x * z <= y * z"; -proof -; - assume "(#0::real) <= z" "x <= y"; - hence "x < y | x = y"; by (force simp add: order_le_less); - thus ?thesis; - proof (elim disjE); - assume "x < y"; show ?thesis; by (rule real_mult_le_less_mono1) simp; - next; - assume "x = y"; thus ?thesis;; by simp; - qed; -qed; + "[| (#0::real) <= z; x <= y |] ==> x * z <= y * z" +proof - + assume "(#0::real) <= z" "x <= y" + hence "x < y | x = y" by (force simp add: order_le_less) + thus ?thesis + proof (elim disjE) + assume "x < y" show ?thesis by (rule real_mult_le_less_mono1) simp + next + assume "x = y" thus ?thesis by simp + qed +qed lemma real_mult_less_le_anti: - "[| z < (#0::real); x <= y |] ==> z * y <= z * x"; -proof -; - assume "z < (#0::real)" "x <= y"; - hence "(#0::real) < - z"; by simp; - hence "(#0::real) <= - z"; by (rule real_less_imp_le); - hence "x * (- z) <= y * (- z)"; - by (rule real_mult_le_le_mono2); - hence "- (x * z) <= - (y * z)"; - by (simp only: real_minus_mult_eq2); - thus ?thesis; by (simp only: real_mult_commute); -qed; + "[| z < (#0::real); x <= y |] ==> z * y <= z * x" +proof - + assume "z < #0" "x <= y" + hence "#0 < - z" by simp + hence "#0 <= - z" by (rule real_less_imp_le) + hence "x * (- z) <= y * (- z)" + by (rule real_mult_le_le_mono2) + hence "- (x * z) <= - (y * z)" + by (simp only: real_minus_mult_eq2) + thus ?thesis by (simp only: real_mult_commute) +qed lemma real_mult_less_le_mono: - "[| (#0::real) < z; x <= y |] ==> z * x <= z * y"; -proof -; - assume "(#0::real) < z" "x <= y"; - have "(#0::real) <= z"; by (rule real_less_imp_le); - hence "x * z <= y * z"; - by (rule real_mult_le_le_mono2); - thus ?thesis; by (simp only: real_mult_commute); -qed; + "[| (#0::real) < z; x <= y |] ==> z * x <= z * y" +proof - + assume "#0 < z" "x <= y" + have "#0 <= z" by (rule real_less_imp_le) + hence "x * z <= y * z" + by (rule real_mult_le_le_mono2) + thus ?thesis by (simp only: real_mult_commute) +qed -lemma real_rinv_gt_zero1: "#0 < x ==> #0 < rinv x"; -proof -; - assume "#0 < x"; - have "0r < x"; by simp; - hence "0r < rinv x"; by (rule real_rinv_gt_zero); - thus ?thesis; by simp; -qed; +lemma real_rinv_gt_zero1: "#0 < x ==> #0 < rinv x" +proof - + assume "#0 < x" + hence "0r < x" by simp + hence "0r < rinv x" by (rule real_rinv_gt_zero) + thus ?thesis by simp +qed -lemma real_mult_inv_right1: "x ~= #0 ==> x*rinv(x) = #1"; - by simp; +lemma real_mult_inv_right1: "x ~= #0 ==> x*rinv(x) = #1" + by simp -lemma real_mult_inv_left1: "x ~= #0 ==> rinv(x)*x = #1"; - by simp; +lemma real_mult_inv_left1: "x ~= #0 ==> rinv(x)*x = #1" + by simp lemma real_le_mult_order1a: - "[| (#0::real) <= x; #0 <= y |] ==> #0 <= x * y"; -proof -; - assume "#0 <= x" "#0 <= y"; - have "[|0r <= x; 0r <= y|] ==> 0r <= x * y"; - by (rule real_le_mult_order); - thus ?thesis; by (simp!); -qed; + "[| (#0::real) <= x; #0 <= y |] ==> #0 <= x * y" +proof - + assume "#0 <= x" "#0 <= y" + have "[|0r <= x; 0r <= y|] ==> 0r <= x * y" + by (rule real_le_mult_order) + thus ?thesis by (simp!) +qed lemma real_mult_diff_distrib: - "a * (- x - (y::real)) = - a * x - a * y"; -proof -; - have "- x - y = - x + - y"; by simp; - also; have "a * ... = a * - x + a * - y"; - by (simp only: real_add_mult_distrib2); - also; have "... = - a * x - a * y"; - by (simp add: real_minus_mult_eq2 [RS sym] real_minus_mult_eq1); - finally; show ?thesis; .; -qed; + "a * (- x - (y::real)) = - a * x - a * y" +proof - + have "- x - y = - x + - y" by simp + also have "a * ... = a * - x + a * - y" + by (simp only: real_add_mult_distrib2) + also have "... = - a * x - a * y" + by (simp add: real_minus_mult_eq2 [RS sym] real_minus_mult_eq1) + finally show ?thesis . +qed -lemma real_mult_diff_distrib2: "a * (x - (y::real)) = a * x - a * y"; -proof -; - have "x - y = x + - y"; by simp; - also; have "a * ... = a * x + a * - y"; - by (simp only: real_add_mult_distrib2); - also; have "... = a * x - a * y"; - by (simp add: real_minus_mult_eq2 [RS sym] real_minus_mult_eq1); - finally; show ?thesis; .; -qed; +lemma real_mult_diff_distrib2: "a * (x - (y::real)) = a * x - a * y" +proof - + have "x - y = x + - y" by simp + also have "a * ... = a * x + a * - y" + by (simp only: real_add_mult_distrib2) + also have "... = a * x - a * y" + by (simp add: real_minus_mult_eq2 [RS sym] real_minus_mult_eq1) + finally show ?thesis . +qed -lemma real_minus_le: "- (x::real) <= y ==> - y <= x"; - by simp; +lemma real_minus_le: "- (x::real) <= y ==> - y <= x" + by simp lemma real_diff_ineq_swap: - "(d::real) - b <= c + a ==> - a - b <= c - d"; - by simp; + "(d::real) - b <= c + a ==> - a - b <= c - d" + by simp -end; \ No newline at end of file +end \ No newline at end of file diff -r ea4dc7603f0b -r 371f023d3dbd src/HOL/Real/HahnBanach/Bounds.thy --- a/src/HOL/Real/HahnBanach/Bounds.thy Sun Jun 04 00:09:04 2000 +0200 +++ b/src/HOL/Real/HahnBanach/Bounds.thy Sun Jun 04 19:39:29 2000 +0200 @@ -3,11 +3,11 @@ Author: Gertrud Bauer, TU Munich *) -header {* Bounds *}; +header {* Bounds *} -theory Bounds = Main + Real:; +theory Bounds = Main + Real: (*<*) -subsection {* The sets of lower and upper bounds *}; +subsection {* The sets of lower and upper bounds *} constdefs is_LowerBound :: "('a::order) set => 'a set => 'a => bool" @@ -20,7 +20,7 @@ "is_UpperBound A B == \x. x:A & (ALL y:B. y <= x)" UpperBounds :: "('a::order) set => 'a set => 'a set" - "UpperBounds A B == Collect (is_UpperBound A B)"; + "UpperBounds A B == Collect (is_UpperBound A B)" syntax "_UPPERS" :: "[pttrn, 'a set, 'a => bool] => 'a set" @@ -30,16 +30,16 @@ "_LOWERS" :: "[pttrn, 'a set, 'a => bool] => 'a set" ("(3LOWER'_BOUNDS _:_./ _)" 10) "_LOWERS_U" :: "[pttrn, 'a => bool] => 'a set" - ("(3LOWER'_BOUNDS _./ _)" 10); + ("(3LOWER'_BOUNDS _./ _)" 10) translations "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. P" == "LOWER_BOUNDS x:UNIV. P"; + "LOWER_BOUNDS x. P" == "LOWER_BOUNDS x:UNIV. P" -subsection {* Least and greatest elements *}; +subsection {* Least and greatest elements *} constdefs is_Least :: "('a::order) set => 'a => bool" @@ -52,44 +52,44 @@ "is_Greatest B == is_UpperBound B B" Greatest :: "('a::order) set => 'a" - "Greatest B == Eps (is_Greatest B)"; + "Greatest B == Eps (is_Greatest B)" syntax "_LEAST" :: "[pttrn, 'a => bool] => 'a" ("(3LLEAST _./ _)" 10) "_GREATEST" :: "[pttrn, 'a => bool] => 'a" - ("(3GREATEST _./ _)" 10); + ("(3GREATEST _./ _)" 10) translations "LLEAST x. P" == "Least {x. P}" - "GREATEST x. P" == "Greatest {x. P}"; + "GREATEST x. P" == "Greatest {x. P}" -subsection {* Infimum and Supremum *}; +subsection {* Infimum and Supremum *} (*>*) text {* A supremum\footnote{The definition of the supremum is based on one in \url{http://isabelle.in.tum.de/library/HOL/HOL-Real/Lubs.html}} of an ordered set $B$ w.~r.~t.~$A$ is defined as a least upper bound of $B$, which lies in $A$. -*}; +*} text{* If a supremum exists, then $\idt{Sup}\ap A\ap B$ -is equal to the supremum. *}; +is equal to the supremum. *} constdefs is_Sup :: "('a::order) set => 'a set => 'a => bool" "is_Sup A B x == isLub A B x" Sup :: "('a::order) set => 'a set => 'a" - "Sup A B == Eps (is_Sup A B)"; + "Sup A B == Eps (is_Sup A B)" (*<*) constdefs is_Inf :: "('a::order) set => 'a set => 'a => bool" "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)"; + "Inf A B == Eps (is_Inf A B)" syntax "_SUP" :: "[pttrn, 'a set, 'a => bool] => 'a set" @@ -99,35 +99,35 @@ "_INF" :: "[pttrn, 'a set, 'a => bool] => 'a set" ("(3INF _:_./ _)" 10) "_INF_U" :: "[pttrn, 'a => bool] => 'a set" - ("(3INF _./ _)" 10); + ("(3INF _./ _)" 10) translations "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. P" == "INF x:UNIV. P"; + "INF x. P" == "INF x:UNIV. P" (*>*) text{* The supremum of $B$ is less than any upper bound -of $B$.*}; +of $B$.*} -lemma sup_le_ub: "isUb A B y ==> is_Sup A B s ==> s <= y"; - by (unfold is_Sup_def, rule isLub_le_isUb); +lemma sup_le_ub: "isUb A B y ==> is_Sup A B s ==> s <= y" + by (unfold is_Sup_def, rule isLub_le_isUb) -text {* The supremum $B$ is an upper bound for $B$. *}; +text {* The supremum $B$ is an upper bound for $B$. *} -lemma sup_ub: "y:B ==> is_Sup A B s ==> y <= s"; - by (unfold is_Sup_def, rule isLubD2); +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$. *}; +than a lower bound of $B$. *} lemma sup_ub1: - "[| ALL y:B. a <= y; is_Sup A B s; x:B |] ==> a <= s"; -proof -; - assume "ALL 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"; .; -qed; + "[| ALL y:B. a <= y; is_Sup A B s; x:B |] ==> a <= s" +proof - + assume "ALL 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" . +qed -end; \ No newline at end of file +end \ No newline at end of file diff -r ea4dc7603f0b -r 371f023d3dbd src/HOL/Real/HahnBanach/FunctionNorm.thy --- a/src/HOL/Real/HahnBanach/FunctionNorm.thy Sun Jun 04 00:09:04 2000 +0200 +++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy Sun Jun 04 19:39:29 2000 +0200 @@ -3,43 +3,43 @@ Author: Gertrud Bauer, TU Munich *) -header {* The norm of a function *}; +header {* The norm of a function *} -theory FunctionNorm = NormedSpace + FunctionOrder:; +theory FunctionNorm = NormedSpace + FunctionOrder: -subsection {* Continuous linear forms*}; +subsection {* Continuous linear forms*} text{* A linear form $f$ on a normed vector space $(V, \norm{\cdot})$ is \emph{continuous}, iff it is bounded, i.~e. \[\Ex {c\in R}{\All {x\in V} {|f\ap x| \leq c \cdot \norm x}}\] In our application no other functions than linear forms are considered, so we can define continuous linear forms as bounded linear forms: -*}; +*} constdefs is_continuous :: "['a::{minus, plus} set, 'a => real, 'a => real] => bool" "is_continuous V norm f == - is_linearform V f & (EX c. ALL x:V. abs (f x) <= c * norm x)"; + is_linearform V f & (EX c. ALL x:V. abs (f x) <= c * norm x)" lemma continuousI [intro]: "[| is_linearform V f; !! x. x:V ==> abs (f x) <= c * norm x |] - ==> is_continuous V norm f"; -proof (unfold is_continuous_def, intro exI conjI ballI); - assume r: "!! x. x:V ==> abs (f x) <= c * norm x"; - fix x; assume "x:V"; show "abs (f x) <= c * norm x"; by (rule r); -qed; + ==> is_continuous V norm f" +proof (unfold is_continuous_def, intro exI conjI ballI) + assume r: "!! x. x:V ==> abs (f x) <= c * norm x" + fix x assume "x:V" show "abs (f x) <= c * norm x" by (rule r) +qed lemma continuous_linearform [intro??]: - "is_continuous V norm f ==> is_linearform V f"; - by (unfold is_continuous_def) force; + "is_continuous V norm f ==> is_linearform V f" + by (unfold is_continuous_def) force lemma continuous_bounded [intro??]: "is_continuous V norm f - ==> EX c. ALL x:V. abs (f x) <= c * norm x"; - by (unfold is_continuous_def) force; + ==> EX c. ALL x:V. abs (f x) <= c * norm x" + by (unfold is_continuous_def) force -subsection{* The norm of a linear form *}; +subsection{* The norm of a linear form *} text{* The least real number $c$ for which holds @@ -61,327 +61,327 @@ \[ \{ 0 \} \Un \left\{ \frac{|f\ap x|}{\norm x} \dt x\neq \zero \And x\in F\right\} \] -*}; +*} constdefs B :: "[ 'a set, 'a => real, 'a => real ] => real set" "B V norm f == - {(#0::real)} \Un {abs (f x) * rinv (norm x) | x. x ~= 00 & x:V}"; + {#0} Un {abs (f x) * rinv (norm x) | x. x ~= 00 & x:V}" text{* $n$ is the function norm of $f$, iff $n$ is the supremum of $B$. -*}; +*} constdefs is_function_norm :: " ['a set, 'a => real, 'a => real] => real => bool" - "is_function_norm V norm f fn == is_Sup UNIV (B V norm f) fn"; + "is_function_norm V norm f fn == is_Sup UNIV (B V norm f) fn" text{* $\idt{function{\dsh}norm}$ is equal to the supremum of $B$, -if the supremum exists. Otherwise it is undefined. *}; +if the supremum exists. Otherwise it is undefined. *} constdefs function_norm :: " ['a set, 'a => real, 'a => real] => real" - "function_norm V norm f == Sup UNIV (B V norm f)"; + "function_norm V norm f == Sup UNIV (B V norm f)" -lemma B_not_empty: "(#0::real) : B V norm f"; - by (unfold B_def, force); +lemma B_not_empty: "#0 : B V norm f" + by (unfold B_def, force) text {* The following lemma states that every continuous linear form -on a normed space $(V, \norm{\cdot})$ has a function norm. *}; +on a normed space $(V, \norm{\cdot})$ has a function norm. *} lemma ex_fnorm [intro??]: "[| is_normed_vectorspace V norm; is_continuous V norm f|] - ==> is_function_norm V norm f (function_norm V norm f)"; + ==> is_function_norm V norm f (function_norm V norm f)" proof (unfold function_norm_def is_function_norm_def - is_continuous_def Sup_def, elim conjE, rule selectI2EX); - assume "is_normed_vectorspace V norm"; + is_continuous_def Sup_def, elim conjE, rule selectI2EX) + assume "is_normed_vectorspace V norm" assume "is_linearform V f" - and e: "EX c. ALL x:V. abs (f x) <= c * norm x"; + and e: "EX c. ALL x:V. abs (f x) <= c * norm x" txt {* The existence of the supremum is shown using the completeness of the reals. Completeness means, that every non-empty bounded set of reals has a - supremum. *}; - show "EX a. is_Sup UNIV (B V norm f) a"; - proof (unfold is_Sup_def, rule reals_complete); + supremum. *} + show "EX 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: *}; + txt {* First we have to show that $B$ is non-empty: *} - show "EX X. X : B V norm f"; - proof (intro exI); - show "(#0::real) : (B V norm f)"; by (unfold B_def, force); - qed; + show "EX X. X : B V norm f" + proof (intro exI) + show "#0 : (B V norm f)" by (unfold B_def, force) + qed - txt {* Then we have to show that $B$ is bounded: *}; + txt {* Then we have to show that $B$ is bounded: *} - from e; show "EX Y. isUb UNIV (B V norm f) Y"; - proof; + from e show "EX Y. isUb UNIV (B V norm f) Y" + proof - txt {* We know that $f$ is bounded by some value $c$. *}; + txt {* We know that $f$ is bounded by some value $c$. *} - fix c; assume a: "ALL x:V. abs (f x) <= c * norm x"; - def b == "max c (#0::real)"; + fix c assume a: "ALL x:V. abs (f x) <= c * norm x" + def b == "max c #0" - show "?thesis"; + show "?thesis" proof (intro exI isUbI setleI ballI, unfold B_def, - elim UnE CollectE exE conjE singletonE); + elim UnE CollectE exE conjE singletonE) 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); + fix y assume "y = (#0::real)" + show "y <= b" by (simp! add: le_max2) txt{* The second case is $y = {|f\ap x|}/{\norm x}$ for some - $x\in V$ with $x \neq \zero$. *}; + $x\in V$ with $x \neq \zero$. *} - next; - fix x y; - assume "x:V" "x ~= 00"; (*** + next + fix x y + assume "x:V" "x ~= 00" (*** - have ge: "(#0::real) <= rinv (norm x)"; + have ge: "#0 <= rinv (norm x)"; by (rule real_less_imp_le, rule real_rinv_gt_zero, - rule normed_vs_norm_gt_zero); (*** + rule normed_vs_norm_gt_zero); ( *** proof (rule real_less_imp_le); - show "(#0::real) < rinv (norm x)"; + show "#0 < rinv (norm x)"; proof (rule real_rinv_gt_zero); - show "(#0::real) < norm x"; ..; + show "#0 < norm x"; ..; qed; - qed; ***) - have nz: "norm x ~= (#0::real)"; + qed; *** ) + have nz: "norm x ~= #0" by (rule not_sym, rule lt_imp_not_eq, - rule normed_vs_norm_gt_zero); (*** + rule normed_vs_norm_gt_zero) (*** proof (rule not_sym); - show "(#0::real) ~= norm x"; + show "#0 ~= norm x"; proof (rule lt_imp_not_eq); - show "(#0::real) < norm x"; ..; + show "#0 < norm x"; ..; qed; qed; ***)***) txt {* The thesis follows by a short calculation using the - fact that $f$ is bounded. *}; + fact that $f$ is bounded. *} - assume "y = abs (f x) * rinv (norm x)"; - also; have "... <= c * norm x * rinv (norm x)"; - proof (rule real_mult_le_le_mono2); - show "(#0::real) <= rinv (norm x)"; + assume "y = abs (f x) * rinv (norm x)" + also have "... <= c * norm x * rinv (norm x)" + proof (rule real_mult_le_le_mono2) + show "#0 <= rinv (norm x)" by (rule real_less_imp_le, rule real_rinv_gt_zero1, - rule normed_vs_norm_gt_zero); - from a; show "abs (f x) <= c * norm x"; ..; - qed; - also; have "... = c * (norm x * rinv (norm x))"; - by (rule real_mult_assoc); - also; have "(norm x * rinv (norm x)) = (#1::real)"; - proof (rule real_mult_inv_right1); - show nz: "norm x ~= (#0::real)"; + rule normed_vs_norm_gt_zero) + from a show "abs (f x) <= c * norm x" .. + qed + also have "... = c * (norm x * rinv (norm x))" + by (rule real_mult_assoc) + also have "(norm x * rinv (norm x)) = (#1::real)" + proof (rule real_mult_inv_right1) + show nz: "norm x ~= #0" by (rule not_sym, rule lt_imp_not_eq, - rule normed_vs_norm_gt_zero); - qed; - also; have "c * ... <= b "; by (simp! add: le_max1); - finally; show "y <= b"; .; - qed simp; - qed; - qed; -qed; + rule normed_vs_norm_gt_zero) + qed + also have "c * ... <= b " by (simp! add: le_max1) + finally show "y <= b" . + qed simp + qed + qed +qed -text {* The norm of a continuous function is always $\geq 0$. *}; +text {* The norm of a continuous function is always $\geq 0$. *} lemma fnorm_ge_zero [intro??]: "[| is_continuous V norm f; is_normed_vectorspace V norm|] - ==> (#0::real) <= function_norm V norm f"; -proof -; + ==> #0 <= function_norm V norm f" +proof - assume c: "is_continuous V norm f" - and n: "is_normed_vectorspace V norm"; + and n: "is_normed_vectorspace V norm" txt {* The function norm is defined as the supremum of $B$. So it is $\geq 0$ if all elements in $B$ are $\geq 0$, provided - the supremum exists and $B$ is not empty. *}; + the supremum exists and $B$ is not empty. *} - show ?thesis; - proof (unfold function_norm_def, rule sup_ub1); - show "ALL x:(B V norm f). (#0::real) <= x"; + show ?thesis + proof (unfold function_norm_def, rule sup_ub1) + show "ALL x:(B V norm f). #0 <= x" proof (intro ballI, unfold B_def, - elim UnE singletonE CollectE exE conjE); - fix x r; + elim UnE singletonE CollectE exE conjE) + fix x r assume "x : V" "x ~= 00" - and r: "r = abs (f x) * rinv (norm x)"; + and r: "r = abs (f x) * rinv (norm x)" - have ge: "(#0::real) <= abs (f x)"; by (simp! only: abs_ge_zero); - have "(#0::real) <= rinv (norm x)"; - by (rule real_less_imp_le, rule real_rinv_gt_zero1, rule);(*** + have ge: "#0 <= abs (f x)" by (simp! only: abs_ge_zero) + have "#0 <= rinv (norm x)" + by (rule real_less_imp_le, rule real_rinv_gt_zero1, rule)(*** proof (rule real_less_imp_le); - show "(#0::real) < rinv (norm x)"; + show "#0 < rinv (norm x)"; proof (rule real_rinv_gt_zero); - show "(#0::real) < norm x"; ..; + show "#0 < norm x"; ..; qed; qed; ***) - with ge; show "(#0::real) <= r"; - by (simp only: r, rule real_le_mult_order1a); - qed (simp!); + with ge show "#0 <= r" + by (simp only: r, rule real_le_mult_order1a) + qed (simp!) - txt {* Since $f$ is continuous the function norm exists: *}; + txt {* Since $f$ is continuous the function norm exists: *} - have "is_function_norm V norm f (function_norm V norm f)"; ..; - thus "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"; - by (unfold is_function_norm_def function_norm_def); + have "is_function_norm V norm f (function_norm V norm f)" .. + 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: *}; + txt {* $B$ is non-empty by construction: *} - show "(#0::real) : B V norm f"; by (rule B_not_empty); - qed; -qed; + show "#0 : B V norm f" by (rule B_not_empty) + qed +qed text{* \medskip The fundamental property of function norms is: \begin{matharray}{l} | f\ap x | \leq {\fnorm {f}} \cdot {\norm x} \end{matharray} -*}; +*} lemma norm_fx_le_norm_f_norm_x: "[| is_normed_vectorspace V norm; x:V; is_continuous V norm f |] - ==> abs (f x) <= function_norm V norm f * norm x"; -proof -; + ==> abs (f x) <= function_norm V norm f * norm x" +proof - assume "is_normed_vectorspace V norm" "x:V" - and c: "is_continuous V norm f"; - have v: "is_vectorspace V"; ..; - assume "x:V"; + and c: "is_continuous V norm f" + have v: "is_vectorspace V" .. + assume "x:V" - txt{* The proof is by case analysis on $x$. *}; + txt{* The proof is by case analysis on $x$. *} - show ?thesis; - proof cases; + show ?thesis + proof cases txt {* For the case $x = \zero$ the thesis follows from the linearity of $f$: for every linear function - holds $f\ap \zero = 0$. *}; + holds $f\ap \zero = 0$. *} - assume "x = 00"; - have "abs (f x) = abs (f 00)"; by (simp!); - also; from v continuous_linearform; have "f 00 = (#0::real)"; ..; - also; note abs_zero; - also; have "(#0::real) <= function_norm V norm f * norm x"; - proof (rule real_le_mult_order1a); - show "(#0::real) <= function_norm V norm f"; ..; - show "(#0::real) <= norm x"; ..; - qed; - finally; - show "abs (f x) <= function_norm V norm f * norm x"; .; + assume "x = 00" + have "abs (f x) = abs (f 00)" by (simp!) + also from v continuous_linearform have "f 00 = #0" .. + also note abs_zero + also have "#0 <= function_norm V norm f * norm x" + proof (rule real_le_mult_order1a) + show "#0 <= function_norm V norm f" .. + show "#0 <= norm x" .. + qed + finally + show "abs (f x) <= function_norm V norm f * norm x" . - next; - assume "x ~= 00"; - have n: "(#0::real) <= norm x"; ..; - have nz: "norm x ~= (#0::real)"; - proof (rule lt_imp_not_eq [RS not_sym]); - show "(#0::real) < norm x"; ..; - qed; + next + assume "x ~= 00" + have n: "#0 <= norm x" .. + have nz: "norm x ~= #0" + proof (rule lt_imp_not_eq [RS not_sym]) + show "#0 < norm x" .. + qed txt {* For the case $x\neq \zero$ we derive the following - fact from the definition of the function norm:*}; + fact from the definition of the function norm:*} - have l: "abs (f x) * rinv (norm x) <= function_norm V norm f"; - proof (unfold function_norm_def, rule sup_ub); - from ex_fnorm [OF _ c]; - show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"; - by (simp! add: is_function_norm_def function_norm_def); - show "abs (f x) * rinv (norm x) : B V norm f"; + have l: "abs (f x) * rinv (norm x) <= function_norm V norm f" + proof (unfold function_norm_def, rule sup_ub) + from ex_fnorm [OF _ c] + show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))" + by (simp! add: is_function_norm_def function_norm_def) + show "abs (f x) * rinv (norm x) : B V norm f" by (unfold B_def, intro UnI2 CollectI exI [of _ x] - conjI, simp); - qed; + conjI, simp) + qed - txt {* The thesis now follows by a short calculation: *}; + txt {* The thesis now follows by a short calculation: *} - have "abs (f x) = abs (f x) * (#1::real)"; by (simp!); - also; from nz; have "(#1::real) = rinv (norm x) * norm x"; - by (rule real_mult_inv_left1 [RS sym]); - also; - have "abs (f x) * ... = abs (f x) * rinv (norm x) * norm x"; - by (simp! add: real_mult_assoc [of "abs (f x)"]); - also; have "... <= function_norm V norm f * norm x"; - by (rule real_mult_le_le_mono2 [OF n l]); - finally; - show "abs (f x) <= function_norm V norm f * norm x"; .; - qed; -qed; + have "abs (f x) = abs (f x) * (#1::real)" by (simp!) + also from nz have "(#1::real) = rinv (norm x) * norm x" + by (rule real_mult_inv_left1 [RS sym]) + also + have "abs (f x) * ... = abs (f x) * rinv (norm x) * norm x" + by (simp! add: real_mult_assoc [of "abs (f x)"]) + also have "... <= function_norm V norm f * norm x" + by (rule real_mult_le_le_mono2 [OF n l]) + finally + show "abs (f x) <= function_norm V norm f * norm x" . + qed +qed text{* \medskip The function norm is the least positive real number for which the following inequation holds: \begin{matharray}{l} | f\ap x | \leq c \cdot {\norm x} \end{matharray} -*}; +*} lemma fnorm_le_ub: "[| is_normed_vectorspace V norm; is_continuous V norm f; - ALL x:V. abs (f x) <= c * norm x; (#0::real) <= c |] - ==> function_norm V norm f <= c"; -proof (unfold function_norm_def); - assume "is_normed_vectorspace V norm"; - assume c: "is_continuous V norm f"; + ALL x:V. abs (f x) <= c * norm x; #0 <= c |] + ==> function_norm V norm f <= c" +proof (unfold function_norm_def) + assume "is_normed_vectorspace V norm" + assume c: "is_continuous V norm f" assume fb: "ALL x:V. abs (f x) <= c * norm x" - and "(#0::real) <= c"; + 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 than the function norm since the function norm is the least upper bound. - *}; + *} - show "Sup UNIV (B V norm f) <= c"; - proof (rule sup_le_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 "Sup UNIV (B V norm f) <= c" + proof (rule sup_le_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) txt {* $c$ is an upper bound of $B$, i.~e.~every - $y\in B$ is less than $c$. *}; + $y\in B$ is less than $c$. *} - show "isUb UNIV (B V norm f) c"; - proof (intro isUbI setleI ballI); - fix y; assume "y: B V norm f"; - thus le: "y <= c"; - proof (unfold B_def, elim UnE CollectE exE conjE singletonE); + show "isUb UNIV (B V norm f) c" + proof (intro isUbI setleI ballI) + fix y assume "y: B V norm f" + thus le: "y <= c" + proof (unfold B_def, elim UnE CollectE exE conjE singletonE) - txt {* The first case for $y\in B$ is $y=0$. *}; + txt {* The first case for $y\in B$ is $y=0$. *} - assume "y = (#0::real)"; - show "y <= c"; by (force!); + assume "y = #0" + show "y <= c" by (force!) txt{* The second case is $y = {|f\ap x|}/{\norm x}$ for some - $x\in V$ with $x \neq \zero$. *}; + $x\in V$ with $x \neq \zero$. *} - next; - fix x; - assume "x : V" "x ~= 00"; + next + fix x + assume "x : V" "x ~= 00" - have lz: "(#0::real) < norm x"; - by (simp! add: normed_vs_norm_gt_zero); + have lz: "#0 < norm x" + by (simp! add: normed_vs_norm_gt_zero) - have nz: "norm x ~= (#0::real)"; - proof (rule not_sym); - from lz; show "(#0::real) ~= norm x"; - by (simp! add: order_less_imp_not_eq); - qed; + have nz: "norm x ~= #0" + proof (rule not_sym) + from lz show "#0 ~= norm x" + by (simp! add: order_less_imp_not_eq) + qed - from lz; have "(#0::real) < rinv (norm x)"; - by (simp! add: real_rinv_gt_zero1); - hence rinv_gez: "(#0::real) <= rinv (norm x)"; - by (rule real_less_imp_le); + from lz have "#0 < rinv (norm x)" + by (simp! add: real_rinv_gt_zero1) + hence rinv_gez: "#0 <= rinv (norm x)" + by (rule real_less_imp_le) - assume "y = abs (f x) * rinv (norm x)"; - also; from rinv_gez; have "... <= c * norm x * rinv (norm x)"; - proof (rule real_mult_le_le_mono2); - show "abs (f x) <= c * norm x"; by (rule bspec); - qed; - also; have "... <= c"; by (simp add: nz real_mult_assoc); - finally; show ?thesis; .; - qed; - qed force; - qed; -qed; + assume "y = abs (f x) * rinv (norm x)" + also from rinv_gez have "... <= c * norm x * rinv (norm x)" + proof (rule real_mult_le_le_mono2) + show "abs (f x) <= c * norm x" by (rule bspec) + qed + also have "... <= c" by (simp add: nz real_mult_assoc) + finally show ?thesis . + qed + qed force + qed +qed -end; \ No newline at end of file +end \ No newline at end of file diff -r ea4dc7603f0b -r 371f023d3dbd src/HOL/Real/HahnBanach/FunctionOrder.thy --- a/src/HOL/Real/HahnBanach/FunctionOrder.thy Sun Jun 04 00:09:04 2000 +0200 +++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy Sun Jun 04 19:39:29 2000 +0200 @@ -3,11 +3,11 @@ Author: Gertrud Bauer, TU Munich *) -header {* An order on functions *}; +header {* An order on functions *} -theory FunctionOrder = Subspace + Linearform:; +theory FunctionOrder = Subspace + Linearform: -subsection {* The graph of a function *}; +subsection {* The graph of a function *} text{* We define the \emph{graph} of a (real) function $f$ with domain $F$ as the set @@ -16,55 +16,55 @@ \] So we are modeling partial functions by specifying the domain and the mapping function. We use the term ``function'' also for its graph. -*}; +*} -types 'a graph = "('a * real) set"; +types 'a graph = "('a * real) set" 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"; - by (unfold graph_def, intro CollectI exI) force; +lemma graphI [intro??]: "x:F ==> (x, f x) : graph F f" + by (unfold graph_def, intro CollectI exI) force -lemma graphI2 [intro??]: "x:F ==> EX t: (graph F f). t = (x, f x)"; - by (unfold graph_def, force); +lemma graphI2 [intro??]: "x:F ==> EX t: (graph F f). t = (x, f x)" + by (unfold graph_def, force) -lemma graphD1 [intro??]: "(x, y): graph F f ==> x:F"; - by (unfold graph_def, elim CollectE exE) force; +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"; - by (unfold graph_def, elim CollectE exE) force; +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 *}; +subsection {* Functions ordered by domain extension *} text{* A function $h'$ is an extension of $h$, iff the graph of -$h$ is a subset of the graph of $h'$.*}; +$h$ is a subset of the graph of $h'$.*} lemma graph_extI: "[| !! x. x: H ==> h x = h' x; H <= H'|] - ==> graph H h <= graph H' h'"; - by (unfold graph_def, force); + ==> 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"; - by (unfold graph_def, force); + "[| graph H h <= graph H' h'; x:H |] ==> h x = h' x" + by (unfold graph_def, force) lemma graph_extD2 [intro??]: - "[| graph H h <= graph H' h' |] ==> H <= H'"; - by (unfold graph_def, force); + "[| graph H h <= graph H' h' |] ==> H <= H'" + by (unfold graph_def, force) -subsection {* Domain and function of a graph *}; +subsection {* Domain and function of a graph *} text{* The inverse functions to $\idt{graph}$ are $\idt{domain}$ and -$\idt{funct}$.*}; +$\idt{funct}$.*} constdefs domain :: "'a graph => 'a set" "domain g == {x. EX 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} @@ -72,32 +72,32 @@ \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. *}; +if the relation induced by $g$ is unique. *} lemma graph_domain_funct: "(!!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 "EX y. (a, y) : g"; ..; - assume uniq: "!!x y z. (x, y):g ==> (x, z):g ==> z = y"; - show "b = (SOME y. (a, y) : g)"; - proof (rule select_equality [RS sym]); - fix y; assume "(a, y):g"; show "y = b"; by (rule uniq); - qed; -qed; + ==> graph (domain g) (funct g) = g" +proof (unfold domain_def funct_def graph_def, auto) + fix a b assume "(a, b) : g" + show "(a, SOME y. (a, y) : g) : g" by (rule selectI2) + show "EX y. (a, y) : g" .. + assume uniq: "!!x y z. (x, y):g ==> (x, z):g ==> z = y" + show "b = (SOME y. (a, y) : g)" + proof (rule select_equality [RS sym]) + fix y assume "(a, y):g" show "y = b" by (rule uniq) + qed +qed -subsection {* Norm-preserving extensions of a function *}; +subsection {* Norm-preserving extensions of a function *} text {* Given a linear form $f$ on the space $F$ and a seminorm $p$ on $E$. The set of all linear extensions of $f$, to superspaces $H$ of -$F$, which are bounded by $p$, is defined as follows. *}; +$F$, which are bounded by $p$, is defined as follows. *} constdefs @@ -110,7 +110,7 @@ & is_subspace H E & is_subspace F H & graph F f <= graph H h - & (ALL x:H. h x <= p x)}"; + & (ALL x:H. h x <= p x)}" lemma norm_pres_extension_D: "g : norm_pres_extensions E p F f @@ -119,14 +119,14 @@ & is_subspace H E & is_subspace F H & graph F f <= graph H h - & (ALL x:H. h x <= p x)"; - by (unfold norm_pres_extensions_def) force; + & (ALL 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; ALL x:H. h x <= p x |] - ==> (graph H h : norm_pres_extensions E p F f)"; - by (unfold norm_pres_extensions_def) force; + ==> (graph H h : norm_pres_extensions E p F f)" + by (unfold norm_pres_extensions_def) force lemma norm_pres_extensionI [intro]: "EX H h. graph H h = g @@ -135,8 +135,7 @@ & is_subspace F H & graph F f <= graph H h & (ALL x:H. h x <= p x) - ==> g: norm_pres_extensions E p F f"; - by (unfold norm_pres_extensions_def) force; + ==> g: norm_pres_extensions E p F f" + by (unfold norm_pres_extensions_def) force -end; - +end \ No newline at end of file diff -r ea4dc7603f0b -r 371f023d3dbd src/HOL/Real/HahnBanach/HahnBanach.thy --- a/src/HOL/Real/HahnBanach/HahnBanach.thy Sun Jun 04 00:09:04 2000 +0200 +++ b/src/HOL/Real/HahnBanach/HahnBanach.thy Sun Jun 04 19:39:29 2000 +0200 @@ -3,17 +3,17 @@ Author: Gertrud Bauer, TU Munich *) -header {* The Hahn-Banach Theorem *}; +header {* The Hahn-Banach Theorem *} theory HahnBanach - = HahnBanachSupLemmas + HahnBanachExtLemmas + ZornLemma:; + = HahnBanachSupLemmas + HahnBanachExtLemmas + ZornLemma: text {* We present the proof of two different versions of the Hahn-Banach Theorem, closely following \cite[\S36]{Heuser:1986}. -*}; +*} -subsection {* The Hahn-Banach Theorem for vector spaces *}; +subsection {* The Hahn-Banach Theorem for vector spaces *} text {* {\bf Theorem.} Let $f$ be a linear form defined on a subspace $F$ of a real vector space $E$, such that $f$ is bounded by a seminorm @@ -32,282 +32,282 @@ a norm-preserving way to a greater vector space $H_0$. So $g$ cannot be maximal in $M$. \bigskip -*}; +*} theorem HahnBanach: "[| is_vectorspace E; is_subspace F E; is_seminorm E p; is_linearform F f; ALL x:F. f x <= p x |] ==> EX h. is_linearform E h & (ALL x:F. h x = f x) - & (ALL x:E. h x <= p x)"; -proof -; + & (ALL x:E. h x <= p x)" +proof - -txt {* 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$. *}; +txt {* 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$. *} assume "is_vectorspace E" "is_subspace F E" "is_seminorm E p" - "is_linearform F f" "ALL x:F. f x <= p x"; + "is_linearform F f" "ALL x:F. f x <= p x" -txt {* Define $M$ as the set of all norm-preserving extensions of $F$. *}; +txt {* Define $M$ as the set of all norm-preserving extensions of $F$. *} - def M == "norm_pres_extensions E p F f"; - {; - fix c; assume "c : chain M" "EX x. x:c"; + def M == "norm_pres_extensions E p F f" + { + fix c assume "c : chain M" "EX x. x:c" -txt {* Show that every non-empty chain $c$ in $M$ has an upper bound in $M$: $\Union c$ is greater that every element of the chain $c$, so $\Union c$ is an upper bound of $c$ that lies in $M$. *}; +txt {* Show that every non-empty chain $c$ in $M$ has an upper bound in $M$: $\Union c$ is greater that every element of the chain $c$, so $\Union c$ is an upper bound of $c$ that lies in $M$. *} - have "Union c : M"; - proof (unfold M_def, rule norm_pres_extensionI); + have "Union c : M" + proof (unfold M_def, rule norm_pres_extensionI) show "EX (H::'a set) h::'a => real. graph H h = Union c & is_linearform H h & is_subspace H E & is_subspace F H & graph F f <= graph H h - & (ALL x::'a:H. h x <= p x)"; - proof (intro exI conjI); - let ?H = "domain (Union c)"; - let ?h = "funct (Union c)"; + & (ALL x::'a:H. h x <= p x)" + proof (intro exI conjI) + let ?H = "domain (Union c)" + let ?h = "funct (Union c)" - show a: "graph ?H ?h = Union c"; - proof (rule graph_domain_funct); - fix x y z; assume "(x, y) : Union c" "(x, z) : Union c"; - show "z = y"; by (rule sup_definite); - qed; - show "is_linearform ?H ?h"; - by (simp! add: sup_lf a); - show "is_subspace ?H E"; - by (rule sup_subE [OF _ _ _ a]) (simp!)+; - show "is_subspace F ?H"; - by (rule sup_supF [OF _ _ _ a]) (simp!)+; - show "graph F f <= graph ?H ?h"; - by (rule sup_ext [OF _ _ _ a]) (simp!)+; - show "ALL x::'a:?H. ?h x <= p x"; - by (rule sup_norm_pres [OF _ _ a]) (simp!)+; - qed; - qed; - }; + show a: "graph ?H ?h = Union c" + proof (rule graph_domain_funct) + fix x y z assume "(x, y) : Union c" "(x, z) : Union c" + show "z = y" by (rule sup_definite) + qed + show "is_linearform ?H ?h" + by (simp! add: sup_lf a) + show "is_subspace ?H E" + by (rule sup_subE [OF _ _ _ a]) (simp!)+ + show "is_subspace F ?H" + by (rule sup_supF [OF _ _ _ a]) (simp!)+ + show "graph F f <= graph ?H ?h" + by (rule sup_ext [OF _ _ _ a]) (simp!)+ + show "ALL x::'a:?H. ?h x <= p x" + by (rule sup_norm_pres [OF _ _ a]) (simp!)+ + qed + qed + } -txt {* With Zorn's Lemma we can conclude that there is a maximal element $g$ in $M$. *}; +txt {* With Zorn's Lemma we can conclude that there is a maximal element $g$ in $M$. *} - hence "EX g:M. ALL x:M. g <= x --> g = x"; - proof (rule Zorn's_Lemma); - txt {* We show that $M$ is non-empty: *}; - 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!); - qed; - thus ?thesis; - proof; + hence "EX g:M. ALL x:M. g <= x --> g = x" + proof (rule Zorn's_Lemma) + txt {* We show that $M$ is non-empty: *} + 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!) + qed + thus ?thesis + proof -txt {* We take this maximal element $g$. *}; +txt {* We take this maximal element $g$. *} - fix g; assume "g:M" "ALL x:M. g <= x --> g = x"; - show ?thesis; + fix g assume "g:M" "ALL x:M. g <= x --> g = x" + show ?thesis txt {* $g$ is a norm-preserving extension of $f$, that is: $g$ is the graph of a linear form $h$, defined on a subspace $H$ of $E$, which is a superspace of $F$. $h$ is an extension of $f$ - and $h$ is again bounded by $p$. *}; + and $h$ is again bounded by $p$. *} 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" - "ALL x:H. h x <= p x"; - proof -; + "ALL x:H. h x <= p x" + proof - have "EX H h. graph H h = g & is_linearform H h & is_subspace H E & is_subspace F H & graph F f <= graph H h - & (ALL x:H. h x <= p x)"; by (simp! add: norm_pres_extension_D); - thus ?thesis; by (elim exE conjE) rule; - qed; - have h: "is_vectorspace H"; ..; + & (ALL 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" .. -txt {* We show that $h$ is defined on whole $E$ by classical contradiction. *}; +txt {* We show that $h$ is defined on whole $E$ by classical contradiction. *} - have "H = E"; - proof (rule classical); + have "H = E" + proof (rule classical) - txt {* Assume $h$ is not defined on whole $E$. *}; + txt {* Assume $h$ is not defined on whole $E$. *} - assume "H ~= E"; + assume "H ~= E" -txt {* Then show that $h$ can be extended in a norm-preserving way to a function $h_0$ with the graph $g_{h0}$. *}; +txt {* Then show that $h$ can be extended in a norm-preserving way to a function $h_0$ with the graph $g_{h0}$. *} - have "EX g_h0 : M. g <= g_h0 & g ~= g_h0"; + have "EX g_h0 : M. g <= g_h0 & g ~= g_h0" - txt {* Consider $x_0 \in E \setminus H$. *}; + txt {* Consider $x_0 \in E \setminus H$. *} - obtain x0 where "x0:E" "x0~:H"; - proof -; - have "EX x0:E. x0~:H"; - proof (rule set_less_imp_diff_not_empty); - have "H <= E"; ..; - thus "H < E"; ..; - qed; - thus ?thesis; by blast; - qed; - have x0: "x0 ~= 00"; - proof (rule classical); - presume "x0 = 00"; - with h; have "x0:H"; by simp; - thus ?thesis; by contradiction; - qed blast; + obtain x0 where "x0:E" "x0~:H" + proof - + have "EX x0:E. x0~:H" + proof (rule set_less_imp_diff_not_empty) + have "H <= E" .. + thus "H < E" .. + qed + thus ?thesis by blast + qed + have x0: "x0 ~= 00" + proof (rule classical) + presume "x0 = 00" + with h have "x0:H" by simp + thus ?thesis by contradiction + qed blast -txt {* Define $H_0$ as the direct sum of $H$ and the linear closure of $x_0$. *}; +txt {* Define $H_0$ as the direct sum of $H$ and the linear closure of $x_0$. *} - def H0 == "H + lin x0"; - show ?thesis; + def H0 == "H + lin x0" + show ?thesis txt {* Pick a real number $\xi$ that fulfills certain inequations, which will be used to establish that $h_0$ is - a norm-preserving extension of $h$. *}; + a norm-preserving extension of $h$. *} obtain xi where "ALL y:H. - p (y + x0) - h y <= xi - & xi <= p (y + x0) - h y"; - proof -; - from h; have "EX xi. ALL y:H. - p (y + x0) - h y <= xi - & xi <= p (y + x0) - h y"; - proof (rule ex_xi); - 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)"; - by (simp!); - also; have "v - u = x0 + - x0 + v + - u"; - by (simp! add: diff_eq1); - also; have "... = v + x0 + - (u + x0)"; - by (simp!); - also; have "... = (v + x0) - (u + x0)"; - by (simp! add: diff_eq1); - also; have "p ... <= p (v + x0) + p (u + x0)"; - by (rule seminorm_diff_subadditive) (simp!)+; - finally; have "h v - h u <= p (v + x0) + p (u + x0)"; .; + & xi <= p (y + x0) - h y" + proof - + from h have "EX xi. ALL y:H. - p (y + x0) - h y <= xi + & xi <= p (y + x0) - h y" + proof (rule ex_xi) + 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)" + by (simp!) + also have "v - u = x0 + - x0 + v + - u" + by (simp! add: diff_eq1) + also have "... = v + x0 + - (u + x0)" + by (simp!) + also have "... = (v + x0) - (u + x0)" + by (simp! add: diff_eq1) + also have "p ... <= p (v + x0) + p (u + x0)" + by (rule seminorm_diff_subadditive) (simp!)+ + finally have "h v - h u <= p (v + x0) + p (u + x0)" . - thus "- p (u + x0) - h u <= p (v + x0) - h v"; - by (rule real_diff_ineq_swap); - qed; - thus ?thesis; by rule rule; - qed; + thus "- p (u + x0) - h u <= p (v + x0) - h v" + by (rule real_diff_ineq_swap) + qed + thus ?thesis by rule rule + qed -txt {* Define the extension $h_0$ of $h$ to $H_0$ using $\xi$. *}; +txt {* Define the extension $h_0$ of $h$ to $H_0$ using $\xi$. *} def h0 == "\\x. let (y,a) = SOME (y, a). x = y + a (*) x0 & y:H - in (h y) + a * xi"; - show ?thesis; - proof; + in (h y) + a * xi" + show ?thesis + proof -txt {* Show that $h_0$ is an extension of $h$ *}; +txt {* Show that $h_0$ is an extension of $h$ *} - show "g <= graph H0 h0 & g ~= graph H0 h0"; - proof; - show "g <= graph H0 h0"; - proof -; - have "graph H h <= graph H0 h0"; - proof (rule graph_extI); - fix t; assume "t:H"; + show "g <= graph H0 h0 & g ~= graph H0 h0" + proof + show "g <= graph H0 h0" + proof - + have "graph H h <= graph H0 h0" + proof (rule graph_extI) + fix t assume "t:H" have "(SOME (y, a). t = y + a (*) x0 & y : H) - = (t,#0)"; - by (rule decomp_H0_H [OF _ _ _ _ _ x0]); - thus "h t = h0 t"; by (simp! add: Let_def); - next; - show "H <= H0"; - proof (rule subspace_subset); - show "is_subspace H H0"; - proof (unfold H0_def, rule subspace_vs_sum1); - show "is_vectorspace H"; ..; - show "is_vectorspace (lin x0)"; ..; - qed; - qed; - qed; - thus ?thesis; by (simp!); - qed; - show "g ~= graph H0 h0"; - proof -; - have "graph H h ~= graph H0 h0"; - proof; - assume e: "graph H h = graph H0 h0"; - have "x0 : H0"; - proof (unfold H0_def, rule vs_sumI); - show "x0 = 00 + x0"; by (simp!); - from h; show "00 : H"; ..; - show "x0 : lin x0"; by (rule x_lin_x); - qed; - hence "(x0, h0 x0) : graph H0 h0"; ..; - with e; have "(x0, h0 x0) : graph H h"; by simp; - hence "x0 : H"; ..; - thus False; by contradiction; - qed; - thus ?thesis; by (simp!); - qed; - qed; + = (t,#0)" + by (rule decomp_H0_H [OF _ _ _ _ _ x0]) + thus "h t = h0 t" by (simp! add: Let_def) + next + show "H <= H0" + proof (rule subspace_subset) + show "is_subspace H H0" + proof (unfold H0_def, rule subspace_vs_sum1) + show "is_vectorspace H" .. + show "is_vectorspace (lin x0)" .. + qed + qed + qed + thus ?thesis by (simp!) + qed + show "g ~= graph H0 h0" + proof - + have "graph H h ~= graph H0 h0" + proof + assume e: "graph H h = graph H0 h0" + have "x0 : H0" + proof (unfold H0_def, rule vs_sumI) + show "x0 = 00 + x0" by (simp!) + from h show "00 : H" .. + show "x0 : lin x0" by (rule x_lin_x) + qed + hence "(x0, h0 x0) : graph H0 h0" .. + with e have "(x0, h0 x0) : graph H h" by simp + hence "x0 : H" .. + thus False by contradiction + qed + thus ?thesis by (simp!) + qed + qed -txt {* and $h_0$ is norm-preserving. *}; +txt {* and $h_0$ is norm-preserving. *} - show "graph H0 h0 : M"; - proof -; - have "graph H0 h0 : norm_pres_extensions E p F f"; - proof (rule norm_pres_extensionI2); - show "is_linearform H0 h0"; - by (rule h0_lf [OF _ _ _ _ _ _ x0]) (simp!)+; - show "is_subspace H0 E"; - by (unfold H0_def) (rule vs_sum_subspace [OF _ lin_subspace]); - have "is_subspace F H"; .; - also; from h lin_vs; - have [fold H0_def]: "is_subspace H (H + lin x0)"; ..; - finally (subspace_trans [OF _ h]); - show f_h0: "is_subspace F H0"; .; + show "graph H0 h0 : M" + proof - + have "graph H0 h0 : norm_pres_extensions E p F f" + proof (rule norm_pres_extensionI2) + show "is_linearform H0 h0" + by (rule h0_lf [OF _ _ _ _ _ _ x0]) (simp!)+ + show "is_subspace H0 E" + by (unfold H0_def) (rule vs_sum_subspace [OF _ lin_subspace]) + have "is_subspace F H" . + also from h lin_vs + have [fold H0_def]: "is_subspace H (H + lin x0)" .. + finally (subspace_trans [OF _ h]) + show f_h0: "is_subspace F H0" . - show "graph F f <= graph H0 h0"; - proof (rule graph_extI); - 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)"; - by (simp add: Let_def); - also; have - "(x, #0) = (SOME (y, a). x = y + a (*) x0 & y : H)"; - by (rule decomp_H0_H [RS sym, OF _ _ _ _ _ x0]) (simp!)+; - also; have + show "graph F f <= graph H0 h0" + proof (rule graph_extI) + 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)" + by (simp add: Let_def) + also have + "(x, #0) = (SOME (y, a). x = y + a (*) x0 & y : H)" + by (rule decomp_H0_H [RS sym, OF _ _ _ _ _ x0]) (simp!)+ + also have "(let (y,a) = (SOME (y,a). x = y + a (*) x0 & y : H) in h y + a * xi) - = h0 x"; by (simp!); - finally; show "f x = h0 x"; .; - next; - from f_h0; show "F <= H0"; ..; - qed; + = h0 x" by (simp!) + finally show "f x = h0 x" . + next + from f_h0 show "F <= H0" .. + qed - show "ALL x:H0. h0 x <= p x"; - by (rule h0_norm_pres [OF _ _ _ _ x0]); - qed; - thus "graph H0 h0 : M"; by (simp!); - qed; - qed; - qed; - qed; + show "ALL x:H0. h0 x <= p x" + by (rule h0_norm_pres [OF _ _ _ _ x0]) + qed + thus "graph H0 h0 : M" by (simp!) + qed + qed + qed + qed -txt {* So the graph $g$ of $h$ cannot be maximal. Contradiction. *}; +txt {* So the graph $g$ of $h$ cannot be maximal. Contradiction. *} - hence "~ (ALL x:M. g <= x --> g = x)"; by simp; - thus ?thesis; by contradiction; - qed; + hence "~ (ALL x:M. g <= x --> g = x)" by simp + thus ?thesis by contradiction + qed txt {* Now we have a linear extension $h$ of $f$ to $E$ that is -bounded by $p$. *}; +bounded by $p$. *} thus "EX h. is_linearform E h & (ALL x:F. h x = f x) - & (ALL x:E. h x <= p x)"; - proof (intro exI conjI); - assume eq: "H = E"; - from eq; show "is_linearform E h"; by (simp!); - show "ALL x:F. h x = f x"; - proof (intro ballI, rule sym); - fix x; assume "x:F"; show "f x = h x "; ..; - qed; - from eq; show "ALL x:E. h x <= p x"; by (force!); - qed; - qed; - qed; -qed; + & (ALL x:E. h x <= p x)" + proof (intro exI conjI) + assume eq: "H = E" + from eq show "is_linearform E h" by (simp!) + show "ALL x:F. h x = f x" + proof (intro ballI, rule sym) + fix x assume "x:F" show "f x = h x " .. + qed + from eq show "ALL x:E. h x <= p x" by (force!) + qed + qed + qed +qed (* theorem HahnBanach: "[| is_vectorspace E; is_subspace F E; is_seminorm E p; @@ -320,69 +320,69 @@ "is_linearform F f" "ALL x:F. f x <= p x"; txt{* We define $M$ to be the set of all linear extensions - of $f$ to superspaces of $F$, which are bounded by $p$. *}; + of $f$ to superspaces of $F$, which are bounded by $p$. *} - def M == "norm_pres_extensions E p F f"; + def M == "norm_pres_extensions E p F f" - txt{* We show that $M$ is non-empty: *}; + txt{* We show that $M$ is non-empty: *} - have aM: "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!)+; + have aM: "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!)+ - subsubsect {* Existence of a limit function *}; + subsubsect {* Existence of a limit function *} txt {* For every non-empty chain of norm-preserving extensions the union of all functions in the chain is again a norm-preserving extension. (The union is an upper bound for all elements. It is even the least upper bound, because every upper bound of $M$ - is also an upper bound for $\Union c$, as $\Union c\in M$) *}; + is also an upper bound for $\Union c$, as $\Union c\in M$) *} - {; - fix c; assume "c:chain M" "EX x. x:c"; - have "Union c : M"; + { + fix c assume "c:chain M" "EX x. x:c" + have "Union c : M" - proof (unfold M_def, rule norm_pres_extensionI); + proof (unfold M_def, rule norm_pres_extensionI) show "EX (H::'a set) h::'a => real. graph H h = Union c & is_linearform H h & is_subspace H E & is_subspace F H & graph F f <= graph H h - & (ALL x::'a:H. h x <= p x)"; - proof (intro exI conjI); - let ?H = "domain (Union c)"; - let ?h = "funct (Union c)"; + & (ALL x::'a:H. h x <= p x)" + proof (intro exI conjI) + let ?H = "domain (Union c)" + let ?h = "funct (Union c)" - show a: "graph ?H ?h = Union c"; - proof (rule graph_domain_funct); - fix x y z; assume "(x, y) : Union c" "(x, z) : Union c"; - show "z = y"; by (rule sup_definite); - qed; - show "is_linearform ?H ?h"; - by (simp! add: sup_lf a); - show "is_subspace ?H E"; - 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"; - by (rule sup_ext, rule a) (simp!)+; - show "ALL x::'a:?H. ?h x <= p x"; - by (rule sup_norm_pres, rule a) (simp!)+; - qed; - qed; - }; + show a: "graph ?H ?h = Union c" + proof (rule graph_domain_funct) + fix x y z assume "(x, y) : Union c" "(x, z) : Union c" + show "z = y" by (rule sup_definite) + qed + show "is_linearform ?H ?h" + by (simp! add: sup_lf a) + show "is_subspace ?H E" + 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" + by (rule sup_ext, rule a) (simp!)+ + show "ALL x::'a:?H. ?h x <= p x" + by (rule sup_norm_pres, rule a) (simp!)+ + qed + qed + } txt {* According to Zorn's Lemma there is - a maximal norm-preserving extension $g\in M$. *}; + a maximal norm-preserving extension $g\in M$. *} - with aM; have bex_g: "EX g:M. ALL x:M. g <= x --> g = x"; - by (simp! add: Zorn's_Lemma); + with aM have bex_g: "EX g:M. ALL x:M. g <= x --> g = x" + by (simp! add: Zorn's_Lemma) - thus ?thesis; - proof; - fix g; assume g: "g:M" "ALL x:M. g <= x --> g = x"; + thus ?thesis + proof + fix g assume g: "g:M" "ALL x:M. g <= x --> g = x" have ex_Hh: "EX H h. graph H h = g @@ -390,145 +390,145 @@ & is_subspace H E & is_subspace F H & graph F f <= graph H h - & (ALL x:H. h x <= p x) "; - by (simp! add: norm_pres_extension_D); - thus ?thesis; - proof (elim exE conjE, intro exI); - fix H h; + & (ALL x:H. h x <= p x) " + by (simp! add: norm_pres_extension_D) + thus ?thesis + proof (elim exE conjE, intro exI) + fix H h assume "graph H h = g" "is_linearform (H::'a set) h" "is_subspace H E" "is_subspace F H" and h_ext: "graph F f <= graph H h" - and h_bound: "ALL x:H. h x <= p x"; + and h_bound: "ALL x:H. h x <= p x" - have h: "is_vectorspace H"; ..; - have f: "is_vectorspace F"; ..; + have h: "is_vectorspace H" .. + have f: "is_vectorspace F" .. -subsubsect {* The domain of the limit function *}; +subsubsect {* The domain of the limit function *} -have eq: "H = E"; -proof (rule classical); +have eq: "H = E" +proof (rule classical) -txt {* Assume that the domain of the supremum is not $E$, *}; +txt {* Assume that the domain of the supremum is not $E$, *} - assume "H ~= E"; - have "H <= E"; ..; - hence "H < E"; ..; + assume "H ~= E" + have "H <= E" .. + hence "H < E" .. - txt{* then there exists an element $x_0$ in $E \setminus H$: *}; + txt{* then there exists an element $x_0$ in $E \setminus H$: *} - hence "EX x0:E. x0~:H"; - by (rule set_less_imp_diff_not_empty); + hence "EX x0:E. x0~:H" + by (rule set_less_imp_diff_not_empty) txt {* We get that $h$ can be extended in a - norm-preserving way to some $H_0$. *}; + norm-preserving way to some $H_0$. *} hence "EX H0 h0. g <= graph H0 h0 & g ~= graph H0 h0 - & graph H0 h0 : M"; - proof; - fix x0; assume "x0:E" "x0~:H"; + & graph H0 h0 : M" + proof + fix x0 assume "x0:E" "x0~:H" - have x0: "x0 ~= 00"; - proof (rule classical); - presume "x0 = 00"; - with h; have "x0:H"; by simp; - thus ?thesis; by contradiction; - qed blast; + have x0: "x0 ~= 00" + proof (rule classical) + presume "x0 = 00" + with h have "x0:H" by simp + thus ?thesis by contradiction + qed blast txt {* Define $H_0$ as the (direct) sum of H and the - linear closure of $x_0$. \label{ex-xi-use}*}; + linear closure of $x_0$. \label{ex-xi-use}*} - def H0 == "H + lin x0"; + def H0 == "H + lin x0" - from h; have xi: "EX xi. ALL y:H. - p (y + x0) - h y <= xi - & xi <= p (y + x0) - h y"; - proof (rule ex_xi); - fix u v; assume "u:H" "v:H"; - from h; have "h v - h u = h (v - u)"; - by (simp! add: linearform_diff); - also; from h_bound; have "... <= p (v - u)"; - by (simp!); - also; have "v - u = x0 + - x0 + v + - u"; - by (simp! add: diff_eq1); - also; have "... = v + x0 + - (u + x0)"; - by (simp!); - also; have "... = (v + x0) - (u + x0)"; - by (simp! add: diff_eq1); - also; have "p ... <= p (v + x0) + p (u + x0)"; - by (rule seminorm_diff_subadditive) (simp!)+; - finally; have "h v - h u <= p (v + x0) + p (u + x0)"; .; + from h have xi: "EX xi. ALL y:H. - p (y + x0) - h y <= xi + & xi <= p (y + x0) - h y" + proof (rule ex_xi) + fix u v assume "u:H" "v:H" + from h have "h v - h u = h (v - u)" + by (simp! add: linearform_diff) + also from h_bound have "... <= p (v - u)" + by (simp!) + also have "v - u = x0 + - x0 + v + - u" + by (simp! add: diff_eq1) + also have "... = v + x0 + - (u + x0)" + by (simp!) + also have "... = (v + x0) - (u + x0)" + by (simp! add: diff_eq1) + also have "p ... <= p (v + x0) + p (u + x0)" + by (rule seminorm_diff_subadditive) (simp!)+ + finally have "h v - h u <= p (v + x0) + p (u + x0)" . - thus "- p (u + x0) - h u <= p (v + x0) - h v"; - by (rule real_diff_ineq_swap); - qed; + thus "- p (u + x0) - h u <= p (v + x0) - h v" + by (rule real_diff_ineq_swap) + qed hence "EX h0. g <= graph H0 h0 & g ~= graph H0 h0 - & graph H0 h0 : M"; - proof (elim exE, intro exI conjI); - fix xi; + & graph H0 h0 : M" + proof (elim exE, intro exI conjI) + fix xi assume a: "ALL y:H. - p (y + x0) - h y <= xi - & xi <= p (y + x0) - h y"; + & xi <= p (y + x0) - h y" txt {* Define $h_0$ as the canonical linear extension - of $h$ on $H_0$:*}; + of $h$ on $H_0$:*} def h0 == "\\x. let (y,a) = SOME (y, a). x = y + a ( * ) x0 & y:H - in (h y) + a * xi"; + in (h y) + a * xi" txt {* We get that the graph of $h_0$ extends that of - $h$. *}; + $h$. *} - have "graph H h <= graph H0 h0"; - proof (rule graph_extI); - fix t; assume "t:H"; - have "(SOME (y, a). t = y + a ( * ) x0 & y : H) = (t,#0)"; - by (rule decomp_H0_H, rule x0); - thus "h t = h0 t"; by (simp! add: Let_def); - next; - show "H <= H0"; - proof (rule subspace_subset); - show "is_subspace H H0"; - proof (unfold H0_def, rule subspace_vs_sum1); - show "is_vectorspace H"; ..; - show "is_vectorspace (lin x0)"; ..; - qed; - qed; - qed; - thus "g <= graph H0 h0"; by (simp!); + have "graph H h <= graph H0 h0" + proof (rule graph_extI) + fix t assume "t:H" + have "(SOME (y, a). t = y + a ( * ) x0 & y : H) = (t,#0)" + by (rule decomp_H0_H, rule x0) + thus "h t = h0 t" by (simp! add: Let_def) + next + show "H <= H0" + proof (rule subspace_subset) + show "is_subspace H H0" + proof (unfold H0_def, rule subspace_vs_sum1) + show "is_vectorspace H" .. + show "is_vectorspace (lin x0)" .. + qed + qed + qed + thus "g <= graph H0 h0" by (simp!) - txt {* Apparently $h_0$ is not equal to $h$. *}; + txt {* Apparently $h_0$ is not equal to $h$. *} - have "graph H h ~= graph H0 h0"; - proof; - assume e: "graph H h = graph H0 h0"; - have "x0 : H0"; - proof (unfold H0_def, rule vs_sumI); - show "x0 = 00 + x0"; by (simp!); - from h; show "00 : H"; ..; - show "x0 : lin x0"; by (rule x_lin_x); - qed; - hence "(x0, h0 x0) : graph H0 h0"; ..; - with e; have "(x0, h0 x0) : graph H h"; by simp; - hence "x0 : H"; ..; - thus False; by contradiction; - qed; - thus "g ~= graph H0 h0"; by (simp!); + have "graph H h ~= graph H0 h0" + proof + assume e: "graph H h = graph H0 h0" + have "x0 : H0" + proof (unfold H0_def, rule vs_sumI) + show "x0 = 00 + x0" by (simp!) + from h show "00 : H" .. + show "x0 : lin x0" by (rule x_lin_x) + qed + hence "(x0, h0 x0) : graph H0 h0" .. + with e have "(x0, h0 x0) : graph H h" by simp + hence "x0 : H" .. + thus False by contradiction + qed + thus "g ~= graph H0 h0" by (simp!) txt {* Furthermore $h_0$ is a norm-preserving extension - of $f$. *}; + of $f$. *} - have "graph H0 h0 : norm_pres_extensions E p F f"; - proof (rule norm_pres_extensionI2); - show "is_linearform H0 h0"; - by (rule h0_lf, rule x0) (simp!)+; - show "is_subspace H0 E"; + have "graph H0 h0 : norm_pres_extensions E p F f" + proof (rule norm_pres_extensionI2) + show "is_linearform H0 h0" + by (rule h0_lf, rule x0) (simp!)+ + show "is_subspace H0 E" by (unfold H0_def, rule vs_sum_subspace, - rule lin_subspace); + rule lin_subspace) - have "is_subspace F H"; .; - also; from h lin_vs; - have [fold H0_def]: "is_subspace H (H + lin x0)"; ..; - finally (subspace_trans [OF _ h]); - show f_h0: "is_subspace F H0"; .; (*** + have "is_subspace F H" . + also from h lin_vs + have [fold H0_def]: "is_subspace H (H + lin x0)" .. + finally (subspace_trans [OF _ h]) + show f_h0: "is_subspace F H0" . (*** backwards: show f_h0: "is_subspace F H0"; .; proof (rule subspace_trans [of F H H0]); @@ -537,63 +537,63 @@ thus "is_subspace H H0"; by (unfold H0_def); qed; ***) - show "graph F f <= graph H0 h0"; - proof (rule graph_extI); - 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)"; - by (simp add: Let_def); - also; have - "(x, #0) = (SOME (y, a). x = y + a ( * ) x0 & y : H)"; - by (rule decomp_H0_H [RS sym], rule x0) (simp!)+; - also; have + show "graph F f <= graph H0 h0" + proof (rule graph_extI) + 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)" + by (simp add: Let_def) + also have + "(x, #0) = (SOME (y, a). x = y + a ( * ) x0 & y : H)" + by (rule decomp_H0_H [RS sym], rule x0) (simp!)+ + also have "(let (y,a) = (SOME (y,a). x = y + a ( * ) x0 & y : H) in h y + a * xi) - = h0 x"; by (simp!); - finally; show "f x = h0 x"; .; - next; - from f_h0; show "F <= H0"; ..; - qed; + = h0 x" by (simp!) + finally show "f x = h0 x" . + next + from f_h0 show "F <= H0" .. + qed - show "ALL x:H0. h0 x <= p x"; - by (rule h0_norm_pres, rule x0) (assumption | simp!)+; - qed; - thus "graph H0 h0 : M"; by (simp!); - qed; - thus ?thesis; ..; - qed; + show "ALL x:H0. h0 x <= p x" + by (rule h0_norm_pres, rule x0) (assumption | simp!)+ + qed + thus "graph H0 h0 : M" by (simp!) + qed + thus ?thesis .. + qed txt {* We have shown that $h$ can still be extended to some $h_0$, in contradiction to the assumption that - $h$ is a maximal element. *}; + $h$ is a maximal element. *} - hence "EX x:M. g <= x & g ~= x"; - by (elim exE conjE, intro bexI conjI); - hence "~ (ALL x:M. g <= x --> g = x)"; by simp; - thus ?thesis; by contradiction; -qed; + hence "EX x:M. g <= x & g ~= x" + by (elim exE conjE, intro bexI conjI) + hence "~ (ALL x:M. g <= x --> g = x)" by simp + thus ?thesis by contradiction +qed -txt{* It follows $H = E$, and the thesis can be shown. *}; +txt{* It follows $H = E$, and the thesis can be shown. *} show "is_linearform E h & (ALL x:F. h x = f x) - & (ALL x:E. h x <= p x)"; -proof (intro conjI); - from eq; show "is_linearform E h"; by (simp!); - show "ALL x:F. h x = f x"; - proof (intro ballI, rule sym); - fix x; assume "x:F"; show "f x = h x "; ..; - qed; - from eq; show "ALL x:E. h x <= p x"; by (force!); -qed; + & (ALL x:E. h x <= p x)" +proof (intro conjI) + from eq show "is_linearform E h" by (simp!) + show "ALL x:F. h x = f x" + proof (intro ballI, rule sym) + fix x assume "x:F" show "f x = h x " .. + qed + from eq show "ALL x:E. h x <= p x" by (force!) +qed -qed; -qed; -qed; +qed +qed +qed *) -subsection {* Alternative formulation *}; +subsection {* Alternative formulation *} text {* The following alternative formulation of the Hahn-Banach Theorem\label{abs-HahnBanach} uses the fact that for a real linear form @@ -604,35 +604,35 @@ \forall x\in H.\ap |h\ap x|\leq p\ap x& {\rm and}\\ \forall x\in H.\ap h\ap x\leq p\ap x\\ \end{matharray} -*}; +*} theorem abs_HahnBanach: "[| is_vectorspace E; is_subspace F E; is_linearform F f; is_seminorm E p; ALL x:F. abs (f x) <= p x |] ==> EX g. is_linearform E g & (ALL x:F. g x = f x) - & (ALL x:E. abs (g x) <= p x)"; -proof -; + & (ALL x:E. abs (g x) <= p x)" +proof - assume "is_vectorspace E" "is_subspace F E" "is_seminorm E p" - "is_linearform F f" "ALL x:F. abs (f x) <= p x"; - have "ALL x:F. f x <= p x"; by (rule abs_ineq_iff [RS iffD1]); + "is_linearform F f" "ALL x:F. abs (f x) <= p x" + have "ALL x:F. f x <= p x" by (rule abs_ineq_iff [RS iffD1]) hence "EX g. is_linearform E g & (ALL x:F. g x = f x) - & (ALL x:E. g x <= p x)"; - by (simp! only: HahnBanach); - thus ?thesis; - proof (elim exE conjE); - fix g; assume "is_linearform E g" "ALL x:F. g x = f x" - "ALL x:E. g x <= p x"; - hence "ALL x:E. abs (g x) <= p x"; - by (simp! add: abs_ineq_iff [OF subspace_refl]); - thus ?thesis; by (intro exI conjI); - qed; -qed; + & (ALL x:E. g x <= p x)" + by (simp! only: HahnBanach) + thus ?thesis + proof (elim exE conjE) + fix g assume "is_linearform E g" "ALL x:F. g x = f x" + "ALL x:E. g x <= p x" + hence "ALL x:E. abs (g x) <= p x" + by (simp! add: abs_ineq_iff [OF subspace_refl]) + thus ?thesis by (intro exI conjI) + qed +qed -subsection {* The Hahn-Banach Theorem for normed spaces *}; +subsection {* The Hahn-Banach Theorem for normed spaces *} text {* Every continuous linear form $f$ on a subspace $F$ of a norm space $E$, can be extended to a continuous linear form $g$ on -$E$ such that $\fnorm{f} = \fnorm {g}$. *}; +$E$ such that $\fnorm{f} = \fnorm {g}$. *} theorem norm_HahnBanach: "[| is_normed_vectorspace E norm; is_subspace F E; @@ -640,119 +640,119 @@ ==> EX g. is_linearform E g & is_continuous E norm g & (ALL x:F. g x = f x) - & function_norm E norm g = function_norm F norm f"; -proof -; - assume e_norm: "is_normed_vectorspace E norm"; - assume f: "is_subspace F E" "is_linearform F f"; - assume f_cont: "is_continuous F norm f"; - have e: "is_vectorspace E"; ..; - with _; have f_norm: "is_normed_vectorspace F norm"; ..; + & function_norm E norm g = function_norm F norm f" +proof - + assume e_norm: "is_normed_vectorspace E norm" + assume f: "is_subspace F E" "is_linearform F f" + assume f_cont: "is_continuous F norm f" + have e: "is_vectorspace E" .. + with _ have f_norm: "is_normed_vectorspace F norm" .. txt{* We define a function $p$ on $E$ as follows: \begin{matharray}{l} p \: x = \fnorm f \cdot \norm x\\ \end{matharray} - *}; + *} - def p == "\\x. function_norm F norm f * norm x"; + def p == "\\x. function_norm F norm f * norm x" - txt{* $p$ is a seminorm on $E$: *}; + txt{* $p$ is a seminorm on $E$: *} - have q: "is_seminorm E p"; - proof; - fix x y a; assume "x:E" "y:E"; + have q: "is_seminorm E p" + proof + fix x y a assume "x:E" "y:E" - txt{* $p$ is positive definite: *}; + txt{* $p$ is positive definite: *} - show "#0 <= p x"; - proof (unfold p_def, rule real_le_mult_order1a); - from _ f_norm; show "#0 <= function_norm F norm f"; ..; - show "#0 <= norm x"; ..; - qed; + show "#0 <= p x" + proof (unfold p_def, rule real_le_mult_order1a) + from _ f_norm show "#0 <= function_norm F norm f" .. + show "#0 <= norm x" .. + qed - txt{* $p$ is absolutely homogenous: *}; + txt{* $p$ is absolutely homogenous: *} - show "p (a (*) x) = abs a * p x"; - proof -; - have "p (a (*) x) = function_norm F norm f * norm (a (*) x)"; - by (simp!); - also; have "norm (a (*) x) = abs a * norm x"; - by (rule normed_vs_norm_abs_homogenous); - also; have "function_norm F norm f * (abs a * norm x) - = abs a * (function_norm F norm f * norm x)"; - by (simp! only: real_mult_left_commute); - also; have "... = abs a * p x"; by (simp!); - finally; show ?thesis; .; - qed; + show "p (a (*) x) = abs a * p x" + proof - + have "p (a (*) x) = function_norm F norm f * norm (a (*) x)" + by (simp!) + also have "norm (a (*) x) = abs a * norm x" + by (rule normed_vs_norm_abs_homogenous) + also have "function_norm F norm f * (abs a * norm x) + = abs a * (function_norm F norm f * norm x)" + by (simp! only: real_mult_left_commute) + also have "... = abs a * p x" by (simp!) + finally show ?thesis . + qed - txt{* Furthermore, $p$ is subadditive: *}; + txt{* Furthermore, $p$ is subadditive: *} - show "p (x + y) <= p x + p y"; - proof -; - have "p (x + y) = function_norm F norm f * norm (x + y)"; - by (simp!); - also; - have "... <= function_norm F norm f * (norm x + norm y)"; - proof (rule real_mult_le_le_mono1a); - from _ f_norm; show "#0 <= function_norm F norm f"; ..; - show "norm (x + y) <= norm x + norm y"; ..; - qed; - also; have "... = function_norm F norm f * norm x - + function_norm F norm f * norm y"; - by (simp! only: real_add_mult_distrib2); - finally; show ?thesis; by (simp!); - qed; - qed; + show "p (x + y) <= p x + p y" + proof - + have "p (x + y) = function_norm F norm f * norm (x + y)" + by (simp!) + also + have "... <= function_norm F norm f * (norm x + norm y)" + proof (rule real_mult_le_le_mono1a) + from _ f_norm show "#0 <= function_norm F norm f" .. + show "norm (x + y) <= norm x + norm y" .. + qed + also have "... = function_norm F norm f * norm x + + function_norm F norm f * norm y" + by (simp! only: real_add_mult_distrib2) + finally show ?thesis by (simp!) + qed + qed - txt{* $f$ is bounded by $p$. *}; + txt{* $f$ is bounded by $p$. *} - have "ALL x:F. abs (f x) <= p x"; - proof; - fix x; assume "x:F"; - from f_norm; show "abs (f x) <= p x"; - by (simp! add: norm_fx_le_norm_f_norm_x); - qed; + have "ALL x:F. abs (f x) <= p x" + proof + fix x assume "x:F" + from f_norm show "abs (f x) <= p x" + by (simp! add: norm_fx_le_norm_f_norm_x) + qed txt{* Using the fact that $p$ is a seminorm and $f$ is bounded by $p$ we can apply the Hahn-Banach Theorem for real vector spaces. So $f$ can be extended in a norm-preserving way to some function - $g$ on the whole vector space $E$. *}; + $g$ on the whole vector space $E$. *} - with e f q; + with e f q have "EX g. is_linearform E g & (ALL x:F. g x = f x) - & (ALL x:E. abs (g x) <= p x)"; - by (simp! add: abs_HahnBanach); + & (ALL x:E. abs (g x) <= p x)" + by (simp! add: abs_HahnBanach) - thus ?thesis; - proof (elim exE conjE); - fix g; + thus ?thesis + proof (elim exE conjE) + fix g assume "is_linearform E g" and a: "ALL x:F. g x = f x" - and b: "ALL x:E. abs (g x) <= p x"; + and b: "ALL x:E. abs (g x) <= p x" show "EX g. is_linearform E g & is_continuous E norm g & (ALL x:F. g x = f x) - & function_norm E norm g = function_norm F norm f"; - proof (intro exI conjI); + & function_norm E norm g = function_norm F norm f" + proof (intro exI conjI) txt{* We furthermore have to show that - $g$ is also continuous: *}; + $g$ is also continuous: *} - show g_cont: "is_continuous E norm g"; - proof; - fix x; assume "x:E"; - from b [RS bspec, OF this]; - show "abs (g x) <= function_norm F norm f * norm x"; - by (unfold p_def); - qed; + show g_cont: "is_continuous E norm g" + proof + fix x assume "x:E" + from b [RS bspec, OF this] + show "abs (g x) <= function_norm F norm f * norm x" + by (unfold p_def) + qed txt {* To complete the proof, we show that - $\fnorm g = \fnorm f$. \label{order_antisym} *}; + $\fnorm g = \fnorm f$. \label{order_antisym} *} show "function_norm E norm g = function_norm F norm f" - (is "?L = ?R"); - proof (rule order_antisym); + (is "?L = ?R") + proof (rule order_antisym) txt{* First we show $\fnorm g \leq \fnorm f$. The function norm $\fnorm g$ is defined as the smallest $c\in\bbbR$ such that @@ -763,42 +763,42 @@ \begin{matharray}{l} \All {x\in E} {|g\ap x| \leq \fnorm f \cdot \norm x} \end{matharray} - *}; + *} - have "ALL x:E. abs (g x) <= function_norm F norm f * norm x"; - proof; - fix x; assume "x:E"; - show "abs (g x) <= function_norm F norm f * norm x"; - by (simp!); - qed; + have "ALL x:E. abs (g x) <= function_norm F norm f * norm x" + proof + fix x assume "x:E" + show "abs (g x) <= function_norm F norm f * norm x" + by (simp!) + qed - with _ g_cont; show "?L <= ?R"; - proof (rule fnorm_le_ub); - from f_cont f_norm; show "#0 <= function_norm F norm f"; ..; - qed; + with _ g_cont show "?L <= ?R" + proof (rule fnorm_le_ub) + from f_cont f_norm show "#0 <= function_norm F norm f" .. + qed txt{* The other direction is achieved by a similar - argument. *}; + argument. *} - have "ALL x:F. abs (f x) <= function_norm E norm g * norm x"; - proof; - fix x; assume "x : F"; - from a; have "g x = f x"; ..; - hence "abs (f x) = abs (g x)"; by simp; - also; from _ _ g_cont; - have "... <= function_norm E norm g * norm x"; - proof (rule norm_fx_le_norm_f_norm_x); - show "x:E"; ..; - qed; - finally; show "abs (f x) <= function_norm E norm g * norm x"; .; - qed; - thus "?R <= ?L"; - proof (rule fnorm_le_ub [OF f_norm f_cont]); - from g_cont; show "#0 <= function_norm E norm g"; ..; - qed; - qed; - qed; - qed; -qed; + have "ALL x:F. abs (f x) <= function_norm E norm g * norm x" + proof + fix x assume "x : F" + from a have "g x = f x" .. + hence "abs (f x) = abs (g x)" by simp + also from _ _ g_cont + have "... <= function_norm E norm g * norm x" + proof (rule norm_fx_le_norm_f_norm_x) + show "x:E" .. + qed + finally show "abs (f x) <= function_norm E norm g * norm x" . + qed + thus "?R <= ?L" + proof (rule fnorm_le_ub [OF f_norm f_cont]) + from g_cont show "#0 <= function_norm E norm g" .. + qed + qed + qed + qed +qed -end; +end \ No newline at end of file diff -r ea4dc7603f0b -r 371f023d3dbd src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy --- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Sun Jun 04 00:09:04 2000 +0200 +++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Sun Jun 04 19:39:29 2000 +0200 @@ -3,9 +3,9 @@ Author: Gertrud Bauer, TU Munich *) -header {* Extending non-maximal functions *}; +header {* Extending non-maximal functions *} -theory HahnBanachExtLemmas = FunctionNorm:; +theory HahnBanachExtLemmas = FunctionNorm: text{* In this section the following context is presumed. Let $E$ be a real vector space with a @@ -19,7 +19,7 @@ $h_0\ap x = h\ap y + a \cdot \xi$ for a certain $\xi$. Subsequently we show some properties of this extension $h_0$ of $h$. -*}; +*} text {* This lemma will be used to show the existence of a linear @@ -32,212 +32,212 @@ it suffices to show that \begin{matharray}{l} \All {u\in F}{\All {v\in F}{a\ap u \leq b \ap v}} -\end{matharray} *}; +\end{matharray} *} lemma ex_xi: "[| is_vectorspace F; !! u v. [| u:F; v:F |] ==> a u <= b v |] - ==> EX (xi::real). ALL y:F. a y <= xi & xi <= b y"; -proof -; - assume vs: "is_vectorspace F"; - assume r: "(!! u v. [| u:F; v:F |] ==> a u <= (b v::real))"; + ==> EX (xi::real). ALL 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))" 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. *}; + 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 "EX xi. isLub UNIV ?S xi"; - proof (rule reals_complete); + have "EX xi. isLub UNIV ?S xi" + proof (rule reals_complete) - txt {* The set $S$ is non-empty, since $a\ap\zero \in S$: *}; + txt {* The set $S$ is non-empty, since $a\ap\zero \in S$: *} - from vs; have "a 00 : ?S"; by force; - thus "EX X. X : ?S"; ..; + from vs have "a 00 : ?S" by force + thus "EX X. X : ?S" .. - txt {* $b\ap \zero$ is an upper bound of $S$: *}; + txt {* $b\ap \zero$ is an upper bound of $S$: *} - show "EX Y. isUb UNIV ?S Y"; - proof; - show "isUb UNIV ?S (b 00)"; - proof (intro isUbI setleI ballI); - show "b 00 : UNIV"; ..; - next; + show "EX Y. isUb UNIV ?S Y" + proof + show "isUb UNIV ?S (b 00)" + proof (intro isUbI setleI ballI) + show "b 00 : UNIV" .. + next - txt {* Every element $y\in S$ is less than $b\ap \zero$: *}; + txt {* Every element $y\in S$ is less than $b\ap \zero$: *} - fix y; assume y: "y : ?S"; - from y; have "EX u:F. y = a u"; by fast; - thus "y <= b 00"; - proof; - fix u; assume "u:F"; - assume "y = a u"; - also; have "a u <= b 00"; by (rule r) (simp!)+; - finally; show ?thesis; .; - qed; - qed; - qed; - qed; + fix y assume y: "y : ?S" + from y have "EX u:F. y = a u" by fast + thus "y <= b 00" + proof + fix u assume "u:F" + assume "y = a u" + also have "a u <= b 00" by (rule r) (simp!)+ + finally show ?thesis . + qed + qed + qed + qed - thus "EX xi. ALL y:F. a y <= xi & xi <= b y"; - proof (elim exE); - fix xi; assume "isLub UNIV ?S xi"; - show ?thesis; - proof (intro exI conjI ballI); + thus "EX xi. ALL y:F. a y <= xi & xi <= b y" + proof (elim exE) + fix xi assume "isLub UNIV ?S xi" + show ?thesis + proof (intro exI conjI ballI) - txt {* For all $y\in F$ holds $a\ap y \leq \xi$: *}; + txt {* For all $y\in F$ holds $a\ap y \leq \xi$: *} - fix y; assume y: "y:F"; - show "a y <= xi"; - proof (rule isUbD); - show "isUb UNIV ?S xi"; ..; - qed (force!); - next; + fix y assume y: "y:F" + show "a y <= xi" + proof (rule isUbD) + show "isUb UNIV ?S xi" .. + qed (force!) + next - txt {* For all $y\in F$ holds $\xi\leq b\ap y$: *}; + txt {* For all $y\in F$ holds $\xi\leq b\ap y$: *} - fix y; assume "y:F"; - show "xi <= b y"; - proof (intro isLub_le_isUb isUbI setleI); - show "b y : UNIV"; ..; - show "ALL ya : ?S. ya <= b y"; - proof; - fix au; assume au: "au : ?S "; - hence "EX u:F. au = a u"; by fast; - thus "au <= b y"; - proof; - fix u; assume "u:F"; assume "au = a u"; - also; have "... <= b y"; by (rule r); - finally; show ?thesis; .; - qed; - qed; - qed; - qed; - qed; -qed; + fix y assume "y:F" + show "xi <= b y" + proof (intro isLub_le_isUb isUbI setleI) + show "b y : UNIV" .. + show "ALL ya : ?S. ya <= b y" + proof + fix au assume au: "au : ?S " + hence "EX u:F. au = a u" by fast + thus "au <= b y" + proof + fix u assume "u:F" assume "au = a u" + also have "... <= b y" by (rule r) + finally show ?thesis . + qed + qed + qed + qed + 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$. *}; +is a linear extension of $h$ to $H_0$. *} lemma h0_lf: "[| h0 == (\x. let (y, a) = SOME (y, a). x = y + a (*) x0 & y:H in h y + a * xi); H0 == H + lin x0; is_subspace H E; is_linearform H h; x0 ~: H; x0 : E; x0 ~= 00; is_vectorspace E |] - ==> is_linearform H0 h0"; -proof -; + ==> is_linearform H0 h0" +proof - assume h0_def: "h0 == (\x. let (y, a) = SOME (y, a). x = y + a (*) x0 & y:H in h y + a * xi)" and H0_def: "H0 == H + lin x0" and vs: "is_subspace H E" "is_linearform H h" "x0 ~: H" - "x0 ~= 00" "x0 : E" "is_vectorspace E"; + "x0 ~= 00" "x0 : E" "is_vectorspace E" - have h0: "is_vectorspace H0"; - proof (unfold H0_def, rule vs_sum_vs); - show "is_subspace (lin x0) E"; ..; - qed; + have h0: "is_vectorspace H0" + proof (unfold H0_def, rule vs_sum_vs) + show "is_subspace (lin x0) E" .. + qed - show ?thesis; - proof; - fix x1 x2; assume x1: "x1 : H0" and x2: "x2 : H0"; + show ?thesis + proof + fix x1 x2 assume x1: "x1 : H0" and x2: "x2 : H0" txt{* We now have to show that $h_0$ is additive, i.~e.\ $h_0 \ap (x_1\plus x_2) = h_0\ap x_1 + h_0\ap x_2$ - for $x_1, x_2\in H$. *}; + for $x_1, x_2\in H$. *} - have x1x2: "x1 + x2 : H0"; - by (rule vs_add_closed, rule h0); - from x1; - have ex_x1: "EX y1 a1. x1 = y1 + a1 (*) x0 & y1 : H"; - by (unfold H0_def vs_sum_def lin_def) fast; - from x2; - have ex_x2: "EX y2 a2. x2 = y2 + a2 (*) x0 & y2 : H"; - by (unfold H0_def vs_sum_def lin_def) fast; - from x1x2; - have ex_x1x2: "EX y a. x1 + x2 = y + a (*) x0 & y : H"; - by (unfold H0_def vs_sum_def lin_def) fast; + have x1x2: "x1 + x2 : H0" + by (rule vs_add_closed, rule h0) + from x1 + have ex_x1: "EX y1 a1. x1 = y1 + a1 (*) x0 & y1 : H" + by (unfold H0_def vs_sum_def lin_def) fast + from x2 + have ex_x2: "EX y2 a2. x2 = y2 + a2 (*) x0 & y2 : H" + by (unfold H0_def vs_sum_def lin_def) fast + from x1x2 + have ex_x1x2: "EX y a. x1 + x2 = y + a (*) x0 & y : H" + by (unfold H0_def vs_sum_def lin_def) fast - from ex_x1 ex_x2 ex_x1x2; - show "h0 (x1 + x2) = h0 x1 + h0 x2"; - proof (elim exE conjE); - fix y1 y2 y a1 a2 a; + from ex_x1 ex_x2 ex_x1x2 + show "h0 (x1 + x2) = h0 x1 + h0 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"; + and y: "x1 + x2 = y + a (*) x0" and y': "y : H" - have ya: "y1 + y2 = y & a1 + a2 = a"; - proof (rule decomp_H0);; - txt_raw {* \label{decomp-H0-use} *};; - show "y1 + y2 + (a1 + a2) (*) x0 = y + a (*) x0"; - by (simp! add: vs_add_mult_distrib2 [of E]); - show "y1 + y2 : H"; ..; - qed; + have ya: "y1 + y2 = y & a1 + a2 = a" + proof (rule decomp_H0) + txt_raw {* \label{decomp-H0-use} *} + show "y1 + y2 + (a1 + a2) (*) x0 = y + a (*) x0" + by (simp! add: vs_add_mult_distrib2 [of E]) + show "y1 + y2 : H" .. + qed - have "h0 (x1 + x2) = h y + a * xi"; - by (rule h0_definite); - also; have "... = h (y1 + y2) + (a1 + a2) * xi"; - by (simp add: ya); - also; from vs y1' y2'; - have "... = h y1 + h y2 + a1 * xi + a2 * xi"; + have "h0 (x1 + x2) = h y + a * xi" + by (rule h0_definite) + also have "... = h (y1 + y2) + (a1 + a2) * xi" + by (simp add: ya) + also from vs y1' y2' + have "... = h y1 + h y2 + a1 * xi + a2 * xi" by (simp add: linearform_add [of H] - real_add_mult_distrib); - also; have "... = (h y1 + a1 * xi) + (h y2 + a2 * xi)"; - by simp; - also; have "h y1 + a1 * xi = h0 x1"; - by (rule h0_definite [RS sym]); - also; have "h y2 + a2 * xi = h0 x2"; - by (rule h0_definite [RS sym]); - finally; show ?thesis; .; - qed; + real_add_mult_distrib) + also have "... = (h y1 + a1 * xi) + (h y2 + a2 * xi)" + by simp + also have "h y1 + a1 * xi = h0 x1" + by (rule h0_definite [RS sym]) + also have "h y2 + a2 * xi = h0 x2" + by (rule h0_definite [RS sym]) + 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$ for $x\in H$ and $c\in \bbbR$. - *}; + *} - next; - fix c x1; assume x1: "x1 : H0"; - have ax1: "c (*) x1 : H0"; - by (rule vs_mult_closed, rule h0); - from x1; have ex_x: "!! x. x: H0 - ==> EX y a. x = y + a (*) x0 & y : H"; - by (unfold H0_def vs_sum_def lin_def) fast; + next + fix c x1 assume x1: "x1 : H0" + have ax1: "c (*) x1 : H0" + by (rule vs_mult_closed, rule h0) + from x1 have ex_x: "!! x. x: H0 + ==> EX y a. x = y + a (*) x0 & y : H" + by (unfold H0_def vs_sum_def lin_def) fast - from x1; have ex_x1: "EX y1 a1. x1 = y1 + a1 (*) x0 & y1 : H"; - by (unfold H0_def vs_sum_def lin_def) fast; - with ex_x [of "c (*) x1", OF ax1]; - show "h0 (c (*) x1) = c * (h0 x1)"; - proof (elim exE conjE); - fix y1 y a1 a; + from x1 have ex_x1: "EX y1 a1. x1 = y1 + a1 (*) x0 & y1 : H" + by (unfold H0_def vs_sum_def lin_def) fast + with ex_x [of "c (*) x1", OF ax1] + show "h0 (c (*) x1) = c * (h0 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"; + and y: "c (*) x1 = y + a (*) x0" and y': "y : H" - have ya: "c (*) y1 = y & c * a1 = a"; - proof (rule decomp_H0); - show "c (*) y1 + (c * a1) (*) x0 = y + a (*) x0"; - by (simp! add: add: vs_add_mult_distrib1); - show "c (*) y1 : H"; ..; - qed; + have ya: "c (*) y1 = y & c * a1 = a" + proof (rule decomp_H0) + show "c (*) y1 + (c * a1) (*) x0 = y + a (*) x0" + by (simp! add: add: vs_add_mult_distrib1) + show "c (*) y1 : H" .. + qed - have "h0 (c (*) x1) = h y + a * xi"; - by (rule h0_definite); - 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]); - also; from vs y1'; have "... = c * (h y1 + a1 * xi)"; - by (simp add: real_add_mult_distrib2 real_mult_assoc); - also; have "h y1 + a1 * xi = h0 x1"; - by (rule h0_definite [RS sym]); - finally; show ?thesis; .; - qed; - qed; -qed; + have "h0 (c (*) x1) = h y + a * xi" + by (rule h0_definite) + 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]) + also from vs y1' have "... = c * (h y1 + a1 * xi)" + by (simp add: real_add_mult_distrib2 real_mult_assoc) + also have "h y1 + a1 * xi = h0 x1" + by (rule h0_definite [RS sym]) + finally show ?thesis . + qed + qed +qed text{* \medskip The linear extension $h_0$ of $h$ -is bounded by the seminorm $p$. *}; +is bounded by the seminorm $p$. *} lemma h0_norm_pres: "[| h0 == (\x. let (y, a) = SOME (y, a). x = y + a (*) x0 & y:H @@ -245,105 +245,105 @@ H0 == H + lin x0; x0 ~: H; x0 : E; x0 ~= 00; is_vectorspace E; is_subspace H E; is_seminorm E p; is_linearform H h; ALL y:H. h y <= p y; ALL y:H. - p (y + x0) - h y <= xi & xi <= p (y + x0) - h y |] - ==> ALL x:H0. h0 x <= p x"; -proof; + ==> ALL x:H0. h0 x <= p x" +proof assume h0_def: "h0 == (\x. let (y, a) = SOME (y, a). x = y + a (*) x0 & y:H in (h y) + a * xi)" and H0_def: "H0 == H + lin x0" and vs: "x0 ~: H" "x0 : E" "x0 ~= 00" "is_vectorspace E" "is_subspace H E" "is_seminorm E p" "is_linearform H h" - and a: "ALL y:H. h y <= p y"; - presume a1: "ALL ya:H. - p (ya + x0) - h ya <= xi"; - presume a2: "ALL ya:H. xi <= p (ya + x0) - h ya"; - fix x; assume "x : H0"; + and a: "ALL y:H. h y <= p y" + presume a1: "ALL ya:H. - p (ya + x0) - h ya <= xi" + presume a2: "ALL ya:H. xi <= p (ya + x0) - h ya" + fix x assume "x : H0" have ex_x: - "!! x. x : H0 ==> EX y a. x = y + a (*) x0 & y : H"; - by (unfold H0_def vs_sum_def lin_def) fast; - have "EX y a. x = y + a (*) x0 & y : H"; - by (rule ex_x); - thus "h0 x <= p x"; - proof (elim exE conjE); - fix y a; assume x: "x = y + a (*) x0" and y: "y : H"; - have "h0 x = h y + a * xi"; - by (rule h0_definite); + "!! x. x : H0 ==> EX y a. x = y + a (*) x0 & y : H" + by (unfold H0_def vs_sum_def lin_def) fast + have "EX y a. x = y + a (*) x0 & y : H" + by (rule ex_x) + thus "h0 x <= p x" + proof (elim exE conjE) + fix y a assume x: "x = y + a (*) x0" and y: "y : H" + have "h0 x = h y + a * xi" + by (rule h0_definite) txt{* Now we show $h\ap y + a \cdot \xi\leq p\ap (y\plus a \mult x_0)$ - by case analysis on $a$. \label{linorder_linear_split}*}; + by case analysis on $a$. \label{linorder_linear_split}*} - also; have "... <= p (y + a (*) x0)"; - proof (rule linorder_linear_split); + also have "... <= p (y + a (*) x0)" + proof (rule linorder_linear_split) - assume z: "a = (#0::real)"; - with vs y a; show ?thesis; by simp; + assume z: "a = #0" + with vs y a show ?thesis by simp txt {* In the case $a < 0$, we use $a_1$ with $\idt{ya}$ - taken as $y/a$: *}; + taken as $y/a$: *} - next; - assume lz: "a < #0"; hence nz: "a ~= #0"; by simp; - from a1; - have "- p (rinv a (*) y + x0) - h (rinv a (*) y) <= xi"; - by (rule bspec) (simp!); + next + assume lz: "a < #0" hence nz: "a ~= #0" by simp + from a1 + 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. *}; + calculation. *} 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))"; - by (rule real_mult_diff_distrib); - 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)"; - by (simp add: vs_add_mult_distrib1); - 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"; .; + <= 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))" + by (rule real_mult_diff_distrib) + 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)" + by (simp add: vs_add_mult_distrib1) + 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" . - 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; + 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 txt {* In the case $a > 0$, we use $a_2$ with $\idt{ya}$ - taken as $y/a$: *}; + 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)"; - by (rule bspec) (simp!); + next + 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: *}; + calculation: *} - 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)"; - by (rule real_mult_diff_distrib2); - also; from gz vs 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)" + by (rule real_mult_diff_distrib2) + also from gz vs y 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)"; - by (simp add: vs_add_mult_distrib1); - 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"; .; + = p (a (*) (rinv a (*) y + x0))" + by (simp add: seminorm_abs_homogenous abs_eqI2) + 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" + by (simp add: linearform_mult [RS sym]) + finally have "a * xi <= 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; - also; from x; have "... = p x"; by simp; - finally; show ?thesis; .; - qed; -qed blast+; + 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 + also from x have "... = p x" by simp + finally show ?thesis . + qed +qed blast+ -end; \ No newline at end of file +end \ No newline at end of file diff -r ea4dc7603f0b -r 371f023d3dbd src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy --- a/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy Sun Jun 04 00:09:04 2000 +0200 +++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy Sun Jun 04 19:39:29 2000 +0200 @@ -3,10 +3,9 @@ Author: Gertrud Bauer, TU Munich *) -header {* The supremum w.r.t.~the function order *}; +header {* The supremum w.r.t.~the function order *} -theory HahnBanachSupLemmas = FunctionNorm + ZornLemma:; - +theory HahnBanachSupLemmas = FunctionNorm + ZornLemma: text{* This section contains some lemmas that will be used in the @@ -18,7 +17,7 @@ $\Union c = \idt{graph}\ap H\ap h$. We will show some properties about the limit function $h$, i.e.\ the supremum of the chain $c$. -*}; +*} (*** lemma some_H'h't: @@ -63,7 +62,7 @@ text{* Let $c$ be a chain of norm-preserving extensions of the function $f$ and let $\idt{graph}\ap H\ap h$ be the supremum of $c$. Every element in $H$ is member of -one of the elements of the chain. *}; +one of the elements of the chain. *} lemma some_H'h't: "[| M = norm_pres_extensions E p F f; c: chain M; @@ -71,78 +70,78 @@ ==> EX 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' - & (ALL x:H'. h' x <= p x)"; -proof -; + & (ALL 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 = Union c" "x:H"; + and u: "graph H h = Union c" "x:H" - have h: "(x, h x) : graph H h"; ..; - with u; have "(x, h x) : Union c"; by simp; - hence ex1: "EX 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); + have h: "(x, h x) : graph H h" .. + with u have "(x, h x) : Union c" by simp + hence ex1: "EX 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 "EX H' h'. graph H' h' = g & is_linearform H' h' & is_subspace H' E & is_subspace F H' & graph F f <= graph H' h' - & (ALL x:H'. h' x <= p x)"; - by (rule norm_pres_extension_D); - thus ?thesis; - proof (elim exE conjE); - fix H' h'; + & (ALL 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'" "ALL 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!); - qed; - qed; - qed; -qed; + "graph F f <= graph H' h'" "ALL 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!) + qed + qed + qed +qed text{* \medskip Let $c$ be a chain of norm-preserving extensions of the function $f$ and let $\idt{graph}\ap H\ap h$ be the supremum of $c$. Every element in the domain $H$ of the supremum function is member of the domain $H'$ of some function $h'$, such that $h$ extends $h'$. -*}; +*} lemma some_H'h': "[| M = norm_pres_extensions E p F f; c: chain M; graph H h = Union c; x:H |] ==> EX 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' & (ALL x:H'. h' x <= p x)"; -proof -; + & graph F f <= graph H' h' & (ALL 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 = Union c" "x:H"; + and u: "graph H h = Union c" "x:H" have "EX 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' - & (ALL 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" + & (ALL 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" "is_linearform H' h'" "is_subspace H' E" "is_subspace F H'" - "graph F f <= graph H' h'" "ALL x:H'. h' x <= p x"; - show ?thesis; - proof (intro exI conjI); - 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; -qed; + "graph F f <= graph H' h'" "ALL 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" + by (simp! only: chain_ball_Union_upper) + qed + qed +qed (*** lemma some_H'h': @@ -186,81 +185,81 @@ text{* \medskip Any two elements $x$ and $y$ in the domain $H$ of the supremum function $h$ are both in the domain $H'$ of some function -$h'$, such that $h$ extends $h'$. *}; +$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 = Union c; x:H; y:H |] ==> EX 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' & (ALL x:H'. h' x <= p x)"; -proof -; + & graph F f <= graph H' h' & (ALL x:H'. h' x <= p x)" +proof - assume "M = norm_pres_extensions E p F f" "c: chain M" - "graph H h = Union c" "x:H" "y:H"; + "graph H h = Union c" "x:H" "y:H" txt {* $x$ is in the domain $H'$ of some function $h'$, - such that $h$ extends $h'$. *}; + such that $h$ extends $h'$. *} have e1: "EX 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' - & (ALL x:H'. h' x <= p x)"; - by (rule some_H'h't); + & (ALL 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''$. *}; + such that $h$ extends $h''$. *} have e2: "EX 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'' - & (ALL x:H''. h'' x <= p x)"; - by (rule some_H'h't); + & (ALL 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" + from e1 e2 show ?thesis + proof (elim exE conjE) + 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'" "ALL x:H'. h' x <= p x"; + "graph F f <= graph H' h'" "ALL 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''" "ALL x:H''. h'' x <= p x"; + "graph F f <= graph H'' h''" "ALL 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}*}; + $x$ and $y$ are contained in the greater one. \label{cases1}*} have "graph H'' h'' <= graph H' h' | graph H' h' <= graph H'' h''" - (is "?case1 | ?case2"); - by (rule chainD); - thus ?thesis; - proof; - 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"; - 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"; - by (simp! only: chain_ball_Union_upper); - qed; - qed; - qed; -qed; + (is "?case1 | ?case2") + by (rule chainD) + thus ?thesis + proof + 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" + 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" + by (simp! only: chain_ball_Union_upper) + qed + qed + qed +qed (*** lemma some_H'h'2: @@ -337,303 +336,303 @@ ***) text{* \medskip The relation induced by the graph of the supremum -of a chain $c$ is definite, i.~e.~it is the graph of a function. *}; +of a chain $c$ is definite, i.~e.~it is the graph of a function. *} lemma sup_definite: "[| M == norm_pres_extensions E p F f; c : chain M; - (x, y) : Union c; (x, z) : Union c |] ==> z = y"; -proof -; + (x, y) : Union c; (x, z) : Union c |] ==> z = y" +proof - assume "c:chain M" "M == norm_pres_extensions E p F f" - "(x, y) : Union c" "(x, z) : Union c"; - thus ?thesis; - proof (elim UnionE chainE2); + "(x, y) : Union c" "(x, z) : Union c" + thus ?thesis + proof (elim UnionE chainE2) txt{* Since both $(x, y) \in \Union c$ and $(x, z) \in \Union c$ they are members of some graphs $G_1$ and $G_2$, resp., such that - both $G_1$ and $G_2$ are members of $c$.*}; + 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"; + fix G1 G2 assume + "(x, y) : G1" "G1 : c" "(x, z) : G2" "G2 : c" "c <= M" - have "G1 : M"; ..; - hence e1: "EX H1 h1. graph H1 h1 = G1"; - by (force! dest: norm_pres_extension_D); - have "G2 : M"; ..; - hence e2: "EX H2 h2. graph H2 h2 = G2"; - by (force! dest: norm_pres_extension_D); - from e1 e2; show ?thesis; - proof (elim exE); - fix H1 h1 H2 h2; - assume "graph H1 h1 = G1" "graph H2 h2 = G2"; + have "G1 : M" .. + hence e1: "EX H1 h1. graph H1 h1 = G1" + by (force! dest: norm_pres_extension_D) + have "G2 : M" .. + hence e2: "EX H2 h2. graph H2 h2 = G2" + by (force! dest: norm_pres_extension_D) + from e1 e2 show ?thesis + proof (elim exE) + fix H1 h1 H2 h2 + assume "graph H1 h1 = G1" "graph H2 h2 = G2" txt{* $G_1$ is contained in $G_2$ or vice versa, - since both $G_1$ and $G_2$ are members of $c$. \label{cases2}*}; + since both $G_1$ and $G_2$ are members of $c$. \label{cases2}*} - have "G1 <= G2 | G2 <= G1" (is "?case1 | ?case2"); ..; - thus ?thesis; - proof; - assume ?case1; - have "(x, y) : graph H2 h2"; by (force!); - hence "y = h2 x"; ..; - 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!); - hence "y = h1 x"; ..; - also; have "(x, z) : graph H1 h1"; by (force!); - hence "z = h1 x"; ..; - finally; show ?thesis; .; - qed; - qed; - qed; -qed; + have "G1 <= G2 | G2 <= G1" (is "?case1 | ?case2") .. + thus ?thesis + proof + assume ?case1 + have "(x, y) : graph H2 h2" by (force!) + hence "y = h2 x" .. + 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!) + hence "y = h1 x" .. + also have "(x, z) : graph H1 h1" by (force!) + hence "z = h1 x" .. + finally show ?thesis . + qed + qed + qed +qed text{* \medskip The limit function $h$ is linear. Every element $x$ in the domain of $h$ is in the domain of a function $h'$ in the chain of norm preserving extensions. Furthermore, $h$ is an extension of $h'$ so the function values of $x$ are identical for $h'$ and $h$. Finally, the -function $h'$ is linear by construction of $M$. *}; +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 = Union c |] ==> is_linearform H h"; -proof -; + graph H h = Union c |] ==> is_linearform H h" +proof - assume "M = norm_pres_extensions E p F f" "c: chain M" - "graph H h = Union c"; + "graph H h = Union c" - show "is_linearform H h"; - proof; - fix x y; assume "x : H" "y : H"; + show "is_linearform H h" + proof + fix x y assume "x : H" "y : H" have "EX 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' - & (ALL x:H'. h' x <= p x)"; - by (rule some_H'h'2); + & (ALL x:H'. h' x <= p x)" + by (rule some_H'h'2) - txt {* We have to show that $h$ is additive. *}; + 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'" + 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" - 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'"; ..; - with b; have "h' (x + y) = h (x + y)"; ..; - finally; show ?thesis; .; - qed; - next; - fix a x; assume "x : 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'" .. + with b have "h' (x + y) = h (x + y)" .. + finally show ?thesis . + qed + next + fix a x assume "x : H" have "EX 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' - & (ALL x:H'. h' x <= p x)"; - by (rule some_H'h'); + & (ALL x:H'. h' x <= p x)" + by (rule some_H'h') - txt{* We have to show that $h$ is multiplicative. *}; + txt{* We have to show that $h$ is multiplicative. *} - thus "h (a (*) x) = a * h x"; - proof (elim exE conjE); - fix H' h'; assume "x:H'" + 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" - and "is_linearform H' h'" "is_subspace H' E"; - 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)"; ..; - finally; show ?thesis; .; - qed; - qed; -qed; + and "is_linearform H' h'" "is_subspace H' E" + 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)" .. + finally show ?thesis . + qed + qed +qed text{* \medskip The limit of a non-empty chain of norm preserving extensions of $f$ is an extension of $f$, since every element of the chain is an extension of $f$ and the supremum is an extension -for every element of the chain.*}; +for every element of the chain.*} lemma sup_ext: "[| M = norm_pres_extensions E p F f; c: chain M; EX x. x:c; - graph H h = Union c |] ==> graph F f <= graph H h"; -proof -; + graph H h = Union c |] ==> graph F f <= graph H h" +proof - assume "M = norm_pres_extensions E p F f" "c: chain M" - "graph H h = Union c"; - assume "EX 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!); + "graph H h = Union c" + assume "EX 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!) hence "EX G g. graph G g = x & is_linearform G g & is_subspace G E & is_subspace F G & graph F f <= graph G g - & (ALL x:G. g x <= p x)"; - by (simp! add: norm_pres_extension_D); + & (ALL 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"; - also; assume "graph G g = x"; - also; have "... : c"; .; - hence "x <= Union c"; by fast; - also; have [RS sym]: "graph H h = Union c"; .; - finally; show ?thesis; .; - qed; - qed; -qed; + thus ?thesis + proof (elim exE conjE) + fix G g assume "graph F f <= graph G g" + also assume "graph G g = x" + also have "... : c" . + hence "x <= Union c" by fast + also have [RS sym]: "graph H h = Union c" . + finally show ?thesis . + qed + qed +qed text{* \medskip The domain $H$ of the limit function is a superspace of $F$, since $F$ is a subset of $H$. The existence of the $\zero$ element in $F$ and the closure properties follow from the fact that $F$ is a -vector space. *}; +vector space. *} lemma sup_supF: "[| M = norm_pres_extensions E p F f; c: chain M; EX x. x:c; graph H h = Union c; is_subspace F E; is_vectorspace E |] - ==> is_subspace F H"; -proof -; + ==> is_subspace F H" +proof - assume "M = norm_pres_extensions E p F f" "c: chain M" "EX x. x:c" - "graph H h = Union c" "is_subspace F E" "is_vectorspace E"; + "graph H h = Union c" "is_subspace F E" "is_vectorspace E" - show ?thesis; - proof; - show "00 : F"; ..; - show "F <= H"; - proof (rule graph_extD2); - show "graph F f <= graph H h"; - by (rule sup_ext); - qed; - show "ALL x:F. ALL y:F. x + y : F"; - proof (intro ballI); - fix x y; assume "x:F" "y:F"; - show "x + y : F"; by (simp!); - qed; - show "ALL x:F. ALL a. a (*) x : F"; - proof (intro ballI allI); - fix x a; assume "x:F"; - show "a (*) x : F"; by (simp!); - qed; - qed; -qed; + show ?thesis + proof + show "00 : F" .. + show "F <= H" + proof (rule graph_extD2) + show "graph F f <= graph H h" + by (rule sup_ext) + qed + show "ALL x:F. ALL y:F. x + y : F" + proof (intro ballI) + fix x y assume "x:F" "y:F" + show "x + y : F" by (simp!) + qed + show "ALL x:F. ALL a. a (*) x : F" + proof (intro ballI allI) + fix x a assume "x:F" + show "a (*) x : F" by (simp!) + qed + qed +qed text{* \medskip The domain $H$ of the limit function is a subspace -of $E$. *}; +of $E$. *} lemma sup_subE: "[| M = norm_pres_extensions E p F f; c: chain M; EX x. x:c; graph H h = Union c; is_subspace F E; is_vectorspace E |] - ==> is_subspace H E"; -proof -; + ==> is_subspace H E" +proof - assume "M = norm_pres_extensions E p F f" "c: chain M" "EX x. x:c" - "graph H h = Union c" "is_subspace F E" "is_vectorspace E"; - show ?thesis; - proof; + "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$: *}; + of $H$: *} - have "00 : F"; ..; - also; have "is_subspace F H"; by (rule sup_supF); - hence "F <= H"; ..; - finally; show "00 : H"; .; + have "00 : F" .. + also have "is_subspace F H" by (rule sup_supF) + hence "F <= H" .. + finally show "00 : H" . - txt{* $H$ is a subset of $E$: *}; + txt{* $H$ is a subset of $E$: *} - show "H <= E"; - proof; - fix x; assume "x:H"; + show "H <= E" + proof + fix x assume "x:H" have "EX 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' - & (ALL x:H'. h' x <= p x)"; - by (rule some_H'h'); - thus "x:E"; - proof (elim exE conjE); - fix H' h'; assume "x:H'" "is_subspace H' E"; - have "H' <= E"; ..; - thus "x:E"; ..; - qed; - qed; + & (ALL x:H'. h' x <= p x)" + by (rule some_H'h') + thus "x:E" + proof (elim exE conjE) + fix H' h' assume "x:H'" "is_subspace H' E" + have "H' <= E" .. + thus "x:E" .. + qed + qed - txt{* $H$ is closed under addition: *}; + txt{* $H$ is closed under addition: *} - show "ALL x:H. ALL y:H. x + y : H"; - proof (intro ballI); - fix x y; assume "x:H" "y:H"; + show "ALL x:H. ALL y:H. x + y : H" + proof (intro ballI) + fix x y assume "x:H" "y:H" have "EX 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' - & (ALL x:H'. h' x <= p x)"; - by (rule some_H'h'2); - thus "x + y : H"; - proof (elim exE conjE); - fix H' h'; + & (ALL x:H'. h' x <= p x)" + by (rule some_H'h'2) + 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"; ..; - finally; show ?thesis; .; - qed; - qed; + "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: *}; + txt{* $H$ is closed under scalar multiplication: *} - show "ALL x:H. ALL a. a (*) x : H"; - proof (intro ballI allI); - fix x a; assume "x:H"; + show "ALL x:H. ALL a. a (*) x : H" + proof (intro ballI allI) + fix x a assume "x:H" have "EX 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' - & (ALL x:H'. h' x <= p x)"; - by (rule some_H'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"; ..; - finally; show ?thesis; .; - qed; - qed; - qed; -qed; + & (ALL x:H'. h' x <= p x)" + by (rule some_H'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" .. + finally show ?thesis . + qed + qed + qed +qed text {* \medskip The limit function is bounded by the norm $p$ as well, since all elements in the chain are bounded by $p$. -*}; +*} lemma sup_norm_pres: "[| M = norm_pres_extensions E p F f; c: chain M; - graph H h = Union c |] ==> ALL x:H. h x <= p x"; -proof; + graph H h = Union c |] ==> ALL x:H. h x <= p x" +proof assume "M = norm_pres_extensions E p F f" "c: chain M" - "graph H h = Union c"; - fix x; assume "x:H"; + "graph H h = Union c" + fix x assume "x:H" have "EX 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' & (ALL x:H'. h' x <= p x)"; - by (rule some_H'h'); - thus "h x <= p x"; - proof (elim exE conjE); - fix H' h'; + & graph F f <= graph H' h' & (ALL x:H'. h' x <= p x)" + by (rule some_H'h') + thus "h x <= p x" + proof (elim exE conjE) + fix H' h' assume "x: H'" "graph H' h' <= graph H h" - and a: "ALL x: H'. h' x <= p x"; - have [RS sym]: "h' x = h x"; ..; - also; from a; have "h' x <= p x "; ..; - finally; show ?thesis; .; - qed; -qed; + and a: "ALL x: H'. h' x <= p x" + have [RS sym]: "h' x = h x" .. + also from a have "h' x <= p x " .. + finally show ?thesis . + qed +qed text{* \medskip The following lemma is a property of linear forms on @@ -644,47 +643,47 @@ \forall x\in H.\ap |h\ap x|\leq p\ap x& {\rm and}\\ \forall x\in H.\ap h\ap x\leq p\ap x\\ \end{matharray} -*}; +*} lemma abs_ineq_iff: "[| is_subspace H E; is_vectorspace E; is_seminorm E p; is_linearform H h |] ==> (ALL x:H. abs (h x) <= p x) = (ALL x:H. h x <= p x)" - (concl is "?L = ?R"); -proof -; + (concl is "?L = ?R") +proof - assume "is_subspace H E" "is_vectorspace E" "is_seminorm E p" - "is_linearform H h"; - have h: "is_vectorspace H"; ..; - show ?thesis; - proof; - assume l: ?L; - show ?R; - proof; - fix x; assume x: "x:H"; - have "h x <= abs (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 |] ==> abs b <= a"; - by arith; - show "- p x <= h x"; - proof (rule real_minus_le); - from h; have "- h x = h (- x)"; - by (rule linearform_neg [RS sym]); - 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"; .; - qed; - from r; show "h x <= p x"; ..; - qed; - qed; -qed; + "is_linearform H h" + have h: "is_vectorspace H" .. + show ?thesis + proof + assume l: ?L + show ?R + proof + fix x assume x: "x:H" + have "h x <= abs (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 |] ==> abs b <= a" + by arith + show "- p x <= h x" + proof (rule real_minus_le) + from h have "- h x = h (- x)" + by (rule linearform_neg [RS sym]) + 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" . + qed + from r show "h x <= p x" .. + qed + qed +qed -end; \ No newline at end of file +end \ No newline at end of file diff -r ea4dc7603f0b -r 371f023d3dbd src/HOL/Real/HahnBanach/Linearform.thy --- a/src/HOL/Real/HahnBanach/Linearform.thy Sun Jun 04 00:09:04 2000 +0200 +++ b/src/HOL/Real/HahnBanach/Linearform.thy Sun Jun 04 19:39:29 2000 +0200 @@ -3,67 +3,67 @@ Author: Gertrud Bauer, TU Munich *) -header {* Linearforms *}; +header {* Linearforms *} -theory Linearform = VectorSpace:; +theory Linearform = VectorSpace: text{* A \emph{linear form} is a function on a vector -space into the reals that is additive and multiplicative. *}; +space into the reals that is additive and multiplicative. *} constdefs is_linearform :: "['a::{minus, plus} set, 'a => real] => bool" "is_linearform V f == (ALL x: V. ALL y: V. f (x + y) = f x + f y) & - (ALL x: V. ALL a. f (a (*) x) = a * (f x))"; + (ALL x: V. ALL a. f (a (*) x) = a * (f x))" lemma is_linearformI [intro]: "[| !! x y. [| x : V; y : V |] ==> f (x + y) = f x + f y; !! x c. x : V ==> f (c (*) x) = c * f x |] - ==> is_linearform V f"; - by (unfold is_linearform_def) force; + ==> is_linearform V f" + by (unfold is_linearform_def) force lemma linearform_add [intro??]: - "[| is_linearform V f; x:V; y:V |] ==> f (x + y) = f x + f y"; - by (unfold is_linearform_def) fast; + "[| is_linearform V f; x:V; y:V |] ==> f (x + y) = f x + f y" + by (unfold is_linearform_def) fast lemma linearform_mult [intro??]: - "[| is_linearform V f; x:V |] ==> f (a (*) x) = a * (f x)"; - by (unfold is_linearform_def) fast; + "[| is_linearform V f; x:V |] ==> f (a (*) x) = a * (f x)" + by (unfold is_linearform_def) fast lemma linearform_neg [intro??]: "[| is_vectorspace V; is_linearform V f; x:V|] - ==> f (- x) = - f x"; -proof -; - assume "is_linearform V f" "is_vectorspace V" "x:V"; - have "f (- x) = f ((- (#1::real)) (*) x)"; by (simp! add: negate_eq1); - also; have "... = (- #1) * (f x)"; by (rule linearform_mult); - also; have "... = - (f x)"; by (simp!); - finally; show ?thesis; .; -qed; + ==> f (- x) = - f x" +proof - + assume "is_linearform V f" "is_vectorspace V" "x:V" + have "f (- x) = f ((- #1) (*) x)" by (simp! add: negate_eq1) + also have "... = (- #1) * (f x)" by (rule linearform_mult) + also have "... = - (f x)" by (simp!) + finally show ?thesis . +qed lemma linearform_diff [intro??]: "[| is_vectorspace V; is_linearform V f; x:V; y:V |] - ==> f (x - y) = f x - f y"; -proof -; - assume "is_vectorspace V" "is_linearform V f" "x:V" "y:V"; - have "f (x - y) = f (x + - y)"; by (simp! only: diff_eq1); - also; have "... = f x + f (- y)"; - by (rule linearform_add) (simp!)+; - also; have "f (- y) = - f y"; by (rule linearform_neg); - finally; show "f (x - y) = f x - f y"; by (simp!); -qed; + ==> f (x - y) = f x - f y" +proof - + assume "is_vectorspace V" "is_linearform V f" "x:V" "y:V" + have "f (x - y) = f (x + - y)" by (simp! only: diff_eq1) + also have "... = f x + f (- y)" + by (rule linearform_add) (simp!)+ + also have "f (- y) = - f y" by (rule linearform_neg) + finally show "f (x - y) = f x - f y" by (simp!) +qed -text{* Every linear form yields $0$ for the $\zero$ vector.*}; +text{* Every linear form yields $0$ for the $\zero$ vector.*} lemma linearform_zero [intro??, simp]: - "[| is_vectorspace V; is_linearform V f |] ==> f 00 = (#0::real)"; -proof -; - assume "is_vectorspace V" "is_linearform V f"; - have "f 00 = f (00 - 00)"; by (simp!); - also; have "... = f 00 - f 00"; - by (rule linearform_diff) (simp!)+; - also; have "... = (#0::real)"; by simp; - finally; show "f 00 = (#0::real)"; .; -qed; + "[| is_vectorspace V; is_linearform V f |] ==> f 00 = #0" +proof - + assume "is_vectorspace V" "is_linearform V f" + have "f 00 = f (00 - 00)" by (simp!) + also have "... = f 00 - f 00" + by (rule linearform_diff) (simp!)+ + also have "... = #0" by simp + finally show "f 00 = #0" . +qed -end; \ No newline at end of file +end \ No newline at end of file diff -r ea4dc7603f0b -r 371f023d3dbd src/HOL/Real/HahnBanach/NormedSpace.thy --- a/src/HOL/Real/HahnBanach/NormedSpace.thy Sun Jun 04 00:09:04 2000 +0200 +++ b/src/HOL/Real/HahnBanach/NormedSpace.thy Sun Jun 04 19:39:29 2000 +0200 @@ -3,184 +3,183 @@ Author: Gertrud Bauer, TU Munich *) -header {* Normed vector spaces *}; +header {* Normed vector spaces *} -theory NormedSpace = Subspace:; +theory NormedSpace = Subspace: - -subsection {* Quasinorms *}; +subsection {* Quasinorms *} text{* A \emph{seminorm} $\norm{\cdot}$ is a function on a real vector space into the reals that has the following properties: It is positive -definite, absolute homogenous and subadditive. *}; +definite, absolute homogenous and subadditive. *} constdefs is_seminorm :: "['a::{plus, minus} set, 'a => real] => bool" "is_seminorm V norm == ALL x: V. ALL y:V. ALL a. - (#0::real) <= norm x + #0 <= norm x & norm (a (*) x) = (abs a) * (norm x) - & norm (x + y) <= norm x + norm y"; + & norm (x + y) <= norm x + norm y" lemma is_seminormI [intro]: - "[| !! x y a. [| x:V; y:V|] ==> (#0::real) <= norm x; + "[| !! x y a. [| x:V; y:V|] ==> #0 <= norm x; !! x a. x:V ==> norm (a (*) x) = (abs a) * (norm x); !! x y. [|x:V; y:V |] ==> norm (x + y) <= norm x + norm y |] - ==> is_seminorm V norm"; - by (unfold is_seminorm_def, force); + ==> is_seminorm V norm" + by (unfold is_seminorm_def, force) lemma seminorm_ge_zero [intro??]: - "[| is_seminorm V norm; x:V |] ==> (#0::real) <= norm x"; - by (unfold is_seminorm_def, force); + "[| is_seminorm V norm; x:V |] ==> #0 <= norm x" + by (unfold is_seminorm_def, force) lemma seminorm_abs_homogenous: "[| is_seminorm V norm; x:V |] - ==> norm (a (*) x) = (abs a) * (norm x)"; - by (unfold is_seminorm_def, force); + ==> norm (a (*) x) = (abs a) * (norm x)" + by (unfold is_seminorm_def, force) lemma seminorm_subadditive: "[| is_seminorm V norm; x:V; y:V |] - ==> norm (x + y) <= norm x + norm y"; - by (unfold is_seminorm_def, force); + ==> norm (x + y) <= norm x + norm y" + by (unfold is_seminorm_def, force) lemma seminorm_diff_subadditive: "[| is_seminorm V norm; x:V; y:V; is_vectorspace V |] - ==> norm (x - y) <= norm x + norm y"; -proof -; - assume "is_seminorm V norm" "x:V" "y:V" "is_vectorspace V"; - have "norm (x - y) = norm (x + - (#1::real) (*) y)"; - by (simp! add: diff_eq2 negate_eq2a); - also; have "... <= norm x + norm (- (#1::real) (*) y)"; - by (simp! add: seminorm_subadditive); - also; have "norm (- (#1::real) (*) y) = abs (- (#1::real)) * norm y"; - by (rule seminorm_abs_homogenous); - also; have "abs (- (#1::real)) = (#1::real)"; by (rule abs_minus_one); - finally; show "norm (x - y) <= norm x + norm y"; by simp; -qed; + ==> norm (x - y) <= norm x + norm y" +proof - + assume "is_seminorm V norm" "x:V" "y:V" "is_vectorspace V" + have "norm (x - y) = norm (x + - #1 (*) y)" + by (simp! add: diff_eq2 negate_eq2a) + also have "... <= norm x + norm (- #1 (*) y)" + by (simp! add: seminorm_subadditive) + also have "norm (- #1 (*) y) = abs (- #1) * norm y" + by (rule seminorm_abs_homogenous) + also have "abs (- #1) = (#1::real)" by (rule abs_minus_one) + finally show "norm (x - y) <= norm x + norm y" by simp +qed lemma seminorm_minus: "[| is_seminorm V norm; x:V; is_vectorspace V |] - ==> norm (- x) = norm x"; -proof -; - assume "is_seminorm V norm" "x:V" "is_vectorspace V"; - have "norm (- x) = norm (- (#1::real) (*) x)"; by (simp! only: negate_eq1); - also; have "... = abs (- (#1::real)) * norm x"; - by (rule seminorm_abs_homogenous); - also; have "abs (- (#1::real)) = (#1::real)"; by (rule abs_minus_one); - finally; show "norm (- x) = norm x"; by simp; -qed; + ==> norm (- x) = norm x" +proof - + assume "is_seminorm V norm" "x:V" "is_vectorspace V" + have "norm (- x) = norm (- #1 (*) x)" by (simp! only: negate_eq1) + also have "... = abs (- #1) * norm x" + by (rule seminorm_abs_homogenous) + also have "abs (- #1) = (#1::real)" by (rule abs_minus_one) + finally show "norm (- x) = norm x" by simp +qed -subsection {* Norms *}; +subsection {* Norms *} text{* A \emph{norm} $\norm{\cdot}$ is a seminorm that maps only the -$\zero$ vector to $0$. *}; +$\zero$ vector to $0$. *} constdefs is_norm :: "['a::{minus, plus} set, 'a => real] => bool" "is_norm V norm == ALL x: V. is_seminorm V norm - & (norm x = (#0::real)) = (x = 00)"; + & (norm x = #0) = (x = 00)" lemma is_normI [intro]: - "ALL x: V. is_seminorm V norm & (norm x = (#0::real)) = (x = 00) - ==> is_norm V norm"; by (simp only: is_norm_def); + "ALL x: V. is_seminorm V norm & (norm x = #0) = (x = 00) + ==> is_norm V norm" by (simp only: is_norm_def) lemma norm_is_seminorm [intro??]: - "[| is_norm V norm; x:V |] ==> is_seminorm V norm"; - by (unfold is_norm_def, force); + "[| is_norm V norm; x:V |] ==> is_seminorm V norm" + by (unfold is_norm_def, force) lemma norm_zero_iff: - "[| is_norm V norm; x:V |] ==> (norm x = (#0::real)) = (x = 00)"; - by (unfold is_norm_def, force); + "[| is_norm V norm; x:V |] ==> (norm x = #0) = (x = 00)" + by (unfold is_norm_def, force) lemma norm_ge_zero [intro??]: - "[|is_norm V norm; x:V |] ==> (#0::real) <= norm x"; - by (unfold is_norm_def is_seminorm_def, force); + "[|is_norm V norm; x:V |] ==> #0 <= norm x" + by (unfold is_norm_def is_seminorm_def, force) -subsection {* Normed vector spaces *}; +subsection {* Normed vector spaces *} text{* A vector space together with a norm is called -a \emph{normed space}. *}; +a \emph{normed space}. *} constdefs is_normed_vectorspace :: "['a::{plus, minus} set, 'a => real] => bool" "is_normed_vectorspace V norm == is_vectorspace V & - is_norm V norm"; + is_norm V norm" lemma normed_vsI [intro]: "[| is_vectorspace V; is_norm V norm |] - ==> is_normed_vectorspace V norm"; - by (unfold is_normed_vectorspace_def) blast; + ==> is_normed_vectorspace V norm" + by (unfold is_normed_vectorspace_def) blast lemma normed_vs_vs [intro??]: - "is_normed_vectorspace V norm ==> is_vectorspace V"; - by (unfold is_normed_vectorspace_def) force; + "is_normed_vectorspace V norm ==> is_vectorspace V" + by (unfold is_normed_vectorspace_def) force lemma normed_vs_norm [intro??]: - "is_normed_vectorspace V norm ==> is_norm V norm"; - by (unfold is_normed_vectorspace_def, elim conjE); + "is_normed_vectorspace V norm ==> is_norm V norm" + by (unfold is_normed_vectorspace_def, elim conjE) lemma normed_vs_norm_ge_zero [intro??]: - "[| is_normed_vectorspace V norm; x:V |] ==> (#0::real) <= norm x"; - by (unfold is_normed_vectorspace_def, rule, elim conjE); + "[| is_normed_vectorspace V norm; x:V |] ==> #0 <= norm x" + by (unfold is_normed_vectorspace_def, rule, elim conjE) lemma normed_vs_norm_gt_zero [intro??]: - "[| is_normed_vectorspace V norm; x:V; x ~= 00 |] ==> (#0::real) < norm x"; -proof (unfold is_normed_vectorspace_def, elim conjE); - assume "x : V" "x ~= 00" "is_vectorspace V" "is_norm V norm"; - have "(#0::real) <= norm x"; ..; - also; have "(#0::real) ~= norm x"; - proof; - presume "norm x = (#0::real)"; - also; have "?this = (x = 00)"; by (rule norm_zero_iff); - finally; have "x = 00"; .; - thus "False"; by contradiction; - qed (rule sym); - finally; show "(#0::real) < norm x"; .; -qed; + "[| is_normed_vectorspace V norm; x:V; x ~= 00 |] ==> #0 < norm x" +proof (unfold is_normed_vectorspace_def, elim conjE) + assume "x : V" "x ~= 00" "is_vectorspace V" "is_norm V norm" + have "#0 <= norm x" .. + also have "#0 ~= norm x" + proof + presume "norm x = #0" + also have "?this = (x = 00)" by (rule norm_zero_iff) + finally have "x = 00" . + thus "False" by contradiction + qed (rule sym) + finally show "#0 < norm x" . +qed lemma normed_vs_norm_abs_homogenous [intro??]: "[| is_normed_vectorspace V norm; x:V |] - ==> norm (a (*) x) = (abs a) * (norm x)"; + ==> norm (a (*) x) = (abs a) * (norm x)" by (rule seminorm_abs_homogenous, rule norm_is_seminorm, - rule normed_vs_norm); + rule normed_vs_norm) lemma normed_vs_norm_subadditive [intro??]: "[| is_normed_vectorspace V norm; x:V; y:V |] - ==> norm (x + y) <= norm x + norm y"; + ==> norm (x + y) <= norm x + norm y" by (rule seminorm_subadditive, rule norm_is_seminorm, - rule normed_vs_norm); + rule normed_vs_norm) text{* Any subspace of a normed vector space is again a -normed vectorspace.*}; +normed vectorspace.*} lemma subspace_normed_vs [intro??]: "[| is_subspace F E; is_vectorspace E; - is_normed_vectorspace E norm |] ==> is_normed_vectorspace F norm"; -proof (rule normed_vsI); + is_normed_vectorspace E norm |] ==> is_normed_vectorspace F norm" +proof (rule normed_vsI) assume "is_subspace F E" "is_vectorspace E" - "is_normed_vectorspace E norm"; - show "is_vectorspace F"; ..; - show "is_norm F norm"; - proof (intro is_normI ballI conjI); - show "is_seminorm F norm"; - proof; - fix x y a; presume "x : E"; - show "(#0::real) <= norm x"; ..; - show "norm (a (*) x) = abs a * norm x"; ..; - presume "y : E"; - show "norm (x + y) <= norm x + norm y"; ..; - qed (simp!)+; + "is_normed_vectorspace E norm" + show "is_vectorspace F" .. + show "is_norm F norm" + proof (intro is_normI ballI conjI) + show "is_seminorm F norm" + proof + fix x y a presume "x : E" + show "#0 <= norm x" .. + show "norm (a (*) x) = abs a * norm x" .. + presume "y : E" + show "norm (x + y) <= norm x + norm y" .. + qed (simp!)+ - fix x; assume "x : F"; - show "(norm x = (#0::real)) = (x = 00)"; - proof (rule norm_zero_iff); - show "is_norm E norm"; ..; - qed (simp!); - qed; -qed; + fix x assume "x : F" + show "(norm x = #0) = (x = 00)" + proof (rule norm_zero_iff) + show "is_norm E norm" .. + qed (simp!) + qed +qed -end; \ No newline at end of file +end \ No newline at end of file diff -r ea4dc7603f0b -r 371f023d3dbd src/HOL/Real/HahnBanach/Subspace.thy --- a/src/HOL/Real/HahnBanach/Subspace.thy Sun Jun 04 00:09:04 2000 +0200 +++ b/src/HOL/Real/HahnBanach/Subspace.thy Sun Jun 04 19:39:29 2000 +0200 @@ -4,218 +4,218 @@ *) -header {* Subspaces *}; +header {* Subspaces *} -theory Subspace = VectorSpace:; +theory Subspace = VectorSpace: -subsection {* Definition *}; +subsection {* Definition *} text {* A non-empty subset $U$ of a vector space $V$ is a \emph{subspace} of $V$, iff $U$ is closed under addition and -scalar multiplication. *}; +scalar multiplication. *} constdefs is_subspace :: "['a::{minus, plus} set, 'a set] => bool" "is_subspace U V == U ~= {} & U <= V - & (ALL x:U. ALL y:U. ALL a. x + y : U & a (*) x : U)"; + & (ALL x:U. ALL y:U. ALL a. x + y : U & a (*) x : U)" lemma subspaceI [intro]: "[| 00 : U; U <= V; ALL x:U. ALL y:U. (x + y : U); ALL x:U. ALL a. a (*) x : U |] - ==> is_subspace U V"; -proof (unfold is_subspace_def, intro conjI); - assume "00 : U"; thus "U ~= {}"; by fast; -qed (simp+); + ==> is_subspace U V" +proof (unfold is_subspace_def, intro conjI) + assume "00 : U" thus "U ~= {}" by fast +qed (simp+) -lemma subspace_not_empty [intro??]: "is_subspace U V ==> U ~= {}"; - by (unfold is_subspace_def) simp; +lemma subspace_not_empty [intro??]: "is_subspace U V ==> U ~= {}" + by (unfold is_subspace_def) simp -lemma subspace_subset [intro??]: "is_subspace U V ==> U <= V"; - by (unfold is_subspace_def) simp; +lemma subspace_subset [intro??]: "is_subspace U V ==> U <= V" + by (unfold is_subspace_def) simp lemma subspace_subsetD [simp, intro??]: - "[| is_subspace U V; x:U |] ==> x:V"; - by (unfold is_subspace_def) force; + "[| is_subspace U V; x:U |] ==> x:V" + by (unfold is_subspace_def) force lemma subspace_add_closed [simp, intro??]: - "[| is_subspace U V; x:U; y:U |] ==> x + y : U"; - by (unfold is_subspace_def) simp; + "[| is_subspace U V; x:U; y:U |] ==> x + y : U" + by (unfold is_subspace_def) simp lemma subspace_mult_closed [simp, intro??]: - "[| is_subspace U V; x:U |] ==> a (*) x : U"; - by (unfold is_subspace_def) simp; + "[| is_subspace U V; x:U |] ==> a (*) x : U" + by (unfold is_subspace_def) simp lemma subspace_diff_closed [simp, intro??]: "[| is_subspace U V; is_vectorspace V; x:U; y:U |] - ==> x - y : U"; - by (simp! add: diff_eq1 negate_eq1); + ==> x - y : U" + by (simp! add: diff_eq1 negate_eq1) text {* Similar as for linear spaces, the existence of the zero element in every subspace follows from the non-emptiness -of the carrier set and by vector space laws.*}; +of the carrier set and by vector space laws.*} lemma zero_in_subspace [intro??]: - "[| is_subspace U V; is_vectorspace V |] ==> 00 : U"; -proof -; - assume "is_subspace U V" and v: "is_vectorspace V"; - have "U ~= {}"; ..; - hence "EX x. x:U"; by force; - thus ?thesis; - proof; - fix x; assume u: "x:U"; - hence "x:V"; by (simp!); - with v; have "00 = x - x"; by (simp!); - also; have "... : U"; by (rule subspace_diff_closed); - finally; show ?thesis; .; - qed; -qed; + "[| is_subspace U V; is_vectorspace V |] ==> 00 : U" +proof - + assume "is_subspace U V" and v: "is_vectorspace V" + have "U ~= {}" .. + hence "EX x. x:U" by force + thus ?thesis + proof + fix x assume u: "x:U" + hence "x:V" by (simp!) + with v have "00 = x - x" by (simp!) + also have "... : U" by (rule subspace_diff_closed) + finally show ?thesis . + qed +qed lemma subspace_neg_closed [simp, intro??]: - "[| is_subspace U V; is_vectorspace V; x:U |] ==> - x : U"; - by (simp add: negate_eq1); + "[| is_subspace U V; is_vectorspace V; x:U |] ==> - x : U" + by (simp add: negate_eq1) -text_raw {* \medskip *}; -text {* Further derived laws: every subspace is a vector space. *}; +text_raw {* \medskip *} +text {* Further derived laws: every subspace is a vector space. *} lemma subspace_vs [intro??]: - "[| is_subspace U V; is_vectorspace V |] ==> is_vectorspace U"; -proof -; - assume "is_subspace U V" "is_vectorspace V"; - show ?thesis; - proof; - show "00 : U"; ..; - show "ALL x:U. ALL a. a (*) x : U"; by (simp!); - show "ALL x:U. ALL y:U. x + y : U"; by (simp!); - show "ALL x:U. - x = -#1 (*) x"; by (simp! add: negate_eq1); - show "ALL x:U. ALL y:U. x - y = x + - y"; - by (simp! add: diff_eq1); - qed (simp! add: vs_add_mult_distrib1 vs_add_mult_distrib2)+; -qed; + "[| is_subspace U V; is_vectorspace V |] ==> is_vectorspace U" +proof - + assume "is_subspace U V" "is_vectorspace V" + show ?thesis + proof + show "00 : U" .. + show "ALL x:U. ALL a. a (*) x : U" by (simp!) + show "ALL x:U. ALL y:U. x + y : U" by (simp!) + show "ALL x:U. - x = -#1 (*) x" by (simp! add: negate_eq1) + show "ALL x:U. ALL y:U. x - y = x + - y" + by (simp! add: diff_eq1) + qed (simp! add: vs_add_mult_distrib1 vs_add_mult_distrib2)+ +qed -text {* The subspace relation is reflexive. *}; +text {* The subspace relation is reflexive. *} -lemma subspace_refl [intro]: "is_vectorspace V ==> is_subspace V V"; -proof; - assume "is_vectorspace V"; - show "00 : V"; ..; - show "V <= V"; ..; - show "ALL x:V. ALL y:V. x + y : V"; by (simp!); - show "ALL x:V. ALL a. a (*) x : V"; by (simp!); -qed; +lemma subspace_refl [intro]: "is_vectorspace V ==> is_subspace V V" +proof + assume "is_vectorspace V" + show "00 : V" .. + show "V <= V" .. + show "ALL x:V. ALL y:V. x + y : V" by (simp!) + show "ALL x:V. ALL a. a (*) x : V" by (simp!) +qed -text {* The subspace relation is transitive. *}; +text {* The subspace relation is transitive. *} lemma subspace_trans: "[| is_subspace U V; is_vectorspace V; is_subspace V W |] - ==> is_subspace U W"; -proof; - assume "is_subspace U V" "is_subspace V W" "is_vectorspace V"; - show "00 : U"; ..; + ==> is_subspace U W" +proof + assume "is_subspace U V" "is_subspace V W" "is_vectorspace V" + show "00 : U" .. - have "U <= V"; ..; - also; have "V <= W"; ..; - finally; show "U <= W"; .; + have "U <= V" .. + also have "V <= W" .. + finally show "U <= W" . - show "ALL x:U. ALL y:U. x + y : U"; - proof (intro ballI); - fix x y; assume "x:U" "y:U"; - show "x + y : U"; by (simp!); - qed; + show "ALL x:U. ALL y:U. x + y : U" + proof (intro ballI) + fix x y assume "x:U" "y:U" + show "x + y : U" by (simp!) + qed - show "ALL x:U. ALL a. a (*) x : U"; - proof (intro ballI allI); - fix x a; assume "x:U"; - show "a (*) x : U"; by (simp!); - qed; -qed; + show "ALL x:U. ALL a. a (*) x : U" + proof (intro ballI allI) + fix x a assume "x:U" + show "a (*) x : U" by (simp!) + qed +qed -subsection {* Linear closure *}; +subsection {* Linear closure *} text {* The \emph{linear closure} of a vector $x$ is the set of all -scalar multiples of $x$. *}; +scalar multiples of $x$. *} constdefs lin :: "'a => 'a set" - "lin x == {a (*) x | a. True}"; + "lin x == {a (*) x | a. True}" -lemma linD: "x : lin v = (EX a::real. x = a (*) v)"; - by (unfold lin_def) fast; +lemma linD: "x : lin v = (EX a::real. x = a (*) v)" + by (unfold lin_def) fast -lemma linI [intro??]: "a (*) x0 : lin x0"; - by (unfold lin_def) fast; +lemma linI [intro??]: "a (*) x0 : lin x0" + by (unfold lin_def) fast -text {* Every vector is contained in its linear closure. *}; +text {* Every vector is contained in its linear closure. *} -lemma x_lin_x: "[| is_vectorspace V; x:V |] ==> x : lin x"; -proof (unfold lin_def, intro CollectI exI conjI); - assume "is_vectorspace V" "x:V"; - show "x = #1 (*) x"; by (simp!); -qed simp; +lemma x_lin_x: "[| is_vectorspace V; x:V |] ==> x : lin x" +proof (unfold lin_def, intro CollectI exI conjI) + assume "is_vectorspace V" "x:V" + show "x = #1 (*) x" by (simp!) +qed simp -text {* Any linear closure is a subspace. *}; +text {* Any linear closure is a subspace. *} lemma lin_subspace [intro??]: - "[| is_vectorspace V; x:V |] ==> is_subspace (lin x) V"; -proof; - assume "is_vectorspace V" "x:V"; - show "00 : lin x"; - proof (unfold lin_def, intro CollectI exI conjI); - show "00 = (#0::real) (*) x"; by (simp!); - qed simp; + "[| is_vectorspace V; x:V |] ==> is_subspace (lin x) V" +proof + assume "is_vectorspace V" "x:V" + show "00 : lin x" + proof (unfold lin_def, intro CollectI exI conjI) + show "00 = (#0::real) (*) x" by (simp!) + qed simp - show "lin x <= V"; - proof (unfold lin_def, intro subsetI, elim CollectE exE conjE); - fix xa a; assume "xa = a (*) x"; - show "xa:V"; by (simp!); - qed; + show "lin x <= V" + proof (unfold lin_def, intro subsetI, elim CollectE exE conjE) + fix xa a assume "xa = a (*) x" + show "xa:V" by (simp!) + qed - show "ALL x1 : lin x. ALL x2 : lin x. x1 + x2 : lin x"; - proof (intro ballI); - fix x1 x2; assume "x1 : lin x" "x2 : lin x"; - thus "x1 + x2 : lin x"; + show "ALL x1 : lin x. ALL x2 : lin x. x1 + x2 : lin x" + proof (intro ballI) + fix x1 x2 assume "x1 : lin x" "x2 : lin x" + thus "x1 + x2 : lin x" proof (unfold lin_def, elim CollectE exE conjE, - intro CollectI exI conjI); - fix a1 a2; assume "x1 = a1 (*) x" "x2 = a2 (*) x"; - show "x1 + x2 = (a1 + a2) (*) x"; - by (simp! add: vs_add_mult_distrib2); - qed simp; - qed; + intro CollectI exI conjI) + fix a1 a2 assume "x1 = a1 (*) x" "x2 = a2 (*) x" + show "x1 + x2 = (a1 + a2) (*) x" + by (simp! add: vs_add_mult_distrib2) + qed simp + qed - show "ALL xa:lin x. ALL a. a (*) xa : lin x"; - proof (intro ballI allI); - fix x1 a; assume "x1 : lin x"; - thus "a (*) x1 : lin x"; + show "ALL xa:lin x. ALL a. a (*) xa : lin x" + proof (intro ballI allI) + fix x1 a assume "x1 : lin x" + thus "a (*) x1 : lin x" proof (unfold lin_def, elim CollectE exE conjE, - intro CollectI exI conjI); - fix a1; assume "x1 = a1 (*) x"; - show "a (*) x1 = (a * a1) (*) x"; by (simp!); - qed simp; - qed; -qed; + intro CollectI exI conjI) + fix a1 assume "x1 = a1 (*) x" + show "a (*) x1 = (a * a1) (*) x" by (simp!) + qed simp + qed +qed -text {* Any linear closure is a vector space. *}; +text {* Any linear closure is a vector space. *} lemma lin_vs [intro??]: - "[| is_vectorspace V; x:V |] ==> is_vectorspace (lin x)"; -proof (rule subspace_vs); - assume "is_vectorspace V" "x:V"; - show "is_subspace (lin x) V"; ..; -qed; + "[| is_vectorspace V; x:V |] ==> is_vectorspace (lin x)" +proof (rule subspace_vs) + assume "is_vectorspace V" "x:V" + show "is_subspace (lin x) V" .. +qed -subsection {* Sum of two vectorspaces *}; +subsection {* Sum of two vectorspaces *} text {* The \emph{sum} of two vectorspaces $U$ and $V$ is the set of -all sums of elements from $U$ and $V$. *}; +all sums of elements from $U$ and $V$. *} -instance set :: (plus) plus; by intro_classes; +instance set :: (plus) plus by intro_classes defs vs_sum_def: - "U + V == {u + v | u v. u:U & v:V}"; (*** + "U + V == {u + v | u v. u:U & v:V}" (*** constdefs vs_sum :: @@ -224,253 +224,253 @@ ***) lemma vs_sumD: - "x: U + V = (EX u:U. EX v:V. x = u + v)"; - by (unfold vs_sum_def) fast; + "x: U + V = (EX u:U. EX v:V. x = u + v)" + by (unfold vs_sum_def) fast -lemmas vs_sumE = vs_sumD [RS iffD1, elimify]; +lemmas vs_sumE = vs_sumD [RS iffD1, elimify] lemma vs_sumI [intro??]: - "[| x:U; y:V; t= x + y |] ==> t : U + V"; - by (unfold vs_sum_def) fast; + "[| x:U; y:V; t= x + y |] ==> t : U + V" + by (unfold vs_sum_def) fast -text{* $U$ is a subspace of $U + V$. *}; +text{* $U$ is a subspace of $U + V$. *} lemma subspace_vs_sum1 [intro??]: "[| is_vectorspace U; is_vectorspace V |] - ==> is_subspace U (U + V)"; -proof; - assume "is_vectorspace U" "is_vectorspace V"; - show "00 : U"; ..; - show "U <= U + V"; - proof (intro subsetI vs_sumI); - fix x; assume "x:U"; - show "x = x + 00"; by (simp!); - show "00 : V"; by (simp!); - qed; - show "ALL x:U. ALL y:U. x + y : U"; - proof (intro ballI); - fix x y; assume "x:U" "y:U"; show "x + y : U"; by (simp!); - qed; - show "ALL x:U. ALL a. a (*) x : U"; - proof (intro ballI allI); - fix x a; assume "x:U"; show "a (*) x : U"; by (simp!); - qed; -qed; + ==> is_subspace U (U + V)" +proof + assume "is_vectorspace U" "is_vectorspace V" + show "00 : U" .. + show "U <= U + V" + proof (intro subsetI vs_sumI) + fix x assume "x:U" + show "x = x + 00" by (simp!) + show "00 : V" by (simp!) + qed + show "ALL x:U. ALL y:U. x + y : U" + proof (intro ballI) + fix x y assume "x:U" "y:U" show "x + y : U" by (simp!) + qed + show "ALL x:U. ALL a. a (*) x : U" + proof (intro ballI allI) + fix x a assume "x:U" show "a (*) x : U" by (simp!) + qed +qed -text{* The sum of two subspaces is again a subspace.*}; +text{* The sum of two subspaces is again a subspace.*} lemma vs_sum_subspace [intro??]: "[| is_subspace U E; is_subspace V E; is_vectorspace E |] - ==> is_subspace (U + V) E"; -proof; - assume "is_subspace U E" "is_subspace V E" "is_vectorspace E"; - show "00 : U + V"; - proof (intro vs_sumI); - show "00 : U"; ..; - show "00 : V"; ..; - show "(00::'a) = 00 + 00"; by (simp!); - qed; + ==> is_subspace (U + V) E" +proof + assume "is_subspace U E" "is_subspace V E" "is_vectorspace E" + show "00 : U + V" + proof (intro vs_sumI) + show "00 : U" .. + show "00 : V" .. + show "(00::'a) = 00 + 00" by (simp!) + qed - show "U + V <= E"; - proof (intro subsetI, elim vs_sumE bexE); - fix x u v; assume "u : U" "v : V" "x = u + v"; - show "x:E"; by (simp!); - qed; + show "U + V <= E" + proof (intro subsetI, elim vs_sumE bexE) + fix x u v assume "u : U" "v : V" "x = u + v" + show "x:E" by (simp!) + qed - show "ALL x: U + V. ALL y: U + V. x + y : U + V"; - proof (intro ballI); - fix x y; assume "x : U + V" "y : U + V"; - thus "x + y : U + V"; - proof (elim vs_sumE bexE, intro vs_sumI); - fix ux vx uy vy; + show "ALL x: U + V. ALL y: U + V. x + y : U + V" + proof (intro ballI) + fix x y assume "x : U + V" "y : U + V" + thus "x + y : U + V" + proof (elim vs_sumE bexE, intro vs_sumI) + fix ux vx uy vy assume "ux : U" "vx : V" "x = ux + vx" - and "uy : U" "vy : V" "y = uy + vy"; - show "x + y = (ux + uy) + (vx + vy)"; by (simp!); - qed (simp!)+; - qed; + and "uy : U" "vy : V" "y = uy + vy" + show "x + y = (ux + uy) + (vx + vy)" by (simp!) + qed (simp!)+ + qed - show "ALL x : U + V. ALL a. a (*) x : U + V"; - proof (intro ballI allI); - fix x a; assume "x : U + V"; - thus "a (*) x : U + V"; - proof (elim vs_sumE bexE, intro vs_sumI); - fix a x u v; assume "u : U" "v : V" "x = u + v"; - show "a (*) x = (a (*) u) + (a (*) v)"; - by (simp! add: vs_add_mult_distrib1); - qed (simp!)+; - qed; -qed; + show "ALL x : U + V. ALL a. a (*) x : U + V" + proof (intro ballI allI) + fix x a assume "x : U + V" + thus "a (*) x : U + V" + proof (elim vs_sumE bexE, intro vs_sumI) + fix a x u v assume "u : U" "v : V" "x = u + v" + show "a (*) x = (a (*) u) + (a (*) v)" + by (simp! add: vs_add_mult_distrib1) + qed (simp!)+ + qed +qed -text{* The sum of two subspaces is a vectorspace. *}; +text{* The sum of two subspaces is a vectorspace. *} lemma vs_sum_vs [intro??]: "[| is_subspace U E; is_subspace V E; is_vectorspace E |] - ==> is_vectorspace (U + V)"; -proof (rule subspace_vs); - assume "is_subspace U E" "is_subspace V E" "is_vectorspace E"; - show "is_subspace (U + V) E"; ..; -qed; + ==> is_vectorspace (U + V)" +proof (rule subspace_vs) + assume "is_subspace U E" "is_subspace V E" "is_vectorspace E" + show "is_subspace (U + V) E" .. +qed -subsection {* Direct sums *}; +subsection {* Direct sums *} text {* The sum of $U$ and $V$ is called \emph{direct}, iff the zero element is the only common element of $U$ and $V$. For every element $x$ of the direct sum of $U$ and $V$ the decomposition in -$x = u + v$ with $u \in U$ and $v \in V$ is unique.*}; +$x = u + v$ with $u \in U$ and $v \in V$ is unique.*} lemma decomp: "[| is_vectorspace E; is_subspace U E; is_subspace V E; U Int V = {00}; u1:U; u2:U; v1:V; v2:V; u1 + v1 = u2 + v2 |] - ==> u1 = u2 & v1 = v2"; -proof; + ==> u1 = u2 & v1 = v2" +proof assume "is_vectorspace E" "is_subspace U E" "is_subspace V E" "U Int V = {00}" "u1:U" "u2:U" "v1:V" "v2:V" - "u1 + v1 = u2 + v2"; - have eq: "u1 - u2 = v2 - v1"; by (simp! add: vs_add_diff_swap); - have u: "u1 - u2 : U"; by (simp!); - with eq; have v': "v2 - v1 : U"; by simp; - have v: "v2 - v1 : V"; by (simp!); - with eq; have u': "u1 - u2 : V"; by simp; + "u1 + v1 = u2 + v2" + have eq: "u1 - u2 = v2 - v1" by (simp! add: vs_add_diff_swap) + have u: "u1 - u2 : U" by (simp!) + with eq have v': "v2 - v1 : U" by simp + have v: "v2 - v1 : V" by (simp!) + with eq have u': "u1 - u2 : V" by simp - show "u1 = u2"; - proof (rule vs_add_minus_eq); - show "u1 - u2 = 00"; by (rule Int_singletonD [OF _ u u']); - show "u1 : E"; ..; - show "u2 : E"; ..; - qed; + show "u1 = u2" + proof (rule vs_add_minus_eq) + show "u1 - u2 = 00" by (rule Int_singletonD [OF _ u u']) + show "u1 : E" .. + show "u2 : E" .. + qed - show "v1 = v2"; - proof (rule vs_add_minus_eq [RS sym]); - show "v2 - v1 = 00"; by (rule Int_singletonD [OF _ v' v]); - show "v1 : E"; ..; - show "v2 : E"; ..; - qed; -qed; + show "v1 = v2" + proof (rule vs_add_minus_eq [RS sym]) + show "v2 - v1 = 00" by (rule Int_singletonD [OF _ v' v]) + show "v1 : E" .. + show "v2 : E" .. + qed +qed text {* An application of the previous lemma will be used in the proof of the Hahn-Banach Theorem (see page \pageref{decomp-H0-use}): for any element $y + a \mult x_0$ of the direct sum of a vectorspace $H$ and the linear closure of $x_0$ the components $y \in H$ and $a$ are -uniquely determined. *}; +uniquely determined. *} lemma decomp_H0: "[| is_vectorspace E; is_subspace H E; y1 : H; y2 : H; x0 ~: H; x0 : E; x0 ~= 00; y1 + a1 (*) x0 = y2 + a2 (*) x0 |] - ==> y1 = y2 & a1 = a2"; -proof; + ==> y1 = y2 & a1 = a2" +proof assume "is_vectorspace E" and h: "is_subspace H E" and "y1 : H" "y2 : H" "x0 ~: H" "x0 : E" "x0 ~= 00" - "y1 + a1 (*) x0 = y2 + a2 (*) x0"; + "y1 + a1 (*) x0 = y2 + a2 (*) x0" - have c: "y1 = y2 & a1 (*) x0 = a2 (*) x0"; - proof (rule decomp); - show "a1 (*) x0 : lin x0"; ..; - show "a2 (*) x0 : lin x0"; ..; - show "H Int (lin x0) = {00}"; - proof; - show "H Int lin x0 <= {00}"; - proof (intro subsetI, elim IntE, rule singleton_iff[RS iffD2]); - fix x; assume "x:H" "x : lin x0"; - thus "x = 00"; - proof (unfold lin_def, elim CollectE exE conjE); - fix a; assume "x = a (*) x0"; - show ?thesis; - proof cases; - assume "a = (#0::real)"; show ?thesis; by (simp!); - next; - assume "a ~= (#0::real)"; - from h; have "rinv a (*) a (*) x0 : H"; - by (rule subspace_mult_closed) (simp!); - also; have "rinv a (*) a (*) x0 = x0"; by (simp!); - finally; have "x0 : H"; .; - thus ?thesis; by contradiction; - qed; - qed; - qed; - show "{00} <= H Int lin x0"; - proof -; - have "00: H Int lin x0"; - proof (rule IntI); - show "00:H"; ..; - from lin_vs; show "00 : lin x0"; ..; - qed; - thus ?thesis; by simp; - qed; - qed; - show "is_subspace (lin x0) E"; ..; - qed; + have c: "y1 = y2 & a1 (*) x0 = a2 (*) x0" + proof (rule decomp) + show "a1 (*) x0 : lin x0" .. + show "a2 (*) x0 : lin x0" .. + show "H Int (lin x0) = {00}" + proof + show "H Int lin x0 <= {00}" + proof (intro subsetI, elim IntE, rule singleton_iff[RS iffD2]) + fix x assume "x:H" "x : lin x0" + thus "x = 00" + proof (unfold lin_def, elim CollectE exE conjE) + fix a assume "x = a (*) x0" + show ?thesis + proof cases + assume "a = (#0::real)" show ?thesis by (simp!) + next + assume "a ~= (#0::real)" + from h have "rinv a (*) a (*) x0 : H" + by (rule subspace_mult_closed) (simp!) + also have "rinv a (*) a (*) x0 = x0" by (simp!) + finally have "x0 : H" . + thus ?thesis by contradiction + qed + qed + qed + show "{00} <= H Int lin x0" + proof - + have "00: H Int lin x0" + proof (rule IntI) + show "00:H" .. + from lin_vs show "00 : lin x0" .. + qed + thus ?thesis by simp + qed + qed + show "is_subspace (lin x0) E" .. + qed - from c; show "y1 = y2"; by simp; + from c show "y1 = y2" by simp - show "a1 = a2"; - proof (rule vs_mult_right_cancel [RS iffD1]); - from c; show "a1 (*) x0 = a2 (*) x0"; by simp; - qed; -qed; + show "a1 = a2" + proof (rule vs_mult_right_cancel [RS iffD1]) + from c show "a1 (*) x0 = a2 (*) x0" by simp + qed +qed text {* Since for any element $y + a \mult x_0$ of the direct sum of a vectorspace $H$ and the linear closure of $x_0$ the components $y\in H$ and $a$ are unique, it follows from $y\in H$ that -$a = 0$.*}; +$a = 0$.*} lemma decomp_H0_H: "[| is_vectorspace E; is_subspace H E; t:H; x0 ~: H; x0:E; x0 ~= 00 |] - ==> (SOME (y, a). t = y + a (*) x0 & y : H) = (t, (#0::real))"; -proof (rule, unfold split_paired_all); + ==> (SOME (y, a). t = y + a (*) x0 & y : H) = (t, (#0::real))" +proof (rule, unfold split_paired_all) assume "is_vectorspace E" "is_subspace H E" "t:H" "x0 ~: H" "x0:E" - "x0 ~= 00"; - have h: "is_vectorspace H"; ..; - fix y a; presume t1: "t = y + a (*) x0" and "y:H"; - have "y = t & a = (#0::real)"; - by (rule decomp_H0) (assumption | (simp!))+; - thus "(y, a) = (t, (#0::real))"; by (simp!); -qed (simp!)+; + "x0 ~= 00" + have h: "is_vectorspace H" .. + fix y a presume t1: "t = y + a (*) x0" and "y:H" + have "y = t & a = (#0::real)" + by (rule decomp_H0) (assumption | (simp!))+ + thus "(y, a) = (t, (#0::real))" by (simp!) +qed (simp!)+ text {* The components $y\in H$ and $a$ in $y \plus a \mult x_0$ are unique, so the function $h_0$ defined by -$h_0 (y \plus a \mult x_0) = h y + a \cdot \xi$ is definite. *}; +$h_0 (y \plus a \mult x_0) = h y + a \cdot \xi$ is definite. *} lemma h0_definite: "[| h0 == (\\x. let (y, a) = SOME (y, a). (x = y + a (*) x0 & y:H) in (h y) + a * xi); x = y + a (*) x0; is_vectorspace E; is_subspace H E; y:H; x0 ~: H; x0:E; x0 ~= 00 |] - ==> h0 x = h y + a * xi"; -proof -; + ==> h0 x = h y + a * xi" +proof - assume "h0 == (\\x. let (y, a) = SOME (y, a). (x = y + a (*) x0 & y:H) in (h y) + a * xi)" "x = y + a (*) x0" "is_vectorspace E" "is_subspace H E" - "y:H" "x0 ~: H" "x0:E" "x0 ~= 00"; - have "x : H + (lin x0)"; - by (simp! add: vs_sum_def lin_def) force+; - have "EX! xa. ((\\(y, a). x = y + a (*) x0 & y:H) xa)"; - proof; - show "EX xa. ((\\(y, a). x = y + a (*) x0 & y:H) xa)"; - by (force!); - next; - fix xa ya; + "y:H" "x0 ~: H" "x0:E" "x0 ~= 00" + have "x : H + (lin x0)" + by (simp! add: vs_sum_def lin_def) force+ + have "EX! xa. ((\\(y, a). x = y + a (*) x0 & y:H) xa)" + proof + show "EX xa. ((\\(y, a). x = y + a (*) x0 & y:H) xa)" + by (force!) + next + fix xa ya assume "(\\(y,a). x = y + a (*) x0 & y : H) xa" - "(\\(y,a). x = y + a (*) x0 & y : H) ya"; - show "xa = ya"; ; - proof -; - show "fst xa = fst ya & snd xa = snd ya ==> xa = ya"; - by (rule Pair_fst_snd_eq [RS iffD2]); - have x: "x = fst xa + snd xa (*) x0 & fst xa : H"; - by (force!); - have y: "x = fst ya + snd ya (*) x0 & fst ya : H"; - by (force!); - from x y; show "fst xa = fst ya & snd xa = snd ya"; - by (elim conjE) (rule decomp_H0, (simp!)+); - qed; - qed; - hence eq: "(SOME (y, a). x = y + a (*) x0 & y:H) = (y, a)"; - by (rule select1_equality) (force!); - thus "h0 x = h y + a * xi"; by (simp! add: Let_def); -qed; + "(\\(y,a). x = y + a (*) x0 & y : H) ya" + show "xa = ya" + proof - + show "fst xa = fst ya & snd xa = snd ya ==> xa = ya" + by (rule Pair_fst_snd_eq [RS iffD2]) + have x: "x = fst xa + snd xa (*) x0 & fst xa : H" + by (force!) + have y: "x = fst ya + snd ya (*) x0 & fst ya : H" + by (force!) + from x y show "fst xa = fst ya & snd xa = snd ya" + by (elim conjE) (rule decomp_H0, (simp!)+) + qed + qed + hence eq: "(SOME (y, a). x = y + a (*) x0 & y:H) = (y, a)" + by (rule select1_equality) (force!) + thus "h0 x = h y + a * xi" by (simp! add: Let_def) +qed -end; \ No newline at end of file +end \ No newline at end of file diff -r ea4dc7603f0b -r 371f023d3dbd src/HOL/Real/HahnBanach/VectorSpace.thy --- a/src/HOL/Real/HahnBanach/VectorSpace.thy Sun Jun 04 00:09:04 2000 +0200 +++ b/src/HOL/Real/HahnBanach/VectorSpace.thy Sun Jun 04 19:39:29 2000 +0200 @@ -3,38 +3,38 @@ Author: Gertrud Bauer, TU Munich *) -header {* Vector spaces *}; +header {* Vector spaces *} -theory VectorSpace = Bounds + Aux:; +theory VectorSpace = Bounds + Aux: -subsection {* Signature *}; +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. *}; +element $\zero$ is defined. *} consts prod :: "[real, 'a] => 'a" (infixr "'(*')" 70) - zero :: 'a ("00"); + zero :: 'a ("00") syntax (symbols) prod :: "[real, 'a] => 'a" (infixr "\" 70) - zero :: 'a ("\"); + zero :: 'a ("\") (* text {* The unary and binary minus can be considered as -abbreviations: *}; +abbreviations: *} *) (*** constdefs negate :: "'a => 'a" ("- _" [100] 100) - "- x == (- (#1::real)) ( * ) x" + "- x == (- #1) ( * ) x" diff :: "'a => 'a => 'a" (infixl "-" 68) "x - y == x + - y"; ***) -subsection {* Vector space laws *}; +subsection {* Vector space laws *} text {* A \emph{vector space} is a non-empty set $V$ of elements from $\alpha$ with the following vector space laws: The set $V$ is closed @@ -44,7 +44,7 @@ multiplication are distributive; scalar multiplication is associative and the real number $1$ is the neutral element of scalar multiplication. -*}; +*} constdefs is_vectorspace :: "('a::{plus,minus}) set => bool" @@ -59,12 +59,12 @@ & a (*) (x + y) = a (*) x + a (*) y & (a + b) (*) x = a (*) x + b (*) x & (a * b) (*) x = a (*) b (*) x - & (#1::real) (*) x = x - & - x = (- (#1::real)) (*) x - & x - y = x + - y)"; + & #1 (*) x = x + & - x = (- #1) (*) x + & x - y = x + - y)" -text_raw {* \medskip *}; -text {* The corresponding introduction rule is:*}; +text_raw {* \medskip *} +text {* The corresponding introduction rule is:*} lemma vsI [intro]: "[| 00:V; @@ -77,326 +77,326 @@ ALL x:V. ALL y:V. ALL a. a (*) (x + y) = a (*) x + a (*) y; ALL x:V. ALL a b. (a + b) (*) x = a (*) x + b (*) x; ALL x:V. ALL a b. (a * b) (*) x = a (*) b (*) x; - ALL x:V. (#1::real) (*) x = x; - ALL x:V. - x = (- (#1::real)) (*) x; - ALL x:V. ALL y:V. x - y = x + - y |] ==> is_vectorspace V"; -proof (unfold is_vectorspace_def, intro conjI ballI allI); - fix x y z; + ALL x:V. #1 (*) x = x; + ALL x:V. - x = (- #1) (*) x; + ALL x:V. ALL y:V. x - y = x + - y |] ==> is_vectorspace V" +proof (unfold is_vectorspace_def, intro conjI ballI allI) + fix x y z assume "x:V" "y:V" "z:V" - "ALL x:V. ALL y:V. ALL z:V. x + y + z = x + (y + z)"; - thus "x + y + z = x + (y + z)"; by (elim bspec[elimify]); -qed force+; + "ALL x:V. ALL y:V. ALL z:V. x + y + z = x + (y + z)" + thus "x + y + z = x + (y + z)" by (elim bspec[elimify]) +qed force+ -text_raw {* \medskip *}; -text {* The corresponding destruction rules are: *}; +text_raw {* \medskip *} +text {* The corresponding destruction rules are: *} lemma negate_eq1: - "[| is_vectorspace V; x:V |] ==> - x = (- (#1::real)) (*) x"; - by (unfold is_vectorspace_def) simp; + "[| 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"; - by (unfold is_vectorspace_def) simp; + "[| 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::real)) (*) x = - x"; - by (unfold is_vectorspace_def) simp; + "[| is_vectorspace V; x:V |] ==> (- #1) (*) x = - x" + by (unfold is_vectorspace_def) simp lemma negate_eq2a: - "[| is_vectorspace V; x:V |] ==> ((#-1::real)) (*) x = - x"; - by (unfold is_vectorspace_def) simp; + "[| 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"; - by (unfold is_vectorspace_def) simp; + "[| 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 ~= {})"; - by (unfold is_vectorspace_def) simp; +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"; - by (unfold is_vectorspace_def) simp; + "[| 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"; - by (unfold is_vectorspace_def) simp; + "[| 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"; - by (simp add: diff_eq1 negate_eq1); + "[| 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"; - by (simp add: negate_eq1); + "[| 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 |] - ==> (x + y) + z = x + (y + z)"; - by (unfold is_vectorspace_def) fast; + ==> (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"; - by (unfold is_vectorspace_def) simp; + "[| 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 |] - ==> x + (y + z) = y + (x + z)"; -proof -; - 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); - also; have "... = y + (x + z)"; by (simp! only: vs_add_assoc); - finally; show ?thesis; .; -qed; + ==> x + (y + z) = y + (x + z)" +proof - + 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) + also have "... = y + (x + z)" by (simp! only: vs_add_assoc) + finally show ?thesis . +qed -theorems vs_add_ac = vs_add_assoc vs_add_commute vs_add_left_commute; +theorems vs_add_ac = vs_add_assoc vs_add_commute vs_add_left_commute lemma vs_diff_self [simp]: - "[| is_vectorspace V; x:V |] ==> x - x = 00"; - by (unfold is_vectorspace_def) simp; + "[| is_vectorspace V; x:V |] ==> x - x = 00" + 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. *}; +follows from the non-emptiness of carrier set. *} -lemma zero_in_vs [simp, intro]: "is_vectorspace V ==> 00:V"; -proof -; - assume "is_vectorspace V"; - have "V ~= {}"; ..; - hence "EX x. x:V"; by force; - thus ?thesis; - proof; - fix x; assume "x:V"; - have "00 = x - x"; by (simp!); - also; have "... : V"; by (simp! only: vs_diff_closed); - finally; show ?thesis; .; - qed; -qed; +lemma zero_in_vs [simp, intro]: "is_vectorspace V ==> 00:V" +proof - + assume "is_vectorspace V" + have "V ~= {}" .. + hence "EX x. x:V" by force + thus ?thesis + proof + fix x assume "x:V" + have "00 = x - x" by (simp!) + also have "... : V" by (simp! only: vs_diff_closed) + finally show ?thesis . + qed +qed lemma vs_add_zero_left [simp]: - "[| is_vectorspace V; x:V |] ==> 00 + x = x"; - by (unfold is_vectorspace_def) simp; + "[| is_vectorspace V; x:V |] ==> 00 + x = x" + by (unfold is_vectorspace_def) simp lemma vs_add_zero_right [simp]: - "[| is_vectorspace V; x:V |] ==> x + 00 = x"; -proof -; - assume "is_vectorspace V" "x:V"; - hence "x + 00 = 00 + x"; by simp; - also; have "... = x"; by (simp!); - finally; show ?thesis; .; -qed; + "[| is_vectorspace V; x:V |] ==> x + 00 = x" +proof - + assume "is_vectorspace V" "x:V" + hence "x + 00 = 00 + 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"; - by (unfold is_vectorspace_def) simp; + ==> 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"; - by (unfold is_vectorspace_def) simp; + ==> (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)"; - by (unfold is_vectorspace_def) simp; + "[| 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"; - by (simp only: vs_mult_assoc); + "[| 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::real) (*) x = x"; - by (unfold is_vectorspace_def) simp; + "[| 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"; - by (simp add: diff_eq1 negate_eq1 vs_add_mult_distrib1); + ==> 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)"; -proof -; - 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"; - by (rule vs_add_mult_distrib2); - also; have "... = a (*) x + - (b (*) x)"; - by (simp! add: negate_eq1); - also; have "... = a (*) x - (b (*) x)"; - by (simp! add: diff_eq1); - finally; show ?thesis; .; -qed; + ==> (a - b) (*) x = a (*) x - (b (*) x)" +proof - + 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" + by (rule vs_add_mult_distrib2) + also have "... = a (*) x + - (b (*) x)" + by (simp! add: negate_eq1) + also have "... = a (*) x - (b (*) x)" + by (simp! add: diff_eq1) + finally show ?thesis . +qed -(*text_raw {* \paragraph {Further derived laws.} *};*) -text_raw {* \medskip *}; -text{* Further derived laws: *}; +(*text_raw {* \paragraph {Further derived laws.} *}*) +text_raw {* \medskip *} +text{* Further derived laws: *} lemma vs_mult_zero_left [simp]: - "[| is_vectorspace V; x:V |] ==> (#0::real) (*) x = 00"; -proof -; - assume "is_vectorspace V" "x:V"; - have "(#0::real) (*) x = ((#1::real) - (#1::real)) (*) x"; by simp; - also; have "... = ((#1::real) + - (#1::real)) (*) x"; by simp; - also; have "... = (#1::real) (*) x + (- (#1::real)) (*) x"; - by (rule vs_add_mult_distrib2); - also; have "... = x + (- (#1::real)) (*) x"; by (simp!); - also; have "... = x + - x"; by (simp! add: negate_eq2a);; - also; have "... = x - x"; by (simp! add: diff_eq2); - also; have "... = 00"; by (simp!); - finally; show ?thesis; .; -qed; + "[| is_vectorspace V; x:V |] ==> #0 (*) x = 00" +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" + by (rule vs_add_mult_distrib2) + 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 "... = 00" by (simp!) + finally show ?thesis . +qed lemma vs_mult_zero_right [simp]: "[| is_vectorspace (V:: 'a::{plus, minus} set) |] - ==> a (*) 00 = (00::'a)"; -proof -; - assume "is_vectorspace V"; - have "a (*) 00 = a (*) (00 - (00::'a))"; by (simp!); - also; have "... = a (*) 00 - a (*) 00"; - by (rule vs_diff_mult_distrib1) (simp!)+; - also; have "... = 00"; by (simp!); - finally; show ?thesis; .; -qed; + ==> a (*) 00 = (00::'a)" +proof - + assume "is_vectorspace V" + have "a (*) 00 = a (*) (00 - (00::'a))" by (simp!) + also have "... = a (*) 00 - a (*) 00" + by (rule vs_diff_mult_distrib1) (simp!)+ + also have "... = 00" by (simp!) + finally show ?thesis . +qed lemma vs_minus_mult_cancel [simp]: - "[| is_vectorspace V; x:V |] ==> (- a) (*) - x = a (*) x"; - by (simp add: negate_eq1); + "[| 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"; -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"]); - also; have "... = y - x"; by (simp! add: diff_eq1); - finally; show ?thesis; .; -qed; + "[| 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"]) + 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 = 00"; - by (simp! add: diff_eq2); + "[| is_vectorspace V; x:V |] ==> x + - x = 00" + by (simp! add: diff_eq2) lemma vs_add_minus_left [simp]: - "[| is_vectorspace V; x:V |] ==> - x + x = 00"; - by (simp! add: diff_eq2); + "[| is_vectorspace V; x:V |] ==> - x + x = 00" + by (simp! add: diff_eq2) lemma vs_minus_minus [simp]: - "[| is_vectorspace V; x:V |] ==> - (- x) = x"; - by (simp add: negate_eq1); + "[| is_vectorspace V; x:V |] ==> - (- x) = x" + by (simp add: negate_eq1) lemma vs_minus_zero [simp]: - "is_vectorspace (V::'a::{minus, plus} set) ==> - (00::'a) = 00"; - by (simp add: negate_eq1); + "is_vectorspace (V::'a::{minus, plus} set) ==> - (00::'a) = 00" + by (simp add: negate_eq1) lemma vs_minus_zero_iff [simp]: "[| is_vectorspace V; x:V |] ==> (- x = 00) = (x = 00)" - (concl is "?L = ?R"); -proof -; - assume "is_vectorspace V" "x:V"; - show "?L = ?R"; - proof; - have "x = - (- x)"; by (rule vs_minus_minus [RS sym]); - also; assume ?L; - also; have "- ... = 00"; by (rule vs_minus_zero); - finally; show ?R; .; - qed (simp!); -qed; + (concl is "?L = ?R") +proof - + assume "is_vectorspace V" "x:V" + show "?L = ?R" + proof + have "x = - (- x)" by (rule vs_minus_minus [RS sym]) + also assume ?L + also have "- ... = 00" by (rule vs_minus_zero) + finally show ?R . + qed (simp!) +qed lemma vs_add_minus_cancel [simp]: - "[| is_vectorspace V; x:V; y:V |] ==> x + (- x + y) = y"; - by (simp add: vs_add_assoc [RS sym] del: vs_add_commute); + "[| 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"; - by (simp add: vs_add_assoc [RS sym] del: vs_add_commute); + "[| 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 |] - ==> - (x + y) = - x + - y"; - by (simp add: negate_eq1 vs_add_mult_distrib1); + ==> - (x + y) = - x + - y" + by (simp add: negate_eq1 vs_add_mult_distrib1) lemma vs_diff_zero [simp]: - "[| is_vectorspace V; x:V |] ==> x - 00 = x"; - by (simp add: diff_eq1); + "[| is_vectorspace V; x:V |] ==> x - 00 = x" + by (simp add: diff_eq1) lemma vs_diff_zero_right [simp]: - "[| is_vectorspace V; x:V |] ==> 00 - x = - x"; - by (simp add:diff_eq1); + "[| is_vectorspace V; x:V |] ==> 00 - x = - x" + by (simp add:diff_eq1) lemma vs_add_left_cancel: "[| 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"; - have "y = 00 + 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; have "... = z"; by (simp!); - finally; show ?R; .; -qed force; + (concl is "?L = ?R") +proof + assume "is_vectorspace V" "x:V" "y:V" "z:V" + have "y = 00 + 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 have "... = z" by (simp!) + finally show ?R . +qed force lemma vs_add_right_cancel: "[| 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); + ==> (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 |] - ==> x + y = x' + y' ==> x + (y + z) = x' + (y' + z)"; - by (simp only: vs_add_assoc [RS sym]); + ==> 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"; - by (simp add: real_mult_commute); + ==> x (*) y (*) z = y (*) x (*) z" + by (simp add: real_mult_commute) lemma vs_mult_zero_uniq : - "[| is_vectorspace V; x:V; a (*) x = 00; x ~= 00 |] ==> a = (#0::real)"; -proof (rule classical); - assume "is_vectorspace V" "x:V" "a (*) x = 00" "x ~= 00"; - assume "a ~= (#0::real)"; - have "x = (rinv a * a) (*) x"; by (simp!); - also; have "... = rinv a (*) (a (*) x)"; by (rule vs_mult_assoc); - also; have "... = rinv a (*) 00"; by (simp!); - also; have "... = 00"; by (simp!); - finally; have "x = 00"; .; - thus "a = (#0::real)"; by contradiction; -qed; + "[| is_vectorspace V; x:V; a (*) x = 00; x ~= 00 |] ==> a = #0" +proof (rule classical) + assume "is_vectorspace V" "x:V" "a (*) x = 00" "x ~= 00" + assume "a ~= #0" + have "x = (rinv a * a) (*) x" by (simp!) + also have "... = rinv a (*) (a (*) x)" by (rule vs_mult_assoc) + also have "... = rinv a (*) 00" by (simp!) + also have "... = 00" by (simp!) + finally have "x = 00" . + thus "a = #0" by contradiction +qed lemma vs_mult_left_cancel: - "[| is_vectorspace V; x:V; y:V; a ~= (#0::real) |] ==> + "[| 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::real)"; - have "x = (#1::real) (*) 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!); - finally; show ?R; .; -qed simp; + (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)" + by (simp! only: vs_mult_assoc) + also assume ?L + also have "rinv a (*) ... = y" by (simp!) + finally show ?R . +qed simp lemma vs_mult_right_cancel: (*** forward ***) "[| is_vectorspace V; x:V; x ~= 00 |] - ==> (a (*) x = b (*) x) = (a = b)" (concl is "?L = ?R"); -proof; - assume "is_vectorspace V" "x:V" "x ~= 00"; - have "(a - b) (*) x = a (*) x - b (*) x"; - by (simp! add: vs_diff_mult_distrib2); - also; assume ?L; hence "a (*) x - b (*) x = 00"; by (simp!); - finally; have "(a - b) (*) x = 00"; .; - hence "a - b = (#0::real)"; by (simp! add: vs_mult_zero_uniq); - thus "a = b"; by (rule real_add_minus_eq); -qed simp; (*** + ==> (a (*) x = b (*) x) = (a = b)" (concl is "?L = ?R") +proof + assume "is_vectorspace V" "x:V" "x ~= 00" + have "(a - b) (*) x = a (*) x - b (*) x" + by (simp! add: vs_diff_mult_distrib2) + also assume ?L hence "a (*) x - b (*) x = 00" by (simp!) + finally have "(a - b) (*) x = 00" . + hence "a - b = #0" by (simp! add: vs_mult_zero_uniq) + thus "a = b" by (rule real_add_minus_eq) +qed simp (*** backward : lemma vs_mult_right_cancel: @@ -425,115 +425,115 @@ lemma vs_eq_diff_eq: "[| 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"; - show "?L = ?R"; - proof; - assume ?L; - hence "x + y = z - y + y"; by simp; - also; have "... = z + - y + y"; by (simp! add: diff_eq1); - also; have "... = z + (- y + y)"; - by (rule vs_add_assoc) (simp!)+; - also; from vs; have "... = z + 00"; - by (simp only: vs_add_minus_left); - also; from vs; have "... = z"; by (simp only: vs_add_zero_right); - finally; show ?R; .; - next; - assume ?R; - hence "z - y = (x + y) - y"; by simp; - also; from vs; have "... = x + y + - y"; - by (simp add: diff_eq1); - also; have "... = x + (y + - y)"; - by (rule vs_add_assoc) (simp!)+; - also; have "... = x"; by (simp!); - finally; show ?L; by (rule sym); - qed; -qed; + (concl is "?L = ?R" ) +proof - + assume vs: "is_vectorspace V" "x:V" "y:V" "z:V" + show "?L = ?R" + proof + assume ?L + hence "x + y = z - y + y" by simp + also have "... = z + - y + y" by (simp! add: diff_eq1) + also have "... = z + (- y + y)" + by (rule vs_add_assoc) (simp!)+ + also from vs have "... = z + 00" + by (simp only: vs_add_minus_left) + also from vs have "... = z" by (simp only: vs_add_zero_right) + finally show ?R . + next + assume ?R + hence "z - y = (x + y) - y" by simp + also from vs have "... = x + y + - y" + by (simp add: diff_eq1) + also have "... = x + (y + - y)" + by (rule vs_add_assoc) (simp!)+ + also have "... = x" by (simp!) + finally show ?L by (rule sym) + qed +qed lemma vs_add_minus_eq_minus: - "[| is_vectorspace V; x:V; y:V; x + y = 00 |] ==> x = - y"; -proof -; - 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 = 00"; - also; have "- y + 00 = - y"; by (simp!); - finally; show "x = - y"; .; -qed; + "[| is_vectorspace V; x:V; y:V; x + y = 00 |] ==> x = - y" +proof - + 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 = 00" + also have "- y + 00 = - y" by (simp!) + finally show "x = - y" . +qed lemma vs_add_minus_eq: - "[| is_vectorspace V; x:V; y:V; x - y = 00 |] ==> x = y"; -proof -; - assume "is_vectorspace V" "x:V" "y:V" "x - y = 00"; - assume "x - y = 00"; - hence e: "x + - y = 00"; by (simp! add: diff_eq1); - with _ _ _; have "x = - (- y)"; - by (rule vs_add_minus_eq_minus) (simp!)+; - thus "x = y"; by (simp!); -qed; + "[| is_vectorspace V; x:V; y:V; x - y = 00 |] ==> x = y" +proof - + assume "is_vectorspace V" "x:V" "y:V" "x - y = 00" + assume "x - y = 00" + hence e: "x + - y = 00" by (simp! add: diff_eq1) + with _ _ _ have "x = - (- y)" + by (rule vs_add_minus_eq_minus) (simp!)+ + thus "x = y" by (simp!) +qed lemma vs_add_diff_swap: "[| is_vectorspace V; a:V; b:V; c:V; d:V; a + b = c + d |] - ==> a - c = d - b"; -proof -; + ==> a - c = d - b" +proof - 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); - also; have "... = d"; by (rule vs_minus_add_cancel); - finally; have eq: "- c + (a + b) = d"; .; - from vs; have "a - c = (- c + (a + b)) + - b"; - by (simp add: vs_add_ac diff_eq1); - also; from eq; have "... = d + - b"; - by (simp! add: vs_add_right_cancel); - also; have "... = d - b"; by (simp! add : diff_eq2); - finally; show "a - c = d - b"; .; -qed; + and eq: "a + b = c + d" + have "- c + (a + b) = - c + (c + d)" + by (simp! add: vs_add_left_cancel) + also have "... = d" by (rule vs_minus_add_cancel) + finally have eq: "- c + (a + b) = d" . + from vs have "a - c = (- c + (a + b)) + - b" + by (simp add: vs_add_ac diff_eq1) + also from eq have "... = d + - b" + by (simp! add: vs_add_right_cancel) + also have "... = d - b" by (simp! add : diff_eq2) + finally show "a - c = d - b" . +qed lemma vs_add_cancel_21: "[| 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"; - show "?L = ?R"; - proof; - have "x + z = - y + y + (x + z)"; by (simp!); - also; have "... = - y + (y + (x + z))"; - by (rule vs_add_assoc) (simp!)+; - also; have "y + (x + z) = x + (y + z)"; by (simp!); - also; assume ?L; - also; have "- y + (y + u) = u"; by (simp!); - finally; show ?R; .; - qed (simp! only: vs_add_left_commute [of V x]); -qed; + (concl is "?L = ?R") +proof - + 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!) + also have "... = - y + (y + (x + z))" + by (rule vs_add_assoc) (simp!)+ + also have "y + (x + z) = x + (y + z)" by (simp!) + also assume ?L + also have "- y + (y + u) = u" by (simp!) + finally show ?R . + qed (simp! only: vs_add_left_commute [of V x]) +qed lemma vs_add_cancel_end: "[| 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"; - show "?L = ?R"; - proof; - assume l: ?L; - have "x + z = 00"; - proof (rule vs_add_left_cancel [RS iffD1]); - have "y + (x + z) = x + (y + z)"; by (simp!); - also; note l; - also; have "y = y + 00"; by (simp!); - finally; show "y + (x + z) = y + 00"; .; - qed (simp!)+; - thus "x = - z"; by (simp! add: vs_add_minus_eq_minus); - next; - assume r: ?R; - hence "x + (y + z) = - z + (y + z)"; by simp; - also; have "... = y + (- z + z)"; - by (simp! only: vs_add_left_commute); - also; have "... = y"; by (simp!); - finally; show ?L; .; - qed; -qed; + (concl is "?L = ?R" ) +proof - + assume "is_vectorspace V" "x:V" "y:V" "z:V" + show "?L = ?R" + proof + assume l: ?L + have "x + z = 00" + proof (rule vs_add_left_cancel [RS iffD1]) + have "y + (x + z) = x + (y + z)" by (simp!) + also note l + also have "y = y + 00" by (simp!) + finally show "y + (x + z) = y + 00" . + qed (simp!)+ + thus "x = - z" by (simp! add: vs_add_minus_eq_minus) + next + assume r: ?R + hence "x + (y + z) = - z + (y + z)" by simp + also have "... = y + (- z + z)" + by (simp! only: vs_add_left_commute) + also have "... = y" by (simp!) + finally show ?L . + qed +qed -end; +end \ No newline at end of file diff -r ea4dc7603f0b -r 371f023d3dbd src/HOL/Real/HahnBanach/ZornLemma.thy --- a/src/HOL/Real/HahnBanach/ZornLemma.thy Sun Jun 04 00:09:04 2000 +0200 +++ b/src/HOL/Real/HahnBanach/ZornLemma.thy Sun Jun 04 19:39:29 2000 +0200 @@ -3,9 +3,9 @@ Author: Gertrud Bauer, TU Munich *) -header {* Zorn's Lemma *}; +header {* Zorn's Lemma *} -theory ZornLemma = Aux + Zorn:; +theory ZornLemma = Aux + Zorn: text {* Zorn's Lemmas states: if every linear ordered subset of an ordered set $S$ has an upper bound in $S$, then there exists a maximal @@ -13,43 +13,43 @@ set inclusion. Since the union of a chain of sets is an upper bound for all elements of the chain, the conditions of Zorn's lemma can be modified: if $S$ is non-empty, it suffices to show that for every -non-empty chain $c$ in $S$ the union of $c$ also lies in $S$. *}; +non-empty chain $c$ in $S$ the union of $c$ also lies in $S$. *} theorem Zorn's_Lemma: "(!!c. c: chain S ==> EX x. x:c ==> Union c : S) ==> a:S - ==> EX y: S. ALL z: S. y <= z --> y = z"; -proof (rule Zorn_Lemma2); + ==> EX y: S. ALL z: S. y <= z --> y = z" +proof (rule Zorn_Lemma2) txt_raw {* \footnote{See - \url{http://isabelle.in.tum.de/library/HOL/HOL-Real/Zorn.html}} \isanewline *}; - assume r: "!!c. c: chain S ==> EX x. x:c ==> Union c : S"; - assume aS: "a:S"; - show "ALL c:chain S. EX y:S. ALL z:c. z <= y"; - proof; - fix c; assume "c:chain S"; - show "EX y:S. ALL z:c. z <= y"; - proof cases; + \url{http://isabelle.in.tum.de/library/HOL/HOL-Real/Zorn.html}} \isanewline *} + assume r: "!!c. c: chain S ==> EX x. x:c ==> Union c : S" + assume aS: "a:S" + show "ALL c:chain S. EX y:S. ALL z:c. z <= y" + proof + fix c assume "c:chain S" + show "EX y:S. ALL z:c. z <= y" + proof cases txt{* If $c$ is an empty chain, then every element - in $S$ is an upper bound of $c$. *}; + in $S$ is an upper bound of $c$. *} - assume "c={}"; - with aS; show ?thesis; by fast; + assume "c={}" + with aS show ?thesis by fast txt{* If $c$ is non-empty, then $\Union c$ - is an upper bound of $c$, lying in $S$. *}; + is an upper bound of $c$, lying in $S$. *} - next; - assume c: "c~={}"; - show ?thesis; - proof; - show "ALL z:c. z <= Union c"; by fast; - show "Union c : S"; - proof (rule r); - from c; show "EX x. x:c"; by fast; - qed; - qed; - qed; - qed; -qed; + next + assume c: "c~={}" + show ?thesis + proof + show "ALL z:c. z <= Union c" by fast + show "Union c : S" + proof (rule r) + from c show "EX x. x:c" by fast + qed + qed + qed + qed +qed -end; +end \ No newline at end of file