author | fleuriot |
Thu, 01 Jun 2000 11:22:27 +0200 | |
changeset 9013 | 9dd0274f76af |
parent 8838 | 4eaa99f0d223 |
child 9035 | 371f023d3dbd |
permissions | -rw-r--r-- |
7566 | 1 |
(* Title: HOL/Real/HahnBanach/Aux.thy |
2 |
ID: $Id$ |
|
3 |
Author: Gertrud Bauer, TU Munich |
|
4 |
*) |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
5 |
|
7808 | 6 |
header {* Auxiliary theorems *}; |
7 |
||
7656 | 8 |
theory Aux = Real + Zorn:; |
7566 | 9 |
|
7917 | 10 |
text {* Some existing theorems are declared as extra introduction |
11 |
or elimination rules, respectively. *}; |
|
12 |
||
8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
7978
diff
changeset
|
13 |
lemmas [intro??] = isLub_isUb; |
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
7978
diff
changeset
|
14 |
lemmas [intro??] = chainD; |
7656 | 15 |
lemmas chainE2 = chainD2 [elimify]; |
7917 | 16 |
|
17 |
text_raw {* \medskip *}; |
|
7978 | 18 |
text{* Lemmas about sets. *}; |
7917 | 19 |
|
20 |
lemma Int_singletonD: "[| A Int B = {v}; x:A; x:B |] ==> x = v"; |
|
21 |
by (fast elim: equalityE); |
|
22 |
||
23 |
lemma set_less_imp_diff_not_empty: "H < E ==> EX x0:E. x0 ~: H"; |
|
24 |
by (force simp add: psubset_eq); |
|
25 |
||
26 |
text_raw {* \medskip *}; |
|
7978 | 27 |
text{* Some lemmas about orders. *}; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
28 |
|
7917 | 29 |
lemma lt_imp_not_eq: "x < (y::'a::order) ==> x ~= y"; |
30 |
by (rule order_less_le[RS iffD1, RS conjunct2]); |
|
31 |
||
32 |
lemma le_noteq_imp_less: |
|
33 |
"[| x <= (r::'a::order); x ~= r |] ==> x < r"; |
|
34 |
proof -; |
|
35 |
assume "x <= (r::'a::order)" and ne:"x ~= r"; |
|
36 |
hence "x < r | x = r"; by (simp add: order_le_less); |
|
37 |
with ne; show ?thesis; by simp; |
|
38 |
qed; |
|
39 |
||
40 |
text_raw {* \medskip *}; |
|
41 |
text {* Some lemmas about linear orders. *}; |
|
7808 | 42 |
|
43 |
theorem linorder_linear_split: |
|
44 |
"[| x < a ==> Q; x = a ==> Q; a < (x::'a::linorder) ==> Q |] ==> Q"; |
|
7917 | 45 |
by (rule linorder_less_linear [of x a, elimify]) force+; |
7566 | 46 |
|
47 |
lemma le_max1: "x <= max x (y::'a::linorder)"; |
|
48 |
by (simp add: le_max_iff_disj[of x x y]); |
|
49 |
||
50 |
lemma le_max2: "y <= max x (y::'a::linorder)"; |
|
51 |
by (simp add: le_max_iff_disj[of y x y]); |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
52 |
|
7917 | 53 |
text_raw {* \medskip *}; |
54 |
text{* Some lemmas for the reals. *}; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
55 |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
56 |
lemma real_add_minus_eq: "x - y = (#0::real) ==> x = y"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
57 |
by simp; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
58 |
|
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
59 |
lemma abs_minus_one: "abs (- (#1::real)) = #1"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
60 |
by simp; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
61 |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
62 |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
63 |
lemma real_mult_le_le_mono1a: |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
64 |
"[| (#0::real) <= z; x <= y |] ==> z * x <= z * y"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
65 |
proof -; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
66 |
assume "(#0::real) <= z" "x <= y"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
67 |
hence "x < y | x = y"; by (force simp add: order_le_less); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
68 |
thus ?thesis; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
69 |
proof (elim disjE); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
70 |
assume "x < y"; show ?thesis; by (rule real_mult_le_less_mono2) simp; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
71 |
next; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
72 |
assume "x = y"; thus ?thesis;; by simp; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
73 |
qed; |
7656 | 74 |
qed; |
75 |
||
7808 | 76 |
lemma real_mult_le_le_mono2: |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
77 |
"[| (#0::real) <= z; x <= y |] ==> x * z <= y * z"; |
7656 | 78 |
proof -; |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
79 |
assume "(#0::real) <= z" "x <= y"; |
7656 | 80 |
hence "x < y | x = y"; by (force simp add: order_le_less); |
81 |
thus ?thesis; |
|
82 |
proof (elim disjE); |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
83 |
assume "x < y"; show ?thesis; by (rule real_mult_le_less_mono1) simp; |
7656 | 84 |
next; |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
85 |
assume "x = y"; thus ?thesis;; by simp; |
7656 | 86 |
qed; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
87 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
88 |
|
7808 | 89 |
lemma real_mult_less_le_anti: |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
90 |
"[| z < (#0::real); x <= y |] ==> z * y <= z * x"; |
7656 | 91 |
proof -; |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
92 |
assume "z < (#0::real)" "x <= y"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
93 |
hence "(#0::real) < - z"; by simp; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
94 |
hence "(#0::real) <= - z"; by (rule real_less_imp_le); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
95 |
hence "x * (- z) <= y * (- z)"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
96 |
by (rule real_mult_le_le_mono2); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
97 |
hence "- (x * z) <= - (y * z)"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
98 |
by (simp only: real_minus_mult_eq2); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
99 |
thus ?thesis; by (simp only: real_mult_commute); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
100 |
qed; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
101 |
|
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
102 |
lemma real_mult_less_le_mono: |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
103 |
"[| (#0::real) < z; x <= y |] ==> z * x <= z * y"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
104 |
proof -; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
105 |
assume "(#0::real) < z" "x <= y"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
106 |
have "(#0::real) <= z"; by (rule real_less_imp_le); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
107 |
hence "x * z <= y * z"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
108 |
by (rule real_mult_le_le_mono2); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
109 |
thus ?thesis; by (simp only: real_mult_commute); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
110 |
qed; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
111 |
|
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
112 |
lemma real_rinv_gt_zero1: "#0 < x ==> #0 < rinv x"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
113 |
proof -; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
114 |
assume "#0 < x"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
115 |
have "0r < x"; by simp; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
116 |
hence "0r < rinv x"; by (rule real_rinv_gt_zero); |
7656 | 117 |
thus ?thesis; by simp; |
118 |
qed; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
119 |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
120 |
lemma real_mult_inv_right1: "x ~= #0 ==> x*rinv(x) = #1"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
121 |
by simp; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
122 |
|
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
123 |
lemma real_mult_inv_left1: "x ~= #0 ==> rinv(x)*x = #1"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
124 |
by simp; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
125 |
|
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
126 |
lemma real_le_mult_order1a: |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
127 |
"[| (#0::real) <= x; #0 <= y |] ==> #0 <= x * y"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
128 |
proof -; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
129 |
assume "#0 <= x" "#0 <= y"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
130 |
have "[|0r <= x; 0r <= y|] ==> 0r <= x * y"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
131 |
by (rule real_le_mult_order); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
132 |
thus ?thesis; by (simp!); |
7656 | 133 |
qed; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
134 |
|
7808 | 135 |
lemma real_mult_diff_distrib: |
136 |
"a * (- x - (y::real)) = - a * x - a * y"; |
|
7656 | 137 |
proof -; |
7808 | 138 |
have "- x - y = - x + - y"; by simp; |
139 |
also; have "a * ... = a * - x + a * - y"; |
|
140 |
by (simp only: real_add_mult_distrib2); |
|
7656 | 141 |
also; have "... = - a * x - a * y"; |
7808 | 142 |
by (simp add: real_minus_mult_eq2 [RS sym] real_minus_mult_eq1); |
7656 | 143 |
finally; show ?thesis; .; |
144 |
qed; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
145 |
|
7656 | 146 |
lemma real_mult_diff_distrib2: "a * (x - (y::real)) = a * x - a * y"; |
147 |
proof -; |
|
7808 | 148 |
have "x - y = x + - y"; by simp; |
149 |
also; have "a * ... = a * x + a * - y"; |
|
150 |
by (simp only: real_add_mult_distrib2); |
|
7656 | 151 |
also; have "... = a * x - a * y"; |
7808 | 152 |
by (simp add: real_minus_mult_eq2 [RS sym] real_minus_mult_eq1); |
7656 | 153 |
finally; show ?thesis; .; |
154 |
qed; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
155 |
|
7808 | 156 |
lemma real_minus_le: "- (x::real) <= y ==> - y <= x"; |
157 |
by simp; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
158 |
|
7808 | 159 |
lemma real_diff_ineq_swap: |
160 |
"(d::real) - b <= c + a ==> - a - b <= c - d"; |
|
161 |
by simp; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
162 |
|
7808 | 163 |
end; |