src/HOL/Real/HahnBanach/Aux.thy
 author wenzelm Tue Sep 12 22:13:23 2000 +0200 (2000-09-12) changeset 9941 fe05af7ec816 parent 9906 5c027cca6262 child 10606 e3229a37d53f permissions -rw-r--r--
renamed atts: rulify to rule_format, elimify to elim_format;
1 (*  Title:      HOL/Real/HahnBanach/Aux.thy
2     ID:         \$Id\$
3     Author:     Gertrud Bauer, TU Munich
4 *)
6 header {* Auxiliary theorems *}
8 theory Aux = Real + Zorn:
10 text {* Some existing theorems are declared as extra introduction
11 or elimination rules, respectively. *}
13 lemmas [intro?] = isLub_isUb
14 lemmas [intro?] = chainD
15 lemmas chainE2 = chainD2 [elim_format, standard]
17 text_raw {* \medskip *}
18 text{* Lemmas about sets. *}
20 lemma Int_singletonD: "[| A \<inter> B = {v}; x \<in> A; x \<in> B |] ==> x = v"
21   by (fast elim: equalityE)
23 lemma set_less_imp_diff_not_empty: "H < E ==> \<exists>x0 \<in> E. x0 \<notin> H"
24   by (force simp add: psubset_eq)
26 text_raw {* \medskip *}
27 text{* Some lemmas about orders. *}
29 lemma lt_imp_not_eq: "x < (y::'a::order) ==> x \<noteq> y"
32 lemma le_noteq_imp_less:
33   "[| x <= (r::'a::order); x \<noteq> r |] ==> x < r"
34 proof -
35   assume "x <= r" and ne:"x \<noteq> r"
36   hence "x < r | x = r" by (simp add: order_le_less)
37   with ne show ?thesis by simp
38 qed
40 text_raw {* \medskip *}
41 text{* Some lemmas for the reals. *}
43 lemma real_add_minus_eq: "x - y = (#0::real) ==> x = y"
44   by simp
46 lemma abs_minus_one: "abs (- (#1::real)) = #1"
47   by simp
49 lemma real_mult_le_le_mono1a:
50   "[| (#0::real) <= z; x <= y |] ==> z * x  <= z * y"
51 proof -
52   assume z: "(#0::real) <= z" and "x <= y"
53   hence "x < y | x = y" by (force simp add: order_le_less)
54   thus ?thesis
55   proof (elim disjE)
56     assume "x < y" show ?thesis by  (rule real_mult_le_less_mono2) simp
57   next
58     assume "x = y" thus ?thesis by simp
59   qed
60 qed
62 lemma real_mult_le_le_mono2:
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)
69     assume "x < y" show ?thesis by (rule real_mult_le_less_mono1) simp
70   next
71     assume "x = y" thus ?thesis by simp
72   qed
73 qed
75 lemma real_mult_less_le_anti:
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
88 lemma real_mult_less_le_mono:
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
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
106 lemma real_mult_inv_right1: "x \<noteq> #0 ==> x * rinv(x) = #1"
107   by simp
109 lemma real_mult_inv_left1: "x \<noteq> #0 ==> rinv(x) * x = #1"
110   by simp
112 lemma real_le_mult_order1a:
113   "[| (#0::real) <= x; #0 <= y |] ==> #0 <= x * y"
114 proof -
115   assume "#0 <= x" "#0 <= y"
116   have "[|0 <= x; 0 <= y|] ==> 0 <= x * y"
117     by (rule real_le_mult_order)
118   thus ?thesis by (simp!)
119 qed
121 lemma real_mult_diff_distrib:
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"
127   also have "... = - a * x - a * y"
128     by simp
129   finally show ?thesis .
130 qed
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"