--- 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
--- 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
--- 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
--- 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 == \<lambda>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 (\<lambda>x. P))"
"UPPER_BOUNDS x. P" == "UPPER_BOUNDS x:UNIV. P"
"LOWER_BOUNDS x:A. P" == "LowerBounds A (Collect (\<lambda>x. P))"
- "LOWER_BOUNDS x. 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 (\<lambda>x. P))"
"SUP x. P" == "SUP x:UNIV. P"
"INF x:A. P" == "Inf A (Collect (\<lambda>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
--- 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
--- 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 == \<lambda>x. (SOME y. (x, y):g)";
+ "funct g == \<lambda>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
--- 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 == "\\<lambda>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 ==
"\\<lambda>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 == "\\<lambda>x. function_norm F norm f * norm x";
+ def p == "\\<lambda>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
--- 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 == (\<lambda>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 == (\<lambda>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 == (\<lambda>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 == (\<lambda>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
--- 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
--- 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
--- 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
--- 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 == (\\<lambda>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 == (\\<lambda>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. ((\\<lambda>(y, a). x = y + a (*) x0 & y:H) xa)";
- proof;
- show "EX xa. ((\\<lambda>(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. ((\\<lambda>(y, a). x = y + a (*) x0 & y:H) xa)"
+ proof
+ show "EX xa. ((\\<lambda>(y, a). x = y + a (*) x0 & y:H) xa)"
+ by (force!)
+ next
+ fix xa ya
assume "(\\<lambda>(y,a). x = y + a (*) x0 & y : H) xa"
- "(\\<lambda>(y,a). x = y + a (*) x0 & y : H) ya";
- 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;
+ "(\\<lambda>(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
--- 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 "\<prod>" 70)
- zero :: 'a ("\<zero>");
+ zero :: 'a ("\<zero>")
(* 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
--- 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