--- a/src/HOL/Real/HahnBanach/Aux.thy Thu May 06 20:43:30 2004 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,90 +0,0 @@
-(* Title: HOL/Real/HahnBanach/Aux.thy
- ID: $Id$
- Author: Gertrud Bauer, TU Munich
-*)
-
-header {* Auxiliary theorems *} (* FIXME clean: many are in Ring_and_Field *)
-
-theory Aux = Real + Bounds + Zorn:
-
-text {* Some existing theorems are declared as extra introduction
-or elimination rules, respectively. *}
-
-lemmas [dest?] = chainD
-lemmas chainE2 [elim?] = chainD2 [elim_format, standard]
-
-
-text{* \medskip Some lemmas about orders. *}
-
-lemma lt_imp_not_eq: "x < (y::'a::order) \<Longrightarrow> x \<noteq> y"
- by (simp add: order_less_le)
-
-lemma le_noteq_imp_less:
- "x \<le> (r::'a::order) \<Longrightarrow> x \<noteq> r \<Longrightarrow> x < r"
-proof -
- assume "x \<le> r" and ne:"x \<noteq> r"
- hence "x < r \<or> x = r" by (simp add: order_le_less)
- with ne show ?thesis by simp
-qed
-
-
-text {* \medskip Some lemmas for the reals. *}
-
-lemma real_add_minus_eq: "x - y = (0::real) \<Longrightarrow> x = y"
- by simp
-
-lemma abs_minus_one: "abs (- (1::real)) = 1"
- by simp
-
-lemma real_mult_le_le_mono1a:
- "(0::real) \<le> z \<Longrightarrow> x \<le> y \<Longrightarrow> z * x \<le> z * y"
- by (simp add: mult_left_mono)
-
-text{*The next two results are needlessly weak*}
-lemma real_mult_less_le_anti:
- "z < (0::real) \<Longrightarrow> x \<le> y \<Longrightarrow> z * y \<le> z * x"
- by (simp add: mult_left_mono_neg order_less_imp_le)
-
-lemma real_mult_less_le_mono:
- "(0::real) < z \<Longrightarrow> x \<le> y \<Longrightarrow> z * x \<le> z * y"
- by (simp add: mult_left_mono order_less_imp_le)
-
-lemma real_mult_inv_right1: "(x::real) \<noteq> 0 \<Longrightarrow> x * inverse x = 1"
- by simp
-
-lemma real_mult_inv_left1: "(x::real) \<noteq> 0 \<Longrightarrow> inverse x * x = 1"
- by simp
-
-lemma real_le_mult_order1a:
- "(0::real) \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> x * y"
- by (simp add: zero_le_mult_iff)
-
-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: right_distrib)
- also have "... = - a * x - a * y"
- by simp
- 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: right_distrib)
- also have "... = a * x - a * y"
- by simp
- finally show ?thesis .
-qed
-
-lemma real_minus_le: "- (x::real) \<le> y \<Longrightarrow> - y \<le> x"
- by simp
-
-lemma real_diff_ineq_swap:
- "(d::real) - b \<le> c + a \<Longrightarrow> - a - b \<le> c - d"
- by simp
-
-end
--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy Thu May 06 20:43:30 2004 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy Fri May 07 12:16:57 2004 +0200
@@ -137,7 +137,7 @@
by (rule real_mult_assoc)
also
from gt have "\<parallel>x\<parallel> \<noteq> 0" by simp
- hence "\<parallel>x\<parallel> * inverse \<parallel>x\<parallel> = 1" by (simp add: real_mult_inv_right1)
+ hence "\<parallel>x\<parallel> * inverse \<parallel>x\<parallel> = 1" by simp
also have "c * 1 \<le> b" by (simp add: b_def le_maxI1)
finally show "y \<le> b" .
qed
@@ -199,13 +199,11 @@
then have "\<bar>f x\<bar> = \<bar>f 0\<bar>" by simp
also have "f 0 = 0" ..
also have "\<bar>\<dots>\<bar> = 0" by simp
- also have "\<dots> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
- proof (rule real_le_mult_order1a)
- show "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
+ also have a: "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
by (unfold B_def fn_norm_def)
(rule fn_norm_ge_zero [OF _ continuous.intro])
- show "0 \<le> norm x" ..
- qed
+ have "0 \<le> norm x" ..
+ with a have "0 \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" by (simp add: zero_le_mult_iff)
finally show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" .
next
assume "x \<noteq> 0"
--- a/src/HOL/Real/HahnBanach/HahnBanach.thy Thu May 06 20:43:30 2004 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy Fri May 07 12:16:57 2004 +0200
@@ -355,11 +355,10 @@
fix x y a assume x: "x \<in> E" and y: "y \<in> E"
txt {* @{text p} is positive definite: *}
- show "0 \<le> p x"
- proof (unfold p_def, rule real_le_mult_order1a)
- show "0 \<le> \<parallel>f\<parallel>\<hyphen>F" by (rule ge_zero)
- from x show "0 \<le> \<parallel>x\<parallel>" ..
- qed
+ have "0 \<le> \<parallel>f\<parallel>\<hyphen>F" by (rule ge_zero)
+ moreover from x have "0 \<le> \<parallel>x\<parallel>" ..
+ ultimately show "0 \<le> p x"
+ by (simp add: p_def zero_le_mult_iff)
txt {* @{text p} is absolutely homogenous: *}
@@ -377,11 +376,10 @@
show "p (x + y) \<le> p x + p y"
proof -
have "p (x + y) = \<parallel>f\<parallel>\<hyphen>F * \<parallel>x + y\<parallel>" by (simp only: p_def)
- also have "\<dots> \<le> \<parallel>f\<parallel>\<hyphen>F * (\<parallel>x\<parallel> + \<parallel>y\<parallel>)"
- proof (rule real_mult_le_le_mono1a)
- show "0 \<le> \<parallel>f\<parallel>\<hyphen>F" by (rule ge_zero)
- from x y show "\<parallel>x + y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>" ..
- qed
+ also have a: "0 \<le> \<parallel>f\<parallel>\<hyphen>F" by (rule ge_zero)
+ from x y have "\<parallel>x + y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>" ..
+ with a have " \<parallel>f\<parallel>\<hyphen>F * \<parallel>x + y\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>F * (\<parallel>x\<parallel> + \<parallel>y\<parallel>)"
+ by (simp add: mult_left_mono)
also have "\<dots> = \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel> + \<parallel>f\<parallel>\<hyphen>F * \<parallel>y\<parallel>" by (simp only: right_distrib)
also have "\<dots> = p x + p y" by (simp only: p_def)
finally show ?thesis .
--- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Thu May 06 20:43:30 2004 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Fri May 07 12:16:57 2004 +0200
@@ -5,7 +5,7 @@
header {* Extending non-maximal functions *}
-theory HahnBanachExtLemmas = FunctionNorm:
+theory HahnBanachExtLemmas = FunctionNorm + RealLemmas:
text {*
In this section the following context is presumed. Let @{text E} be
@@ -223,10 +223,11 @@
have "- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y) \<le> xi" ..
with lz have "a * xi \<le>
a * (- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))"
- by (rule real_mult_less_le_anti)
+ by (simp add: mult_left_mono_neg order_less_imp_le)
+
also have "\<dots> =
- a * (p (inverse a \<cdot> y + x0)) - a * (h (inverse a \<cdot> y))"
- by (rule real_mult_diff_distrib)
+ by (rule real_mult_diff_distrib)
also from lz x0 y' have "- a * (p (inverse a \<cdot> y + x0)) =
p (a \<cdot> (inverse a \<cdot> y + x0))"
by (simp add: abs_homogenous abs_minus_eqI2)
@@ -244,9 +245,9 @@
have "xi \<le> p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y)" ..
with gz have "a * xi \<le>
a * (p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))"
- by (rule real_mult_less_le_mono)
+ by simp
also have "... = a * p (inverse a \<cdot> y + x0) - a * h (inverse a \<cdot> y)"
- by (rule real_mult_diff_distrib2)
+ by (rule real_mult_diff_distrib2)
also from gz x0 y'
have "a * p (inverse a \<cdot> y + x0) = p (a \<cdot> (inverse a \<cdot> y + x0))"
by (simp add: abs_homogenous abs_eqI2)
--- a/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy Thu May 06 20:43:30 2004 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy Fri May 07 12:16:57 2004 +0200
@@ -22,6 +22,8 @@
of @{text c}. Every element in @{text H} is member of one of the
elements of the chain.
*}
+lemmas [dest?] = chainD
+lemmas chainE2 [elim?] = chainD2 [elim_format, standard]
lemma some_H'h't:
assumes M: "M = norm_pres_extensions E p F f"
@@ -417,19 +419,17 @@
fix x assume x: "x \<in> H"
show "\<And>a b :: real. - a \<le> b \<Longrightarrow> b \<le> a \<Longrightarrow> \<bar>b\<bar> \<le> a"
by arith
- show "- p x \<le> h x"
- proof (rule real_minus_le)
- have "linearform H h" .
- from this H x have "- h x = h (- x)" by (rule linearform.neg [symmetric])
- also
- from H x have "- x \<in> H" by (rule vectorspace.neg_closed)
- with r have "h (- x) \<le> p (- x)" ..
- also have "\<dots> = p x"
- proof (rule seminorm.minus)
- from x show "x \<in> E" ..
- qed
- finally show "- h x \<le> p x" .
+ have "linearform H h" .
+ from this H x have "- h x = h (- x)" by (rule linearform.neg [symmetric])
+ also
+ from H x have "- x \<in> H" by (rule vectorspace.neg_closed)
+ with r have "h (- x) \<le> p (- x)" ..
+ also have "\<dots> = p x"
+ proof (rule seminorm.minus)
+ from x show "x \<in> E" ..
qed
+ finally have "- h x \<le> p x" .
+ then show "- p x \<le> h x" by simp
from r x show "h x \<le> p x" ..
qed
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Real/HahnBanach/RealLemmas.thy Fri May 07 12:16:57 2004 +0200
@@ -0,0 +1,32 @@
+(* Title: HOL/Real/HahnBanach/RealLemmas.thy
+ ID: $Id$
+ Author: Gertrud Bauer, TU Munich
+*)
+
+header {* Auxiliary theorems *}
+
+theory RealLemmas = Real:
+
+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: right_distrib)
+ also have "... = - a * x - a * y"
+ by simp
+ 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: right_distrib)
+ also have "... = a * x - a * y"
+ by simp
+ finally show ?thesis .
+qed
+
+end
--- a/src/HOL/Real/HahnBanach/VectorSpace.thy Thu May 06 20:43:30 2004 +0200
+++ b/src/HOL/Real/HahnBanach/VectorSpace.thy Fri May 07 12:16:57 2004 +0200
@@ -5,7 +5,9 @@
header {* Vector spaces *}
-theory VectorSpace = Aux:
+(* theory VectorSpace = Aux: *)
+
+theory VectorSpace = Real + Bounds + Zorn:
subsection {* Signature *}
--- a/src/HOL/Real/HahnBanach/ZornLemma.thy Thu May 06 20:43:30 2004 +0200
+++ b/src/HOL/Real/HahnBanach/ZornLemma.thy Fri May 07 12:16:57 2004 +0200
@@ -5,7 +5,7 @@
header {* Zorn's Lemma *}
-theory ZornLemma = Aux + Zorn:
+theory ZornLemma = Zorn:
text {*
Zorn's Lemmas states: if every linear ordered subset of an ordered