1.1 --- a/src/HOL/Complex/ROOT.ML Thu Nov 20 10:42:00 2003 +0100
1.2 +++ b/src/HOL/Complex/ROOT.ML Fri Nov 21 11:15:40 2003 +0100
1.3 @@ -5,7 +5,6 @@
1.4 The Complex Numbers
1.5 *)
1.6
1.7 -no_document time_use_thy "Ring_and_Field";
1.8 with_path "../Real" use_thy "Real";
1.9 with_path "../Hyperreal" use_thy "Hyperreal";
1.10 time_use_thy "Complex_Main";
2.1 --- a/src/HOL/Hyperreal/NthRoot.ML Thu Nov 20 10:42:00 2003 +0100
2.2 +++ b/src/HOL/Hyperreal/NthRoot.ML Fri Nov 21 11:15:40 2003 +0100
2.3 @@ -35,14 +35,12 @@
2.4 by (ALLGOALS(rtac ccontr));
2.5 by (ALLGOALS(dtac not_real_leE));
2.6 by (dtac realpow_ge_self2 1 THEN assume_tac 1);
2.7 -by (dres_inst_tac [("n","n")] (conjI
2.8 - RSN (2,conjI RS realpow_less)) 1);
2.9 +by (dres_inst_tac [("n","n")] realpow_less 1);
2.10 by (REPEAT(assume_tac 1));
2.11 by (dtac real_le_trans 1 THEN assume_tac 1);
2.12 by (dres_inst_tac [("y","y ^ n")] order_less_le_trans 1);
2.13 by (assume_tac 1 THEN etac real_less_irrefl 1);
2.14 -by (dres_inst_tac [("n","n")] ((real_zero_less_one) RS (conjI
2.15 - RSN (2,conjI RS realpow_less))) 1);
2.16 +by (dres_inst_tac [("n","n")] ((real_zero_less_one) RS realpow_less) 1);
2.17 by (Auto_tac);
2.18 qed "lemma_nth_realpow_isUb_ex";
2.19
2.20 @@ -164,8 +162,8 @@
2.21 by (auto_tac (claset() addSIs [realpow_pos_nth],simpset()));
2.22 by (cut_inst_tac [("R1.0","r"),("R2.0","y")] real_linear 1);
2.23 by (Auto_tac);
2.24 -by (dres_inst_tac [("x","r")] (conjI RS realpow_less) 1);
2.25 -by (dres_inst_tac [("x","y")] (conjI RS realpow_less) 3);
2.26 +by (dres_inst_tac [("x","r")] realpow_less 1);
2.27 +by (dres_inst_tac [("x","y")] realpow_less 4);
2.28 by (auto_tac (claset(),simpset() addsimps [real_less_not_refl]));
2.29 qed "realpow_pos_nth_unique";
2.30
3.1 --- a/src/HOL/Hyperreal/Transcendental.ML Thu Nov 20 10:42:00 2003 +0100
3.2 +++ b/src/HOL/Hyperreal/Transcendental.ML Fri Nov 21 11:15:40 2003 +0100
3.3 @@ -28,10 +28,8 @@
3.4 by (forw_inst_tac [("n","n")] realpow_gt_zero 2);
3.5 by (auto_tac (claset(),simpset() addsimps [real_0_less_mult_iff]));
3.6 by (res_inst_tac [("R1.0","u"),("R2.0","x")] real_linear_less2 1);
3.7 -by (dres_inst_tac [("n3","n"),("x","u")]
3.8 - (zero_less_Suc RSN (3,conjI RSN (2,conjI RS realpow_less))) 1);
3.9 -by (dres_inst_tac [("n3","n"),("x","x")]
3.10 - (zero_less_Suc RSN (3,conjI RSN (2,conjI RS realpow_less))) 4);
3.11 +by (dres_inst_tac [("n1","n"),("x","u")] (zero_less_Suc RSN (3, realpow_less)) 1);
3.12 +by (dres_inst_tac [("n1","n"),("x","x")] (zero_less_Suc RSN (3, realpow_less)) 4);
3.13 by (auto_tac (claset(),simpset() addsimps [real_less_not_refl]));
3.14 qed "real_root_pos";
3.15
4.1 --- a/src/HOL/IsaMakefile Thu Nov 20 10:42:00 2003 +0100
4.2 +++ b/src/HOL/IsaMakefile Fri Nov 21 11:15:40 2003 +0100
4.3 @@ -96,7 +96,8 @@
4.4 Nat.thy NatArith.ML NatArith.thy Numeral.thy \
4.5 Power.ML Power.thy PreList.thy Product_Type.ML Product_Type.thy ROOT.ML \
4.6 Recdef.thy Record.thy Relation.ML Relation.thy Relation_Power.ML \
4.7 - Relation_Power.thy Set.ML Set.thy SetInterval.ML SetInterval.thy \
4.8 + Relation_Power.thy Ring_and_Field.thy\
4.9 + Set.ML Set.thy SetInterval.ML SetInterval.thy \
4.10 Sum_Type.ML Sum_Type.thy Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML \
4.11 Tools/datatype_codegen.ML Tools/datatype_package.ML Tools/datatype_prop.ML \
4.12 Tools/datatype_realizer.ML Tools/datatype_rep_proofs.ML \
4.13 @@ -144,7 +145,7 @@
4.14 Real/RealArith0.ML Real/RealArith0.thy Real/real_arith0.ML \
4.15 Real/RealArith.thy Real/real_arith.ML Real/RealBin.ML \
4.16 Real/RealBin.thy Real/RealDef.ML Real/RealDef.thy Real/RealInt.ML \
4.17 - Real/RealInt.thy Real/RealOrd.ML Real/RealOrd.thy Real/RealPow.ML \
4.18 + Real/RealInt.thy Real/RealOrd.thy \
4.19 Real/RealPow.thy Real/document/root.tex Real/real_arith.ML\
4.20 Hyperreal/EvenOdd.ML Hyperreal/EvenOdd.thy Hyperreal/ExtraThms2.ML\
4.21 Hyperreal/ExtraThms2.thy Hyperreal/Fact.ML Hyperreal/Fact.thy\
4.22 @@ -198,8 +199,7 @@
4.23 $(LOG)/HOL-Library.gz: $(OUT)/HOL Library/Accessible_Part.thy \
4.24 Library/FuncSet.thy Library/Library.thy \
4.25 Library/List_Prefix.thy Library/Multiset.thy Library/NatPair.thy \
4.26 - Library/Permutation.thy Library/Primes.thy \
4.27 - Library/Quotient.thy Library/Ring_and_Field.thy \
4.28 + Library/Permutation.thy Library/Primes.thy Library/Quotient.thy \
4.29 Library/Ring_and_Field_Example.thy Library/Nat_Infinity.thy \
4.30 Library/README.html Library/Continuity.thy \
4.31 Library/Nested_Environment.thy Library/Rational_Numbers.thy \
5.1 --- a/src/HOL/Library/Ring_and_Field.thy Thu Nov 20 10:42:00 2003 +0100
5.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
5.3 @@ -1,376 +0,0 @@
5.4 -(* Title: HOL/Library/Ring_and_Field.thy
5.5 - ID: $Id$
5.6 - Author: Gertrud Bauer and Markus Wenzel, TU Muenchen
5.7 - License: GPL (GNU GENERAL PUBLIC LICENSE)
5.8 -*)
5.9 -
5.10 -header {*
5.11 - \title{Ring and field structures}
5.12 - \author{Gertrud Bauer and Markus Wenzel}
5.13 -*}
5.14 -
5.15 -theory Ring_and_Field = Main:
5.16 -
5.17 -subsection {* Abstract algebraic structures *}
5.18 -
5.19 -axclass ring \<subseteq> zero, one, plus, minus, times
5.20 - add_assoc: "(a + b) + c = a + (b + c)"
5.21 - add_commute: "a + b = b + a"
5.22 - left_zero [simp]: "0 + a = a"
5.23 - left_minus [simp]: "- a + a = 0"
5.24 - diff_minus: "a - b = a + (-b)"
5.25 -
5.26 - mult_assoc: "(a * b) * c = a * (b * c)"
5.27 - mult_commute: "a * b = b * a"
5.28 - left_one [simp]: "1 * a = a"
5.29 -
5.30 - left_distrib: "(a + b) * c = a * c + b * c"
5.31 -
5.32 -axclass ordered_ring \<subseteq> ring, linorder
5.33 - add_left_mono: "a \<le> b ==> c + a \<le> c + b"
5.34 - mult_strict_left_mono: "a < b ==> 0 < c ==> c * a < c * b"
5.35 - abs_if: "\<bar>a\<bar> = (if a < 0 then -a else a)"
5.36 -
5.37 -axclass field \<subseteq> ring, inverse
5.38 - left_inverse [simp]: "a \<noteq> 0 ==> inverse a * a = 1"
5.39 - divide_inverse: "b \<noteq> 0 ==> a / b = a * inverse b"
5.40 - zero_neq_one [simp]: "0 \<noteq> 1"
5.41 -
5.42 -axclass ordered_field \<subseteq> ordered_ring, field
5.43 -
5.44 -axclass division_by_zero \<subseteq> zero, inverse
5.45 - inverse_zero: "inverse 0 = 0"
5.46 - divide_zero: "a / 0 = 0"
5.47 -
5.48 -
5.49 -
5.50 -subsection {* Derived rules for addition *}
5.51 -
5.52 -lemma right_zero [simp]: "a + 0 = (a::'a::ring)"
5.53 -proof -
5.54 - have "a + 0 = 0 + a" by (simp only: add_commute)
5.55 - also have "... = a" by simp
5.56 - finally show ?thesis .
5.57 -qed
5.58 -
5.59 -lemma add_left_commute: "a + (b + c) = b + (a + (c::'a::ring))"
5.60 - by (rule mk_left_commute [of "op +", OF add_assoc add_commute])
5.61 -
5.62 -theorems ring_add_ac = add_assoc add_commute add_left_commute
5.63 -
5.64 -lemma right_minus [simp]: "a + -(a::'a::ring) = 0"
5.65 -proof -
5.66 - have "a + -a = -a + a" by (simp add: ring_add_ac)
5.67 - also have "... = 0" by simp
5.68 - finally show ?thesis .
5.69 -qed
5.70 -
5.71 -lemma right_minus_eq: "(a - b = 0) = (a = (b::'a::ring))"
5.72 -proof
5.73 - have "a = a - b + b" by (simp add: diff_minus ring_add_ac)
5.74 - also assume "a - b = 0"
5.75 - finally show "a = b" by simp
5.76 -next
5.77 - assume "a = b"
5.78 - thus "a - b = 0" by (simp add: diff_minus)
5.79 -qed
5.80 -
5.81 -lemma diff_self [simp]: "a - (a::'a::ring) = 0"
5.82 - by (simp add: diff_minus)
5.83 -
5.84 -lemma add_left_cancel [simp]:
5.85 - "(a + b = a + c) = (b = (c::'a::ring))"
5.86 -proof
5.87 - assume eq: "a + b = a + c"
5.88 - then have "(-a + a) + b = (-a + a) + c"
5.89 - by (simp only: eq add_assoc)
5.90 - then show "b = c" by simp
5.91 -next
5.92 - assume eq: "b = c"
5.93 - then show "a + b = a + c" by simp
5.94 -qed
5.95 -
5.96 -lemma add_right_cancel [simp]:
5.97 - "(b + a = c + a) = (b = (c::'a::ring))"
5.98 - by (simp add: add_commute)
5.99 -
5.100 -lemma minus_minus [simp]: "- (- (a::'a::ring)) = a"
5.101 - proof (rule add_left_cancel [of "-a", THEN iffD1])
5.102 - show "(-a + -(-a) = -a + a)"
5.103 - by simp
5.104 - qed
5.105 -
5.106 -lemma equals_zero_I: "a+b = 0 ==> -a = (b::'a::ring)"
5.107 -apply (rule right_minus_eq [THEN iffD1, symmetric])
5.108 -apply (simp add: diff_minus add_commute)
5.109 -done
5.110 -
5.111 -lemma minus_zero [simp]: "- 0 = (0::'a::ring)"
5.112 -by (simp add: equals_zero_I)
5.113 -
5.114 -lemma neg_equal_iff_equal [simp]: "(-a = -b) = (a = (b::'a::ring))"
5.115 - proof
5.116 - assume "- a = - b"
5.117 - then have "- (- a) = - (- b)"
5.118 - by simp
5.119 - then show "a=b"
5.120 - by simp
5.121 - next
5.122 - assume "a=b"
5.123 - then show "-a = -b"
5.124 - by simp
5.125 - qed
5.126 -
5.127 -lemma neg_equal_0_iff_equal [simp]: "(-a = 0) = (a = (0::'a::ring))"
5.128 -by (subst neg_equal_iff_equal [symmetric], simp)
5.129 -
5.130 -lemma neg_0_equal_iff_equal [simp]: "(0 = -a) = (0 = (a::'a::ring))"
5.131 -by (subst neg_equal_iff_equal [symmetric], simp)
5.132 -
5.133 -
5.134 -subsection {* Derived rules for multiplication *}
5.135 -
5.136 -lemma right_one [simp]: "a = a * (1::'a::field)"
5.137 -proof -
5.138 - have "a = 1 * a" by simp
5.139 - also have "... = a * 1" by (simp add: mult_commute)
5.140 - finally show ?thesis .
5.141 -qed
5.142 -
5.143 -lemma mult_left_commute: "a * (b * c) = b * (a * (c::'a::ring))"
5.144 - by (rule mk_left_commute [of "op *", OF mult_assoc mult_commute])
5.145 -
5.146 -theorems ring_mult_ac = mult_assoc mult_commute mult_left_commute
5.147 -
5.148 -lemma right_inverse [simp]: "a \<noteq> 0 ==> a * inverse (a::'a::field) = 1"
5.149 -proof -
5.150 - have "a * inverse a = inverse a * a" by (simp add: ring_mult_ac)
5.151 - also assume "a \<noteq> 0"
5.152 - hence "inverse a * a = 1" by simp
5.153 - finally show ?thesis .
5.154 -qed
5.155 -
5.156 -lemma right_inverse_eq: "b \<noteq> 0 ==> (a / b = 1) = (a = (b::'a::field))"
5.157 -proof
5.158 - assume neq: "b \<noteq> 0"
5.159 - {
5.160 - hence "a = (a / b) * b" by (simp add: divide_inverse ring_mult_ac)
5.161 - also assume "a / b = 1"
5.162 - finally show "a = b" by simp
5.163 - next
5.164 - assume "a = b"
5.165 - with neq show "a / b = 1" by (simp add: divide_inverse)
5.166 - }
5.167 -qed
5.168 -
5.169 -lemma divide_self [simp]: "a \<noteq> 0 ==> a / (a::'a::field) = 1"
5.170 - by (simp add: divide_inverse)
5.171 -
5.172 -lemma mult_left_zero [simp]:
5.173 - "0 * a = (0::'a::ring)"
5.174 -proof -
5.175 - have "0*a + 0*a = 0*a + 0"
5.176 - by (simp add: left_distrib [symmetric])
5.177 - then show ?thesis by (simp only: add_left_cancel)
5.178 -qed
5.179 -
5.180 -lemma mult_right_zero [simp]:
5.181 - "a * 0 = (0::'a::ring)"
5.182 - by (simp add: mult_commute)
5.183 -
5.184 -
5.185 -subsection {* Distribution rules *}
5.186 -
5.187 -lemma right_distrib: "a * (b + c) = a * b + a * (c::'a::ring)"
5.188 -proof -
5.189 - have "a * (b + c) = (b + c) * a" by (simp add: ring_mult_ac)
5.190 - also have "... = b * a + c * a" by (simp only: left_distrib)
5.191 - also have "... = a * b + a * c" by (simp add: ring_mult_ac)
5.192 - finally show ?thesis .
5.193 -qed
5.194 -
5.195 -theorems ring_distrib = right_distrib left_distrib
5.196 -
5.197 -lemma minus_add_distrib [simp]: "- (a + b) = -a + -(b::'a::ring)"
5.198 -apply (rule equals_zero_I)
5.199 -apply (simp add: ring_add_ac)
5.200 -done
5.201 -
5.202 -lemma minus_mult_left: "- (a * b) = (-a) * (b::'a::ring)"
5.203 -apply (rule equals_zero_I)
5.204 -apply (simp add: left_distrib [symmetric])
5.205 -done
5.206 -
5.207 -lemma minus_mult_right: "- (a * b) = a * -(b::'a::ring)"
5.208 -apply (rule equals_zero_I)
5.209 -apply (simp add: right_distrib [symmetric])
5.210 -done
5.211 -
5.212 -lemma right_diff_distrib: "a * (b - c) = a * b - a * (c::'a::ring)"
5.213 -by (simp add: right_distrib diff_minus
5.214 - minus_mult_left [symmetric] minus_mult_right [symmetric])
5.215 -
5.216 -
5.217 -subsection {* Ordering rules *}
5.218 -
5.219 -lemma add_right_mono: "a \<le> (b::'a::ordered_ring) ==> a + c \<le> b + c"
5.220 -by (simp add: add_commute [of _ c] add_left_mono)
5.221 -
5.222 -lemma le_imp_neg_le: "a \<le> (b::'a::ordered_ring) ==> -b \<le> -a"
5.223 - proof -
5.224 - assume "a\<le>b"
5.225 - then have "-a+a \<le> -a+b"
5.226 - by (rule add_left_mono)
5.227 - then have "0 \<le> -a+b"
5.228 - by simp
5.229 - then have "0 + (-b) \<le> (-a + b) + (-b)"
5.230 - by (rule add_right_mono)
5.231 - then show ?thesis
5.232 - by (simp add: add_assoc)
5.233 - qed
5.234 -
5.235 -lemma neg_le_iff_le [simp]: "(-b \<le> -a) = (a \<le> (b::'a::ordered_ring))"
5.236 - proof
5.237 - assume "- b \<le> - a"
5.238 - then have "- (- a) \<le> - (- b)"
5.239 - by (rule le_imp_neg_le)
5.240 - then show "a\<le>b"
5.241 - by simp
5.242 - next
5.243 - assume "a\<le>b"
5.244 - then show "-b \<le> -a"
5.245 - by (rule le_imp_neg_le)
5.246 - qed
5.247 -
5.248 -lemma neg_le_0_iff_le [simp]: "(-a \<le> 0) = (0 \<le> (a::'a::ordered_ring))"
5.249 -by (subst neg_le_iff_le [symmetric], simp)
5.250 -
5.251 -lemma neg_0_le_iff_le [simp]: "(0 \<le> -a) = (a \<le> (0::'a::ordered_ring))"
5.252 -by (subst neg_le_iff_le [symmetric], simp)
5.253 -
5.254 -lemma neg_less_iff_less [simp]: "(-b < -a) = (a < (b::'a::ordered_ring))"
5.255 -by (force simp add: order_less_le)
5.256 -
5.257 -lemma neg_less_0_iff_less [simp]: "(-a < 0) = (0 < (a::'a::ordered_ring))"
5.258 -by (subst neg_less_iff_less [symmetric], simp)
5.259 -
5.260 -lemma neg_0_less_iff_less [simp]: "(0 < -a) = (a < (0::'a::ordered_ring))"
5.261 -by (subst neg_less_iff_less [symmetric], simp)
5.262 -
5.263 -lemma mult_strict_right_mono:
5.264 - "[|a < b; 0 < c|] ==> a * c < b * (c::'a::ordered_ring)"
5.265 -by (simp add: mult_commute [of _ c] mult_strict_left_mono)
5.266 -
5.267 -lemma mult_left_mono: "[|a \<le> b; 0 < c|] ==> c * a \<le> c * (b::'a::ordered_ring)"
5.268 -by (force simp add: mult_strict_left_mono order_le_less)
5.269 -
5.270 -lemma mult_right_mono: "[|a \<le> b; 0 < c|] ==> a*c \<le> b * (c::'a::ordered_ring)"
5.271 -by (force simp add: mult_strict_right_mono order_le_less)
5.272 -
5.273 -lemma mult_strict_left_mono_neg:
5.274 - "[|b < a; c < 0|] ==> c * a < c * (b::'a::ordered_ring)"
5.275 -apply (drule mult_strict_left_mono [of _ _ "-c"])
5.276 -apply (simp_all add: minus_mult_left [symmetric])
5.277 -done
5.278 -
5.279 -lemma mult_strict_right_mono_neg:
5.280 - "[|b < a; c < 0|] ==> a * c < b * (c::'a::ordered_ring)"
5.281 -apply (drule mult_strict_right_mono [of _ _ "-c"])
5.282 -apply (simp_all add: minus_mult_right [symmetric])
5.283 -done
5.284 -
5.285 -lemma mult_left_mono_neg:
5.286 - "[|b \<le> a; c < 0|] ==> c * a \<le> c * (b::'a::ordered_ring)"
5.287 -by (force simp add: mult_strict_left_mono_neg order_le_less)
5.288 -
5.289 -lemma mult_right_mono_neg:
5.290 - "[|b \<le> a; c < 0|] ==> a * c \<le> b * (c::'a::ordered_ring)"
5.291 -by (force simp add: mult_strict_right_mono_neg order_le_less)
5.292 -
5.293 -
5.294 -subsection{* Products of Signs *}
5.295 -
5.296 -lemma mult_pos: "[| (0::'a::ordered_ring) < a; 0 < b |] ==> 0 < a*b"
5.297 -by (drule mult_strict_left_mono [of 0 b], auto)
5.298 -
5.299 -lemma mult_pos_neg: "[| (0::'a::ordered_ring) < a; b < 0 |] ==> a*b < 0"
5.300 -by (drule mult_strict_left_mono [of b 0], auto)
5.301 -
5.302 -lemma mult_neg: "[| a < (0::'a::ordered_ring); b < 0 |] ==> 0 < a*b"
5.303 -by (drule mult_strict_right_mono_neg, auto)
5.304 -
5.305 -lemma zero_less_mult_pos: "[| 0 < a*b; 0 < a|] ==> 0 < (b::'a::ordered_ring)"
5.306 -apply (case_tac "b\<le>0")
5.307 - apply (auto simp add: order_le_less linorder_not_less)
5.308 -apply (drule_tac mult_pos_neg [of a b])
5.309 - apply (auto dest: order_less_not_sym)
5.310 -done
5.311 -
5.312 -lemma zero_less_mult_iff:
5.313 - "((0::'a::ordered_ring) < a*b) = (0 < a & 0 < b | a < 0 & b < 0)"
5.314 -apply (auto simp add: order_le_less linorder_not_less mult_pos mult_neg)
5.315 -apply (blast dest: zero_less_mult_pos)
5.316 -apply (simp add: mult_commute [of a b])
5.317 -apply (blast dest: zero_less_mult_pos)
5.318 -done
5.319 -
5.320 -
5.321 -lemma mult_eq_0_iff [iff]: "(a*b = (0::'a::ordered_ring)) = (a = 0 | b = 0)"
5.322 -apply (case_tac "a < 0")
5.323 -apply (auto simp add: linorder_not_less order_le_less linorder_neq_iff)
5.324 -apply (force dest: mult_strict_right_mono_neg mult_strict_right_mono)+
5.325 -done
5.326 -
5.327 -lemma zero_le_mult_iff:
5.328 - "((0::'a::ordered_ring) \<le> a*b) = (0 \<le> a & 0 \<le> b | a \<le> 0 & b \<le> 0)"
5.329 -by (auto simp add: order_le_less linorder_not_less zero_less_mult_iff)
5.330 -
5.331 -lemma mult_less_0_iff:
5.332 - "(a*b < (0::'a::ordered_ring)) = (0 < a & b < 0 | a < 0 & 0 < b)"
5.333 -apply (insert zero_less_mult_iff [of "-a" b])
5.334 -apply (force simp add: minus_mult_left[symmetric])
5.335 -done
5.336 -
5.337 -lemma mult_le_0_iff:
5.338 - "(a*b \<le> (0::'a::ordered_ring)) = (0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)"
5.339 -apply (insert zero_le_mult_iff [of "-a" b])
5.340 -apply (force simp add: minus_mult_left[symmetric])
5.341 -done
5.342 -
5.343 -lemma zero_le_square: "(0::'a::ordered_ring) \<le> a*a"
5.344 -by (simp add: zero_le_mult_iff linorder_linear)
5.345 -
5.346 -
5.347 -subsection {* Absolute Value *}
5.348 -
5.349 -text{*But is it really better than just rewriting with @{text abs_if}?*}
5.350 -lemma abs_split:
5.351 - "P(abs(a::'a::ordered_ring)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
5.352 -by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
5.353 -
5.354 -lemma abs_zero [simp]: "abs 0 = (0::'a::ordered_ring)"
5.355 -by (simp add: abs_if)
5.356 -
5.357 -lemma abs_mult: "abs (x * y) = abs x * abs (y::'a::ordered_ring)"
5.358 -apply (case_tac "x=0 | y=0", force)
5.359 -apply (auto elim: order_less_asym
5.360 - simp add: abs_if mult_less_0_iff linorder_neq_iff
5.361 - minus_mult_left [symmetric] minus_mult_right [symmetric])
5.362 -done
5.363 -
5.364 -lemma abs_eq_0 [iff]: "(abs x = 0) = (x = (0::'a::ordered_ring))"
5.365 -by (simp add: abs_if)
5.366 -
5.367 -lemma zero_less_abs_iff [iff]: "(0 < abs x) = (x ~= (0::'a::ordered_ring))"
5.368 -by (simp add: abs_if linorder_neq_iff)
5.369 -
5.370 -
5.371 -subsection {* Fields *}
5.372 -
5.373 -lemma zero_less_one: "(0::'a::ordered_field) < 1"
5.374 -apply (insert zero_le_square [of 1])
5.375 -apply (simp add: order_less_le)
5.376 -done
5.377 -
5.378 -
5.379 -end
6.1 --- a/src/HOL/Library/Ring_and_Field_Example.thy Thu Nov 20 10:42:00 2003 +0100
6.2 +++ b/src/HOL/Library/Ring_and_Field_Example.thy Fri Nov 21 11:15:40 2003 +0100
6.3 @@ -1,8 +1,9 @@
6.4
6.5 header {* \title{}\subsection{Example: The ordered ring of integers} *}
6.6
6.7 -theory Ring_and_Field_Example = Ring_and_Field:
6.8 +theory Ring_and_Field_Example = Main:
6.9
6.10 +text{*The Integers Form an Ordered Ring*}
6.11 instance int :: ordered_ring
6.12 proof
6.13 fix i j k :: int
6.14 @@ -15,6 +16,7 @@
6.15 show "i * j = j * i" by simp
6.16 show "1 * i = i" by simp
6.17 show "(i + j) * k = i * k + j * k" by (simp add: int_distrib)
6.18 + show "0 \<noteq> (1::int)" by simp
6.19 show "i \<le> j ==> k + i \<le> k + j" by simp
6.20 show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: zmult_zless_mono2)
6.21 show "\<bar>i\<bar> = (if i < 0 then -i else i)" by (simp only: zabs_def)
7.1 --- a/src/HOL/MicroJava/BV/Product.thy Thu Nov 20 10:42:00 2003 +0100
7.2 +++ b/src/HOL/MicroJava/BV/Product.thy Fri Nov 21 11:15:40 2003 +0100
7.3 @@ -44,7 +44,7 @@
7.4 "order(Product.le rA rB) = (order rA & order rB)"
7.5 apply (unfold order_def)
7.6 apply simp
7.7 -apply blast
7.8 +apply meson
7.9 done
7.10
7.11
8.1 --- a/src/HOL/Nat.thy Thu Nov 20 10:42:00 2003 +0100
8.2 +++ b/src/HOL/Nat.thy Fri Nov 21 11:15:40 2003 +0100
8.3 @@ -8,7 +8,7 @@
8.4
8.5 header {* Natural numbers *}
8.6
8.7 -theory Nat = Wellfounded_Recursion:
8.8 +theory Nat = Wellfounded_Recursion + Ring_and_Field:
8.9
8.10 subsection {* Type @{text ind} *}
8.11
8.12 @@ -584,6 +584,7 @@
8.13 done
8.14
8.15
8.16 +
8.17 subsection {* @{term min} and @{term max} *}
8.18
8.19 lemma min_0L [simp]: "min 0 n = (0::nat)"
8.20 @@ -833,6 +834,30 @@
8.21 apply (induct_tac [2] n, simp_all)
8.22 done
8.23
8.24 +text {* strict, in 1st argument; proof is by induction on @{text "k > 0"} *}
8.25 +lemma mult_less_mono2: "(i::nat) < j ==> 0 < k ==> k * i < k * j"
8.26 + apply (erule_tac m1 = 0 in less_imp_Suc_add [THEN exE], simp)
8.27 + apply (induct_tac x)
8.28 + apply (simp_all add: add_less_mono)
8.29 + done
8.30 +
8.31 +text{*The Naturals Form an Ordered Semiring*}
8.32 +instance nat :: ordered_semiring
8.33 +proof
8.34 + fix i j k :: nat
8.35 + show "(i + j) + k = i + (j + k)" by (rule add_assoc)
8.36 + show "i + j = j + i" by (rule add_commute)
8.37 + show "0 + i = i" by simp
8.38 + show "(i * j) * k = i * (j * k)" by (rule mult_assoc)
8.39 + show "i * j = j * i" by (rule mult_commute)
8.40 + show "1 * i = i" by simp
8.41 + show "(i + j) * k = i * k + j * k" by (simp add: add_mult_distrib)
8.42 + show "0 \<noteq> (1::nat)" by simp
8.43 + show "i \<le> j ==> k + i \<le> k + j" by simp
8.44 + show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: mult_less_mono2)
8.45 +qed
8.46 +
8.47 +
8.48
8.49 subsection {* Difference *}
8.50
8.51 @@ -964,13 +989,6 @@
8.52 apply (erule mult_le_mono2)
8.53 done
8.54
8.55 -text {* strict, in 1st argument; proof is by induction on @{text "k > 0"} *}
8.56 -lemma mult_less_mono2: "(i::nat) < j ==> 0 < k ==> k * i < k * j"
8.57 - apply (erule_tac m1 = 0 in less_imp_Suc_add [THEN exE], simp)
8.58 - apply (induct_tac x)
8.59 - apply (simp_all add: add_less_mono)
8.60 - done
8.61 -
8.62 lemma mult_less_mono1: "(i::nat) < j ==> 0 < k ==> i * k < j * k"
8.63 by (drule mult_less_mono2) (simp_all add: mult_commute)
8.64
8.65 @@ -1041,4 +1059,5 @@
8.66 apply (fastsimp dest: mult_less_mono2)
8.67 done
8.68
8.69 +
8.70 end
9.1 --- a/src/HOL/Real/Complex_Numbers.thy Thu Nov 20 10:42:00 2003 +0100
9.2 +++ b/src/HOL/Real/Complex_Numbers.thy Fri Nov 21 11:15:40 2003 +0100
9.3 @@ -8,29 +8,6 @@
9.4
9.5 theory Complex_Numbers = RealPow + Ring_and_Field:
9.6
9.7 -subsection {* The field of real numbers *} (* FIXME move *)
9.8 -
9.9 -instance real :: field
9.10 - by intro_classes (simp_all add: real_add_mult_distrib real_divide_def)
9.11 -
9.12 -lemma real_power_two: "(r::real)\<twosuperior> = r * r"
9.13 - by (simp add: numeral_2_eq_2)
9.14 -
9.15 -lemma real_sqr_ge_zero [iff]: "0 \<le> (r::real)\<twosuperior>"
9.16 - by (simp add: real_power_two)
9.17 -
9.18 -lemma real_sqr_gt_zero: "(r::real) \<noteq> 0 ==> 0 < r\<twosuperior>"
9.19 -proof -
9.20 - assume "r \<noteq> 0"
9.21 - hence "0 \<noteq> r\<twosuperior>" by simp
9.22 - also have "0 \<le> r\<twosuperior>" by (simp add: real_sqr_ge_zero)
9.23 - finally show ?thesis .
9.24 -qed
9.25 -
9.26 -lemma real_sqr_not_zero: "r \<noteq> 0 ==> (r::real)\<twosuperior> \<noteq> 0"
9.27 - by simp
9.28 -
9.29 -
9.30 subsection {* Representation of complex numbers *}
9.31
9.32 datatype complex = Complex real real
9.33 @@ -121,7 +98,7 @@
9.34 show "z - w = z + -w"
9.35 by (simp add: add_complex_def minus_complex_def uminus_complex_def)
9.36 show "(u * v) * w = u * (v * w)"
9.37 - by (simp add: mult_complex_def ring_mult_ac ring_distrib real_diff_def) (* FIXME *)
9.38 + by (simp add: mult_complex_def mult_ac ring_distrib real_diff_def) (* FIXME *)
9.39 show "z * w = w * z"
9.40 by (simp add: mult_complex_def)
9.41 show "1 * z = z"
10.1 --- a/src/HOL/Real/ROOT.ML Thu Nov 20 10:42:00 2003 +0100
10.2 +++ b/src/HOL/Real/ROOT.ML Fri Nov 21 11:15:40 2003 +0100
10.3 @@ -7,5 +7,4 @@
10.4 by Jacques Fleuriot
10.5 *)
10.6
10.7 -no_document time_use_thy "Ring_and_Field";
10.8 time_use_thy "Real";
11.1 --- a/src/HOL/Real/RealAbs.thy Thu Nov 20 10:42:00 2003 +0100
11.2 +++ b/src/HOL/Real/RealAbs.thy Fri Nov 21 11:15:40 2003 +0100
11.3 @@ -5,10 +5,4 @@
11.4 Description : Absolute value function for the reals
11.5 *)
11.6
11.7 -RealAbs = RealArith +
11.8 -
11.9 -
11.10 -defs
11.11 - real_abs_def "abs r == (if (0::real) <= r then r else -r)"
11.12 -
11.13 -end
11.14 +RealAbs = RealArith
12.1 --- a/src/HOL/Real/RealOrd.ML Thu Nov 20 10:42:00 2003 +0100
12.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
12.3 @@ -1,587 +0,0 @@
12.4 -(* Title: HOL/Real/Real.ML
12.5 - ID: $Id$
12.6 - Author: Jacques D. Fleuriot and Lawrence C. Paulson
12.7 - Copyright: 1998 University of Cambridge
12.8 - Description: Type "real" is a linear order
12.9 -*)
12.10 -
12.11 -(**** The simproc abel_cancel ****)
12.12 -
12.13 -(*** Two lemmas needed for the simprocs ***)
12.14 -
12.15 -(*Deletion of other terms in the formula, seeking the -x at the front of z*)
12.16 -Goal "((x::real) + (y + z) = y + u) = ((x + z) = u)";
12.17 -by (stac real_add_left_commute 1);
12.18 -by (rtac real_add_left_cancel 1);
12.19 -qed "real_add_cancel_21";
12.20 -
12.21 -(*A further rule to deal with the case that
12.22 - everything gets cancelled on the right.*)
12.23 -Goal "((x::real) + (y + z) = y) = (x = -z)";
12.24 -by (stac real_add_left_commute 1);
12.25 -by (res_inst_tac [("t", "y")] (real_add_zero_right RS subst) 1
12.26 - THEN stac real_add_left_cancel 1);
12.27 -by (simp_tac (simpset() addsimps [real_eq_diff_eq RS sym]) 1);
12.28 -qed "real_add_cancel_end";
12.29 -
12.30 -
12.31 -structure Real_Cancel_Data =
12.32 -struct
12.33 - val ss = HOL_ss
12.34 - val eq_reflection = eq_reflection
12.35 -
12.36 - val sg_ref = Sign.self_ref (Theory.sign_of (the_context ()))
12.37 - val T = HOLogic.realT
12.38 - val zero = Const ("0", T)
12.39 - val restrict_to_left = restrict_to_left
12.40 - val add_cancel_21 = real_add_cancel_21
12.41 - val add_cancel_end = real_add_cancel_end
12.42 - val add_left_cancel = real_add_left_cancel
12.43 - val add_assoc = real_add_assoc
12.44 - val add_commute = real_add_commute
12.45 - val add_left_commute = real_add_left_commute
12.46 - val add_0 = real_add_zero_left
12.47 - val add_0_right = real_add_zero_right
12.48 -
12.49 - val eq_diff_eq = real_eq_diff_eq
12.50 - val eqI_rules = [real_less_eqI, real_eq_eqI, real_le_eqI]
12.51 - fun dest_eqI th =
12.52 - #1 (HOLogic.dest_bin "op =" HOLogic.boolT
12.53 - (HOLogic.dest_Trueprop (concl_of th)))
12.54 -
12.55 - val diff_def = real_diff_def
12.56 - val minus_add_distrib = real_minus_add_distrib
12.57 - val minus_minus = real_minus_minus
12.58 - val minus_0 = real_minus_zero
12.59 - val add_inverses = [real_add_minus, real_add_minus_left]
12.60 - val cancel_simps = [real_add_minus_cancel, real_minus_add_cancel]
12.61 -end;
12.62 -
12.63 -structure Real_Cancel = Abel_Cancel (Real_Cancel_Data);
12.64 -
12.65 -Addsimprocs [Real_Cancel.sum_conv, Real_Cancel.rel_conv];
12.66 -
12.67 -Goal "- (z - y) = y - (z::real)";
12.68 -by (Simp_tac 1);
12.69 -qed "real_minus_diff_eq";
12.70 -Addsimps [real_minus_diff_eq];
12.71 -
12.72 -
12.73 -(**** Theorems about the ordering ****)
12.74 -
12.75 -Goal "(0 < x) = (EX y. x = real_of_preal y)";
12.76 -by (auto_tac (claset(), simpset() addsimps [real_of_preal_zero_less]));
12.77 -by (cut_inst_tac [("x","x")] real_of_preal_trichotomy 1);
12.78 -by (blast_tac (claset() addSEs [real_less_irrefl,
12.79 - real_of_preal_not_minus_gt_zero RS notE]) 1);
12.80 -qed "real_gt_zero_preal_Ex";
12.81 -
12.82 -Goal "real_of_preal z < x ==> EX y. x = real_of_preal y";
12.83 -by (blast_tac (claset() addSDs [real_of_preal_zero_less RS real_less_trans]
12.84 - addIs [real_gt_zero_preal_Ex RS iffD1]) 1);
12.85 -qed "real_gt_preal_preal_Ex";
12.86 -
12.87 -Goal "real_of_preal z <= x ==> EX y. x = real_of_preal y";
12.88 -by (blast_tac (claset() addDs [order_le_imp_less_or_eq,
12.89 - real_gt_preal_preal_Ex]) 1);
12.90 -qed "real_ge_preal_preal_Ex";
12.91 -
12.92 -Goal "y <= 0 ==> ALL x. y < real_of_preal x";
12.93 -by (auto_tac (claset() addEs [order_le_imp_less_or_eq RS disjE]
12.94 - addIs [real_of_preal_zero_less RSN(2,real_less_trans)],
12.95 - simpset() addsimps [real_of_preal_zero_less]));
12.96 -qed "real_less_all_preal";
12.97 -
12.98 -Goal "~ 0 < y ==> ALL x. y < real_of_preal x";
12.99 -by (blast_tac (claset() addSIs [real_less_all_preal,real_leI]) 1);
12.100 -qed "real_less_all_real2";
12.101 -
12.102 -Goal "[| R + L = S; (0::real) < L |] ==> R < S";
12.103 -by (rtac (real_less_sum_gt_0_iff RS iffD1) 1);
12.104 -by (auto_tac (claset(), simpset() addsimps real_add_ac));
12.105 -qed "real_lemma_add_positive_imp_less";
12.106 -
12.107 -Goal "EX T::real. 0 < T & R + T = S ==> R < S";
12.108 -by (blast_tac (claset() addIs [real_lemma_add_positive_imp_less]) 1);
12.109 -qed "real_ex_add_positive_left_less";
12.110 -
12.111 -(*Alternative definition for real_less. NOT for rewriting*)
12.112 -Goal "(R < S) = (EX T::real. 0 < T & R + T = S)";
12.113 -by (blast_tac (claset() addSIs [real_less_add_positive_left_Ex,
12.114 - real_ex_add_positive_left_less]) 1);
12.115 -qed "real_less_iff_add";
12.116 -
12.117 -Goal "(real_of_preal m1 <= real_of_preal m2) = (m1 <= m2)";
12.118 -by (auto_tac (claset() addSIs [preal_leI],
12.119 - simpset() addsimps [real_less_le_iff RS sym]));
12.120 -by (dtac order_le_less_trans 1 THEN assume_tac 1);
12.121 -by (etac preal_less_irrefl 1);
12.122 -qed "real_of_preal_le_iff";
12.123 -
12.124 -Goal "[| 0 < x; 0 < y |] ==> (0::real) < x * y";
12.125 -by (auto_tac (claset(), simpset() addsimps [real_gt_zero_preal_Ex]));
12.126 -by (res_inst_tac [("x","y*ya")] exI 1);
12.127 -by (full_simp_tac (simpset() addsimps [real_of_preal_mult]) 1);
12.128 -qed "real_mult_order";
12.129 -
12.130 -Goal "[| x < 0; y < 0 |] ==> (0::real) < x * y";
12.131 -by (REPEAT(dtac (real_minus_zero_less_iff RS iffD2) 1));
12.132 -by (dtac real_mult_order 1 THEN assume_tac 1);
12.133 -by (Asm_full_simp_tac 1);
12.134 -qed "neg_real_mult_order";
12.135 -
12.136 -Goal "[| 0 < x; y < 0 |] ==> x*y < (0::real)";
12.137 -by (dtac (real_minus_zero_less_iff RS iffD2) 1);
12.138 -by (dtac real_mult_order 1 THEN assume_tac 1);
12.139 -by (rtac (real_minus_zero_less_iff RS iffD1) 1);
12.140 -by (Asm_full_simp_tac 1);
12.141 -qed "real_mult_less_0";
12.142 -
12.143 -Goalw [real_one_def] "0 < (1::real)";
12.144 -by (auto_tac (claset() addIs [real_gt_zero_preal_Ex RS iffD2],
12.145 - simpset() addsimps [real_of_preal_def]));
12.146 -qed "real_zero_less_one";
12.147 -
12.148 -(*** Monotonicity results ***)
12.149 -
12.150 -Goal "(v+z < w+z) = (v < (w::real))";
12.151 -by (Simp_tac 1);
12.152 -qed "real_add_right_cancel_less";
12.153 -
12.154 -Goal "(z+v < z+w) = (v < (w::real))";
12.155 -by (Simp_tac 1);
12.156 -qed "real_add_left_cancel_less";
12.157 -
12.158 -Addsimps [real_add_right_cancel_less, real_add_left_cancel_less];
12.159 -
12.160 -Goal "(v+z <= w+z) = (v <= (w::real))";
12.161 -by (Simp_tac 1);
12.162 -qed "real_add_right_cancel_le";
12.163 -
12.164 -Goal "(z+v <= z+w) = (v <= (w::real))";
12.165 -by (Simp_tac 1);
12.166 -qed "real_add_left_cancel_le";
12.167 -
12.168 -Addsimps [real_add_right_cancel_le, real_add_left_cancel_le];
12.169 -
12.170 -(*"v<=w ==> v+z <= w+z"*)
12.171 -bind_thm ("real_add_less_mono1", real_add_right_cancel_less RS iffD2);
12.172 -
12.173 -(*"v<=w ==> v+z <= w+z"*)
12.174 -bind_thm ("real_add_le_mono1", real_add_right_cancel_le RS iffD2);
12.175 -
12.176 -Goal "!!z z'::real. [| w'<w; z'<=z |] ==> w' + z' < w + z";
12.177 -by (etac (real_add_less_mono1 RS order_less_le_trans) 1);
12.178 -by (Simp_tac 1);
12.179 -qed "real_add_less_le_mono";
12.180 -
12.181 -Goal "!!z z'::real. [| w'<=w; z'<z |] ==> w' + z' < w + z";
12.182 -by (etac (real_add_le_mono1 RS order_le_less_trans) 1);
12.183 -by (Simp_tac 1);
12.184 -qed "real_add_le_less_mono";
12.185 -
12.186 -Goal "!!(A::real). A < B ==> C + A < C + B";
12.187 -by (Simp_tac 1);
12.188 -qed "real_add_less_mono2";
12.189 -
12.190 -Goal "!!(A::real). A + C < B + C ==> A < B";
12.191 -by (Full_simp_tac 1);
12.192 -qed "real_less_add_right_cancel";
12.193 -
12.194 -Goal "!!(A::real). C + A < C + B ==> A < B";
12.195 -by (Full_simp_tac 1);
12.196 -qed "real_less_add_left_cancel";
12.197 -
12.198 -Goal "!!(A::real). A + C <= B + C ==> A <= B";
12.199 -by (Full_simp_tac 1);
12.200 -qed "real_le_add_right_cancel";
12.201 -
12.202 -Goal "!!(A::real). C + A <= C + B ==> A <= B";
12.203 -by (Full_simp_tac 1);
12.204 -qed "real_le_add_left_cancel";
12.205 -
12.206 -Goal "[| 0 < x; 0 < y |] ==> (0::real) < x + y";
12.207 -by (etac order_less_trans 1);
12.208 -by (dtac real_add_less_mono2 1);
12.209 -by (Full_simp_tac 1);
12.210 -qed "real_add_order";
12.211 -
12.212 -Goal "[| 0 <= x; 0 <= y |] ==> (0::real) <= x + y";
12.213 -by (REPEAT(dtac order_le_imp_less_or_eq 1));
12.214 -by (auto_tac (claset() addIs [real_add_order, order_less_imp_le],
12.215 - simpset()));
12.216 -qed "real_le_add_order";
12.217 -
12.218 -Goal "[| R1 < S1; R2 < S2 |] ==> R1 + R2 < S1 + (S2::real)";
12.219 -by (dtac real_add_less_mono1 1);
12.220 -by (etac order_less_trans 1);
12.221 -by (etac real_add_less_mono2 1);
12.222 -qed "real_add_less_mono";
12.223 -
12.224 -Goal "!!(q1::real). q1 <= q2 ==> x + q1 <= x + q2";
12.225 -by (Simp_tac 1);
12.226 -qed "real_add_left_le_mono1";
12.227 -
12.228 -Goal "[|i<=j; k<=l |] ==> i + k <= j + (l::real)";
12.229 -by (dtac real_add_le_mono1 1);
12.230 -by (etac order_trans 1);
12.231 -by (Simp_tac 1);
12.232 -qed "real_add_le_mono";
12.233 -
12.234 -Goal "EX (x::real). x < y";
12.235 -by (rtac (real_add_zero_right RS subst) 1);
12.236 -by (res_inst_tac [("x","y + (- (1::real))")] exI 1);
12.237 -by (auto_tac (claset() addSIs [real_add_less_mono2],
12.238 - simpset() addsimps [real_minus_zero_less_iff2, real_zero_less_one]));
12.239 -qed "real_less_Ex";
12.240 -
12.241 -Goal "(0::real) < r ==> u + (-r) < u";
12.242 -by (res_inst_tac [("C","r")] real_less_add_right_cancel 1);
12.243 -by (simp_tac (simpset() addsimps [real_add_assoc]) 1);
12.244 -qed "real_add_minus_positive_less_self";
12.245 -
12.246 -Goal "(-s <= -r) = ((r::real) <= s)";
12.247 -by (rtac sym 1);
12.248 -by (Step_tac 1);
12.249 -by (dres_inst_tac [("x","-s")] real_add_left_le_mono1 1);
12.250 -by (dres_inst_tac [("x","r")] real_add_left_le_mono1 2);
12.251 -by Auto_tac;
12.252 -by (dres_inst_tac [("z","-r")] real_add_le_mono1 1);
12.253 -by (dres_inst_tac [("z","s")] real_add_le_mono1 2);
12.254 -by (auto_tac (claset(), simpset() addsimps [real_add_assoc]));
12.255 -qed "real_le_minus_iff";
12.256 -Addsimps [real_le_minus_iff];
12.257 -
12.258 -Goal "(0::real) <= x*x";
12.259 -by (res_inst_tac [("R2.0","0"),("R1.0","x")] real_linear_less2 1);
12.260 -by (auto_tac (claset() addIs [real_mult_order,
12.261 - neg_real_mult_order,order_less_imp_le],
12.262 - simpset()));
12.263 -qed "real_le_square";
12.264 -Addsimps [real_le_square];
12.265 -
12.266 -(*----------------------------------------------------------------------------
12.267 - An embedding of the naturals in the reals
12.268 - ----------------------------------------------------------------------------*)
12.269 -
12.270 -Goalw [real_of_posnat_def] "real_of_posnat 0 = (1::real)";
12.271 -by (simp_tac (simpset() addsimps [pnat_one_iff RS sym,real_of_preal_def,
12.272 - symmetric real_one_def]) 1);
12.273 -qed "real_of_posnat_one";
12.274 -
12.275 -Goalw [real_of_posnat_def] "real_of_posnat (Suc 0) = (1::real) + (1::real)";
12.276 -by (simp_tac (simpset() addsimps [real_of_preal_def,real_one_def,
12.277 - pnat_two_eq,real_add,prat_of_pnat_add RS sym,
12.278 - preal_of_prat_add RS sym] @ pnat_add_ac) 1);
12.279 -qed "real_of_posnat_two";
12.280 -
12.281 -Goalw [real_of_posnat_def]
12.282 - "real_of_posnat n1 + real_of_posnat n2 = real_of_posnat (n1 + n2) + (1::real)";
12.283 -by (full_simp_tac (simpset() addsimps [real_of_posnat_one RS sym,
12.284 - real_of_posnat_def,real_of_preal_add RS sym,preal_of_prat_add RS sym,
12.285 - prat_of_pnat_add RS sym,pnat_of_nat_add]) 1);
12.286 -qed "real_of_posnat_add";
12.287 -
12.288 -Goal "real_of_posnat (n + 1) = real_of_posnat n + (1::real)";
12.289 -by (res_inst_tac [("x1","(1::real)")] (real_add_right_cancel RS iffD1) 1);
12.290 -by (rtac (real_of_posnat_add RS subst) 1);
12.291 -by (full_simp_tac (simpset() addsimps [real_of_posnat_two,real_add_assoc]) 1);
12.292 -qed "real_of_posnat_add_one";
12.293 -
12.294 -Goal "real_of_posnat (Suc n) = real_of_posnat n + (1::real)";
12.295 -by (stac (real_of_posnat_add_one RS sym) 1);
12.296 -by (Simp_tac 1);
12.297 -qed "real_of_posnat_Suc";
12.298 -
12.299 -Goal "inj(real_of_posnat)";
12.300 -by (rtac injI 1);
12.301 -by (rewtac real_of_posnat_def);
12.302 -by (dtac (inj_real_of_preal RS injD) 1);
12.303 -by (dtac (inj_preal_of_prat RS injD) 1);
12.304 -by (dtac (inj_prat_of_pnat RS injD) 1);
12.305 -by (etac (inj_pnat_of_nat RS injD) 1);
12.306 -qed "inj_real_of_posnat";
12.307 -
12.308 -Goalw [real_of_nat_def] "real (0::nat) = 0";
12.309 -by (simp_tac (simpset() addsimps [real_of_posnat_one]) 1);
12.310 -qed "real_of_nat_zero";
12.311 -
12.312 -Goalw [real_of_nat_def] "real (Suc 0) = (1::real)";
12.313 -by (simp_tac (simpset() addsimps [real_of_posnat_two, real_add_assoc]) 1);
12.314 -qed "real_of_nat_one";
12.315 -Addsimps [real_of_nat_zero, real_of_nat_one];
12.316 -
12.317 -Goalw [real_of_nat_def]
12.318 - "real (m + n) = real (m::nat) + real n";
12.319 -by (simp_tac (simpset() addsimps
12.320 - [real_of_posnat_add,real_add_assoc RS sym]) 1);
12.321 -qed "real_of_nat_add";
12.322 -Addsimps [real_of_nat_add];
12.323 -
12.324 -(*Not for addsimps: often the LHS is used to represent a positive natural*)
12.325 -Goalw [real_of_nat_def] "real (Suc n) = real n + (1::real)";
12.326 -by (simp_tac (simpset() addsimps [real_of_posnat_Suc] @ real_add_ac) 1);
12.327 -qed "real_of_nat_Suc";
12.328 -
12.329 -Goalw [real_of_nat_def, real_of_posnat_def]
12.330 - "(real (n::nat) < real m) = (n < m)";
12.331 -by Auto_tac;
12.332 -qed "real_of_nat_less_iff";
12.333 -AddIffs [real_of_nat_less_iff];
12.334 -
12.335 -Goal "(real (n::nat) <= real m) = (n <= m)";
12.336 -by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
12.337 -qed "real_of_nat_le_iff";
12.338 -AddIffs [real_of_nat_le_iff];
12.339 -
12.340 -Goal "inj (real :: nat => real)";
12.341 -by (rtac injI 1);
12.342 -by (auto_tac (claset() addSIs [inj_real_of_posnat RS injD],
12.343 - simpset() addsimps [real_of_nat_def,real_add_right_cancel]));
12.344 -qed "inj_real_of_nat";
12.345 -
12.346 -Goal "0 <= real (n::nat)";
12.347 -by (induct_tac "n" 1);
12.348 -by (auto_tac (claset(),
12.349 - simpset () addsimps [real_of_nat_Suc]));
12.350 -by (dtac real_add_le_less_mono 1);
12.351 -by (rtac real_zero_less_one 1);
12.352 -by (asm_full_simp_tac (simpset() addsimps [order_less_imp_le]) 1);
12.353 -qed "real_of_nat_ge_zero";
12.354 -AddIffs [real_of_nat_ge_zero];
12.355 -
12.356 -Goal "real (m * n) = real (m::nat) * real n";
12.357 -by (induct_tac "m" 1);
12.358 -by (auto_tac (claset(),
12.359 - simpset() addsimps [real_of_nat_Suc,
12.360 - real_add_mult_distrib, real_add_commute]));
12.361 -qed "real_of_nat_mult";
12.362 -Addsimps [real_of_nat_mult];
12.363 -
12.364 -Goal "(real (n::nat) = real m) = (n = m)";
12.365 -by (auto_tac (claset() addDs [inj_real_of_nat RS injD], simpset()));
12.366 -qed "real_of_nat_inject";
12.367 -AddIffs [real_of_nat_inject];
12.368 -
12.369 -Goal "n <= m --> real (m - n) = real (m::nat) - real n";
12.370 -by (induct_tac "m" 1);
12.371 -by (auto_tac (claset(),
12.372 - simpset() addsimps [real_diff_def, Suc_diff_le, le_Suc_eq,
12.373 - real_of_nat_Suc, real_of_nat_zero] @ real_add_ac));
12.374 -qed_spec_mp "real_of_nat_diff";
12.375 -
12.376 -Goal "(real (n::nat) = 0) = (n = 0)";
12.377 -by (auto_tac ((claset() addIs [inj_real_of_nat RS injD], simpset()) delIffs [real_of_nat_inject]));
12.378 -qed "real_of_nat_zero_iff";
12.379 -
12.380 -Goal "neg z ==> real (nat z) = 0";
12.381 -by (asm_simp_tac (simpset() addsimps [neg_nat, real_of_nat_zero]) 1);
12.382 -qed "real_of_nat_neg_int";
12.383 -Addsimps [real_of_nat_neg_int];
12.384 -
12.385 -
12.386 -(*----------------------------------------------------------------------------
12.387 - inverse, etc.
12.388 - ----------------------------------------------------------------------------*)
12.389 -
12.390 -Goal "0 < x ==> 0 < inverse (x::real)";
12.391 -by (EVERY1[rtac ccontr, dtac real_leI]);
12.392 -by (forward_tac [real_minus_zero_less_iff2 RS iffD2] 1);
12.393 -by (forward_tac [real_not_refl2 RS not_sym] 1);
12.394 -by (dtac (real_not_refl2 RS not_sym RS real_inverse_not_zero) 1);
12.395 -by (EVERY1[dtac order_le_imp_less_or_eq, Step_tac]);
12.396 -by (dtac neg_real_mult_order 1 THEN assume_tac 1);
12.397 -by (auto_tac (claset() addIs [real_zero_less_one RS real_less_asym],
12.398 - simpset()));
12.399 -qed "real_inverse_gt_0";
12.400 -
12.401 -Goal "x < 0 ==> inverse (x::real) < 0";
12.402 -by (ftac real_not_refl2 1);
12.403 -by (dtac (real_minus_zero_less_iff RS iffD2) 1);
12.404 -by (rtac (real_minus_zero_less_iff RS iffD1) 1);
12.405 -by (stac (real_minus_inverse RS sym) 1);
12.406 -by (auto_tac (claset() addIs [real_inverse_gt_0], simpset()));
12.407 -qed "real_inverse_less_0";
12.408 -
12.409 -Goal "[| (0::real) < z; x < y |] ==> x*z < y*z";
12.410 -by (rotate_tac 1 1);
12.411 -by (dtac real_less_sum_gt_zero 1);
12.412 -by (rtac real_sum_gt_zero_less 1);
12.413 -by (dtac real_mult_order 1 THEN assume_tac 1);
12.414 -by (asm_full_simp_tac
12.415 - (simpset() addsimps [real_add_mult_distrib2, real_mult_commute ]) 1);
12.416 -qed "real_mult_less_mono1";
12.417 -
12.418 -Goal "[| (0::real) < z; x < y |] ==> z * x < z * y";
12.419 -by (asm_simp_tac
12.420 - (simpset() addsimps [real_mult_commute,real_mult_less_mono1]) 1);
12.421 -qed "real_mult_less_mono2";
12.422 -
12.423 -Goal "[| (0::real) < z; x * z < y * z |] ==> x < y";
12.424 -by (forw_inst_tac [("x","x*z")]
12.425 - (real_inverse_gt_0 RS real_mult_less_mono1) 1);
12.426 -by (auto_tac (claset(),
12.427 - simpset() addsimps [real_mult_assoc,real_not_refl2 RS not_sym]));
12.428 -qed "real_mult_less_cancel1";
12.429 -
12.430 -Goal "[| (0::real) < z; z*x < z*y |] ==> x < y";
12.431 -by (etac real_mult_less_cancel1 1);
12.432 -by (asm_full_simp_tac (simpset() addsimps [real_mult_commute]) 1);
12.433 -qed "real_mult_less_cancel2";
12.434 -
12.435 -Goal "(0::real) < z ==> (x*z < y*z) = (x < y)";
12.436 -by (blast_tac
12.437 - (claset() addIs [real_mult_less_mono1, real_mult_less_cancel1]) 1);
12.438 -qed "real_mult_less_iff1";
12.439 -
12.440 -Goal "(0::real) < z ==> (z*x < z*y) = (x < y)";
12.441 -by (blast_tac
12.442 - (claset() addIs [real_mult_less_mono2, real_mult_less_cancel2]) 1);
12.443 -qed "real_mult_less_iff2";
12.444 -
12.445 -Addsimps [real_mult_less_iff1,real_mult_less_iff2];
12.446 -
12.447 -(* 05/00 *)
12.448 -Goalw [real_le_def] "(0::real) < z ==> (x*z <= y*z) = (x <= y)";
12.449 -by (Auto_tac);
12.450 -qed "real_mult_le_cancel_iff1";
12.451 -
12.452 -Goalw [real_le_def] "(0::real) < z ==> (z*x <= z*y) = (x <= y)";
12.453 -by (Auto_tac);
12.454 -qed "real_mult_le_cancel_iff2";
12.455 -
12.456 -Addsimps [real_mult_le_cancel_iff1,real_mult_le_cancel_iff2];
12.457 -
12.458 -
12.459 -Goal "[| (0::real) <= z; x < y |] ==> x*z <= y*z";
12.460 -by (EVERY1 [rtac real_less_or_eq_imp_le, dtac order_le_imp_less_or_eq]);
12.461 -by (auto_tac (claset() addIs [real_mult_less_mono1],simpset()));
12.462 -qed "real_mult_le_less_mono1";
12.463 -
12.464 -Goal "[| u<v; x<y; (0::real) < v; 0 < x |] ==> u*x < v* y";
12.465 -by (etac (real_mult_less_mono1 RS order_less_trans) 1);
12.466 -by (assume_tac 1);
12.467 -by (etac real_mult_less_mono2 1);
12.468 -by (assume_tac 1);
12.469 -qed "real_mult_less_mono";
12.470 -
12.471 -(*Variant of the theorem above; sometimes it's stronger*)
12.472 -Goal "[| x < y; r1 < r2; (0::real) <= r1; 0 <= x|] ==> r1 * x < r2 * y";
12.473 -by (subgoal_tac "0<r2" 1);
12.474 -by (blast_tac (claset() addIs [order_le_less_trans]) 2);
12.475 -by (case_tac "x=0" 1);
12.476 -by (auto_tac (claset() addSDs [order_le_imp_less_or_eq]
12.477 - addIs [real_mult_less_mono, real_mult_order],
12.478 - simpset()));
12.479 -qed "real_mult_less_mono'";
12.480 -
12.481 -Goal "(1::real) <= x ==> 0 < x";
12.482 -by (rtac ccontr 1 THEN dtac real_leI 1);
12.483 -by (dtac order_trans 1 THEN assume_tac 1);
12.484 -by (auto_tac (claset() addDs [real_zero_less_one RSN (2,order_le_less_trans)],
12.485 - simpset()));
12.486 -qed "real_gt_zero";
12.487 -
12.488 -Goal "[| (1::real) < r; (1::real) <= x |] ==> x <= r * x";
12.489 -by (dtac (real_gt_zero RS order_less_imp_le) 1);
12.490 -by (auto_tac (claset() addSDs [real_mult_le_less_mono1],
12.491 - simpset()));
12.492 -qed "real_mult_self_le";
12.493 -
12.494 -Goal "[| (1::real) <= r; (1::real) <= x |] ==> x <= r * x";
12.495 -by (dtac order_le_imp_less_or_eq 1);
12.496 -by (auto_tac (claset() addIs [real_mult_self_le], simpset()));
12.497 -qed "real_mult_self_le2";
12.498 -
12.499 -Goal "[| 0 < r; r < x |] ==> inverse x < inverse (r::real)";
12.500 -by (ftac order_less_trans 1 THEN assume_tac 1);
12.501 -by (ftac real_inverse_gt_0 1);
12.502 -by (forw_inst_tac [("x","x")] real_inverse_gt_0 1);
12.503 -by (forw_inst_tac [("x","r"),("z","inverse r")] real_mult_less_mono1 1);
12.504 -by (assume_tac 1);
12.505 -by (asm_full_simp_tac (simpset() addsimps [real_not_refl2 RS
12.506 - not_sym RS real_mult_inv_right]) 1);
12.507 -by (ftac real_inverse_gt_0 1);
12.508 -by (forw_inst_tac [("x","(1::real)"),("z","inverse x")] real_mult_less_mono2 1);
12.509 -by (assume_tac 1);
12.510 -by (asm_full_simp_tac (simpset() addsimps [real_not_refl2 RS
12.511 - not_sym RS real_mult_inv_left,real_mult_assoc RS sym]) 1);
12.512 -qed "real_inverse_less_swap";
12.513 -
12.514 -Goal "(x*y = 0) = (x = 0 | y = (0::real))";
12.515 -by Auto_tac;
12.516 -by (blast_tac (claset() addIs [ccontr] addDs [real_mult_not_zero]) 1);
12.517 -qed "real_mult_is_0";
12.518 -AddIffs [real_mult_is_0];
12.519 -
12.520 -Goal "[| x ~= 0; y ~= 0 |] \
12.521 -\ ==> inverse x + inverse y = (x + y) * inverse (x * (y::real))";
12.522 -by (asm_full_simp_tac (simpset() addsimps
12.523 - [real_inverse_distrib,real_add_mult_distrib,
12.524 - real_mult_assoc RS sym]) 1);
12.525 -by (stac real_mult_assoc 1);
12.526 -by (rtac (real_mult_left_commute RS subst) 1);
12.527 -by (asm_full_simp_tac (simpset() addsimps [real_add_commute]) 1);
12.528 -qed "real_inverse_add";
12.529 -
12.530 -(* 05/00 *)
12.531 -Goal "(0 <= -R) = (R <= (0::real))";
12.532 -by (auto_tac (claset() addDs [sym],
12.533 - simpset() addsimps [real_le_less]));
12.534 -qed "real_minus_zero_le_iff";
12.535 -
12.536 -Goal "(-R <= 0) = ((0::real) <= R)";
12.537 -by (auto_tac (claset(),simpset() addsimps
12.538 - [real_minus_zero_less_iff2,real_le_less]));
12.539 -qed "real_minus_zero_le_iff2";
12.540 -
12.541 -Addsimps [real_minus_zero_le_iff, real_minus_zero_le_iff2];
12.542 -
12.543 -Goal "x * x + y * y = 0 ==> x = (0::real)";
12.544 -by (dtac real_add_minus_eq_minus 1);
12.545 -by (cut_inst_tac [("x","x")] real_le_square 1);
12.546 -by (Auto_tac THEN dtac real_le_anti_sym 1);
12.547 -by Auto_tac;
12.548 -qed "real_sum_squares_cancel";
12.549 -
12.550 -Goal "x * x + y * y = 0 ==> y = (0::real)";
12.551 -by (res_inst_tac [("y","x")] real_sum_squares_cancel 1);
12.552 -by (asm_full_simp_tac (simpset() addsimps [real_add_commute]) 1);
12.553 -qed "real_sum_squares_cancel2";
12.554 -
12.555 -(*----------------------------------------------------------------------------
12.556 - Some convenient biconditionals for products of signs (lcp)
12.557 - ----------------------------------------------------------------------------*)
12.558 -
12.559 -Goal "((0::real) < x*y) = (0 < x & 0 < y | x < 0 & y < 0)";
12.560 -by (auto_tac (claset(),
12.561 - simpset() addsimps [order_le_less, linorder_not_less,
12.562 - real_mult_order, neg_real_mult_order]));
12.563 -by (ALLGOALS (rtac ccontr));
12.564 -by (auto_tac (claset(), simpset() addsimps [order_le_less, linorder_not_less]));
12.565 -by (ALLGOALS (etac rev_mp));
12.566 -by (ALLGOALS (dtac real_mult_less_0 THEN' assume_tac));
12.567 -by (auto_tac (claset() addDs [order_less_not_sym],
12.568 - simpset() addsimps [real_mult_commute]));
12.569 -qed "real_0_less_mult_iff";
12.570 -
12.571 -Goal "((0::real) <= x*y) = (0 <= x & 0 <= y | x <= 0 & y <= 0)";
12.572 -by (auto_tac (claset(),
12.573 - simpset() addsimps [order_le_less, linorder_not_less,
12.574 - real_0_less_mult_iff]));
12.575 -qed "real_0_le_mult_iff";
12.576 -
12.577 -Goal "(x*y < (0::real)) = (0 < x & y < 0 | x < 0 & 0 < y)";
12.578 -by (auto_tac (claset(),
12.579 - simpset() addsimps [real_0_le_mult_iff,
12.580 - linorder_not_le RS sym]));
12.581 -by (auto_tac (claset() addDs [order_less_not_sym],
12.582 - simpset() addsimps [linorder_not_le]));
12.583 -qed "real_mult_less_0_iff";
12.584 -
12.585 -Goal "(x*y <= (0::real)) = (0 <= x & y <= 0 | x <= 0 & 0 <= y)";
12.586 -by (auto_tac (claset() addDs [order_less_not_sym],
12.587 - simpset() addsimps [real_0_less_mult_iff,
12.588 - linorder_not_less RS sym]));
12.589 -qed "real_mult_le_0_iff";
12.590 -
13.1 --- a/src/HOL/Real/RealOrd.thy Thu Nov 20 10:42:00 2003 +0100
13.2 +++ b/src/HOL/Real/RealOrd.thy Fri Nov 21 11:15:40 2003 +0100
13.3 @@ -2,15 +2,696 @@
13.4 ID: $Id$
13.5 Author: Jacques D. Fleuriot and Lawrence C. Paulson
13.6 Copyright: 1998 University of Cambridge
13.7 - Description: Type "real" is a linear order and also
13.8 - satisfies plus_ac0: + is an AC-operator with zero
13.9 *)
13.10
13.11 -RealOrd = RealDef +
13.12 +header{*The Reals Form an Ordered Field, etc.*}
13.13
13.14 -instance real :: order (real_le_refl,real_le_trans,real_le_anti_sym,real_less_le)
13.15 -instance real :: linorder (real_le_linear)
13.16 +theory RealOrd = RealDef:
13.17
13.18 -instance real :: plus_ac0 (real_add_commute,real_add_assoc,real_add_zero_left)
13.19 +instance real :: order
13.20 + by (intro_classes,
13.21 + (assumption |
13.22 + rule real_le_refl real_le_trans real_le_anti_sym real_less_le)+)
13.23 +
13.24 +instance real :: linorder
13.25 + by (intro_classes, rule real_le_linear)
13.26 +
13.27 +instance real :: plus_ac0
13.28 + by (intro_classes,
13.29 + (assumption |
13.30 + rule real_add_commute real_add_assoc real_add_zero_left)+)
13.31 +
13.32 +
13.33 +defs (overloaded)
13.34 + real_abs_def: "abs (r::real) == (if 0 \<le> r then r else -r)"
13.35 +
13.36 +
13.37 +
13.38 +
13.39 +subsection{* The Simproc @{text abel_cancel}*}
13.40 +
13.41 +(*Deletion of other terms in the formula, seeking the -x at the front of z*)
13.42 +lemma real_add_cancel_21: "((x::real) + (y + z) = y + u) = ((x + z) = u)"
13.43 +apply (subst real_add_left_commute)
13.44 +apply (rule real_add_left_cancel)
13.45 +done
13.46 +
13.47 +(*A further rule to deal with the case that
13.48 + everything gets cancelled on the right.*)
13.49 +lemma real_add_cancel_end: "((x::real) + (y + z) = y) = (x = -z)"
13.50 +apply (subst real_add_left_commute)
13.51 +apply (rule_tac t = "y" in real_add_zero_right [THEN subst] , subst real_add_left_cancel)
13.52 +apply (simp (no_asm) add: real_eq_diff_eq [symmetric])
13.53 +done
13.54 +
13.55 +
13.56 +ML
13.57 +{*
13.58 +val real_add_cancel_21 = thm "real_add_cancel_21";
13.59 +val real_add_cancel_end = thm "real_add_cancel_end";
13.60 +
13.61 +structure Real_Cancel_Data =
13.62 +struct
13.63 + val ss = HOL_ss
13.64 + val eq_reflection = eq_reflection
13.65 +
13.66 + val sg_ref = Sign.self_ref (Theory.sign_of (the_context ()))
13.67 + val T = HOLogic.realT
13.68 + val zero = Const ("0", T)
13.69 + val restrict_to_left = restrict_to_left
13.70 + val add_cancel_21 = real_add_cancel_21
13.71 + val add_cancel_end = real_add_cancel_end
13.72 + val add_left_cancel = real_add_left_cancel
13.73 + val add_assoc = real_add_assoc
13.74 + val add_commute = real_add_commute
13.75 + val add_left_commute = real_add_left_commute
13.76 + val add_0 = real_add_zero_left
13.77 + val add_0_right = real_add_zero_right
13.78 +
13.79 + val eq_diff_eq = real_eq_diff_eq
13.80 + val eqI_rules = [real_less_eqI, real_eq_eqI, real_le_eqI]
13.81 + fun dest_eqI th =
13.82 + #1 (HOLogic.dest_bin "op =" HOLogic.boolT
13.83 + (HOLogic.dest_Trueprop (concl_of th)))
13.84 +
13.85 + val diff_def = real_diff_def
13.86 + val minus_add_distrib = real_minus_add_distrib
13.87 + val minus_minus = real_minus_minus
13.88 + val minus_0 = real_minus_zero
13.89 + val add_inverses = [real_add_minus, real_add_minus_left]
13.90 + val cancel_simps = [real_add_minus_cancel, real_minus_add_cancel]
13.91 +end;
13.92 +
13.93 +structure Real_Cancel = Abel_Cancel (Real_Cancel_Data);
13.94 +
13.95 +Addsimprocs [Real_Cancel.sum_conv, Real_Cancel.rel_conv];
13.96 +*}
13.97 +
13.98 +lemma real_minus_diff_eq: "- (z - y) = y - (z::real)"
13.99 +apply (simp (no_asm))
13.100 +done
13.101 +declare real_minus_diff_eq [simp]
13.102 +
13.103 +
13.104 +subsection{*Theorems About the Ordering*}
13.105 +
13.106 +lemma real_gt_zero_preal_Ex: "(0 < x) = (\<exists>y. x = real_of_preal y)"
13.107 +apply (auto simp add: real_of_preal_zero_less)
13.108 +apply (cut_tac x = "x" in real_of_preal_trichotomy)
13.109 +apply (blast elim!: real_less_irrefl real_of_preal_not_minus_gt_zero [THEN notE])
13.110 +done
13.111 +
13.112 +lemma real_gt_preal_preal_Ex: "real_of_preal z < x ==> \<exists>y. x = real_of_preal y"
13.113 +apply (blast dest!: real_of_preal_zero_less [THEN real_less_trans]
13.114 + intro: real_gt_zero_preal_Ex [THEN iffD1])
13.115 +done
13.116 +
13.117 +lemma real_ge_preal_preal_Ex: "real_of_preal z \<le> x ==> \<exists>y. x = real_of_preal y"
13.118 +apply (blast dest: order_le_imp_less_or_eq real_gt_preal_preal_Ex)
13.119 +done
13.120 +
13.121 +lemma real_less_all_preal: "y \<le> 0 ==> \<forall>x. y < real_of_preal x"
13.122 +apply (auto elim: order_le_imp_less_or_eq [THEN disjE]
13.123 + intro: real_of_preal_zero_less [THEN [2] real_less_trans]
13.124 + simp add: real_of_preal_zero_less)
13.125 +done
13.126 +
13.127 +lemma real_less_all_real2: "~ 0 < y ==> \<forall>x. y < real_of_preal x"
13.128 +apply (blast intro!: real_less_all_preal real_leI)
13.129 +done
13.130 +
13.131 +lemma real_lemma_add_positive_imp_less: "[| R + L = S; (0::real) < L |] ==> R < S"
13.132 +apply (rule real_less_sum_gt_0_iff [THEN iffD1])
13.133 +apply (auto simp add: real_add_ac)
13.134 +done
13.135 +
13.136 +lemma real_ex_add_positive_left_less: "\<exists>T::real. 0 < T & R + T = S ==> R < S"
13.137 +apply (blast intro: real_lemma_add_positive_imp_less)
13.138 +done
13.139 +
13.140 +(*Alternative definition for real_less. NOT for rewriting*)
13.141 +lemma real_less_iff_add: "(R < S) = (\<exists>T::real. 0 < T & R + T = S)"
13.142 +apply (blast intro!: real_less_add_positive_left_Ex real_ex_add_positive_left_less)
13.143 +done
13.144 +
13.145 +lemma real_of_preal_le_iff: "(real_of_preal m1 \<le> real_of_preal m2) = (m1 \<le> m2)"
13.146 +apply (auto intro!: preal_leI simp add: real_less_le_iff [symmetric])
13.147 +apply (drule order_le_less_trans , assumption)
13.148 +apply (erule preal_less_irrefl)
13.149 +done
13.150 +
13.151 +lemma real_mult_order: "[| 0 < x; 0 < y |] ==> (0::real) < x * y"
13.152 +apply (auto simp add: real_gt_zero_preal_Ex)
13.153 +apply (rule_tac x = "y*ya" in exI)
13.154 +apply (simp (no_asm_use) add: real_of_preal_mult)
13.155 +done
13.156 +
13.157 +lemma neg_real_mult_order: "[| x < 0; y < 0 |] ==> (0::real) < x * y"
13.158 +apply (drule real_minus_zero_less_iff [THEN iffD2])+
13.159 +apply (drule real_mult_order , assumption)
13.160 +apply simp
13.161 +done
13.162 +
13.163 +lemma real_mult_less_0: "[| 0 < x; y < 0 |] ==> x*y < (0::real)"
13.164 +apply (drule real_minus_zero_less_iff [THEN iffD2])
13.165 +apply (drule real_mult_order , assumption)
13.166 +apply (rule real_minus_zero_less_iff [THEN iffD1])
13.167 +apply simp
13.168 +done
13.169 +
13.170 +lemma real_zero_less_one: "0 < (1::real)"
13.171 +apply (unfold real_one_def)
13.172 +apply (auto intro: real_gt_zero_preal_Ex [THEN iffD2]
13.173 + simp add: real_of_preal_def)
13.174 +done
13.175 +
13.176 +
13.177 +subsection{*Monotonicity of Addition*}
13.178 +
13.179 +lemma real_add_right_cancel_less: "(v+z < w+z) = (v < (w::real))"
13.180 +apply (simp (no_asm))
13.181 +done
13.182 +
13.183 +lemma real_add_left_cancel_less: "(z+v < z+w) = (v < (w::real))"
13.184 +apply (simp (no_asm))
13.185 +done
13.186 +
13.187 +declare real_add_right_cancel_less [simp] real_add_left_cancel_less [simp]
13.188 +
13.189 +lemma real_add_right_cancel_le: "(v+z \<le> w+z) = (v \<le> (w::real))"
13.190 +apply (simp (no_asm))
13.191 +done
13.192 +
13.193 +lemma real_add_left_cancel_le: "(z+v \<le> z+w) = (v \<le> (w::real))"
13.194 +apply (simp (no_asm))
13.195 +done
13.196 +
13.197 +declare real_add_right_cancel_le [simp] real_add_left_cancel_le [simp]
13.198 +
13.199 +(*"v\<le>w ==> v+z \<le> w+z"*)
13.200 +lemmas real_add_less_mono1 = real_add_right_cancel_less [THEN iffD2, standard]
13.201 +
13.202 +(*"v\<le>w ==> v+z \<le> w+z"*)
13.203 +lemmas real_add_le_mono1 = real_add_right_cancel_le [THEN iffD2, standard]
13.204 +
13.205 +lemma real_add_less_le_mono: "!!z z'::real. [| w'<w; z'\<le>z |] ==> w' + z' < w + z"
13.206 +apply (erule real_add_less_mono1 [THEN order_less_le_trans])
13.207 +apply (simp (no_asm))
13.208 +done
13.209 +
13.210 +lemma real_add_le_less_mono: "!!z z'::real. [| w'\<le>w; z'<z |] ==> w' + z' < w + z"
13.211 +apply (erule real_add_le_mono1 [THEN order_le_less_trans])
13.212 +apply (simp (no_asm))
13.213 +done
13.214 +
13.215 +lemma real_add_less_mono2: "!!(A::real). A < B ==> C + A < C + B"
13.216 +apply (simp (no_asm))
13.217 +done
13.218 +
13.219 +lemma real_less_add_right_cancel: "!!(A::real). A + C < B + C ==> A < B"
13.220 +apply (simp (no_asm_use))
13.221 +done
13.222 +
13.223 +lemma real_less_add_left_cancel: "!!(A::real). C + A < C + B ==> A < B"
13.224 +apply (simp (no_asm_use))
13.225 +done
13.226 +
13.227 +lemma real_le_add_right_cancel: "!!(A::real). A + C \<le> B + C ==> A \<le> B"
13.228 +apply (simp (no_asm_use))
13.229 +done
13.230 +
13.231 +lemma real_le_add_left_cancel: "!!(A::real). C + A \<le> C + B ==> A \<le> B"
13.232 +apply (simp (no_asm_use))
13.233 +done
13.234 +
13.235 +lemma real_add_order: "[| 0 < x; 0 < y |] ==> (0::real) < x + y"
13.236 +apply (erule order_less_trans)
13.237 +apply (drule real_add_less_mono2)
13.238 +apply (simp (no_asm_use))
13.239 +done
13.240 +
13.241 +lemma real_le_add_order: "[| 0 \<le> x; 0 \<le> y |] ==> (0::real) \<le> x + y"
13.242 +apply (drule order_le_imp_less_or_eq)+
13.243 +apply (auto intro: real_add_order order_less_imp_le)
13.244 +done
13.245 +
13.246 +lemma real_add_less_mono: "[| R1 < S1; R2 < S2 |] ==> R1 + R2 < S1 + (S2::real)"
13.247 +apply (drule real_add_less_mono1)
13.248 +apply (erule order_less_trans)
13.249 +apply (erule real_add_less_mono2)
13.250 +done
13.251 +
13.252 +lemma real_add_left_le_mono1: "!!(q1::real). q1 \<le> q2 ==> x + q1 \<le> x + q2"
13.253 +apply (simp (no_asm))
13.254 +done
13.255 +
13.256 +lemma real_add_le_mono: "[|i\<le>j; k\<le>l |] ==> i + k \<le> j + (l::real)"
13.257 +apply (drule real_add_le_mono1)
13.258 +apply (erule order_trans)
13.259 +apply (simp (no_asm))
13.260 +done
13.261 +
13.262 +lemma real_less_Ex: "\<exists>(x::real). x < y"
13.263 +apply (rule real_add_zero_right [THEN subst])
13.264 +apply (rule_tac x = "y + (- (1::real))" in exI)
13.265 +apply (auto intro!: real_add_less_mono2 simp add: real_minus_zero_less_iff2 real_zero_less_one)
13.266 +done
13.267 +
13.268 +lemma real_add_minus_positive_less_self: "(0::real) < r ==> u + (-r) < u"
13.269 +apply (rule_tac C = "r" in real_less_add_right_cancel)
13.270 +apply (simp (no_asm) add: real_add_assoc)
13.271 +done
13.272 +
13.273 +lemma real_le_minus_iff: "(-s \<le> -r) = ((r::real) \<le> s)"
13.274 +apply (rule sym)
13.275 +apply safe
13.276 +apply (drule_tac x = "-s" in real_add_left_le_mono1)
13.277 +apply (drule_tac [2] x = "r" in real_add_left_le_mono1)
13.278 +apply auto
13.279 +apply (drule_tac z = "-r" in real_add_le_mono1)
13.280 +apply (drule_tac [2] z = "s" in real_add_le_mono1)
13.281 +apply (auto simp add: real_add_assoc)
13.282 +done
13.283 +declare real_le_minus_iff [simp]
13.284 +
13.285 +lemma real_le_square: "(0::real) \<le> x*x"
13.286 +apply (rule_tac real_linear_less2 [of x 0])
13.287 +apply (auto intro: real_mult_order neg_real_mult_order order_less_imp_le)
13.288 +done
13.289 +declare real_le_square [simp]
13.290 +
13.291 +lemma real_mult_less_mono1: "[| (0::real) < z; x < y |] ==> x*z < y*z"
13.292 +apply (rotate_tac 1)
13.293 +apply (drule real_less_sum_gt_zero)
13.294 +apply (rule real_sum_gt_zero_less)
13.295 +apply (drule real_mult_order , assumption)
13.296 +apply (simp add: real_add_mult_distrib2 real_mult_commute)
13.297 +done
13.298 +
13.299 +lemma real_mult_less_mono2: "[| (0::real) < z; x < y |] ==> z * x < z * y"
13.300 +apply (simp (no_asm_simp) add: real_mult_commute real_mult_less_mono1)
13.301 +done
13.302 +
13.303 +
13.304 +subsection{*The Reals Form an Ordered Field*}
13.305 +
13.306 +instance real :: inverse ..
13.307 +
13.308 +instance real :: ordered_field
13.309 +proof
13.310 + fix x y z :: real
13.311 + show "(x + y) + z = x + (y + z)" by (rule real_add_assoc)
13.312 + show "x + y = y + x" by (rule real_add_commute)
13.313 + show "0 + x = x" by simp
13.314 + show "- x + x = 0" by simp
13.315 + show "x - y = x + (-y)" by (simp add: real_diff_def)
13.316 + show "(x * y) * z = x * (y * z)" by (rule real_mult_assoc)
13.317 + show "x * y = y * x" by (rule real_mult_commute)
13.318 + show "1 * x = x" by simp
13.319 + show "(x + y) * z = x * z + y * z" by (simp add: real_add_mult_distrib)
13.320 + show "0 \<noteq> (1::real)" by (rule real_zero_not_eq_one)
13.321 + show "x \<le> y ==> z + x \<le> z + y" by simp
13.322 + show "x < y ==> 0 < z ==> z * x < z * y" by (simp add: real_mult_less_mono2)
13.323 + show "\<bar>x\<bar> = (if x < 0 then -x else x)"
13.324 + by (auto dest: order_le_less_trans simp add: real_abs_def linorder_not_le)
13.325 + show "x \<noteq> 0 ==> inverse x * x = 1" by simp;
13.326 + show "y \<noteq> 0 ==> x / y = x * inverse y" by (simp add: real_divide_def)
13.327 +qed
13.328 +
13.329 +
13.330 +
13.331 +(*----------------------------------------------------------------------------
13.332 + An embedding of the naturals in the reals
13.333 + ----------------------------------------------------------------------------*)
13.334 +
13.335 +lemma real_of_posnat_one: "real_of_posnat 0 = (1::real)"
13.336 +
13.337 +apply (unfold real_of_posnat_def)
13.338 +apply (simp (no_asm) add: pnat_one_iff [symmetric] real_of_preal_def symmetric real_one_def)
13.339 +done
13.340 +
13.341 +lemma real_of_posnat_two: "real_of_posnat (Suc 0) = (1::real) + (1::real)"
13.342 +apply (simp add: real_of_posnat_def real_of_preal_def real_one_def pnat_two_eq
13.343 + real_add
13.344 + prat_of_pnat_add [symmetric] preal_of_prat_add [symmetric]
13.345 + pnat_add_ac)
13.346 +done
13.347 +
13.348 +lemma real_of_posnat_add:
13.349 + "real_of_posnat n1 + real_of_posnat n2 = real_of_posnat (n1 + n2) + (1::real)"
13.350 +apply (unfold real_of_posnat_def)
13.351 +apply (simp (no_asm_use) add: real_of_posnat_one [symmetric] real_of_posnat_def real_of_preal_add [symmetric] preal_of_prat_add [symmetric] prat_of_pnat_add [symmetric] pnat_of_nat_add)
13.352 +done
13.353 +
13.354 +lemma real_of_posnat_add_one: "real_of_posnat (n + 1) = real_of_posnat n + (1::real)"
13.355 +apply (rule_tac x1 = " (1::real) " in real_add_right_cancel [THEN iffD1])
13.356 +apply (rule real_of_posnat_add [THEN subst])
13.357 +apply (simp (no_asm_use) add: real_of_posnat_two real_add_assoc)
13.358 +done
13.359 +
13.360 +lemma real_of_posnat_Suc: "real_of_posnat (Suc n) = real_of_posnat n + (1::real)"
13.361 +apply (subst real_of_posnat_add_one [symmetric])
13.362 +apply (simp (no_asm))
13.363 +done
13.364 +
13.365 +lemma inj_real_of_posnat: "inj(real_of_posnat)"
13.366 +apply (rule inj_onI)
13.367 +apply (unfold real_of_posnat_def)
13.368 +apply (drule inj_real_of_preal [THEN injD])
13.369 +apply (drule inj_preal_of_prat [THEN injD])
13.370 +apply (drule inj_prat_of_pnat [THEN injD])
13.371 +apply (erule inj_pnat_of_nat [THEN injD])
13.372 +done
13.373 +
13.374 +lemma real_of_nat_zero: "real (0::nat) = 0"
13.375 +apply (unfold real_of_nat_def)
13.376 +apply (simp (no_asm) add: real_of_posnat_one)
13.377 +done
13.378 +
13.379 +lemma real_of_nat_one: "real (Suc 0) = (1::real)"
13.380 +apply (unfold real_of_nat_def)
13.381 +apply (simp (no_asm) add: real_of_posnat_two real_add_assoc)
13.382 +done
13.383 +declare real_of_nat_zero [simp] real_of_nat_one [simp]
13.384 +
13.385 +lemma real_of_nat_add:
13.386 + "real (m + n) = real (m::nat) + real n"
13.387 +apply (simp add: real_of_nat_def real_add_assoc)
13.388 +apply (simp add: real_of_posnat_add real_add_assoc [symmetric])
13.389 +done
13.390 +declare real_of_nat_add [simp]
13.391 +
13.392 +(*Not for addsimps: often the LHS is used to represent a positive natural*)
13.393 +lemma real_of_nat_Suc: "real (Suc n) = real n + (1::real)"
13.394 +apply (unfold real_of_nat_def)
13.395 +apply (simp (no_asm) add: real_of_posnat_Suc real_add_ac)
13.396 +done
13.397 +
13.398 +lemma real_of_nat_less_iff:
13.399 + "(real (n::nat) < real m) = (n < m)"
13.400 +apply (unfold real_of_nat_def real_of_posnat_def)
13.401 +apply auto
13.402 +done
13.403 +declare real_of_nat_less_iff [iff]
13.404 +
13.405 +lemma real_of_nat_le_iff: "(real (n::nat) \<le> real m) = (n \<le> m)"
13.406 +apply (simp (no_asm) add: linorder_not_less [symmetric])
13.407 +done
13.408 +declare real_of_nat_le_iff [iff]
13.409 +
13.410 +lemma inj_real_of_nat: "inj (real :: nat => real)"
13.411 +apply (rule inj_onI)
13.412 +apply (auto intro!: inj_real_of_posnat [THEN injD]
13.413 + simp add: real_of_nat_def real_add_right_cancel)
13.414 +done
13.415 +
13.416 +lemma real_of_nat_ge_zero: "0 \<le> real (n::nat)"
13.417 +apply (induct_tac "n")
13.418 +apply (auto simp add: real_of_nat_Suc)
13.419 +apply (drule real_add_le_less_mono)
13.420 +apply (rule real_zero_less_one)
13.421 +apply (simp add: order_less_imp_le)
13.422 +done
13.423 +declare real_of_nat_ge_zero [iff]
13.424 +
13.425 +lemma real_of_nat_mult: "real (m * n) = real (m::nat) * real n"
13.426 +apply (induct_tac "m")
13.427 +apply (auto simp add: real_of_nat_Suc real_add_mult_distrib real_add_commute)
13.428 +done
13.429 +declare real_of_nat_mult [simp]
13.430 +
13.431 +lemma real_of_nat_inject: "(real (n::nat) = real m) = (n = m)"
13.432 +apply (auto dest: inj_real_of_nat [THEN injD])
13.433 +done
13.434 +declare real_of_nat_inject [iff]
13.435 +
13.436 +lemma real_of_nat_diff [rule_format (no_asm)]: "n \<le> m --> real (m - n) = real (m::nat) - real n"
13.437 +apply (induct_tac "m")
13.438 +apply (auto simp add: real_diff_def Suc_diff_le le_Suc_eq real_of_nat_Suc real_of_nat_zero real_add_ac)
13.439 +done
13.440 +
13.441 +lemma real_of_nat_zero_iff: "(real (n::nat) = 0) = (n = 0)"
13.442 + proof
13.443 + assume "real n = 0"
13.444 + have "real n = real (0::nat)" by simp
13.445 + then show "n = 0" by (simp only: real_of_nat_inject)
13.446 + next
13.447 + show "n = 0 \<Longrightarrow> real n = 0" by simp
13.448 + qed
13.449 +
13.450 +lemma real_of_nat_neg_int: "neg z ==> real (nat z) = 0"
13.451 +apply (simp (no_asm_simp) add: neg_nat real_of_nat_zero)
13.452 +done
13.453 +declare real_of_nat_neg_int [simp]
13.454 +
13.455 +
13.456 +(*----------------------------------------------------------------------------
13.457 + inverse, etc.
13.458 + ----------------------------------------------------------------------------*)
13.459 +
13.460 +lemma real_inverse_gt_0: "0 < x ==> 0 < inverse (x::real)"
13.461 +apply (rule ccontr)
13.462 +apply (drule real_leI)
13.463 +apply (frule real_minus_zero_less_iff2 [THEN iffD2])
13.464 +apply (frule real_not_refl2 [THEN not_sym])
13.465 +apply (drule real_not_refl2 [THEN not_sym, THEN real_inverse_not_zero])
13.466 +apply (drule order_le_imp_less_or_eq)
13.467 +apply safe;
13.468 +apply (drule neg_real_mult_order, assumption)
13.469 +apply (auto intro: real_zero_less_one [THEN real_less_asym])
13.470 +done
13.471 +
13.472 +lemma real_inverse_less_0: "x < 0 ==> inverse (x::real) < 0"
13.473 +apply (frule real_not_refl2)
13.474 +apply (drule real_minus_zero_less_iff [THEN iffD2])
13.475 +apply (rule real_minus_zero_less_iff [THEN iffD1])
13.476 +apply (subst real_minus_inverse [symmetric])
13.477 +apply (auto intro: real_inverse_gt_0)
13.478 +done
13.479 +
13.480 +lemma real_mult_less_cancel1: "[| (0::real) < z; x * z < y * z |] ==> x < y"
13.481 +apply (frule_tac x = "x*z" in real_inverse_gt_0 [THEN real_mult_less_mono1])
13.482 +apply (auto simp add: real_mult_assoc real_not_refl2 [THEN not_sym])
13.483 +done
13.484 +
13.485 +lemma real_mult_less_cancel2: "[| (0::real) < z; z*x < z*y |] ==> x < y"
13.486 +apply (erule real_mult_less_cancel1)
13.487 +apply (simp add: real_mult_commute)
13.488 +done
13.489 +
13.490 +lemma real_mult_less_iff1: "(0::real) < z ==> (x*z < y*z) = (x < y)"
13.491 +apply (blast intro: real_mult_less_mono1 real_mult_less_cancel1)
13.492 +done
13.493 +
13.494 +lemma real_mult_less_iff2: "(0::real) < z ==> (z*x < z*y) = (x < y)"
13.495 +apply (blast intro: real_mult_less_mono2 real_mult_less_cancel2)
13.496 +done
13.497 +
13.498 +declare real_mult_less_iff1 [simp] real_mult_less_iff2 [simp]
13.499 +
13.500 +(* 05/00 *)
13.501 +lemma real_mult_le_cancel_iff1: "(0::real) < z ==> (x*z \<le> y*z) = (x \<le> y)"
13.502 +apply (unfold real_le_def)
13.503 +apply auto
13.504 +done
13.505 +
13.506 +lemma real_mult_le_cancel_iff2: "(0::real) < z ==> (z*x \<le> z*y) = (x \<le> y)"
13.507 +apply (unfold real_le_def)
13.508 +apply auto
13.509 +done
13.510 +
13.511 +declare real_mult_le_cancel_iff1 [simp] real_mult_le_cancel_iff2 [simp]
13.512 +
13.513 +
13.514 +lemma real_mult_le_less_mono1: "[| (0::real) \<le> z; x < y |] ==> x*z \<le> y*z"
13.515 +apply (rule real_less_or_eq_imp_le)
13.516 +apply (drule order_le_imp_less_or_eq)
13.517 +apply (auto intro: real_mult_less_mono1)
13.518 +done
13.519 +
13.520 +lemma real_mult_less_mono: "[| u<v; x<y; (0::real) < v; 0 < x |] ==> u*x < v* y"
13.521 +apply (erule real_mult_less_mono1 [THEN order_less_trans])
13.522 +apply assumption
13.523 +apply (erule real_mult_less_mono2)
13.524 +apply assumption
13.525 +done
13.526 +
13.527 +(*Variant of the theorem above; sometimes it's stronger*)
13.528 +lemma real_mult_less_mono': "[| x < y; r1 < r2; (0::real) \<le> r1; 0 \<le> x|] ==> r1 * x < r2 * y"
13.529 +apply (subgoal_tac "0<r2")
13.530 +prefer 2 apply (blast intro: order_le_less_trans)
13.531 +apply (case_tac "x=0")
13.532 +apply (auto dest!: order_le_imp_less_or_eq intro: real_mult_less_mono real_mult_order)
13.533 +done
13.534 +
13.535 +lemma real_gt_zero: "(1::real) \<le> x ==> 0 < x"
13.536 +apply (rule ccontr , drule real_leI)
13.537 +apply (drule order_trans , assumption)
13.538 +apply (auto dest: real_zero_less_one [THEN [2] order_le_less_trans])
13.539 +done
13.540 +
13.541 +lemma real_mult_self_le: "[| (1::real) < r; (1::real) \<le> x |] ==> x \<le> r * x"
13.542 +apply (drule real_gt_zero [THEN order_less_imp_le])
13.543 +apply (auto dest!: real_mult_le_less_mono1)
13.544 +done
13.545 +
13.546 +lemma real_mult_self_le2: "[| (1::real) \<le> r; (1::real) \<le> x |] ==> x \<le> r * x"
13.547 +apply (drule order_le_imp_less_or_eq)
13.548 +apply (auto intro: real_mult_self_le)
13.549 +done
13.550 +
13.551 +lemma real_inverse_less_swap: "[| 0 < r; r < x |] ==> inverse x < inverse (r::real)"
13.552 +apply (frule order_less_trans , assumption)
13.553 +apply (frule real_inverse_gt_0)
13.554 +apply (frule_tac x = "x" in real_inverse_gt_0)
13.555 +apply (frule_tac x = "r" and z = "inverse r" in real_mult_less_mono1)
13.556 +apply assumption
13.557 +apply (simp add: real_not_refl2 [THEN not_sym, THEN real_mult_inv_right])
13.558 +apply (frule real_inverse_gt_0)
13.559 +apply (frule_tac x = " (1::real) " and z = "inverse x" in real_mult_less_mono2)
13.560 +apply assumption
13.561 +apply (simp add: real_not_refl2 [THEN not_sym, THEN real_mult_inv_left] real_mult_assoc [symmetric])
13.562 +done
13.563 +
13.564 +lemma real_mult_is_0: "(x*y = 0) = (x = 0 | y = (0::real))"
13.565 +apply auto
13.566 +done
13.567 +declare real_mult_is_0 [iff]
13.568 +
13.569 +lemma real_inverse_add: "[| x \<noteq> 0; y \<noteq> 0 |]
13.570 + ==> inverse x + inverse y = (x + y) * inverse (x * (y::real))"
13.571 +apply (simp add: real_inverse_distrib real_add_mult_distrib real_mult_assoc [symmetric])
13.572 +apply (subst real_mult_assoc)
13.573 +apply (rule real_mult_left_commute [THEN subst])
13.574 +apply (simp add: real_add_commute)
13.575 +done
13.576 +
13.577 +(* 05/00 *)
13.578 +lemma real_minus_zero_le_iff: "(0 \<le> -R) = (R \<le> (0::real))"
13.579 +apply (auto dest: sym simp add: real_le_less)
13.580 +done
13.581 +
13.582 +lemma real_minus_zero_le_iff2: "(-R \<le> 0) = ((0::real) \<le> R)"
13.583 +apply (auto simp add: real_minus_zero_less_iff2 real_le_less)
13.584 +done
13.585 +
13.586 +declare real_minus_zero_le_iff [simp] real_minus_zero_le_iff2 [simp]
13.587 +
13.588 +lemma real_sum_squares_cancel: "x * x + y * y = 0 ==> x = (0::real)"
13.589 +apply (drule real_add_minus_eq_minus)
13.590 +apply (cut_tac x = "x" in real_le_square)
13.591 +apply (auto , drule real_le_anti_sym)
13.592 +apply auto
13.593 +done
13.594 +
13.595 +lemma real_sum_squares_cancel2: "x * x + y * y = 0 ==> y = (0::real)"
13.596 +apply (rule_tac y = "x" in real_sum_squares_cancel)
13.597 +apply (simp add: real_add_commute)
13.598 +done
13.599 +
13.600 +(*----------------------------------------------------------------------------
13.601 + Some convenient biconditionals for products of signs (lcp)
13.602 + ----------------------------------------------------------------------------*)
13.603 +
13.604 +lemma real_0_less_mult_iff: "((0::real) < x*y) = (0<x & 0<y | x<0 & y<0)"
13.605 + by (rule Ring_and_Field.zero_less_mult_iff)
13.606 +
13.607 +lemma real_0_le_mult_iff: "((0::real)\<le>x*y) = (0\<le>x & 0\<le>y | x\<le>0 & y\<le>0)"
13.608 + by (rule zero_le_mult_iff)
13.609 +
13.610 +lemma real_mult_less_0_iff: "(x*y < (0::real)) = (0<x & y<0 | x<0 & 0<y)"
13.611 + by (rule mult_less_0_iff)
13.612 +
13.613 +lemma real_mult_le_0_iff: "(x*y \<le> (0::real)) = (0\<le>x & y\<le>0 | x\<le>0 & 0\<le>y)"
13.614 + by (rule mult_le_0_iff)
13.615 +
13.616 +
13.617 +ML
13.618 +{*
13.619 +val real_abs_def = thm "real_abs_def";
13.620 +
13.621 +val real_minus_diff_eq = thm "real_minus_diff_eq";
13.622 +val real_gt_zero_preal_Ex = thm "real_gt_zero_preal_Ex";
13.623 +val real_gt_preal_preal_Ex = thm "real_gt_preal_preal_Ex";
13.624 +val real_ge_preal_preal_Ex = thm "real_ge_preal_preal_Ex";
13.625 +val real_less_all_preal = thm "real_less_all_preal";
13.626 +val real_less_all_real2 = thm "real_less_all_real2";
13.627 +val real_lemma_add_positive_imp_less = thm "real_lemma_add_positive_imp_less";
13.628 +val real_ex_add_positive_left_less = thm "real_ex_add_positive_left_less";
13.629 +val real_less_iff_add = thm "real_less_iff_add";
13.630 +val real_of_preal_le_iff = thm "real_of_preal_le_iff";
13.631 +val real_mult_order = thm "real_mult_order";
13.632 +val neg_real_mult_order = thm "neg_real_mult_order";
13.633 +val real_mult_less_0 = thm "real_mult_less_0";
13.634 +val real_zero_less_one = thm "real_zero_less_one";
13.635 +val real_add_right_cancel_less = thm "real_add_right_cancel_less";
13.636 +val real_add_left_cancel_less = thm "real_add_left_cancel_less";
13.637 +val real_add_right_cancel_le = thm "real_add_right_cancel_le";
13.638 +val real_add_left_cancel_le = thm "real_add_left_cancel_le";
13.639 +val real_add_less_mono1 = thm "real_add_less_mono1";
13.640 +val real_add_le_mono1 = thm "real_add_le_mono1";
13.641 +val real_add_less_le_mono = thm "real_add_less_le_mono";
13.642 +val real_add_le_less_mono = thm "real_add_le_less_mono";
13.643 +val real_add_less_mono2 = thm "real_add_less_mono2";
13.644 +val real_less_add_right_cancel = thm "real_less_add_right_cancel";
13.645 +val real_less_add_left_cancel = thm "real_less_add_left_cancel";
13.646 +val real_le_add_right_cancel = thm "real_le_add_right_cancel";
13.647 +val real_le_add_left_cancel = thm "real_le_add_left_cancel";
13.648 +val real_add_order = thm "real_add_order";
13.649 +val real_le_add_order = thm "real_le_add_order";
13.650 +val real_add_less_mono = thm "real_add_less_mono";
13.651 +val real_add_left_le_mono1 = thm "real_add_left_le_mono1";
13.652 +val real_add_le_mono = thm "real_add_le_mono";
13.653 +val real_less_Ex = thm "real_less_Ex";
13.654 +val real_add_minus_positive_less_self = thm "real_add_minus_positive_less_self";
13.655 +val real_le_minus_iff = thm "real_le_minus_iff";
13.656 +val real_le_square = thm "real_le_square";
13.657 +val real_mult_less_mono1 = thm "real_mult_less_mono1";
13.658 +val real_mult_less_mono2 = thm "real_mult_less_mono2";
13.659 +val real_of_posnat_one = thm "real_of_posnat_one";
13.660 +val real_of_posnat_two = thm "real_of_posnat_two";
13.661 +val real_of_posnat_add = thm "real_of_posnat_add";
13.662 +val real_of_posnat_add_one = thm "real_of_posnat_add_one";
13.663 +val real_of_posnat_Suc = thm "real_of_posnat_Suc";
13.664 +val inj_real_of_posnat = thm "inj_real_of_posnat";
13.665 +val real_of_nat_zero = thm "real_of_nat_zero";
13.666 +val real_of_nat_one = thm "real_of_nat_one";
13.667 +val real_of_nat_add = thm "real_of_nat_add";
13.668 +val real_of_nat_Suc = thm "real_of_nat_Suc";
13.669 +val real_of_nat_less_iff = thm "real_of_nat_less_iff";
13.670 +val real_of_nat_le_iff = thm "real_of_nat_le_iff";
13.671 +val inj_real_of_nat = thm "inj_real_of_nat";
13.672 +val real_of_nat_ge_zero = thm "real_of_nat_ge_zero";
13.673 +val real_of_nat_mult = thm "real_of_nat_mult";
13.674 +val real_of_nat_inject = thm "real_of_nat_inject";
13.675 +val real_of_nat_diff = thm "real_of_nat_diff";
13.676 +val real_of_nat_zero_iff = thm "real_of_nat_zero_iff";
13.677 +val real_of_nat_neg_int = thm "real_of_nat_neg_int";
13.678 +val real_inverse_gt_0 = thm "real_inverse_gt_0";
13.679 +val real_inverse_less_0 = thm "real_inverse_less_0";
13.680 +val real_mult_less_cancel1 = thm "real_mult_less_cancel1";
13.681 +val real_mult_less_cancel2 = thm "real_mult_less_cancel2";
13.682 +val real_mult_less_iff1 = thm "real_mult_less_iff1";
13.683 +val real_mult_less_iff2 = thm "real_mult_less_iff2";
13.684 +val real_mult_le_cancel_iff1 = thm "real_mult_le_cancel_iff1";
13.685 +val real_mult_le_cancel_iff2 = thm "real_mult_le_cancel_iff2";
13.686 +val real_mult_le_less_mono1 = thm "real_mult_le_less_mono1";
13.687 +val real_mult_less_mono = thm "real_mult_less_mono";
13.688 +val real_mult_less_mono' = thm "real_mult_less_mono'";
13.689 +val real_gt_zero = thm "real_gt_zero";
13.690 +val real_mult_self_le = thm "real_mult_self_le";
13.691 +val real_mult_self_le2 = thm "real_mult_self_le2";
13.692 +val real_inverse_less_swap = thm "real_inverse_less_swap";
13.693 +val real_mult_is_0 = thm "real_mult_is_0";
13.694 +val real_inverse_add = thm "real_inverse_add";
13.695 +val real_minus_zero_le_iff = thm "real_minus_zero_le_iff";
13.696 +val real_minus_zero_le_iff2 = thm "real_minus_zero_le_iff2";
13.697 +val real_sum_squares_cancel = thm "real_sum_squares_cancel";
13.698 +val real_sum_squares_cancel2 = thm "real_sum_squares_cancel2";
13.699 +val real_0_less_mult_iff = thm "real_0_less_mult_iff";
13.700 +val real_0_le_mult_iff = thm "real_0_le_mult_iff";
13.701 +val real_mult_less_0_iff = thm "real_mult_less_0_iff";
13.702 +val real_mult_le_0_iff = thm "real_mult_le_0_iff";
13.703 +*}
13.704
13.705 end
14.1 --- a/src/HOL/Real/RealPow.ML Thu Nov 20 10:42:00 2003 +0100
14.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
14.3 @@ -1,388 +0,0 @@
14.4 -(* Title : RealPow.ML
14.5 - ID : $Id$
14.6 - Author : Jacques D. Fleuriot
14.7 - Copyright : 1998 University of Cambridge
14.8 - Description : Natural Powers of reals theory
14.9 -
14.10 -FIXME: most of the theorems for Suc (Suc 0) are redundant!
14.11 -*)
14.12 -
14.13 -bind_thm ("realpow_Suc", thm "realpow_Suc");
14.14 -
14.15 -Goal "(0::real) ^ (Suc n) = 0";
14.16 -by Auto_tac;
14.17 -qed "realpow_zero";
14.18 -Addsimps [realpow_zero];
14.19 -
14.20 -Goal "r ~= (0::real) --> r ^ n ~= 0";
14.21 -by (induct_tac "n" 1);
14.22 -by Auto_tac;
14.23 -qed_spec_mp "realpow_not_zero";
14.24 -
14.25 -Goal "r ^ n = (0::real) ==> r = 0";
14.26 -by (rtac ccontr 1);
14.27 -by (auto_tac (claset() addDs [realpow_not_zero], simpset()));
14.28 -qed "realpow_zero_zero";
14.29 -
14.30 -Goal "inverse ((r::real) ^ n) = (inverse r) ^ n";
14.31 -by (induct_tac "n" 1);
14.32 -by (auto_tac (claset(), simpset() addsimps [real_inverse_distrib]));
14.33 -qed "realpow_inverse";
14.34 -
14.35 -Goal "abs(r ^ n) = abs(r::real) ^ n";
14.36 -by (induct_tac "n" 1);
14.37 -by (auto_tac (claset(), simpset() addsimps [abs_mult]));
14.38 -qed "realpow_abs";
14.39 -
14.40 -Goal "(r::real) ^ (n + m) = (r ^ n) * (r ^ m)";
14.41 -by (induct_tac "n" 1);
14.42 -by (auto_tac (claset(),simpset() addsimps real_mult_ac));
14.43 -qed "realpow_add";
14.44 -
14.45 -Goal "(r::real) ^ 1 = r";
14.46 -by (Simp_tac 1);
14.47 -qed "realpow_one";
14.48 -Addsimps [realpow_one];
14.49 -
14.50 -Goal "(r::real)^ (Suc (Suc 0)) = r * r";
14.51 -by (Simp_tac 1);
14.52 -qed "realpow_two";
14.53 -
14.54 -Goal "(0::real) < r --> 0 < r ^ n";
14.55 -by (induct_tac "n" 1);
14.56 -by (auto_tac (claset() addIs [real_mult_order],
14.57 - simpset() addsimps [real_zero_less_one]));
14.58 -qed_spec_mp "realpow_gt_zero";
14.59 -
14.60 -Goal "(0::real) <= r --> 0 <= r ^ n";
14.61 -by (induct_tac "n" 1);
14.62 -by (auto_tac (claset(), simpset() addsimps [real_0_le_mult_iff]));
14.63 -qed_spec_mp "realpow_ge_zero";
14.64 -
14.65 -Goal "(0::real) <= x & x <= y --> x ^ n <= y ^ n";
14.66 -by (induct_tac "n" 1);
14.67 -by (auto_tac (claset() addSIs [real_mult_le_mono], simpset()));
14.68 -by (asm_simp_tac (simpset() addsimps [realpow_ge_zero]) 1);
14.69 -qed_spec_mp "realpow_le";
14.70 -
14.71 -Goal "(0::real) < x & x < y & 0 < n --> x ^ n < y ^ n";
14.72 -by (induct_tac "n" 1);
14.73 -by (auto_tac (claset() addIs [real_mult_less_mono, gr0I]
14.74 - addDs [realpow_gt_zero],
14.75 - simpset()));
14.76 -qed_spec_mp "realpow_less";
14.77 -
14.78 -Goal "1 ^ n = (1::real)";
14.79 -by (induct_tac "n" 1);
14.80 -by Auto_tac;
14.81 -qed "realpow_eq_one";
14.82 -Addsimps [realpow_eq_one];
14.83 -
14.84 -Goal "abs((-1) ^ n) = (1::real)";
14.85 -by (induct_tac "n" 1);
14.86 -by (auto_tac (claset(), simpset() addsimps [abs_mult]));
14.87 -qed "abs_realpow_minus_one";
14.88 -Addsimps [abs_realpow_minus_one];
14.89 -
14.90 -Goal "((r::real) * s) ^ n = (r ^ n) * (s ^ n)";
14.91 -by (induct_tac "n" 1);
14.92 -by (auto_tac (claset(),simpset() addsimps real_mult_ac));
14.93 -qed "realpow_mult";
14.94 -
14.95 -Goal "(0::real) <= r^ Suc (Suc 0)";
14.96 -by (simp_tac (simpset() addsimps [real_le_square]) 1);
14.97 -qed "realpow_two_le";
14.98 -Addsimps [realpow_two_le];
14.99 -
14.100 -Goal "abs((x::real)^Suc (Suc 0)) = x^Suc (Suc 0)";
14.101 -by (simp_tac (simpset() addsimps [abs_eqI1,
14.102 - real_le_square]) 1);
14.103 -qed "abs_realpow_two";
14.104 -Addsimps [abs_realpow_two];
14.105 -
14.106 -Goal "abs(x::real)^Suc (Suc 0) = x^Suc (Suc 0)";
14.107 -by (simp_tac (simpset() addsimps [realpow_abs RS sym,abs_eqI1]
14.108 - delsimps [realpow_Suc]) 1);
14.109 -qed "realpow_two_abs";
14.110 -Addsimps [realpow_two_abs];
14.111 -
14.112 -Goal "(1::real) < r ==> 1 < r^ (Suc (Suc 0))";
14.113 -by Auto_tac;
14.114 -by (cut_facts_tac [real_zero_less_one] 1);
14.115 -by (forw_inst_tac [("x","0")] order_less_trans 1);
14.116 -by (assume_tac 1);
14.117 -by (dres_inst_tac [("z","r"),("x","1")]
14.118 - (real_mult_less_mono1) 1);
14.119 -by (auto_tac (claset() addIs [order_less_trans], simpset()));
14.120 -qed "realpow_two_gt_one";
14.121 -
14.122 -Goal "(1::real) < r --> 1 <= r ^ n";
14.123 -by (induct_tac "n" 1);
14.124 -by Auto_tac;
14.125 -by (subgoal_tac "1*1 <= r * r^n" 1);
14.126 -by (rtac real_mult_le_mono 2);
14.127 -by Auto_tac;
14.128 -qed_spec_mp "realpow_ge_one";
14.129 -
14.130 -Goal "(1::real) <= r ==> 1 <= r ^ n";
14.131 -by (dtac order_le_imp_less_or_eq 1);
14.132 -by (auto_tac (claset() addDs [realpow_ge_one], simpset()));
14.133 -qed "realpow_ge_one2";
14.134 -
14.135 -Goal "(1::real) <= 2 ^ n";
14.136 -by (res_inst_tac [("y","1 ^ n")] order_trans 1);
14.137 -by (rtac realpow_le 2);
14.138 -by (auto_tac (claset() addIs [order_less_imp_le], simpset()));
14.139 -qed "two_realpow_ge_one";
14.140 -
14.141 -Goal "real (n::nat) < 2 ^ n";
14.142 -by (induct_tac "n" 1);
14.143 -by (auto_tac (claset(), simpset() addsimps [real_of_nat_Suc]));
14.144 -by (stac real_mult_2 1);
14.145 -by (rtac real_add_less_le_mono 1);
14.146 -by (auto_tac (claset(), simpset() addsimps [two_realpow_ge_one]));
14.147 -qed "two_realpow_gt";
14.148 -Addsimps [two_realpow_gt,two_realpow_ge_one];
14.149 -
14.150 -Goal "(-1) ^ (2*n) = (1::real)";
14.151 -by (induct_tac "n" 1);
14.152 -by Auto_tac;
14.153 -qed "realpow_minus_one";
14.154 -Addsimps [realpow_minus_one];
14.155 -
14.156 -Goal "(-1) ^ Suc (2*n) = -(1::real)";
14.157 -by Auto_tac;
14.158 -qed "realpow_minus_one_odd";
14.159 -Addsimps [realpow_minus_one_odd];
14.160 -
14.161 -Goal "(-1) ^ Suc (Suc (2*n)) = (1::real)";
14.162 -by Auto_tac;
14.163 -qed "realpow_minus_one_even";
14.164 -Addsimps [realpow_minus_one_even];
14.165 -
14.166 -Goal "(0::real) < r & r < (1::real) --> r ^ Suc n < r ^ n";
14.167 -by (induct_tac "n" 1);
14.168 -by Auto_tac;
14.169 -qed_spec_mp "realpow_Suc_less";
14.170 -
14.171 -Goal "0 <= r & r < (1::real) --> r ^ Suc n <= r ^ n";
14.172 -by (induct_tac "n" 1);
14.173 -by (auto_tac (claset() addIs [order_less_imp_le]
14.174 - addSDs [order_le_imp_less_or_eq],
14.175 - simpset()));
14.176 -qed_spec_mp "realpow_Suc_le";
14.177 -
14.178 -Goal "(0::real) <= 0 ^ n";
14.179 -by (case_tac "n" 1);
14.180 -by Auto_tac;
14.181 -qed "realpow_zero_le";
14.182 -Addsimps [realpow_zero_le];
14.183 -
14.184 -Goal "0 < r & r < (1::real) --> r ^ Suc n <= r ^ n";
14.185 -by (blast_tac (claset() addSIs [order_less_imp_le,
14.186 - realpow_Suc_less]) 1);
14.187 -qed_spec_mp "realpow_Suc_le2";
14.188 -
14.189 -Goal "[| 0 <= r; r < (1::real) |] ==> r ^ Suc n <= r ^ n";
14.190 -by (etac (order_le_imp_less_or_eq RS disjE) 1);
14.191 -by (rtac realpow_Suc_le2 1);
14.192 -by Auto_tac;
14.193 -qed "realpow_Suc_le3";
14.194 -
14.195 -Goal "0 <= r & r < (1::real) & n < N --> r ^ N <= r ^ n";
14.196 -by (induct_tac "N" 1);
14.197 -by (ALLGOALS Asm_simp_tac);
14.198 -by (Clarify_tac 1);
14.199 -by (subgoal_tac "r * r ^ na <= 1 * r ^ n" 1);
14.200 -by (Asm_full_simp_tac 1);
14.201 -by (rtac real_mult_le_mono 1);
14.202 -by (auto_tac (claset(), simpset() addsimps [realpow_ge_zero, less_Suc_eq]));
14.203 -qed_spec_mp "realpow_less_le";
14.204 -
14.205 -Goal "[| 0 <= r; r < (1::real); n <= N |] ==> r ^ N <= r ^ n";
14.206 -by (dres_inst_tac [("n","N")] le_imp_less_or_eq 1);
14.207 -by (auto_tac (claset() addIs [realpow_less_le],
14.208 - simpset()));
14.209 -qed "realpow_le_le";
14.210 -
14.211 -Goal "[| 0 < r; r < (1::real) |] ==> r ^ Suc n <= r";
14.212 -by (dres_inst_tac [("n","1"),("N","Suc n")]
14.213 - (order_less_imp_le RS realpow_le_le) 1);
14.214 -by Auto_tac;
14.215 -qed "realpow_Suc_le_self";
14.216 -
14.217 -Goal "[| 0 < r; r < (1::real) |] ==> r ^ Suc n < 1";
14.218 -by (blast_tac (claset() addIs [realpow_Suc_le_self, order_le_less_trans]) 1);
14.219 -qed "realpow_Suc_less_one";
14.220 -
14.221 -Goal "(1::real) <= r --> r ^ n <= r ^ Suc n";
14.222 -by (induct_tac "n" 1);
14.223 -by Auto_tac;
14.224 -qed_spec_mp "realpow_le_Suc";
14.225 -
14.226 -Goal "(1::real) < r --> r ^ n < r ^ Suc n";
14.227 -by (induct_tac "n" 1);
14.228 -by Auto_tac;
14.229 -qed_spec_mp "realpow_less_Suc";
14.230 -
14.231 -Goal "(1::real) < r --> r ^ n <= r ^ Suc n";
14.232 -by (blast_tac (claset() addSIs [order_less_imp_le, realpow_less_Suc]) 1);
14.233 -qed_spec_mp "realpow_le_Suc2";
14.234 -
14.235 -Goal "(1::real) < r & n < N --> r ^ n <= r ^ N";
14.236 -by (induct_tac "N" 1);
14.237 -by Auto_tac;
14.238 -by (ALLGOALS(forw_inst_tac [("n","na")] realpow_ge_one));
14.239 -by (ALLGOALS(dtac (real_mult_self_le)));
14.240 -by (assume_tac 1);
14.241 -by (assume_tac 2);
14.242 -by (auto_tac (claset() addIs [order_trans],
14.243 - simpset() addsimps [less_Suc_eq]));
14.244 -qed_spec_mp "realpow_gt_ge";
14.245 -
14.246 -Goal "(1::real) <= r & n < N --> r ^ n <= r ^ N";
14.247 -by (induct_tac "N" 1);
14.248 -by Auto_tac;
14.249 -by (ALLGOALS(forw_inst_tac [("n","na")] realpow_ge_one2));
14.250 -by (ALLGOALS(dtac (real_mult_self_le2)));
14.251 -by (assume_tac 1);
14.252 -by (assume_tac 2);
14.253 -by (auto_tac (claset() addIs [order_trans],
14.254 - simpset() addsimps [less_Suc_eq]));
14.255 -qed_spec_mp "realpow_gt_ge2";
14.256 -
14.257 -Goal "[| (1::real) < r; n <= N |] ==> r ^ n <= r ^ N";
14.258 -by (dres_inst_tac [("n","N")] le_imp_less_or_eq 1);
14.259 -by (auto_tac (claset() addIs [realpow_gt_ge], simpset()));
14.260 -qed "realpow_ge_ge";
14.261 -
14.262 -Goal "[| (1::real) <= r; n <= N |] ==> r ^ n <= r ^ N";
14.263 -by (dres_inst_tac [("n","N")] le_imp_less_or_eq 1);
14.264 -by (auto_tac (claset() addIs [realpow_gt_ge2], simpset()));
14.265 -qed "realpow_ge_ge2";
14.266 -
14.267 -Goal "(1::real) < r ==> r <= r ^ Suc n";
14.268 -by (dres_inst_tac [("n","1"),("N","Suc n")]
14.269 - realpow_ge_ge 1);
14.270 -by Auto_tac;
14.271 -qed_spec_mp "realpow_Suc_ge_self";
14.272 -
14.273 -Goal "(1::real) <= r ==> r <= r ^ Suc n";
14.274 -by (dres_inst_tac [("n","1"),("N","Suc n")]
14.275 - realpow_ge_ge2 1);
14.276 -by Auto_tac;
14.277 -qed_spec_mp "realpow_Suc_ge_self2";
14.278 -
14.279 -Goal "[| (1::real) < r; 0 < n |] ==> r <= r ^ n";
14.280 -by (dtac (less_not_refl2 RS not0_implies_Suc) 1);
14.281 -by (auto_tac (claset() addSIs
14.282 - [realpow_Suc_ge_self],simpset()));
14.283 -qed "realpow_ge_self";
14.284 -
14.285 -Goal "[| (1::real) <= r; 0 < n |] ==> r <= r ^ n";
14.286 -by (dtac (less_not_refl2 RS not0_implies_Suc) 1);
14.287 -by (auto_tac (claset() addSIs [realpow_Suc_ge_self2],simpset()));
14.288 -qed "realpow_ge_self2";
14.289 -
14.290 -Goal "0 < n --> (x::real) ^ (n - 1) * x = x ^ n";
14.291 -by (induct_tac "n" 1);
14.292 -by (auto_tac (claset(),simpset()
14.293 - addsimps [real_mult_commute]));
14.294 -qed_spec_mp "realpow_minus_mult";
14.295 -Addsimps [realpow_minus_mult];
14.296 -
14.297 -Goal "r ~= 0 ==> r * inverse r ^Suc (Suc 0) = inverse (r::real)";
14.298 -by (asm_simp_tac (simpset() addsimps [realpow_two,
14.299 - real_mult_assoc RS sym]) 1);
14.300 -qed "realpow_two_mult_inverse";
14.301 -Addsimps [realpow_two_mult_inverse];
14.302 -
14.303 -(* 05/00 *)
14.304 -Goal "(-x)^Suc (Suc 0) = (x::real)^Suc (Suc 0)";
14.305 -by (Simp_tac 1);
14.306 -qed "realpow_two_minus";
14.307 -Addsimps [realpow_two_minus];
14.308 -
14.309 -Goalw [real_diff_def] "(x::real)^Suc (Suc 0) - y^Suc (Suc 0) = (x - y) * (x + y)";
14.310 -by (simp_tac (simpset() addsimps
14.311 - [real_add_mult_distrib2, real_add_mult_distrib] @ real_mult_ac) 1);
14.312 -qed "realpow_two_diff";
14.313 -
14.314 -Goalw [real_diff_def] "((x::real)^Suc (Suc 0) = y^Suc (Suc 0)) = (x = y | x = -y)";
14.315 -by (cut_inst_tac [("x","x"),("y","y")] realpow_two_diff 1);
14.316 -by (auto_tac (claset(), simpset() delsimps [realpow_Suc]));
14.317 -qed "realpow_two_disj";
14.318 -
14.319 -(* used in Transc *)
14.320 -Goal "[|(x::real) ~= 0; m <= n |] ==> x ^ (n - m) = x ^ n * inverse (x ^ m)";
14.321 -by (auto_tac (claset(),
14.322 - simpset() addsimps [le_eq_less_or_eq, less_iff_Suc_add, realpow_add,
14.323 - realpow_not_zero] @ real_mult_ac));
14.324 -qed "realpow_diff";
14.325 -
14.326 -Goal "real (m::nat) ^ n = real (m ^ n)";
14.327 -by (induct_tac "n" 1);
14.328 -by (auto_tac (claset(),
14.329 - simpset() addsimps [real_of_nat_one, real_of_nat_mult]));
14.330 -qed "realpow_real_of_nat";
14.331 -
14.332 -Goal "0 < real (Suc (Suc 0) ^ n)";
14.333 -by (induct_tac "n" 1);
14.334 -by (auto_tac (claset(),
14.335 - simpset() addsimps [real_of_nat_mult, real_0_less_mult_iff]));
14.336 -qed "realpow_real_of_nat_two_pos";
14.337 -Addsimps [realpow_real_of_nat_two_pos];
14.338 -
14.339 -
14.340 -Goal "(0::real) <= x --> 0 <= y --> x ^ Suc n <= y ^ Suc n --> x <= y";
14.341 -by (induct_tac "n" 1);
14.342 -by Auto_tac;
14.343 -by (asm_full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
14.344 -by (swap_res_tac [real_mult_less_mono'] 1);
14.345 -by Auto_tac;
14.346 -by (auto_tac (claset(), simpset() addsimps [real_0_le_mult_iff]));
14.347 -by (auto_tac (claset(), simpset() addsimps [linorder_not_less RS sym]));
14.348 -by (dres_inst_tac [("n","n")] realpow_gt_zero 1);
14.349 -by Auto_tac;
14.350 -qed_spec_mp "realpow_increasing";
14.351 -
14.352 -Goal "[| (0::real) <= x; 0 <= y; x ^ Suc n = y ^ Suc n |] ==> x = y";
14.353 -by (blast_tac (claset() addIs [realpow_increasing, order_antisym,
14.354 - order_eq_refl, sym]) 1);
14.355 -qed_spec_mp "realpow_Suc_cancel_eq";
14.356 -
14.357 -
14.358 -(*** Logical equivalences for inequalities ***)
14.359 -
14.360 -Goal "(x^n = 0) = (x = (0::real) & 0<n)";
14.361 -by (induct_tac "n" 1);
14.362 -by Auto_tac;
14.363 -qed "realpow_eq_0_iff";
14.364 -Addsimps [realpow_eq_0_iff];
14.365 -
14.366 -Goal "(0 < (abs x)^n) = (x ~= (0::real) | n=0)";
14.367 -by (induct_tac "n" 1);
14.368 -by (auto_tac (claset(), simpset() addsimps [real_0_less_mult_iff]));
14.369 -qed "zero_less_realpow_abs_iff";
14.370 -Addsimps [zero_less_realpow_abs_iff];
14.371 -
14.372 -Goal "(0::real) <= (abs x)^n";
14.373 -by (induct_tac "n" 1);
14.374 -by (auto_tac (claset(), simpset() addsimps [real_0_le_mult_iff]));
14.375 -qed "zero_le_realpow_abs";
14.376 -Addsimps [zero_le_realpow_abs];
14.377 -
14.378 -
14.379 -(*** Literal arithmetic involving powers, type real ***)
14.380 -
14.381 -Goal "real (x::int) ^ n = real (x ^ n)";
14.382 -by (induct_tac "n" 1);
14.383 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [nat_mult_distrib])));
14.384 -qed "real_of_int_power";
14.385 -Addsimps [real_of_int_power RS sym];
14.386 -
14.387 -Goal "(number_of v :: real) ^ n = real ((number_of v :: int) ^ n)";
14.388 -by (simp_tac (HOL_ss addsimps [real_number_of_def, real_of_int_power]) 1);
14.389 -qed "power_real_number_of";
14.390 -
14.391 -Addsimps [inst "n" "number_of ?w" power_real_number_of];
15.1 --- a/src/HOL/Real/RealPow.thy Thu Nov 20 10:42:00 2003 +0100
15.2 +++ b/src/HOL/Real/RealPow.thy Fri Nov 21 11:15:40 2003 +0100
15.3 @@ -11,11 +11,477 @@
15.4 (*belongs to theory RealAbs*)
15.5 lemmas [arith_split] = abs_split
15.6
15.7 -
15.8 instance real :: power ..
15.9
15.10 primrec (realpow)
15.11 realpow_0: "r ^ 0 = 1"
15.12 realpow_Suc: "r ^ (Suc n) = (r::real) * (r ^ n)"
15.13
15.14 +
15.15 +(*FIXME: most of the theorems for Suc (Suc 0) are redundant!
15.16 +*)
15.17 +
15.18 +lemma realpow_zero: "(0::real) ^ (Suc n) = 0"
15.19 +apply auto
15.20 +done
15.21 +declare realpow_zero [simp]
15.22 +
15.23 +lemma realpow_not_zero [rule_format (no_asm)]: "r \<noteq> (0::real) --> r ^ n \<noteq> 0"
15.24 +apply (induct_tac "n")
15.25 +apply auto
15.26 +done
15.27 +
15.28 +lemma realpow_zero_zero: "r ^ n = (0::real) ==> r = 0"
15.29 +apply (rule ccontr)
15.30 +apply (auto dest: realpow_not_zero)
15.31 +done
15.32 +
15.33 +lemma realpow_inverse: "inverse ((r::real) ^ n) = (inverse r) ^ n"
15.34 +apply (induct_tac "n")
15.35 +apply (auto simp add: real_inverse_distrib)
15.36 +done
15.37 +
15.38 +lemma realpow_abs: "abs(r ^ n) = abs(r::real) ^ n"
15.39 +apply (induct_tac "n")
15.40 +apply (auto simp add: abs_mult)
15.41 +done
15.42 +
15.43 +lemma realpow_add: "(r::real) ^ (n + m) = (r ^ n) * (r ^ m)"
15.44 +apply (induct_tac "n")
15.45 +apply (auto simp add: real_mult_ac)
15.46 +done
15.47 +
15.48 +lemma realpow_one: "(r::real) ^ 1 = r"
15.49 +apply (simp (no_asm))
15.50 +done
15.51 +declare realpow_one [simp]
15.52 +
15.53 +lemma realpow_two: "(r::real)^ (Suc (Suc 0)) = r * r"
15.54 +apply (simp (no_asm))
15.55 +done
15.56 +
15.57 +lemma realpow_gt_zero [rule_format (no_asm)]: "(0::real) < r --> 0 < r ^ n"
15.58 +apply (induct_tac "n")
15.59 +apply (auto intro: real_mult_order simp add: real_zero_less_one)
15.60 +done
15.61 +
15.62 +lemma realpow_ge_zero [rule_format (no_asm)]: "(0::real) \<le> r --> 0 \<le> r ^ n"
15.63 +apply (induct_tac "n")
15.64 +apply (auto simp add: real_0_le_mult_iff)
15.65 +done
15.66 +
15.67 +lemma realpow_le [rule_format (no_asm)]: "(0::real) \<le> x & x \<le> y --> x ^ n \<le> y ^ n"
15.68 +apply (induct_tac "n")
15.69 +apply (auto intro!: real_mult_le_mono)
15.70 +apply (simp (no_asm_simp) add: realpow_ge_zero)
15.71 +done
15.72 +
15.73 +lemma realpow_0_left [rule_format, simp]:
15.74 + "0 < n --> 0 ^ n = (0::real)"
15.75 +apply (induct_tac "n")
15.76 +apply (auto );
15.77 +done
15.78 +
15.79 +lemma realpow_less' [rule_format]:
15.80 + "[|(0::real) \<le> x; x < y |] ==> 0 < n --> x ^ n < y ^ n"
15.81 +apply (induct n)
15.82 +apply (auto simp add: real_mult_less_mono' realpow_ge_zero);
15.83 +done
15.84 +
15.85 +text{*Legacy: weaker version of the theorem above*}
15.86 +lemma realpow_less [rule_format]:
15.87 + "[|(0::real) < x; x < y; 0 < n|] ==> x ^ n < y ^ n"
15.88 +apply (rule realpow_less')
15.89 +apply (auto );
15.90 +done
15.91 +
15.92 +lemma realpow_eq_one: "1 ^ n = (1::real)"
15.93 +apply (induct_tac "n")
15.94 +apply auto
15.95 +done
15.96 +declare realpow_eq_one [simp]
15.97 +
15.98 +lemma abs_realpow_minus_one: "abs((-1) ^ n) = (1::real)"
15.99 +apply (induct_tac "n")
15.100 +apply (auto simp add: abs_mult)
15.101 +done
15.102 +declare abs_realpow_minus_one [simp]
15.103 +
15.104 +lemma realpow_mult: "((r::real) * s) ^ n = (r ^ n) * (s ^ n)"
15.105 +apply (induct_tac "n")
15.106 +apply (auto simp add: real_mult_ac)
15.107 +done
15.108 +
15.109 +lemma realpow_two_le: "(0::real) \<le> r^ Suc (Suc 0)"
15.110 +apply (simp (no_asm) add: real_le_square)
15.111 +done
15.112 +declare realpow_two_le [simp]
15.113 +
15.114 +lemma abs_realpow_two: "abs((x::real)^Suc (Suc 0)) = x^Suc (Suc 0)"
15.115 +apply (simp (no_asm) add: abs_eqI1 real_le_square)
15.116 +done
15.117 +declare abs_realpow_two [simp]
15.118 +
15.119 +lemma realpow_two_abs: "abs(x::real)^Suc (Suc 0) = x^Suc (Suc 0)"
15.120 +apply (simp (no_asm) add: realpow_abs [symmetric] abs_eqI1 del: realpow_Suc)
15.121 +done
15.122 +declare realpow_two_abs [simp]
15.123 +
15.124 +lemma realpow_two_gt_one: "(1::real) < r ==> 1 < r^ (Suc (Suc 0))"
15.125 +apply auto
15.126 +apply (cut_tac real_zero_less_one)
15.127 +apply (frule_tac x = "0" in order_less_trans)
15.128 +apply assumption
15.129 +apply (drule_tac z = "r" and x = "1" in real_mult_less_mono1)
15.130 +apply (auto intro: order_less_trans)
15.131 +done
15.132 +
15.133 +lemma realpow_ge_one [rule_format (no_asm)]: "(1::real) < r --> 1 \<le> r ^ n"
15.134 +apply (induct_tac "n")
15.135 +apply auto
15.136 +apply (subgoal_tac "1*1 \<le> r * r^n")
15.137 +apply (rule_tac [2] real_mult_le_mono)
15.138 +apply auto
15.139 +done
15.140 +
15.141 +lemma realpow_ge_one2: "(1::real) \<le> r ==> 1 \<le> r ^ n"
15.142 +apply (drule order_le_imp_less_or_eq)
15.143 +apply (auto dest: realpow_ge_one)
15.144 +done
15.145 +
15.146 +lemma two_realpow_ge_one: "(1::real) \<le> 2 ^ n"
15.147 +apply (rule_tac y = "1 ^ n" in order_trans)
15.148 +apply (rule_tac [2] realpow_le)
15.149 +apply (auto intro: order_less_imp_le)
15.150 +done
15.151 +
15.152 +lemma two_realpow_gt: "real (n::nat) < 2 ^ n"
15.153 +apply (induct_tac "n")
15.154 +apply (auto simp add: real_of_nat_Suc)
15.155 +apply (subst real_mult_2)
15.156 +apply (rule real_add_less_le_mono)
15.157 +apply (auto simp add: two_realpow_ge_one)
15.158 +done
15.159 +declare two_realpow_gt [simp] two_realpow_ge_one [simp]
15.160 +
15.161 +lemma realpow_minus_one: "(-1) ^ (2*n) = (1::real)"
15.162 +apply (induct_tac "n")
15.163 +apply auto
15.164 +done
15.165 +declare realpow_minus_one [simp]
15.166 +
15.167 +lemma realpow_minus_one_odd: "(-1) ^ Suc (2*n) = -(1::real)"
15.168 +apply auto
15.169 +done
15.170 +declare realpow_minus_one_odd [simp]
15.171 +
15.172 +lemma realpow_minus_one_even: "(-1) ^ Suc (Suc (2*n)) = (1::real)"
15.173 +apply auto
15.174 +done
15.175 +declare realpow_minus_one_even [simp]
15.176 +
15.177 +lemma realpow_Suc_less [rule_format (no_asm)]: "(0::real) < r & r < (1::real) --> r ^ Suc n < r ^ n"
15.178 +apply (induct_tac "n")
15.179 +apply auto
15.180 +done
15.181 +
15.182 +lemma realpow_Suc_le [rule_format (no_asm)]: "0 \<le> r & r < (1::real) --> r ^ Suc n \<le> r ^ n"
15.183 +apply (induct_tac "n")
15.184 +apply (auto intro: order_less_imp_le dest!: order_le_imp_less_or_eq)
15.185 +done
15.186 +
15.187 +lemma realpow_zero_le: "(0::real) \<le> 0 ^ n"
15.188 +apply (case_tac "n")
15.189 +apply auto
15.190 +done
15.191 +declare realpow_zero_le [simp]
15.192 +
15.193 +lemma realpow_Suc_le2 [rule_format (no_asm)]: "0 < r & r < (1::real) --> r ^ Suc n \<le> r ^ n"
15.194 +apply (blast intro!: order_less_imp_le realpow_Suc_less)
15.195 +done
15.196 +
15.197 +lemma realpow_Suc_le3: "[| 0 \<le> r; r < (1::real) |] ==> r ^ Suc n \<le> r ^ n"
15.198 +apply (erule order_le_imp_less_or_eq [THEN disjE])
15.199 +apply (rule realpow_Suc_le2)
15.200 +apply auto
15.201 +done
15.202 +
15.203 +lemma realpow_less_le [rule_format (no_asm)]: "0 \<le> r & r < (1::real) & n < N --> r ^ N \<le> r ^ n"
15.204 +apply (induct_tac "N")
15.205 +apply (simp_all (no_asm_simp))
15.206 +apply clarify
15.207 +apply (subgoal_tac "r * r ^ na \<le> 1 * r ^ n")
15.208 +apply simp
15.209 +apply (rule real_mult_le_mono)
15.210 +apply (auto simp add: realpow_ge_zero less_Suc_eq)
15.211 +done
15.212 +
15.213 +lemma realpow_le_le: "[| 0 \<le> r; r < (1::real); n \<le> N |] ==> r ^ N \<le> r ^ n"
15.214 +apply (drule_tac n = "N" in le_imp_less_or_eq)
15.215 +apply (auto intro: realpow_less_le)
15.216 +done
15.217 +
15.218 +lemma realpow_Suc_le_self: "[| 0 < r; r < (1::real) |] ==> r ^ Suc n \<le> r"
15.219 +apply (drule_tac n = "1" and N = "Suc n" in order_less_imp_le [THEN realpow_le_le])
15.220 +apply auto
15.221 +done
15.222 +
15.223 +lemma realpow_Suc_less_one: "[| 0 < r; r < (1::real) |] ==> r ^ Suc n < 1"
15.224 +apply (blast intro: realpow_Suc_le_self order_le_less_trans)
15.225 +done
15.226 +
15.227 +lemma realpow_le_Suc [rule_format (no_asm)]: "(1::real) \<le> r --> r ^ n \<le> r ^ Suc n"
15.228 +apply (induct_tac "n")
15.229 +apply auto
15.230 +done
15.231 +
15.232 +lemma realpow_less_Suc [rule_format (no_asm)]: "(1::real) < r --> r ^ n < r ^ Suc n"
15.233 +apply (induct_tac "n")
15.234 +apply auto
15.235 +done
15.236 +
15.237 +lemma realpow_le_Suc2 [rule_format (no_asm)]: "(1::real) < r --> r ^ n \<le> r ^ Suc n"
15.238 +apply (blast intro!: order_less_imp_le realpow_less_Suc)
15.239 +done
15.240 +
15.241 +lemma realpow_gt_ge [rule_format (no_asm)]: "(1::real) < r & n < N --> r ^ n \<le> r ^ N"
15.242 +apply (induct_tac "N")
15.243 +apply auto
15.244 +apply (frule_tac [!] n = "na" in realpow_ge_one)
15.245 +apply (drule_tac [!] real_mult_self_le)
15.246 +apply assumption
15.247 +prefer 2 apply (assumption)
15.248 +apply (auto intro: order_trans simp add: less_Suc_eq)
15.249 +done
15.250 +
15.251 +lemma realpow_gt_ge2 [rule_format (no_asm)]: "(1::real) \<le> r & n < N --> r ^ n \<le> r ^ N"
15.252 +apply (induct_tac "N")
15.253 +apply auto
15.254 +apply (frule_tac [!] n = "na" in realpow_ge_one2)
15.255 +apply (drule_tac [!] real_mult_self_le2)
15.256 +apply assumption
15.257 +prefer 2 apply (assumption)
15.258 +apply (auto intro: order_trans simp add: less_Suc_eq)
15.259 +done
15.260 +
15.261 +lemma realpow_ge_ge: "[| (1::real) < r; n \<le> N |] ==> r ^ n \<le> r ^ N"
15.262 +apply (drule_tac n = "N" in le_imp_less_or_eq)
15.263 +apply (auto intro: realpow_gt_ge)
15.264 +done
15.265 +
15.266 +lemma realpow_ge_ge2: "[| (1::real) \<le> r; n \<le> N |] ==> r ^ n \<le> r ^ N"
15.267 +apply (drule_tac n = "N" in le_imp_less_or_eq)
15.268 +apply (auto intro: realpow_gt_ge2)
15.269 +done
15.270 +
15.271 +lemma realpow_Suc_ge_self [rule_format (no_asm)]: "(1::real) < r ==> r \<le> r ^ Suc n"
15.272 +apply (drule_tac n = "1" and N = "Suc n" in realpow_ge_ge)
15.273 +apply auto
15.274 +done
15.275 +
15.276 +lemma realpow_Suc_ge_self2 [rule_format (no_asm)]: "(1::real) \<le> r ==> r \<le> r ^ Suc n"
15.277 +apply (drule_tac n = "1" and N = "Suc n" in realpow_ge_ge2)
15.278 +apply auto
15.279 +done
15.280 +
15.281 +lemma realpow_ge_self: "[| (1::real) < r; 0 < n |] ==> r \<le> r ^ n"
15.282 +apply (drule less_not_refl2 [THEN not0_implies_Suc])
15.283 +apply (auto intro!: realpow_Suc_ge_self)
15.284 +done
15.285 +
15.286 +lemma realpow_ge_self2: "[| (1::real) \<le> r; 0 < n |] ==> r \<le> r ^ n"
15.287 +apply (drule less_not_refl2 [THEN not0_implies_Suc])
15.288 +apply (auto intro!: realpow_Suc_ge_self2)
15.289 +done
15.290 +
15.291 +lemma realpow_minus_mult [rule_format (no_asm)]: "0 < n --> (x::real) ^ (n - 1) * x = x ^ n"
15.292 +apply (induct_tac "n")
15.293 +apply (auto simp add: real_mult_commute)
15.294 +done
15.295 +declare realpow_minus_mult [simp]
15.296 +
15.297 +lemma realpow_two_mult_inverse: "r \<noteq> 0 ==> r * inverse r ^Suc (Suc 0) = inverse (r::real)"
15.298 +apply (simp (no_asm_simp) add: realpow_two real_mult_assoc [symmetric])
15.299 +done
15.300 +declare realpow_two_mult_inverse [simp]
15.301 +
15.302 +(* 05/00 *)
15.303 +lemma realpow_two_minus: "(-x)^Suc (Suc 0) = (x::real)^Suc (Suc 0)"
15.304 +apply (simp (no_asm))
15.305 +done
15.306 +declare realpow_two_minus [simp]
15.307 +
15.308 +lemma realpow_two_diff: "(x::real)^Suc (Suc 0) - y^Suc (Suc 0) = (x - y) * (x + y)"
15.309 +apply (unfold real_diff_def)
15.310 +apply (simp add: real_add_mult_distrib2 real_add_mult_distrib real_mult_ac)
15.311 +done
15.312 +
15.313 +lemma realpow_two_disj: "((x::real)^Suc (Suc 0) = y^Suc (Suc 0)) = (x = y | x = -y)"
15.314 +apply (cut_tac x = "x" and y = "y" in realpow_two_diff)
15.315 +apply (auto simp del: realpow_Suc)
15.316 +done
15.317 +
15.318 +(* used in Transc *)
15.319 +lemma realpow_diff: "[|(x::real) \<noteq> 0; m \<le> n |] ==> x ^ (n - m) = x ^ n * inverse (x ^ m)"
15.320 +apply (auto simp add: le_eq_less_or_eq less_iff_Suc_add realpow_add realpow_not_zero real_mult_ac)
15.321 +done
15.322 +
15.323 +lemma realpow_real_of_nat: "real (m::nat) ^ n = real (m ^ n)"
15.324 +apply (induct_tac "n")
15.325 +apply (auto simp add: real_of_nat_one real_of_nat_mult)
15.326 +done
15.327 +
15.328 +lemma realpow_real_of_nat_two_pos: "0 < real (Suc (Suc 0) ^ n)"
15.329 +apply (induct_tac "n")
15.330 +apply (auto simp add: real_of_nat_mult real_0_less_mult_iff)
15.331 +done
15.332 +declare realpow_real_of_nat_two_pos [simp]
15.333 +
15.334 +lemma realpow_increasing:
15.335 + assumes xnonneg: "(0::real) \<le> x"
15.336 + and ynonneg: "0 \<le> y"
15.337 + and le: "x ^ Suc n \<le> y ^ Suc n"
15.338 + shows "x \<le> y"
15.339 + proof (rule ccontr)
15.340 + assume "~ x \<le> y"
15.341 + then have "y<x" by simp
15.342 + then have "y ^ Suc n < x ^ Suc n"
15.343 + by (simp only: prems realpow_less')
15.344 + from le and this show "False"
15.345 + by simp
15.346 + qed
15.347 +
15.348 +lemma realpow_Suc_cancel_eq: "[| (0::real) \<le> x; 0 \<le> y; x ^ Suc n = y ^ Suc n |] ==> x = y"
15.349 +apply (blast intro: realpow_increasing order_antisym order_eq_refl sym)
15.350 +done
15.351 +
15.352 +
15.353 +(*** Logical equivalences for inequalities ***)
15.354 +
15.355 +lemma realpow_eq_0_iff: "(x^n = 0) = (x = (0::real) & 0<n)"
15.356 +apply (induct_tac "n")
15.357 +apply auto
15.358 +done
15.359 +declare realpow_eq_0_iff [simp]
15.360 +
15.361 +lemma zero_less_realpow_abs_iff: "(0 < (abs x)^n) = (x \<noteq> (0::real) | n=0)"
15.362 +apply (induct_tac "n")
15.363 +apply (auto simp add: real_0_less_mult_iff)
15.364 +done
15.365 +declare zero_less_realpow_abs_iff [simp]
15.366 +
15.367 +lemma zero_le_realpow_abs: "(0::real) \<le> (abs x)^n"
15.368 +apply (induct_tac "n")
15.369 +apply (auto simp add: real_0_le_mult_iff)
15.370 +done
15.371 +declare zero_le_realpow_abs [simp]
15.372 +
15.373 +
15.374 +(*** Literal arithmetic involving powers, type real ***)
15.375 +
15.376 +lemma real_of_int_power: "real (x::int) ^ n = real (x ^ n)"
15.377 +apply (induct_tac "n")
15.378 +apply (simp_all (no_asm_simp) add: nat_mult_distrib)
15.379 +done
15.380 +declare real_of_int_power [symmetric, simp]
15.381 +
15.382 +lemma power_real_number_of: "(number_of v :: real) ^ n = real ((number_of v :: int) ^ n)"
15.383 +apply (simp only: real_number_of_def real_of_int_power)
15.384 +done
15.385 +
15.386 +declare power_real_number_of [of _ "number_of w", standard, simp]
15.387 +
15.388 +
15.389 +lemma real_power_two: "(r::real)\<twosuperior> = r * r"
15.390 + by (simp add: numeral_2_eq_2)
15.391 +
15.392 +lemma real_sqr_ge_zero [iff]: "0 \<le> (r::real)\<twosuperior>"
15.393 + by (simp add: real_power_two)
15.394 +
15.395 +lemma real_sqr_gt_zero: "(r::real) \<noteq> 0 ==> 0 < r\<twosuperior>"
15.396 +proof -
15.397 + assume "r \<noteq> 0"
15.398 + hence "0 \<noteq> r\<twosuperior>" by simp
15.399 + also have "0 \<le> r\<twosuperior>" by (simp add: real_sqr_ge_zero)
15.400 + finally show ?thesis .
15.401 +qed
15.402 +
15.403 +lemma real_sqr_not_zero: "r \<noteq> 0 ==> (r::real)\<twosuperior> \<noteq> 0"
15.404 + by simp
15.405 +
15.406 +
15.407 +ML
15.408 +{*
15.409 +val realpow_0 = thm "realpow_0";
15.410 +val realpow_Suc = thm "realpow_Suc";
15.411 +
15.412 +val realpow_zero = thm "realpow_zero";
15.413 +val realpow_not_zero = thm "realpow_not_zero";
15.414 +val realpow_zero_zero = thm "realpow_zero_zero";
15.415 +val realpow_inverse = thm "realpow_inverse";
15.416 +val realpow_abs = thm "realpow_abs";
15.417 +val realpow_add = thm "realpow_add";
15.418 +val realpow_one = thm "realpow_one";
15.419 +val realpow_two = thm "realpow_two";
15.420 +val realpow_gt_zero = thm "realpow_gt_zero";
15.421 +val realpow_ge_zero = thm "realpow_ge_zero";
15.422 +val realpow_le = thm "realpow_le";
15.423 +val realpow_0_left = thm "realpow_0_left";
15.424 +val realpow_less = thm "realpow_less";
15.425 +val realpow_eq_one = thm "realpow_eq_one";
15.426 +val abs_realpow_minus_one = thm "abs_realpow_minus_one";
15.427 +val realpow_mult = thm "realpow_mult";
15.428 +val realpow_two_le = thm "realpow_two_le";
15.429 +val abs_realpow_two = thm "abs_realpow_two";
15.430 +val realpow_two_abs = thm "realpow_two_abs";
15.431 +val realpow_two_gt_one = thm "realpow_two_gt_one";
15.432 +val realpow_ge_one = thm "realpow_ge_one";
15.433 +val realpow_ge_one2 = thm "realpow_ge_one2";
15.434 +val two_realpow_ge_one = thm "two_realpow_ge_one";
15.435 +val two_realpow_gt = thm "two_realpow_gt";
15.436 +val realpow_minus_one = thm "realpow_minus_one";
15.437 +val realpow_minus_one_odd = thm "realpow_minus_one_odd";
15.438 +val realpow_minus_one_even = thm "realpow_minus_one_even";
15.439 +val realpow_Suc_less = thm "realpow_Suc_less";
15.440 +val realpow_Suc_le = thm "realpow_Suc_le";
15.441 +val realpow_zero_le = thm "realpow_zero_le";
15.442 +val realpow_Suc_le2 = thm "realpow_Suc_le2";
15.443 +val realpow_Suc_le3 = thm "realpow_Suc_le3";
15.444 +val realpow_less_le = thm "realpow_less_le";
15.445 +val realpow_le_le = thm "realpow_le_le";
15.446 +val realpow_Suc_le_self = thm "realpow_Suc_le_self";
15.447 +val realpow_Suc_less_one = thm "realpow_Suc_less_one";
15.448 +val realpow_le_Suc = thm "realpow_le_Suc";
15.449 +val realpow_less_Suc = thm "realpow_less_Suc";
15.450 +val realpow_le_Suc2 = thm "realpow_le_Suc2";
15.451 +val realpow_gt_ge = thm "realpow_gt_ge";
15.452 +val realpow_gt_ge2 = thm "realpow_gt_ge2";
15.453 +val realpow_ge_ge = thm "realpow_ge_ge";
15.454 +val realpow_ge_ge2 = thm "realpow_ge_ge2";
15.455 +val realpow_Suc_ge_self = thm "realpow_Suc_ge_self";
15.456 +val realpow_Suc_ge_self2 = thm "realpow_Suc_ge_self2";
15.457 +val realpow_ge_self = thm "realpow_ge_self";
15.458 +val realpow_ge_self2 = thm "realpow_ge_self2";
15.459 +val realpow_minus_mult = thm "realpow_minus_mult";
15.460 +val realpow_two_mult_inverse = thm "realpow_two_mult_inverse";
15.461 +val realpow_two_minus = thm "realpow_two_minus";
15.462 +val realpow_two_diff = thm "realpow_two_diff";
15.463 +val realpow_two_disj = thm "realpow_two_disj";
15.464 +val realpow_diff = thm "realpow_diff";
15.465 +val realpow_real_of_nat = thm "realpow_real_of_nat";
15.466 +val realpow_real_of_nat_two_pos = thm "realpow_real_of_nat_two_pos";
15.467 +val realpow_increasing = thm "realpow_increasing";
15.468 +val realpow_Suc_cancel_eq = thm "realpow_Suc_cancel_eq";
15.469 +val realpow_eq_0_iff = thm "realpow_eq_0_iff";
15.470 +val zero_less_realpow_abs_iff = thm "zero_less_realpow_abs_iff";
15.471 +val zero_le_realpow_abs = thm "zero_le_realpow_abs";
15.472 +val real_of_int_power = thm "real_of_int_power";
15.473 +val power_real_number_of = thm "power_real_number_of";
15.474 +val real_power_two = thm "real_power_two";
15.475 +val real_sqr_ge_zero = thm "real_sqr_ge_zero";
15.476 +val real_sqr_gt_zero = thm "real_sqr_gt_zero";
15.477 +val real_sqr_not_zero = thm "real_sqr_not_zero";
15.478 +*}
15.479 +
15.480 +
15.481 end
16.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
16.2 +++ b/src/HOL/Ring_and_Field.thy Fri Nov 21 11:15:40 2003 +0100
16.3 @@ -0,0 +1,382 @@
16.4 +(* Title: HOL/Ring_and_Field.thy
16.5 + ID: $Id$
16.6 + Author: Gertrud Bauer and Markus Wenzel, TU Muenchen
16.7 + License: GPL (GNU GENERAL PUBLIC LICENSE)
16.8 +*)
16.9 +
16.10 +header {*
16.11 + \title{Ring and field structures}
16.12 + \author{Gertrud Bauer and Markus Wenzel}
16.13 +*}
16.14 +
16.15 +theory Ring_and_Field = Inductive:
16.16 +
16.17 +text{*Lemmas and extension to semirings by L. C. Paulson*}
16.18 +
16.19 +subsection {* Abstract algebraic structures *}
16.20 +
16.21 +axclass semiring \<subseteq> zero, one, plus, times
16.22 + add_assoc: "(a + b) + c = a + (b + c)"
16.23 + add_commute: "a + b = b + a"
16.24 + left_zero [simp]: "0 + a = a"
16.25 +
16.26 + mult_assoc: "(a * b) * c = a * (b * c)"
16.27 + mult_commute: "a * b = b * a"
16.28 + left_one [simp]: "1 * a = a"
16.29 +
16.30 + left_distrib: "(a + b) * c = a * c + b * c"
16.31 + zero_neq_one [simp]: "0 \<noteq> 1"
16.32 +
16.33 +axclass ring \<subseteq> semiring, minus
16.34 + left_minus [simp]: "- a + a = 0"
16.35 + diff_minus: "a - b = a + (-b)"
16.36 +
16.37 +axclass ordered_semiring \<subseteq> semiring, linorder
16.38 + add_left_mono: "a \<le> b ==> c + a \<le> c + b"
16.39 + mult_strict_left_mono: "a < b ==> 0 < c ==> c * a < c * b"
16.40 +
16.41 +axclass ordered_ring \<subseteq> ordered_semiring, ring
16.42 + abs_if: "\<bar>a\<bar> = (if a < 0 then -a else a)"
16.43 +
16.44 +axclass field \<subseteq> ring, inverse
16.45 + left_inverse [simp]: "a \<noteq> 0 ==> inverse a * a = 1"
16.46 + divide_inverse: "b \<noteq> 0 ==> a / b = a * inverse b"
16.47 +
16.48 +axclass ordered_field \<subseteq> ordered_ring, field
16.49 +
16.50 +axclass division_by_zero \<subseteq> zero, inverse
16.51 + inverse_zero: "inverse 0 = 0"
16.52 + divide_zero: "a / 0 = 0"
16.53 +
16.54 +
16.55 +subsection {* Derived rules for addition *}
16.56 +
16.57 +lemma right_zero [simp]: "a + 0 = (a::'a::semiring)"
16.58 +proof -
16.59 + have "a + 0 = 0 + a" by (simp only: add_commute)
16.60 + also have "... = a" by simp
16.61 + finally show ?thesis .
16.62 +qed
16.63 +
16.64 +lemma add_left_commute: "a + (b + c) = b + (a + (c::'a::semiring))"
16.65 + by (rule mk_left_commute [of "op +", OF add_assoc add_commute])
16.66 +
16.67 +theorems add_ac = add_assoc add_commute add_left_commute
16.68 +
16.69 +lemma right_minus [simp]: "a + -(a::'a::ring) = 0"
16.70 +proof -
16.71 + have "a + -a = -a + a" by (simp add: add_ac)
16.72 + also have "... = 0" by simp
16.73 + finally show ?thesis .
16.74 +qed
16.75 +
16.76 +lemma right_minus_eq: "(a - b = 0) = (a = (b::'a::ring))"
16.77 +proof
16.78 + have "a = a - b + b" by (simp add: diff_minus add_ac)
16.79 + also assume "a - b = 0"
16.80 + finally show "a = b" by simp
16.81 +next
16.82 + assume "a = b"
16.83 + thus "a - b = 0" by (simp add: diff_minus)
16.84 +qed
16.85 +
16.86 +lemma diff_self [simp]: "a - (a::'a::ring) = 0"
16.87 + by (simp add: diff_minus)
16.88 +
16.89 +lemma add_left_cancel [simp]:
16.90 + "(a + b = a + c) = (b = (c::'a::ring))"
16.91 +proof
16.92 + assume eq: "a + b = a + c"
16.93 + then have "(-a + a) + b = (-a + a) + c"
16.94 + by (simp only: eq add_assoc)
16.95 + then show "b = c" by simp
16.96 +next
16.97 + assume eq: "b = c"
16.98 + then show "a + b = a + c" by simp
16.99 +qed
16.100 +
16.101 +lemma add_right_cancel [simp]:
16.102 + "(b + a = c + a) = (b = (c::'a::ring))"
16.103 + by (simp add: add_commute)
16.104 +
16.105 +lemma minus_minus [simp]: "- (- (a::'a::ring)) = a"
16.106 + proof (rule add_left_cancel [of "-a", THEN iffD1])
16.107 + show "(-a + -(-a) = -a + a)"
16.108 + by simp
16.109 + qed
16.110 +
16.111 +lemma equals_zero_I: "a+b = 0 ==> -a = (b::'a::ring)"
16.112 +apply (rule right_minus_eq [THEN iffD1, symmetric])
16.113 +apply (simp add: diff_minus add_commute)
16.114 +done
16.115 +
16.116 +lemma minus_zero [simp]: "- 0 = (0::'a::ring)"
16.117 +by (simp add: equals_zero_I)
16.118 +
16.119 +lemma neg_equal_iff_equal [simp]: "(-a = -b) = (a = (b::'a::ring))"
16.120 + proof
16.121 + assume "- a = - b"
16.122 + then have "- (- a) = - (- b)"
16.123 + by simp
16.124 + then show "a=b"
16.125 + by simp
16.126 + next
16.127 + assume "a=b"
16.128 + then show "-a = -b"
16.129 + by simp
16.130 + qed
16.131 +
16.132 +lemma neg_equal_0_iff_equal [simp]: "(-a = 0) = (a = (0::'a::ring))"
16.133 +by (subst neg_equal_iff_equal [symmetric], simp)
16.134 +
16.135 +lemma neg_0_equal_iff_equal [simp]: "(0 = -a) = (0 = (a::'a::ring))"
16.136 +by (subst neg_equal_iff_equal [symmetric], simp)
16.137 +
16.138 +
16.139 +subsection {* Derived rules for multiplication *}
16.140 +
16.141 +lemma right_one [simp]: "a = a * (1::'a::semiring)"
16.142 +proof -
16.143 + have "a = 1 * a" by simp
16.144 + also have "... = a * 1" by (simp add: mult_commute)
16.145 + finally show ?thesis .
16.146 +qed
16.147 +
16.148 +lemma mult_left_commute: "a * (b * c) = b * (a * (c::'a::semiring))"
16.149 + by (rule mk_left_commute [of "op *", OF mult_assoc mult_commute])
16.150 +
16.151 +theorems mult_ac = mult_assoc mult_commute mult_left_commute
16.152 +
16.153 +lemma right_inverse [simp]: "a \<noteq> 0 ==> a * inverse (a::'a::field) = 1"
16.154 +proof -
16.155 + have "a * inverse a = inverse a * a" by (simp add: mult_ac)
16.156 + also assume "a \<noteq> 0"
16.157 + hence "inverse a * a = 1" by simp
16.158 + finally show ?thesis .
16.159 +qed
16.160 +
16.161 +lemma right_inverse_eq: "b \<noteq> 0 ==> (a / b = 1) = (a = (b::'a::field))"
16.162 +proof
16.163 + assume neq: "b \<noteq> 0"
16.164 + {
16.165 + hence "a = (a / b) * b" by (simp add: divide_inverse mult_ac)
16.166 + also assume "a / b = 1"
16.167 + finally show "a = b" by simp
16.168 + next
16.169 + assume "a = b"
16.170 + with neq show "a / b = 1" by (simp add: divide_inverse)
16.171 + }
16.172 +qed
16.173 +
16.174 +lemma divide_self [simp]: "a \<noteq> 0 ==> a / (a::'a::field) = 1"
16.175 + by (simp add: divide_inverse)
16.176 +
16.177 +lemma mult_left_zero [simp]: "0 * a = (0::'a::ring)"
16.178 +proof -
16.179 + have "0*a + 0*a = 0*a + 0"
16.180 + by (simp add: left_distrib [symmetric])
16.181 + then show ?thesis by (simp only: add_left_cancel)
16.182 +qed
16.183 +
16.184 +lemma mult_right_zero [simp]: "a * 0 = (0::'a::ring)"
16.185 + by (simp add: mult_commute)
16.186 +
16.187 +
16.188 +subsection {* Distribution rules *}
16.189 +
16.190 +lemma right_distrib: "a * (b + c) = a * b + a * (c::'a::semiring)"
16.191 +proof -
16.192 + have "a * (b + c) = (b + c) * a" by (simp add: mult_ac)
16.193 + also have "... = b * a + c * a" by (simp only: left_distrib)
16.194 + also have "... = a * b + a * c" by (simp add: mult_ac)
16.195 + finally show ?thesis .
16.196 +qed
16.197 +
16.198 +theorems ring_distrib = right_distrib left_distrib
16.199 +
16.200 +lemma minus_add_distrib [simp]: "- (a + b) = -a + -(b::'a::ring)"
16.201 +apply (rule equals_zero_I)
16.202 +apply (simp add: add_ac)
16.203 +done
16.204 +
16.205 +lemma minus_mult_left: "- (a * b) = (-a) * (b::'a::ring)"
16.206 +apply (rule equals_zero_I)
16.207 +apply (simp add: left_distrib [symmetric])
16.208 +done
16.209 +
16.210 +lemma minus_mult_right: "- (a * b) = a * -(b::'a::ring)"
16.211 +apply (rule equals_zero_I)
16.212 +apply (simp add: right_distrib [symmetric])
16.213 +done
16.214 +
16.215 +lemma right_diff_distrib: "a * (b - c) = a * b - a * (c::'a::ring)"
16.216 +by (simp add: right_distrib diff_minus
16.217 + minus_mult_left [symmetric] minus_mult_right [symmetric])
16.218 +
16.219 +
16.220 +subsection {* Ordering rules *}
16.221 +
16.222 +lemma add_right_mono: "a \<le> (b::'a::ordered_semiring) ==> a + c \<le> b + c"
16.223 +by (simp add: add_commute [of _ c] add_left_mono)
16.224 +
16.225 +lemma le_imp_neg_le:
16.226 + assumes "a \<le> (b::'a::ordered_ring)" shows "-b \<le> -a"
16.227 + proof -
16.228 + have "-a+a \<le> -a+b"
16.229 + by (rule add_left_mono)
16.230 + then have "0 \<le> -a+b"
16.231 + by simp
16.232 + then have "0 + (-b) \<le> (-a + b) + (-b)"
16.233 + by (rule add_right_mono)
16.234 + then show ?thesis
16.235 + by (simp add: add_assoc)
16.236 + qed
16.237 +
16.238 +lemma neg_le_iff_le [simp]: "(-b \<le> -a) = (a \<le> (b::'a::ordered_ring))"
16.239 + proof
16.240 + assume "- b \<le> - a"
16.241 + then have "- (- a) \<le> - (- b)"
16.242 + by (rule le_imp_neg_le)
16.243 + then show "a\<le>b"
16.244 + by simp
16.245 + next
16.246 + assume "a\<le>b"
16.247 + then show "-b \<le> -a"
16.248 + by (rule le_imp_neg_le)
16.249 + qed
16.250 +
16.251 +lemma neg_le_0_iff_le [simp]: "(-a \<le> 0) = (0 \<le> (a::'a::ordered_ring))"
16.252 +by (subst neg_le_iff_le [symmetric], simp)
16.253 +
16.254 +lemma neg_0_le_iff_le [simp]: "(0 \<le> -a) = (a \<le> (0::'a::ordered_ring))"
16.255 +by (subst neg_le_iff_le [symmetric], simp)
16.256 +
16.257 +lemma neg_less_iff_less [simp]: "(-b < -a) = (a < (b::'a::ordered_ring))"
16.258 +by (force simp add: order_less_le)
16.259 +
16.260 +lemma neg_less_0_iff_less [simp]: "(-a < 0) = (0 < (a::'a::ordered_ring))"
16.261 +by (subst neg_less_iff_less [symmetric], simp)
16.262 +
16.263 +lemma neg_0_less_iff_less [simp]: "(0 < -a) = (a < (0::'a::ordered_ring))"
16.264 +by (subst neg_less_iff_less [symmetric], simp)
16.265 +
16.266 +lemma mult_strict_right_mono:
16.267 + "[|a < b; 0 < c|] ==> a * c < b * (c::'a::ordered_semiring)"
16.268 +by (simp add: mult_commute [of _ c] mult_strict_left_mono)
16.269 +
16.270 +lemma mult_left_mono:
16.271 + "[|a \<le> b; 0 < c|] ==> c * a \<le> c * (b::'a::ordered_semiring)"
16.272 +by (force simp add: mult_strict_left_mono order_le_less)
16.273 +
16.274 +lemma mult_right_mono:
16.275 + "[|a \<le> b; 0 < c|] ==> a*c \<le> b * (c::'a::ordered_semiring)"
16.276 +by (force simp add: mult_strict_right_mono order_le_less)
16.277 +
16.278 +lemma mult_strict_left_mono_neg:
16.279 + "[|b < a; c < 0|] ==> c * a < c * (b::'a::ordered_ring)"
16.280 +apply (drule mult_strict_left_mono [of _ _ "-c"])
16.281 +apply (simp_all add: minus_mult_left [symmetric])
16.282 +done
16.283 +
16.284 +lemma mult_strict_right_mono_neg:
16.285 + "[|b < a; c < 0|] ==> a * c < b * (c::'a::ordered_ring)"
16.286 +apply (drule mult_strict_right_mono [of _ _ "-c"])
16.287 +apply (simp_all add: minus_mult_right [symmetric])
16.288 +done
16.289 +
16.290 +lemma mult_left_mono_neg:
16.291 + "[|b \<le> a; c < 0|] ==> c * a \<le> c * (b::'a::ordered_ring)"
16.292 +by (force simp add: mult_strict_left_mono_neg order_le_less)
16.293 +
16.294 +lemma mult_right_mono_neg:
16.295 + "[|b \<le> a; c < 0|] ==> a * c \<le> b * (c::'a::ordered_ring)"
16.296 +by (force simp add: mult_strict_right_mono_neg order_le_less)
16.297 +
16.298 +
16.299 +subsection{* Products of Signs *}
16.300 +
16.301 +lemma mult_pos: "[| (0::'a::ordered_ring) < a; 0 < b |] ==> 0 < a*b"
16.302 +by (drule mult_strict_left_mono [of 0 b], auto)
16.303 +
16.304 +lemma mult_pos_neg: "[| (0::'a::ordered_ring) < a; b < 0 |] ==> a*b < 0"
16.305 +by (drule mult_strict_left_mono [of b 0], auto)
16.306 +
16.307 +lemma mult_neg: "[| a < (0::'a::ordered_ring); b < 0 |] ==> 0 < a*b"
16.308 +by (drule mult_strict_right_mono_neg, auto)
16.309 +
16.310 +lemma zero_less_mult_pos: "[| 0 < a*b; 0 < a|] ==> 0 < (b::'a::ordered_ring)"
16.311 +apply (case_tac "b\<le>0")
16.312 + apply (auto simp add: order_le_less linorder_not_less)
16.313 +apply (drule_tac mult_pos_neg [of a b])
16.314 + apply (auto dest: order_less_not_sym)
16.315 +done
16.316 +
16.317 +lemma zero_less_mult_iff:
16.318 + "((0::'a::ordered_ring) < a*b) = (0 < a & 0 < b | a < 0 & b < 0)"
16.319 +apply (auto simp add: order_le_less linorder_not_less mult_pos mult_neg)
16.320 +apply (blast dest: zero_less_mult_pos)
16.321 +apply (simp add: mult_commute [of a b])
16.322 +apply (blast dest: zero_less_mult_pos)
16.323 +done
16.324 +
16.325 +
16.326 +lemma mult_eq_0_iff [iff]: "(a*b = (0::'a::ordered_ring)) = (a = 0 | b = 0)"
16.327 +apply (case_tac "a < 0")
16.328 +apply (auto simp add: linorder_not_less order_le_less linorder_neq_iff)
16.329 +apply (force dest: mult_strict_right_mono_neg mult_strict_right_mono)+
16.330 +done
16.331 +
16.332 +lemma zero_le_mult_iff:
16.333 + "((0::'a::ordered_ring) \<le> a*b) = (0 \<le> a & 0 \<le> b | a \<le> 0 & b \<le> 0)"
16.334 +by (auto simp add: eq_commute [of 0] order_le_less linorder_not_less
16.335 + zero_less_mult_iff)
16.336 +
16.337 +lemma mult_less_0_iff:
16.338 + "(a*b < (0::'a::ordered_ring)) = (0 < a & b < 0 | a < 0 & 0 < b)"
16.339 +apply (insert zero_less_mult_iff [of "-a" b])
16.340 +apply (force simp add: minus_mult_left[symmetric])
16.341 +done
16.342 +
16.343 +lemma mult_le_0_iff:
16.344 + "(a*b \<le> (0::'a::ordered_ring)) = (0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)"
16.345 +apply (insert zero_le_mult_iff [of "-a" b])
16.346 +apply (force simp add: minus_mult_left[symmetric])
16.347 +done
16.348 +
16.349 +lemma zero_le_square: "(0::'a::ordered_ring) \<le> a*a"
16.350 +by (simp add: zero_le_mult_iff linorder_linear)
16.351 +
16.352 +lemma zero_less_one: "(0::'a::ordered_ring) < 1"
16.353 +apply (insert zero_le_square [of 1])
16.354 +apply (simp add: order_less_le)
16.355 +done
16.356 +
16.357 +
16.358 +subsection {* Absolute Value *}
16.359 +
16.360 +text{*But is it really better than just rewriting with @{text abs_if}?*}
16.361 +lemma abs_split:
16.362 + "P(abs(a::'a::ordered_ring)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
16.363 +by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
16.364 +
16.365 +lemma abs_zero [simp]: "abs 0 = (0::'a::ordered_ring)"
16.366 +by (simp add: abs_if)
16.367 +
16.368 +lemma abs_mult: "abs (x * y) = abs x * abs (y::'a::ordered_ring)"
16.369 +apply (case_tac "x=0 | y=0", force)
16.370 +apply (auto elim: order_less_asym
16.371 + simp add: abs_if mult_less_0_iff linorder_neq_iff
16.372 + minus_mult_left [symmetric] minus_mult_right [symmetric])
16.373 +done
16.374 +
16.375 +lemma abs_eq_0 [iff]: "(abs x = 0) = (x = (0::'a::ordered_ring))"
16.376 +by (simp add: abs_if)
16.377 +
16.378 +lemma zero_less_abs_iff [iff]: "(0 < abs x) = (x ~= (0::'a::ordered_ring))"
16.379 +by (simp add: abs_if linorder_neq_iff)
16.380 +
16.381 +
16.382 +subsection {* Fields *}
16.383 +
16.384 +
16.385 +end