conversion of integers to use Ring_and_Field;
authorpaulson
Mon Nov 24 15:33:07 2003 +0100 (2003-11-24)
changeset 1426608b34c902618
parent 14265 95b42e69436c
child 14267 b963e9cee2a0
conversion of integers to use Ring_and_Field;
new lemmas for Ring_and_Field
src/HOL/Hyperreal/Poly.ML
src/HOL/Hyperreal/Transcendental.ML
src/HOL/Integ/Bin.ML
src/HOL/Integ/Int.thy
src/HOL/Integ/IntArith.thy
src/HOL/IsaMakefile
src/HOL/Library/Library.thy
src/HOL/Library/Ring_and_Field_Example.thy
src/HOL/Nat.thy
src/HOL/Real/RealOrd.thy
src/HOL/Ring_and_Field.thy
     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,74 +404,70 @@
   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 +  by simp
   4.240 +
   4.241 +lemma zmult_zless_cancel2: "(m*k < n*k) = (((0::int) < k & m<n) | (k<0 & n<m))"
   4.242 +  by (rule Ring_and_Field.mult_less_cancel_right)
   4.243 +
   4.244 +lemma zmult_zless_cancel1:
   4.245 +     "(k*m < k*n) = (((0::int) < k & m<n) | (k < 0 & n<m))"
   4.246 +  by (rule Ring_and_Field.mult_less_cancel_left)
   4.247 +
   4.248 +lemma zmult_zle_cancel2:
   4.249 +     "(m*k \<le> n*k) = (((0::int) < k --> m\<le>n) & (k < 0 --> n\<le>m))"
   4.250 +  by (rule Ring_and_Field.mult_le_cancel_right)
   4.251 +
   4.252 +lemma zmult_zle_cancel1:
   4.253 +     "(k*m \<le> k*n) = (((0::int) < k --> m\<le>n) & (k < 0 --> n\<le>m))"
   4.254 +  by (rule Ring_and_Field.mult_le_cancel_left)
   4.255 +
   4.256 +lemma zmult_cancel2: "(m*k = n*k) = (k = (0::int) | m=n)"
   4.257 + by (rule Ring_and_Field.mult_cancel_right)
   4.258 +
   4.259 +lemma zmult_cancel1 [simp]: "(k*m = k*n) = (k = (0::int) | m=n)"
   4.260 + by (rule Ring_and_Field.mult_cancel_left)
   4.261 +
   4.262 +(*Analogous to zadd_int*)
   4.263 +lemma zdiff_int [rule_format]: "n\<le>m --> int m - int n = int (m-n)"
   4.264 +apply (induct_tac m n rule: diff_induct)
   4.265 +apply (auto simp add: int_Suc symmetric zdiff_def)
   4.266  done
   4.267  
   4.268  
   4.269 -text{*Cancellation laws for k*m < k*n and m*k < n*k, also for <= and =,
   4.270 -    but not (yet?) for k*m < n*k.*}
   4.271 -
   4.272 -lemma zmult_zless_cancel2: "(m*k < n*k) = (((0::int) < k & m<n) | (k < 0 & n<m))"
   4.273 -apply (case_tac "k = (0::int) ")
   4.274 -apply (auto simp add: linorder_neq_iff zmult_zless_mono1 zmult_zless_mono1_neg)
   4.275 -apply (auto simp add: linorder_not_less 
   4.276 -                      linorder_not_le [symmetric, of "m*k"]
   4.277 -                      linorder_not_le [symmetric, of m])
   4.278 -apply (erule_tac [!] notE)
   4.279 -apply (auto simp add: order_less_imp_le zmult_zle_mono1 zmult_zle_mono1_neg)
   4.280 -done
   4.281 -
   4.282 -
   4.283 -lemma zmult_zless_cancel1:
   4.284 -     "(k*m < k*n) = (((0::int) < k & m<n) | (k < 0 & n<m))"
   4.285 -by (simp add: zmult_commute [of k] zmult_zless_cancel2)
   4.286 -
   4.287 -lemma zmult_zle_cancel2:
   4.288 -     "(m*k <= n*k) = (((0::int) < k --> m<=n) & (k < 0 --> n<=m))"
   4.289 -by (simp add: linorder_not_less [symmetric] zmult_zless_cancel2)
   4.290 -
   4.291 -lemma zmult_zle_cancel1:
   4.292 -     "(k*m <= k*n) = (((0::int) < k --> m<=n) & (k < 0 --> n<=m))"
   4.293 -by (simp add: linorder_not_less [symmetric] zmult_zless_cancel1)
   4.294 -
   4.295 -lemma zmult_cancel2 [simp]: "(m*k = n*k) = (k = (0::int) | m=n)"
   4.296 -apply (cut_tac linorder_less_linear [of 0 k])
   4.297 -apply (force dest: zmult_zless_mono1_neg zmult_zless_mono1 
   4.298 -             simp add: linorder_neq_iff)
   4.299 -done
   4.300 -
   4.301 -lemma zmult_cancel1 [simp]: "(k*m = k*n) = (k = (0::int) | m=n)"
   4.302 -by (simp add: zmult_commute [of k] zmult_cancel2)
   4.303 -
   4.304 -(*Analogous to zadd_int*)
   4.305 -lemma zdiff_int [rule_format (no_asm)]: "n<=m --> int m - int n = int (m-n)"
   4.306 -apply (induct_tac m n rule: diff_induct)
   4.307 -apply (auto simp add: int_Suc symmetric zdiff_def)
   4.308 -done
   4.309  
   4.310  ML
   4.311  {*
     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 -
  10.128 -declare real_add_right_cancel_less [simp] real_add_left_cancel_less [simp]
  10.129 +lemma real_add_left_cancel_less [simp]: "(z+v < z+w) = (v < (w::real))"
  10.130 +by simp
  10.131  
  10.132 -lemma real_add_right_cancel_le: "(v+z \<le> w+z) = (v \<le> (w::real))"
  10.133 -apply (simp (no_asm))
  10.134 -done
  10.135 +lemma real_add_right_cancel_le [simp]: "(v+z \<le> w+z) = (v \<le> (w::real))"
  10.136 +by simp
  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