author | wenzelm |
Thu, 07 Sep 2000 21:10:11 +0200 | |
changeset 9906 | 5c027cca6262 |
parent 9560 | b87a6afe5881 |
child 9941 | fe05af7ec816 |
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 |
|
9035 | 6 |
header {* Auxiliary theorems *} |
7808 | 7 |
|
9035 | 8 |
theory Aux = Real + Zorn: |
7566 | 9 |
|
7917 | 10 |
text {* Some existing theorems are declared as extra introduction |
9035 | 11 |
or elimination rules, respectively. *} |
7917 | 12 |
|
9408 | 13 |
lemmas [intro?] = isLub_isUb |
14 |
lemmas [intro?] = chainD |
|
9906 | 15 |
lemmas chainE2 = chainD2 [elimified] |
7917 | 16 |
|
9035 | 17 |
text_raw {* \medskip *} |
18 |
text{* Lemmas about sets. *} |
|
7917 | 19 |
|
9503 | 20 |
lemma Int_singletonD: "[| A \<inter> B = {v}; x \<in> A; x \<in> B |] ==> x = v" |
9035 | 21 |
by (fast elim: equalityE) |
7917 | 22 |
|
9503 | 23 |
lemma set_less_imp_diff_not_empty: "H < E ==> \<exists>x0 \<in> E. x0 \<notin> H" |
9379 | 24 |
by (force simp add: psubset_eq) |
7917 | 25 |
|
9035 | 26 |
text_raw {* \medskip *} |
27 |
text{* Some lemmas about orders. *} |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
28 |
|
9503 | 29 |
lemma lt_imp_not_eq: "x < (y::'a::order) ==> x \<noteq> y" |
9379 | 30 |
by (simp add: order_less_le) |
7917 | 31 |
|
32 |
lemma le_noteq_imp_less: |
|
9503 | 33 |
"[| x <= (r::'a::order); x \<noteq> r |] ==> x < r" |
9035 | 34 |
proof - |
9503 | 35 |
assume "x <= r" and ne:"x \<noteq> r" |
9035 | 36 |
hence "x < r | x = r" by (simp add: order_le_less) |
37 |
with ne show ?thesis by simp |
|
38 |
qed |
|
7917 | 39 |
|
9035 | 40 |
text_raw {* \medskip *} |
41 |
text{* Some lemmas for the reals. *} |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
42 |
|
9035 | 43 |
lemma real_add_minus_eq: "x - y = (#0::real) ==> x = y" |
44 |
by simp |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
45 |
|
9035 | 46 |
lemma abs_minus_one: "abs (- (#1::real)) = #1" |
47 |
by simp |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
48 |
|
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
49 |
lemma real_mult_le_le_mono1a: |
9035 | 50 |
"[| (#0::real) <= z; x <= y |] ==> z * x <= z * y" |
51 |
proof - |
|
9256 | 52 |
assume z: "(#0::real) <= z" and "x <= y" |
9035 | 53 |
hence "x < y | x = y" by (force simp add: order_le_less) |
54 |
thus ?thesis |
|
55 |
proof (elim disjE) |
|
9394 | 56 |
assume "x < y" show ?thesis by (rule real_mult_le_less_mono2) simp |
9035 | 57 |
next |
9394 | 58 |
assume "x = y" thus ?thesis by simp |
9035 | 59 |
qed |
60 |
qed |
|
7656 | 61 |
|
7808 | 62 |
lemma real_mult_le_le_mono2: |
9035 | 63 |
"[| (#0::real) <= z; x <= y |] ==> x * z <= y * z" |
64 |
proof - |
|
65 |
assume "(#0::real) <= z" "x <= y" |
|
66 |
hence "x < y | x = y" by (force simp add: order_le_less) |
|
67 |
thus ?thesis |
|
68 |
proof (elim disjE) |
|
9394 | 69 |
assume "x < y" show ?thesis by (rule real_mult_le_less_mono1) simp |
9035 | 70 |
next |
9394 | 71 |
assume "x = y" thus ?thesis by simp |
9035 | 72 |
qed |
73 |
qed |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
74 |
|
7808 | 75 |
lemma real_mult_less_le_anti: |
9035 | 76 |
"[| z < (#0::real); x <= y |] ==> z * y <= z * x" |
77 |
proof - |
|
78 |
assume "z < #0" "x <= y" |
|
79 |
hence "#0 < - z" by simp |
|
80 |
hence "#0 <= - z" by (rule real_less_imp_le) |
|
81 |
hence "x * (- z) <= y * (- z)" |
|
82 |
by (rule real_mult_le_le_mono2) |
|
83 |
hence "- (x * z) <= - (y * z)" |
|
84 |
by (simp only: real_minus_mult_eq2) |
|
85 |
thus ?thesis by (simp only: real_mult_commute) |
|
86 |
qed |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
87 |
|
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
88 |
lemma real_mult_less_le_mono: |
9035 | 89 |
"[| (#0::real) < z; x <= y |] ==> z * x <= z * y" |
90 |
proof - |
|
91 |
assume "#0 < z" "x <= y" |
|
92 |
have "#0 <= z" by (rule real_less_imp_le) |
|
93 |
hence "x * z <= y * z" |
|
94 |
by (rule real_mult_le_le_mono2) |
|
95 |
thus ?thesis by (simp only: real_mult_commute) |
|
96 |
qed |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
97 |
|
9394 | 98 |
lemma real_rinv_gt_zero1: "#0 < x ==> #0 < rinv x" |
99 |
proof - |
|
100 |
assume "#0 < x" |
|
101 |
have "0 < x" by simp |
|
102 |
hence "0 < rinv x" by (rule real_rinv_gt_zero) |
|
103 |
thus ?thesis by simp |
|
104 |
qed |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
105 |
|
9560 | 106 |
lemma real_mult_inv_right1: "x \<noteq> #0 ==> x * rinv(x) = #1" |
9394 | 107 |
by simp |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
108 |
|
9503 | 109 |
lemma real_mult_inv_left1: "x \<noteq> #0 ==> rinv(x) * x = #1" |
9394 | 110 |
by simp |
9013
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_le_mult_order1a: |
9394 | 113 |
"[| (#0::real) <= x; #0 <= y |] ==> #0 <= x * y" |
9035 | 114 |
proof - |
115 |
assume "#0 <= x" "#0 <= y" |
|
9394 | 116 |
have "[|0 <= x; 0 <= y|] ==> 0 <= x * y" |
117 |
by (rule real_le_mult_order) |
|
118 |
thus ?thesis by (simp!) |
|
9035 | 119 |
qed |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
120 |
|
7808 | 121 |
lemma real_mult_diff_distrib: |
9035 | 122 |
"a * (- x - (y::real)) = - a * x - a * y" |
123 |
proof - |
|
124 |
have "- x - y = - x + - y" by simp |
|
125 |
also have "a * ... = a * - x + a * - y" |
|
126 |
by (simp only: real_add_mult_distrib2) |
|
127 |
also have "... = - a * x - a * y" |
|
9394 | 128 |
by simp |
9035 | 129 |
finally show ?thesis . |
130 |
qed |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
131 |
|
9035 | 132 |
lemma real_mult_diff_distrib2: "a * (x - (y::real)) = a * x - a * y" |
133 |
proof - |
|
134 |
have "x - y = x + - y" by simp |
|
135 |
also have "a * ... = a * x + a * - y" |
|
136 |
by (simp only: real_add_mult_distrib2) |
|
137 |
also have "... = a * x - a * y" |
|
9394 | 138 |
by simp |
9035 | 139 |
finally show ?thesis . |
140 |
qed |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
141 |
|
9035 | 142 |
lemma real_minus_le: "- (x::real) <= y ==> - y <= x" |
143 |
by simp |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
144 |
|
7808 | 145 |
lemma real_diff_ineq_swap: |
9394 | 146 |
"(d::real) - b <= c + a ==> - a - b <= c - d" |
9035 | 147 |
by simp |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
148 |
|
9035 | 149 |
end |