--- a/src/HOL/Hyperreal/Poly.ML Fri Nov 21 11:15:40 2003 +0100
+++ b/src/HOL/Hyperreal/Poly.ML Mon Nov 24 15:33:07 2003 +0100
@@ -1003,7 +1003,7 @@
by (dtac (poly_mult_left_cancel RS iffD1) 1);
by (Asm_full_simp_tac 1);
by (asm_full_simp_tac (simpset() addsimps [fun_eq,poly_mult,poly_add,poly_cmult,
- poly_minus] delsimps [pmult_Cons]) 1);
+ poly_minus] delsimps [pmult_Cons, thm"mult_cancel_left"]) 1);
by (Step_tac 1);
by (res_inst_tac [("c1","real (Suc n)")] (real_mult_left_cancel
RS iffD1) 1);
--- a/src/HOL/Hyperreal/Transcendental.ML Fri Nov 21 11:15:40 2003 +0100
+++ b/src/HOL/Hyperreal/Transcendental.ML Mon Nov 24 15:33:07 2003 +0100
@@ -559,7 +559,6 @@
addsimps [lemma_realpow_diff_sumr2,
real_diff_mult_distrib2 RS sym,real_mult_assoc]
delsimps [realpow_Suc,sumr_Suc]));
-by (rtac (real_mult_left_cancel RS iffD2) 1);
by (auto_tac (claset(),simpset() addsimps [lemma_realpow_rev_sumr]
delsimps [sumr_Suc]));
by (auto_tac (claset(),simpset() addsimps [real_of_nat_Suc,sumr_diff_mult_const,
@@ -773,7 +772,9 @@
\ (real (n - Suc 0) * abs (c n) * inverse r) * r ^ (n - Suc 0))")]
(CLAIM "(a = b) ==> a ==> b") 1 THEN assume_tac 2);
by (res_inst_tac [("f","summable")] arg_cong 1 THEN rtac ext 1);
-(* 75 *)
+by (dtac (abs_ge_zero RS order_le_less_trans) 2);
+by (asm_full_simp_tac (simpset() addsimps real_mult_ac) 2);
+(* 77 *)
by (case_tac "n" 1);
by Auto_tac;
by (case_tac "nat" 1);
@@ -1016,6 +1017,7 @@
Goal "exp(x + y) = exp(x) * exp(y)";
by (cut_inst_tac [("x1","x"),("y1","y"),("z","exp x")]
(exp_add_mult_minus RS (CLAIM "x = y ==> z * y = z * (x::real)")) 1);
+by (asm_full_simp_tac HOL_ss 1);
by (asm_full_simp_tac (simpset() delsimps [exp_add_mult_minus]
addsimps real_mult_ac) 1);
qed "exp_add";
--- a/src/HOL/Integ/Bin.ML Fri Nov 21 11:15:40 2003 +0100
+++ b/src/HOL/Integ/Bin.ML Mon Nov 24 15:33:07 2003 +0100
@@ -250,8 +250,8 @@
by (Simp_tac 1);
qed "iszero_number_of_Pls";
-Goalw [iszero_def] "~ iszero ((number_of bin.Min)::int)";
-by (Simp_tac 1);
+Goalw [iszero_def] "~ iszero ((number_of bin.Min)::int)";
+by (simp_tac (simpset() addsimps [eq_commute]) 1);
qed "nonzero_number_of_Min";
fun int_case_tac x = res_inst_tac [("z",x)] int_cases;
--- a/src/HOL/Integ/Int.thy Fri Nov 21 11:15:40 2003 +0100
+++ b/src/HOL/Integ/Int.thy Mon Nov 24 15:33:07 2003 +0100
@@ -37,7 +37,7 @@
lemma neg_eq_less_0: "neg x = (x < 0)"
by (unfold zdiff_def zless_def, auto)
-lemma not_neg_eq_ge_0: "(~neg x) = (0 <= x)"
+lemma not_neg_eq_ge_0: "(~neg x) = (0 \<le> x)"
apply (unfold zle_def)
apply (simp add: neg_eq_less_0)
done
@@ -152,7 +152,7 @@
lemma eq_eq_iszero: "(w=z) = iszero(w-z)"
by (simp add: iszero_def zdiff_eq_eq)
-lemma zle_eq_not_neg: "(w<=z) = (~ neg(z-w))"
+lemma zle_eq_not_neg: "(w\<le>z) = (~ neg(z-w))"
by (simp add: zle_def zless_def)
subsection{*Inequality reasoning*}
@@ -163,13 +163,13 @@
apply (simp add: int_Suc)
done
-lemma add1_zle_eq: "(w + (1::int) <= z) = (w<z)"
+lemma add1_zle_eq: "(w + (1::int) \<le> z) = (w<z)"
apply (simp add: zle_def zless_add1_eq)
apply (auto intro: zless_asym zle_anti_sym
simp add: order_less_imp_le symmetric zle_def)
done
-lemma add1_left_zle_eq: "((1::int) + w <= z) = (w<z)"
+lemma add1_left_zle_eq: "((1::int) + w \<le> z) = (w<z)"
apply (subst zadd_commute)
apply (rule add1_zle_eq)
done
@@ -183,28 +183,28 @@
lemma zadd_left_cancel_zless [simp]: "(z+v < z+w) = (v < (w::int))"
by simp
-lemma zadd_right_cancel_zle [simp] : "(v+z <= w+z) = (v <= (w::int))"
+lemma zadd_right_cancel_zle [simp] : "(v+z \<le> w+z) = (v \<le> (w::int))"
by simp
-lemma zadd_left_cancel_zle [simp] : "(z+v <= z+w) = (v <= (w::int))"
+lemma zadd_left_cancel_zle [simp] : "(z+v \<le> z+w) = (v \<le> (w::int))"
by simp
-(*"v<=w ==> v+z <= w+z"*)
+(*"v\<le>w ==> v+z \<le> w+z"*)
lemmas zadd_zless_mono1 = zadd_right_cancel_zless [THEN iffD2, standard]
-(*"v<=w ==> z+v <= z+w"*)
+(*"v\<le>w ==> z+v \<le> z+w"*)
lemmas zadd_zless_mono2 = zadd_left_cancel_zless [THEN iffD2, standard]
-(*"v<=w ==> v+z <= w+z"*)
+(*"v\<le>w ==> v+z \<le> w+z"*)
lemmas zadd_zle_mono1 = zadd_right_cancel_zle [THEN iffD2, standard]
-(*"v<=w ==> z+v <= z+w"*)
+(*"v\<le>w ==> z+v \<le> z+w"*)
lemmas zadd_zle_mono2 = zadd_left_cancel_zle [THEN iffD2, standard]
-lemma zadd_zle_mono: "[| w'<=w; z'<=z |] ==> w' + z' <= w + (z::int)"
+lemma zadd_zle_mono: "[| w'\<le>w; z'\<le>z |] ==> w' + z' \<le> w + (z::int)"
by (erule zadd_zle_mono1 [THEN zle_trans], simp)
-lemma zadd_zless_mono: "[| w'<w; z'<=z |] ==> w' + z' < w + (z::int)"
+lemma zadd_zless_mono: "[| w'<w; z'\<le>z |] ==> w' + z' < w + (z::int)"
by (erule zadd_zless_mono1 [THEN order_less_le_trans], simp)
@@ -213,7 +213,7 @@
lemma zminus_zless_zminus [simp]: "(- x < - y) = (y < (x::int))"
by (simp add: zless_def zdiff_def zadd_ac)
-lemma zminus_zle_zminus [simp]: "(- x <= - y) = (y <= (x::int))"
+lemma zminus_zle_zminus [simp]: "(- x \<le> - y) = (y \<le> (x::int))"
by (simp add: zle_def)
text{*The next several equations can make the simplifier loop!*}
@@ -224,10 +224,10 @@
lemma zminus_zless: "(- x < y) = (- y < (x::int))"
by (simp add: zless_def zdiff_def zadd_ac)
-lemma zle_zminus: "(x <= - y) = (y <= - (x::int))"
+lemma zle_zminus: "(x \<le> - y) = (y \<le> - (x::int))"
by (simp add: zle_def zminus_zless)
-lemma zminus_zle: "(- x <= y) = (- y <= (x::int))"
+lemma zminus_zle: "(- x \<le> y) = (- y \<le> (x::int))"
by (simp add: zle_def zless_zminus)
lemma equation_zminus: "(x = - y) = (y = - (x::int))"
@@ -254,16 +254,16 @@
lemma negative_zless [iff]: "- (int (Suc n)) < int m"
by (rule negative_zless_0 [THEN order_less_le_trans], simp)
-lemma negative_zle_0: "- int n <= 0"
+lemma negative_zle_0: "- int n \<le> 0"
by (simp add: zminus_zle)
-lemma negative_zle [iff]: "- int n <= int m"
+lemma negative_zle [iff]: "- int n \<le> int m"
by (simp add: zless_def zle_def zdiff_def zadd_int)
-lemma not_zle_0_negative [simp]: "~(0 <= - (int (Suc n)))"
+lemma not_zle_0_negative [simp]: "~(0 \<le> - (int (Suc n)))"
by (subst zle_zminus, simp)
-lemma int_zle_neg: "(int n <= - int m) = (n = 0 & m = 0)"
+lemma int_zle_neg: "(int n \<le> - int m) = (n = 0 & m = 0)"
apply safe
apply (drule_tac [2] zle_zminus [THEN iffD1])
apply (auto dest: zle_trans [OF _ negative_zle_0])
@@ -279,7 +279,7 @@
apply (simp_all (no_asm_simp))
done
-lemma zle_iff_zadd: "(w <= z) = (EX n. z = w + int n)"
+lemma zle_iff_zadd: "(w \<le> z) = (EX n. z = w + int n)"
by (force intro: exI [of _ "0::nat"]
intro!: not_sym [THEN not0_implies_Suc]
simp add: zless_iff_Suc_zadd int_le_less)
@@ -322,13 +322,13 @@
apply (auto dest: order_less_trans simp add: neg_eq_less_0)
done
-lemma nat_0_le [simp]: "0 <= z ==> int (nat z) = z"
+lemma nat_0_le [simp]: "0 \<le> z ==> int (nat z) = z"
by (simp add: neg_eq_less_0 zle_def not_neg_nat)
-lemma nat_le_0 [simp]: "z <= 0 ==> nat z = 0"
+lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0"
by (auto simp add: order_le_less neg_eq_less_0 zle_def neg_nat)
-(*An alternative condition is 0 <= w *)
+(*An alternative condition is 0 \<le> w *)
lemma nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)"
apply (subst zless_int [symmetric])
apply (simp (no_asm_simp) add: not_neg_nat not_neg_eq_ge_0 order_le_less)
@@ -355,34 +355,34 @@
subsection{*Monotonicity of Multiplication*}
-lemma zmult_zle_mono1_lemma: "i <= (j::int) ==> i * int k <= j * int k"
+lemma zmult_zle_mono1_lemma: "i \<le> (j::int) ==> i * int k \<le> j * int k"
apply (induct_tac "k")
apply (simp_all (no_asm_simp) add: int_Suc zadd_zmult_distrib2 zadd_zle_mono int_Suc0_eq_1)
done
-lemma zmult_zle_mono1: "[| i <= j; (0::int) <= k |] ==> i*k <= j*k"
+lemma zmult_zle_mono1: "[| i \<le> j; (0::int) \<le> k |] ==> i*k \<le> j*k"
apply (rule_tac t = k in not_neg_nat [THEN subst])
apply (erule_tac [2] zmult_zle_mono1_lemma)
apply (simp (no_asm_use) add: not_neg_eq_ge_0)
done
-lemma zmult_zle_mono1_neg: "[| i <= j; k <= (0::int) |] ==> j*k <= i*k"
+lemma zmult_zle_mono1_neg: "[| i \<le> j; k \<le> (0::int) |] ==> j*k \<le> i*k"
apply (rule zminus_zle_zminus [THEN iffD1])
apply (simp add: zmult_zminus_right [symmetric] zmult_zle_mono1 zle_zminus)
done
-lemma zmult_zle_mono2: "[| i <= j; (0::int) <= k |] ==> k*i <= k*j"
+lemma zmult_zle_mono2: "[| i \<le> j; (0::int) \<le> k |] ==> k*i \<le> k*j"
apply (drule zmult_zle_mono1)
apply (simp_all add: zmult_commute)
done
-lemma zmult_zle_mono2_neg: "[| i <= j; k <= (0::int) |] ==> k*j <= k*i"
+lemma zmult_zle_mono2_neg: "[| i \<le> j; k \<le> (0::int) |] ==> k*j \<le> k*i"
apply (drule zmult_zle_mono1_neg)
apply (simp_all add: zmult_commute)
done
-(* <= monotonicity, BOTH arguments*)
-lemma zmult_zle_mono: "[| i <= j; k <= l; (0::int) <= j; (0::int) <= k |] ==> i*k <= j*l"
+(* \<le> monotonicity, BOTH arguments*)
+lemma zmult_zle_mono: "[| i \<le> j; k \<le> l; (0::int) \<le> j; (0::int) \<le> k |] ==> i*k \<le> j*l"
apply (erule zmult_zle_mono1 [THEN order_trans], assumption)
apply (erule zmult_zle_mono2, assumption)
done
@@ -404,74 +404,70 @@
apply (frule conjI [THEN zless_nat_conj [THEN iffD2]], auto)
done
+text{*The Integers Form an Ordered Ring*}
+instance int :: ordered_ring
+proof
+ fix i j k :: int
+ show "(i + j) + k = i + (j + k)" by simp
+ show "i + j = j + i" by simp
+ show "0 + i = i" by simp
+ show "- i + i = 0" by simp
+ show "i - j = i + (-j)" by simp
+ show "(i * j) * k = i * (j * k)" by (rule zmult_assoc)
+ show "i * j = j * i" by (rule zmult_commute)
+ show "1 * i = i" by simp
+ show "(i + j) * k = i * k + j * k" by (simp add: int_distrib)
+ show "0 \<noteq> (1::int)" by simp
+ show "i \<le> j ==> k + i \<le> k + j" by simp
+ show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: zmult_zless_mono2)
+ show "\<bar>i\<bar> = (if i < 0 then -i else i)" by (simp only: zabs_def)
+qed
+
lemma zmult_zless_mono1: "[| i<j; (0::int) < k |] ==> i*k < j*k"
-apply (drule zmult_zless_mono2)
-apply (simp_all add: zmult_commute)
-done
+ by (rule Ring_and_Field.mult_strict_right_mono)
(* < monotonicity, BOTH arguments*)
-lemma zmult_zless_mono: "[| i < j; k < l; (0::int) < j; (0::int) < k |] ==> i*k < j*l"
-apply (erule zmult_zless_mono1 [THEN order_less_trans], assumption)
-apply (erule zmult_zless_mono2, assumption)
-done
+lemma zmult_zless_mono:
+ "[| i < j; k < l; (0::int) < j; (0::int) < k |] ==> i*k < j*l"
+ by (rule Ring_and_Field.mult_strict_mono)
lemma zmult_zless_mono1_neg: "[| i<j; k < (0::int) |] ==> j*k < i*k"
-apply (rule zminus_zless_zminus [THEN iffD1])
-apply (simp add: zmult_zminus_right [symmetric] zmult_zless_mono1 zless_zminus)
-done
+ by (rule Ring_and_Field.mult_strict_right_mono_neg)
lemma zmult_zless_mono2_neg: "[| i<j; k < (0::int) |] ==> k*j < k*i"
-apply (rule zminus_zless_zminus [THEN iffD1])
-apply (simp add: zmult_zminus [symmetric] zmult_zless_mono2 zless_zminus)
-done
+ by (rule Ring_and_Field.mult_strict_left_mono_neg)
lemma zmult_eq_0_iff [iff]: "(m*n = (0::int)) = (m = 0 | n = 0)"
-apply (case_tac "m < (0::int) ")
-apply (auto simp add: linorder_not_less order_le_less linorder_neq_iff)
-apply (force dest: zmult_zless_mono1_neg zmult_zless_mono1)+
+ by simp
+
+lemma zmult_zless_cancel2: "(m*k < n*k) = (((0::int) < k & m<n) | (k<0 & n<m))"
+ by (rule Ring_and_Field.mult_less_cancel_right)
+
+lemma zmult_zless_cancel1:
+ "(k*m < k*n) = (((0::int) < k & m<n) | (k < 0 & n<m))"
+ by (rule Ring_and_Field.mult_less_cancel_left)
+
+lemma zmult_zle_cancel2:
+ "(m*k \<le> n*k) = (((0::int) < k --> m\<le>n) & (k < 0 --> n\<le>m))"
+ by (rule Ring_and_Field.mult_le_cancel_right)
+
+lemma zmult_zle_cancel1:
+ "(k*m \<le> k*n) = (((0::int) < k --> m\<le>n) & (k < 0 --> n\<le>m))"
+ by (rule Ring_and_Field.mult_le_cancel_left)
+
+lemma zmult_cancel2: "(m*k = n*k) = (k = (0::int) | m=n)"
+ by (rule Ring_and_Field.mult_cancel_right)
+
+lemma zmult_cancel1 [simp]: "(k*m = k*n) = (k = (0::int) | m=n)"
+ by (rule Ring_and_Field.mult_cancel_left)
+
+(*Analogous to zadd_int*)
+lemma zdiff_int [rule_format]: "n\<le>m --> int m - int n = int (m-n)"
+apply (induct_tac m n rule: diff_induct)
+apply (auto simp add: int_Suc symmetric zdiff_def)
done
-text{*Cancellation laws for k*m < k*n and m*k < n*k, also for <= and =,
- but not (yet?) for k*m < n*k.*}
-
-lemma zmult_zless_cancel2: "(m*k < n*k) = (((0::int) < k & m<n) | (k < 0 & n<m))"
-apply (case_tac "k = (0::int) ")
-apply (auto simp add: linorder_neq_iff zmult_zless_mono1 zmult_zless_mono1_neg)
-apply (auto simp add: linorder_not_less
- linorder_not_le [symmetric, of "m*k"]
- linorder_not_le [symmetric, of m])
-apply (erule_tac [!] notE)
-apply (auto simp add: order_less_imp_le zmult_zle_mono1 zmult_zle_mono1_neg)
-done
-
-
-lemma zmult_zless_cancel1:
- "(k*m < k*n) = (((0::int) < k & m<n) | (k < 0 & n<m))"
-by (simp add: zmult_commute [of k] zmult_zless_cancel2)
-
-lemma zmult_zle_cancel2:
- "(m*k <= n*k) = (((0::int) < k --> m<=n) & (k < 0 --> n<=m))"
-by (simp add: linorder_not_less [symmetric] zmult_zless_cancel2)
-
-lemma zmult_zle_cancel1:
- "(k*m <= k*n) = (((0::int) < k --> m<=n) & (k < 0 --> n<=m))"
-by (simp add: linorder_not_less [symmetric] zmult_zless_cancel1)
-
-lemma zmult_cancel2 [simp]: "(m*k = n*k) = (k = (0::int) | m=n)"
-apply (cut_tac linorder_less_linear [of 0 k])
-apply (force dest: zmult_zless_mono1_neg zmult_zless_mono1
- simp add: linorder_neq_iff)
-done
-
-lemma zmult_cancel1 [simp]: "(k*m = k*n) = (k = (0::int) | m=n)"
-by (simp add: zmult_commute [of k] zmult_cancel2)
-
-(*Analogous to zadd_int*)
-lemma zdiff_int [rule_format (no_asm)]: "n<=m --> int m - int n = int (m-n)"
-apply (induct_tac m n rule: diff_induct)
-apply (auto simp add: int_Suc symmetric zdiff_def)
-done
ML
{*
--- a/src/HOL/Integ/IntArith.thy Fri Nov 21 11:15:40 2003 +0100
+++ b/src/HOL/Integ/IntArith.thy Mon Nov 24 15:33:07 2003 +0100
@@ -233,48 +233,34 @@
subsection{*Some convenient biconditionals for products of signs*}
lemma zmult_pos: "[| (0::int) < i; 0 < j |] ==> 0 < i*j"
-by (drule zmult_zless_mono1, auto)
+ by (rule Ring_and_Field.mult_pos)
lemma zmult_neg: "[| i < (0::int); j < 0 |] ==> 0 < i*j"
-by (drule zmult_zless_mono1_neg, auto)
+ by (rule Ring_and_Field.mult_neg)
lemma zmult_pos_neg: "[| (0::int) < i; j < 0 |] ==> i*j < 0"
-by (drule zmult_zless_mono1_neg, auto)
+ by (rule Ring_and_Field.mult_pos_neg)
lemma int_0_less_mult_iff: "((0::int) < x*y) = (0 < x & 0 < y | x < 0 & y < 0)"
-apply (auto simp add: order_le_less linorder_not_less zmult_pos zmult_neg)
-apply (rule_tac [!] ccontr)
-apply (auto simp add: order_le_less linorder_not_less)
-apply (erule_tac [!] rev_mp)
-apply (drule_tac [!] zmult_pos_neg)
-apply (auto dest: order_less_not_sym simp add: zmult_commute)
-done
+ by (rule Ring_and_Field.zero_less_mult_iff)
lemma int_0_le_mult_iff: "((0::int) \<le> x*y) = (0 \<le> x & 0 \<le> y | x \<le> 0 & y \<le> 0)"
-by (auto simp add: order_le_less linorder_not_less int_0_less_mult_iff)
+ by (rule Ring_and_Field.zero_le_mult_iff)
lemma zmult_less_0_iff: "(x*y < (0::int)) = (0 < x & y < 0 | x < 0 & 0 < y)"
-by (auto simp add: int_0_le_mult_iff linorder_not_le [symmetric])
+ by (rule Ring_and_Field.mult_less_0_iff)
lemma zmult_le_0_iff: "(x*y \<le> (0::int)) = (0 \<le> x & y \<le> 0 | x \<le> 0 & 0 \<le> y)"
-by (auto dest: order_less_not_sym simp add: int_0_less_mult_iff linorder_not_less [symmetric])
-
-lemma abs_mult: "abs (x * y) = abs x * abs (y::int)"
-by (simp del: number_of_reorient split
- add: zabs_split split add: zabs_split add: zmult_less_0_iff zle_def)
+ by (rule Ring_and_Field.mult_le_0_iff)
lemma abs_eq_0 [iff]: "(abs x = 0) = (x = (0::int))"
-by (simp split add: zabs_split)
+ by (rule Ring_and_Field.abs_eq_0)
lemma zero_less_abs_iff [iff]: "(0 < abs x) = (x ~= (0::int))"
-by (simp split add: zabs_split, arith)
+ by (rule Ring_and_Field.zero_less_abs_iff)
-(* THIS LOOKS WRONG: [intro]*)
lemma square_nonzero [simp]: "0 \<le> x * (x::int)"
-apply (subgoal_tac " (- x) * x \<le> 0")
- apply simp
-apply (simp only: zmult_le_0_iff, auto)
-done
+ by (rule Ring_and_Field.zero_le_square)
subsection{*Products and 1, by T. M. Rasmussen*}
--- a/src/HOL/IsaMakefile Fri Nov 21 11:15:40 2003 +0100
+++ b/src/HOL/IsaMakefile Mon Nov 24 15:33:07 2003 +0100
@@ -200,7 +200,7 @@
Library/FuncSet.thy Library/Library.thy \
Library/List_Prefix.thy Library/Multiset.thy Library/NatPair.thy \
Library/Permutation.thy Library/Primes.thy Library/Quotient.thy \
- Library/Ring_and_Field_Example.thy Library/Nat_Infinity.thy \
+ Library/Nat_Infinity.thy \
Library/README.html Library/Continuity.thy \
Library/Nested_Environment.thy Library/Rational_Numbers.thy \
Library/Zorn.thy\
--- a/src/HOL/Library/Library.thy Fri Nov 21 11:15:40 2003 +0100
+++ b/src/HOL/Library/Library.thy Mon Nov 24 15:33:07 2003 +0100
@@ -1,7 +1,6 @@
(*<*)
theory Library =
Quotient +
- Ring_and_Field + Ring_and_Field_Example +
Nat_Infinity +
Rational_Numbers +
List_Prefix +
--- a/src/HOL/Library/Ring_and_Field_Example.thy Fri Nov 21 11:15:40 2003 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,25 +0,0 @@
-
-header {* \title{}\subsection{Example: The ordered ring of integers} *}
-
-theory Ring_and_Field_Example = Main:
-
-text{*The Integers Form an Ordered Ring*}
-instance int :: ordered_ring
-proof
- fix i j k :: int
- show "(i + j) + k = i + (j + k)" by simp
- show "i + j = j + i" by simp
- show "0 + i = i" by simp
- show "- i + i = 0" by simp
- show "i - j = i + (-j)" by simp
- show "(i * j) * k = i * (j * k)" by simp
- show "i * j = j * i" by simp
- show "1 * i = i" by simp
- show "(i + j) * k = i * k + j * k" by (simp add: int_distrib)
- show "0 \<noteq> (1::int)" by simp
- show "i \<le> j ==> k + i \<le> k + j" by simp
- show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: zmult_zless_mono2)
- show "\<bar>i\<bar> = (if i < 0 then -i else i)" by (simp only: zabs_def)
-qed
-
-end
--- a/src/HOL/Nat.thy Fri Nov 21 11:15:40 2003 +0100
+++ b/src/HOL/Nat.thy Mon Nov 24 15:33:07 2003 +0100
@@ -992,7 +992,9 @@
lemma mult_less_mono1: "(i::nat) < j ==> 0 < k ==> i * k < j * k"
by (drule mult_less_mono2) (simp_all add: mult_commute)
-lemma zero_less_mult_iff [simp]: "(0 < (m::nat) * n) = (0 < m & 0 < n)"
+text{*Differs from the standard @{text zero_less_mult_iff} in that
+ there are no negative numbers.*}
+lemma nat_0_less_mult_iff [simp]: "(0 < (m::nat) * n) = (0 < m & 0 < n)"
apply (induct m)
apply (case_tac [2] n, simp_all)
done
--- a/src/HOL/Real/RealOrd.thy Fri Nov 21 11:15:40 2003 +0100
+++ b/src/HOL/Real/RealOrd.thy Mon Nov 24 15:33:07 2003 +0100
@@ -27,7 +27,6 @@
-
subsection{* The Simproc @{text abel_cancel}*}
(*Deletion of other terms in the formula, seeking the -x at the front of z*)
@@ -40,8 +39,8 @@
everything gets cancelled on the right.*)
lemma real_add_cancel_end: "((x::real) + (y + z) = y) = (x = -z)"
apply (subst real_add_left_commute)
-apply (rule_tac t = "y" in real_add_zero_right [THEN subst] , subst real_add_left_cancel)
-apply (simp (no_asm) add: real_eq_diff_eq [symmetric])
+apply (rule_tac t = y in real_add_zero_right [THEN subst], subst real_add_left_cancel)
+apply (simp add: real_eq_diff_eq [symmetric])
done
@@ -87,38 +86,32 @@
Addsimprocs [Real_Cancel.sum_conv, Real_Cancel.rel_conv];
*}
-lemma real_minus_diff_eq: "- (z - y) = y - (z::real)"
-apply (simp (no_asm))
-done
-declare real_minus_diff_eq [simp]
+lemma real_minus_diff_eq [simp]: "- (z - y) = y - (z::real)"
+by simp
subsection{*Theorems About the Ordering*}
lemma real_gt_zero_preal_Ex: "(0 < x) = (\<exists>y. x = real_of_preal y)"
apply (auto simp add: real_of_preal_zero_less)
-apply (cut_tac x = "x" in real_of_preal_trichotomy)
+apply (cut_tac x = x in real_of_preal_trichotomy)
apply (blast elim!: real_less_irrefl real_of_preal_not_minus_gt_zero [THEN notE])
done
lemma real_gt_preal_preal_Ex: "real_of_preal z < x ==> \<exists>y. x = real_of_preal y"
-apply (blast dest!: real_of_preal_zero_less [THEN real_less_trans]
+by (blast dest!: real_of_preal_zero_less [THEN real_less_trans]
intro: real_gt_zero_preal_Ex [THEN iffD1])
-done
lemma real_ge_preal_preal_Ex: "real_of_preal z \<le> x ==> \<exists>y. x = real_of_preal y"
-apply (blast dest: order_le_imp_less_or_eq real_gt_preal_preal_Ex)
-done
+by (blast dest: order_le_imp_less_or_eq real_gt_preal_preal_Ex)
lemma real_less_all_preal: "y \<le> 0 ==> \<forall>x. y < real_of_preal x"
-apply (auto elim: order_le_imp_less_or_eq [THEN disjE]
+by (auto elim: order_le_imp_less_or_eq [THEN disjE]
intro: real_of_preal_zero_less [THEN [2] real_less_trans]
simp add: real_of_preal_zero_less)
-done
lemma real_less_all_real2: "~ 0 < y ==> \<forall>x. y < real_of_preal x"
-apply (blast intro!: real_less_all_preal real_leI)
-done
+by (blast intro!: real_less_all_preal real_leI)
lemma real_lemma_add_positive_imp_less: "[| R + L = S; (0::real) < L |] ==> R < S"
apply (rule real_less_sum_gt_0_iff [THEN iffD1])
@@ -126,17 +119,15 @@
done
lemma real_ex_add_positive_left_less: "\<exists>T::real. 0 < T & R + T = S ==> R < S"
-apply (blast intro: real_lemma_add_positive_imp_less)
-done
+by (blast intro: real_lemma_add_positive_imp_less)
(*Alternative definition for real_less. NOT for rewriting*)
lemma real_less_iff_add: "(R < S) = (\<exists>T::real. 0 < T & R + T = S)"
-apply (blast intro!: real_less_add_positive_left_Ex real_ex_add_positive_left_less)
-done
+by (blast intro!: real_less_add_positive_left_Ex real_ex_add_positive_left_less)
lemma real_of_preal_le_iff: "(real_of_preal m1 \<le> real_of_preal m2) = (m1 \<le> m2)"
apply (auto intro!: preal_leI simp add: real_less_le_iff [symmetric])
-apply (drule order_le_less_trans , assumption)
+apply (drule order_le_less_trans, assumption)
apply (erule preal_less_irrefl)
done
@@ -148,45 +139,33 @@
lemma neg_real_mult_order: "[| x < 0; y < 0 |] ==> (0::real) < x * y"
apply (drule real_minus_zero_less_iff [THEN iffD2])+
-apply (drule real_mult_order , assumption)
-apply simp
+apply (drule real_mult_order, assumption, simp)
done
lemma real_mult_less_0: "[| 0 < x; y < 0 |] ==> x*y < (0::real)"
apply (drule real_minus_zero_less_iff [THEN iffD2])
-apply (drule real_mult_order , assumption)
-apply (rule real_minus_zero_less_iff [THEN iffD1])
-apply simp
+apply (drule real_mult_order, assumption)
+apply (rule real_minus_zero_less_iff [THEN iffD1], simp)
done
lemma real_zero_less_one: "0 < (1::real)"
-apply (unfold real_one_def)
-apply (auto intro: real_gt_zero_preal_Ex [THEN iffD2]
- simp add: real_of_preal_def)
-done
+by (auto intro: real_gt_zero_preal_Ex [THEN iffD2]
+ simp add: real_one_def real_of_preal_def)
subsection{*Monotonicity of Addition*}
-lemma real_add_right_cancel_less: "(v+z < w+z) = (v < (w::real))"
-apply (simp (no_asm))
-done
+lemma real_add_right_cancel_less [simp]: "(v+z < w+z) = (v < (w::real))"
+by simp
-lemma real_add_left_cancel_less: "(z+v < z+w) = (v < (w::real))"
-apply (simp (no_asm))
-done
-
-declare real_add_right_cancel_less [simp] real_add_left_cancel_less [simp]
+lemma real_add_left_cancel_less [simp]: "(z+v < z+w) = (v < (w::real))"
+by simp
-lemma real_add_right_cancel_le: "(v+z \<le> w+z) = (v \<le> (w::real))"
-apply (simp (no_asm))
-done
+lemma real_add_right_cancel_le [simp]: "(v+z \<le> w+z) = (v \<le> (w::real))"
+by simp
-lemma real_add_left_cancel_le: "(z+v \<le> z+w) = (v \<le> (w::real))"
-apply (simp (no_asm))
-done
-
-declare real_add_right_cancel_le [simp] real_add_left_cancel_le [simp]
+lemma real_add_left_cancel_le [simp]: "(z+v \<le> z+w) = (v \<le> (w::real))"
+by simp
(*"v\<le>w ==> v+z \<le> w+z"*)
lemmas real_add_less_mono1 = real_add_right_cancel_less [THEN iffD2, standard]
@@ -195,18 +174,13 @@
lemmas real_add_le_mono1 = real_add_right_cancel_le [THEN iffD2, standard]
lemma real_add_less_le_mono: "!!z z'::real. [| w'<w; z'\<le>z |] ==> w' + z' < w + z"
-apply (erule real_add_less_mono1 [THEN order_less_le_trans])
-apply (simp (no_asm))
-done
+by (erule real_add_less_mono1 [THEN order_less_le_trans], simp)
lemma real_add_le_less_mono: "!!z z'::real. [| w'\<le>w; z'<z |] ==> w' + z' < w + z"
-apply (erule real_add_le_mono1 [THEN order_le_less_trans])
-apply (simp (no_asm))
-done
+by (erule real_add_le_mono1 [THEN order_le_less_trans], simp)
lemma real_add_less_mono2: "!!(A::real). A < B ==> C + A < C + B"
-apply (simp (no_asm))
-done
+by simp
lemma real_less_add_right_cancel: "!!(A::real). A + C < B + C ==> A < B"
apply (simp (no_asm_use))
@@ -242,13 +216,11 @@
done
lemma real_add_left_le_mono1: "!!(q1::real). q1 \<le> q2 ==> x + q1 \<le> x + q2"
-apply (simp (no_asm))
-done
+by simp
lemma real_add_le_mono: "[|i\<le>j; k\<le>l |] ==> i + k \<le> j + (l::real)"
apply (drule real_add_le_mono1)
-apply (erule order_trans)
-apply (simp (no_asm))
+apply (erule order_trans, simp)
done
lemma real_less_Ex: "\<exists>(x::real). x < y"
@@ -258,33 +230,29 @@
done
lemma real_add_minus_positive_less_self: "(0::real) < r ==> u + (-r) < u"
-apply (rule_tac C = "r" in real_less_add_right_cancel)
-apply (simp (no_asm) add: real_add_assoc)
+apply (rule_tac C = r in real_less_add_right_cancel)
+apply (simp add: real_add_assoc)
done
-lemma real_le_minus_iff: "(-s \<le> -r) = ((r::real) \<le> s)"
-apply (rule sym)
-apply safe
+lemma real_le_minus_iff [simp]: "(-s \<le> -r) = ((r::real) \<le> s)"
+apply (rule sym, safe)
apply (drule_tac x = "-s" in real_add_left_le_mono1)
-apply (drule_tac [2] x = "r" in real_add_left_le_mono1)
-apply auto
+apply (drule_tac [2] x = r in real_add_left_le_mono1, auto)
apply (drule_tac z = "-r" in real_add_le_mono1)
-apply (drule_tac [2] z = "s" in real_add_le_mono1)
+apply (drule_tac [2] z = s in real_add_le_mono1)
apply (auto simp add: real_add_assoc)
done
-declare real_le_minus_iff [simp]
-lemma real_le_square: "(0::real) \<le> x*x"
+lemma real_le_square [simp]: "(0::real) \<le> x*x"
apply (rule_tac real_linear_less2 [of x 0])
apply (auto intro: real_mult_order neg_real_mult_order order_less_imp_le)
done
-declare real_le_square [simp]
lemma real_mult_less_mono1: "[| (0::real) < z; x < y |] ==> x*z < y*z"
apply (rotate_tac 1)
apply (drule real_less_sum_gt_zero)
apply (rule real_sum_gt_zero_less)
-apply (drule real_mult_order , assumption)
+apply (drule real_mult_order, assumption)
apply (simp add: real_add_mult_distrib2 real_mult_commute)
done
@@ -314,7 +282,7 @@
show "x < y ==> 0 < z ==> z * x < z * y" by (simp add: real_mult_less_mono2)
show "\<bar>x\<bar> = (if x < 0 then -x else x)"
by (auto dest: order_le_less_trans simp add: real_abs_def linorder_not_le)
- show "x \<noteq> 0 ==> inverse x * x = 1" by simp;
+ show "x \<noteq> 0 ==> inverse x * x = 1" by simp
show "y \<noteq> 0 ==> x / y = x * inverse y" by (simp add: real_divide_def)
qed
@@ -325,17 +293,14 @@
----------------------------------------------------------------------------*)
lemma real_of_posnat_one: "real_of_posnat 0 = (1::real)"
-
-apply (unfold real_of_posnat_def)
-apply (simp (no_asm) add: pnat_one_iff [symmetric] real_of_preal_def symmetric real_one_def)
-done
+by (simp add: real_of_posnat_def pnat_one_iff [symmetric]
+ real_of_preal_def symmetric real_one_def)
lemma real_of_posnat_two: "real_of_posnat (Suc 0) = (1::real) + (1::real)"
-apply (simp add: real_of_posnat_def real_of_preal_def real_one_def pnat_two_eq
+by (simp add: real_of_posnat_def real_of_preal_def real_one_def pnat_two_eq
real_add
prat_of_pnat_add [symmetric] preal_of_prat_add [symmetric]
pnat_add_ac)
-done
lemma real_of_posnat_add:
"real_of_posnat n1 + real_of_posnat n2 = real_of_posnat (n1 + n2) + (1::real)"
@@ -350,9 +315,7 @@
done
lemma real_of_posnat_Suc: "real_of_posnat (Suc n) = real_of_posnat n + (1::real)"
-apply (subst real_of_posnat_add_one [symmetric])
-apply (simp (no_asm))
-done
+by (subst real_of_posnat_add_one [symmetric], simp)
lemma inj_real_of_posnat: "inj(real_of_posnat)"
apply (rule inj_onI)
@@ -363,41 +326,28 @@
apply (erule inj_pnat_of_nat [THEN injD])
done
-lemma real_of_nat_zero: "real (0::nat) = 0"
-apply (unfold real_of_nat_def)
-apply (simp (no_asm) add: real_of_posnat_one)
-done
+lemma real_of_nat_zero [simp]: "real (0::nat) = 0"
+by (simp add: real_of_nat_def real_of_posnat_one)
-lemma real_of_nat_one: "real (Suc 0) = (1::real)"
-apply (unfold real_of_nat_def)
-apply (simp (no_asm) add: real_of_posnat_two real_add_assoc)
-done
-declare real_of_nat_zero [simp] real_of_nat_one [simp]
+lemma real_of_nat_one [simp]: "real (Suc 0) = (1::real)"
+by (simp add: real_of_nat_def real_of_posnat_two real_add_assoc)
-lemma real_of_nat_add:
+lemma real_of_nat_add [simp]:
"real (m + n) = real (m::nat) + real n"
apply (simp add: real_of_nat_def real_add_assoc)
apply (simp add: real_of_posnat_add real_add_assoc [symmetric])
done
-declare real_of_nat_add [simp]
(*Not for addsimps: often the LHS is used to represent a positive natural*)
lemma real_of_nat_Suc: "real (Suc n) = real n + (1::real)"
-apply (unfold real_of_nat_def)
-apply (simp (no_asm) add: real_of_posnat_Suc real_add_ac)
-done
+by (simp add: real_of_nat_def real_of_posnat_Suc real_add_ac)
-lemma real_of_nat_less_iff:
+lemma real_of_nat_less_iff [iff]:
"(real (n::nat) < real m) = (n < m)"
-apply (unfold real_of_nat_def real_of_posnat_def)
-apply auto
-done
-declare real_of_nat_less_iff [iff]
+by (auto simp add: real_of_nat_def real_of_posnat_def)
-lemma real_of_nat_le_iff: "(real (n::nat) \<le> real m) = (n \<le> m)"
-apply (simp (no_asm) add: linorder_not_less [symmetric])
-done
-declare real_of_nat_le_iff [iff]
+lemma real_of_nat_le_iff [iff]: "(real (n::nat) \<le> real m) = (n \<le> m)"
+by (simp add: linorder_not_less [symmetric])
lemma inj_real_of_nat: "inj (real :: nat => real)"
apply (rule inj_onI)
@@ -405,27 +355,24 @@
simp add: real_of_nat_def real_add_right_cancel)
done
-lemma real_of_nat_ge_zero: "0 \<le> real (n::nat)"
+lemma real_of_nat_ge_zero [iff]: "0 \<le> real (n::nat)"
apply (induct_tac "n")
apply (auto simp add: real_of_nat_Suc)
apply (drule real_add_le_less_mono)
apply (rule real_zero_less_one)
apply (simp add: order_less_imp_le)
done
-declare real_of_nat_ge_zero [iff]
-lemma real_of_nat_mult: "real (m * n) = real (m::nat) * real n"
+lemma real_of_nat_mult [simp]: "real (m * n) = real (m::nat) * real n"
apply (induct_tac "m")
apply (auto simp add: real_of_nat_Suc real_add_mult_distrib real_add_commute)
done
-declare real_of_nat_mult [simp]
-lemma real_of_nat_inject: "(real (n::nat) = real m) = (n = m)"
-apply (auto dest: inj_real_of_nat [THEN injD])
-done
-declare real_of_nat_inject [iff]
+lemma real_of_nat_inject [iff]: "(real (n::nat) = real m) = (n = m)"
+by (auto dest: inj_real_of_nat [THEN injD])
-lemma real_of_nat_diff [rule_format (no_asm)]: "n \<le> m --> real (m - n) = real (m::nat) - real n"
+lemma real_of_nat_diff [rule_format]:
+ "n \<le> m --> real (m - n) = real (m::nat) - real n"
apply (induct_tac "m")
apply (auto simp add: real_diff_def Suc_diff_le le_Suc_eq real_of_nat_Suc real_of_nat_zero real_add_ac)
done
@@ -439,10 +386,9 @@
show "n = 0 \<Longrightarrow> real n = 0" by simp
qed
-lemma real_of_nat_neg_int: "neg z ==> real (nat z) = 0"
+lemma real_of_nat_neg_int [simp]: "neg z ==> real (nat z) = 0"
apply (simp (no_asm_simp) add: neg_nat real_of_nat_zero)
done
-declare real_of_nat_neg_int [simp]
(*----------------------------------------------------------------------------
@@ -455,8 +401,7 @@
apply (frule real_minus_zero_less_iff2 [THEN iffD2])
apply (frule real_not_refl2 [THEN not_sym])
apply (drule real_not_refl2 [THEN not_sym, THEN real_inverse_not_zero])
-apply (drule order_le_imp_less_or_eq)
-apply safe;
+apply (drule order_le_imp_less_or_eq, safe)
apply (drule neg_real_mult_order, assumption)
apply (auto intro: real_zero_less_one [THEN real_less_asym])
done
@@ -470,38 +415,26 @@
done
lemma real_mult_less_cancel1: "[| (0::real) < z; x * z < y * z |] ==> x < y"
-apply (frule_tac x = "x*z" in real_inverse_gt_0 [THEN real_mult_less_mono1])
-apply (auto simp add: real_mult_assoc real_not_refl2 [THEN not_sym])
-done
+by (force simp add: Ring_and_Field.mult_less_cancel_right
+ elim: order_less_asym)
lemma real_mult_less_cancel2: "[| (0::real) < z; z*x < z*y |] ==> x < y"
apply (erule real_mult_less_cancel1)
apply (simp add: real_mult_commute)
done
-lemma real_mult_less_iff1: "(0::real) < z ==> (x*z < y*z) = (x < y)"
-apply (blast intro: real_mult_less_mono1 real_mult_less_cancel1)
-done
+lemma real_mult_less_iff1 [simp]: "(0::real) < z ==> (x*z < y*z) = (x < y)"
+by (blast intro: real_mult_less_mono1 real_mult_less_cancel1)
-lemma real_mult_less_iff2: "(0::real) < z ==> (z*x < z*y) = (x < y)"
-apply (blast intro: real_mult_less_mono2 real_mult_less_cancel2)
-done
-
-declare real_mult_less_iff1 [simp] real_mult_less_iff2 [simp]
+lemma real_mult_less_iff2 [simp]: "(0::real) < z ==> (z*x < z*y) = (x < y)"
+by (blast intro: real_mult_less_mono2 real_mult_less_cancel2)
(* 05/00 *)
-lemma real_mult_le_cancel_iff1: "(0::real) < z ==> (x*z \<le> y*z) = (x \<le> y)"
-apply (unfold real_le_def)
-apply auto
-done
+lemma real_mult_le_cancel_iff1 [simp]: "(0::real) < z ==> (x*z \<le> y*z) = (x \<le> y)"
+by (auto simp add: real_le_def)
-lemma real_mult_le_cancel_iff2: "(0::real) < z ==> (z*x \<le> z*y) = (x \<le> y)"
-apply (unfold real_le_def)
-apply auto
-done
-
-declare real_mult_le_cancel_iff1 [simp] real_mult_le_cancel_iff2 [simp]
-
+lemma real_mult_le_cancel_iff2 [simp]: "(0::real) < z ==> (z*x \<le> z*y) = (x \<le> y)"
+by (auto simp add: real_le_def)
lemma real_mult_le_less_mono1: "[| (0::real) \<le> z; x < y |] ==> x*z \<le> y*z"
apply (rule real_less_or_eq_imp_le)
@@ -510,29 +443,22 @@
done
lemma real_mult_less_mono: "[| u<v; x<y; (0::real) < v; 0 < x |] ==> u*x < v* y"
-apply (erule real_mult_less_mono1 [THEN order_less_trans])
-apply assumption
-apply (erule real_mult_less_mono2)
-apply assumption
-done
+ by (rule Ring_and_Field.mult_strict_mono)
-(*Variant of the theorem above; sometimes it's stronger*)
-lemma real_mult_less_mono': "[| x < y; r1 < r2; (0::real) \<le> r1; 0 \<le> x|] ==> r1 * x < r2 * y"
+text{*Variant of the theorem above; sometimes it's stronger*}
+lemma real_mult_less_mono':
+ "[| x < y; r1 < r2; (0::real) \<le> r1; 0 \<le> x|] ==> r1 * x < r2 * y"
apply (subgoal_tac "0<r2")
-prefer 2 apply (blast intro: order_le_less_trans)
+ prefer 2 apply (blast intro: order_le_less_trans)
apply (case_tac "x=0")
-apply (auto dest!: order_le_imp_less_or_eq intro: real_mult_less_mono real_mult_order)
-done
-
-lemma real_gt_zero: "(1::real) \<le> x ==> 0 < x"
-apply (rule ccontr , drule real_leI)
-apply (drule order_trans , assumption)
-apply (auto dest: real_zero_less_one [THEN [2] order_le_less_trans])
+apply (auto dest!: order_le_imp_less_or_eq
+ intro: real_mult_less_mono real_mult_order)
done
lemma real_mult_self_le: "[| (1::real) < r; (1::real) \<le> x |] ==> x \<le> r * x"
-apply (drule real_gt_zero [THEN order_less_imp_le])
-apply (auto dest!: real_mult_le_less_mono1)
+apply (subgoal_tac "0\<le>x")
+apply (force dest!: real_mult_le_less_mono1)
+apply (force intro: order_trans [OF zero_less_one [THEN order_less_imp_le]])
done
lemma real_mult_self_le2: "[| (1::real) \<le> r; (1::real) \<le> x |] ==> x \<le> r * x"
@@ -541,11 +467,10 @@
done
lemma real_inverse_less_swap: "[| 0 < r; r < x |] ==> inverse x < inverse (r::real)"
-apply (frule order_less_trans , assumption)
+apply (frule order_less_trans, assumption)
apply (frule real_inverse_gt_0)
-apply (frule_tac x = "x" in real_inverse_gt_0)
-apply (frule_tac x = "r" and z = "inverse r" in real_mult_less_mono1)
-apply assumption
+apply (frule_tac x = x in real_inverse_gt_0)
+apply (frule_tac x = r and z = "inverse r" in real_mult_less_mono1, assumption)
apply (simp add: real_not_refl2 [THEN not_sym, THEN real_mult_inv_right])
apply (frule real_inverse_gt_0)
apply (frule_tac x = " (1::real) " and z = "inverse x" in real_mult_less_mono2)
@@ -553,10 +478,8 @@
apply (simp add: real_not_refl2 [THEN not_sym, THEN real_mult_inv_left] real_mult_assoc [symmetric])
done
-lemma real_mult_is_0: "(x*y = 0) = (x = 0 | y = (0::real))"
-apply auto
-done
-declare real_mult_is_0 [iff]
+lemma real_mult_is_0 [iff]: "(x*y = 0) = (x = 0 | y = (0::real))"
+by auto
lemma real_inverse_add: "[| x \<noteq> 0; y \<noteq> 0 |]
==> inverse x + inverse y = (x + y) * inverse (x * (y::real))"
@@ -567,25 +490,20 @@
done
(* 05/00 *)
-lemma real_minus_zero_le_iff: "(0 \<le> -R) = (R \<le> (0::real))"
-apply (auto dest: sym simp add: real_le_less)
-done
+lemma real_minus_zero_le_iff [simp]: "(0 \<le> -R) = (R \<le> (0::real))"
+by (auto dest: sym simp add: real_le_less)
-lemma real_minus_zero_le_iff2: "(-R \<le> 0) = ((0::real) \<le> R)"
-apply (auto simp add: real_minus_zero_less_iff2 real_le_less)
-done
-
-declare real_minus_zero_le_iff [simp] real_minus_zero_le_iff2 [simp]
+lemma real_minus_zero_le_iff2 [simp]: "(-R \<le> 0) = ((0::real) \<le> R)"
+by (auto simp add: real_minus_zero_less_iff2 real_le_less)
lemma real_sum_squares_cancel: "x * x + y * y = 0 ==> x = (0::real)"
apply (drule real_add_minus_eq_minus)
-apply (cut_tac x = "x" in real_le_square)
-apply (auto , drule real_le_anti_sym)
-apply auto
+apply (cut_tac x = x in real_le_square)
+apply (auto, drule real_le_anti_sym, auto)
done
lemma real_sum_squares_cancel2: "x * x + y * y = 0 ==> y = (0::real)"
-apply (rule_tac y = "x" in real_sum_squares_cancel)
+apply (rule_tac y = x in real_sum_squares_cancel)
apply (simp add: real_add_commute)
done
@@ -678,7 +596,6 @@
val real_mult_le_less_mono1 = thm "real_mult_le_less_mono1";
val real_mult_less_mono = thm "real_mult_less_mono";
val real_mult_less_mono' = thm "real_mult_less_mono'";
-val real_gt_zero = thm "real_gt_zero";
val real_mult_self_le = thm "real_mult_self_le";
val real_mult_self_le2 = thm "real_mult_self_le2";
val real_inverse_less_swap = thm "real_inverse_less_swap";
--- a/src/HOL/Ring_and_Field.thy Fri Nov 21 11:15:40 2003 +0100
+++ b/src/HOL/Ring_and_Field.thy Mon Nov 24 15:33:07 2003 +0100
@@ -89,10 +89,10 @@
assume eq: "a + b = a + c"
then have "(-a + a) + b = (-a + a) + c"
by (simp only: eq add_assoc)
- then show "b = c" by simp
+ thus "b = c" by simp
next
assume eq: "b = c"
- then show "a + b = a + c" by simp
+ thus "a + b = a + c" by simp
qed
lemma add_right_cancel [simp]:
@@ -118,12 +118,10 @@
assume "- a = - b"
then have "- (- a) = - (- b)"
by simp
- then show "a=b"
- by simp
+ thus "a=b" by simp
next
assume "a=b"
- then show "-a = -b"
- by simp
+ thus "-a = -b" by simp
qed
lemma neg_equal_0_iff_equal [simp]: "(-a = 0) = (a = (0::'a::ring))"
@@ -175,7 +173,7 @@
proof -
have "0*a + 0*a = 0*a + 0"
by (simp add: left_distrib [symmetric])
- then show ?thesis by (simp only: add_left_cancel)
+ thus ?thesis by (simp only: add_left_cancel)
qed
lemma mult_right_zero [simp]: "a * 0 = (0::'a::ring)"
@@ -228,7 +226,7 @@
by simp
then have "0 + (-b) \<le> (-a + b) + (-b)"
by (rule add_right_mono)
- then show ?thesis
+ thus ?thesis
by (simp add: add_assoc)
qed
@@ -237,12 +235,10 @@
assume "- b \<le> - a"
then have "- (- a) \<le> - (- b)"
by (rule le_imp_neg_le)
- then show "a\<le>b"
- by simp
+ thus "a\<le>b" by simp
next
assume "a\<le>b"
- then show "-b \<le> -a"
- by (rule le_imp_neg_le)
+ thus "-b \<le> -a" by (rule le_imp_neg_le)
qed
lemma neg_le_0_iff_le [simp]: "(-a \<le> 0) = (0 \<le> (a::'a::ordered_ring))"
@@ -292,6 +288,55 @@
"[|b \<le> a; c < 0|] ==> a * c \<le> b * (c::'a::ordered_ring)"
by (force simp add: mult_strict_right_mono_neg order_le_less)
+text{*Strict monotonicity in both arguments*}
+lemma mult_strict_mono:
+ "[|a<b; c<d; 0<b; 0<c|] ==> a * c < b * (d::'a::ordered_semiring)"
+apply (erule mult_strict_right_mono [THEN order_less_trans], assumption)
+apply (erule mult_strict_left_mono, assumption)
+done
+
+subsection{*Cancellation Laws for Relationships With a Common Factor*}
+
+text{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"},
+ also with the relations @{text "\<le>"} and equality.*}
+
+lemma mult_less_cancel_right:
+ "(a*c < b*c) = ((0 < c & a < b) | (c < 0 & b < (a::'a::ordered_ring)))"
+apply (case_tac "c = 0")
+apply (auto simp add: linorder_neq_iff mult_strict_right_mono
+ mult_strict_right_mono_neg)
+apply (auto simp add: linorder_not_less
+ linorder_not_le [symmetric, of "a*c"]
+ linorder_not_le [symmetric, of a])
+apply (erule_tac [!] notE)
+apply (auto simp add: order_less_imp_le mult_right_mono
+ mult_right_mono_neg)
+done
+
+lemma mult_less_cancel_left:
+ "(c*a < c*b) = ((0 < c & a < b) | (c < 0 & b < (a::'a::ordered_ring)))"
+by (simp add: mult_commute [of c] mult_less_cancel_right)
+
+lemma mult_le_cancel_right:
+ "(a*c \<le> b*c) = ((0<c --> a\<le>b) & (c<0 --> b \<le> (a::'a::ordered_ring)))"
+by (simp add: linorder_not_less [symmetric] mult_less_cancel_right)
+
+lemma mult_le_cancel_left:
+ "(c*a \<le> c*b) = ((0<c --> a\<le>b) & (c<0 --> b \<le> (a::'a::ordered_ring)))"
+by (simp add: mult_commute [of c] mult_le_cancel_right)
+
+text{*Cancellation of equalities with a common factor*}
+lemma mult_cancel_right [simp]:
+ "(a*c = b*c) = (c = (0::'a::ordered_ring) | a=b)"
+apply (cut_tac linorder_less_linear [of 0 c])
+apply (force dest: mult_strict_right_mono_neg mult_strict_right_mono
+ simp add: linorder_neq_iff)
+done
+
+lemma mult_cancel_left [simp]:
+ "(c*a = c*b) = (c = (0::'a::ordered_ring) | a=b)"
+by (simp add: mult_commute [of c] mult_cancel_right)
+
subsection{* Products of Signs *}
@@ -319,8 +364,7 @@
apply (blast dest: zero_less_mult_pos)
done
-
-lemma mult_eq_0_iff [iff]: "(a*b = (0::'a::ordered_ring)) = (a = 0 | b = 0)"
+lemma mult_eq_0_iff [simp]: "(a*b = (0::'a::ordered_ring)) = (a = 0 | b = 0)"
apply (case_tac "a < 0")
apply (auto simp add: linorder_not_less order_le_less linorder_neq_iff)
apply (force dest: mult_strict_right_mono_neg mult_strict_right_mono)+
@@ -369,10 +413,10 @@
minus_mult_left [symmetric] minus_mult_right [symmetric])
done
-lemma abs_eq_0 [iff]: "(abs x = 0) = (x = (0::'a::ordered_ring))"
+lemma abs_eq_0 [simp]: "(abs x = 0) = (x = (0::'a::ordered_ring))"
by (simp add: abs_if)
-lemma zero_less_abs_iff [iff]: "(0 < abs x) = (x ~= (0::'a::ordered_ring))"
+lemma zero_less_abs_iff [simp]: "(0 < abs x) = (x ~= (0::'a::ordered_ring))"
by (simp add: abs_if linorder_neq_iff)