1.1 --- a/src/HOL/Hyperreal/Poly.ML Fri Nov 21 11:15:40 2003 +0100
1.2 +++ b/src/HOL/Hyperreal/Poly.ML Mon Nov 24 15:33:07 2003 +0100
1.3 @@ -1003,7 +1003,7 @@
1.4 by (dtac (poly_mult_left_cancel RS iffD1) 1);
1.5 by (Asm_full_simp_tac 1);
1.6 by (asm_full_simp_tac (simpset() addsimps [fun_eq,poly_mult,poly_add,poly_cmult,
1.7 - poly_minus] delsimps [pmult_Cons]) 1);
1.8 + poly_minus] delsimps [pmult_Cons, thm"mult_cancel_left"]) 1);
1.9 by (Step_tac 1);
1.10 by (res_inst_tac [("c1","real (Suc n)")] (real_mult_left_cancel
1.11 RS iffD1) 1);
2.1 --- a/src/HOL/Hyperreal/Transcendental.ML Fri Nov 21 11:15:40 2003 +0100
2.2 +++ b/src/HOL/Hyperreal/Transcendental.ML Mon Nov 24 15:33:07 2003 +0100
2.3 @@ -559,7 +559,6 @@
2.4 addsimps [lemma_realpow_diff_sumr2,
2.5 real_diff_mult_distrib2 RS sym,real_mult_assoc]
2.6 delsimps [realpow_Suc,sumr_Suc]));
2.7 -by (rtac (real_mult_left_cancel RS iffD2) 1);
2.8 by (auto_tac (claset(),simpset() addsimps [lemma_realpow_rev_sumr]
2.9 delsimps [sumr_Suc]));
2.10 by (auto_tac (claset(),simpset() addsimps [real_of_nat_Suc,sumr_diff_mult_const,
2.11 @@ -773,7 +772,9 @@
2.12 \ (real (n - Suc 0) * abs (c n) * inverse r) * r ^ (n - Suc 0))")]
2.13 (CLAIM "(a = b) ==> a ==> b") 1 THEN assume_tac 2);
2.14 by (res_inst_tac [("f","summable")] arg_cong 1 THEN rtac ext 1);
2.15 -(* 75 *)
2.16 +by (dtac (abs_ge_zero RS order_le_less_trans) 2);
2.17 +by (asm_full_simp_tac (simpset() addsimps real_mult_ac) 2);
2.18 +(* 77 *)
2.19 by (case_tac "n" 1);
2.20 by Auto_tac;
2.21 by (case_tac "nat" 1);
2.22 @@ -1016,6 +1017,7 @@
2.23 Goal "exp(x + y) = exp(x) * exp(y)";
2.24 by (cut_inst_tac [("x1","x"),("y1","y"),("z","exp x")]
2.25 (exp_add_mult_minus RS (CLAIM "x = y ==> z * y = z * (x::real)")) 1);
2.26 +by (asm_full_simp_tac HOL_ss 1);
2.27 by (asm_full_simp_tac (simpset() delsimps [exp_add_mult_minus]
2.28 addsimps real_mult_ac) 1);
2.29 qed "exp_add";
3.1 --- a/src/HOL/Integ/Bin.ML Fri Nov 21 11:15:40 2003 +0100
3.2 +++ b/src/HOL/Integ/Bin.ML Mon Nov 24 15:33:07 2003 +0100
3.3 @@ -250,8 +250,8 @@
3.4 by (Simp_tac 1);
3.5 qed "iszero_number_of_Pls";
3.6
3.7 -Goalw [iszero_def] "~ iszero ((number_of bin.Min)::int)";
3.8 -by (Simp_tac 1);
3.9 +Goalw [iszero_def] "~ iszero ((number_of bin.Min)::int)";
3.10 +by (simp_tac (simpset() addsimps [eq_commute]) 1);
3.11 qed "nonzero_number_of_Min";
3.12
3.13 fun int_case_tac x = res_inst_tac [("z",x)] int_cases;
4.1 --- a/src/HOL/Integ/Int.thy Fri Nov 21 11:15:40 2003 +0100
4.2 +++ b/src/HOL/Integ/Int.thy Mon Nov 24 15:33:07 2003 +0100
4.3 @@ -37,7 +37,7 @@
4.4 lemma neg_eq_less_0: "neg x = (x < 0)"
4.5 by (unfold zdiff_def zless_def, auto)
4.6
4.7 -lemma not_neg_eq_ge_0: "(~neg x) = (0 <= x)"
4.8 +lemma not_neg_eq_ge_0: "(~neg x) = (0 \<le> x)"
4.9 apply (unfold zle_def)
4.10 apply (simp add: neg_eq_less_0)
4.11 done
4.12 @@ -152,7 +152,7 @@
4.13 lemma eq_eq_iszero: "(w=z) = iszero(w-z)"
4.14 by (simp add: iszero_def zdiff_eq_eq)
4.15
4.16 -lemma zle_eq_not_neg: "(w<=z) = (~ neg(z-w))"
4.17 +lemma zle_eq_not_neg: "(w\<le>z) = (~ neg(z-w))"
4.18 by (simp add: zle_def zless_def)
4.19
4.20 subsection{*Inequality reasoning*}
4.21 @@ -163,13 +163,13 @@
4.22 apply (simp add: int_Suc)
4.23 done
4.24
4.25 -lemma add1_zle_eq: "(w + (1::int) <= z) = (w<z)"
4.26 +lemma add1_zle_eq: "(w + (1::int) \<le> z) = (w<z)"
4.27 apply (simp add: zle_def zless_add1_eq)
4.28 apply (auto intro: zless_asym zle_anti_sym
4.29 simp add: order_less_imp_le symmetric zle_def)
4.30 done
4.31
4.32 -lemma add1_left_zle_eq: "((1::int) + w <= z) = (w<z)"
4.33 +lemma add1_left_zle_eq: "((1::int) + w \<le> z) = (w<z)"
4.34 apply (subst zadd_commute)
4.35 apply (rule add1_zle_eq)
4.36 done
4.37 @@ -183,28 +183,28 @@
4.38 lemma zadd_left_cancel_zless [simp]: "(z+v < z+w) = (v < (w::int))"
4.39 by simp
4.40
4.41 -lemma zadd_right_cancel_zle [simp] : "(v+z <= w+z) = (v <= (w::int))"
4.42 +lemma zadd_right_cancel_zle [simp] : "(v+z \<le> w+z) = (v \<le> (w::int))"
4.43 by simp
4.44
4.45 -lemma zadd_left_cancel_zle [simp] : "(z+v <= z+w) = (v <= (w::int))"
4.46 +lemma zadd_left_cancel_zle [simp] : "(z+v \<le> z+w) = (v \<le> (w::int))"
4.47 by simp
4.48
4.49 -(*"v<=w ==> v+z <= w+z"*)
4.50 +(*"v\<le>w ==> v+z \<le> w+z"*)
4.51 lemmas zadd_zless_mono1 = zadd_right_cancel_zless [THEN iffD2, standard]
4.52
4.53 -(*"v<=w ==> z+v <= z+w"*)
4.54 +(*"v\<le>w ==> z+v \<le> z+w"*)
4.55 lemmas zadd_zless_mono2 = zadd_left_cancel_zless [THEN iffD2, standard]
4.56
4.57 -(*"v<=w ==> v+z <= w+z"*)
4.58 +(*"v\<le>w ==> v+z \<le> w+z"*)
4.59 lemmas zadd_zle_mono1 = zadd_right_cancel_zle [THEN iffD2, standard]
4.60
4.61 -(*"v<=w ==> z+v <= z+w"*)
4.62 +(*"v\<le>w ==> z+v \<le> z+w"*)
4.63 lemmas zadd_zle_mono2 = zadd_left_cancel_zle [THEN iffD2, standard]
4.64
4.65 -lemma zadd_zle_mono: "[| w'<=w; z'<=z |] ==> w' + z' <= w + (z::int)"
4.66 +lemma zadd_zle_mono: "[| w'\<le>w; z'\<le>z |] ==> w' + z' \<le> w + (z::int)"
4.67 by (erule zadd_zle_mono1 [THEN zle_trans], simp)
4.68
4.69 -lemma zadd_zless_mono: "[| w'<w; z'<=z |] ==> w' + z' < w + (z::int)"
4.70 +lemma zadd_zless_mono: "[| w'<w; z'\<le>z |] ==> w' + z' < w + (z::int)"
4.71 by (erule zadd_zless_mono1 [THEN order_less_le_trans], simp)
4.72
4.73
4.74 @@ -213,7 +213,7 @@
4.75 lemma zminus_zless_zminus [simp]: "(- x < - y) = (y < (x::int))"
4.76 by (simp add: zless_def zdiff_def zadd_ac)
4.77
4.78 -lemma zminus_zle_zminus [simp]: "(- x <= - y) = (y <= (x::int))"
4.79 +lemma zminus_zle_zminus [simp]: "(- x \<le> - y) = (y \<le> (x::int))"
4.80 by (simp add: zle_def)
4.81
4.82 text{*The next several equations can make the simplifier loop!*}
4.83 @@ -224,10 +224,10 @@
4.84 lemma zminus_zless: "(- x < y) = (- y < (x::int))"
4.85 by (simp add: zless_def zdiff_def zadd_ac)
4.86
4.87 -lemma zle_zminus: "(x <= - y) = (y <= - (x::int))"
4.88 +lemma zle_zminus: "(x \<le> - y) = (y \<le> - (x::int))"
4.89 by (simp add: zle_def zminus_zless)
4.90
4.91 -lemma zminus_zle: "(- x <= y) = (- y <= (x::int))"
4.92 +lemma zminus_zle: "(- x \<le> y) = (- y \<le> (x::int))"
4.93 by (simp add: zle_def zless_zminus)
4.94
4.95 lemma equation_zminus: "(x = - y) = (y = - (x::int))"
4.96 @@ -254,16 +254,16 @@
4.97 lemma negative_zless [iff]: "- (int (Suc n)) < int m"
4.98 by (rule negative_zless_0 [THEN order_less_le_trans], simp)
4.99
4.100 -lemma negative_zle_0: "- int n <= 0"
4.101 +lemma negative_zle_0: "- int n \<le> 0"
4.102 by (simp add: zminus_zle)
4.103
4.104 -lemma negative_zle [iff]: "- int n <= int m"
4.105 +lemma negative_zle [iff]: "- int n \<le> int m"
4.106 by (simp add: zless_def zle_def zdiff_def zadd_int)
4.107
4.108 -lemma not_zle_0_negative [simp]: "~(0 <= - (int (Suc n)))"
4.109 +lemma not_zle_0_negative [simp]: "~(0 \<le> - (int (Suc n)))"
4.110 by (subst zle_zminus, simp)
4.111
4.112 -lemma int_zle_neg: "(int n <= - int m) = (n = 0 & m = 0)"
4.113 +lemma int_zle_neg: "(int n \<le> - int m) = (n = 0 & m = 0)"
4.114 apply safe
4.115 apply (drule_tac [2] zle_zminus [THEN iffD1])
4.116 apply (auto dest: zle_trans [OF _ negative_zle_0])
4.117 @@ -279,7 +279,7 @@
4.118 apply (simp_all (no_asm_simp))
4.119 done
4.120
4.121 -lemma zle_iff_zadd: "(w <= z) = (EX n. z = w + int n)"
4.122 +lemma zle_iff_zadd: "(w \<le> z) = (EX n. z = w + int n)"
4.123 by (force intro: exI [of _ "0::nat"]
4.124 intro!: not_sym [THEN not0_implies_Suc]
4.125 simp add: zless_iff_Suc_zadd int_le_less)
4.126 @@ -322,13 +322,13 @@
4.127 apply (auto dest: order_less_trans simp add: neg_eq_less_0)
4.128 done
4.129
4.130 -lemma nat_0_le [simp]: "0 <= z ==> int (nat z) = z"
4.131 +lemma nat_0_le [simp]: "0 \<le> z ==> int (nat z) = z"
4.132 by (simp add: neg_eq_less_0 zle_def not_neg_nat)
4.133
4.134 -lemma nat_le_0 [simp]: "z <= 0 ==> nat z = 0"
4.135 +lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0"
4.136 by (auto simp add: order_le_less neg_eq_less_0 zle_def neg_nat)
4.137
4.138 -(*An alternative condition is 0 <= w *)
4.139 +(*An alternative condition is 0 \<le> w *)
4.140 lemma nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)"
4.141 apply (subst zless_int [symmetric])
4.142 apply (simp (no_asm_simp) add: not_neg_nat not_neg_eq_ge_0 order_le_less)
4.143 @@ -355,34 +355,34 @@
4.144
4.145 subsection{*Monotonicity of Multiplication*}
4.146
4.147 -lemma zmult_zle_mono1_lemma: "i <= (j::int) ==> i * int k <= j * int k"
4.148 +lemma zmult_zle_mono1_lemma: "i \<le> (j::int) ==> i * int k \<le> j * int k"
4.149 apply (induct_tac "k")
4.150 apply (simp_all (no_asm_simp) add: int_Suc zadd_zmult_distrib2 zadd_zle_mono int_Suc0_eq_1)
4.151 done
4.152
4.153 -lemma zmult_zle_mono1: "[| i <= j; (0::int) <= k |] ==> i*k <= j*k"
4.154 +lemma zmult_zle_mono1: "[| i \<le> j; (0::int) \<le> k |] ==> i*k \<le> j*k"
4.155 apply (rule_tac t = k in not_neg_nat [THEN subst])
4.156 apply (erule_tac [2] zmult_zle_mono1_lemma)
4.157 apply (simp (no_asm_use) add: not_neg_eq_ge_0)
4.158 done
4.159
4.160 -lemma zmult_zle_mono1_neg: "[| i <= j; k <= (0::int) |] ==> j*k <= i*k"
4.161 +lemma zmult_zle_mono1_neg: "[| i \<le> j; k \<le> (0::int) |] ==> j*k \<le> i*k"
4.162 apply (rule zminus_zle_zminus [THEN iffD1])
4.163 apply (simp add: zmult_zminus_right [symmetric] zmult_zle_mono1 zle_zminus)
4.164 done
4.165
4.166 -lemma zmult_zle_mono2: "[| i <= j; (0::int) <= k |] ==> k*i <= k*j"
4.167 +lemma zmult_zle_mono2: "[| i \<le> j; (0::int) \<le> k |] ==> k*i \<le> k*j"
4.168 apply (drule zmult_zle_mono1)
4.169 apply (simp_all add: zmult_commute)
4.170 done
4.171
4.172 -lemma zmult_zle_mono2_neg: "[| i <= j; k <= (0::int) |] ==> k*j <= k*i"
4.173 +lemma zmult_zle_mono2_neg: "[| i \<le> j; k \<le> (0::int) |] ==> k*j \<le> k*i"
4.174 apply (drule zmult_zle_mono1_neg)
4.175 apply (simp_all add: zmult_commute)
4.176 done
4.177
4.178 -(* <= monotonicity, BOTH arguments*)
4.179 -lemma zmult_zle_mono: "[| i <= j; k <= l; (0::int) <= j; (0::int) <= k |] ==> i*k <= j*l"
4.180 +(* \<le> monotonicity, BOTH arguments*)
4.181 +lemma zmult_zle_mono: "[| i \<le> j; k \<le> l; (0::int) \<le> j; (0::int) \<le> k |] ==> i*k \<le> j*l"
4.182 apply (erule zmult_zle_mono1 [THEN order_trans], assumption)
4.183 apply (erule zmult_zle_mono2, assumption)
4.184 done
4.185 @@ -404,75 +404,71 @@
4.186 apply (frule conjI [THEN zless_nat_conj [THEN iffD2]], auto)
4.187 done
4.188
4.189 +text{*The Integers Form an Ordered Ring*}
4.190 +instance int :: ordered_ring
4.191 +proof
4.192 + fix i j k :: int
4.193 + show "(i + j) + k = i + (j + k)" by simp
4.194 + show "i + j = j + i" by simp
4.195 + show "0 + i = i" by simp
4.196 + show "- i + i = 0" by simp
4.197 + show "i - j = i + (-j)" by simp
4.198 + show "(i * j) * k = i * (j * k)" by (rule zmult_assoc)
4.199 + show "i * j = j * i" by (rule zmult_commute)
4.200 + show "1 * i = i" by simp
4.201 + show "(i + j) * k = i * k + j * k" by (simp add: int_distrib)
4.202 + show "0 \<noteq> (1::int)" by simp
4.203 + show "i \<le> j ==> k + i \<le> k + j" by simp
4.204 + show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: zmult_zless_mono2)
4.205 + show "\<bar>i\<bar> = (if i < 0 then -i else i)" by (simp only: zabs_def)
4.206 +qed
4.207 +
4.208 lemma zmult_zless_mono1: "[| i<j; (0::int) < k |] ==> i*k < j*k"
4.209 -apply (drule zmult_zless_mono2)
4.210 -apply (simp_all add: zmult_commute)
4.211 -done
4.212 + by (rule Ring_and_Field.mult_strict_right_mono)
4.213
4.214 (* < monotonicity, BOTH arguments*)
4.215 -lemma zmult_zless_mono: "[| i < j; k < l; (0::int) < j; (0::int) < k |] ==> i*k < j*l"
4.216 -apply (erule zmult_zless_mono1 [THEN order_less_trans], assumption)
4.217 -apply (erule zmult_zless_mono2, assumption)
4.218 -done
4.219 +lemma zmult_zless_mono:
4.220 + "[| i < j; k < l; (0::int) < j; (0::int) < k |] ==> i*k < j*l"
4.221 + by (rule Ring_and_Field.mult_strict_mono)
4.222
4.223 lemma zmult_zless_mono1_neg: "[| i<j; k < (0::int) |] ==> j*k < i*k"
4.224 -apply (rule zminus_zless_zminus [THEN iffD1])
4.225 -apply (simp add: zmult_zminus_right [symmetric] zmult_zless_mono1 zless_zminus)
4.226 -done
4.227 + by (rule Ring_and_Field.mult_strict_right_mono_neg)
4.228
4.229 lemma zmult_zless_mono2_neg: "[| i<j; k < (0::int) |] ==> k*j < k*i"
4.230 -apply (rule zminus_zless_zminus [THEN iffD1])
4.231 -apply (simp add: zmult_zminus [symmetric] zmult_zless_mono2 zless_zminus)
4.232 -done
4.233 + by (rule Ring_and_Field.mult_strict_left_mono_neg)
4.234
4.235 lemma zmult_eq_0_iff [iff]: "(m*n = (0::int)) = (m = 0 | n = 0)"
4.236 -apply (case_tac "m < (0::int) ")
4.237 -apply (auto simp add: linorder_not_less order_le_less linorder_neq_iff)
4.238 -apply (force dest: zmult_zless_mono1_neg zmult_zless_mono1)+
4.239 -done
4.240 + by simp
4.241
4.242 -
4.243 -text{*Cancellation laws for k*m < k*n and m*k < n*k, also for <= and =,
4.244 - but not (yet?) for k*m < n*k.*}
4.245 -
4.246 -lemma zmult_zless_cancel2: "(m*k < n*k) = (((0::int) < k & m<n) | (k < 0 & n<m))"
4.247 -apply (case_tac "k = (0::int) ")
4.248 -apply (auto simp add: linorder_neq_iff zmult_zless_mono1 zmult_zless_mono1_neg)
4.249 -apply (auto simp add: linorder_not_less
4.250 - linorder_not_le [symmetric, of "m*k"]
4.251 - linorder_not_le [symmetric, of m])
4.252 -apply (erule_tac [!] notE)
4.253 -apply (auto simp add: order_less_imp_le zmult_zle_mono1 zmult_zle_mono1_neg)
4.254 -done
4.255 -
4.256 +lemma zmult_zless_cancel2: "(m*k < n*k) = (((0::int) < k & m<n) | (k<0 & n<m))"
4.257 + by (rule Ring_and_Field.mult_less_cancel_right)
4.258
4.259 lemma zmult_zless_cancel1:
4.260 "(k*m < k*n) = (((0::int) < k & m<n) | (k < 0 & n<m))"
4.261 -by (simp add: zmult_commute [of k] zmult_zless_cancel2)
4.262 + by (rule Ring_and_Field.mult_less_cancel_left)
4.263
4.264 lemma zmult_zle_cancel2:
4.265 - "(m*k <= n*k) = (((0::int) < k --> m<=n) & (k < 0 --> n<=m))"
4.266 -by (simp add: linorder_not_less [symmetric] zmult_zless_cancel2)
4.267 + "(m*k \<le> n*k) = (((0::int) < k --> m\<le>n) & (k < 0 --> n\<le>m))"
4.268 + by (rule Ring_and_Field.mult_le_cancel_right)
4.269
4.270 lemma zmult_zle_cancel1:
4.271 - "(k*m <= k*n) = (((0::int) < k --> m<=n) & (k < 0 --> n<=m))"
4.272 -by (simp add: linorder_not_less [symmetric] zmult_zless_cancel1)
4.273 + "(k*m \<le> k*n) = (((0::int) < k --> m\<le>n) & (k < 0 --> n\<le>m))"
4.274 + by (rule Ring_and_Field.mult_le_cancel_left)
4.275
4.276 -lemma zmult_cancel2 [simp]: "(m*k = n*k) = (k = (0::int) | m=n)"
4.277 -apply (cut_tac linorder_less_linear [of 0 k])
4.278 -apply (force dest: zmult_zless_mono1_neg zmult_zless_mono1
4.279 - simp add: linorder_neq_iff)
4.280 -done
4.281 +lemma zmult_cancel2: "(m*k = n*k) = (k = (0::int) | m=n)"
4.282 + by (rule Ring_and_Field.mult_cancel_right)
4.283
4.284 lemma zmult_cancel1 [simp]: "(k*m = k*n) = (k = (0::int) | m=n)"
4.285 -by (simp add: zmult_commute [of k] zmult_cancel2)
4.286 + by (rule Ring_and_Field.mult_cancel_left)
4.287
4.288 (*Analogous to zadd_int*)
4.289 -lemma zdiff_int [rule_format (no_asm)]: "n<=m --> int m - int n = int (m-n)"
4.290 +lemma zdiff_int [rule_format]: "n\<le>m --> int m - int n = int (m-n)"
4.291 apply (induct_tac m n rule: diff_induct)
4.292 apply (auto simp add: int_Suc symmetric zdiff_def)
4.293 done
4.294
4.295 +
4.296 +
4.297 ML
4.298 {*
4.299 val zminus_zdiff_eq = thm "zminus_zdiff_eq";
5.1 --- a/src/HOL/Integ/IntArith.thy Fri Nov 21 11:15:40 2003 +0100
5.2 +++ b/src/HOL/Integ/IntArith.thy Mon Nov 24 15:33:07 2003 +0100
5.3 @@ -233,48 +233,34 @@
5.4 subsection{*Some convenient biconditionals for products of signs*}
5.5
5.6 lemma zmult_pos: "[| (0::int) < i; 0 < j |] ==> 0 < i*j"
5.7 -by (drule zmult_zless_mono1, auto)
5.8 + by (rule Ring_and_Field.mult_pos)
5.9
5.10 lemma zmult_neg: "[| i < (0::int); j < 0 |] ==> 0 < i*j"
5.11 -by (drule zmult_zless_mono1_neg, auto)
5.12 + by (rule Ring_and_Field.mult_neg)
5.13
5.14 lemma zmult_pos_neg: "[| (0::int) < i; j < 0 |] ==> i*j < 0"
5.15 -by (drule zmult_zless_mono1_neg, auto)
5.16 + by (rule Ring_and_Field.mult_pos_neg)
5.17
5.18 lemma int_0_less_mult_iff: "((0::int) < x*y) = (0 < x & 0 < y | x < 0 & y < 0)"
5.19 -apply (auto simp add: order_le_less linorder_not_less zmult_pos zmult_neg)
5.20 -apply (rule_tac [!] ccontr)
5.21 -apply (auto simp add: order_le_less linorder_not_less)
5.22 -apply (erule_tac [!] rev_mp)
5.23 -apply (drule_tac [!] zmult_pos_neg)
5.24 -apply (auto dest: order_less_not_sym simp add: zmult_commute)
5.25 -done
5.26 + by (rule Ring_and_Field.zero_less_mult_iff)
5.27
5.28 lemma int_0_le_mult_iff: "((0::int) \<le> x*y) = (0 \<le> x & 0 \<le> y | x \<le> 0 & y \<le> 0)"
5.29 -by (auto simp add: order_le_less linorder_not_less int_0_less_mult_iff)
5.30 + by (rule Ring_and_Field.zero_le_mult_iff)
5.31
5.32 lemma zmult_less_0_iff: "(x*y < (0::int)) = (0 < x & y < 0 | x < 0 & 0 < y)"
5.33 -by (auto simp add: int_0_le_mult_iff linorder_not_le [symmetric])
5.34 + by (rule Ring_and_Field.mult_less_0_iff)
5.35
5.36 lemma zmult_le_0_iff: "(x*y \<le> (0::int)) = (0 \<le> x & y \<le> 0 | x \<le> 0 & 0 \<le> y)"
5.37 -by (auto dest: order_less_not_sym simp add: int_0_less_mult_iff linorder_not_less [symmetric])
5.38 -
5.39 -lemma abs_mult: "abs (x * y) = abs x * abs (y::int)"
5.40 -by (simp del: number_of_reorient split
5.41 - add: zabs_split split add: zabs_split add: zmult_less_0_iff zle_def)
5.42 + by (rule Ring_and_Field.mult_le_0_iff)
5.43
5.44 lemma abs_eq_0 [iff]: "(abs x = 0) = (x = (0::int))"
5.45 -by (simp split add: zabs_split)
5.46 + by (rule Ring_and_Field.abs_eq_0)
5.47
5.48 lemma zero_less_abs_iff [iff]: "(0 < abs x) = (x ~= (0::int))"
5.49 -by (simp split add: zabs_split, arith)
5.50 + by (rule Ring_and_Field.zero_less_abs_iff)
5.51
5.52 -(* THIS LOOKS WRONG: [intro]*)
5.53 lemma square_nonzero [simp]: "0 \<le> x * (x::int)"
5.54 -apply (subgoal_tac " (- x) * x \<le> 0")
5.55 - apply simp
5.56 -apply (simp only: zmult_le_0_iff, auto)
5.57 -done
5.58 + by (rule Ring_and_Field.zero_le_square)
5.59
5.60
5.61 subsection{*Products and 1, by T. M. Rasmussen*}
6.1 --- a/src/HOL/IsaMakefile Fri Nov 21 11:15:40 2003 +0100
6.2 +++ b/src/HOL/IsaMakefile Mon Nov 24 15:33:07 2003 +0100
6.3 @@ -200,7 +200,7 @@
6.4 Library/FuncSet.thy Library/Library.thy \
6.5 Library/List_Prefix.thy Library/Multiset.thy Library/NatPair.thy \
6.6 Library/Permutation.thy Library/Primes.thy Library/Quotient.thy \
6.7 - Library/Ring_and_Field_Example.thy Library/Nat_Infinity.thy \
6.8 + Library/Nat_Infinity.thy \
6.9 Library/README.html Library/Continuity.thy \
6.10 Library/Nested_Environment.thy Library/Rational_Numbers.thy \
6.11 Library/Zorn.thy\
7.1 --- a/src/HOL/Library/Library.thy Fri Nov 21 11:15:40 2003 +0100
7.2 +++ b/src/HOL/Library/Library.thy Mon Nov 24 15:33:07 2003 +0100
7.3 @@ -1,7 +1,6 @@
7.4 (*<*)
7.5 theory Library =
7.6 Quotient +
7.7 - Ring_and_Field + Ring_and_Field_Example +
7.8 Nat_Infinity +
7.9 Rational_Numbers +
7.10 List_Prefix +
8.1 --- a/src/HOL/Library/Ring_and_Field_Example.thy Fri Nov 21 11:15:40 2003 +0100
8.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
8.3 @@ -1,25 +0,0 @@
8.4 -
8.5 -header {* \title{}\subsection{Example: The ordered ring of integers} *}
8.6 -
8.7 -theory Ring_and_Field_Example = Main:
8.8 -
8.9 -text{*The Integers Form an Ordered Ring*}
8.10 -instance int :: ordered_ring
8.11 -proof
8.12 - fix i j k :: int
8.13 - show "(i + j) + k = i + (j + k)" by simp
8.14 - show "i + j = j + i" by simp
8.15 - show "0 + i = i" by simp
8.16 - show "- i + i = 0" by simp
8.17 - show "i - j = i + (-j)" by simp
8.18 - show "(i * j) * k = i * (j * k)" by simp
8.19 - show "i * j = j * i" by simp
8.20 - show "1 * i = i" by simp
8.21 - show "(i + j) * k = i * k + j * k" by (simp add: int_distrib)
8.22 - show "0 \<noteq> (1::int)" by simp
8.23 - show "i \<le> j ==> k + i \<le> k + j" by simp
8.24 - show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: zmult_zless_mono2)
8.25 - show "\<bar>i\<bar> = (if i < 0 then -i else i)" by (simp only: zabs_def)
8.26 -qed
8.27 -
8.28 -end
9.1 --- a/src/HOL/Nat.thy Fri Nov 21 11:15:40 2003 +0100
9.2 +++ b/src/HOL/Nat.thy Mon Nov 24 15:33:07 2003 +0100
9.3 @@ -992,7 +992,9 @@
9.4 lemma mult_less_mono1: "(i::nat) < j ==> 0 < k ==> i * k < j * k"
9.5 by (drule mult_less_mono2) (simp_all add: mult_commute)
9.6
9.7 -lemma zero_less_mult_iff [simp]: "(0 < (m::nat) * n) = (0 < m & 0 < n)"
9.8 +text{*Differs from the standard @{text zero_less_mult_iff} in that
9.9 + there are no negative numbers.*}
9.10 +lemma nat_0_less_mult_iff [simp]: "(0 < (m::nat) * n) = (0 < m & 0 < n)"
9.11 apply (induct m)
9.12 apply (case_tac [2] n, simp_all)
9.13 done
10.1 --- a/src/HOL/Real/RealOrd.thy Fri Nov 21 11:15:40 2003 +0100
10.2 +++ b/src/HOL/Real/RealOrd.thy Mon Nov 24 15:33:07 2003 +0100
10.3 @@ -27,7 +27,6 @@
10.4
10.5
10.6
10.7 -
10.8 subsection{* The Simproc @{text abel_cancel}*}
10.9
10.10 (*Deletion of other terms in the formula, seeking the -x at the front of z*)
10.11 @@ -40,8 +39,8 @@
10.12 everything gets cancelled on the right.*)
10.13 lemma real_add_cancel_end: "((x::real) + (y + z) = y) = (x = -z)"
10.14 apply (subst real_add_left_commute)
10.15 -apply (rule_tac t = "y" in real_add_zero_right [THEN subst] , subst real_add_left_cancel)
10.16 -apply (simp (no_asm) add: real_eq_diff_eq [symmetric])
10.17 +apply (rule_tac t = y in real_add_zero_right [THEN subst], subst real_add_left_cancel)
10.18 +apply (simp add: real_eq_diff_eq [symmetric])
10.19 done
10.20
10.21
10.22 @@ -87,38 +86,32 @@
10.23 Addsimprocs [Real_Cancel.sum_conv, Real_Cancel.rel_conv];
10.24 *}
10.25
10.26 -lemma real_minus_diff_eq: "- (z - y) = y - (z::real)"
10.27 -apply (simp (no_asm))
10.28 -done
10.29 -declare real_minus_diff_eq [simp]
10.30 +lemma real_minus_diff_eq [simp]: "- (z - y) = y - (z::real)"
10.31 +by simp
10.32
10.33
10.34 subsection{*Theorems About the Ordering*}
10.35
10.36 lemma real_gt_zero_preal_Ex: "(0 < x) = (\<exists>y. x = real_of_preal y)"
10.37 apply (auto simp add: real_of_preal_zero_less)
10.38 -apply (cut_tac x = "x" in real_of_preal_trichotomy)
10.39 +apply (cut_tac x = x in real_of_preal_trichotomy)
10.40 apply (blast elim!: real_less_irrefl real_of_preal_not_minus_gt_zero [THEN notE])
10.41 done
10.42
10.43 lemma real_gt_preal_preal_Ex: "real_of_preal z < x ==> \<exists>y. x = real_of_preal y"
10.44 -apply (blast dest!: real_of_preal_zero_less [THEN real_less_trans]
10.45 +by (blast dest!: real_of_preal_zero_less [THEN real_less_trans]
10.46 intro: real_gt_zero_preal_Ex [THEN iffD1])
10.47 -done
10.48
10.49 lemma real_ge_preal_preal_Ex: "real_of_preal z \<le> x ==> \<exists>y. x = real_of_preal y"
10.50 -apply (blast dest: order_le_imp_less_or_eq real_gt_preal_preal_Ex)
10.51 -done
10.52 +by (blast dest: order_le_imp_less_or_eq real_gt_preal_preal_Ex)
10.53
10.54 lemma real_less_all_preal: "y \<le> 0 ==> \<forall>x. y < real_of_preal x"
10.55 -apply (auto elim: order_le_imp_less_or_eq [THEN disjE]
10.56 +by (auto elim: order_le_imp_less_or_eq [THEN disjE]
10.57 intro: real_of_preal_zero_less [THEN [2] real_less_trans]
10.58 simp add: real_of_preal_zero_less)
10.59 -done
10.60
10.61 lemma real_less_all_real2: "~ 0 < y ==> \<forall>x. y < real_of_preal x"
10.62 -apply (blast intro!: real_less_all_preal real_leI)
10.63 -done
10.64 +by (blast intro!: real_less_all_preal real_leI)
10.65
10.66 lemma real_lemma_add_positive_imp_less: "[| R + L = S; (0::real) < L |] ==> R < S"
10.67 apply (rule real_less_sum_gt_0_iff [THEN iffD1])
10.68 @@ -126,17 +119,15 @@
10.69 done
10.70
10.71 lemma real_ex_add_positive_left_less: "\<exists>T::real. 0 < T & R + T = S ==> R < S"
10.72 -apply (blast intro: real_lemma_add_positive_imp_less)
10.73 -done
10.74 +by (blast intro: real_lemma_add_positive_imp_less)
10.75
10.76 (*Alternative definition for real_less. NOT for rewriting*)
10.77 lemma real_less_iff_add: "(R < S) = (\<exists>T::real. 0 < T & R + T = S)"
10.78 -apply (blast intro!: real_less_add_positive_left_Ex real_ex_add_positive_left_less)
10.79 -done
10.80 +by (blast intro!: real_less_add_positive_left_Ex real_ex_add_positive_left_less)
10.81
10.82 lemma real_of_preal_le_iff: "(real_of_preal m1 \<le> real_of_preal m2) = (m1 \<le> m2)"
10.83 apply (auto intro!: preal_leI simp add: real_less_le_iff [symmetric])
10.84 -apply (drule order_le_less_trans , assumption)
10.85 +apply (drule order_le_less_trans, assumption)
10.86 apply (erule preal_less_irrefl)
10.87 done
10.88
10.89 @@ -148,45 +139,33 @@
10.90
10.91 lemma neg_real_mult_order: "[| x < 0; y < 0 |] ==> (0::real) < x * y"
10.92 apply (drule real_minus_zero_less_iff [THEN iffD2])+
10.93 -apply (drule real_mult_order , assumption)
10.94 -apply simp
10.95 +apply (drule real_mult_order, assumption, simp)
10.96 done
10.97
10.98 lemma real_mult_less_0: "[| 0 < x; y < 0 |] ==> x*y < (0::real)"
10.99 apply (drule real_minus_zero_less_iff [THEN iffD2])
10.100 -apply (drule real_mult_order , assumption)
10.101 -apply (rule real_minus_zero_less_iff [THEN iffD1])
10.102 -apply simp
10.103 +apply (drule real_mult_order, assumption)
10.104 +apply (rule real_minus_zero_less_iff [THEN iffD1], simp)
10.105 done
10.106
10.107 lemma real_zero_less_one: "0 < (1::real)"
10.108 -apply (unfold real_one_def)
10.109 -apply (auto intro: real_gt_zero_preal_Ex [THEN iffD2]
10.110 - simp add: real_of_preal_def)
10.111 -done
10.112 +by (auto intro: real_gt_zero_preal_Ex [THEN iffD2]
10.113 + simp add: real_one_def real_of_preal_def)
10.114
10.115
10.116 subsection{*Monotonicity of Addition*}
10.117
10.118 -lemma real_add_right_cancel_less: "(v+z < w+z) = (v < (w::real))"
10.119 -apply (simp (no_asm))
10.120 -done
10.121 +lemma real_add_right_cancel_less [simp]: "(v+z < w+z) = (v < (w::real))"
10.122 +by simp
10.123
10.124 -lemma real_add_left_cancel_less: "(z+v < z+w) = (v < (w::real))"
10.125 -apply (simp (no_asm))
10.126 -done
10.127 +lemma real_add_left_cancel_less [simp]: "(z+v < z+w) = (v < (w::real))"
10.128 +by simp
10.129
10.130 -declare real_add_right_cancel_less [simp] real_add_left_cancel_less [simp]
10.131 +lemma real_add_right_cancel_le [simp]: "(v+z \<le> w+z) = (v \<le> (w::real))"
10.132 +by simp
10.133
10.134 -lemma real_add_right_cancel_le: "(v+z \<le> w+z) = (v \<le> (w::real))"
10.135 -apply (simp (no_asm))
10.136 -done
10.137 -
10.138 -lemma real_add_left_cancel_le: "(z+v \<le> z+w) = (v \<le> (w::real))"
10.139 -apply (simp (no_asm))
10.140 -done
10.141 -
10.142 -declare real_add_right_cancel_le [simp] real_add_left_cancel_le [simp]
10.143 +lemma real_add_left_cancel_le [simp]: "(z+v \<le> z+w) = (v \<le> (w::real))"
10.144 +by simp
10.145
10.146 (*"v\<le>w ==> v+z \<le> w+z"*)
10.147 lemmas real_add_less_mono1 = real_add_right_cancel_less [THEN iffD2, standard]
10.148 @@ -195,18 +174,13 @@
10.149 lemmas real_add_le_mono1 = real_add_right_cancel_le [THEN iffD2, standard]
10.150
10.151 lemma real_add_less_le_mono: "!!z z'::real. [| w'<w; z'\<le>z |] ==> w' + z' < w + z"
10.152 -apply (erule real_add_less_mono1 [THEN order_less_le_trans])
10.153 -apply (simp (no_asm))
10.154 -done
10.155 +by (erule real_add_less_mono1 [THEN order_less_le_trans], simp)
10.156
10.157 lemma real_add_le_less_mono: "!!z z'::real. [| w'\<le>w; z'<z |] ==> w' + z' < w + z"
10.158 -apply (erule real_add_le_mono1 [THEN order_le_less_trans])
10.159 -apply (simp (no_asm))
10.160 -done
10.161 +by (erule real_add_le_mono1 [THEN order_le_less_trans], simp)
10.162
10.163 lemma real_add_less_mono2: "!!(A::real). A < B ==> C + A < C + B"
10.164 -apply (simp (no_asm))
10.165 -done
10.166 +by simp
10.167
10.168 lemma real_less_add_right_cancel: "!!(A::real). A + C < B + C ==> A < B"
10.169 apply (simp (no_asm_use))
10.170 @@ -242,13 +216,11 @@
10.171 done
10.172
10.173 lemma real_add_left_le_mono1: "!!(q1::real). q1 \<le> q2 ==> x + q1 \<le> x + q2"
10.174 -apply (simp (no_asm))
10.175 -done
10.176 +by simp
10.177
10.178 lemma real_add_le_mono: "[|i\<le>j; k\<le>l |] ==> i + k \<le> j + (l::real)"
10.179 apply (drule real_add_le_mono1)
10.180 -apply (erule order_trans)
10.181 -apply (simp (no_asm))
10.182 +apply (erule order_trans, simp)
10.183 done
10.184
10.185 lemma real_less_Ex: "\<exists>(x::real). x < y"
10.186 @@ -258,33 +230,29 @@
10.187 done
10.188
10.189 lemma real_add_minus_positive_less_self: "(0::real) < r ==> u + (-r) < u"
10.190 -apply (rule_tac C = "r" in real_less_add_right_cancel)
10.191 -apply (simp (no_asm) add: real_add_assoc)
10.192 +apply (rule_tac C = r in real_less_add_right_cancel)
10.193 +apply (simp add: real_add_assoc)
10.194 done
10.195
10.196 -lemma real_le_minus_iff: "(-s \<le> -r) = ((r::real) \<le> s)"
10.197 -apply (rule sym)
10.198 -apply safe
10.199 +lemma real_le_minus_iff [simp]: "(-s \<le> -r) = ((r::real) \<le> s)"
10.200 +apply (rule sym, safe)
10.201 apply (drule_tac x = "-s" in real_add_left_le_mono1)
10.202 -apply (drule_tac [2] x = "r" in real_add_left_le_mono1)
10.203 -apply auto
10.204 +apply (drule_tac [2] x = r in real_add_left_le_mono1, auto)
10.205 apply (drule_tac z = "-r" in real_add_le_mono1)
10.206 -apply (drule_tac [2] z = "s" in real_add_le_mono1)
10.207 +apply (drule_tac [2] z = s in real_add_le_mono1)
10.208 apply (auto simp add: real_add_assoc)
10.209 done
10.210 -declare real_le_minus_iff [simp]
10.211
10.212 -lemma real_le_square: "(0::real) \<le> x*x"
10.213 +lemma real_le_square [simp]: "(0::real) \<le> x*x"
10.214 apply (rule_tac real_linear_less2 [of x 0])
10.215 apply (auto intro: real_mult_order neg_real_mult_order order_less_imp_le)
10.216 done
10.217 -declare real_le_square [simp]
10.218
10.219 lemma real_mult_less_mono1: "[| (0::real) < z; x < y |] ==> x*z < y*z"
10.220 apply (rotate_tac 1)
10.221 apply (drule real_less_sum_gt_zero)
10.222 apply (rule real_sum_gt_zero_less)
10.223 -apply (drule real_mult_order , assumption)
10.224 +apply (drule real_mult_order, assumption)
10.225 apply (simp add: real_add_mult_distrib2 real_mult_commute)
10.226 done
10.227
10.228 @@ -314,7 +282,7 @@
10.229 show "x < y ==> 0 < z ==> z * x < z * y" by (simp add: real_mult_less_mono2)
10.230 show "\<bar>x\<bar> = (if x < 0 then -x else x)"
10.231 by (auto dest: order_le_less_trans simp add: real_abs_def linorder_not_le)
10.232 - show "x \<noteq> 0 ==> inverse x * x = 1" by simp;
10.233 + show "x \<noteq> 0 ==> inverse x * x = 1" by simp
10.234 show "y \<noteq> 0 ==> x / y = x * inverse y" by (simp add: real_divide_def)
10.235 qed
10.236
10.237 @@ -325,17 +293,14 @@
10.238 ----------------------------------------------------------------------------*)
10.239
10.240 lemma real_of_posnat_one: "real_of_posnat 0 = (1::real)"
10.241 -
10.242 -apply (unfold real_of_posnat_def)
10.243 -apply (simp (no_asm) add: pnat_one_iff [symmetric] real_of_preal_def symmetric real_one_def)
10.244 -done
10.245 +by (simp add: real_of_posnat_def pnat_one_iff [symmetric]
10.246 + real_of_preal_def symmetric real_one_def)
10.247
10.248 lemma real_of_posnat_two: "real_of_posnat (Suc 0) = (1::real) + (1::real)"
10.249 -apply (simp add: real_of_posnat_def real_of_preal_def real_one_def pnat_two_eq
10.250 +by (simp add: real_of_posnat_def real_of_preal_def real_one_def pnat_two_eq
10.251 real_add
10.252 prat_of_pnat_add [symmetric] preal_of_prat_add [symmetric]
10.253 pnat_add_ac)
10.254 -done
10.255
10.256 lemma real_of_posnat_add:
10.257 "real_of_posnat n1 + real_of_posnat n2 = real_of_posnat (n1 + n2) + (1::real)"
10.258 @@ -350,9 +315,7 @@
10.259 done
10.260
10.261 lemma real_of_posnat_Suc: "real_of_posnat (Suc n) = real_of_posnat n + (1::real)"
10.262 -apply (subst real_of_posnat_add_one [symmetric])
10.263 -apply (simp (no_asm))
10.264 -done
10.265 +by (subst real_of_posnat_add_one [symmetric], simp)
10.266
10.267 lemma inj_real_of_posnat: "inj(real_of_posnat)"
10.268 apply (rule inj_onI)
10.269 @@ -363,41 +326,28 @@
10.270 apply (erule inj_pnat_of_nat [THEN injD])
10.271 done
10.272
10.273 -lemma real_of_nat_zero: "real (0::nat) = 0"
10.274 -apply (unfold real_of_nat_def)
10.275 -apply (simp (no_asm) add: real_of_posnat_one)
10.276 -done
10.277 +lemma real_of_nat_zero [simp]: "real (0::nat) = 0"
10.278 +by (simp add: real_of_nat_def real_of_posnat_one)
10.279
10.280 -lemma real_of_nat_one: "real (Suc 0) = (1::real)"
10.281 -apply (unfold real_of_nat_def)
10.282 -apply (simp (no_asm) add: real_of_posnat_two real_add_assoc)
10.283 -done
10.284 -declare real_of_nat_zero [simp] real_of_nat_one [simp]
10.285 +lemma real_of_nat_one [simp]: "real (Suc 0) = (1::real)"
10.286 +by (simp add: real_of_nat_def real_of_posnat_two real_add_assoc)
10.287
10.288 -lemma real_of_nat_add:
10.289 +lemma real_of_nat_add [simp]:
10.290 "real (m + n) = real (m::nat) + real n"
10.291 apply (simp add: real_of_nat_def real_add_assoc)
10.292 apply (simp add: real_of_posnat_add real_add_assoc [symmetric])
10.293 done
10.294 -declare real_of_nat_add [simp]
10.295
10.296 (*Not for addsimps: often the LHS is used to represent a positive natural*)
10.297 lemma real_of_nat_Suc: "real (Suc n) = real n + (1::real)"
10.298 -apply (unfold real_of_nat_def)
10.299 -apply (simp (no_asm) add: real_of_posnat_Suc real_add_ac)
10.300 -done
10.301 +by (simp add: real_of_nat_def real_of_posnat_Suc real_add_ac)
10.302
10.303 -lemma real_of_nat_less_iff:
10.304 +lemma real_of_nat_less_iff [iff]:
10.305 "(real (n::nat) < real m) = (n < m)"
10.306 -apply (unfold real_of_nat_def real_of_posnat_def)
10.307 -apply auto
10.308 -done
10.309 -declare real_of_nat_less_iff [iff]
10.310 +by (auto simp add: real_of_nat_def real_of_posnat_def)
10.311
10.312 -lemma real_of_nat_le_iff: "(real (n::nat) \<le> real m) = (n \<le> m)"
10.313 -apply (simp (no_asm) add: linorder_not_less [symmetric])
10.314 -done
10.315 -declare real_of_nat_le_iff [iff]
10.316 +lemma real_of_nat_le_iff [iff]: "(real (n::nat) \<le> real m) = (n \<le> m)"
10.317 +by (simp add: linorder_not_less [symmetric])
10.318
10.319 lemma inj_real_of_nat: "inj (real :: nat => real)"
10.320 apply (rule inj_onI)
10.321 @@ -405,27 +355,24 @@
10.322 simp add: real_of_nat_def real_add_right_cancel)
10.323 done
10.324
10.325 -lemma real_of_nat_ge_zero: "0 \<le> real (n::nat)"
10.326 +lemma real_of_nat_ge_zero [iff]: "0 \<le> real (n::nat)"
10.327 apply (induct_tac "n")
10.328 apply (auto simp add: real_of_nat_Suc)
10.329 apply (drule real_add_le_less_mono)
10.330 apply (rule real_zero_less_one)
10.331 apply (simp add: order_less_imp_le)
10.332 done
10.333 -declare real_of_nat_ge_zero [iff]
10.334
10.335 -lemma real_of_nat_mult: "real (m * n) = real (m::nat) * real n"
10.336 +lemma real_of_nat_mult [simp]: "real (m * n) = real (m::nat) * real n"
10.337 apply (induct_tac "m")
10.338 apply (auto simp add: real_of_nat_Suc real_add_mult_distrib real_add_commute)
10.339 done
10.340 -declare real_of_nat_mult [simp]
10.341
10.342 -lemma real_of_nat_inject: "(real (n::nat) = real m) = (n = m)"
10.343 -apply (auto dest: inj_real_of_nat [THEN injD])
10.344 -done
10.345 -declare real_of_nat_inject [iff]
10.346 +lemma real_of_nat_inject [iff]: "(real (n::nat) = real m) = (n = m)"
10.347 +by (auto dest: inj_real_of_nat [THEN injD])
10.348
10.349 -lemma real_of_nat_diff [rule_format (no_asm)]: "n \<le> m --> real (m - n) = real (m::nat) - real n"
10.350 +lemma real_of_nat_diff [rule_format]:
10.351 + "n \<le> m --> real (m - n) = real (m::nat) - real n"
10.352 apply (induct_tac "m")
10.353 apply (auto simp add: real_diff_def Suc_diff_le le_Suc_eq real_of_nat_Suc real_of_nat_zero real_add_ac)
10.354 done
10.355 @@ -439,10 +386,9 @@
10.356 show "n = 0 \<Longrightarrow> real n = 0" by simp
10.357 qed
10.358
10.359 -lemma real_of_nat_neg_int: "neg z ==> real (nat z) = 0"
10.360 +lemma real_of_nat_neg_int [simp]: "neg z ==> real (nat z) = 0"
10.361 apply (simp (no_asm_simp) add: neg_nat real_of_nat_zero)
10.362 done
10.363 -declare real_of_nat_neg_int [simp]
10.364
10.365
10.366 (*----------------------------------------------------------------------------
10.367 @@ -455,8 +401,7 @@
10.368 apply (frule real_minus_zero_less_iff2 [THEN iffD2])
10.369 apply (frule real_not_refl2 [THEN not_sym])
10.370 apply (drule real_not_refl2 [THEN not_sym, THEN real_inverse_not_zero])
10.371 -apply (drule order_le_imp_less_or_eq)
10.372 -apply safe;
10.373 +apply (drule order_le_imp_less_or_eq, safe)
10.374 apply (drule neg_real_mult_order, assumption)
10.375 apply (auto intro: real_zero_less_one [THEN real_less_asym])
10.376 done
10.377 @@ -470,38 +415,26 @@
10.378 done
10.379
10.380 lemma real_mult_less_cancel1: "[| (0::real) < z; x * z < y * z |] ==> x < y"
10.381 -apply (frule_tac x = "x*z" in real_inverse_gt_0 [THEN real_mult_less_mono1])
10.382 -apply (auto simp add: real_mult_assoc real_not_refl2 [THEN not_sym])
10.383 -done
10.384 +by (force simp add: Ring_and_Field.mult_less_cancel_right
10.385 + elim: order_less_asym)
10.386
10.387 lemma real_mult_less_cancel2: "[| (0::real) < z; z*x < z*y |] ==> x < y"
10.388 apply (erule real_mult_less_cancel1)
10.389 apply (simp add: real_mult_commute)
10.390 done
10.391
10.392 -lemma real_mult_less_iff1: "(0::real) < z ==> (x*z < y*z) = (x < y)"
10.393 -apply (blast intro: real_mult_less_mono1 real_mult_less_cancel1)
10.394 -done
10.395 +lemma real_mult_less_iff1 [simp]: "(0::real) < z ==> (x*z < y*z) = (x < y)"
10.396 +by (blast intro: real_mult_less_mono1 real_mult_less_cancel1)
10.397
10.398 -lemma real_mult_less_iff2: "(0::real) < z ==> (z*x < z*y) = (x < y)"
10.399 -apply (blast intro: real_mult_less_mono2 real_mult_less_cancel2)
10.400 -done
10.401 -
10.402 -declare real_mult_less_iff1 [simp] real_mult_less_iff2 [simp]
10.403 +lemma real_mult_less_iff2 [simp]: "(0::real) < z ==> (z*x < z*y) = (x < y)"
10.404 +by (blast intro: real_mult_less_mono2 real_mult_less_cancel2)
10.405
10.406 (* 05/00 *)
10.407 -lemma real_mult_le_cancel_iff1: "(0::real) < z ==> (x*z \<le> y*z) = (x \<le> y)"
10.408 -apply (unfold real_le_def)
10.409 -apply auto
10.410 -done
10.411 +lemma real_mult_le_cancel_iff1 [simp]: "(0::real) < z ==> (x*z \<le> y*z) = (x \<le> y)"
10.412 +by (auto simp add: real_le_def)
10.413
10.414 -lemma real_mult_le_cancel_iff2: "(0::real) < z ==> (z*x \<le> z*y) = (x \<le> y)"
10.415 -apply (unfold real_le_def)
10.416 -apply auto
10.417 -done
10.418 -
10.419 -declare real_mult_le_cancel_iff1 [simp] real_mult_le_cancel_iff2 [simp]
10.420 -
10.421 +lemma real_mult_le_cancel_iff2 [simp]: "(0::real) < z ==> (z*x \<le> z*y) = (x \<le> y)"
10.422 +by (auto simp add: real_le_def)
10.423
10.424 lemma real_mult_le_less_mono1: "[| (0::real) \<le> z; x < y |] ==> x*z \<le> y*z"
10.425 apply (rule real_less_or_eq_imp_le)
10.426 @@ -510,29 +443,22 @@
10.427 done
10.428
10.429 lemma real_mult_less_mono: "[| u<v; x<y; (0::real) < v; 0 < x |] ==> u*x < v* y"
10.430 -apply (erule real_mult_less_mono1 [THEN order_less_trans])
10.431 -apply assumption
10.432 -apply (erule real_mult_less_mono2)
10.433 -apply assumption
10.434 -done
10.435 + by (rule Ring_and_Field.mult_strict_mono)
10.436
10.437 -(*Variant of the theorem above; sometimes it's stronger*)
10.438 -lemma real_mult_less_mono': "[| x < y; r1 < r2; (0::real) \<le> r1; 0 \<le> x|] ==> r1 * x < r2 * y"
10.439 +text{*Variant of the theorem above; sometimes it's stronger*}
10.440 +lemma real_mult_less_mono':
10.441 + "[| x < y; r1 < r2; (0::real) \<le> r1; 0 \<le> x|] ==> r1 * x < r2 * y"
10.442 apply (subgoal_tac "0<r2")
10.443 -prefer 2 apply (blast intro: order_le_less_trans)
10.444 + prefer 2 apply (blast intro: order_le_less_trans)
10.445 apply (case_tac "x=0")
10.446 -apply (auto dest!: order_le_imp_less_or_eq intro: real_mult_less_mono real_mult_order)
10.447 -done
10.448 -
10.449 -lemma real_gt_zero: "(1::real) \<le> x ==> 0 < x"
10.450 -apply (rule ccontr , drule real_leI)
10.451 -apply (drule order_trans , assumption)
10.452 -apply (auto dest: real_zero_less_one [THEN [2] order_le_less_trans])
10.453 +apply (auto dest!: order_le_imp_less_or_eq
10.454 + intro: real_mult_less_mono real_mult_order)
10.455 done
10.456
10.457 lemma real_mult_self_le: "[| (1::real) < r; (1::real) \<le> x |] ==> x \<le> r * x"
10.458 -apply (drule real_gt_zero [THEN order_less_imp_le])
10.459 -apply (auto dest!: real_mult_le_less_mono1)
10.460 +apply (subgoal_tac "0\<le>x")
10.461 +apply (force dest!: real_mult_le_less_mono1)
10.462 +apply (force intro: order_trans [OF zero_less_one [THEN order_less_imp_le]])
10.463 done
10.464
10.465 lemma real_mult_self_le2: "[| (1::real) \<le> r; (1::real) \<le> x |] ==> x \<le> r * x"
10.466 @@ -541,11 +467,10 @@
10.467 done
10.468
10.469 lemma real_inverse_less_swap: "[| 0 < r; r < x |] ==> inverse x < inverse (r::real)"
10.470 -apply (frule order_less_trans , assumption)
10.471 +apply (frule order_less_trans, assumption)
10.472 apply (frule real_inverse_gt_0)
10.473 -apply (frule_tac x = "x" in real_inverse_gt_0)
10.474 -apply (frule_tac x = "r" and z = "inverse r" in real_mult_less_mono1)
10.475 -apply assumption
10.476 +apply (frule_tac x = x in real_inverse_gt_0)
10.477 +apply (frule_tac x = r and z = "inverse r" in real_mult_less_mono1, assumption)
10.478 apply (simp add: real_not_refl2 [THEN not_sym, THEN real_mult_inv_right])
10.479 apply (frule real_inverse_gt_0)
10.480 apply (frule_tac x = " (1::real) " and z = "inverse x" in real_mult_less_mono2)
10.481 @@ -553,10 +478,8 @@
10.482 apply (simp add: real_not_refl2 [THEN not_sym, THEN real_mult_inv_left] real_mult_assoc [symmetric])
10.483 done
10.484
10.485 -lemma real_mult_is_0: "(x*y = 0) = (x = 0 | y = (0::real))"
10.486 -apply auto
10.487 -done
10.488 -declare real_mult_is_0 [iff]
10.489 +lemma real_mult_is_0 [iff]: "(x*y = 0) = (x = 0 | y = (0::real))"
10.490 +by auto
10.491
10.492 lemma real_inverse_add: "[| x \<noteq> 0; y \<noteq> 0 |]
10.493 ==> inverse x + inverse y = (x + y) * inverse (x * (y::real))"
10.494 @@ -567,25 +490,20 @@
10.495 done
10.496
10.497 (* 05/00 *)
10.498 -lemma real_minus_zero_le_iff: "(0 \<le> -R) = (R \<le> (0::real))"
10.499 -apply (auto dest: sym simp add: real_le_less)
10.500 -done
10.501 +lemma real_minus_zero_le_iff [simp]: "(0 \<le> -R) = (R \<le> (0::real))"
10.502 +by (auto dest: sym simp add: real_le_less)
10.503
10.504 -lemma real_minus_zero_le_iff2: "(-R \<le> 0) = ((0::real) \<le> R)"
10.505 -apply (auto simp add: real_minus_zero_less_iff2 real_le_less)
10.506 -done
10.507 -
10.508 -declare real_minus_zero_le_iff [simp] real_minus_zero_le_iff2 [simp]
10.509 +lemma real_minus_zero_le_iff2 [simp]: "(-R \<le> 0) = ((0::real) \<le> R)"
10.510 +by (auto simp add: real_minus_zero_less_iff2 real_le_less)
10.511
10.512 lemma real_sum_squares_cancel: "x * x + y * y = 0 ==> x = (0::real)"
10.513 apply (drule real_add_minus_eq_minus)
10.514 -apply (cut_tac x = "x" in real_le_square)
10.515 -apply (auto , drule real_le_anti_sym)
10.516 -apply auto
10.517 +apply (cut_tac x = x in real_le_square)
10.518 +apply (auto, drule real_le_anti_sym, auto)
10.519 done
10.520
10.521 lemma real_sum_squares_cancel2: "x * x + y * y = 0 ==> y = (0::real)"
10.522 -apply (rule_tac y = "x" in real_sum_squares_cancel)
10.523 +apply (rule_tac y = x in real_sum_squares_cancel)
10.524 apply (simp add: real_add_commute)
10.525 done
10.526
10.527 @@ -678,7 +596,6 @@
10.528 val real_mult_le_less_mono1 = thm "real_mult_le_less_mono1";
10.529 val real_mult_less_mono = thm "real_mult_less_mono";
10.530 val real_mult_less_mono' = thm "real_mult_less_mono'";
10.531 -val real_gt_zero = thm "real_gt_zero";
10.532 val real_mult_self_le = thm "real_mult_self_le";
10.533 val real_mult_self_le2 = thm "real_mult_self_le2";
10.534 val real_inverse_less_swap = thm "real_inverse_less_swap";
11.1 --- a/src/HOL/Ring_and_Field.thy Fri Nov 21 11:15:40 2003 +0100
11.2 +++ b/src/HOL/Ring_and_Field.thy Mon Nov 24 15:33:07 2003 +0100
11.3 @@ -89,10 +89,10 @@
11.4 assume eq: "a + b = a + c"
11.5 then have "(-a + a) + b = (-a + a) + c"
11.6 by (simp only: eq add_assoc)
11.7 - then show "b = c" by simp
11.8 + thus "b = c" by simp
11.9 next
11.10 assume eq: "b = c"
11.11 - then show "a + b = a + c" by simp
11.12 + thus "a + b = a + c" by simp
11.13 qed
11.14
11.15 lemma add_right_cancel [simp]:
11.16 @@ -118,12 +118,10 @@
11.17 assume "- a = - b"
11.18 then have "- (- a) = - (- b)"
11.19 by simp
11.20 - then show "a=b"
11.21 - by simp
11.22 + thus "a=b" by simp
11.23 next
11.24 assume "a=b"
11.25 - then show "-a = -b"
11.26 - by simp
11.27 + thus "-a = -b" by simp
11.28 qed
11.29
11.30 lemma neg_equal_0_iff_equal [simp]: "(-a = 0) = (a = (0::'a::ring))"
11.31 @@ -175,7 +173,7 @@
11.32 proof -
11.33 have "0*a + 0*a = 0*a + 0"
11.34 by (simp add: left_distrib [symmetric])
11.35 - then show ?thesis by (simp only: add_left_cancel)
11.36 + thus ?thesis by (simp only: add_left_cancel)
11.37 qed
11.38
11.39 lemma mult_right_zero [simp]: "a * 0 = (0::'a::ring)"
11.40 @@ -228,7 +226,7 @@
11.41 by simp
11.42 then have "0 + (-b) \<le> (-a + b) + (-b)"
11.43 by (rule add_right_mono)
11.44 - then show ?thesis
11.45 + thus ?thesis
11.46 by (simp add: add_assoc)
11.47 qed
11.48
11.49 @@ -237,12 +235,10 @@
11.50 assume "- b \<le> - a"
11.51 then have "- (- a) \<le> - (- b)"
11.52 by (rule le_imp_neg_le)
11.53 - then show "a\<le>b"
11.54 - by simp
11.55 + thus "a\<le>b" by simp
11.56 next
11.57 assume "a\<le>b"
11.58 - then show "-b \<le> -a"
11.59 - by (rule le_imp_neg_le)
11.60 + thus "-b \<le> -a" by (rule le_imp_neg_le)
11.61 qed
11.62
11.63 lemma neg_le_0_iff_le [simp]: "(-a \<le> 0) = (0 \<le> (a::'a::ordered_ring))"
11.64 @@ -292,6 +288,55 @@
11.65 "[|b \<le> a; c < 0|] ==> a * c \<le> b * (c::'a::ordered_ring)"
11.66 by (force simp add: mult_strict_right_mono_neg order_le_less)
11.67
11.68 +text{*Strict monotonicity in both arguments*}
11.69 +lemma mult_strict_mono:
11.70 + "[|a<b; c<d; 0<b; 0<c|] ==> a * c < b * (d::'a::ordered_semiring)"
11.71 +apply (erule mult_strict_right_mono [THEN order_less_trans], assumption)
11.72 +apply (erule mult_strict_left_mono, assumption)
11.73 +done
11.74 +
11.75 +subsection{*Cancellation Laws for Relationships With a Common Factor*}
11.76 +
11.77 +text{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"},
11.78 + also with the relations @{text "\<le>"} and equality.*}
11.79 +
11.80 +lemma mult_less_cancel_right:
11.81 + "(a*c < b*c) = ((0 < c & a < b) | (c < 0 & b < (a::'a::ordered_ring)))"
11.82 +apply (case_tac "c = 0")
11.83 +apply (auto simp add: linorder_neq_iff mult_strict_right_mono
11.84 + mult_strict_right_mono_neg)
11.85 +apply (auto simp add: linorder_not_less
11.86 + linorder_not_le [symmetric, of "a*c"]
11.87 + linorder_not_le [symmetric, of a])
11.88 +apply (erule_tac [!] notE)
11.89 +apply (auto simp add: order_less_imp_le mult_right_mono
11.90 + mult_right_mono_neg)
11.91 +done
11.92 +
11.93 +lemma mult_less_cancel_left:
11.94 + "(c*a < c*b) = ((0 < c & a < b) | (c < 0 & b < (a::'a::ordered_ring)))"
11.95 +by (simp add: mult_commute [of c] mult_less_cancel_right)
11.96 +
11.97 +lemma mult_le_cancel_right:
11.98 + "(a*c \<le> b*c) = ((0<c --> a\<le>b) & (c<0 --> b \<le> (a::'a::ordered_ring)))"
11.99 +by (simp add: linorder_not_less [symmetric] mult_less_cancel_right)
11.100 +
11.101 +lemma mult_le_cancel_left:
11.102 + "(c*a \<le> c*b) = ((0<c --> a\<le>b) & (c<0 --> b \<le> (a::'a::ordered_ring)))"
11.103 +by (simp add: mult_commute [of c] mult_le_cancel_right)
11.104 +
11.105 +text{*Cancellation of equalities with a common factor*}
11.106 +lemma mult_cancel_right [simp]:
11.107 + "(a*c = b*c) = (c = (0::'a::ordered_ring) | a=b)"
11.108 +apply (cut_tac linorder_less_linear [of 0 c])
11.109 +apply (force dest: mult_strict_right_mono_neg mult_strict_right_mono
11.110 + simp add: linorder_neq_iff)
11.111 +done
11.112 +
11.113 +lemma mult_cancel_left [simp]:
11.114 + "(c*a = c*b) = (c = (0::'a::ordered_ring) | a=b)"
11.115 +by (simp add: mult_commute [of c] mult_cancel_right)
11.116 +
11.117
11.118 subsection{* Products of Signs *}
11.119
11.120 @@ -319,8 +364,7 @@
11.121 apply (blast dest: zero_less_mult_pos)
11.122 done
11.123
11.124 -
11.125 -lemma mult_eq_0_iff [iff]: "(a*b = (0::'a::ordered_ring)) = (a = 0 | b = 0)"
11.126 +lemma mult_eq_0_iff [simp]: "(a*b = (0::'a::ordered_ring)) = (a = 0 | b = 0)"
11.127 apply (case_tac "a < 0")
11.128 apply (auto simp add: linorder_not_less order_le_less linorder_neq_iff)
11.129 apply (force dest: mult_strict_right_mono_neg mult_strict_right_mono)+
11.130 @@ -369,10 +413,10 @@
11.131 minus_mult_left [symmetric] minus_mult_right [symmetric])
11.132 done
11.133
11.134 -lemma abs_eq_0 [iff]: "(abs x = 0) = (x = (0::'a::ordered_ring))"
11.135 +lemma abs_eq_0 [simp]: "(abs x = 0) = (x = (0::'a::ordered_ring))"
11.136 by (simp add: abs_if)
11.137
11.138 -lemma zero_less_abs_iff [iff]: "(0 < abs x) = (x ~= (0::'a::ordered_ring))"
11.139 +lemma zero_less_abs_iff [simp]: "(0 < abs x) = (x ~= (0::'a::ordered_ring))"
11.140 by (simp add: abs_if linorder_neq_iff)
11.141
11.142