# HG changeset patch # User paulson # Date 1069684387 -3600 # Node ID 08b34c902618a16f49167dec08461c22304eb31b # Parent 95b42e69436c0446128ed6f727f1cc964644dae7 conversion of integers to use Ring_and_Field; new lemmas for Ring_and_Field diff -r 95b42e69436c -r 08b34c902618 src/HOL/Hyperreal/Poly.ML --- 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); diff -r 95b42e69436c -r 08b34c902618 src/HOL/Hyperreal/Transcendental.ML --- 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"; diff -r 95b42e69436c -r 08b34c902618 src/HOL/Integ/Bin.ML --- 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; diff -r 95b42e69436c -r 08b34c902618 src/HOL/Integ/Int.thy --- 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 \ 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\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) = (w z) = (w w+z) = (v \ (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 \ z+w) = (v \ (w::int))" by simp -(*"v<=w ==> v+z <= w+z"*) +(*"v\w ==> v+z \ w+z"*) lemmas zadd_zless_mono1 = zadd_right_cancel_zless [THEN iffD2, standard] -(*"v<=w ==> z+v <= z+w"*) +(*"v\w ==> z+v \ z+w"*) lemmas zadd_zless_mono2 = zadd_left_cancel_zless [THEN iffD2, standard] -(*"v<=w ==> v+z <= w+z"*) +(*"v\w ==> v+z \ w+z"*) lemmas zadd_zle_mono1 = zadd_right_cancel_zle [THEN iffD2, standard] -(*"v<=w ==> z+v <= z+w"*) +(*"v\w ==> z+v \ 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'\w; z'\z |] ==> w' + z' \ w + (z::int)" by (erule zadd_zle_mono1 [THEN zle_trans], simp) -lemma zadd_zless_mono: "[| w' w' + z' < w + (z::int)" +lemma zadd_zless_mono: "[| w'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 \ - y) = (y \ (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 \ - y) = (y \ - (x::int))" by (simp add: zle_def zminus_zless) -lemma zminus_zle: "(- x <= y) = (- y <= (x::int))" +lemma zminus_zle: "(- x \ y) = (- y \ (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 \ 0" by (simp add: zminus_zle) -lemma negative_zle [iff]: "- int n <= int m" +lemma negative_zle [iff]: "- int n \ 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 \ - (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 \ - 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 \ 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 \ 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 \ 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 \ 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 \ (j::int) ==> i * int k \ 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 \ j; (0::int) \ k |] ==> i*k \ 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 \ j; k \ (0::int) |] ==> j*k \ 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 \ j; (0::int) \ k |] ==> k*i \ 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 \ j; k \ (0::int) |] ==> k*j \ 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" +(* \ monotonicity, BOTH arguments*) +lemma zmult_zle_mono: "[| i \ j; k \ l; (0::int) \ j; (0::int) \ k |] ==> i*k \ 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 \ (1::int)" by simp + show "i \ j ==> k + i \ k + j" by simp + show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: zmult_zless_mono2) + show "\i\ = (if i < 0 then -i else i)" by (simp only: zabs_def) +qed + lemma zmult_zless_mono1: "[| i 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 < 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 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::int) < k --> m\n) & (k < 0 --> n\m))" + by (rule Ring_and_Field.mult_le_cancel_right) + +lemma zmult_zle_cancel1: + "(k*m \ k*n) = (((0::int) < k --> m\n) & (k < 0 --> n\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\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 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 {* diff -r 95b42e69436c -r 08b34c902618 src/HOL/Integ/IntArith.thy --- 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) \ x*y) = (0 \ x & 0 \ y | x \ 0 & y \ 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 \ (0::int)) = (0 \ x & y \ 0 | x \ 0 & 0 \ 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 \ x * (x::int)" -apply (subgoal_tac " (- x) * x \ 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*} diff -r 95b42e69436c -r 08b34c902618 src/HOL/IsaMakefile --- 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\ diff -r 95b42e69436c -r 08b34c902618 src/HOL/Library/Library.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 + diff -r 95b42e69436c -r 08b34c902618 src/HOL/Library/Ring_and_Field_Example.thy --- 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 \ (1::int)" by simp - show "i \ j ==> k + i \ k + j" by simp - show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: zmult_zless_mono2) - show "\i\ = (if i < 0 then -i else i)" by (simp only: zabs_def) -qed - -end diff -r 95b42e69436c -r 08b34c902618 src/HOL/Nat.thy --- 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 diff -r 95b42e69436c -r 08b34c902618 src/HOL/Real/RealOrd.thy --- 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) = (\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 ==> \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 \ x ==> \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 \ 0 ==> \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 ==> \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: "\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) = (\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 \ real_of_preal m2) = (m1 \ 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 \ w+z) = (v \ (w::real))" -apply (simp (no_asm)) -done +lemma real_add_right_cancel_le [simp]: "(v+z \ w+z) = (v \ (w::real))" +by simp -lemma real_add_left_cancel_le: "(z+v \ z+w) = (v \ (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 \ z+w) = (v \ (w::real))" +by simp (*"v\w ==> v+z \ 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'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'\w; 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 \ q2 ==> x + q1 \ x + q2" -apply (simp (no_asm)) -done +by simp lemma real_add_le_mono: "[|i\j; k\l |] ==> i + k \ 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: "\(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 \ -r) = ((r::real) \ s)" -apply (rule sym) -apply safe +lemma real_le_minus_iff [simp]: "(-s \ -r) = ((r::real) \ 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) \ x*x" +lemma real_le_square [simp]: "(0::real) \ 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 "\x\ = (if x < 0 then -x else x)" by (auto dest: order_le_less_trans simp add: real_abs_def linorder_not_le) - show "x \ 0 ==> inverse x * x = 1" by simp; + show "x \ 0 ==> inverse x * x = 1" by simp show "y \ 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) \ real m) = (n \ 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) \ real m) = (n \ 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 \ real (n::nat)" +lemma real_of_nat_ge_zero [iff]: "0 \ 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 \ m --> real (m - n) = real (m::nat) - real n" +lemma real_of_nat_diff [rule_format]: + "n \ 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 \ 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 \ y*z) = (x \ y)" -apply (unfold real_le_def) -apply auto -done +lemma real_mult_le_cancel_iff1 [simp]: "(0::real) < z ==> (x*z \ y*z) = (x \ y)" +by (auto simp add: real_le_def) -lemma real_mult_le_cancel_iff2: "(0::real) < z ==> (z*x \ z*y) = (x \ 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 \ z*y) = (x \ y)" +by (auto simp add: real_le_def) lemma real_mult_le_less_mono1: "[| (0::real) \ z; x < y |] ==> x*z \ y*z" apply (rule real_less_or_eq_imp_le) @@ -510,29 +443,22 @@ done lemma real_mult_less_mono: "[| u 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) \ r1; 0 \ 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) \ r1; 0 \ x|] ==> r1 * x < r2 * y" apply (subgoal_tac "0 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) \ x |] ==> x \ r * x" -apply (drule real_gt_zero [THEN order_less_imp_le]) -apply (auto dest!: real_mult_le_less_mono1) +apply (subgoal_tac "0\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) \ r; (1::real) \ x |] ==> x \ 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 \ 0; y \ 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 \ -R) = (R \ (0::real))" -apply (auto dest: sym simp add: real_le_less) -done +lemma real_minus_zero_le_iff [simp]: "(0 \ -R) = (R \ (0::real))" +by (auto dest: sym simp add: real_le_less) -lemma real_minus_zero_le_iff2: "(-R \ 0) = ((0::real) \ 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 \ 0) = ((0::real) \ 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"; diff -r 95b42e69436c -r 08b34c902618 src/HOL/Ring_and_Field.thy --- 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) \ (-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 \ - a" then have "- (- a) \ - (- b)" by (rule le_imp_neg_le) - then show "a\b" - by simp + thus "a\b" by simp next assume "a\b" - then show "-b \ -a" - by (rule le_imp_neg_le) + thus "-b \ -a" by (rule le_imp_neg_le) qed lemma neg_le_0_iff_le [simp]: "(-a \ 0) = (0 \ (a::'a::ordered_ring))" @@ -292,6 +288,55 @@ "[|b \ a; c < 0|] ==> a * c \ 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 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 "\"} 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 \ b*c) = ((0 a\b) & (c<0 --> b \ (a::'a::ordered_ring)))" +by (simp add: linorder_not_less [symmetric] mult_less_cancel_right) + +lemma mult_le_cancel_left: + "(c*a \ c*b) = ((0 a\b) & (c<0 --> b \ (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)