author bauerg Fri, 07 May 2004 12:16:57 +0200 changeset 14710 247615bfffb8 parent 14709 d01983034ded child 14711 521aa281808a
replaced Aux.thy by RealLemmas.thy
 src/HOL/Real/HahnBanach/Aux.thy file | annotate | diff | comparison | revisions src/HOL/Real/HahnBanach/FunctionNorm.thy file | annotate | diff | comparison | revisions src/HOL/Real/HahnBanach/HahnBanach.thy file | annotate | diff | comparison | revisions src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy file | annotate | diff | comparison | revisions src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy file | annotate | diff | comparison | revisions src/HOL/Real/HahnBanach/RealLemmas.thy file | annotate | diff | comparison | revisions src/HOL/Real/HahnBanach/VectorSpace.thy file | annotate | diff | comparison | revisions src/HOL/Real/HahnBanach/ZornLemma.thy file | annotate | diff | comparison | revisions
```--- 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"
-
-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"
-
-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"
-
-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>)"
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))"
@@ -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))"
```--- 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
+*)
+
+
+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 @@

-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 @@