# HG changeset patch # User nipkow # Date 1233156556 -3600 # Node ID 53103fc8ffa3d1cab9620b2794f6d1c8f1e5c45a # Parent 7187373c6cb1ff412cc01fd91a2af86a88950e71 Replaced group_ and ring_simps by algebra_simps; removed compare_rls - use algebra_simps now diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/Algebra/abstract/Ring2.thy --- a/src/HOL/Algebra/abstract/Ring2.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/Algebra/abstract/Ring2.thy Wed Jan 28 16:29:16 2009 +0100 @@ -224,10 +224,6 @@ {* Method.no_args (Method.SIMPLE_METHOD' (full_simp_tac ring_ss)) *} {* computes distributive normal form in rings *} -lemmas ring_simps = - l_zero r_zero l_neg r_neg minus_minus minus0 - l_one r_one l_null r_null l_minus r_minus - subsection {* Rings and the summation operator *} diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/Algebra/poly/UnivPoly2.thy --- a/src/HOL/Algebra/poly/UnivPoly2.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/Algebra/poly/UnivPoly2.thy Wed Jan 28 16:29:16 2009 +0100 @@ -189,7 +189,7 @@ lemma coeff_smult [simp]: "coeff (a *s p) n = (a::'a::ring) * coeff p n" proof - have "!!f. f : UP ==> (%n. a * f n) : UP" - by (unfold UP_def) (force simp add: ring_simps) + by (unfold UP_def) (force simp add: algebra_simps) *) (* this force step is slow *) (* then show ?thesis apply (simp add: coeff_def smult_def Abs_UP_inverse Rep_UP) @@ -198,7 +198,7 @@ lemma coeff_smult [simp]: "coeff (a *s p) n = (a::'a::ring) * coeff p n" proof - have "Rep_UP p : UP ==> (%n. a * Rep_UP p n) : UP" - by (unfold UP_def) (force simp add: ring_simps) + by (unfold UP_def) (force simp add: algebra_simps) (* this force step is slow *) then show ?thesis by (simp add: coeff_def smult_def Abs_UP_inverse Rep_UP) @@ -220,7 +220,7 @@ fix i assume "max n m < i" with boundn and boundm show "f i + g i = 0" - by (fastsimp simp add: ring_simps) + by (fastsimp simp add: algebra_simps) qed then show "(%i. (f i + g i)) : UP" by (unfold UP_def) fast @@ -251,15 +251,15 @@ have "f i * g (k-i) = 0" proof cases assume "n < i" - with `bound n f` show ?thesis by (auto simp add: ring_simps) + with `bound n f` show ?thesis by (auto simp add: algebra_simps) next assume "~ (n < i)" with bound have "m < k-i" by arith - with `bound m g` show ?thesis by (auto simp add: ring_simps) + with `bound m g` show ?thesis by (auto simp add: algebra_simps) qed } then show "setsum (%i. f i * g (k-i)) {..k} = 0" - by (simp add: ring_simps) + by (simp add: algebra_simps) qed then show "(%n. setsum (%i. f i * g (n-i)) {..n}) : UP" by (unfold UP_def) fast @@ -270,7 +270,7 @@ qed lemma coeff_uminus [simp]: "coeff (-p) n = (-coeff p n::'a::ring)" -by (unfold up_uminus_def) (simp add: ring_simps) +by (unfold up_uminus_def) (simp add: algebra_simps) (* Other lemmas *) @@ -388,7 +388,7 @@ proof (cases k) case 0 then show ?thesis by simp ring next - case Suc then show ?thesis by (simp add: ring_simps) ring + case Suc then show ?thesis by (simp add: algebra_simps) ring qed then show "coeff (monom a 0 * p) k = coeff (a *s p) k" by ring qed diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/Complex.thy --- a/src/HOL/Complex.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/Complex.thy Wed Jan 28 16:29:16 2009 +0100 @@ -237,9 +237,9 @@ show "scaleR 1 x = x" by (simp add: expand_complex_eq) show "scaleR a x * y = scaleR a (x * y)" - by (simp add: expand_complex_eq ring_simps) + by (simp add: expand_complex_eq algebra_simps) show "x * scaleR a y = scaleR a (x * y)" - by (simp add: expand_complex_eq ring_simps) + by (simp add: expand_complex_eq algebra_simps) qed end @@ -312,7 +312,7 @@ (simp add: power_mult_distrib right_distrib [symmetric] real_sqrt_mult) show "norm (x * y) = norm x * norm y" by (induct x, induct y) - (simp add: real_sqrt_mult [symmetric] power2_eq_square ring_simps) + (simp add: real_sqrt_mult [symmetric] power2_eq_square algebra_simps) show "sgn x = x /\<^sub>R cmod x" by(simp add: complex_sgn_def) qed diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/Dense_Linear_Order.thy --- a/src/HOL/Dense_Linear_Order.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/Dense_Linear_Order.thy Wed Jan 28 16:29:16 2009 +0100 @@ -552,7 +552,7 @@ lemma neg_prod_lt:"(c\'a\ordered_field) < 0 \ ((c*x < 0) == (x > 0))" proof- assume H: "c < 0" - have "c*x < 0 = (0/c < x)" by (simp only: neg_divide_less_eq[OF H] ring_simps) + have "c*x < 0 = (0/c < x)" by (simp only: neg_divide_less_eq[OF H] algebra_simps) also have "\ = (0 < x)" by simp finally show "(c*x < 0) == (x > 0)" by simp qed @@ -560,7 +560,7 @@ lemma pos_prod_lt:"(c\'a\ordered_field) > 0 \ ((c*x < 0) == (x < 0))" proof- assume H: "c > 0" - hence "c*x < 0 = (0/c > x)" by (simp only: pos_less_divide_eq[OF H] ring_simps) + hence "c*x < 0 = (0/c > x)" by (simp only: pos_less_divide_eq[OF H] algebra_simps) also have "\ = (0 > x)" by simp finally show "(c*x < 0) == (x < 0)" by simp qed @@ -569,7 +569,7 @@ proof- assume H: "c < 0" have "c*x + t< 0 = (c*x < -t)" by (subst less_iff_diff_less_0 [of "c*x" "-t"], simp) - also have "\ = (-t/c < x)" by (simp only: neg_divide_less_eq[OF H] ring_simps) + also have "\ = (-t/c < x)" by (simp only: neg_divide_less_eq[OF H] algebra_simps) also have "\ = ((- 1/c)*t < x)" by simp finally show "(c*x + t < 0) == (x > (- 1/c)*t)" by simp qed @@ -578,7 +578,7 @@ proof- assume H: "c > 0" have "c*x + t< 0 = (c*x < -t)" by (subst less_iff_diff_less_0 [of "c*x" "-t"], simp) - also have "\ = (-t/c > x)" by (simp only: pos_less_divide_eq[OF H] ring_simps) + also have "\ = (-t/c > x)" by (simp only: pos_less_divide_eq[OF H] algebra_simps) also have "\ = ((- 1/c)*t > x)" by simp finally show "(c*x + t < 0) == (x < (- 1/c)*t)" by simp qed @@ -589,7 +589,7 @@ lemma neg_prod_le:"(c\'a\ordered_field) < 0 \ ((c*x <= 0) == (x >= 0))" proof- assume H: "c < 0" - have "c*x <= 0 = (0/c <= x)" by (simp only: neg_divide_le_eq[OF H] ring_simps) + have "c*x <= 0 = (0/c <= x)" by (simp only: neg_divide_le_eq[OF H] algebra_simps) also have "\ = (0 <= x)" by simp finally show "(c*x <= 0) == (x >= 0)" by simp qed @@ -597,7 +597,7 @@ lemma pos_prod_le:"(c\'a\ordered_field) > 0 \ ((c*x <= 0) == (x <= 0))" proof- assume H: "c > 0" - hence "c*x <= 0 = (0/c >= x)" by (simp only: pos_le_divide_eq[OF H] ring_simps) + hence "c*x <= 0 = (0/c >= x)" by (simp only: pos_le_divide_eq[OF H] algebra_simps) also have "\ = (0 >= x)" by simp finally show "(c*x <= 0) == (x <= 0)" by simp qed @@ -606,7 +606,7 @@ proof- assume H: "c < 0" have "c*x + t <= 0 = (c*x <= -t)" by (subst le_iff_diff_le_0 [of "c*x" "-t"], simp) - also have "\ = (-t/c <= x)" by (simp only: neg_divide_le_eq[OF H] ring_simps) + also have "\ = (-t/c <= x)" by (simp only: neg_divide_le_eq[OF H] algebra_simps) also have "\ = ((- 1/c)*t <= x)" by simp finally show "(c*x + t <= 0) == (x >= (- 1/c)*t)" by simp qed @@ -615,7 +615,7 @@ proof- assume H: "c > 0" have "c*x + t <= 0 = (c*x <= -t)" by (subst le_iff_diff_le_0 [of "c*x" "-t"], simp) - also have "\ = (-t/c >= x)" by (simp only: pos_le_divide_eq[OF H] ring_simps) + also have "\ = (-t/c >= x)" by (simp only: pos_le_divide_eq[OF H] algebra_simps) also have "\ = ((- 1/c)*t >= x)" by simp finally show "(c*x + t <= 0) == (x <= (- 1/c)*t)" by simp qed @@ -628,7 +628,7 @@ proof- assume H: "c \ 0" have "c*x + t = 0 = (c*x = -t)" by (subst eq_iff_diff_eq_0 [of "c*x" "-t"], simp) - also have "\ = (x = -t/c)" by (simp only: nonzero_eq_divide_eq[OF H] ring_simps) + also have "\ = (x = -t/c)" by (simp only: nonzero_eq_divide_eq[OF H] algebra_simps) finally show "(c*x + t = 0) == (x = (- 1/c)*t)" by simp qed lemma sum_eq:"((x::'a::pordered_ab_group_add) + t = 0) == (x = - t)" diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/Deriv.thy --- a/src/HOL/Deriv.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/Deriv.thy Wed Jan 28 16:29:16 2009 +0100 @@ -141,7 +141,7 @@ lemma inverse_diff_inverse: "\(a::'a::division_ring) \ 0; b \ 0\ \ inverse a - inverse b = - (inverse a * (a - b) * inverse b)" -by (simp add: ring_simps) +by (simp add: algebra_simps) lemma DERIV_inverse_lemma: "\a \ 0; b \ (0::'a::real_normed_field)\ @@ -206,7 +206,7 @@ case (Suc k) from DERIV_mult' [OF f Suc] show ?case apply (simp only: of_nat_Suc ring_distribs mult_1_left) - apply (simp only: power_Suc right_distrib mult_ac add_ac) + apply (simp only: power_Suc algebra_simps) done qed @@ -724,7 +724,7 @@ from isCont_bounded [OF le this] obtain k where k: "!!x. a \ x & x \ b --> inverse (M - f x) \ k" by auto have Minv: "!!x. a \ x & x \ b --> 0 < inverse (M - f (x))" - by (simp add: M3 compare_rls) + by (simp add: M3 algebra_simps) have "!!x. a \ x & x \ b --> inverse (M - f x) < k+1" using k by (auto intro: order_le_less_trans [of _ k]) with Minv @@ -1398,7 +1398,7 @@ have "?h b - ?h a = ((f b)*(g b) - (f a)*(g b) - (g b)*(f b) + (g a)*(f b)) - ((f b)*(g a) - (f a)*(g a) - (g b)*(f a) + (g a)*(f a))" - by (simp add: mult_ac add_ac right_diff_distrib) + by (simp add: algebra_simps) hence "?h b - ?h a = 0" by auto } ultimately have "(b - a) * (g'c * (f b - f a) - f'c * (g b - g a)) = 0" by auto @@ -1427,7 +1427,7 @@ lemma coeff_pderiv: "coeff (pderiv p) n = of_nat (Suc n) * coeff p (Suc n)" apply (induct p arbitrary: n, simp) - apply (simp add: pderiv_pCons coeff_pCons ring_simps split: nat.split) + apply (simp add: pderiv_pCons coeff_pCons algebra_simps split: nat.split) done lemma pderiv_eq_0_iff: "pderiv p = 0 \ degree p = 0" @@ -1451,21 +1451,21 @@ by (simp add: pderiv_pCons) lemma pderiv_add: "pderiv (p + q) = pderiv p + pderiv q" -by (rule poly_ext, simp add: coeff_pderiv ring_simps) +by (rule poly_ext, simp add: coeff_pderiv algebra_simps) lemma pderiv_minus: "pderiv (- p) = - pderiv p" by (rule poly_ext, simp add: coeff_pderiv) lemma pderiv_diff: "pderiv (p - q) = pderiv p - pderiv q" -by (rule poly_ext, simp add: coeff_pderiv ring_simps) +by (rule poly_ext, simp add: coeff_pderiv algebra_simps) lemma pderiv_smult: "pderiv (smult a p) = smult a (pderiv p)" -by (rule poly_ext, simp add: coeff_pderiv ring_simps) +by (rule poly_ext, simp add: coeff_pderiv algebra_simps) lemma pderiv_mult: "pderiv (p * q) = p * pderiv q + q * pderiv p" apply (induct p) apply simp -apply (simp add: pderiv_add pderiv_smult pderiv_pCons ring_simps) +apply (simp add: pderiv_add pderiv_smult pderiv_pCons algebra_simps) done lemma pderiv_power_Suc: @@ -1475,7 +1475,7 @@ apply (subst power_Suc) apply (subst pderiv_mult) apply (erule ssubst) -apply (simp add: smult_add_left ring_simps) +apply (simp add: smult_add_left algebra_simps) done lemma DERIV_cmult2: "DERIV f x :> D ==> DERIV (%x. (f x) * c :: real) x :> D * c" diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/Divides.thy Wed Jan 28 16:29:16 2009 +0100 @@ -38,10 +38,10 @@ by (simp only: add_ac) lemma div_mod_equality: "((a div b) * b + a mod b) + c = a + c" - by (simp add: mod_div_equality) +by (simp add: mod_div_equality) lemma div_mod_equality2: "(b * (a div b) + a mod b) + c = a + c" - by (simp add: mod_div_equality2) +by (simp add: mod_div_equality2) lemma mod_by_0 [simp]: "a mod 0 = a" using mod_div_equality [of a zero] by simp @@ -63,7 +63,7 @@ by (simp add: mod_div_equality) also from False div_mult_self1 [of b a c] have "\ = (c + a div b) * b + (a + c * b) mod b" - by (simp add: left_distrib add_ac) + by (simp add: algebra_simps) finally have "a = a div b * b + (a + c * b) mod b" by (simp add: add_commute [of a] add_assoc left_distrib) then have "a div b * b + (a + c * b) mod b = a div b * b + a mod b" @@ -72,7 +72,7 @@ qed lemma mod_mult_self2 [simp]: "(a + b * c) mod b = a mod b" - by (simp add: mult_commute [of b]) +by (simp add: mult_commute [of b]) lemma div_mult_self1_is_id [simp]: "b \ 0 \ b * a div b = a" using div_mult_self2 [of b 0 a] by simp @@ -217,7 +217,7 @@ have "(a * b) mod c = ((a div c * c + a mod c) * b) mod c" by (simp only: mod_div_equality) also have "\ = (a mod c * b + a div c * b * c) mod c" - by (simp only: left_distrib right_distrib add_ac mult_ac) + by (simp only: algebra_simps) also have "\ = (a mod c * b) mod c" by (rule mod_mult_self1) finally show ?thesis . @@ -228,7 +228,7 @@ have "(a * b) mod c = (a * (b div c * c + b mod c)) mod c" by (simp only: mod_div_equality) also have "\ = (a * (b mod c) + a * (b div c) * c) mod c" - by (simp only: left_distrib right_distrib add_ac mult_ac) + by (simp only: algebra_simps) also have "\ = (a * (b mod c)) mod c" by (rule mod_mult_self1) finally show ?thesis . @@ -552,7 +552,7 @@ lemma divmod_if [code]: "divmod m n = (if n = 0 \ m < n then (0, m) else let (q, r) = divmod (m - n) n in (Suc q, r))" - by (simp add: divmod_zero divmod_base divmod_step) +by (simp add: divmod_zero divmod_base divmod_step) (simp add: divmod_div_mod) code_modulename SML @@ -568,16 +568,16 @@ subsubsection {* Quotient *} lemma div_geq: "0 < n \ \ m < n \ m div n = Suc ((m - n) div n)" - by (simp add: le_div_geq linorder_not_less) +by (simp add: le_div_geq linorder_not_less) lemma div_if: "0 < n \ m div n = (if m < n then 0 else Suc ((m - n) div n))" - by (simp add: div_geq) +by (simp add: div_geq) lemma div_mult_self_is_m [simp]: "0 (m*n) div n = (m::nat)" - by simp +by simp lemma div_mult_self1_is_m [simp]: "0 (n*m) div n = (m::nat)" - by simp +by simp subsubsection {* Remainder *} @@ -597,13 +597,13 @@ qed lemma mod_geq: "\ m < (n\nat) \ m mod n = (m - n) mod n" - by (simp add: le_mod_geq linorder_not_less) +by (simp add: le_mod_geq linorder_not_less) lemma mod_if: "m mod (n\nat) = (if m < n then m else (m - n) mod n)" - by (simp add: le_mod_geq) +by (simp add: le_mod_geq) lemma mod_1 [simp]: "m mod Suc 0 = 0" - by (induct m) (simp_all add: mod_geq) +by (induct m) (simp_all add: mod_geq) lemma mod_mult_distrib: "(m mod n) * (k\nat) = (m * k) mod (n * k)" apply (cases "n = 0", simp) @@ -614,11 +614,11 @@ done lemma mod_mult_distrib2: "(k::nat) * (m mod n) = (k*m) mod (k*n)" - by (simp add: mult_commute [of k] mod_mult_distrib) +by (simp add: mult_commute [of k] mod_mult_distrib) (* a simple rearrangement of mod_div_equality: *) lemma mult_div_cancel: "(n::nat) * (m div n) = m - (m mod n)" - by (cut_tac a = m and b = n in mod_div_equality2, arith) +by (cut_tac a = m and b = n in mod_div_equality2, arith) lemma mod_le_divisor[simp]: "0 < n \ m mod n \ (n::nat)" apply (drule mod_less_divisor [where m = m]) @@ -630,7 +630,7 @@ lemma divmod_rel_mult1_eq: "[| divmod_rel b c q r; c > 0 |] ==> divmod_rel (a*b) c (a*q + a*r div c) (a*r mod c)" -by (auto simp add: split_ifs mult_ac divmod_rel_def add_mult_distrib2) +by (auto simp add: split_ifs divmod_rel_def algebra_simps) lemma div_mult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::nat)" apply (cases "c = 0", simp) @@ -638,19 +638,19 @@ done lemma mod_mult1_eq: "(a*b) mod c = a*(b mod c) mod (c::nat)" - by (rule mod_mult_right_eq) +by (rule mod_mult_right_eq) lemma mod_mult1_eq': "(a*b) mod (c::nat) = ((a mod c) * b) mod c" - by (rule mod_mult_left_eq) +by (rule mod_mult_left_eq) lemma mod_mult_distrib_mod: "(a*b) mod (c::nat) = ((a mod c) * (b mod c)) mod c" - by (rule mod_mult_eq) +by (rule mod_mult_eq) lemma divmod_rel_add1_eq: "[| divmod_rel a c aq ar; divmod_rel b c bq br; c > 0 |] ==> divmod_rel (a + b) c (aq + bq + (ar+br) div c) ((ar + br) mod c)" -by (auto simp add: split_ifs mult_ac divmod_rel_def add_mult_distrib2) +by (auto simp add: split_ifs divmod_rel_def algebra_simps) (*NOT suitable for rewriting: the RHS has an instance of the LHS*) lemma div_add1_eq: @@ -660,7 +660,7 @@ done lemma mod_add1_eq: "(a+b) mod (c::nat) = (a mod c + b mod c) mod c" - by (rule mod_add_eq) +by (rule mod_add_eq) lemma mod_lemma: "[| (0::nat) < c; r < b |] ==> b * (q mod c) + r < b * c" apply (cut_tac m = q and n = c in mod_less_divisor) @@ -671,7 +671,7 @@ lemma divmod_rel_mult2_eq: "[| divmod_rel a b q r; 0 < b; 0 < c |] ==> divmod_rel a (b*c) (q div c) (b*(q mod c) + r)" - by (auto simp add: mult_ac divmod_rel_def add_mult_distrib2 [symmetric] mod_lemma) +by (auto simp add: mult_ac divmod_rel_def add_mult_distrib2 [symmetric] mod_lemma) lemma div_mult2_eq: "a div (b*c) = (a div b) div (c::nat)" apply (cases "b = 0", simp) @@ -690,7 +690,7 @@ lemma div_mult_mult_lemma: "[| (0::nat) < b; 0 < c |] ==> (c*a) div (c*b) = a div b" - by (auto simp add: div_mult2_eq) +by (auto simp add: div_mult2_eq) lemma div_mult_mult1 [simp]: "(0::nat) < c ==> (c*a) div (c*b) = a div b" apply (cases "b = 0") @@ -706,7 +706,7 @@ subsubsection{*Further Facts about Quotient and Remainder*} lemma div_1 [simp]: "m div Suc 0 = m" - by (induct m) (simp_all add: div_geq) +by (induct m) (simp_all add: div_geq) (* Monotonicity of div in first argument *) @@ -780,10 +780,10 @@ done lemma nat_mod_div_trivial: "m mod n div n = (0 :: nat)" - by simp +by simp lemma nat_mod_mod_trivial: "m mod n mod n = (m mod n :: nat)" - by simp +by simp subsubsection {* The Divides Relation *} @@ -792,7 +792,7 @@ unfolding dvd_def by simp lemma dvd_1_iff_1 [simp]: "(m dvd Suc 0) = (m = Suc 0)" - by (simp add: dvd_def) +by (simp add: dvd_def) lemma dvd_anti_sym: "[| m dvd n; n dvd m |] ==> m = (n::nat)" unfolding dvd_def @@ -813,7 +813,7 @@ done lemma dvd_diffD1: "[| k dvd m-n; k dvd m; n\m |] ==> k dvd (n::nat)" - by (drule_tac m = m in dvd_diff, auto) +by (drule_tac m = m in dvd_diff, auto) lemma dvd_reduce: "(k dvd n + k) = (k dvd (n::nat))" apply (rule iffI) @@ -839,7 +839,7 @@ done lemma dvd_mod_iff: "k dvd n ==> ((k::nat) dvd m mod n) = (k dvd m)" - by (blast intro: dvd_mod_imp_dvd dvd_mod) +by (blast intro: dvd_mod_imp_dvd dvd_mod) lemma dvd_mult_cancel: "!!k::nat. [| k*m dvd k*n; 0 m dvd n" unfolding dvd_def @@ -894,7 +894,7 @@ done lemma mod_eq_0_iff: "(m mod d = 0) = (\q::nat. m = d*q)" - by (auto simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def) +by (auto simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def) lemmas mod_eq_0D [dest!] = mod_eq_0_iff [THEN iffD1] diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/Finite_Set.thy Wed Jan 28 16:29:16 2009 +0100 @@ -1033,12 +1033,12 @@ lemma setsum_Un_nat: "finite A ==> finite B ==> (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)" -- {* For the natural numbers, we have subtraction. *} -by (subst setsum_Un_Int [symmetric], auto simp add: ring_simps) +by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps) lemma setsum_Un: "finite A ==> finite B ==> (setsum f (A Un B) :: 'a :: ab_group_add) = setsum f A + setsum f B - setsum f (A Int B)" -by (subst setsum_Un_Int [symmetric], auto simp add: ring_simps) +by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps) lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) = (if a:A then setsum f A - f a else setsum f A)" @@ -1711,7 +1711,7 @@ lemma setsum_constant [simp]: "(\x \ A. y) = of_nat(card A) * y" apply (cases "finite A") apply (erule finite_induct) -apply (auto simp add: ring_simps) +apply (auto simp add: algebra_simps) done lemma setprod_constant: "finite A ==> (\x\ A. (y::'a::{recpower, comm_monoid_mult})) = y^(card A)" @@ -2220,16 +2220,16 @@ thus ?case proof assume "a = x" thus ?thesis using insert - by (simp add: mult_ac_idem) + by (simp add: mult_ac) next assume "a \ F" hence bel: "fold1 inf F \ a" by (rule insert) have "inf (fold1 inf (insert x F)) a = inf x (inf (fold1 inf F) a)" - using insert by (simp add: mult_ac_idem) + using insert by (simp add: mult_ac) also have "inf (fold1 inf F) a = fold1 inf F" using bel by (auto intro: antisym) also have "inf x \ = fold1 inf (insert x F)" - using insert by (simp add: mult_ac_idem) + using insert by (simp add: mult_ac) finally have aux: "inf (fold1 inf (insert x F)) a = fold1 inf (insert x F)" . moreover have "inf (fold1 inf (insert x F)) a \ a" by simp ultimately show ?thesis by simp diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/Fundamental_Theorem_Algebra.thy --- a/src/HOL/Fundamental_Theorem_Algebra.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/Fundamental_Theorem_Algebra.thy Wed Jan 28 16:29:16 2009 +0100 @@ -45,7 +45,7 @@ have th2: "2 *(y * sqrt ((sqrt (x * x + y * y) - x) * (sqrt (x * x + y * y) + x) / 4)) / \y\ = y" using iffD2[OF real_sqrt_pow2_iff sum_power2_ge_zero[of x y]] y0 unfolding power2_eq_square - by (simp add: ring_simps real_sqrt_divide sqrt4) + by (simp add: algebra_simps real_sqrt_divide sqrt4) from y0 xy have ?thesis apply (simp add: csqrt_def power2_eq_square) apply (simp add: real_sqrt_sum_squares_mult_ge_zero[of x y] real_sqrt_pow2[OF th(1)[of x y], unfolded power2_eq_square] real_sqrt_pow2[OF th(2)[of x y], unfolded power2_eq_square] real_sqrt_mult[symmetric]) using th1 th2 ..} @@ -109,7 +109,7 @@ lemma poly_offset_poly: "poly (offset_poly p h) x = poly p (h + x)" apply (induct p) apply (simp add: offset_poly_0) -apply (simp add: offset_poly_pCons ring_simps) +apply (simp add: offset_poly_pCons algebra_simps) done lemma offset_poly_eq_0_lemma: "smult c p + pCons a p = 0 \ p = 0" @@ -350,7 +350,7 @@ from md z have xy: "x^2 + y^2 = 1" by (simp add: cmod_def) {assume C: "cmod (z + 1) \ 1" "cmod (z - 1) \ 1" "cmod (z + ii) \ 1" "cmod (z - ii) \ 1" from C z xy have "2*x \ 1" "2*x \ -1" "2*y \ 1" "2*y \ -1" - by (simp_all add: cmod_def power2_eq_square ring_simps) + by (simp_all add: cmod_def power2_eq_square algebra_simps) hence "abs (2*x) \ 1" "abs (2*y) \ 1" by simp_all hence "(abs (2 * x))^2 <= 1^2" "(abs (2 * y)) ^2 <= 1^2" by - (rule power_mono, simp, simp)+ @@ -391,9 +391,9 @@ 1" apply (simp add: power2_eq_square norm_mult[symmetric] norm_inverse[symmetric]) using right_inverse[OF b'] - by (simp add: power2_eq_square[symmetric] power_inverse[symmetric] ring_simps) + by (simp add: power2_eq_square[symmetric] power_inverse[symmetric] algebra_simps) have th0: "cmod (complex_of_real (cmod b) / b) = 1" - apply (simp add: complex_Re_mult cmod_def power2_eq_square Re_complex_of_real Im_complex_of_real divide_inverse ring_simps ) + apply (simp add: complex_Re_mult cmod_def power2_eq_square Re_complex_of_real Im_complex_of_real divide_inverse algebra_simps ) by (simp add: real_sqrt_mult[symmetric] th0) from o have "\m. n = Suc (2*m)" by presburger+ then obtain m where m: "n = Suc (2*m)" by blast @@ -667,10 +667,10 @@ from h have z1: "cmod z \ 1" by arith from order_trans[OF th0 mult_right_mono[OF z1 norm_ge_zero[of "poly (pCons c cs) z"]]] have th1: "d \ cmod(z * poly (pCons c cs) z) - cmod a" - unfolding norm_mult by (simp add: ring_simps) + unfolding norm_mult by (simp add: algebra_simps) from complex_mod_triangle_sub[of "z * poly (pCons c cs) z" a] have th2: "cmod(z * poly (pCons c cs) z) - cmod a \ cmod (poly (pCons a (pCons c cs)) z)" - by (simp add: diff_le_eq ring_simps) + by (simp add: diff_le_eq algebra_simps) from th1 th2 have "d \ cmod (poly (pCons a (pCons c cs)) z)" by arith} hence ?case by blast} moreover @@ -685,7 +685,7 @@ have ath: "\mzh mazh ma. mzh <= mazh + ma ==> abs(d) + ma <= mzh ==> d <= mazh" by arith from complex_mod_triangle_sub[of "z*c" a ] have th1: "cmod (z * c) \ cmod (a + z * c) + cmod a" - by (simp add: ring_simps) + by (simp add: algebra_simps) from ath[OF th1 th0] have "d \ cmod (poly (pCons a (pCons c cs)) z)" using cs0' by simp} then have ?case by blast} @@ -850,7 +850,7 @@ with kas(3) lgqr[symmetric] q(1) n[symmetric] have s0:"s=0" by auto {fix w have "cmod (poly ?r w) = cmod (1 + a * w ^ k)" - using kas(4)[rule_format, of w] s0 r01 by (simp add: ring_simps)} + using kas(4)[rule_format, of w] s0 r01 by (simp add: algebra_simps)} note hth = this [symmetric] from reduce_poly_simple[OF kas(1,2)] have "\w. cmod (poly ?r w) < 1" unfolding hth by blast} @@ -866,7 +866,7 @@ from H[rule_format, OF k1n th01 th02] obtain w where w: "1 + w^k * a = 0" unfolding poly_pCons poly_monom - using kas(2) by (cases k, auto simp add: ring_simps) + using kas(2) by (cases k, auto simp add: algebra_simps) from poly_bound_exists[of "cmod w" s] obtain m where m: "m > 0" "\z. cmod z \ cmod w \ cmod (poly s z) \ m" by blast have w0: "w\0" using kas(2) w by (auto simp add: power_0_left) @@ -879,7 +879,7 @@ t: "t > 0" "t < 1" "t < inverse (cmod w ^ (k + 1) * m)" by blast let ?ct = "complex_of_real t" let ?w = "?ct * w" - have "1 + ?w^k * (a + ?w * poly s ?w) = 1 + ?ct^k * (w^k * a) + ?w^k * ?w * poly s ?w" using kas(1) by (simp add: ring_simps power_mult_distrib) + have "1 + ?w^k * (a + ?w * poly s ?w) = 1 + ?ct^k * (w^k * a) + ?w^k * ?w * poly s ?w" using kas(1) by (simp add: algebra_simps power_mult_distrib) also have "\ = complex_of_real (1 - t^k) + ?w^k * ?w * poly s ?w" unfolding wm1 by (simp) finally have "cmod (1 + ?w^k * (a + ?w * poly s ?w)) = cmod (complex_of_real (1 - t^k) + ?w^k * ?w * poly s ?w)" @@ -898,7 +898,7 @@ have th30: "t^k * (t* (cmod w ^ (k + 1) * m)) < t^k * 1" apply - apply (rule mult_strict_left_mono) by simp_all have "cmod (?w^k * ?w * poly s ?w) = t^k * (t* (cmod w ^ (k+1) * cmod (poly s ?w)))" using w0 t(1) - by (simp add: ring_simps power_mult_distrib norm_of_real norm_power norm_mult) + by (simp add: algebra_simps power_mult_distrib norm_of_real norm_power norm_mult) then have "cmod (?w^k * ?w * poly s ?w) \ t^k * (t* (cmod w ^ (k + 1) * m))" using t(1,2) m(2)[rule_format, OF tw] w0 apply (simp only: ) @@ -1308,14 +1308,14 @@ {assume l: ?lhs then obtain u where u: "q = p * u" .. have "r = p * (smult a u - t)" - using u qrp' [symmetric] t by (simp add: ring_simps mult_smult_right) + using u qrp' [symmetric] t by (simp add: algebra_simps mult_smult_right) then have ?rhs ..} moreover {assume r: ?rhs then obtain u where u: "r = p * u" .. from u [symmetric] t qrp' [symmetric] a0 have "q = p * smult (1/a) (u + t)" - by (simp add: ring_simps mult_smult_right smult_smult) + by (simp add: algebra_simps mult_smult_right smult_smult) hence ?lhs ..} ultimately have "?lhs = ?rhs" by blast } thus "?lhs \ ?rhs" by - (atomize(full), blast) diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/Groebner_Basis.thy --- a/src/HOL/Groebner_Basis.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/Groebner_Basis.thy Wed Jan 28 16:29:16 2009 +0100 @@ -165,7 +165,7 @@ interpretation class_semiring!: gb_semiring "op +" "op *" "op ^" "0::'a::{comm_semiring_1, recpower}" "1" - proof qed (auto simp add: ring_simps power_Suc) + proof qed (auto simp add: algebra_simps power_Suc) lemmas nat_arith = add_nat_number_of @@ -345,13 +345,13 @@ interpretation class_ringb!: ringb "op +" "op *" "op ^" "0::'a::{idom,recpower,number_ring}" "1" "op -" "uminus" -proof(unfold_locales, simp add: ring_simps power_Suc, auto) +proof(unfold_locales, simp add: algebra_simps power_Suc, auto) fix w x y z ::"'a::{idom,recpower,number_ring}" assume p: "w * y + x * z = w * z + x * y" and ynz: "y \ z" hence ynz': "y - z \ 0" by simp from p have "w * y + x* z - w*z - x*y = 0" by simp - hence "w* (y - z) - x * (y - z) = 0" by (simp add: ring_simps) - hence "(y - z) * (w - x) = 0" by (simp add: ring_simps) + hence "w* (y - z) - x * (y - z) = 0" by (simp add: algebra_simps) + hence "(y - z) * (w - x) = 0" by (simp add: algebra_simps) with no_zero_divirors_neq0 [OF ynz'] have "w - x = 0" by blast thus "w = x" by simp @@ -361,20 +361,20 @@ interpretation natgb!: semiringb "op +" "op *" "op ^" "0::nat" "1" -proof (unfold_locales, simp add: ring_simps power_Suc) +proof (unfold_locales, simp add: algebra_simps power_Suc) fix w x y z ::"nat" { assume p: "w * y + x * z = w * z + x * y" and ynz: "y \ z" hence "y < z \ y > z" by arith moreover { assume lt:"y k. z = y + k \ k > 0" by (rule_tac x="z - y" in exI, auto) then obtain k where kp: "k>0" and yz:"z = y + k" by blast - from p have "(w * y + x *y) + x*k = (w * y + x*y) + w*k" by (simp add: yz ring_simps) + from p have "(w * y + x *y) + x*k = (w * y + x*y) + w*k" by (simp add: yz algebra_simps) hence "x*k = w*k" by simp hence "w = x" using kp by (simp add: mult_cancel2) } moreover { assume lt: "y >z" hence "\k. y = z + k \ k>0" by (rule_tac x="y - z" in exI, auto) then obtain k where kp: "k>0" and yz:"y = z + k" by blast - from p have "(w * z + x *z) + w*k = (w * z + x*z) + x*k" by (simp add: yz ring_simps) + from p have "(w * z + x *z) + w*k = (w * z + x*z) + x*k" by (simp add: yz algebra_simps) hence "w*k = x*k" by simp hence "w = x" using kp by (simp add: mult_cancel2)} ultimately have "w=x" by blast } diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/Int.thy --- a/src/HOL/Int.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/Int.thy Wed Jan 28 16:29:16 2009 +0100 @@ -157,13 +157,13 @@ show "i - j = i + - j" by (simp add: diff_int_def) show "(i * j) * k = i * (j * k)" - by (cases i, cases j, cases k) (simp add: mult ring_simps) + by (cases i, cases j, cases k) (simp add: mult algebra_simps) show "i * j = j * i" - by (cases i, cases j) (simp add: mult ring_simps) + by (cases i, cases j) (simp add: mult algebra_simps) show "1 * i = i" by (cases i) (simp add: One_int_def mult) show "(i + j) * k = i * k + j * k" - by (cases i, cases j, cases k) (simp add: add mult ring_simps) + by (cases i, cases j, cases k) (simp add: add mult algebra_simps) show "0 \ (1::int)" by (simp add: Zero_int_def One_int_def) qed @@ -301,36 +301,35 @@ lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j" proof - have "(\(i,j). { of_nat i - (of_nat j :: 'a) }) respects intrel" - by (simp add: congruent_def compare_rls of_nat_add [symmetric] + by (simp add: congruent_def algebra_simps of_nat_add [symmetric] del: of_nat_add) thus ?thesis by (simp add: of_int_def UN_equiv_class [OF equiv_intrel]) qed lemma of_int_0 [simp]: "of_int 0 = 0" - by (simp add: of_int Zero_int_def) +by (simp add: of_int Zero_int_def) lemma of_int_1 [simp]: "of_int 1 = 1" - by (simp add: of_int One_int_def) +by (simp add: of_int One_int_def) lemma of_int_add [simp]: "of_int (w+z) = of_int w + of_int z" - by (cases w, cases z, simp add: compare_rls of_int OrderedGroup.compare_rls add) +by (cases w, cases z, simp add: algebra_simps of_int add) lemma of_int_minus [simp]: "of_int (-z) = - (of_int z)" - by (cases z, simp add: compare_rls of_int minus) +by (cases z, simp add: algebra_simps of_int minus) lemma of_int_diff [simp]: "of_int (w - z) = of_int w - of_int z" - by (simp add: OrderedGroup.diff_minus diff_minus) +by (simp add: OrderedGroup.diff_minus diff_minus) lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z" apply (cases w, cases z) -apply (simp add: compare_rls of_int left_diff_distrib right_diff_distrib - mult add_ac of_nat_mult) +apply (simp add: algebra_simps of_int mult of_nat_mult) done text{*Collapse nested embeddings*} lemma of_int_of_nat_eq [simp]: "of_int (of_nat n) = of_nat n" - by (induct n) auto +by (induct n) auto end @@ -339,7 +338,7 @@ lemma of_int_le_iff [simp]: "of_int w \ of_int z \ w \ z" - by (cases w, cases z, simp add: of_int le minus compare_rls of_nat_add [symmetric] del: of_nat_add) +by (cases w, cases z, simp add: of_int le minus algebra_simps of_nat_add [symmetric] del: of_nat_add) text{*Special cases where either operand is zero*} lemmas of_int_0_le_iff [simp] = of_int_le_iff [of 0, simplified] @@ -511,7 +510,7 @@ also have "\ = (\n. z - w = of_nat n)" by (auto elim: zero_le_imp_eq_int) also have "\ = (\n. z = w + of_nat n)" - by (simp only: group_simps) + by (simp only: algebra_simps) finally show ?thesis . qed @@ -829,7 +828,7 @@ next case (neg n) thus ?thesis by (simp del: of_nat_Suc of_nat_add - add: compare_rls of_nat_1 [symmetric] of_nat_add [symmetric]) + add: algebra_simps of_nat_1 [symmetric] of_nat_add [symmetric]) qed lemma bin_less_0_simps: @@ -1067,16 +1066,16 @@ lemma eq_number_of_eq: "((number_of x::'a::number_ring) = number_of y) = iszero (number_of (x + uminus y) :: 'a)" - unfolding iszero_def number_of_add number_of_minus - by (simp add: compare_rls) +unfolding iszero_def number_of_add number_of_minus +by (simp add: algebra_simps) lemma iszero_number_of_Pls: "iszero ((number_of Pls)::'a::number_ring)" - unfolding iszero_def numeral_0_eq_0 .. +unfolding iszero_def numeral_0_eq_0 .. lemma nonzero_number_of_Min: "~ iszero ((number_of Min)::'a::number_ring)" - unfolding iszero_def numeral_m1_eq_minus_1 by simp +unfolding iszero_def numeral_m1_eq_minus_1 by simp subsubsection {* Comparisons, for Ordered Rings *} @@ -1162,7 +1161,7 @@ next case (neg n) thus ?thesis by (simp del: of_nat_Suc of_nat_add - add: compare_rls of_nat_1 [symmetric] of_nat_add [symmetric]) + add: algebra_simps of_nat_1 [symmetric] of_nat_add [symmetric]) qed text {* Less-Than or Equals *} @@ -1249,9 +1248,7 @@ lemma add_number_of_diff2 [simp]: "number_of v + (c - number_of w) = number_of (v + uminus w) + (c::'a::number_ring)" -apply (subst diff_number_of_eq [symmetric]) -apply (simp only: compare_rls) -done +by (simp add: algebra_simps diff_number_of_eq [symmetric]) subsection {* The Set of Integers *} diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/IntDiv.thy --- a/src/HOL/IntDiv.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/IntDiv.thy Wed Jan 28 16:29:16 2009 +0100 @@ -831,12 +831,13 @@ lemma zmult2_lemma_aux1: "[| (0::int) < c; b < r; r \ 0 |] ==> b*c < b*(q mod c) + r" apply (subgoal_tac "b * (c - q mod c) < r * 1") -apply (simp add: right_diff_distrib) + apply (simp add: algebra_simps) apply (rule order_le_less_trans) -apply (erule_tac [2] mult_strict_right_mono) -apply (rule mult_left_mono_neg) -apply (auto simp add: compare_rls add_commute [of 1] - add1_zle_eq pos_mod_bound) + apply (erule_tac [2] mult_strict_right_mono) + apply (rule mult_left_mono_neg) + using add1_zle_eq[of "q mod c"]apply(simp add: algebra_simps pos_mod_bound) + apply (simp) +apply (simp) done lemma zmult2_lemma_aux2: @@ -854,12 +855,13 @@ lemma zmult2_lemma_aux4: "[| (0::int) < c; 0 \ r; r < b |] ==> b * (q mod c) + r < b * c" apply (subgoal_tac "r * 1 < b * (c - q mod c) ") -apply (simp add: right_diff_distrib) + apply (simp add: right_diff_distrib) apply (rule order_less_le_trans) -apply (erule mult_strict_right_mono) -apply (rule_tac [2] mult_left_mono) -apply (auto simp add: compare_rls add_commute [of 1] - add1_zle_eq pos_mod_bound) + apply (erule mult_strict_right_mono) + apply (rule_tac [2] mult_left_mono) + apply simp + using add1_zle_eq[of "q mod c"] apply (simp add: algebra_simps pos_mod_bound) +apply simp done lemma zmult2_lemma: "[| quorem ((a,b), (q,r)); b \ 0; 0 < c |] @@ -1251,7 +1253,7 @@ lemma zmult_div_cancel: "(n::int) * (m div n) = m - (m mod n)" using zmod_zdiv_equality[where a="m" and b="n"] - by (simp add: ring_simps) + by (simp add: algebra_simps) lemma zdvd_mult_div_cancel:"(n::int) dvd m \ n * (m div n) = m" apply (subgoal_tac "m mod n = 0") diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/Library/Abstract_Rat.thy --- a/src/HOL/Library/Abstract_Rat.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/Library/Abstract_Rat.thy Wed Jan 28 16:29:16 2009 +0100 @@ -240,7 +240,7 @@ by (simp only: of_int_mult[symmetric] of_int_add [symmetric]) then have "of_int x / of_int d = ?t / of_int d" using cong[OF refl[of ?f] eq] by simp - then show ?thesis by (simp add: add_divide_distrib ring_simps prems) + then show ?thesis by (simp add: add_divide_distrib algebra_simps prems) qed lemma of_int_div: "(d::int) ~= 0 ==> d dvd n ==> diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/Library/BigO.thy --- a/src/HOL/Library/BigO.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/Library/BigO.thy Wed Jan 28 16:29:16 2009 +0100 @@ -349,7 +349,7 @@ apply (drule set_plus_imp_minus) apply (rule set_minus_imp_plus) apply (drule bigo_mult3 [where g = g and j = g]) - apply (auto simp add: ring_simps) + apply (auto simp add: algebra_simps) done lemma bigo_mult5: "ALL x. f x ~= 0 ==> @@ -799,14 +799,14 @@ apply simp apply (subst abs_of_nonneg) apply (drule_tac x = x in spec) back - apply (simp add: compare_rls) + apply (simp add: algebra_simps) apply (subst diff_minus)+ apply (rule add_right_mono) apply (erule spec) apply (rule order_trans) prefer 2 apply (rule abs_ge_zero) - apply (simp add: compare_rls) + apply (simp add: algebra_simps) done lemma bigo_lesso3: "f =o g +o O(h) ==> @@ -823,7 +823,7 @@ apply simp apply (subst abs_of_nonneg) apply (drule_tac x = x in spec) back - apply (simp add: compare_rls) + apply (simp add: algebra_simps) apply (subst diff_minus)+ apply (rule add_left_mono) apply (rule le_imp_neg_le) @@ -831,7 +831,7 @@ apply (rule order_trans) prefer 2 apply (rule abs_ge_zero) - apply (simp add: compare_rls) + apply (simp add: algebra_simps) done lemma bigo_lesso4: "f 'b::ordered_field) ==> @@ -844,7 +844,7 @@ apply assumption apply (erule bigo_lesseq2) back apply (rule allI) - apply (auto simp add: func_plus fun_diff_def compare_rls + apply (auto simp add: func_plus fun_diff_def algebra_simps split: split_max abs_split) done @@ -856,7 +856,7 @@ apply (rule allI) apply (drule_tac x = x in spec) apply (subgoal_tac "abs(max (f x - g x) 0) = max (f x - g x) 0") - apply (clarsimp simp add: compare_rls add_ac) + apply (clarsimp simp add: algebra_simps) apply (rule abs_of_nonneg) apply (rule le_maxI2) done diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/Library/Commutative_Ring.thy --- a/src/HOL/Library/Commutative_Ring.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/Library/Commutative_Ring.thy Wed Jan 28 16:29:16 2009 +0100 @@ -173,11 +173,11 @@ text {* mkPinj preserve semantics *} lemma mkPinj_ci: "Ipol l (mkPinj a B) = Ipol l (Pinj a B)" - by (induct B) (auto simp add: mkPinj_def ring_simps) + by (induct B) (auto simp add: mkPinj_def algebra_simps) text {* mkPX preserves semantics *} lemma mkPX_ci: "Ipol l (mkPX A b C) = Ipol l (PX A b C)" - by (cases A) (auto simp add: mkPX_def mkPinj_ci power_add ring_simps) + by (cases A) (auto simp add: mkPX_def mkPinj_ci power_add algebra_simps) text {* Correctness theorems for the implemented operations *} @@ -192,13 +192,13 @@ show ?case proof (rule linorder_cases) assume "x < y" - with 6 show ?case by (simp add: mkPinj_ci ring_simps) + with 6 show ?case by (simp add: mkPinj_ci algebra_simps) next assume "x = y" with 6 show ?case by (simp add: mkPinj_ci) next assume "x > y" - with 6 show ?case by (simp add: mkPinj_ci ring_simps) + with 6 show ?case by (simp add: mkPinj_ci algebra_simps) qed next case (7 x P Q y R) @@ -206,7 +206,7 @@ moreover { assume "x = 0" with 7 have ?case by simp } moreover - { assume "x = 1" with 7 have ?case by (simp add: ring_simps) } + { assume "x = 1" with 7 have ?case by (simp add: algebra_simps) } moreover { assume "x > 1" from 7 have ?case by (cases x) simp_all } ultimately show ?case by blast @@ -225,20 +225,20 @@ show ?case proof (rule linorder_cases) assume a: "x < y" hence "EX d. d + x = y" by arith - with 9 a show ?case by (auto simp add: mkPX_ci power_add ring_simps) + with 9 a show ?case by (auto simp add: mkPX_ci power_add algebra_simps) next assume a: "y < x" hence "EX d. d + y = x" by arith - with 9 a show ?case by (auto simp add: power_add mkPX_ci ring_simps) + with 9 a show ?case by (auto simp add: power_add mkPX_ci algebra_simps) next assume "x = y" - with 9 show ?case by (simp add: mkPX_ci ring_simps) + with 9 show ?case by (simp add: mkPX_ci algebra_simps) qed -qed (auto simp add: ring_simps) +qed (auto simp add: algebra_simps) text {* Multiplication *} lemma mul_ci: "Ipol l (P \ Q) = Ipol l P * Ipol l Q" by (induct P Q arbitrary: l rule: mul.induct) - (simp_all add: mkPX_ci mkPinj_ci ring_simps add_ci power_add) + (simp_all add: mkPX_ci mkPinj_ci algebra_simps add_ci power_add) text {* Substraction *} lemma sub_ci: "Ipol l (P \ Q) = Ipol l P - Ipol l Q" @@ -247,7 +247,7 @@ text {* Square *} lemma sqr_ci: "Ipol ls (sqr P) = Ipol ls P * Ipol ls P" by (induct P arbitrary: ls) - (simp_all add: add_ci mkPinj_ci mkPX_ci mul_ci ring_simps power_add) + (simp_all add: add_ci mkPinj_ci mkPX_ci mul_ci algebra_simps power_add) text {* Power *} lemma even_pow:"even n \ pow n P = pow (n div 2) (sqr P)" diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/Library/Float.thy --- a/src/HOL/Library/Float.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/Library/Float.thy Wed Jan 28 16:29:16 2009 +0100 @@ -38,7 +38,7 @@ show ?thesis proof (induct a) case (1 n) - from pos show ?case by (simp add: ring_simps) + from pos show ?case by (simp add: algebra_simps) next case (2 n) show ?case @@ -59,7 +59,7 @@ show ?case by simp next case (Suc m) - show ?case by (auto simp add: ring_simps pow2_add1 prems) + show ?case by (auto simp add: algebra_simps pow2_add1 prems) qed next case (2 n) @@ -72,7 +72,7 @@ apply (subst pow2_neg[of "-1"]) apply (simp) apply (insert pow2_add1[of "-a"]) - apply (simp add: ring_simps) + apply (simp add: algebra_simps) apply (subst pow2_neg[of "-a"]) apply (simp) done @@ -83,7 +83,7 @@ apply (auto) apply (subst pow2_neg[of "a + (-2 - int m)"]) apply (subst pow2_neg[of "-2 - int m"]) - apply (auto simp add: ring_simps) + apply (auto simp add: algebra_simps) apply (subst a) apply (subst b) apply (simp only: pow2_add1) @@ -91,13 +91,13 @@ apply (subst pow2_neg[of "int m + 1"]) apply auto apply (insert prems) - apply (auto simp add: ring_simps) + apply (auto simp add: algebra_simps) done qed qed lemma "float (a, e) + float (b, e) = float (a + b, e)" -by (simp add: float_def ring_simps) +by (simp add: float_def algebra_simps) definition int_of_real :: "real \ int" where @@ -254,7 +254,7 @@ lemma float_transfer_even: "even a \ float (a, b) = float (a div 2, b+1)" apply (subst float_transfer[where a="a" and b="b" and c="-1", simplified]) - apply (simp_all add: pow2_def even_def real_is_int_def ring_simps) + apply (simp_all add: pow2_def even_def real_is_int_def algebra_simps) apply (auto) proof - fix q::int @@ -319,7 +319,7 @@ "float (a1, e1) + float (a2, e2) = (if e1<=e2 then float (a1+a2*2^(nat(e2-e1)), e1) else float (a1*2^(nat (e1-e2))+a2, e2))" - apply (simp add: float_def ring_simps) + apply (simp add: float_def algebra_simps) apply (auto simp add: pow2_int[symmetric] pow2_add[symmetric]) done diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/Library/Nat_Infinity.thy --- a/src/HOL/Library/Nat_Infinity.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/Library/Nat_Infinity.thy Wed Jan 28 16:29:16 2009 +0100 @@ -223,10 +223,10 @@ end lemma mult_iSuc: "iSuc m * n = n + m * n" - unfolding iSuc_plus_1 by (simp add: ring_simps) + unfolding iSuc_plus_1 by (simp add: algebra_simps) lemma mult_iSuc_right: "m * iSuc n = m + m * n" - unfolding iSuc_plus_1 by (simp add: ring_simps) + unfolding iSuc_plus_1 by (simp add: algebra_simps) lemma of_nat_eq_Fin: "of_nat n = Fin n" apply (induct n) diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/Library/Pocklington.thy --- a/src/HOL/Library/Pocklington.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/Library/Pocklington.thy Wed Jan 28 16:29:16 2009 +0100 @@ -254,7 +254,7 @@ apply (simp add: nat_mod) apply (rule_tac x="q" in exI) apply (rule_tac x="q + q" in exI) - by (auto simp: ring_simps) + by (auto simp: algebra_simps) lemma cong_to_1: "[a = 1] (mod n) \ a = 0 \ n = 1 \ (\m. a = 1 + m * n)" proof- @@ -780,7 +780,7 @@ of "(n - 1) div m * m"] have yn: "coprime ?y n" by (simp add: coprime_commute) have "?y mod n = (a^m)^((n - 1) div m) mod n" - by (simp add: ring_simps power_mult) + by (simp add: algebra_simps power_mult) also have "\ = (a^m mod n)^((n - 1) div m) mod n" using power_mod[of "a^m" n "(n - 1) div m"] by simp also have "\ = 1" using m(3)[unfolded modeq_def onen] onen @@ -1239,7 +1239,7 @@ from bqn psp qrn have bqn: "a ^ (n - 1) mod n = 1" and psp: "list_all (\p. prime p \ coprime (a^(r *(q div p)) mod n - 1) n) ps" unfolding arnb[symmetric] power_mod - by (simp_all add: power_mult[symmetric] ring_simps) + by (simp_all add: power_mult[symmetric] algebra_simps) from n have n0: "n > 0" by arith from mod_div_equality[of "a^(n - 1)" n] mod_less_divisor[OF n0, of "a^(n - 1)"] @@ -1248,7 +1248,7 @@ apply - apply (rule exI[where x="0"]) apply (rule exI[where x="a^(n - 1) div n"]) - by (simp add: ring_simps) + by (simp add: algebra_simps) {fix p assume p: "prime p" "p dvd q" from psp psq have pfpsq: "primefact ps q" by (auto simp add: primefact_variant list_all_iff) diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/Library/Primes.thy --- a/src/HOL/Library/Primes.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/Library/Primes.thy Wed Jan 28 16:29:16 2009 +0100 @@ -204,7 +204,7 @@ from z have z': "?g > 0" by simp from bezout_gcd_strong[OF az, of b] obtain x y where xy: "a*x = b*y + ?g" by blast - from xy a b have "?g * a'*x = ?g * (b'*y + 1)" by (simp add: ring_simps) + from xy a b have "?g * a'*x = ?g * (b'*y + 1)" by (simp add: algebra_simps) hence "?g * (a'*x) = ?g * (b'*y + 1)" by (simp add: mult_assoc) hence "a'*x = (b'*y + 1)" by (simp only: nat_mult_eq_cancel1[OF z']) diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/Library/SetsAndFunctions.thy --- a/src/HOL/Library/SetsAndFunctions.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/Library/SetsAndFunctions.thy Wed Jan 28 16:29:16 2009 +0100 @@ -101,8 +101,8 @@ instance "fun" :: (type,comm_ring_1)comm_ring_1 apply default - apply (auto simp add: func_plus func_times fun_Compl_def fun_diff_def ext - func_one func_zero ring_simps) + apply (auto simp add: func_plus func_times fun_Compl_def fun_diff_def + func_one func_zero algebra_simps) apply (drule fun_cong) apply simp done diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/Library/Univ_Poly.thy --- a/src/HOL/Library/Univ_Poly.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/Library/Univ_Poly.thy Wed Jan 28 16:29:16 2009 +0100 @@ -217,7 +217,7 @@ from Cons.hyps[rule_format, of x] obtain q r where qr: "x#xs = [r] +++ [- a, 1] *** q" by blast have "h#x#xs = [a*r + h] +++ [-a, 1] *** (r#q)" - using qr by(cases q, simp_all add: ring_simps diff_def[symmetric] + using qr by(cases q, simp_all add: algebra_simps diff_def[symmetric] minus_mult_left[symmetric] right_minus) hence "\q r. h#x#xs = [r] +++ [-a, 1] *** q" by blast} thus ?case by blast @@ -303,7 +303,7 @@ from C[of ?i] obtain y where y: "poly p y = 0" "\m\ Suc n. y \ ?i m" by blast from y have "y = a \ poly q y = 0" - by (simp only: q poly_mult_eq_zero_disj poly_add) (simp add: ring_simps) + by (simp only: q poly_mult_eq_zero_disj poly_add) (simp add: algebra_simps) with i[rule_format, of y] y(1) y(2) have False apply auto apply (erule_tac x="m" in allE) apply auto @@ -414,8 +414,8 @@ lemma (in idom_char_0) poly_entire: "poly (p *** q) = poly [] \ poly p = poly [] \ poly q = poly []" -using poly_entire_lemma2[of p q] -by auto (rule ext, simp add: poly_mult)+ +using poly_entire_lemma2[of p q] +by (auto simp add: expand_fun_eq poly_mult) lemma (in idom_char_0) poly_entire_neg: "(poly (p *** q) \ poly []) = ((poly p \ poly []) & (poly q \ poly []))" by (simp add: poly_entire) @@ -424,7 +424,7 @@ by (auto intro!: ext) lemma (in comm_ring_1) poly_add_minus_zero_iff: "(poly (p +++ -- q) = poly []) = (poly p = poly q)" -by (auto simp add: ring_simps poly_add poly_minus_def fun_eq poly_cmult minus_mult_left[symmetric]) +by (auto simp add: algebra_simps poly_add poly_minus_def fun_eq poly_cmult minus_mult_left[symmetric]) lemma (in comm_ring_1) poly_add_minus_mult_eq: "poly (p *** q +++ --(p *** r)) = poly (p *** (q +++ -- r))" by (auto simp add: poly_add poly_minus_def fun_eq poly_mult poly_cmult right_distrib minus_mult_left[symmetric] minus_mult_right[symmetric]) @@ -550,7 +550,7 @@ "[| p divides q; p divides (q +++ r) |] ==> p divides r" apply (simp add: divides_def, auto) apply (rule_tac x = "padd qaa (poly_minus qa)" in exI) -apply (auto simp add: poly_add fun_eq poly_mult poly_minus right_diff_distrib compare_rls add_ac) +apply (auto simp add: poly_add fun_eq poly_mult poly_minus algebra_simps) done lemma (in comm_ring_1) poly_divides_diff2: "[| p divides r; p divides (q +++ r) |] ==> p divides q" @@ -892,15 +892,15 @@ proof assume eq: ?lhs hence "\x. poly ((c#cs) +++ -- (d#ds)) x = 0" - by (simp only: poly_minus poly_add ring_simps) simp - hence "poly ((c#cs) +++ -- (d#ds)) = poly []" by - (rule ext, simp) + by (simp only: poly_minus poly_add algebra_simps) simp + hence "poly ((c#cs) +++ -- (d#ds)) = poly []" by(simp add:expand_fun_eq) hence "c = d \ list_all (\x. x=0) ((cs +++ -- ds))" - unfolding poly_zero by (simp add: poly_minus_def ring_simps minus_mult_left[symmetric]) + unfolding poly_zero by (simp add: poly_minus_def algebra_simps) hence "c = d \ (\x. poly (cs +++ -- ds) x = 0)" unfolding poly_zero[symmetric] by simp - thus ?rhs apply (simp add: poly_minus poly_add ring_simps) apply (rule ext, simp) done + thus ?rhs by (simp add: poly_minus poly_add algebra_simps expand_fun_eq) next - assume ?rhs then show ?lhs by - (rule ext,simp) + assume ?rhs then show ?lhs by(simp add:expand_fun_eq) qed lemma (in idom_char_0) pnormalize_unique: "poly p = poly q \ pnormalize p = pnormalize q" @@ -1008,7 +1008,7 @@ from p have ap: "poly ([a,1] *** p) \ poly []" using poly_mult_not_eq_poly_Nil unfolding poly_entire by auto have eq: "poly ([a,1] %^(Suc n) *** p) = poly ([a,1]%^n *** ([a,1] *** p))" - by (rule ext, simp add: poly_mult poly_add poly_exp poly_cmult mult_ac add_ac right_distrib) + by (rule ext, simp add: poly_mult poly_add poly_exp poly_cmult algebra_simps) from ap have ap': "(poly ([a,1] *** p) = poly []) = False" by blast have th0: "degree ([a,1]%^n *** ([a,1] *** p)) = degree ([a,1] *** p) + n" apply (simp only: Suc.hyps[of a "pmult [a,one] p"] ap') diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/Lim.thy --- a/src/HOL/Lim.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/Lim.thy Wed Jan 28 16:29:16 2009 +0100 @@ -52,7 +52,7 @@ apply (drule_tac r="r" in LIM_D, safe) apply (rule_tac x="s" in exI, safe) apply (drule_tac x="x + k" in spec) -apply (simp add: compare_rls) +apply (simp add: algebra_simps) done lemma LIM_offset_zero: "f -- a --> L \ (\h. f (a + h)) -- 0 --> L" diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/Ln.thy --- a/src/HOL/Ln.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/Ln.thy Wed Jan 28 16:29:16 2009 +0100 @@ -187,7 +187,7 @@ proof - assume a: "0 <= (x::real)" and b: "x < 1" have "(1 - x) * (1 + x + x^2) = (1 - x^3)" - by (simp add: ring_simps power2_eq_square power3_eq_cube) + by (simp add: algebra_simps power2_eq_square power3_eq_cube) also have "... <= 1" by (auto simp add: a) finally have "(1 - x) * (1 + x + x ^ 2) <= 1" . @@ -325,10 +325,10 @@ done also have "... <= 2 * x^2" apply (subgoal_tac "- (-x) - 2 * (-x)^2 <= ln (1 - (-x))") - apply (simp add: compare_rls) + apply (simp add: algebra_simps) apply (rule ln_one_minus_pos_lower_bound) apply (insert prems, auto) - done + done finally show ?thesis . qed @@ -375,7 +375,7 @@ apply simp apply (subst ln_div [THEN sym]) apply arith - apply (auto simp add: ring_simps add_frac_eq frac_eq_eq + apply (auto simp add: algebra_simps add_frac_eq frac_eq_eq add_divide_distrib power2_eq_square) apply (rule mult_pos_pos, assumption)+ apply assumption @@ -394,7 +394,7 @@ apply auto done have "x * ln y - x * ln x = x * (ln y - ln x)" - by (simp add: ring_simps) + by (simp add: algebra_simps) also have "... = x * ln(y / x)" apply (subst ln_div) apply (rule b, rule a, rule refl) diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/Matrix/LP.thy --- a/src/HOL/Matrix/LP.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/Matrix/LP.thy Wed Jan 28 16:29:16 2009 +0100 @@ -20,7 +20,7 @@ proof - from prems have 1: "y * b <= y * b'" by (simp add: mult_left_mono) from prems have 2: "y * (A * x) <= y * b" by (simp add: mult_left_mono) - have 3: "y * (A * x) = c * x + (y * (A - A') + (y * A' - c') + (c'-c)) * x" by (simp add: ring_simps) + have 3: "y * (A * x) = c * x + (y * (A - A') + (y * A' - c') + (c'-c)) * x" by (simp add: algebra_simps) from 1 2 3 have 4: "c * x + (y * (A - A') + (y * A' - c') + (c'-c)) * x <= y * b'" by simp have 5: "c * x <= y * b' + abs((y * (A - A') + (y * A' - c') + (c'-c)) * x)" by (simp only: 4 estimate_by_abs) @@ -32,7 +32,7 @@ by (simp add: abs_triangle_ineq mult_right_mono) have 9: "(abs (y * (A-A')) + abs (y*A'-c') + abs(c'-c)) * abs x <= (abs y * abs (A-A') + abs (y*A'-c') + abs (c'-c)) * abs x" by (simp add: abs_le_mult mult_right_mono) - have 10: "c'-c = -(c-c')" by (simp add: ring_simps) + have 10: "c'-c = -(c-c')" by (simp add: algebra_simps) have 11: "abs (c'-c) = abs (c-c')" by (subst 10, subst abs_minus_cancel, simp) have 12: "(abs y * abs (A-A') + abs (y*A'-c') + abs (c'-c)) * abs x <= (abs y * abs (A-A') + abs (y*A'-c') + \c) * abs x" @@ -85,7 +85,7 @@ apply simp done then have "a * b = pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b" - by (simp add: ring_simps) + by (simp add: algebra_simps) moreover have "pprt a * pprt b <= pprt a2 * pprt b2" by (simp_all add: prems mult_mono) moreover have "pprt a * nprt b <= pprt a1 * nprt b2" @@ -134,10 +134,10 @@ (is "_ <= _ + ?C") proof - from prems have "y * (A * x) <= y * b" by (simp add: mult_left_mono) - moreover have "y * (A * x) = c * x + (y * A - c) * x" by (simp add: ring_simps) + moreover have "y * (A * x) = c * x + (y * A - c) * x" by (simp add: algebra_simps) ultimately have "c * x + (y * A - c) * x <= y * b" by simp then have "c * x <= y * b - (y * A - c) * x" by (simp add: le_diff_eq) - then have cx: "c * x <= y * b + (c - y * A) * x" by (simp add: ring_simps) + then have cx: "c * x <= y * b + (c - y * A) * x" by (simp add: algebra_simps) have s2: "c - y * A <= c2 - y * A1" by (simp add: diff_def prems add_mono mult_left_mono) have s1: "c1 - y * A2 <= c - y * A" diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/Matrix/Matrix.thy --- a/src/HOL/Matrix/Matrix.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/Matrix/Matrix.thy Wed Jan 28 16:29:16 2009 +0100 @@ -1573,17 +1573,17 @@ show "A * B * C = A * (B * C)" apply (simp add: times_matrix_def) apply (rule mult_matrix_assoc) - apply (simp_all add: associative_def ring_simps) + apply (simp_all add: associative_def algebra_simps) done show "(A + B) * C = A * C + B * C" apply (simp add: times_matrix_def plus_matrix_def) apply (rule l_distributive_matrix[simplified l_distributive_def, THEN spec, THEN spec, THEN spec]) - apply (simp_all add: associative_def commutative_def ring_simps) + apply (simp_all add: associative_def commutative_def algebra_simps) done show "A * (B + C) = A * B + A * C" apply (simp add: times_matrix_def plus_matrix_def) apply (rule r_distributive_matrix[simplified r_distributive_def, THEN spec, THEN spec, THEN spec]) - apply (simp_all add: associative_def commutative_def ring_simps) + apply (simp_all add: associative_def commutative_def algebra_simps) done qed @@ -1793,7 +1793,7 @@ by (simp add: scalar_mult_def) lemma scalar_mult_add: "scalar_mult y (a+b) = (scalar_mult y a) + (scalar_mult y b)" -by (simp add: scalar_mult_def apply_matrix_add ring_simps) +by (simp add: scalar_mult_def apply_matrix_add algebra_simps) lemma Rep_scalar_mult[simp]: "Rep_matrix (scalar_mult y a) j i = y * (Rep_matrix a j i)" by (simp add: scalar_mult_def) diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/Matrix/SparseMatrix.thy --- a/src/HOL/Matrix/SparseMatrix.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/Matrix/SparseMatrix.thy Wed Jan 28 16:29:16 2009 +0100 @@ -274,7 +274,7 @@ apply (rule conjI) apply (intro strip) apply (frule_tac as=brr in sorted_spvec_cons1) - apply (simp add: ring_simps sparse_row_matrix_cons) + apply (simp add: algebra_simps sparse_row_matrix_cons) apply (simplesubst Rep_matrix_zero_imp_mult_zero) apply (simp) apply (intro strip) @@ -296,7 +296,7 @@ apply (intro strip | rule conjI)+ apply (frule_tac as=arr in sorted_spvec_cons1) - apply (simp add: ring_simps) + apply (simp add: algebra_simps) apply (subst Rep_matrix_zero_imp_mult_zero) apply (simp) apply (rule disjI2) @@ -310,7 +310,7 @@ apply (simp_all) apply (frule_tac as=arr in sorted_spvec_cons1) apply (frule_tac as=brr in sorted_spvec_cons1) - apply (simp add: sparse_row_matrix_cons ring_simps sparse_row_vector_addmult_spvec) + apply (simp add: sparse_row_matrix_cons algebra_simps sparse_row_vector_addmult_spvec) apply (rule_tac B1 = "sparse_row_matrix brr" in ssubst[OF Rep_matrix_zero_imp_mult_zero]) apply (auto) apply (rule sorted_sparse_row_matrix_zero) @@ -360,7 +360,7 @@ lemma sparse_row_mult_spmat[rule_format]: "sorted_spmat A \ sorted_spvec B \ sparse_row_matrix (mult_spmat A B) = (sparse_row_matrix A) * (sparse_row_matrix B)" apply (induct A) - apply (auto simp add: sparse_row_matrix_cons sparse_row_mult_spvec_spmat ring_simps move_matrix_mult) + apply (auto simp add: sparse_row_matrix_cons sparse_row_mult_spvec_spmat algebra_simps move_matrix_mult) done lemma sorted_spvec_mult_spmat[rule_format]: diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/Matrix/cplex/Cplex.thy --- a/src/HOL/Matrix/cplex/Cplex.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/Matrix/cplex/Cplex.thy Wed Jan 28 16:29:16 2009 +0100 @@ -34,8 +34,8 @@ add_spmat (mult_spmat (nprt_spmat s2) (pprt_spmat r1), mult_spmat (nprt_spmat s1) (nprt_spmat r1)))))))" apply (simp add: Let_def) apply (insert assms) - apply (simp add: sparse_row_matrix_op_simps ring_simps) - apply (rule mult_le_dual_prts[where A=A, simplified Let_def ring_simps]) + apply (simp add: sparse_row_matrix_op_simps algebra_simps) + apply (rule mult_le_dual_prts[where A=A, simplified Let_def algebra_simps]) apply (auto) done diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/MetisExamples/BigO.thy --- a/src/HOL/MetisExamples/BigO.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/MetisExamples/BigO.thy Wed Jan 28 16:29:16 2009 +0100 @@ -486,7 +486,7 @@ have 2: "\X3. (0\'b) + X3 = X3" by (metis diff_eq_eq right_minus_eq) have 3: "\ (0\'b) \ f x - lb x" - by (metis 1 compare_rls(1)) + by (metis 1 diff_minus) have 4: "\ (0\'b) + lb x \ f x" by (metis 3 le_diff_eq) show "False" @@ -1197,7 +1197,7 @@ apply (erule thin_rl) (*sledgehammer*); apply (case_tac "0 <= f x - k x") - apply (simp del: compare_rls diff_minus); + apply (simp) apply (subst abs_of_nonneg) apply (drule_tac x = x in spec) back ML_command{*AtpWrapper.problem_name := "BigO__bigo_lesso3_simpler"*} @@ -1216,7 +1216,7 @@ apply assumption apply (erule bigo_lesseq2) back apply (rule allI) - apply (auto simp add: func_plus fun_diff_def compare_rls + apply (auto simp add: func_plus fun_diff_def algebra_simps split: split_max abs_split) done diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/Nat.thy --- a/src/HOL/Nat.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/Nat.thy Wed Jan 28 16:29:16 2009 +0100 @@ -1254,7 +1254,7 @@ begin lemma of_nat_diff: "n \ m \ of_nat (m - n) = of_nat m - of_nat n" - by (simp add: compare_rls of_nat_add [symmetric]) +by (simp add: algebra_simps of_nat_add [symmetric]) end diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/NumberTheory/IntPrimes.thy --- a/src/HOL/NumberTheory/IntPrimes.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/NumberTheory/IntPrimes.thy Wed Jan 28 16:29:16 2009 +0100 @@ -146,7 +146,7 @@ lemma zcong_trans: "[a = b] (mod m) ==> [b = c] (mod m) ==> [a = c] (mod m)" unfolding zcong_def - apply (auto elim!: dvdE simp add: ring_simps) + apply (auto elim!: dvdE simp add: algebra_simps) unfolding left_distrib [symmetric] apply (rule dvd_mult dvd_refl)+ done @@ -255,7 +255,7 @@ lemma zcong_iff_lin: "([a = b] (mod m)) = (\k. b = a + m * k)" unfolding zcong_def - apply (auto elim!: dvdE simp add: ring_simps) + apply (auto elim!: dvdE simp add: algebra_simps) apply (rule_tac x = "-k" in exI) apply simp done diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/OrderedGroup.thy --- a/src/HOL/OrderedGroup.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/OrderedGroup.thy Wed Jan 28 16:29:16 2009 +0100 @@ -22,17 +22,34 @@ \end{itemize} *} +ML{* +structure AlgebraSimps = + NamedThmsFun(val name = "algebra_simps" + val description = "algebra simplification rules"); +*} + +setup AlgebraSimps.setup + +text{* The rewrites accumulated in @{text algebra_simps} deal with the +classical algebraic structures of groups, rings and family. They simplify +terms by multiplying everything out (in case of a ring) and bringing sums and +products into a canonical form (by ordered rewriting). As a result it decides +group and ring equalities but also helps with inequalities. + +Of course it also works for fields, but it knows nothing about multiplicative +inverses or division. This is catered for by @{text field_simps}. *} + subsection {* Semigroups and Monoids *} class semigroup_add = plus + - assumes add_assoc: "(a + b) + c = a + (b + c)" + assumes add_assoc[algebra_simps]: "(a + b) + c = a + (b + c)" class ab_semigroup_add = semigroup_add + - assumes add_commute: "a + b = b + a" + assumes add_commute[algebra_simps]: "a + b = b + a" begin -lemma add_left_commute: "a + (b + c) = b + (a + c)" - by (rule mk_left_commute [of "plus", OF add_assoc add_commute]) +lemma add_left_commute[algebra_simps]: "a + (b + c) = b + (a + c)" +by (rule mk_left_commute [of "plus", OF add_assoc add_commute]) theorems add_ac = add_assoc add_commute add_left_commute @@ -41,14 +58,14 @@ theorems add_ac = add_assoc add_commute add_left_commute class semigroup_mult = times + - assumes mult_assoc: "(a * b) * c = a * (b * c)" + assumes mult_assoc[algebra_simps]: "(a * b) * c = a * (b * c)" class ab_semigroup_mult = semigroup_mult + - assumes mult_commute: "a * b = b * a" + assumes mult_commute[algebra_simps]: "a * b = b * a" begin -lemma mult_left_commute: "a * (b * c) = b * (a * c)" - by (rule mk_left_commute [of "times", OF mult_assoc mult_commute]) +lemma mult_left_commute[algebra_simps]: "a * (b * c) = b * (a * c)" +by (rule mk_left_commute [of "times", OF mult_assoc mult_commute]) theorems mult_ac = mult_assoc mult_commute mult_left_commute @@ -57,24 +74,20 @@ theorems mult_ac = mult_assoc mult_commute mult_left_commute class ab_semigroup_idem_mult = ab_semigroup_mult + - assumes mult_idem: "x * x = x" + assumes mult_idem[simp]: "x * x = x" begin -lemma mult_left_idem: "x * (x * y) = x * y" +lemma mult_left_idem[simp]: "x * (x * y) = x * y" unfolding mult_assoc [symmetric, of x] mult_idem .. -lemmas mult_ac_idem = mult_ac mult_idem mult_left_idem - end -lemmas mult_ac_idem = mult_ac mult_idem mult_left_idem - class monoid_add = zero + semigroup_add + assumes add_0_left [simp]: "0 + a = a" and add_0_right [simp]: "a + 0 = a" lemma zero_reorient: "0 = x \ x = 0" - by (rule eq_commute) +by (rule eq_commute) class comm_monoid_add = zero + ab_semigroup_add + assumes add_0: "0 + a = a" @@ -90,7 +103,7 @@ assumes mult_1_right [simp]: "a * 1 = a" lemma one_reorient: "1 = x \ x = 1" - by (rule eq_commute) +by (rule eq_commute) class comm_monoid_mult = one + ab_semigroup_mult + assumes mult_1: "1 * a = a" @@ -108,11 +121,11 @@ lemma add_left_cancel [simp]: "a + b = a + c \ b = c" - by (blast dest: add_left_imp_eq) +by (blast dest: add_left_imp_eq) lemma add_right_cancel [simp]: "b + a = c + a \ b = c" - by (blast dest: add_right_imp_eq) +by (blast dest: add_right_imp_eq) end @@ -142,7 +155,7 @@ begin lemma minus_add_cancel: "- a + (a + b) = b" - by (simp add: add_assoc[symmetric]) +by (simp add: add_assoc[symmetric]) lemma minus_zero [simp]: "- 0 = 0" proof - @@ -176,8 +189,7 @@ qed lemma equals_zero_I: - assumes "a + b = 0" - shows "- a = b" + assumes "a + b = 0" shows "- a = b" proof - have "- a = - a + (a + b)" using assms by simp also have "\ = b" by (simp add: add_assoc[symmetric]) @@ -185,23 +197,22 @@ qed lemma diff_self [simp]: "a - a = 0" - by (simp add: diff_minus) +by (simp add: diff_minus) lemma diff_0 [simp]: "0 - a = - a" - by (simp add: diff_minus) +by (simp add: diff_minus) lemma diff_0_right [simp]: "a - 0 = a" - by (simp add: diff_minus) +by (simp add: diff_minus) lemma diff_minus_eq_add [simp]: "a - - b = a + b" - by (simp add: diff_minus) +by (simp add: diff_minus) lemma neg_equal_iff_equal [simp]: "- a = - b \ a = b" proof assume "- a = - b" - hence "- (- a) = - (- b)" - by simp + hence "- (- a) = - (- b)" by simp thus "a = b" by simp next assume "a = b" @@ -210,11 +221,11 @@ lemma neg_equal_0_iff_equal [simp]: "- a = 0 \ a = 0" - by (subst neg_equal_iff_equal [symmetric], simp) +by (subst neg_equal_iff_equal [symmetric], simp) lemma neg_0_equal_iff_equal [simp]: "0 = - a \ 0 = a" - by (subst neg_equal_iff_equal [symmetric], simp) +by (subst neg_equal_iff_equal [symmetric], simp) text{*The next two equations can make the simplifier loop!*} @@ -233,10 +244,12 @@ qed lemma diff_add_cancel: "a - b + b = a" - by (simp add: diff_minus add_assoc) +by (simp add: diff_minus add_assoc) lemma add_diff_cancel: "a + b - b = a" - by (simp add: diff_minus add_assoc) +by (simp add: diff_minus add_assoc) + +declare diff_minus[symmetric, algebra_simps] end @@ -257,43 +270,38 @@ then show "b = c" by simp qed -lemma uminus_add_conv_diff: +lemma uminus_add_conv_diff[algebra_simps]: "- a + b = b - a" - by (simp add:diff_minus add_commute) +by (simp add:diff_minus add_commute) lemma minus_add_distrib [simp]: "- (a + b) = - a + - b" - by (rule equals_zero_I) (simp add: add_ac) +by (rule equals_zero_I) (simp add: add_ac) lemma minus_diff_eq [simp]: "- (a - b) = b - a" - by (simp add: diff_minus add_commute) - -lemma add_diff_eq: "a + (b - c) = (a + b) - c" - by (simp add: diff_minus add_ac) +by (simp add: diff_minus add_commute) -lemma diff_add_eq: "(a - b) + c = (a + c) - b" - by (simp add: diff_minus add_ac) +lemma add_diff_eq[algebra_simps]: "a + (b - c) = (a + b) - c" +by (simp add: diff_minus add_ac) -lemma diff_eq_eq: "a - b = c \ a = c + b" - by (auto simp add: diff_minus add_assoc) +lemma diff_add_eq[algebra_simps]: "(a - b) + c = (a + c) - b" +by (simp add: diff_minus add_ac) -lemma eq_diff_eq: "a = c - b \ a + b = c" - by (auto simp add: diff_minus add_assoc) +lemma diff_eq_eq[algebra_simps]: "a - b = c \ a = c + b" +by (auto simp add: diff_minus add_assoc) -lemma diff_diff_eq: "(a - b) - c = a - (b + c)" - by (simp add: diff_minus add_ac) +lemma eq_diff_eq[algebra_simps]: "a = c - b \ a + b = c" +by (auto simp add: diff_minus add_assoc) -lemma diff_diff_eq2: "a - (b - c) = (a + c) - b" - by (simp add: diff_minus add_ac) +lemma diff_diff_eq[algebra_simps]: "(a - b) - c = a - (b + c)" +by (simp add: diff_minus add_ac) -lemmas compare_rls = - diff_minus [symmetric] - add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2 - diff_eq_eq eq_diff_eq +lemma diff_diff_eq2[algebra_simps]: "a - (b - c) = (a + c) - b" +by (simp add: diff_minus add_ac) lemma eq_iff_diff_eq_0: "a = b \ a - b = 0" - by (simp add: compare_rls) +by (simp add: algebra_simps) end @@ -305,7 +313,7 @@ lemma add_right_mono: "a \ b \ a + c \ b + c" - by (simp add: add_commute [of _ c] add_left_mono) +by (simp add: add_commute [of _ c] add_left_mono) text {* non-strict, in both arguments *} lemma add_mono: @@ -322,11 +330,11 @@ lemma add_strict_left_mono: "a < b \ c + a < c + b" - by (auto simp add: less_le add_left_mono) +by (auto simp add: less_le add_left_mono) lemma add_strict_right_mono: "a < b \ a + c < b + c" - by (simp add: add_commute [of _ c] add_strict_left_mono) +by (simp add: add_commute [of _ c] add_strict_left_mono) text{*Strict monotonicity in both arguments*} lemma add_strict_mono: @@ -355,8 +363,7 @@ begin lemma add_less_imp_less_left: - assumes less: "c + a < c + b" - shows "a < b" + assumes less: "c + a < c + b" shows "a < b" proof - from less have le: "c + a <= c + b" by (simp add: order_le_less) have "a <= b" @@ -381,23 +388,23 @@ lemma add_less_cancel_left [simp]: "c + a < c + b \ a < b" - by (blast intro: add_less_imp_less_left add_strict_left_mono) +by (blast intro: add_less_imp_less_left add_strict_left_mono) lemma add_less_cancel_right [simp]: "a + c < b + c \ a < b" - by (blast intro: add_less_imp_less_right add_strict_right_mono) +by (blast intro: add_less_imp_less_right add_strict_right_mono) lemma add_le_cancel_left [simp]: "c + a \ c + b \ a \ b" - by (auto, drule add_le_imp_le_left, simp_all add: add_left_mono) +by (auto, drule add_le_imp_le_left, simp_all add: add_left_mono) lemma add_le_cancel_right [simp]: "a + c \ b + c \ a \ b" - by (simp add: add_commute [of a c] add_commute [of b c]) +by (simp add: add_commute [of a c] add_commute [of b c]) lemma add_le_imp_le_right: "a + c \ b + c \ a \ b" - by simp +by simp lemma max_add_distrib_left: "max x y + z = max (x + z) (y + z)" @@ -416,8 +423,7 @@ begin lemma add_pos_nonneg: - assumes "0 < a" and "0 \ b" - shows "0 < a + b" + assumes "0 < a" and "0 \ b" shows "0 < a + b" proof - have "0 + 0 < a + b" using assms by (rule add_less_le_mono) @@ -425,13 +431,11 @@ qed lemma add_pos_pos: - assumes "0 < a" and "0 < b" - shows "0 < a + b" - by (rule add_pos_nonneg) (insert assms, auto) + assumes "0 < a" and "0 < b" shows "0 < a + b" +by (rule add_pos_nonneg) (insert assms, auto) lemma add_nonneg_pos: - assumes "0 \ a" and "0 < b" - shows "0 < a + b" + assumes "0 \ a" and "0 < b" shows "0 < a + b" proof - have "0 + 0 < a + b" using assms by (rule add_le_less_mono) @@ -439,8 +443,7 @@ qed lemma add_nonneg_nonneg: - assumes "0 \ a" and "0 \ b" - shows "0 \ a + b" + assumes "0 \ a" and "0 \ b" shows "0 \ a + b" proof - have "0 + 0 \ a + b" using assms by (rule add_mono) @@ -448,8 +451,7 @@ qed lemma add_neg_nonpos: - assumes "a < 0" and "b \ 0" - shows "a + b < 0" + assumes "a < 0" and "b \ 0" shows "a + b < 0" proof - have "a + b < 0 + 0" using assms by (rule add_less_le_mono) @@ -457,13 +459,11 @@ qed lemma add_neg_neg: - assumes "a < 0" and "b < 0" - shows "a + b < 0" - by (rule add_neg_nonpos) (insert assms, auto) + assumes "a < 0" and "b < 0" shows "a + b < 0" +by (rule add_neg_nonpos) (insert assms, auto) lemma add_nonpos_neg: - assumes "a \ 0" and "b < 0" - shows "a + b < 0" + assumes "a \ 0" and "b < 0" shows "a + b < 0" proof - have "a + b < 0 + 0" using assms by (rule add_le_less_mono) @@ -471,8 +471,7 @@ qed lemma add_nonpos_nonpos: - assumes "a \ 0" and "b \ 0" - shows "a + b \ 0" + assumes "a \ 0" and "b \ 0" shows "a + b \ 0" proof - have "a + b \ 0 + 0" using assms by (rule add_mono) @@ -500,31 +499,25 @@ lemma max_diff_distrib_left: shows "max x y - z = max (x - z) (y - z)" - by (simp add: diff_minus, rule max_add_distrib_left) +by (simp add: diff_minus, rule max_add_distrib_left) lemma min_diff_distrib_left: shows "min x y - z = min (x - z) (y - z)" - by (simp add: diff_minus, rule min_add_distrib_left) +by (simp add: diff_minus, rule min_add_distrib_left) lemma le_imp_neg_le: - assumes "a \ b" - shows "-b \ -a" + assumes "a \ b" shows "-b \ -a" proof - - have "-a+a \ -a+b" - using `a \ b` by (rule add_left_mono) - hence "0 \ -a+b" - by simp - hence "0 + (-b) \ (-a + b) + (-b)" - by (rule add_right_mono) - thus ?thesis - by (simp add: add_assoc) + have "-a+a \ -a+b" using `a \ b` by (rule add_left_mono) + hence "0 \ -a+b" by simp + hence "0 + (-b) \ (-a + b) + (-b)" by (rule add_right_mono) + thus ?thesis by (simp add: add_assoc) qed lemma neg_le_iff_le [simp]: "- b \ - a \ a \ b" proof assume "- b \ - a" - hence "- (- a) \ - (- b)" - by (rule le_imp_neg_le) + hence "- (- a) \ - (- b)" by (rule le_imp_neg_le) thus "a\b" by simp next assume "a\b" @@ -532,19 +525,19 @@ qed lemma neg_le_0_iff_le [simp]: "- a \ 0 \ 0 \ a" - by (subst neg_le_iff_le [symmetric], simp) +by (subst neg_le_iff_le [symmetric], simp) lemma neg_0_le_iff_le [simp]: "0 \ - a \ a \ 0" - by (subst neg_le_iff_le [symmetric], simp) +by (subst neg_le_iff_le [symmetric], simp) lemma neg_less_iff_less [simp]: "- b < - a \ a < b" - by (force simp add: less_le) +by (force simp add: less_le) lemma neg_less_0_iff_less [simp]: "- a < 0 \ 0 < a" - by (subst neg_less_iff_less [symmetric], simp) +by (subst neg_less_iff_less [symmetric], simp) lemma neg_0_less_iff_less [simp]: "0 < - a \ a < 0" - by (subst neg_less_iff_less [symmetric], simp) +by (subst neg_less_iff_less [symmetric], simp) text{*The next several equations can make the simplifier loop!*} @@ -573,7 +566,7 @@ qed lemma minus_le_iff: "- a \ b \ - b \ a" - by (auto simp add: le_less minus_less_iff) +by (auto simp add: le_less minus_less_iff) lemma less_iff_diff_less_0: "a < b \ a - b < 0" proof - @@ -583,56 +576,34 @@ finally show ?thesis . qed -lemma diff_less_eq: "a - b < c \ a < c + b" +lemma diff_less_eq[algebra_simps]: "a - b < c \ a < c + b" apply (subst less_iff_diff_less_0 [of a]) apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst]) apply (simp add: diff_minus add_ac) done -lemma less_diff_eq: "a < c - b \ a + b < c" +lemma less_diff_eq[algebra_simps]: "a < c - b \ a + b < c" apply (subst less_iff_diff_less_0 [of "plus a b"]) apply (subst less_iff_diff_less_0 [of a]) apply (simp add: diff_minus add_ac) done -lemma diff_le_eq: "a - b \ c \ a \ c + b" - by (auto simp add: le_less diff_less_eq diff_add_cancel add_diff_cancel) - -lemma le_diff_eq: "a \ c - b \ a + b \ c" - by (auto simp add: le_less less_diff_eq diff_add_cancel add_diff_cancel) +lemma diff_le_eq[algebra_simps]: "a - b \ c \ a \ c + b" +by (auto simp add: le_less diff_less_eq diff_add_cancel add_diff_cancel) -lemmas compare_rls = - diff_minus [symmetric] - add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2 - diff_less_eq less_diff_eq diff_le_eq le_diff_eq - diff_eq_eq eq_diff_eq - -text{*This list of rewrites simplifies (in)equalities by bringing subtractions - to the top and then moving negative terms to the other side. - Use with @{text add_ac}*} -lemmas (in -) compare_rls = - diff_minus [symmetric] - add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2 - diff_less_eq less_diff_eq diff_le_eq le_diff_eq - diff_eq_eq eq_diff_eq +lemma le_diff_eq[algebra_simps]: "a \ c - b \ a + b \ c" +by (auto simp add: le_less less_diff_eq diff_add_cancel add_diff_cancel) lemma le_iff_diff_le_0: "a \ b \ a - b \ 0" - by (simp add: compare_rls) +by (simp add: algebra_simps) -lemmas group_simps = - add_ac - add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2 - diff_eq_eq eq_diff_eq diff_minus [symmetric] uminus_add_conv_diff - diff_less_eq less_diff_eq diff_le_eq le_diff_eq +text{*Legacy - use @{text algebra_simps} *} +lemmas group_simps = algebra_simps end -lemmas group_simps = - mult_ac - add_ac - add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2 - diff_eq_eq eq_diff_eq diff_minus [symmetric] uminus_add_conv_diff - diff_less_eq less_diff_eq diff_le_eq le_diff_eq +text{*Legacy - use @{text algebra_simps} *} +lemmas group_simps = algebra_simps class ordered_ab_semigroup_add = linorder + pordered_ab_semigroup_add @@ -766,8 +737,7 @@ unfolding neg_le_0_iff_le by simp lemma abs_of_nonneg [simp]: - assumes nonneg: "0 \ a" - shows "\a\ = a" + assumes nonneg: "0 \ a" shows "\a\ = a" proof (rule antisym) from nonneg le_imp_neg_le have "- a \ 0" by simp from this nonneg have "- a \ a" by (rule order_trans) @@ -775,8 +745,8 @@ qed (rule abs_ge_self) lemma abs_idempotent [simp]: "\\a\\ = \a\" - by (rule antisym) - (auto intro!: abs_ge_self abs_leI order_trans [of "uminus (abs a)" zero "abs a"]) +by (rule antisym) + (auto intro!: abs_ge_self abs_leI order_trans [of "uminus (abs a)" zero "abs a"]) lemma abs_eq_0 [simp]: "\a\ = 0 \ a = 0" proof - @@ -792,7 +762,7 @@ qed lemma abs_zero [simp]: "\0\ = 0" - by simp +by simp lemma abs_0_eq [simp, noatp]: "0 = \a\ \ a = 0" proof - @@ -811,7 +781,7 @@ qed lemma zero_less_abs_iff [simp]: "0 < \a\ \ a \ 0" - by (simp add: less_le) +by (simp add: less_le) lemma abs_not_less_zero [simp]: "\ \a\ < 0" proof - @@ -834,11 +804,10 @@ qed lemma abs_of_pos: "0 < a \ \a\ = a" - by (rule abs_of_nonneg, rule less_imp_le) +by (rule abs_of_nonneg, rule less_imp_le) lemma abs_of_nonpos [simp]: - assumes "a \ 0" - shows "\a\ = - a" + assumes "a \ 0" shows "\a\ = - a" proof - let ?b = "- a" have "- ?b \ 0 \ \- ?b\ = - (- ?b)" @@ -849,24 +818,24 @@ qed lemma abs_of_neg: "a < 0 \ \a\ = - a" - by (rule abs_of_nonpos, rule less_imp_le) +by (rule abs_of_nonpos, rule less_imp_le) lemma abs_le_D1: "\a\ \ b \ a \ b" - by (insert abs_ge_self, blast intro: order_trans) +by (insert abs_ge_self, blast intro: order_trans) lemma abs_le_D2: "\a\ \ b \ - a \ b" - by (insert abs_le_D1 [of "uminus a"], simp) +by (insert abs_le_D1 [of "uminus a"], simp) lemma abs_le_iff: "\a\ \ b \ a \ b \ - a \ b" - by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2) +by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2) lemma abs_triangle_ineq2: "\a\ - \b\ \ \a - b\" - apply (simp add: compare_rls) - apply (subgoal_tac "abs a = abs (plus (minus a b) b)") + apply (simp add: algebra_simps) + apply (subgoal_tac "abs a = abs (plus b (minus a b))") apply (erule ssubst) apply (rule abs_triangle_ineq) - apply (rule arg_cong) back - apply (simp add: compare_rls) + apply (rule arg_cong[of _ _ abs]) + apply (simp add: algebra_simps) done lemma abs_triangle_ineq3: "\\a\ - \b\\ \ \a - b\" @@ -879,12 +848,9 @@ lemma abs_triangle_ineq4: "\a - b\ \ \a\ + \b\" proof - - have "abs(a - b) = abs(a + - b)" - by (subst diff_minus, rule refl) - also have "... <= abs a + abs (- b)" - by (rule abs_triangle_ineq) - finally show ?thesis - by simp + have "abs(a - b) = abs(a + - b)" by (subst diff_minus, rule refl) + also have "... <= abs a + abs (- b)" by (rule abs_triangle_ineq) + finally show ?thesis by simp qed lemma abs_diff_triangle_ineq: "\a + b - (c + d)\ \ \a - c\ + \b - d\" @@ -999,23 +965,19 @@ qed lemma neg_inf_eq_sup: "- inf a b = sup (-a) (-b)" - by (simp add: inf_eq_neg_sup) +by (simp add: inf_eq_neg_sup) lemma neg_sup_eq_inf: "- sup a b = inf (-a) (-b)" - by (simp add: sup_eq_neg_inf) +by (simp add: sup_eq_neg_inf) lemma add_eq_inf_sup: "a + b = sup a b + inf a b" proof - have "0 = - inf 0 (a-b) + inf (a-b) 0" by (simp add: inf_commute) hence "0 = sup 0 (b-a) + inf (a-b) 0" by (simp add: inf_eq_neg_sup) hence "0 = (-a + sup a b) + (inf a b + (-b))" - apply (simp add: add_sup_distrib_left add_inf_distrib_right) - by (simp add: diff_minus add_commute) - thus ?thesis - apply (simp add: compare_rls) - apply (subst add_left_cancel [symmetric, of "plus a b" "plus (sup a b) (inf a b)" "uminus a"]) - apply (simp only: add_assoc, simp add: add_assoc[symmetric]) - done + by (simp add: add_sup_distrib_left add_inf_distrib_right) + (simp add: algebra_simps) + thus ?thesis by (simp add: algebra_simps) qed subsection {* Positive Part, Negative Part, Absolute Value *} @@ -1044,13 +1006,13 @@ qed lemma prts: "a = pprt a + nprt a" - by (simp add: pprt_def nprt_def add_eq_inf_sup[symmetric]) +by (simp add: pprt_def nprt_def add_eq_inf_sup[symmetric]) lemma zero_le_pprt[simp]: "0 \ pprt a" - by (simp add: pprt_def) +by (simp add: pprt_def) lemma nprt_le_zero[simp]: "nprt a \ 0" - by (simp add: nprt_def) +by (simp add: nprt_def) lemma le_eq_neg: "a \ - b \ a + b \ 0" (is "?l = ?r") proof - @@ -1071,16 +1033,16 @@ lemma nprt_0[simp]: "nprt 0 = 0" by (simp add: nprt_def) lemma pprt_eq_id [simp, noatp]: "0 \ x \ pprt x = x" - by (simp add: pprt_def le_iff_sup sup_ACI) +by (simp add: pprt_def le_iff_sup sup_ACI) lemma nprt_eq_id [simp, noatp]: "x \ 0 \ nprt x = x" - by (simp add: nprt_def le_iff_inf inf_ACI) +by (simp add: nprt_def le_iff_inf inf_ACI) lemma pprt_eq_0 [simp, noatp]: "x \ 0 \ pprt x = 0" - by (simp add: pprt_def le_iff_sup sup_ACI) +by (simp add: pprt_def le_iff_sup sup_ACI) lemma nprt_eq_0 [simp, noatp]: "0 \ x \ nprt x = 0" - by (simp add: nprt_def le_iff_inf inf_ACI) +by (simp add: nprt_def le_iff_inf inf_ACI) lemma sup_0_imp_0: "sup a (- a) = 0 \ a = 0" proof - @@ -1105,10 +1067,10 @@ done lemma inf_0_eq_0 [simp, noatp]: "inf a (- a) = 0 \ a = 0" - by (rule, erule inf_0_imp_0) simp +by (rule, erule inf_0_imp_0) simp lemma sup_0_eq_0 [simp, noatp]: "sup a (- a) = 0 \ a = 0" - by (rule, erule sup_0_imp_0) simp +by (rule, erule sup_0_imp_0) simp lemma zero_le_double_add_iff_zero_le_single_add [simp]: "0 \ a + a \ 0 \ a" @@ -1190,22 +1152,22 @@ qed lemma zero_le_iff_zero_nprt: "0 \ a \ nprt a = 0" - by (simp add: le_iff_inf nprt_def inf_commute) +by (simp add: le_iff_inf nprt_def inf_commute) lemma le_zero_iff_zero_pprt: "a \ 0 \ pprt a = 0" - by (simp add: le_iff_sup pprt_def sup_commute) +by (simp add: le_iff_sup pprt_def sup_commute) lemma le_zero_iff_pprt_id: "0 \ a \ pprt a = a" - by (simp add: le_iff_sup pprt_def sup_commute) +by (simp add: le_iff_sup pprt_def sup_commute) lemma zero_le_iff_nprt_id: "a \ 0 \ nprt a = a" - by (simp add: le_iff_inf nprt_def inf_commute) +by (simp add: le_iff_inf nprt_def inf_commute) lemma pprt_mono [simp, noatp]: "a \ b \ pprt a \ pprt b" - by (simp add: le_iff_sup pprt_def sup_ACI sup_assoc [symmetric, of a]) +by (simp add: le_iff_sup pprt_def sup_ACI sup_assoc [symmetric, of a]) lemma nprt_mono [simp, noatp]: "a \ b \ nprt a \ nprt b" - by (simp add: le_iff_inf nprt_def inf_ACI inf_assoc [symmetric, of a]) +by (simp add: le_iff_inf nprt_def inf_ACI inf_assoc [symmetric, of a]) end @@ -1246,12 +1208,10 @@ show "0 \ \a\" by simp next fix a - show "a \ \a\" - by (auto simp add: abs_lattice) + show "a \ \a\" by (auto simp add: abs_lattice) next fix a - show "\-a\ = \a\" - by (simp add: abs_lattice sup_commute) + show "\-a\ = \a\" by (simp add: abs_lattice sup_commute) next fix a b show "a \ b \ - a \ b \ \a\ \ b" by (erule abs_leI) @@ -1266,8 +1226,7 @@ have c:"?n <= sup ?m ?n" by (simp) from b c have d: "-a-b <= sup ?m ?n" by(rule order_trans) have e:"-a-b = -(a+b)" by (simp add: diff_minus) - from a d e have "abs(a+b) <= sup ?m ?n" - by (drule_tac abs_leI, auto) + from a d e have "abs(a+b) <= sup ?m ?n" by (drule_tac abs_leI, auto) with g[symmetric] show ?thesis by simp qed qed auto @@ -1287,7 +1246,7 @@ lemma abs_if_lattice: fixes a :: "'a\{lordered_ab_group_add_abs, linorder}" shows "\a\ = (if a < 0 then - a else a)" - by auto +by auto text {* Needed for abelian cancellation simprocs: *} @@ -1333,7 +1292,7 @@ "a + b <= (c::'a::lordered_ab_group_add_abs) \ a <= c + abs b" proof - assume "a+b <= c" - hence 2: "a <= c+(-b)" by (simp add: group_simps) + hence 2: "a <= c+(-b)" by (simp add: algebra_simps) have 3: "(-b) <= abs b" by (rule abs_ge_minus_self) show ?thesis by (rule le_add_right_mono[OF 2 3]) qed diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/PReal.thy --- a/src/HOL/PReal.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/PReal.thy Wed Jan 28 16:29:16 2009 +0100 @@ -718,7 +718,7 @@ case (Suc k) from this obtain b where "b \ A" "b + of_nat k * u \ A" .. hence "b + of_int (int k)*u + u \ A" by (simp add: prems) - thus ?case by (force simp add: left_distrib add_ac prems) + thus ?case by (force simp add: algebra_simps prems) qed next case (neg n) @@ -815,7 +815,7 @@ proof - have "r + ?d < r + (r * ?d)/y" by (simp add: dless) also with ypos have "... = (r/y) * (y + ?d)" - by (simp only: right_distrib divide_inverse mult_ac, simp) + by (simp only: algebra_simps divide_inverse, simp) also have "... = r*x" using ypos by (simp add: times_divide_eq_left) finally show "r + ?d < r*x" . diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/Polynomial.thy --- a/src/HOL/Polynomial.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/Polynomial.thy Wed Jan 28 16:29:16 2009 +0100 @@ -442,11 +442,11 @@ lemma smult_add_right: "smult a (p + q) = smult a p + smult a q" - by (rule poly_ext, simp add: ring_simps) + by (rule poly_ext, simp add: algebra_simps) lemma smult_add_left: "smult (a + b) p = smult a p + smult b p" - by (rule poly_ext, simp add: ring_simps) + by (rule poly_ext, simp add: algebra_simps) lemma smult_minus_right [simp]: "smult (a::'a::comm_ring) (- p) = - smult a p" @@ -458,11 +458,11 @@ lemma smult_diff_right: "smult (a::'a::comm_ring) (p - q) = smult a p - smult a q" - by (rule poly_ext, simp add: ring_simps) + by (rule poly_ext, simp add: algebra_simps) lemma smult_diff_left: "smult (a - b::'a::comm_ring) p = smult a p - smult b p" - by (rule poly_ext, simp add: ring_simps) + by (rule poly_ext, simp add: algebra_simps) lemmas smult_distribs = smult_add_left smult_add_right @@ -517,7 +517,7 @@ lemma mult_pCons_right [simp]: "p * pCons a q = smult a p + pCons 0 (p * q)" - by (induct p, simp add: mult_poly_0_left, simp add: ring_simps) + by (induct p, simp add: mult_poly_0_left, simp add: algebra_simps) lemmas mult_poly_0 = mult_poly_0_left mult_poly_0_right @@ -531,7 +531,7 @@ fixes p q r :: "'a poly" shows "(p + q) * r = p * r + q * r" by (induct r, simp add: mult_poly_0, - simp add: smult_distribs group_simps) + simp add: smult_distribs algebra_simps) instance proof fix p q r :: "'a poly" @@ -758,7 +758,7 @@ from 2 have q2: "x = q2 * y + r2" and r2: "r2 = 0 \ degree r2 < degree y" unfolding pdivmod_rel_def by simp_all from q1 q2 have q3: "(q1 - q2) * y = r2 - r1" - by (simp add: ring_simps) + by (simp add: algebra_simps) from r1 r2 have r3: "(r2 - r1) = 0 \ degree (r2 - r1) < degree y" by (auto intro: degree_diff_less) @@ -894,7 +894,7 @@ lemma poly_add [simp]: "poly (p + q) x = poly p x + poly q x" apply (induct p arbitrary: q, simp) - apply (case_tac q, simp, simp add: ring_simps) + apply (case_tac q, simp, simp add: algebra_simps) done lemma poly_minus [simp]: @@ -911,10 +911,10 @@ by (cases "finite A", induct set: finite, simp_all) lemma poly_smult [simp]: "poly (smult a p) x = a * poly p x" - by (induct p, simp, simp add: ring_simps) + by (induct p, simp, simp add: algebra_simps) lemma poly_mult [simp]: "poly (p * q) x = poly p x * poly q x" - by (induct p, simp_all, simp add: ring_simps) + by (induct p, simp_all, simp add: algebra_simps) lemma poly_power [simp]: fixes p :: "'a::{comm_semiring_1,recpower} poly" @@ -983,7 +983,7 @@ fixes c :: "'a::comm_ring_1" shows "[:-c, 1:] * synthetic_div p c + [:poly p c:] = p" using synthetic_div_correct [of p c] - by (simp add: group_simps) + by (simp add: algebra_simps) lemma poly_eq_0_iff_dvd: fixes c :: "'a::idom" diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/Presburger.thy --- a/src/HOL/Presburger.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/Presburger.thy Wed Jan 28 16:29:16 2009 +0100 @@ -59,7 +59,7 @@ "(d::'a::{comm_ring,Ring_and_Field.dvd}) dvd D \ \x k. (d dvd x + t) = (d dvd (x - k*D) + t)" "(d::'a::{comm_ring,Ring_and_Field.dvd}) dvd D \ \x k. (\d dvd x + t) = (\d dvd (x - k*D) + t)" "\x k. F = F" -apply (auto elim!: dvdE simp add: ring_simps) +apply (auto elim!: dvdE simp add: algebra_simps) unfolding mult_assoc [symmetric] left_distrib [symmetric] left_diff_distrib [symmetric] unfolding dvd_def mult_commute [of d] by auto @@ -101,7 +101,7 @@ {fix x assume nob: "\j\{1 .. D}. \b\B. x \ b + j" and g: "x > t" and ng: "\ (x - D) > t" hence "x -t \ D" and "1 \ x - t" by simp+ hence "\j \ {1 .. D}. x - t = j" by auto - hence "\j \ {1 .. D}. x = t + j" by (simp add: ring_simps) + hence "\j \ {1 .. D}. x = t + j" by (simp add: algebra_simps) with nob tB have "False" by simp} thus "\x.(\j\{1 .. D}. \b\B. x \ b + j)\ (x > t) \ (x - D > t)" by blast next @@ -109,7 +109,7 @@ {fix x assume nob: "\j\{1 .. D}. \b\B. x \ b + j" and g: "x \ t" and ng: "\ (x - D) \ t" hence "x - (t - 1) \ D" and "1 \ x - (t - 1)" by simp+ hence "\j \ {1 .. D}. x - (t - 1) = j" by auto - hence "\j \ {1 .. D}. x = (t - 1) + j" by (simp add: ring_simps) + hence "\j \ {1 .. D}. x = (t - 1) + j" by (simp add: algebra_simps) with nob tB have "False" by simp} thus "\x.(\j\{1 .. D}. \b\B. x \ b + j)\ (x \ t) \ (x - D \ t)" by blast next @@ -119,7 +119,7 @@ next assume d: "d dvd D" {fix x assume H: "\(d dvd x + t)" with d have "\ d dvd (x - D) + t" - by (clarsimp simp add: dvd_def,erule_tac x= "ka + k" in allE,simp add: ring_simps)} + by (clarsimp simp add: dvd_def,erule_tac x= "ka + k" in allE,simp add: algebra_simps)} thus "\(x::int).(\j\{1 .. D}. \b\B. x \ b + j)\ (\d dvd x+t) \ (\d dvd (x - D) + t)" by auto qed blast @@ -158,26 +158,26 @@ {fix x assume nob: "\j\{1 .. D}. \b\A. x \ b - j" and g: "x < t" and ng: "\ (x + D) < t" hence "t - x \ D" and "1 \ t - x" by simp+ hence "\j \ {1 .. D}. t - x = j" by auto - hence "\j \ {1 .. D}. x = t - j" by (auto simp add: ring_simps) + hence "\j \ {1 .. D}. x = t - j" by (auto simp add: algebra_simps) with nob tA have "False" by simp} thus "\x.(\j\{1 .. D}. \b\A. x \ b - j)\ (x < t) \ (x + D < t)" by blast next assume dp: "D > 0" and tA:"t + 1\ A" {fix x assume nob: "\j\{1 .. D}. \b\A. x \ b - j" and g: "x \ t" and ng: "\ (x + D) \ t" - hence "(t + 1) - x \ D" and "1 \ (t + 1) - x" by (simp_all add: ring_simps) + hence "(t + 1) - x \ D" and "1 \ (t + 1) - x" by (simp_all add: algebra_simps) hence "\j \ {1 .. D}. (t + 1) - x = j" by auto - hence "\j \ {1 .. D}. x = (t + 1) - j" by (auto simp add: ring_simps) + hence "\j \ {1 .. D}. x = (t + 1) - j" by (auto simp add: algebra_simps) with nob tA have "False" by simp} thus "\x.(\j\{1 .. D}. \b\A. x \ b - j)\ (x \ t) \ (x + D \ t)" by blast next assume d: "d dvd D" {fix x assume H: "d dvd x + t" with d have "d dvd (x + D) + t" - by (clarsimp simp add: dvd_def,rule_tac x= "ka + k" in exI,simp add: ring_simps)} + by (clarsimp simp add: dvd_def,rule_tac x= "ka + k" in exI,simp add: algebra_simps)} thus "\(x::int).(\j\{1 .. D}. \b\A. x \ b - j)\ (d dvd x+t) \ (d dvd (x + D) + t)" by simp next assume d: "d dvd D" {fix x assume H: "\(d dvd x + t)" with d have "\d dvd (x + D) + t" - by (clarsimp simp add: dvd_def,erule_tac x= "ka - k" in allE,simp add: ring_simps)} + by (clarsimp simp add: dvd_def,erule_tac x= "ka - k" in allE,simp add: algebra_simps)} thus "\(x::int).(\j\{1 .. D}. \b\A. x \ b - j)\ (\d dvd x+t) \ (\d dvd (x + D) + t)" by auto qed blast @@ -304,7 +304,7 @@ from ePeqP1 obtain z where P1eqP: "\x>z. P x = P' x" .. let ?w' = "x + (abs(x-z)+1) * d" let ?w = "x - (-(abs(x-z) + 1))*d" - have ww'[simp]: "?w = ?w'" by (simp add: ring_simps) + have ww'[simp]: "?w = ?w'" by (simp add: algebra_simps) from dpos have w: "?w > z" by(simp only: ww' incr_lemma) hence "P' x = P' ?w" using P1eqP1 by blast also have "\ = P(?w)" using w P1eqP by blast diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/RComplete.thy --- a/src/HOL/RComplete.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/RComplete.thy Wed Jan 28 16:29:16 2009 +0100 @@ -376,7 +376,7 @@ hence "real (Suc n) * (inverse (real (Suc n)) * x) < real (Suc n) * 1" by (rule mult_strict_left_mono) simp hence "x < real (Suc n)" - by (simp add: ring_simps) + by (simp add: algebra_simps) thus "\(n::nat). x < real n" .. qed @@ -391,9 +391,9 @@ hence "y * inverse x * x < real n * x" using x_greater_zero by (simp add: mult_strict_right_mono) hence "x * inverse x * y < x * real n" - by (simp add: ring_simps) + by (simp add: algebra_simps) hence "y < real (n::nat) * x" - using x_not_zero by (simp add: ring_simps) + using x_not_zero by (simp add: algebra_simps) thus "\(n::nat). y < real n * x" .. qed @@ -1084,9 +1084,7 @@ done lemma real_natfloor_gt_diff_one: "x - 1 < real(natfloor x)" - apply (simp add: compare_rls) - apply (rule real_natfloor_add_one_gt) -done +using real_natfloor_add_one_gt by (simp add: algebra_simps) lemma ge_natfloor_plus_one_imp_gt: "natfloor z + 1 <= n ==> z < real n" apply (subgoal_tac "z < real(natfloor z) + 1") @@ -1279,7 +1277,7 @@ by simp also have "... = real((natfloor x) div y) + real((natfloor x) mod y) / real y + (x - real(natfloor x)) / real y" - by (auto simp add: ring_simps add_divide_distrib + by (auto simp add: algebra_simps add_divide_distrib diff_divide_distrib prems) finally have "natfloor (x / real y) = natfloor(...)" by simp also have "... = natfloor(real((natfloor x) mod y) / @@ -1293,7 +1291,7 @@ apply simp apply (simp add: prems) apply (rule divide_nonneg_pos) - apply (simp add: compare_rls) + apply (simp add: algebra_simps) apply (rule real_natfloor_le) apply (insert prems, auto) done @@ -1306,7 +1304,7 @@ apply force apply (force simp add: prems) apply (rule divide_nonneg_pos) - apply (simp add: compare_rls) + apply (simp add: algebra_simps) apply (rule real_natfloor_le) apply (auto simp add: prems) apply (insert prems, arith) @@ -1314,8 +1312,8 @@ apply (subgoal_tac "real y = real y - 1 + 1") apply (erule ssubst) apply (rule add_le_less_mono) - apply (simp add: compare_rls) - apply (subgoal_tac "real(natfloor x mod y) + 1 = + apply (simp add: algebra_simps) + apply (subgoal_tac "1 + real(natfloor x mod y) = real(natfloor x mod y + 1)") apply (erule ssubst) apply (subst real_of_nat_le_iff) @@ -1323,9 +1321,8 @@ apply arith apply (rule mod_less_divisor) apply auto - apply (simp add: compare_rls) - apply (subst add_commute) - apply (rule real_natfloor_add_one_gt) + using real_natfloor_add_one_gt + apply (simp add: algebra_simps) done finally show ?thesis by simp qed diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/Rational.thy --- a/src/HOL/Rational.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/Rational.thy Wed Jan 28 16:29:16 2009 +0100 @@ -172,7 +172,7 @@ by (cases q) (simp add: One_rat_def eq_rat) next fix q r s :: rat show "(q + r) + s = q + (r + s)" - by (cases q, cases r, cases s) (simp add: eq_rat ring_simps) + by (cases q, cases r, cases s) (simp add: eq_rat algebra_simps) next fix q r :: rat show "q + r = r + q" by (cases q, cases r) (simp add: eq_rat) @@ -187,7 +187,7 @@ by (cases q, cases r) (simp add: eq_rat) next fix q r s :: rat show "(q + r) * s = q * s + r * s" - by (cases q, cases r, cases s) (simp add: eq_rat ring_simps) + by (cases q, cases r, cases s) (simp add: eq_rat algebra_simps) next show "(0::rat) \ 1" by (simp add: Zero_rat_def One_rat_def eq_rat) next diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/RealDef.thy --- a/src/HOL/RealDef.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/RealDef.thy Wed Jan 28 16:29:16 2009 +0100 @@ -202,18 +202,17 @@ lemma real_mult_assoc: "((z1::real) * z2) * z3 = z1 * (z2 * z3)" apply (cases z1, cases z2, cases z3) -apply (simp add: real_mult right_distrib add_ac mult_ac) +apply (simp add: real_mult algebra_simps) done lemma real_mult_1: "(1::real) * z = z" apply (cases z) -apply (simp add: real_mult real_one_def right_distrib - mult_1_right mult_ac add_ac) +apply (simp add: real_mult real_one_def algebra_simps) done lemma real_add_mult_distrib: "((z1::real) + z2) * w = (z1 * w) + (z2 * w)" apply (cases z1, cases z2, cases w) -apply (simp add: real_add real_mult right_distrib add_ac mult_ac) +apply (simp add: real_add real_mult algebra_simps) done text{*one and zero are distinct*} @@ -253,7 +252,7 @@ apply (rule_tac [2] x = "Abs_Real (realrel``{(inverse (D) + 1, 1)})" in exI) -apply (auto simp add: real_mult preal_mult_inverse_right ring_simps) +apply (auto simp add: real_mult preal_mult_inverse_right algebra_simps) done lemma real_mult_inverse_left: "x \ 0 ==> inverse(x)*x = (1::real)" @@ -373,7 +372,7 @@ assumes le: "x \ y" shows "z + x \ z + (y::real)" proof - have "z + x - (z + y) = (z + -z) + (x - y)" - by (simp add: diff_minus add_ac) + by (simp add: algebra_simps) with le show ?thesis by (simp add: real_le_eq_diff[of x] real_le_eq_diff[of "z+x"] diff_minus) qed @@ -391,8 +390,7 @@ real_zero_def real_le real_mult) --{*Reduce to the (simpler) @{text "\"} relation *} apply (auto dest!: less_add_left_Ex - simp add: add_ac mult_ac - right_distrib preal_self_less_add_left) + simp add: algebra_simps preal_self_less_add_left) done lemma real_mult_less_mono2: "[| (0::real) < z; x < y |] ==> z * x < z * y" @@ -437,11 +435,11 @@ lemma real_of_preal_add: "real_of_preal ((x::preal) + y) = real_of_preal x + real_of_preal y" -by (simp add: real_of_preal_def real_add left_distrib add_ac) +by (simp add: real_of_preal_def real_add algebra_simps) lemma real_of_preal_mult: "real_of_preal ((x::preal) * y) = real_of_preal x* real_of_preal y" -by (simp add: real_of_preal_def real_mult right_distrib add_ac mult_ac) +by (simp add: real_of_preal_def real_mult algebra_simps) text{*Gleason prop 9-4.4 p 127*} @@ -650,7 +648,7 @@ then have "real x / real d = ... / real d" by simp then show ?thesis - by (auto simp add: add_divide_distrib ring_simps prems) + by (auto simp add: add_divide_distrib algebra_simps prems) qed lemma real_of_int_div: "(d::int) ~= 0 ==> d dvd n ==> @@ -665,13 +663,13 @@ apply (case_tac "x = 0") apply simp apply (case_tac "0 < x") - apply (simp add: compare_rls) + apply (simp add: algebra_simps) apply (subst real_of_int_div_aux) apply simp apply simp apply (subst zero_le_divide_iff) apply auto - apply (simp add: compare_rls) + apply (simp add: algebra_simps) apply (subst real_of_int_div_aux) apply simp apply simp @@ -683,7 +681,7 @@ "real (n::int) / real (x) - real (n div x) <= 1" apply(case_tac "x = 0") apply simp - apply (simp add: compare_rls) + apply (simp add: algebra_simps) apply (subst real_of_int_div_aux) apply assumption apply simp @@ -795,7 +793,7 @@ then have "real x / real d = \ / real d" by simp then show ?thesis - by (auto simp add: add_divide_distrib ring_simps prems) + by (auto simp add: add_divide_distrib algebra_simps prems) qed lemma real_of_nat_div: "0 < (d::nat) ==> d dvd n ==> @@ -810,7 +808,7 @@ "0 <= real (n::nat) / real (x) - real (n div x)" apply(case_tac "x = 0") apply (simp) -apply (simp add: compare_rls) +apply (simp add: algebra_simps) apply (subst real_of_nat_div_aux) apply simp apply simp @@ -822,14 +820,14 @@ "real (n::nat) / real (x) - real (n div x) <= 1" apply(case_tac "x = 0") apply (simp) -apply (simp add: compare_rls) +apply (simp add: algebra_simps) apply (subst real_of_nat_div_aux) apply simp apply simp done lemma real_of_nat_div4: "real (n div x) <= real (n::nat) / real x" - by (insert real_of_nat_div2 [of n x], simp) +by (insert real_of_nat_div2 [of n x], simp) lemma real_of_int_real_of_nat: "real (int n) = real n" by (simp add: real_of_nat_def real_of_int_def int_eq_of_nat) diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/RealPow.thy --- a/src/HOL/RealPow.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/RealPow.thy Wed Jan 28 16:29:16 2009 +0100 @@ -58,7 +58,7 @@ lemma realpow_two_diff: "(x::real)^Suc (Suc 0) - y^Suc (Suc 0) = (x - y) * (x + y)" apply (unfold real_diff_def) -apply (simp add: ring_simps) +apply (simp add: algebra_simps) done lemma realpow_two_disj: diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/Ring_and_Field.thy --- a/src/HOL/Ring_and_Field.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/Ring_and_Field.thy Wed Jan 28 16:29:16 2009 +0100 @@ -24,14 +24,14 @@ *} class semiring = ab_semigroup_add + semigroup_mult + - assumes left_distrib: "(a + b) * c = a * c + b * c" - assumes right_distrib: "a * (b + c) = a * b + a * c" + assumes left_distrib[algebra_simps]: "(a + b) * c = a * c + b * c" + assumes right_distrib[algebra_simps]: "a * (b + c) = a * b + a * c" begin text{*For the @{text combine_numerals} simproc*} lemma combine_common_factor: "a * e + (b * e + c) = (a + b) * e + c" - by (simp add: left_distrib add_ac) +by (simp add: left_distrib add_ac) end @@ -47,16 +47,12 @@ subclass semiring_0 proof fix a :: 'a - have "0 * a + 0 * a = 0 * a + 0" - by (simp add: left_distrib [symmetric]) - thus "0 * a = 0" - by (simp only: add_left_cancel) + have "0 * a + 0 * a = 0 * a + 0" by (simp add: left_distrib [symmetric]) + thus "0 * a = 0" by (simp only: add_left_cancel) next fix a :: 'a - have "a * 0 + a * 0 = a * 0 + 0" - by (simp add: right_distrib [symmetric]) - thus "a * 0 = 0" - by (simp only: add_left_cancel) + have "a * 0 + a * 0 = a * 0 + 0" by (simp add: right_distrib [symmetric]) + thus "a * 0 = 0" by (simp only: add_left_cancel) qed end @@ -98,7 +94,7 @@ begin lemma one_neq_zero [simp]: "1 \ 0" - by (rule not_sym) (rule zero_neq_one) +by (rule not_sym) (rule zero_neq_one) end @@ -142,7 +138,7 @@ qed lemma dvd_0_left_iff [noatp, simp]: "0 dvd a \ a = 0" - by (auto intro: dvd_refl elim!: dvdE) +by (auto intro: dvd_refl elim!: dvdE) lemma dvd_0_right [iff]: "a dvd 0" proof @@ -150,10 +146,10 @@ qed lemma one_dvd [simp]: "1 dvd a" - by (auto intro!: dvdI) +by (auto intro!: dvdI) lemma dvd_mult: "a dvd c \ a dvd (b * c)" - by (auto intro!: mult_left_commute dvdI elim!: dvdE) +by (auto intro!: mult_left_commute dvdI elim!: dvdE) lemma dvd_mult2: "a dvd b \ a dvd (b * c)" apply (subst mult_commute) @@ -161,10 +157,10 @@ done lemma dvd_triv_right [simp]: "a dvd b * a" - by (rule dvd_mult) (rule dvd_refl) +by (rule dvd_mult) (rule dvd_refl) lemma dvd_triv_left [simp]: "a dvd a * b" - by (rule dvd_mult2) (rule dvd_refl) +by (rule dvd_mult2) (rule dvd_refl) lemma mult_dvd_mono: assumes ab: "a dvd b" @@ -178,13 +174,13 @@ qed lemma dvd_mult_left: "a * b dvd c \ a dvd c" - by (simp add: dvd_def mult_assoc, blast) +by (simp add: dvd_def mult_assoc, blast) lemma dvd_mult_right: "a * b dvd c \ b dvd c" unfolding mult_ac [of a] by (rule dvd_mult_left) lemma dvd_0_left: "0 dvd a \ a = 0" - by simp +by simp lemma dvd_add: assumes ab: "a dvd b" @@ -230,43 +226,40 @@ text {* Distribution rules *} lemma minus_mult_left: "- (a * b) = - a * b" - by (rule equals_zero_I) (simp add: left_distrib [symmetric]) +by (rule equals_zero_I) (simp add: left_distrib [symmetric]) lemma minus_mult_right: "- (a * b) = a * - b" - by (rule equals_zero_I) (simp add: right_distrib [symmetric]) +by (rule equals_zero_I) (simp add: right_distrib [symmetric]) text{*Extract signs from products*} lemmas mult_minus_left [simp] = minus_mult_left [symmetric] lemmas mult_minus_right [simp] = minus_mult_right [symmetric] lemma minus_mult_minus [simp]: "- a * - b = a * b" - by simp +by simp lemma minus_mult_commute: "- a * b = a * - b" - by simp - -lemma right_diff_distrib: "a * (b - c) = a * b - a * c" - by (simp add: right_distrib diff_minus) - -lemma left_diff_distrib: "(a - b) * c = a * c - b * c" - by (simp add: left_distrib diff_minus) +by simp + +lemma right_diff_distrib[algebra_simps]: "a * (b - c) = a * b - a * c" +by (simp add: right_distrib diff_minus) + +lemma left_diff_distrib[algebra_simps]: "(a - b) * c = a * c - b * c" +by (simp add: left_distrib diff_minus) lemmas ring_distribs = right_distrib left_distrib left_diff_distrib right_diff_distrib -lemmas ring_simps = - add_ac - add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2 - diff_eq_eq eq_diff_eq diff_minus [symmetric] uminus_add_conv_diff - ring_distribs +text{*Legacy - use @{text algebra_simps} *} +lemmas ring_simps = algebra_simps lemma eq_add_iff1: "a * e + c = b * e + d \ (a - b) * e + c = d" - by (simp add: ring_simps) +by (simp add: algebra_simps) lemma eq_add_iff2: "a * e + c = b * e + d \ c = (b - a) * e + d" - by (simp add: ring_simps) +by (simp add: algebra_simps) end @@ -320,7 +313,7 @@ qed lemma dvd_diff: "x dvd y \ x dvd z \ x dvd (y - z)" - by (simp add: diff_minus dvd_add dvd_minus_iff) +by (simp add: diff_minus dvd_add dvd_minus_iff) end @@ -341,18 +334,16 @@ "a * c = b * c \ c = 0 \ a = b" proof - have "(a * c = b * c) = ((a - b) * c = 0)" - by (simp add: ring_distribs right_minus_eq) - thus ?thesis - by (simp add: disj_commute right_minus_eq) + by (simp add: algebra_simps right_minus_eq) + thus ?thesis by (simp add: disj_commute right_minus_eq) qed lemma mult_cancel_left [simp, noatp]: "c * a = c * b \ c = 0 \ a = b" proof - have "(c * a = c * b) = (c * (a - b) = 0)" - by (simp add: ring_distribs right_minus_eq) - thus ?thesis - by (simp add: right_minus_eq) + by (simp add: algebra_simps right_minus_eq) + thus ?thesis by (simp add: right_minus_eq) qed end @@ -362,19 +353,19 @@ lemma mult_cancel_right1 [simp]: "c = b * c \ c = 0 \ b = 1" - by (insert mult_cancel_right [of 1 c b], force) +by (insert mult_cancel_right [of 1 c b], force) lemma mult_cancel_right2 [simp]: "a * c = c \ c = 0 \ a = 1" - by (insert mult_cancel_right [of a c 1], simp) +by (insert mult_cancel_right [of a c 1], simp) lemma mult_cancel_left1 [simp]: "c = c * b \ c = 0 \ b = 1" - by (insert mult_cancel_left [of c 1 b], force) +by (insert mult_cancel_left [of c 1 b], force) lemma mult_cancel_left2 [simp]: "c * a = c \ c = 0 \ a = 1" - by (insert mult_cancel_left [of c a 1], simp) +by (insert mult_cancel_left [of c a 1], simp) end @@ -397,14 +388,11 @@ show "a * b \ 0" proof assume ab: "a * b = 0" - hence "0 = inverse a * (a * b) * inverse b" - by simp + hence "0 = inverse a * (a * b) * inverse b" by simp also have "\ = (inverse a * a) * (b * inverse b)" by (simp only: mult_assoc) - also have "\ = 1" - using a b by simp - finally show False - by simp + also have "\ = 1" using a b by simp + finally show False by simp qed qed @@ -437,45 +425,41 @@ lemma nonzero_inverse_minus_eq: "a \ 0 \ inverse (- a) = - inverse a" - by (rule inverse_unique) simp +by (rule inverse_unique) simp lemma nonzero_inverse_inverse_eq: "a \ 0 \ inverse (inverse a) = a" - by (rule inverse_unique) simp +by (rule inverse_unique) simp lemma nonzero_inverse_eq_imp_eq: assumes "inverse a = inverse b" and "a \ 0" and "b \ 0" shows "a = b" proof - from `inverse a = inverse b` - have "inverse (inverse a) = inverse (inverse b)" - by (rule arg_cong) + have "inverse (inverse a) = inverse (inverse b)" by (rule arg_cong) with `a \ 0` and `b \ 0` show "a = b" by (simp add: nonzero_inverse_inverse_eq) qed lemma inverse_1 [simp]: "inverse 1 = 1" - by (rule inverse_unique) simp +by (rule inverse_unique) simp lemma nonzero_inverse_mult_distrib: assumes "a \ 0" and "b \ 0" shows "inverse (a * b) = inverse b * inverse a" proof - - have "a * (b * inverse b) * inverse a = 1" - using assms by simp - hence "a * b * (inverse b * inverse a) = 1" - by (simp only: mult_assoc) - thus ?thesis - by (rule inverse_unique) + have "a * (b * inverse b) * inverse a = 1" using assms by simp + hence "a * b * (inverse b * inverse a) = 1" by (simp only: mult_assoc) + thus ?thesis by (rule inverse_unique) qed lemma division_ring_inverse_add: "a \ 0 \ b \ 0 \ inverse a + inverse b = inverse a * (a + b) * inverse b" - by (simp add: ring_simps mult_assoc) +by (simp add: algebra_simps) lemma division_ring_inverse_diff: "a \ 0 \ b \ 0 \ inverse a - inverse b = inverse a * (b - a) * inverse b" - by (simp add: ring_simps mult_assoc) +by (simp add: algebra_simps) end @@ -508,19 +492,19 @@ qed lemma nonzero_inverse_eq_divide: "a \ 0 \ inverse a = 1 / a" - by (simp add: divide_inverse) +by (simp add: divide_inverse) lemma divide_self [simp]: "a \ 0 \ a / a = 1" - by (simp add: divide_inverse) +by (simp add: divide_inverse) lemma divide_zero_left [simp]: "0 / a = 0" - by (simp add: divide_inverse) +by (simp add: divide_inverse) lemma inverse_eq_divide: "inverse a = 1 / a" - by (simp add: divide_inverse) +by (simp add: divide_inverse) lemma add_divide_distrib: "(a+b) / c = a/c + b/c" - by (simp add: divide_inverse ring_distribs) +by (simp add: divide_inverse algebra_simps) end @@ -529,11 +513,11 @@ lemma divide_zero [simp]: "a / 0 = (0::'a::{field,division_by_zero})" - by (simp add: divide_inverse) +by (simp add: divide_inverse) lemma divide_self_if [simp]: "a / (a::'a::{field,division_by_zero}) = (if a=0 then 0 else 1)" - by simp +by simp class mult_mono = times + zero + ord + assumes mult_left_mono: "a \ b \ 0 \ c \ c * a \ c * b" @@ -566,16 +550,16 @@ subclass pordered_semiring .. lemma mult_nonneg_nonneg: "0 \ a \ 0 \ b \ 0 \ a * b" - by (drule mult_left_mono [of zero b], auto) +by (drule mult_left_mono [of zero b], auto) lemma mult_nonneg_nonpos: "0 \ a \ b \ 0 \ a * b \ 0" - by (drule mult_left_mono [of b zero], auto) +by (drule mult_left_mono [of b zero], auto) lemma mult_nonneg_nonpos2: "0 \ a \ b \ 0 \ b * a \ 0" - by (drule mult_right_mono [of b zero], auto) +by (drule mult_right_mono [of b zero], auto) lemma split_mult_neg_le: "(0 \ a & b \ 0) | (a \ 0 & 0 \ b) \ a * b \ 0" - by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2) +by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2) end @@ -588,11 +572,11 @@ lemma mult_left_less_imp_less: "c * a < c * b \ 0 \ c \ a < b" - by (force simp add: mult_left_mono not_le [symmetric]) +by (force simp add: mult_left_mono not_le [symmetric]) lemma mult_right_less_imp_less: "a * c < b * c \ 0 \ c \ a < b" - by (force simp add: mult_right_mono not_le [symmetric]) +by (force simp add: mult_right_mono not_le [symmetric]) end @@ -617,23 +601,23 @@ lemma mult_left_le_imp_le: "c * a \ c * b \ 0 < c \ a \ b" - by (force simp add: mult_strict_left_mono _not_less [symmetric]) +by (force simp add: mult_strict_left_mono _not_less [symmetric]) lemma mult_right_le_imp_le: "a * c \ b * c \ 0 < c \ a \ b" - by (force simp add: mult_strict_right_mono not_less [symmetric]) +by (force simp add: mult_strict_right_mono not_less [symmetric]) lemma mult_pos_pos: "0 < a \ 0 < b \ 0 < a * b" - by (drule mult_strict_left_mono [of zero b], auto) +by (drule mult_strict_left_mono [of zero b], auto) lemma mult_pos_neg: "0 < a \ b < 0 \ a * b < 0" - by (drule mult_strict_left_mono [of b zero], auto) +by (drule mult_strict_left_mono [of b zero], auto) lemma mult_pos_neg2: "0 < a \ b < 0 \ b * a < 0" - by (drule mult_strict_right_mono [of b zero], auto) +by (drule mult_strict_right_mono [of b zero], auto) lemma zero_less_mult_pos: "0 < a * b \ 0 < a \ 0 < b" @@ -666,7 +650,7 @@ lemma mult_strict_mono': assumes "a < b" and "c < d" and "0 \ a" and "0 \ c" shows "a * c < b * d" - by (rule mult_strict_mono) (insert assms, auto) +by (rule mult_strict_mono) (insert assms, auto) lemma mult_less_le_imp_less: assumes "a < b" and "c \ d" and "0 \ a" and "0 < c" @@ -697,8 +681,7 @@ assume "\ a < b" hence "b \ a" by (simp add: linorder_not_less) hence "c * b \ c * a" using nonneg by (rule mult_left_mono) - with this and less show False - by (simp add: not_less [symmetric]) + with this and less show False by (simp add: not_less [symmetric]) qed lemma mult_less_imp_less_right: @@ -708,8 +691,7 @@ assume "\ a < b" hence "b \ a" by (simp add: linorder_not_less) hence "b * c \ a * c" using nonneg by (rule mult_right_mono) - with this and less show False - by (simp add: not_less [symmetric]) + with this and less show False by (simp add: not_less [symmetric]) qed end @@ -768,23 +750,24 @@ subclass pordered_ab_group_add .. -lemmas ring_simps = ring_simps group_simps +text{*Legacy - use @{text algebra_simps} *} +lemmas ring_simps = algebra_simps lemma less_add_iff1: "a * e + c < b * e + d \ (a - b) * e + c < d" - by (simp add: ring_simps) +by (simp add: algebra_simps) lemma less_add_iff2: "a * e + c < b * e + d \ c < (b - a) * e + d" - by (simp add: ring_simps) +by (simp add: algebra_simps) lemma le_add_iff1: "a * e + c \ b * e + d \ (a - b) * e + c \ d" - by (simp add: ring_simps) +by (simp add: algebra_simps) lemma le_add_iff2: "a * e + c \ b * e + d \ c \ (b - a) * e + d" - by (simp add: ring_simps) +by (simp add: algebra_simps) lemma mult_left_mono_neg: "b \ a \ c \ 0 \ c * a \ c * b" @@ -800,11 +783,11 @@ lemma mult_nonpos_nonpos: "a \ 0 \ b \ 0 \ 0 \ a * b" - by (drule mult_right_mono_neg [of a zero b]) auto +by (drule mult_right_mono_neg [of a zero b]) auto lemma split_mult_pos_le: "(0 \ a \ 0 \ b) \ (a \ 0 \ b \ 0) \ 0 \ a * b" - by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos) +by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos) end @@ -827,7 +810,7 @@ proof fix a b show "\a + b\ \ \a\ + \b\" - by (auto simp add: abs_if not_less neg_less_eq_nonneg less_eq_neg_nonpos) +by (auto simp add: abs_if not_less neg_less_eq_nonneg less_eq_neg_nonpos) (auto simp del: minus_add_distrib simp add: minus_add_distrib [symmetric] neg_less_eq_nonneg less_eq_neg_nonpos, auto intro: add_nonneg_nonneg, auto intro!: less_imp_le add_neg_neg) @@ -858,7 +841,7 @@ lemma mult_neg_neg: "a < 0 \ b < 0 \ 0 < a * b" - by (drule mult_strict_right_mono_neg, auto) +by (drule mult_strict_right_mono_neg, auto) subclass ring_no_zero_divisors proof @@ -903,7 +886,7 @@ lemma zero_le_mult_iff: "0 \ a * b \ 0 \ a \ 0 \ b \ a \ 0 \ b \ 0" - by (auto simp add: eq_commute [of 0] le_less not_less zero_less_mult_iff) +by (auto simp add: eq_commute [of 0] le_less not_less zero_less_mult_iff) lemma mult_less_0_iff: "a * b < 0 \ 0 < a \ b < 0 \ a < 0 \ 0 < b" @@ -918,10 +901,10 @@ done lemma zero_le_square [simp]: "0 \ a * a" - by (simp add: zero_le_mult_iff linear) +by (simp add: zero_le_mult_iff linear) lemma not_square_less_zero [simp]: "\ (a * a < 0)" - by (simp add: not_less) +by (simp add: not_less) text{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"}, also with the relations @{text "\"} and equality.*} @@ -968,19 +951,16 @@ lemma mult_le_cancel_right: "a * c \ b * c \ (0 < c \ a \ b) \ (c < 0 \ b \ a)" - by (simp add: not_less [symmetric] mult_less_cancel_right_disj) +by (simp add: not_less [symmetric] mult_less_cancel_right_disj) lemma mult_le_cancel_left: "c * a \ c * b \ (0 < c \ a \ b) \ (c < 0 \ b \ a)" - by (simp add: not_less [symmetric] mult_less_cancel_left_disj) +by (simp add: not_less [symmetric] mult_less_cancel_left_disj) end -text{*This list of rewrites simplifies ring terms by multiplying -everything out and bringing sums and products into a canonical form -(by ordered rewriting). As a result it decides ring equalities but -also helps with inequalities. *} -lemmas ring_simps = group_simps ring_distribs +text{*Legacy - use @{text algebra_simps} *} +lemmas ring_simps = algebra_simps class pordered_comm_ring = comm_ring + pordered_comm_semiring @@ -1001,13 +981,13 @@ using add_strict_mono [of zero a b c] by simp lemma zero_le_one [simp]: "0 \ 1" - by (rule zero_less_one [THEN less_imp_le]) +by (rule zero_less_one [THEN less_imp_le]) lemma not_one_le_zero [simp]: "\ 1 \ 0" - by (simp add: not_le) +by (simp add: not_le) lemma not_one_less_zero [simp]: "\ 1 < 0" - by (simp add: not_less) +by (simp add: not_less) lemma less_1_mult: assumes "1 < m" and "1 < n" @@ -1041,35 +1021,35 @@ lemma mult_le_cancel_right1: "c \ b * c \ (0 < c \ 1 \ b) \ (c < 0 \ b \ 1)" - by (insert mult_le_cancel_right [of 1 c b], simp) +by (insert mult_le_cancel_right [of 1 c b], simp) lemma mult_le_cancel_right2: "a * c \ c \ (0 < c \ a \ 1) \ (c < 0 \ 1 \ a)" - by (insert mult_le_cancel_right [of a c 1], simp) +by (insert mult_le_cancel_right [of a c 1], simp) lemma mult_le_cancel_left1: "c \ c * b \ (0 < c \ 1 \ b) \ (c < 0 \ b \ 1)" - by (insert mult_le_cancel_left [of c 1 b], simp) +by (insert mult_le_cancel_left [of c 1 b], simp) lemma mult_le_cancel_left2: "c * a \ c \ (0 < c \ a \ 1) \ (c < 0 \ 1 \ a)" - by (insert mult_le_cancel_left [of c a 1], simp) +by (insert mult_le_cancel_left [of c a 1], simp) lemma mult_less_cancel_right1: "c < b * c \ (0 \ c \ 1 < b) \ (c \ 0 \ b < 1)" - by (insert mult_less_cancel_right [of 1 c b], simp) +by (insert mult_less_cancel_right [of 1 c b], simp) lemma mult_less_cancel_right2: "a * c < c \ (0 \ c \ a < 1) \ (c \ 0 \ 1 < a)" - by (insert mult_less_cancel_right [of a c 1], simp) +by (insert mult_less_cancel_right [of a c 1], simp) lemma mult_less_cancel_left1: "c < c * b \ (0 \ c \ 1 < b) \ (c \ 0 \ b < 1)" - by (insert mult_less_cancel_left [of c 1 b], simp) +by (insert mult_less_cancel_left [of c 1 b], simp) lemma mult_less_cancel_left2: "c * a < c \ (0 \ c \ a < 1) \ (c \ 0 \ 1 < a)" - by (insert mult_less_cancel_left [of c a 1], simp) +by (insert mult_less_cancel_left [of c a 1], simp) lemma sgn_sgn [simp]: "sgn (sgn a) = sgn a" @@ -1089,7 +1069,7 @@ lemma sgn_times: "sgn (a * b) = sgn a * sgn b" - by (auto simp add: sgn_if zero_less_mult_iff) +by (auto simp add: sgn_if zero_less_mult_iff) end @@ -1150,12 +1130,10 @@ "inverse(a*b) = inverse(a) * inverse(b::'a::{field,division_by_zero})" proof cases assume "a \ 0 & b \ 0" - thus ?thesis - by (simp add: nonzero_inverse_mult_distrib mult_commute) + thus ?thesis by (simp add: nonzero_inverse_mult_distrib mult_commute) next assume "~ (a \ 0 & b \ 0)" - thus ?thesis - by force + thus ?thesis by force qed text{*There is no slick version using division by zero.*} @@ -1182,10 +1160,8 @@ by (simp add: divide_inverse nonzero_inverse_mult_distrib) also have "... = a * inverse b * (inverse c * c)" by (simp only: mult_ac) - also have "... = a * inverse b" - by simp - finally show ?thesis - by (simp add: divide_inverse) + also have "... = a * inverse b" by simp + finally show ?thesis by (simp add: divide_inverse) qed lemma mult_divide_mult_cancel_left: @@ -1346,14 +1322,14 @@ lemma divide_eq_imp: "(c::'a::{division_by_zero,field}) ~= 0 ==> b = a * c ==> b / c = a" - by (subst divide_eq_eq, simp) +by (subst divide_eq_eq, simp) lemma eq_divide_imp: "(c::'a::{division_by_zero,field}) ~= 0 ==> a * c = b ==> a = b / c" - by (subst eq_divide_eq, simp) - - -lemmas field_eq_simps = ring_simps +by (subst eq_divide_eq, simp) + + +lemmas field_eq_simps = algebra_simps (* pull / out*) add_divide_eq_iff divide_add_eq_iff diff_divide_eq_iff divide_diff_eq_iff @@ -1475,12 +1451,10 @@ shows "inverse b < inverse (a::'a::ordered_field)" proof (rule ccontr) assume "~ inverse b < inverse a" - hence "inverse a \ inverse b" - by (simp add: linorder_not_less) + hence "inverse a \ inverse b" by (simp add: linorder_not_less) hence "~ (a < b)" by (simp add: linorder_not_less inverse_le_imp_le [OF _ apos]) - thus False - by (rule notE [OF _ less]) + thus False by (rule notE [OF _ less]) qed lemma inverse_less_imp_less: @@ -1711,9 +1685,10 @@ subsection{*Field simplification*} -text{* Lemmas @{text field_simps} multiply with denominators in -in(equations) if they can be proved to be non-zero (for equations) or -positive/negative (for inequations). *} +text{* Lemmas @{text field_simps} multiply with denominators in in(equations) +if they can be proved to be non-zero (for equations) or positive/negative +(for inequations). Can be too aggressive and is therefore separate from the +more benign @{text algebra_simps}. *} lemmas field_simps = field_eq_simps (* multiply ineqn *) @@ -1981,15 +1956,15 @@ lemma mult_right_le_one_le: "0 <= (x::'a::ordered_idom) ==> 0 <= y ==> y <= 1 ==> x * y <= x" - by (auto simp add: mult_compare_simps); +by (auto simp add: mult_compare_simps); lemma mult_left_le_one_le: "0 <= (x::'a::ordered_idom) ==> 0 <= y ==> y <= 1 ==> y * x <= x" - by (auto simp add: mult_compare_simps); +by (auto simp add: mult_compare_simps); lemma mult_imp_div_pos_le: "0 < (y::'a::ordered_field) ==> x <= z * y ==> x / y <= z"; - by (subst pos_divide_le_eq, assumption+); +by (subst pos_divide_le_eq, assumption+); lemma mult_imp_le_div_pos: "0 < (y::'a::ordered_field) ==> z * y <= x ==> z <= x / y" @@ -2054,7 +2029,7 @@ qed lemma zero_less_two: "0 < 1 + 1" - by (blast intro: less_trans zero_less_one less_add_one) +by (blast intro: less_trans zero_less_one less_add_one) end @@ -2086,7 +2061,7 @@ end lemma abs_one [simp]: "abs 1 = (1::'a::ordered_idom)" - by (simp add: abs_if zero_less_one [THEN order_less_not_sym]) +by (simp add: abs_if zero_less_one [THEN order_less_not_sym]) class pordered_ring_abs = pordered_ring + pordered_ab_group_add_abs + assumes abs_eq_mult: @@ -2106,14 +2081,14 @@ let ?x = "pprt a * pprt b - pprt a * nprt b - nprt a * pprt b + nprt a * nprt b" let ?y = "pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b" have a: "(abs a) * (abs b) = ?x" - by (simp only: abs_prts[of a] abs_prts[of b] ring_simps) + by (simp only: abs_prts[of a] abs_prts[of b] algebra_simps) { fix u v :: 'a have bh: "\u = a; v = b\ \ u * v = pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b" apply (subst prts[of u], subst prts[of v]) - apply (simp add: ring_simps) + apply (simp add: algebra_simps) done } note b = this[OF refl[of a] refl[of b]] @@ -2166,7 +2141,7 @@ apply (simp_all add: mulprts abs_prts) apply (insert prems) apply (auto simp add: - ring_simps + algebra_simps iffD1[OF zero_le_iff_zero_nprt] iffD1[OF le_zero_iff_zero_pprt] iffD1[OF le_zero_iff_pprt_id] iffD1[OF zero_le_iff_nprt_id]) apply(drule (1) mult_nonneg_nonpos[of a b], simp) @@ -2178,7 +2153,7 @@ then show ?thesis apply (simp_all add: mulprts abs_prts) apply (insert prems) - apply (auto simp add: ring_simps) + apply (auto simp add: algebra_simps) apply(drule (1) mult_nonneg_nonneg[of a b],simp) apply(drule (1) mult_nonpos_nonpos[of a b],simp) done @@ -2191,10 +2166,10 @@ equal_neg_zero neg_equal_zero mult_less_0_iff) lemma abs_mult: "abs (a * b) = abs a * abs (b::'a::ordered_idom)" - by (simp add: abs_eq_mult linorder_linear) +by (simp add: abs_eq_mult linorder_linear) lemma abs_mult_self: "abs a * abs a = a * (a::'a::ordered_idom)" - by (simp add: abs_if) +by (simp add: abs_if) lemma nonzero_abs_inverse: "a \ 0 ==> abs (inverse (a::'a::ordered_field)) = inverse (abs a)" @@ -2268,7 +2243,7 @@ apply simp done then have "a * b = pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b" - by (simp add: ring_simps) + by (simp add: algebra_simps) moreover have "pprt a * pprt b <= pprt a2 * pprt b2" by (simp_all add: prems mult_mono) moreover have "pprt a * nprt b <= pprt a1 * nprt b2" diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/SEQ.thy --- a/src/HOL/SEQ.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/SEQ.thy Wed Jan 28 16:29:16 2009 +0100 @@ -388,7 +388,7 @@ lemma inverse_diff_inverse: "\(a::'a::division_ring) \ 0; b \ 0\ \ inverse a - inverse b = - (inverse a * (a - b) * inverse b)" -by (simp add: ring_simps) +by (simp add: algebra_simps) lemma Bseq_inverse_lemma: fixes x :: "'a::real_normed_div_algebra" diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/SetInterval.thy --- a/src/HOL/SetInterval.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/SetInterval.thy Wed Jan 28 16:29:16 2009 +0100 @@ -532,15 +532,15 @@ done lemma card_atLeastAtMost_int [simp]: "card {l..u} = nat (u - l + 1)" - apply (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym]) - apply (auto simp add: compare_rls) - done +apply (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym]) +apply (auto simp add: algebra_simps) +done lemma card_greaterThanAtMost_int [simp]: "card {l<..u} = nat (u - l)" - by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp) +by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp) lemma card_greaterThanLessThan_int [simp]: "card {l<.. k < (i::nat)}" proof - @@ -806,7 +806,7 @@ lemma setsum_head_upt_Suc: "m < n \ setsum f {m..i\{1..n - 1}. ?I i) = ((1+1)*?n*a + d*?I (n - 1)*?I n)" by (simp only: mult_ac gauss_sum [of "n - 1"]) (simp add: mult_ac trans [OF add_commute of_nat_Suc [symmetric]]) - finally show ?thesis by (simp add: mult_ac add_ac right_distrib) + finally show ?thesis by (simp add: algebra_simps) next assume "\(n > 1)" hence "n = 1 \ n = 0" by auto - thus ?thesis by (auto simp: mult_ac right_distrib) + thus ?thesis by (auto simp: algebra_simps) qed lemma arith_series_nat: diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/Tools/ComputeNumeral.thy --- a/src/HOL/Tools/ComputeNumeral.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/Tools/ComputeNumeral.thy Wed Jan 28 16:29:16 2009 +0100 @@ -55,7 +55,7 @@ lemma multb0x: "(Int.Bit0 x) * y = Int.Bit0 (x * y)" by (rule mult_Bit0) lemma multxb0: "x * (Int.Bit0 y) = Int.Bit0 (x * y)" unfolding Bit0_def by simp lemma multb1: "(Int.Bit1 x) * (Int.Bit1 y) = Int.Bit1 (Int.Bit0 (x * y) + x + y)" - unfolding Bit0_def Bit1_def by (simp add: ring_simps) + unfolding Bit0_def Bit1_def by (simp add: algebra_simps) lemmas bitmul = mult_Pls mult_Min mult_Pls_right mult_Min_right multb0x multxb0 multb1 lemmas bitarith = bitnorm bitiszero bitneg bitlezero biteq bitless bitle bitsucc bitpred bituminus bitadd bitmul @@ -193,6 +193,3 @@ compute_natarith compute_numberarith max_def min_def compute_num_conversions zpowerarith compute_div_mod compute_even end - - - diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/Transcendental.thy --- a/src/HOL/Transcendental.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/Transcendental.thy Wed Jan 28 16:29:16 2009 +0100 @@ -40,7 +40,7 @@ apply (simp add: right_distrib del: setsum_op_ivl_Suc) apply (subst mult_left_commute [where a="x - y"]) apply (erule subst) -apply (simp add: power_Suc ring_simps) +apply (simp add: power_Suc algebra_simps) done lemma lemma_realpow_rev_sumr: @@ -146,8 +146,7 @@ fixes z :: "'a :: {recpower,comm_ring}" shows "(\p=0..p=0..i = 0..h. \n. c n * (((x + h) ^ n - x ^ n) / h - @@ -1122,7 +1121,7 @@ apply (safe, rule lemma_DERIV_subst) apply (best intro!: DERIV_intros intro: DERIV_chain2) --{*replaces the old @{text DERIV_tac}*} -apply (auto simp add: diff_minus left_distrib right_distrib mult_ac add_ac) +apply (auto simp add: algebra_simps) done lemma sin_cos_add [simp]: @@ -1146,8 +1145,8 @@ lemma lemma_DERIV_sin_cos_minus: "\x. DERIV (%x. (sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2) x :> 0" apply (safe, rule lemma_DERIV_subst) -apply (best intro!: DERIV_intros intro: DERIV_chain2) -apply (auto simp add: diff_minus left_distrib right_distrib mult_ac add_ac) +apply (best intro!: DERIV_intros intro: DERIV_chain2) +apply (simp add: algebra_simps) done lemma sin_cos_minus: @@ -1520,9 +1519,8 @@ apply (drule pi_gt_zero [THEN reals_Archimedean4], safe) apply (subgoal_tac "0 \ x - real n * pi & (x - real n * pi) \ pi & (cos (x - real n * pi) = 0) ") -apply (auto simp add: compare_rls) - prefer 3 apply (simp add: cos_diff) - prefer 2 apply (simp add: real_of_nat_Suc left_distrib) +apply (auto simp add: algebra_simps real_of_nat_Suc) + prefer 2 apply (simp add: cos_diff) apply (simp add: cos_diff) apply (subgoal_tac "EX! x. 0 \ x & x \ pi & cos x = 0") apply (rule_tac [2] cos_total, safe) @@ -1530,7 +1528,7 @@ apply (drule_tac x = "pi/2" in spec) apply (simp add: cos_diff) apply (rule_tac x = "Suc (2 * n)" in exI) -apply (simp add: real_of_nat_Suc left_distrib, auto) +apply (simp add: real_of_nat_Suc algebra_simps, auto) done lemma sin_zero_lemma: @@ -1601,7 +1599,7 @@ apply (rule_tac c1 = "cos x * cos y" in real_mult_right_cancel [THEN subst]) apply (auto simp del: inverse_mult_distrib simp add: mult_assoc left_diff_distrib cos_add) -done +done lemma add_tan_eq: "[| cos x \ 0; cos y \ 0 |] @@ -1982,7 +1980,7 @@ also have "\ = (?c * ?c - ?s * ?s) * ?c - (?s * ?c + ?c * ?s) * ?s" by (simp only: cos_add sin_add) also have "\ = ?c * (?c\ - 3 * ?s\)" - by (simp add: ring_simps power2_eq_square) + by (simp add: algebra_simps power2_eq_square) finally have "?c\ = (sqrt 3 / 2)\" using pos_c by (simp add: sin_squared_eq power_divide) thus ?thesis @@ -2051,7 +2049,7 @@ lemma sin_cos_npi [simp]: "sin (real (Suc (2 * n)) * pi / 2) = (-1) ^ n" proof - have "sin ((real n + 1/2) * pi) = cos (real n * pi)" - by (auto simp add: right_distrib sin_add left_distrib mult_ac) + by (auto simp add: algebra_simps sin_add) thus ?thesis by (simp add: real_of_nat_Suc left_distrib add_divide_distrib mult_commute [of pi]) diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/Word/BinBoolList.thy --- a/src/HOL/Word/BinBoolList.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/Word/BinBoolList.thy Wed Jan 28 16:29:16 2009 +0100 @@ -281,7 +281,7 @@ apply clarsimp apply safe apply (erule allE, erule xtr8 [rotated], - simp add: numeral_simps ring_simps cong add : number_of_False_cong)+ + simp add: numeral_simps algebra_simps cong add : number_of_False_cong)+ done lemma bl_to_bin_lt2p: "bl_to_bin bs < (2 ^ length bs)" @@ -299,7 +299,7 @@ apply clarsimp apply safe apply (erule allE, erule preorder_class.order_trans [rotated], - simp add: numeral_simps ring_simps cong add : number_of_False_cong)+ + simp add: numeral_simps algebra_simps cong add : number_of_False_cong)+ done lemma bl_to_bin_ge0: "bl_to_bin bs >= 0" @@ -1138,4 +1138,3 @@ done end - diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/Word/WordArith.thy --- a/src/HOL/Word/WordArith.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/Word/WordArith.thy Wed Jan 28 16:29:16 2009 +0100 @@ -1002,7 +1002,7 @@ apply (auto simp add: unat_def uint_sub_if') apply (rule nat_diff_distrib) prefer 3 - apply (simp add: group_simps) + apply (simp add: algebra_simps) apply (rule nat_diff_distrib [THEN trans]) prefer 3 apply (subst nat_add_distrib) diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/ZF/LProd.thy --- a/src/HOL/ZF/LProd.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/ZF/LProd.thy Wed Jan 28 16:29:16 2009 +0100 @@ -45,9 +45,9 @@ case (lprod_list ah at bh bt a b) from prems have transR: "trans R" by auto have as: "multiset_of (ah @ a # at) = multiset_of (ah @ at) + {#a#}" (is "_ = ?ma + _") - by (simp add: ring_simps) + by (simp add: algebra_simps) have bs: "multiset_of (bh @ b # bt) = multiset_of (bh @ bt) + {#b#}" (is "_ = ?mb + _") - by (simp add: ring_simps) + by (simp add: algebra_simps) from prems have "(?ma, ?mb) \ mult R" by auto with mult_implies_one_step[OF transR] have @@ -66,7 +66,7 @@ then show ?thesis apply (simp only: as bs) apply (simp only: decomposed True) - apply (simp add: ring_simps) + apply (simp add: algebra_simps) done next case False @@ -78,7 +78,7 @@ then show ?thesis apply (simp only: as bs) apply (simp only: decomposed) - apply (simp add: ring_simps) + apply (simp add: algebra_simps) done qed qed diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/ex/Lagrange.thy --- a/src/HOL/ex/Lagrange.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/ex/Lagrange.thy Wed Jan 28 16:29:16 2009 +0100 @@ -35,7 +35,7 @@ sq (x1*y2 + x2*y1 + x3*y4 - x4*y3) + sq (x1*y3 - x2*y4 + x3*y1 + x4*y2) + sq (x1*y4 + x2*y3 - x3*y2 + x4*y1)" -by (simp add: sq_def ring_simps) +by (simp add: sq_def algebra_simps) text {* A challenge by John Harrison. Takes about 12s on a 1.6GHz machine. *} @@ -51,6 +51,6 @@ sq (p1*u2 + q1*t2 - r1*w2 + s1*v2 - t1*q2 + u1*p2 - v1*s2 + w1*r2) + sq (p1*v2 + q1*w2 + r1*t2 - s1*u2 - t1*r2 + u1*s2 + v1*p2 - w1*q2) + sq (p1*w2 - q1*v2 + r1*u2 + s1*t2 - t1*s2 - u1*r2 + v1*q2 + w1*p2)" -by (simp add: sq_def ring_simps) +by (simp add: sq_def algebra_simps) end diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/ex/MIR.thy --- a/src/HOL/ex/MIR.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/ex/MIR.thy Wed Jan 28 16:29:16 2009 +0100 @@ -709,11 +709,11 @@ next case (2 n c t) hence gd: "g dvd c" by simp from gp have gnz: "g \ 0" by simp - from prems show ?case by (simp add: real_of_int_div[OF gnz gd] ring_simps) + from prems show ?case by (simp add: real_of_int_div[OF gnz gd] algebra_simps) next case (3 c s t) hence gd: "g dvd c" by simp from gp have gnz: "g \ 0" by simp - from prems show ?case by (simp add: real_of_int_div[OF gnz gd] ring_simps) + from prems show ?case by (simp add: real_of_int_div[OF gnz gd] algebra_simps) qed (auto simp add: numgcd_def gp) consts ismaxcoeff:: "num \ int \ bool" recdef ismaxcoeff "measure size" @@ -850,12 +850,12 @@ lemma numadd[simp]: "Inum bs (numadd (t,s)) = Inum bs (Add t s)" apply (induct t s rule: numadd.induct, simp_all add: Let_def) apply (case_tac "c1+c2 = 0",case_tac "n1 \ n2", simp_all) - apply (case_tac "n1 = n2", simp_all add: ring_simps) + apply (case_tac "n1 = n2", simp_all add: algebra_simps) apply (simp only: left_distrib[symmetric]) apply simp apply (case_tac "lex_bnd t1 t2", simp_all) apply (case_tac "c1+c2 = 0") - by (case_tac "t1 = t2", simp_all add: ring_simps left_distrib[symmetric] real_of_int_mult[symmetric] real_of_int_add[symmetric]del: real_of_int_mult real_of_int_add left_distrib) + by (case_tac "t1 = t2", simp_all add: algebra_simps left_distrib[symmetric] real_of_int_mult[symmetric] real_of_int_add[symmetric]del: real_of_int_mult real_of_int_add left_distrib) lemma numadd_nb[simp]: "\ numbound0 t ; numbound0 s\ \ numbound0 (numadd (t,s))" by (induct t s rule: numadd.induct, auto simp add: Let_def) @@ -868,7 +868,7 @@ "nummul t = (\ i. Mul i t)" lemma nummul[simp]: "\ i. Inum bs (nummul t i) = Inum bs (Mul i t)" -by (induct t rule: nummul.induct, auto simp add: ring_simps) +by (induct t rule: nummul.induct, auto simp add: algebra_simps) lemma nummul_nb[simp]: "\ i. numbound0 t \ numbound0 (nummul t i)" by (induct t rule: nummul.induct, auto) @@ -928,7 +928,7 @@ with prems(1) have b:"Inum bs (Add ?bv ?bi) = Inum bs b" and bii: "isint ?bi bs" by blast+ from prems(2) have tibi: "ti = CF c a ?bi" by (simp add: Let_def split_def) from prems(2) b[symmetric] bii show ?case by (auto simp add: Let_def split_def isint_Floor isint_add isint_Mul isint_CF) -qed (auto simp add: Let_def isint_iff isint_Floor isint_add isint_Mul split_def ring_simps) +qed (auto simp add: Let_def isint_iff isint_Floor isint_add isint_Mul split_def algebra_simps) lemma split_int_nb: "numbound0 t \ numbound0 (fst (split_int t)) \ numbound0 (snd (split_int t)) " by (induct t rule: split_int.induct, auto simp add: Let_def split_def) @@ -1768,7 +1768,7 @@ have th: "(real a + b >0) = (real (-a) + (-b)< 0)" by arith show ?thesis using myless[rule_format, where b="real (floor b)"] by (simp only:th split_int_less_real'[where a="-a" and b="-b"]) - (simp add: ring_simps diff_def[symmetric],arith) + (simp add: algebra_simps diff_def[symmetric],arith) qed lemma split_int_le_real: @@ -1795,7 +1795,7 @@ proof- have th: "(real a + b \0) = (real (-a) + (-b) \ 0)" by arith show ?thesis by (simp only: th split_int_le_real'[where a="-a" and b="-b"]) - (simp add: ring_simps diff_def[symmetric],arith) + (simp add: algebra_simps diff_def[symmetric],arith) qed lemma split_int_eq_real: "(real (a::int) = b) = ( a = floor b \ b = real (floor b))" (is "?l = ?r") @@ -2281,9 +2281,9 @@ (is "?ri rdvd ?rc*?rx - ?rc*(?rk*?rd) + ?I x e" is "?ri rdvd ?rt") hence "\ (l::int). ?rt = ?ri * (real l)" by (simp add: rdvd_def) hence "\ (l::int). ?rc*?rx+ ?I x e = ?ri*(real l)+?rc*(?rk * (real i) * (real di))" - by (simp add: ring_simps di_def) + by (simp add: algebra_simps di_def) hence "\ (l::int). ?rc*?rx+ ?I x e = ?ri*(real (l + c*k*di))" - by (simp add: ring_simps) + by (simp add: algebra_simps) hence "\ (l::int). ?rc*?rx+ ?I x e = ?ri* (real l)" by blast thus "real i rdvd real c * real x + Inum (real x # bs) e" using rdvd_def by simp next @@ -2292,7 +2292,7 @@ hence "\ (l::int). ?rc*?rx+?e = ?ri * (real l)" by (simp add: rdvd_def) hence "\ (l::int). ?rc*?rx - real c * (real k * real d) +?e = ?ri * (real l) - real c * (real k * real d)" by simp hence "\ (l::int). ?rc*?rx - real c * (real k * real d) +?e = ?ri * (real l) - real c * (real k * real i * real di)" by (simp add: di_def) - hence "\ (l::int). ?rc*?rx - real c * (real k * real d) +?e = ?ri * (real (l - c*k*di))" by (simp add: ring_simps) + hence "\ (l::int). ?rc*?rx - real c * (real k * real d) +?e = ?ri * (real (l - c*k*di))" by (simp add: algebra_simps) hence "\ (l::int). ?rc*?rx - real c * (real k * real d) +?e = ?ri * (real l)" by blast thus "real i rdvd real c * real x - real c * (real k * real d) + Inum (real x # bs) e" using rdvd_def by simp @@ -2308,9 +2308,9 @@ (is "?ri rdvd ?rc*?rx - ?rc*(?rk*?rd) + ?I x e" is "?ri rdvd ?rt") hence "\ (l::int). ?rt = ?ri * (real l)" by (simp add: rdvd_def) hence "\ (l::int). ?rc*?rx+ ?I x e = ?ri*(real l)+?rc*(?rk * (real i) * (real di))" - by (simp add: ring_simps di_def) + by (simp add: algebra_simps di_def) hence "\ (l::int). ?rc*?rx+ ?I x e = ?ri*(real (l + c*k*di))" - by (simp add: ring_simps) + by (simp add: algebra_simps) hence "\ (l::int). ?rc*?rx+ ?I x e = ?ri* (real l)" by blast thus "real i rdvd real c * real x + Inum (real x # bs) e" using rdvd_def by simp next @@ -2319,7 +2319,7 @@ hence "\ (l::int). ?rc*?rx+?e = ?ri * (real l)" by (simp add: rdvd_def) hence "\ (l::int). ?rc*?rx - real c * (real k * real d) +?e = ?ri * (real l) - real c * (real k * real d)" by simp hence "\ (l::int). ?rc*?rx - real c * (real k * real d) +?e = ?ri * (real l) - real c * (real k * real i * real di)" by (simp add: di_def) - hence "\ (l::int). ?rc*?rx - real c * (real k * real d) +?e = ?ri * (real (l - c*k*di))" by (simp add: ring_simps) + hence "\ (l::int). ?rc*?rx - real c * (real k * real d) +?e = ?ri * (real (l - c*k*di))" by (simp add: algebra_simps) hence "\ (l::int). ?rc*?rx - real c * (real k * real d) +?e = ?ri * (real l)" by blast thus "real i rdvd real c * real x - real c * (real k * real d) + Inum (real x # bs) e" using rdvd_def by simp @@ -2450,16 +2450,16 @@ have th: "(real j rdvd real c * real x - Inum (real x # bs) e) = (real j rdvd - (real c * real x - Inum (real x # bs) e))" by (simp only: rdvd_minus[symmetric]) - from prems show ?case - by (simp add: ring_simps th[simplified ring_simps] + from prems th show ?case + by (simp add: algebra_simps numbound0_I[where bs="bs" and b'="real x" and b="- real x"]) next case (10 j c e) have th: "(real j rdvd real c * real x - Inum (real x # bs) e) = (real j rdvd - (real c * real x - Inum (real x # bs) e))" by (simp only: rdvd_minus[symmetric]) - from prems show ?case - by (simp add: ring_simps th[simplified ring_simps] + from prems th show ?case + by (simp add: algebra_simps numbound0_I[where bs="bs" and b'="real x" and b="- real x"]) qed (auto simp add: numbound0_I[where bs="bs" and b="real x" and b'="- real x"] nth_pos2) @@ -2541,7 +2541,7 @@ hence "(real l * real x + real (l div c) * Inum (real x # bs) e < (0\real)) = (real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e < 0)" by simp - also have "\ = (real (l div c) * (real c * real x + Inum (real x # bs) e) < (real (l div c)) * 0)" by (simp add: ring_simps) + also have "\ = (real (l div c) * (real c * real x + Inum (real x # bs) e) < (real (l div c)) * 0)" by (simp add: algebra_simps) also have "\ = (real c * real x + Inum (real x # bs) e < 0)" using mult_less_0_iff [where a="real (l div c)" and b="real c * real x + Inum (real x # bs) e"] ldcp by simp finally show ?case using numbound0_I[OF be,where b="real (l * x)" and b'="real x" and bs="bs"] be isint_Mul[OF ei] by simp @@ -2559,7 +2559,7 @@ hence "(real l * real x + real (l div c) * Inum (real x # bs) e \ (0\real)) = (real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e \ 0)" by simp - also have "\ = (real (l div c) * (real c * real x + Inum (real x # bs) e) \ (real (l div c)) * 0)" by (simp add: ring_simps) + also have "\ = (real (l div c) * (real c * real x + Inum (real x # bs) e) \ (real (l div c)) * 0)" by (simp add: algebra_simps) also have "\ = (real c * real x + Inum (real x # bs) e \ 0)" using mult_le_0_iff [where a="real (l div c)" and b="real c * real x + Inum (real x # bs) e"] ldcp by simp finally show ?case using numbound0_I[OF be,where b="real (l * x)" and b'="real x" and bs="bs"] be isint_Mul[OF ei] by simp @@ -2577,7 +2577,7 @@ hence "(real l * real x + real (l div c) * Inum (real x # bs) e > (0\real)) = (real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e > 0)" by simp - also have "\ = (real (l div c) * (real c * real x + Inum (real x # bs) e) > (real (l div c)) * 0)" by (simp add: ring_simps) + also have "\ = (real (l div c) * (real c * real x + Inum (real x # bs) e) > (real (l div c)) * 0)" by (simp add: algebra_simps) also have "\ = (real c * real x + Inum (real x # bs) e > 0)" using zero_less_mult_iff [where a="real (l div c)" and b="real c * real x + Inum (real x # bs) e"] ldcp by simp finally show ?case using numbound0_I[OF be,where b="real (l * x)" and b'="real x" and bs="bs"] be isint_Mul[OF ei] by simp @@ -2595,7 +2595,7 @@ hence "(real l * real x + real (l div c) * Inum (real x # bs) e \ (0\real)) = (real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e \ 0)" by simp - also have "\ = (real (l div c) * (real c * real x + Inum (real x # bs) e) \ (real (l div c)) * 0)" by (simp add: ring_simps) + also have "\ = (real (l div c) * (real c * real x + Inum (real x # bs) e) \ (real (l div c)) * 0)" by (simp add: algebra_simps) also have "\ = (real c * real x + Inum (real x # bs) e \ 0)" using zero_le_mult_iff [where a="real (l div c)" and b="real c * real x + Inum (real x # bs) e"] ldcp by simp finally show ?case using numbound0_I[OF be,where b="real (l * x)" and b'="real x" and bs="bs"] be isint_Mul[OF ei] by simp @@ -2613,7 +2613,7 @@ hence "(real l * real x + real (l div c) * Inum (real x # bs) e = (0\real)) = (real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e = 0)" by simp - also have "\ = (real (l div c) * (real c * real x + Inum (real x # bs) e) = (real (l div c)) * 0)" by (simp add: ring_simps) + also have "\ = (real (l div c) * (real c * real x + Inum (real x # bs) e) = (real (l div c)) * 0)" by (simp add: algebra_simps) also have "\ = (real c * real x + Inum (real x # bs) e = 0)" using mult_eq_0_iff [where a="real (l div c)" and b="real c * real x + Inum (real x # bs) e"] ldcp by simp finally show ?case using numbound0_I[OF be,where b="real (l * x)" and b'="real x" and bs="bs"] be isint_Mul[OF ei] by simp @@ -2631,7 +2631,7 @@ hence "(real l * real x + real (l div c) * Inum (real x # bs) e \ (0\real)) = (real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e \ 0)" by simp - also have "\ = (real (l div c) * (real c * real x + Inum (real x # bs) e) \ (real (l div c)) * 0)" by (simp add: ring_simps) + also have "\ = (real (l div c) * (real c * real x + Inum (real x # bs) e) \ (real (l div c)) * 0)" by (simp add: algebra_simps) also have "\ = (real c * real x + Inum (real x # bs) e \ 0)" using zero_le_mult_iff [where a="real (l div c)" and b="real c * real x + Inum (real x # bs) e"] ldcp by simp finally show ?case using numbound0_I[OF be,where b="real (l * x)" and b'="real x" and bs="bs"] be isint_Mul[OF ei] by simp @@ -2647,7 +2647,7 @@ hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp hence "(\ (k::int). real l * real x + real (l div c) * Inum (real x # bs) e = (real (l div c) * real j) * real k) = (\ (k::int). real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e = (real (l div c) * real j) * real k)" by simp - also have "\ = (\ (k::int). real (l div c) * (real c * real x + Inum (real x # bs) e - real j * real k) = real (l div c)*0)" by (simp add: ring_simps) + also have "\ = (\ (k::int). real (l div c) * (real c * real x + Inum (real x # bs) e - real j * real k) = real (l div c)*0)" by (simp add: algebra_simps) also fix k have "\ = (\ (k::int). real c * real x + Inum (real x # bs) e - real j * real k = 0)" using zero_le_mult_iff [where a="real (l div c)" and b="real c * real x + Inum (real x # bs) e - real j * real k"] ldcp by simp also have "\ = (\ (k::int). real c * real x + Inum (real x # bs) e = real j * real k)" by simp @@ -2664,7 +2664,7 @@ hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp hence "(\ (k::int). real l * real x + real (l div c) * Inum (real x # bs) e = (real (l div c) * real j) * real k) = (\ (k::int). real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e = (real (l div c) * real j) * real k)" by simp - also have "\ = (\ (k::int). real (l div c) * (real c * real x + Inum (real x # bs) e - real j * real k) = real (l div c)*0)" by (simp add: ring_simps) + also have "\ = (\ (k::int). real (l div c) * (real c * real x + Inum (real x # bs) e - real j * real k) = real (l div c)*0)" by (simp add: algebra_simps) also fix k have "\ = (\ (k::int). real c * real x + Inum (real x # bs) e - real j * real k = 0)" using zero_le_mult_iff [where a="real (l div c)" and b="real c * real x + Inum (real x # bs) e - real j * real k"] ldcp by simp also have "\ = (\ (k::int). real c * real x + Inum (real x # bs) e = real j * real k)" by simp @@ -2719,7 +2719,7 @@ hence "x + floor ?e \ 1 \ x + floor ?e \ d" by simp hence "\ (j::int) \ {1 .. d}. j = x + floor ?e" by simp hence "\ (j::int) \ {1 .. d}. real x = real (- floor ?e + j)" - by (simp only: real_of_int_inject) (simp add: ring_simps) + by (simp only: real_of_int_inject) (simp add: algebra_simps) hence "\ (j::int) \ {1 .. d}. real x = - ?e + real j" by (simp add: ie[simplified isint_iff]) with nob have ?case by auto} @@ -2744,7 +2744,7 @@ using ie by simp hence "x + floor ?e +1 \ 1 \ x + floor ?e + 1 \ d" by simp hence "\ (j::int) \ {1 .. d}. j = x + floor ?e + 1" by simp - hence "\ (j::int) \ {1 .. d}. x= - floor ?e - 1 + j" by (simp add: ring_simps) + hence "\ (j::int) \ {1 .. d}. x= - floor ?e - 1 + j" by (simp add: algebra_simps) hence "\ (j::int) \ {1 .. d}. real x= real (- floor ?e - 1 + j)" by (simp only: real_of_int_inject) hence "\ (j::int) \ {1 .. d}. real x= - ?e - 1 + real j" @@ -2759,7 +2759,7 @@ have vb: "?v \ set (\ (Eq (CN 0 c e)))" by simp from p have "real x= - ?e" by (simp add: c1) with prems(11) show ?case using dp by simp (erule ballE[where x="1"], - simp_all add:ring_simps numbound0_I[OF bn,where b="real x"and b'="a"and bs="bs"]) + simp_all add:algebra_simps numbound0_I[OF bn,where b="real x"and b'="a"and bs="bs"]) next case (4 c e)hence p: "Ifm (real x #bs) (NEq (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" and ie1: "isint e (a #bs)" using dvd1_eq1[where x="c"] by simp+ @@ -2983,7 +2983,7 @@ from prems have "?I (real x) (?s (Eq (CN 0 c e))) = ((real c * (?N (real x) t / real k) + ?N (real x) e)* real k = 0)" using real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] - numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti ring_simps) + numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti algebra_simps) also have "\ = (?I ?tk (Eq (CN 0 c e)))" using nonzero_eq_divide_eq[OF knz', where a="real c * (?N (real x) t / real k) + ?N (real x) e" and b="0", symmetric] real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) @@ -3005,7 +3005,7 @@ from prems have "?I (real x) (?s (NEq (CN 0 c e))) = ((real c * (?N (real x) t / real k) + ?N (real x) e)* real k \ 0)" using real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] - numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti ring_simps) + numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti algebra_simps) also have "\ = (?I ?tk (NEq (CN 0 c e)))" using nonzero_eq_divide_eq[OF knz', where a="real c * (?N (real x) t / real k) + ?N (real x) e" and b="0", symmetric] real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) @@ -3027,7 +3027,7 @@ from prems have "?I (real x) (?s (Lt (CN 0 c e))) = ((real c * (?N (real x) t / real k) + ?N (real x) e)* real k < 0)" using real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] - numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti ring_simps) + numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti algebra_simps) also have "\ = (?I ?tk (Lt (CN 0 c e)))" using pos_less_divide_eq[OF kpos, where a="real c * (?N (real x) t / real k) + ?N (real x) e" and b="0", symmetric] real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) @@ -3049,7 +3049,7 @@ from prems have "?I (real x) (?s (Le (CN 0 c e))) = ((real c * (?N (real x) t / real k) + ?N (real x) e)* real k \ 0)" using real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] - numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti ring_simps) + numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti algebra_simps) also have "\ = (?I ?tk (Le (CN 0 c e)))" using pos_le_divide_eq[OF kpos, where a="real c * (?N (real x) t / real k) + ?N (real x) e" and b="0", symmetric] real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) @@ -3071,7 +3071,7 @@ from prems have "?I (real x) (?s (Gt (CN 0 c e))) = ((real c * (?N (real x) t / real k) + ?N (real x) e)* real k > 0)" using real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] - numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti ring_simps) + numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti algebra_simps) also have "\ = (?I ?tk (Gt (CN 0 c e)))" using pos_divide_less_eq[OF kpos, where a="real c * (?N (real x) t / real k) + ?N (real x) e" and b="0", symmetric] real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) @@ -3093,7 +3093,7 @@ from prems have "?I (real x) (?s (Ge (CN 0 c e))) = ((real c * (?N (real x) t / real k) + ?N (real x) e)* real k \ 0)" using real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] - numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti ring_simps) + numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti algebra_simps) also have "\ = (?I ?tk (Ge (CN 0 c e)))" using pos_divide_le_eq[OF kpos, where a="real c * (?N (real x) t / real k) + ?N (real x) e" and b="0", symmetric] real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) @@ -3114,7 +3114,7 @@ from prems have "?I (real x) (?s (Dvd i (CN 0 c e))) = (real i * real k rdvd (real c * (?N (real x) t / real k) + ?N (real x) e)* real k)" using real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] - numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti ring_simps) + numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti algebra_simps) also have "\ = (?I ?tk (Dvd i (CN 0 c e)))" using rdvd_mult[OF knz, where n="i"] real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) @@ -3135,7 +3135,7 @@ from prems have "?I (real x) (?s (NDvd i (CN 0 c e))) = (\ (real i * real k rdvd (real c * (?N (real x) t / real k) + ?N (real x) e)* real k))" using real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] - numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti ring_simps) + numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti algebra_simps) also have "\ = (?I ?tk (NDvd i (CN 0 c e)))" using rdvd_mult[OF knz, where n="i"] real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) @@ -3154,7 +3154,7 @@ from kp have knz: "k\0" by simp hence knz': "real k \ 0" by simp {assume kdc: "k dvd c" from prems have ?case using real_of_int_div[OF knz kdc] by simp } moreover - {assume nkdc: "\ k dvd c" hence ?case using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] nonzero_eq_divide_eq[OF knz', where b="0" and a="real c * real x + Inum (real x # bs) e", symmetric] by (simp add: ring_simps)} + {assume nkdc: "\ k dvd c" hence ?case using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] nonzero_eq_divide_eq[OF knz', where b="0" and a="real c * real x + Inum (real x # bs) e", symmetric] by (simp add: algebra_simps)} ultimately show ?case by blast next case (4 c e) @@ -3162,7 +3162,7 @@ from kp have knz: "k\0" by simp hence knz': "real k \ 0" by simp {assume kdc: "k dvd c" from prems have ?case using real_of_int_div[OF knz kdc] by simp } moreover - {assume nkdc: "\ k dvd c" hence ?case using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] nonzero_eq_divide_eq[OF knz', where b="0" and a="real c * real x + Inum (real x # bs) e", symmetric] by (simp add: ring_simps)} + {assume nkdc: "\ k dvd c" hence ?case using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] nonzero_eq_divide_eq[OF knz', where b="0" and a="real c * real x + Inum (real x # bs) e", symmetric] by (simp add: algebra_simps)} ultimately show ?case by blast next case (5 c e) @@ -3170,7 +3170,7 @@ from kp have knz: "k\0" by simp hence knz': "real k \ 0" by simp {assume kdc: "k dvd c" from prems have ?case using real_of_int_div[OF knz kdc] by simp } moreover - {assume nkdc: "\ k dvd c" hence ?case using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] pos_less_divide_eq[OF kp, where b="0" and a="real c * real x + Inum (real x # bs) e", symmetric] by (simp add: ring_simps)} + {assume nkdc: "\ k dvd c" hence ?case using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] pos_less_divide_eq[OF kp, where b="0" and a="real c * real x + Inum (real x # bs) e", symmetric] by (simp add: algebra_simps)} ultimately show ?case by blast next case (6 c e) @@ -3178,7 +3178,7 @@ from kp have knz: "k\0" by simp hence knz': "real k \ 0" by simp {assume kdc: "k dvd c" from prems have ?case using real_of_int_div[OF knz kdc] by simp } moreover - {assume nkdc: "\ k dvd c" hence ?case using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] pos_le_divide_eq[OF kp, where b="0" and a="real c * real x + Inum (real x # bs) e", symmetric] by (simp add: ring_simps)} + {assume nkdc: "\ k dvd c" hence ?case using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] pos_le_divide_eq[OF kp, where b="0" and a="real c * real x + Inum (real x # bs) e", symmetric] by (simp add: algebra_simps)} ultimately show ?case by blast next case (7 c e) @@ -3186,7 +3186,7 @@ from kp have knz: "k\0" by simp hence knz': "real k \ 0" by simp {assume kdc: "k dvd c" from prems have ?case using real_of_int_div[OF knz kdc] by simp } moreover - {assume nkdc: "\ k dvd c" hence ?case using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] pos_divide_less_eq[OF kp, where b="0" and a="real c * real x + Inum (real x # bs) e", symmetric] by (simp add: ring_simps)} + {assume nkdc: "\ k dvd c" hence ?case using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] pos_divide_less_eq[OF kp, where b="0" and a="real c * real x + Inum (real x # bs) e", symmetric] by (simp add: algebra_simps)} ultimately show ?case by blast next case (8 c e) @@ -3194,7 +3194,7 @@ from kp have knz: "k\0" by simp hence knz': "real k \ 0" by simp {assume kdc: "k dvd c" from prems have ?case using real_of_int_div[OF knz kdc] by simp } moreover - {assume nkdc: "\ k dvd c" hence ?case using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] pos_divide_le_eq[OF kp, where b="0" and a="real c * real x + Inum (real x # bs) e", symmetric] by (simp add: ring_simps)} + {assume nkdc: "\ k dvd c" hence ?case using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] pos_divide_le_eq[OF kp, where b="0" and a="real c * real x + Inum (real x # bs) e", symmetric] by (simp add: algebra_simps)} ultimately show ?case by blast next case (9 i c e) @@ -3206,7 +3206,7 @@ hence "Ifm (real (x*k)#bs) (a\ (Dvd i (CN 0 c e)) k) = (real i * real k rdvd (real c * real x + Inum (real x#bs) e) * real k)" using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] - by (simp add: ring_simps) + by (simp add: algebra_simps) also have "\ = (Ifm (real x#bs) (Dvd i (CN 0 c e)))" by (simp add: rdvd_mult[OF knz, where n="i"]) finally have ?case . } ultimately show ?case by blast @@ -3220,7 +3220,7 @@ hence "Ifm (real (x*k)#bs) (a\ (NDvd i (CN 0 c e)) k) = (\ (real i * real k rdvd (real c * real x + Inum (real x#bs) e) * real k))" using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] - by (simp add: ring_simps) + by (simp add: algebra_simps) also have "\ = (Ifm (real x#bs) (NDvd i (CN 0 c e)))" by (simp add: rdvd_mult[OF knz, where n="i"]) finally have ?case . } ultimately show ?case by blast @@ -3233,7 +3233,7 @@ proof- have "(\ x. ?D x \ ?P' x) = (\ x. k dvd x \ ?P' x)" using int_rdvd_iff by simp also have "\ = (\x. ?P' (x*k))" using unity_coeff_ex[where P="?P'" and l="k", simplified] - by (simp add: ring_simps) + by (simp add: algebra_simps) also have "\ = (\ x. ?P x)" using a\ iszlfm_gen[OF lp] kp by auto finally show ?thesis . qed @@ -3297,7 +3297,7 @@ by simp+ {assume "real (c*i) \ - ?N i e + real (c*d)" with numbound0_I[OF nb, where bs="bs" and b="real i - real d" and b'="real i"] - have ?case by (simp add: ring_simps)} + have ?case by (simp add: algebra_simps)} moreover {assume pi: "real (c*i) = - ?N i e + real (c*d)" from mult_strict_left_mono[OF dp cp] have d: "(c*d) \ {1 .. c*d}" by simp @@ -3309,27 +3309,27 @@ real_of_int_mult] show ?case using prems dp by (simp add: add: numbound0_I[where bs="bs" and b="real i - real d" and b'="real i"] - ring_simps) + algebra_simps) next case (6 c e) hence cp: "c > 0" by simp from prems mult_strict_left_mono[OF dp cp, simplified real_of_int_less_iff[symmetric] real_of_int_mult] show ?case using prems dp by (simp add: add: numbound0_I[where bs="bs" and b="real i - real d" and b'="real i"] - ring_simps) + algebra_simps) next case (7 c e) hence cp: "c >0" and nb: "numbound0 e" and ei: "isint e (real i#bs)" and nob: "\ j\ {1 .. c*d}. real (c*i) \ - ?N i e + real j" and pi: "real (c*i) + ?N i e > 0" and cp': "real c >0" by simp+ let ?fe = "floor (?N i e)" - from pi cp have th:"(real i +?N i e / real c)*real c > 0" by (simp add: ring_simps) + from pi cp have th:"(real i +?N i e / real c)*real c > 0" by (simp add: algebra_simps) from pi ei[simplified isint_iff] have "real (c*i + ?fe) > real (0::int)" by simp hence pi': "c*i + ?fe > 0" by (simp only: real_of_int_less_iff[symmetric]) have "real (c*i) + ?N i e > real (c*d) \ real (c*i) + ?N i e \ real (c*d)" by auto moreover {assume "real (c*i) + ?N i e > real (c*d)" hence ?case - by (simp add: ring_simps + by (simp add: algebra_simps numbound0_I[OF nb,where bs="bs" and b="real i - real d" and b'="real i"])} moreover {assume H:"real (c*i) + ?N i e \ real (c*d)" @@ -3337,7 +3337,7 @@ hence pid: "c*i + ?fe \ c*d" by (simp only: real_of_int_le_iff) with pi' have "\ j1\ {1 .. c*d}. c*i + ?fe = j1" by auto hence "\ j1\ {1 .. c*d}. real (c*i) = - ?N i e + real j1" - by (simp only: diff_def[symmetric] real_of_int_mult real_of_int_add real_of_int_inject[symmetric] ei[simplified isint_iff] ring_simps) + by (simp only: diff_def[symmetric] real_of_int_mult real_of_int_add real_of_int_inject[symmetric] ei[simplified isint_iff] algebra_simps) with nob have ?case by blast } ultimately show ?case by blast next @@ -3346,13 +3346,13 @@ and pi: "real (c*i) + ?N i e \ 0" and cp': "real c >0" by simp+ let ?fe = "floor (?N i e)" - from pi cp have th:"(real i +?N i e / real c)*real c \ 0" by (simp add: ring_simps) + from pi cp have th:"(real i +?N i e / real c)*real c \ 0" by (simp add: algebra_simps) from pi ei[simplified isint_iff] have "real (c*i + ?fe) \ real (0::int)" by simp hence pi': "c*i + 1 + ?fe \ 1" by (simp only: real_of_int_le_iff[symmetric]) have "real (c*i) + ?N i e \ real (c*d) \ real (c*i) + ?N i e < real (c*d)" by auto moreover {assume "real (c*i) + ?N i e \ real (c*d)" hence ?case - by (simp add: ring_simps + by (simp add: algebra_simps numbound0_I[OF nb,where bs="bs" and b="real i - real d" and b'="real i"])} moreover {assume H:"real (c*i) + ?N i e < real (c*d)" @@ -3360,9 +3360,9 @@ hence pid: "c*i + 1 + ?fe \ c*d" by (simp only: real_of_int_le_iff) with pi' have "\ j1\ {1 .. c*d}. c*i + 1+ ?fe = j1" by auto hence "\ j1\ {1 .. c*d}. real (c*i) + 1= - ?N i e + real j1" - by (simp only: diff_def[symmetric] real_of_int_mult real_of_int_add real_of_int_inject[symmetric] ei[simplified isint_iff] ring_simps real_of_one) + by (simp only: diff_def[symmetric] real_of_int_mult real_of_int_add real_of_int_inject[symmetric] ei[simplified isint_iff] algebra_simps real_of_one) hence "\ j1\ {1 .. c*d}. real (c*i) = (- ?N i e + real j1) - 1" - by (simp only: ring_simps diff_def[symmetric]) + by (simp only: algebra_simps diff_def[symmetric]) hence "\ j1\ {1 .. c*d}. real (c*i) = - 1 - ?N i e + real j1" by (simp only: add_ac diff_def) with nob have ?case by blast } @@ -3383,10 +3383,10 @@ using int_rdvd_iff[where i="j" and t="(c*i - c*d + floor ?e)",symmetric, simplified] ie by simp also have "\ = (real j rdvd real (c*(i - d)) + ?e)" - using ie by (simp add:ring_simps) + using ie by (simp add:algebra_simps) finally show ?case using numbound0_I[OF bn,where b="real i - real d" and b'="real i" and bs="bs"] p - by (simp add: ring_simps) + by (simp add: algebra_simps) next case (10 j c e) hence p: "\ (real j rdvd real (c*i) + ?N i e)" (is "?p x") and cp: "c > 0" and bn:"numbound0 e" by simp+ let ?e = "Inum (real i # bs) e" @@ -3403,10 +3403,10 @@ using int_rdvd_iff[where i="j" and t="(c*i - c*d + floor ?e)",symmetric, simplified] ie by simp also have "\ = Not (real j rdvd real (c*(i - d)) + ?e)" - using ie by (simp add:ring_simps) + using ie by (simp add:algebra_simps) finally show ?case using numbound0_I[OF bn,where b="real i - real d" and b'="real i" and bs="bs"] p - by (simp add: ring_simps) + by (simp add: algebra_simps) qed(auto simp add: numbound0_I[where bs="bs" and b="real i - real d" and b'="real i"] nth_pos2) lemma \_nb: assumes lp: "iszlfm p (a#bs)" and nb: "numbound0 t" @@ -3649,7 +3649,7 @@ from H have "?I (?p (p',n',s') j) \ (((?N ?nxs \ real ?l) \ (?N ?nxs < real (?l + 1))) \ (?N a = ?N ?nxs ))" - by (simp add: fp_def np ring_simps numsub numadd numfloor) + by (simp add: fp_def np algebra_simps numsub numadd numfloor) also have "\ \ ((floor (?N ?nxs) = ?l) \ (?N a = ?N ?nxs ))" using floor_int_eq[where x="?N ?nxs" and n="?l"] by simp moreover @@ -3675,7 +3675,7 @@ from H have "?I (?p (p',n',s') j) \ (((?N ?nxs \ real ?l) \ (?N ?nxs < real (?l + 1))) \ (?N a = ?N ?nxs ))" - by (simp add: np fp_def ring_simps numneg numfloor numadd numsub) + by (simp add: np fp_def algebra_simps numneg numfloor numadd numsub) also have "\ \ ((floor (?N ?nxs) = ?l) \ (?N a = ?N ?nxs ))" using floor_int_eq[where x="?N ?nxs" and n="?l"] by simp moreover @@ -3691,7 +3691,7 @@ apply (erule_tac x = "(aa, aaa, ba)" in ballE) apply simp_all apply (erule_tac x = "(ab, ac, baa)" in ballE) apply simp_all done -qed (auto simp add: Let_def split_def ring_simps conj_rl) +qed (auto simp add: Let_def split_def algebra_simps conj_rl) lemma real_in_int_intervals: assumes xb: "real m \ x \ x < real ((n::int) + 1)" @@ -3795,7 +3795,7 @@ hence "\ j\ {0 .. n}. 0 \ real n *x + ?N s - ?N (Floor s) - real j \ real n *x + ?N s - ?N (Floor s) - real (j+1) < 0" by(simp only: myl[rule_format, where b="real n * x + Inum (x # bs) s - Inum (x # bs) (Floor s)"] less_iff_diff_less_0[where a="real n *x + ?N s - ?N (Floor s)"]) hence "\ j\ {0.. n}. ?I (?p (p,n,s) j)" - using pns by (simp add: fp_def np ring_simps numsub numadd) + using pns by (simp add: fp_def np algebra_simps numsub numadd) then obtain "j" where j_def: "j\ {0 .. n} \ ?I (?p (p,n,s) j)" by blast hence "\x \ {?p (p,n,s) j |j. 0\ j \ j \ n }. ?I x" by auto hence ?case using pns @@ -3813,7 +3813,7 @@ have "real n *x + ?N s \ real n + ?N s" by simp moreover from real_of_int_floor_le[where r="?N s"] have "real n + ?N s \ real n + ?N (Floor s)" by simp ultimately have "real n *x + ?N s \ ?N (Floor s) + real n" - by (simp only: ring_simps)} + by (simp only: algebra_simps)} ultimately have "?N (Floor s) + real n \ real n *x + ?N s\ real n *x + ?N s < ?N (Floor s) + real (1::int)" by simp hence th: "real n \ real n *x + ?N s - ?N (Floor s) \ real n *x + ?N s - ?N (Floor s) < real (1::int)" by simp have th1: "\ (a::real). (- a > 0) = (a < 0)" by auto @@ -3919,7 +3919,7 @@ fix a n s assume H: "?N a = ?N (CN 0 n s)" show "?I (lt n s) = ?I (Lt a)" using H by (cases "n=0", (simp add: lt_def)) - (cases "n > 0", simp_all add: lt_def ring_simps myless[rule_format, where b="0"]) + (cases "n > 0", simp_all add: lt_def algebra_simps myless[rule_format, where b="0"]) qed lemma lt_l: "isrlfm (rsplit lt a)" @@ -3931,7 +3931,7 @@ fix a n s assume H: "?N a = ?N (CN 0 n s)" show "?I (le n s) = ?I (Le a)" using H by (cases "n=0", (simp add: le_def)) - (cases "n > 0", simp_all add: le_def ring_simps myl[rule_format, where b="0"]) + (cases "n > 0", simp_all add: le_def algebra_simps myl[rule_format, where b="0"]) qed lemma le_l: "isrlfm (rsplit le a)" @@ -3943,7 +3943,7 @@ fix a n s assume H: "?N a = ?N (CN 0 n s)" show "?I (gt n s) = ?I (Gt a)" using H by (cases "n=0", (simp add: gt_def)) - (cases "n > 0", simp_all add: gt_def ring_simps myless[rule_format, where b="0"]) + (cases "n > 0", simp_all add: gt_def algebra_simps myless[rule_format, where b="0"]) qed lemma gt_l: "isrlfm (rsplit gt a)" by (rule rsplit_l[where f="gt" and a="a"], auto simp add: gt_def) @@ -3954,7 +3954,7 @@ fix a n s assume H: "?N a = ?N (CN 0 n s)" show "?I (ge n s) = ?I (Ge a)" using H by (cases "n=0", (simp add: ge_def)) - (cases "n > 0", simp_all add: ge_def ring_simps myl[rule_format, where b="0"]) + (cases "n > 0", simp_all add: ge_def algebra_simps myl[rule_format, where b="0"]) qed lemma ge_l: "isrlfm (rsplit ge a)" by (rule rsplit_l[where f="ge" and a="a"], auto simp add: ge_def) @@ -3964,7 +3964,7 @@ proof(clarify) fix a n s assume H: "?N a = ?N (CN 0 n s)" - show "?I (eq n s) = ?I (Eq a)" using H by (auto simp add: eq_def ring_simps) + show "?I (eq n s) = ?I (Eq a)" using H by (auto simp add: eq_def algebra_simps) qed lemma eq_l: "isrlfm (rsplit eq a)" by (rule rsplit_l[where f="eq" and a="a"], auto simp add: eq_def) @@ -3974,7 +3974,7 @@ proof(clarify) fix a n s bs assume H: "?N a = ?N (CN 0 n s)" - show "?I (neq n s) = ?I (NEq a)" using H by (auto simp add: neq_def ring_simps) + show "?I (neq n s) = ?I (NEq a)" using H by (auto simp add: neq_def algebra_simps) qed lemma neq_l: "isrlfm (rsplit neq a)" @@ -4012,10 +4012,10 @@ also have "\ = (?DE \ ?a \ 0 \ ?a < n)" by(simp only: small_le[OF ss0 ss1] small_lt[OF ss0 ss1]) also have "\ = (?DE \ (\ j\ {0 .. (n - 1)}. ?a = j))" by simp also have "\ = (?DE \ (\ j\ {0 .. (n - 1)}. real (\real n * u - s\) = real j - real \s\ ))" - by (simp only: ring_simps real_of_int_diff[symmetric] real_of_int_inject del: real_of_int_diff) + by (simp only: algebra_simps real_of_int_diff[symmetric] real_of_int_inject del: real_of_int_diff) also have "\ = ((\ j\ {0 .. (n - 1)}. real n * u - s = real j - real \s\ \ real i rdvd real n * u - s))" using int_rdvd_iff[where i="i" and t="\real n * u - s\"] by (auto cong: conj_cong) - also have "\ = ?rhs" by(simp cong: conj_cong) (simp add: ring_simps ) + also have "\ = ?rhs" by(simp cong: conj_cong) (simp add: algebra_simps ) finally show ?thesis . qed @@ -4038,7 +4038,7 @@ from foldr_disj_map[where xs="iupt(0,n - 1)" and bs="x#bs" and f="?f"] have "Ifm (x#bs) (DVDJ i n s) = (\ j\ {0 .. (n - 1)}. Ifm (x#bs) (?f j))" by (simp add: iupt_set np DVDJ_def del: iupt.simps) - also have "\ = (\ j\ {0 .. (n - 1)}. real n * x = (- ?s) - real (floor (- ?s)) + real j \ real i rdvd real (j - floor (- ?s)))" by (simp add: ring_simps diff_def[symmetric]) + also have "\ = (\ j\ {0 .. (n - 1)}. real n * x = (- ?s) - real (floor (- ?s)) + real j \ real i rdvd real (j - floor (- ?s)))" by (simp add: algebra_simps diff_def[symmetric]) also from rdvd01_cs[OF xp x1 np, where i="i" and s="-?s"] have "\ = (real i rdvd real n * x - (-?s))" by simp finally show ?thesis by simp @@ -4053,7 +4053,7 @@ from foldr_conj_map[where xs="iupt(0,n - 1)" and bs="x#bs" and f="?f"] have "Ifm (x#bs) (NDVDJ i n s) = (\ j\ {0 .. (n - 1)}. Ifm (x#bs) (?f j))" by (simp add: iupt_set np NDVDJ_def del: iupt.simps) - also have "\ = (\ (\ j\ {0 .. (n - 1)}. real n * x = (- ?s) - real (floor (- ?s)) + real j \ real i rdvd real (j - floor (- ?s))))" by (simp add: ring_simps diff_def[symmetric]) + also have "\ = (\ (\ j\ {0 .. (n - 1)}. real n * x = (- ?s) - real (floor (- ?s)) + real j \ real i rdvd real (j - floor (- ?s))))" by (simp add: algebra_simps diff_def[symmetric]) also from rdvd01_cs[OF xp x1 np, where i="i" and s="-?s"] have "\ = (\ (real i rdvd real n * x - (-?s)))" by simp finally show ?thesis by simp @@ -4652,40 +4652,40 @@ using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp also have "\ = (?n*(real c *(?t/?n)) + ?n*(?N x e) < 0)" by (simp only: pos_less_divide_eq[OF np, where a="real c *(?t/?n) + (?N x e)" - and b="0", simplified divide_zero_left]) (simp only: ring_simps) + and b="0", simplified divide_zero_left]) (simp only: algebra_simps) also have "\ = (real c *?t + ?n* (?N x e) < 0)" using np by simp - finally show ?case using nbt nb by (simp add: ring_simps) + finally show ?case using nbt nb by (simp add: algebra_simps) next case (6 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+ have "?I ?u (Le (CN 0 c e)) = (real c *(?t/?n) + (?N x e) \ 0)" using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp also have "\ = (?n*(real c *(?t/?n)) + ?n*(?N x e) \ 0)" by (simp only: pos_le_divide_eq[OF np, where a="real c *(?t/?n) + (?N x e)" - and b="0", simplified divide_zero_left]) (simp only: ring_simps) + and b="0", simplified divide_zero_left]) (simp only: algebra_simps) also have "\ = (real c *?t + ?n* (?N x e) \ 0)" using np by simp - finally show ?case using nbt nb by (simp add: ring_simps) + finally show ?case using nbt nb by (simp add: algebra_simps) next case (7 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+ have "?I ?u (Gt (CN 0 c e)) = (real c *(?t/?n) + (?N x e) > 0)" using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp also have "\ = (?n*(real c *(?t/?n)) + ?n*(?N x e) > 0)" by (simp only: pos_divide_less_eq[OF np, where a="real c *(?t/?n) + (?N x e)" - and b="0", simplified divide_zero_left]) (simp only: ring_simps) + and b="0", simplified divide_zero_left]) (simp only: algebra_simps) also have "\ = (real c *?t + ?n* (?N x e) > 0)" using np by simp - finally show ?case using nbt nb by (simp add: ring_simps) + finally show ?case using nbt nb by (simp add: algebra_simps) next case (8 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+ have "?I ?u (Ge (CN 0 c e)) = (real c *(?t/?n) + (?N x e) \ 0)" using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp also have "\ = (?n*(real c *(?t/?n)) + ?n*(?N x e) \ 0)" by (simp only: pos_divide_le_eq[OF np, where a="real c *(?t/?n) + (?N x e)" - and b="0", simplified divide_zero_left]) (simp only: ring_simps) + and b="0", simplified divide_zero_left]) (simp only: algebra_simps) also have "\ = (real c *?t + ?n* (?N x e) \ 0)" using np by simp - finally show ?case using nbt nb by (simp add: ring_simps) + finally show ?case using nbt nb by (simp add: algebra_simps) next case (3 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+ from np have np: "real n \ 0" by simp @@ -4693,10 +4693,10 @@ using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp also have "\ = (?n*(real c *(?t/?n)) + ?n*(?N x e) = 0)" by (simp only: nonzero_eq_divide_eq[OF np, where a="real c *(?t/?n) + (?N x e)" - and b="0", simplified divide_zero_left]) (simp only: ring_simps) + and b="0", simplified divide_zero_left]) (simp only: algebra_simps) also have "\ = (real c *?t + ?n* (?N x e) = 0)" using np by simp - finally show ?case using nbt nb by (simp add: ring_simps) + finally show ?case using nbt nb by (simp add: algebra_simps) next case (4 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+ from np have np: "real n \ 0" by simp @@ -4704,10 +4704,10 @@ using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp also have "\ = (?n*(real c *(?t/?n)) + ?n*(?N x e) \ 0)" by (simp only: nonzero_eq_divide_eq[OF np, where a="real c *(?t/?n) + (?N x e)" - and b="0", simplified divide_zero_left]) (simp only: ring_simps) + and b="0", simplified divide_zero_left]) (simp only: algebra_simps) also have "\ = (real c *?t + ?n* (?N x e) \ 0)" using np by simp - finally show ?case using nbt nb by (simp add: ring_simps) + finally show ?case using nbt nb by (simp add: algebra_simps) qed(simp_all add: nbt numbound0_I[where bs ="bs" and b="(Inum (x#bs) t)/ real n" and b'="x"] nth_pos2) lemma \_l: @@ -4758,7 +4758,7 @@ using lp px noS proof (induct p rule: isrlfm.induct) case (5 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+ - from prems have "x * real c + ?N x e < 0" by (simp add: ring_simps) + from prems have "x * real c + ?N x e < 0" by (simp add: algebra_simps) hence pxc: "x < (- ?N x e) / real c" by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="-?N x e"]) from prems have noSc:"\ t. l < t \ t < u \ t \ (- ?N x e) / real c" by auto @@ -4767,7 +4767,7 @@ moreover {assume y: "y < (-?N x e)/ real c" hence "y * real c < - ?N x e" by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="-?N x e", symmetric]) - hence "real c * y + ?N x e < 0" by (simp add: ring_simps) + hence "real c * y + ?N x e < 0" by (simp add: algebra_simps) hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} moreover {assume y: "y > (- ?N x e) / real c" with yu have eu: "u > (- ?N x e) / real c" by auto @@ -4777,7 +4777,7 @@ ultimately show ?case by blast next case (6 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp + - from prems have "x * real c + ?N x e \ 0" by (simp add: ring_simps) + from prems have "x * real c + ?N x e \ 0" by (simp add: algebra_simps) hence pxc: "x \ (- ?N x e) / real c" by (simp only: pos_le_divide_eq[OF cp, where a="x" and b="-?N x e"]) from prems have noSc:"\ t. l < t \ t < u \ t \ (- ?N x e) / real c" by auto @@ -4786,7 +4786,7 @@ moreover {assume y: "y < (-?N x e)/ real c" hence "y * real c < - ?N x e" by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="-?N x e", symmetric]) - hence "real c * y + ?N x e < 0" by (simp add: ring_simps) + hence "real c * y + ?N x e < 0" by (simp add: algebra_simps) hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} moreover {assume y: "y > (- ?N x e) / real c" with yu have eu: "u > (- ?N x e) / real c" by auto @@ -4796,7 +4796,7 @@ ultimately show ?case by blast next case (7 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+ - from prems have "x * real c + ?N x e > 0" by (simp add: ring_simps) + from prems have "x * real c + ?N x e > 0" by (simp add: algebra_simps) hence pxc: "x > (- ?N x e) / real c" by (simp only: pos_divide_less_eq[OF cp, where a="x" and b="-?N x e"]) from prems have noSc:"\ t. l < t \ t < u \ t \ (- ?N x e) / real c" by auto @@ -4805,7 +4805,7 @@ moreover {assume y: "y > (-?N x e)/ real c" hence "y * real c > - ?N x e" by (simp add: pos_divide_less_eq[OF cp, where a="y" and b="-?N x e", symmetric]) - hence "real c * y + ?N x e > 0" by (simp add: ring_simps) + hence "real c * y + ?N x e > 0" by (simp add: algebra_simps) hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} moreover {assume y: "y < (- ?N x e) / real c" with ly have eu: "l < (- ?N x e) / real c" by auto @@ -4815,7 +4815,7 @@ ultimately show ?case by blast next case (8 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+ - from prems have "x * real c + ?N x e \ 0" by (simp add: ring_simps) + from prems have "x * real c + ?N x e \ 0" by (simp add: algebra_simps) hence pxc: "x \ (- ?N x e) / real c" by (simp only: pos_divide_le_eq[OF cp, where a="x" and b="-?N x e"]) from prems have noSc:"\ t. l < t \ t < u \ t \ (- ?N x e) / real c" by auto @@ -4824,7 +4824,7 @@ moreover {assume y: "y > (-?N x e)/ real c" hence "y * real c > - ?N x e" by (simp add: pos_divide_less_eq[OF cp, where a="y" and b="-?N x e", symmetric]) - hence "real c * y + ?N x e > 0" by (simp add: ring_simps) + hence "real c * y + ?N x e > 0" by (simp add: algebra_simps) hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} moreover {assume y: "y < (- ?N x e) / real c" with ly have eu: "l < (- ?N x e) / real c" by auto @@ -4835,7 +4835,7 @@ next case (3 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+ from cp have cnz: "real c \ 0" by simp - from prems have "x * real c + ?N x e = 0" by (simp add: ring_simps) + from prems have "x * real c + ?N x e = 0" by (simp add: algebra_simps) hence pxc: "x = (- ?N x e) / real c" by (simp only: nonzero_eq_divide_eq[OF cnz, where a="x" and b="-?N x e"]) from prems have noSc:"\ t. l < t \ t < u \ t \ (- ?N x e) / real c" by auto @@ -4848,9 +4848,9 @@ with ly yu have yne: "y \ - ?N x e / real c" by auto hence "y* real c \ -?N x e" by (simp only: nonzero_eq_divide_eq[OF cnz, where a="y" and b="-?N x e"]) simp - hence "y* real c + ?N x e \ 0" by (simp add: ring_simps) + hence "y* real c + ?N x e \ 0" by (simp add: algebra_simps) thus ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] - by (simp add: ring_simps) + by (simp add: algebra_simps) qed (auto simp add: nth_pos2 numbound0_I[where bs="bs" and b="y" and b'="x"]) lemma finite_set_intervals: @@ -5013,7 +5013,7 @@ by (simp add: mult_commute) from tnb snb have st_nb: "numbound0 ?st" by simp have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)" - using mnp mp np by (simp add: ring_simps add_divide_distrib) + using mnp mp np by (simp add: algebra_simps add_divide_distrib) from \_I[OF lp mnp st_nb, where x="x" and bs="bs"] have "?I x (\ p (?st,2*n*m)) = ?I ((?N t / real n + ?N s / real m) /2) p" by (simp only: st[symmetric])} with rinf_\[OF lp nmi npi px] have "?F" by blast hence "?D" by blast} @@ -5082,7 +5082,7 @@ lemma exsplitnum: "Inum (x#y#bs) (exsplitnum t) = Inum ((x+y) #bs) t" - by(induct t rule: exsplitnum.induct) (simp_all add: ring_simps) + by(induct t rule: exsplitnum.induct) (simp_all add: algebra_simps) lemma exsplit: assumes qfp: "qfree p" @@ -5173,14 +5173,14 @@ from Ul th have mnz: "m \ 0" by auto from Ul th have nnz: "n \ 0" by auto have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)" - using mnz nnz by (simp add: ring_simps add_divide_distrib) + using mnz nnz by (simp add: algebra_simps add_divide_distrib) thus "(real m * Inum (x # bs) t + real n * Inum (x # bs) s) / (2 * real n * real m) \ (\((t, n), s, m). (Inum (x # bs) t / real n + Inum (x # bs) s / real m) / 2) ` (set U \ set U)"using mnz nnz th - apply (auto simp add: th add_divide_distrib ring_simps split_def image_def) + apply (auto simp add: th add_divide_distrib algebra_simps split_def image_def) by (rule_tac x="(s,m)" in bexI,simp_all) (rule_tac x="(t,n)" in bexI,simp_all) next @@ -5191,7 +5191,7 @@ from Ul smU have mnz: "m \ 0" by auto from Ul tnU have nnz: "n \ 0" by auto have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)" - using mnz nnz by (simp add: ring_simps add_divide_distrib) + using mnz nnz by (simp add: algebra_simps add_divide_distrib) let ?P = "\ (t',n') (s',m'). (Inum (x # bs) t / real n + Inum (x # bs) s / real m)/2 = (Inum (x # bs) t' / real n' + Inum (x # bs) s' / real m')/2" have Pc:"\ a b. ?P a b = ?P b a" by auto @@ -5204,7 +5204,7 @@ from ts'_U Up have mnz': "m' \ 0" and nnz': "n'\ 0" by auto let ?st' = "Add (Mul m' t') (Mul n' s')" have st': "(?N t' / real n' + ?N s' / real m')/2 = ?N ?st' / real (2*n'*m')" - using mnz' nnz' by (simp add: ring_simps add_divide_distrib) + using mnz' nnz' by (simp add: algebra_simps add_divide_distrib) from Pts' have "(Inum (x # bs) t / real n + Inum (x # bs) s / real m)/2 = (Inum (x # bs) t' / real n' + Inum (x # bs) s' / real m')/2" by simp also have "\ = ((\(t, n). Inum (x # bs) t / real n) ((\((t, n), s, m). (Add (Mul m t) (Mul n s), 2 * n * m)) ((t',n'),(s',m'))))" by (simp add: st') @@ -5234,7 +5234,7 @@ by (simp add: mult_commute real_of_int_mult[symmetric] del: real_of_int_mult) from tnb snb have stnb: "numbound0 ?st" by simp have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)" - using mp np by (simp add: ring_simps add_divide_distrib) + using mp np by (simp add: algebra_simps add_divide_distrib) from tnU smU UU' have "?g ((t,n),(s,m)) \ ?f ` U'" by blast hence "\ (t',n') \ U'. ?g ((t,n),(s,m)) = ?f (t',n')" by auto (rule_tac x="(a,b)" in bexI, auto) @@ -5262,7 +5262,7 @@ by (simp add: mult_commute real_of_int_mult[symmetric] del: real_of_int_mult) from tnb snb have stnb: "numbound0 ?st" by simp have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)" - using mp np by (simp add: ring_simps add_divide_distrib) + using mp np by (simp add: algebra_simps add_divide_distrib) from U' tnU' have tnb': "numbound0 t'" and np': "real n' > 0" by auto from \_I[OF lp np' tnb', where bs="bs" and x="x",simplified th[simplified split_def fst_conv snd_conv] st] Pt' have Pst2: "Ifm (Inum (x # bs) (Add (Mul m t) (Mul n s)) / real (2 * n * m) # bs) p" by simp diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/ex/Numeral.thy --- a/src/HOL/ex/Numeral.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/ex/Numeral.thy Wed Jan 28 16:29:16 2009 +0100 @@ -699,7 +699,7 @@ begin subclass semiring_1_minus - proof qed (simp_all add: ring_simps) + proof qed (simp_all add: algebra_simps) lemma Dig_zero_minus_of_num [numeral]: "0 - of_num n = - of_num n" @@ -783,7 +783,7 @@ "sub (Dig1 m) (Dig1 n) = dup (sub m n)" "sub (Dig1 m) (Dig0 n) = dup (sub m n) + 1" "sub (Dig0 m) (Dig1 n) = dup (sub m n) - 1" - apply (simp_all add: dup_def ring_simps) + apply (simp_all add: dup_def algebra_simps) apply (simp_all add: of_num_plus Dig_one_plus_dec)[4] apply (simp_all add: of_num.simps) done diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/ex/ReflectedFerrack.thy --- a/src/HOL/ex/ReflectedFerrack.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/ex/ReflectedFerrack.thy Wed Jan 28 16:29:16 2009 +0100 @@ -532,7 +532,7 @@ next case (2 n c t) hence gd: "g dvd c" by simp from gp have gnz: "g \ 0" by simp - from prems show ?case by (simp add: real_of_int_div[OF gnz gd] ring_simps) + from prems show ?case by (simp add: real_of_int_div[OF gnz gd] algebra_simps) qed (auto simp add: numgcd_def gp) consts ismaxcoeff:: "num \ int \ bool" recdef ismaxcoeff "measure size" @@ -636,7 +636,7 @@ lemma numadd[simp]: "Inum bs (numadd (t,s)) = Inum bs (Add t s)" apply (induct t s rule: numadd.induct, simp_all add: Let_def) apply (case_tac "c1+c2 = 0",case_tac "n1 \ n2", simp_all) -apply (case_tac "n1 = n2", simp_all add: ring_simps) +apply (case_tac "n1 = n2", simp_all add: algebra_simps) by (simp only: left_distrib[symmetric],simp) lemma numadd_nb[simp]: "\ numbound0 t ; numbound0 s\ \ numbound0 (numadd (t,s))" @@ -648,7 +648,7 @@ "nummul t = (\ i. Mul i t)" lemma nummul[simp]: "\ i. Inum bs (nummul t i) = Inum bs (Mul i t)" -by (induct t rule: nummul.induct, auto simp add: ring_simps) +by (induct t rule: nummul.induct, auto simp add: algebra_simps) lemma nummul_nb[simp]: "\ i. numbound0 t \ numbound0 (nummul t i)" by (induct t rule: nummul.induct, auto ) @@ -1001,10 +1001,10 @@ by(cases "rsplit0 a",auto simp add: Let_def split_def) have "Inum bs ((split (CN 0)) (rsplit0 (Add a b))) = Inum bs ((split (CN 0)) ?sa)+Inum bs ((split (CN 0)) ?sb)" - by (simp add: Let_def split_def ring_simps) + by (simp add: Let_def split_def algebra_simps) also have "\ = Inum bs a + Inum bs b" using prems by (cases "rsplit0 a", simp_all) finally show ?case using nb by simp -qed(auto simp add: Let_def split_def ring_simps , simp add: right_distrib[symmetric]) +qed(auto simp add: Let_def split_def algebra_simps , simp add: right_distrib[symmetric]) (* Linearize a formula*) definition @@ -1396,40 +1396,40 @@ using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp also have "\ = (?n*(real c *(?t/?n)) + ?n*(?N x e) < 0)" by (simp only: pos_less_divide_eq[OF np, where a="real c *(?t/?n) + (?N x e)" - and b="0", simplified divide_zero_left]) (simp only: ring_simps) + and b="0", simplified divide_zero_left]) (simp only: algebra_simps) also have "\ = (real c *?t + ?n* (?N x e) < 0)" using np by simp - finally show ?case using nbt nb by (simp add: ring_simps) + finally show ?case using nbt nb by (simp add: algebra_simps) next case (6 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+ have "?I ?u (Le (CN 0 c e)) = (real c *(?t/?n) + (?N x e) \ 0)" using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp also have "\ = (?n*(real c *(?t/?n)) + ?n*(?N x e) \ 0)" by (simp only: pos_le_divide_eq[OF np, where a="real c *(?t/?n) + (?N x e)" - and b="0", simplified divide_zero_left]) (simp only: ring_simps) + and b="0", simplified divide_zero_left]) (simp only: algebra_simps) also have "\ = (real c *?t + ?n* (?N x e) \ 0)" using np by simp - finally show ?case using nbt nb by (simp add: ring_simps) + finally show ?case using nbt nb by (simp add: algebra_simps) next case (7 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+ have "?I ?u (Gt (CN 0 c e)) = (real c *(?t/?n) + (?N x e) > 0)" using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp also have "\ = (?n*(real c *(?t/?n)) + ?n*(?N x e) > 0)" by (simp only: pos_divide_less_eq[OF np, where a="real c *(?t/?n) + (?N x e)" - and b="0", simplified divide_zero_left]) (simp only: ring_simps) + and b="0", simplified divide_zero_left]) (simp only: algebra_simps) also have "\ = (real c *?t + ?n* (?N x e) > 0)" using np by simp - finally show ?case using nbt nb by (simp add: ring_simps) + finally show ?case using nbt nb by (simp add: algebra_simps) next case (8 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+ have "?I ?u (Ge (CN 0 c e)) = (real c *(?t/?n) + (?N x e) \ 0)" using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp also have "\ = (?n*(real c *(?t/?n)) + ?n*(?N x e) \ 0)" by (simp only: pos_divide_le_eq[OF np, where a="real c *(?t/?n) + (?N x e)" - and b="0", simplified divide_zero_left]) (simp only: ring_simps) + and b="0", simplified divide_zero_left]) (simp only: algebra_simps) also have "\ = (real c *?t + ?n* (?N x e) \ 0)" using np by simp - finally show ?case using nbt nb by (simp add: ring_simps) + finally show ?case using nbt nb by (simp add: algebra_simps) next case (3 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+ from np have np: "real n \ 0" by simp @@ -1437,10 +1437,10 @@ using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp also have "\ = (?n*(real c *(?t/?n)) + ?n*(?N x e) = 0)" by (simp only: nonzero_eq_divide_eq[OF np, where a="real c *(?t/?n) + (?N x e)" - and b="0", simplified divide_zero_left]) (simp only: ring_simps) + and b="0", simplified divide_zero_left]) (simp only: algebra_simps) also have "\ = (real c *?t + ?n* (?N x e) = 0)" using np by simp - finally show ?case using nbt nb by (simp add: ring_simps) + finally show ?case using nbt nb by (simp add: algebra_simps) next case (4 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+ from np have np: "real n \ 0" by simp @@ -1448,10 +1448,10 @@ using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp also have "\ = (?n*(real c *(?t/?n)) + ?n*(?N x e) \ 0)" by (simp only: nonzero_eq_divide_eq[OF np, where a="real c *(?t/?n) + (?N x e)" - and b="0", simplified divide_zero_left]) (simp only: ring_simps) + and b="0", simplified divide_zero_left]) (simp only: algebra_simps) also have "\ = (real c *?t + ?n* (?N x e) \ 0)" using np by simp - finally show ?case using nbt nb by (simp add: ring_simps) + finally show ?case using nbt nb by (simp add: algebra_simps) qed(simp_all add: nbt numbound0_I[where bs ="bs" and b="(Inum (x#bs) t)/ real n" and b'="x"] nth_pos2) lemma uset_l: @@ -1502,7 +1502,7 @@ using lp px noS proof (induct p rule: isrlfm.induct) case (5 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+ - from prems have "x * real c + ?N x e < 0" by (simp add: ring_simps) + from prems have "x * real c + ?N x e < 0" by (simp add: algebra_simps) hence pxc: "x < (- ?N x e) / real c" by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="-?N x e"]) from prems have noSc:"\ t. l < t \ t < u \ t \ (- ?N x e) / real c" by auto @@ -1511,7 +1511,7 @@ moreover {assume y: "y < (-?N x e)/ real c" hence "y * real c < - ?N x e" by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="-?N x e", symmetric]) - hence "real c * y + ?N x e < 0" by (simp add: ring_simps) + hence "real c * y + ?N x e < 0" by (simp add: algebra_simps) hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} moreover {assume y: "y > (- ?N x e) / real c" with yu have eu: "u > (- ?N x e) / real c" by auto @@ -1521,7 +1521,7 @@ ultimately show ?case by blast next case (6 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp + - from prems have "x * real c + ?N x e \ 0" by (simp add: ring_simps) + from prems have "x * real c + ?N x e \ 0" by (simp add: algebra_simps) hence pxc: "x \ (- ?N x e) / real c" by (simp only: pos_le_divide_eq[OF cp, where a="x" and b="-?N x e"]) from prems have noSc:"\ t. l < t \ t < u \ t \ (- ?N x e) / real c" by auto @@ -1530,7 +1530,7 @@ moreover {assume y: "y < (-?N x e)/ real c" hence "y * real c < - ?N x e" by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="-?N x e", symmetric]) - hence "real c * y + ?N x e < 0" by (simp add: ring_simps) + hence "real c * y + ?N x e < 0" by (simp add: algebra_simps) hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} moreover {assume y: "y > (- ?N x e) / real c" with yu have eu: "u > (- ?N x e) / real c" by auto @@ -1540,7 +1540,7 @@ ultimately show ?case by blast next case (7 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+ - from prems have "x * real c + ?N x e > 0" by (simp add: ring_simps) + from prems have "x * real c + ?N x e > 0" by (simp add: algebra_simps) hence pxc: "x > (- ?N x e) / real c" by (simp only: pos_divide_less_eq[OF cp, where a="x" and b="-?N x e"]) from prems have noSc:"\ t. l < t \ t < u \ t \ (- ?N x e) / real c" by auto @@ -1549,7 +1549,7 @@ moreover {assume y: "y > (-?N x e)/ real c" hence "y * real c > - ?N x e" by (simp add: pos_divide_less_eq[OF cp, where a="y" and b="-?N x e", symmetric]) - hence "real c * y + ?N x e > 0" by (simp add: ring_simps) + hence "real c * y + ?N x e > 0" by (simp add: algebra_simps) hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} moreover {assume y: "y < (- ?N x e) / real c" with ly have eu: "l < (- ?N x e) / real c" by auto @@ -1559,7 +1559,7 @@ ultimately show ?case by blast next case (8 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+ - from prems have "x * real c + ?N x e \ 0" by (simp add: ring_simps) + from prems have "x * real c + ?N x e \ 0" by (simp add: algebra_simps) hence pxc: "x \ (- ?N x e) / real c" by (simp only: pos_divide_le_eq[OF cp, where a="x" and b="-?N x e"]) from prems have noSc:"\ t. l < t \ t < u \ t \ (- ?N x e) / real c" by auto @@ -1568,7 +1568,7 @@ moreover {assume y: "y > (-?N x e)/ real c" hence "y * real c > - ?N x e" by (simp add: pos_divide_less_eq[OF cp, where a="y" and b="-?N x e", symmetric]) - hence "real c * y + ?N x e > 0" by (simp add: ring_simps) + hence "real c * y + ?N x e > 0" by (simp add: algebra_simps) hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} moreover {assume y: "y < (- ?N x e) / real c" with ly have eu: "l < (- ?N x e) / real c" by auto @@ -1579,7 +1579,7 @@ next case (3 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+ from cp have cnz: "real c \ 0" by simp - from prems have "x * real c + ?N x e = 0" by (simp add: ring_simps) + from prems have "x * real c + ?N x e = 0" by (simp add: algebra_simps) hence pxc: "x = (- ?N x e) / real c" by (simp only: nonzero_eq_divide_eq[OF cnz, where a="x" and b="-?N x e"]) from prems have noSc:"\ t. l < t \ t < u \ t \ (- ?N x e) / real c" by auto @@ -1592,9 +1592,9 @@ with ly yu have yne: "y \ - ?N x e / real c" by auto hence "y* real c \ -?N x e" by (simp only: nonzero_eq_divide_eq[OF cnz, where a="y" and b="-?N x e"]) simp - hence "y* real c + ?N x e \ 0" by (simp add: ring_simps) + hence "y* real c + ?N x e \ 0" by (simp add: algebra_simps) thus ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] - by (simp add: ring_simps) + by (simp add: algebra_simps) qed (auto simp add: nth_pos2 numbound0_I[where bs="bs" and b="y" and b'="x"]) lemma finite_set_intervals: @@ -1757,7 +1757,7 @@ by (simp add: mult_commute) from tnb snb have st_nb: "numbound0 ?st" by simp have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)" - using mnp mp np by (simp add: ring_simps add_divide_distrib) + using mnp mp np by (simp add: algebra_simps add_divide_distrib) from usubst_I[OF lp mnp st_nb, where x="x" and bs="bs"] have "?I x (usubst p (?st,2*n*m)) = ?I ((?N t / real n + ?N s / real m) /2) p" by (simp only: st[symmetric])} with rinf_uset[OF lp nmi npi px] have "?F" by blast hence "?D" by blast} @@ -1801,14 +1801,14 @@ from Ul th have mnz: "m \ 0" by auto from Ul th have nnz: "n \ 0" by auto have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)" - using mnz nnz by (simp add: ring_simps add_divide_distrib) + using mnz nnz by (simp add: algebra_simps add_divide_distrib) thus "(real m * Inum (x # bs) t + real n * Inum (x # bs) s) / (2 * real n * real m) \ (\((t, n), s, m). (Inum (x # bs) t / real n + Inum (x # bs) s / real m) / 2) ` (set U \ set U)"using mnz nnz th - apply (auto simp add: th add_divide_distrib ring_simps split_def image_def) + apply (auto simp add: th add_divide_distrib algebra_simps split_def image_def) by (rule_tac x="(s,m)" in bexI,simp_all) (rule_tac x="(t,n)" in bexI,simp_all) next @@ -1819,7 +1819,7 @@ from Ul smU have mnz: "m \ 0" by auto from Ul tnU have nnz: "n \ 0" by auto have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)" - using mnz nnz by (simp add: ring_simps add_divide_distrib) + using mnz nnz by (simp add: algebra_simps add_divide_distrib) let ?P = "\ (t',n') (s',m'). (Inum (x # bs) t / real n + Inum (x # bs) s / real m)/2 = (Inum (x # bs) t' / real n' + Inum (x # bs) s' / real m')/2" have Pc:"\ a b. ?P a b = ?P b a" by auto @@ -1832,7 +1832,7 @@ from ts'_U Up have mnz': "m' \ 0" and nnz': "n'\ 0" by auto let ?st' = "Add (Mul m' t') (Mul n' s')" have st': "(?N t' / real n' + ?N s' / real m')/2 = ?N ?st' / real (2*n'*m')" - using mnz' nnz' by (simp add: ring_simps add_divide_distrib) + using mnz' nnz' by (simp add: algebra_simps add_divide_distrib) from Pts' have "(Inum (x # bs) t / real n + Inum (x # bs) s / real m)/2 = (Inum (x # bs) t' / real n' + Inum (x # bs) s' / real m')/2" by simp also have "\ = ((\(t, n). Inum (x # bs) t / real n) ((\((t, n), s, m). (Add (Mul m t) (Mul n s), 2 * n * m)) ((t',n'),(s',m'))))" by (simp add: st') @@ -1862,7 +1862,7 @@ by (simp add: mult_commute real_of_int_mult[symmetric] del: real_of_int_mult) from tnb snb have stnb: "numbound0 ?st" by simp have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)" - using mp np by (simp add: ring_simps add_divide_distrib) + using mp np by (simp add: algebra_simps add_divide_distrib) from tnU smU UU' have "?g ((t,n),(s,m)) \ ?f ` U'" by blast hence "\ (t',n') \ U'. ?g ((t,n),(s,m)) = ?f (t',n')" by auto (rule_tac x="(a,b)" in bexI, auto) @@ -1890,7 +1890,7 @@ by (simp add: mult_commute real_of_int_mult[symmetric] del: real_of_int_mult) from tnb snb have stnb: "numbound0 ?st" by simp have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)" - using mp np by (simp add: ring_simps add_divide_distrib) + using mp np by (simp add: algebra_simps add_divide_distrib) from U' tnU' have tnb': "numbound0 t'" and np': "real n' > 0" by auto from usubst_I[OF lp np' tnb', where bs="bs" and x="x",simplified th[simplified split_def fst_conv snd_conv] st] Pt' have Pst2: "Ifm (Inum (x # bs) (Add (Mul m t) (Mul n s)) / real (2 * n * m) # bs) p" by simp diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/ex/Reflected_Presburger.thy --- a/src/HOL/ex/Reflected_Presburger.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/ex/Reflected_Presburger.thy Wed Jan 28 16:29:16 2009 +0100 @@ -437,7 +437,7 @@ apply (induct t s rule: numadd.induct, simp_all add: Let_def) apply (case_tac "c1+c2 = 0",case_tac "n1 \ n2", simp_all) apply (case_tac "n1 = n2") - apply(simp_all add: ring_simps) + apply(simp_all add: algebra_simps) apply(simp add: left_distrib[symmetric]) done @@ -452,7 +452,7 @@ | "nummul i t = Mul i t" lemma nummul: "\ i. Inum bs (nummul i t) = Inum bs (Mul i t)" -by (induct t rule: nummul.induct, auto simp add: ring_simps numadd) +by (induct t rule: nummul.induct, auto simp add: algebra_simps numadd) lemma nummul_nb: "\ i. numbound0 t \ numbound0 (nummul i t)" by (induct t rule: nummul.induct, auto simp add: numadd_nb) @@ -912,7 +912,7 @@ have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto let ?N = "\ t. Inum (i#bs) t" from prems Ia nb show ?case - apply (auto simp add: Let_def split_def ring_simps) + apply (auto simp add: Let_def split_def algebra_simps) apply (cases "?r",auto) apply (case_tac nat, auto) done @@ -925,7 +925,7 @@ have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto let ?N = "\ t. Inum (i#bs) t" from prems Ia nb show ?case - apply (auto simp add: Let_def split_def ring_simps) + apply (auto simp add: Let_def split_def algebra_simps) apply (cases "?r",auto) apply (case_tac nat, auto) done @@ -938,7 +938,7 @@ have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto let ?N = "\ t. Inum (i#bs) t" from prems Ia nb show ?case - apply (auto simp add: Let_def split_def ring_simps) + apply (auto simp add: Let_def split_def algebra_simps) apply (cases "?r",auto) apply (case_tac nat, auto) done @@ -951,7 +951,7 @@ have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto let ?N = "\ t. Inum (i#bs) t" from prems Ia nb show ?case - apply (auto simp add: Let_def split_def ring_simps) + apply (auto simp add: Let_def split_def algebra_simps) apply (cases "?r",auto) apply (case_tac nat, auto) done @@ -964,7 +964,7 @@ have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto let ?N = "\ t. Inum (i#bs) t" from prems Ia nb show ?case - apply (auto simp add: Let_def split_def ring_simps) + apply (auto simp add: Let_def split_def algebra_simps) apply (cases "?r",auto) apply (case_tac nat, auto) done @@ -977,7 +977,7 @@ have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto let ?N = "\ t. Inum (i#bs) t" from prems Ia nb show ?case - apply (auto simp add: Let_def split_def ring_simps) + apply (auto simp add: Let_def split_def algebra_simps) apply (cases "?r",auto) apply (case_tac nat, auto) done @@ -996,7 +996,7 @@ moreover {assume "?c=0" and "j\0" hence ?case using zsplit0_I[OF spl, where x="i" and bs="bs"] zdvd_abs1[where i="j"] - apply (auto simp add: Let_def split_def ring_simps) + apply (auto simp add: Let_def split_def algebra_simps) apply (cases "?r",auto) apply (case_tac nat, auto) done} @@ -1027,7 +1027,7 @@ moreover {assume "?c=0" and "j\0" hence ?case using zsplit0_I[OF spl, where x="i" and bs="bs"] zdvd_abs1[where i="j"] - apply (auto simp add: Let_def split_def ring_simps) + apply (auto simp add: Let_def split_def algebra_simps) apply (cases "?r",auto) apply (case_tac nat, auto) done} @@ -1301,9 +1301,9 @@ (is "?ri dvd ?rc*?rx - ?rc*(?rk*?rd) + ?I x e" is "?ri dvd ?rt") hence "\ (l::int). ?rt = i * l" by (simp add: dvd_def) hence "\ (l::int). c*x+ ?I x e = i*l+c*(k * i*di)" - by (simp add: ring_simps di_def) + by (simp add: algebra_simps di_def) hence "\ (l::int). c*x+ ?I x e = i*(l + c*k*di)" - by (simp add: ring_simps) + by (simp add: algebra_simps) hence "\ (l::int). c*x+ ?I x e = i*l" by blast thus "i dvd c*x + Inum (x # bs) e" by (simp add: dvd_def) next @@ -1312,7 +1312,7 @@ hence "\ (l::int). c*x+?e = i*l" by (simp add: dvd_def) hence "\ (l::int). c*x - c*(k*d) +?e = i*l - c*(k*d)" by simp hence "\ (l::int). c*x - c*(k*d) +?e = i*l - c*(k*i*di)" by (simp add: di_def) - hence "\ (l::int). c*x - c*(k*d) +?e = i*((l - c*k*di))" by (simp add: ring_simps) + hence "\ (l::int). c*x - c*(k*d) +?e = i*((l - c*k*di))" by (simp add: algebra_simps) hence "\ (l::int). c*x - c * (k*d) +?e = i*l" by blast thus "i dvd c*x - c*(k*d) + Inum (x # bs) e" by (simp add: dvd_def) @@ -1328,9 +1328,9 @@ (is "?ri dvd ?rc*?rx - ?rc*(?rk*?rd) + ?I x e" is "?ri dvd ?rt") hence "\ (l::int). ?rt = i * l" by (simp add: dvd_def) hence "\ (l::int). c*x+ ?I x e = i*l+c*(k * i*di)" - by (simp add: ring_simps di_def) + by (simp add: algebra_simps di_def) hence "\ (l::int). c*x+ ?I x e = i*(l + c*k*di)" - by (simp add: ring_simps) + by (simp add: algebra_simps) hence "\ (l::int). c*x+ ?I x e = i*l" by blast thus "i dvd c*x + Inum (x # bs) e" by (simp add: dvd_def) next @@ -1339,7 +1339,7 @@ hence "\ (l::int). c*x+?e = i*l" by (simp add: dvd_def) hence "\ (l::int). c*x - c*(k*d) +?e = i*l - c*(k*d)" by simp hence "\ (l::int). c*x - c*(k*d) +?e = i*l - c*(k*i*di)" by (simp add: di_def) - hence "\ (l::int). c*x - c*(k*d) +?e = i*((l - c*k*di))" by (simp add: ring_simps) + hence "\ (l::int). c*x - c*(k*d) +?e = i*((l - c*k*di))" by (simp add: algebra_simps) hence "\ (l::int). c*x - c * (k*d) +?e = i*l" by blast thus "i dvd c*x - c*(k*d) + Inum (x # bs) e" by (simp add: dvd_def) @@ -1363,7 +1363,7 @@ by (simp only: zdvd_zminus_iff) also have "\ = (j dvd (c* (- x)) + ?e)" apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_def zadd_ac zminus_zadd_distrib) - by (simp add: ring_simps) + by (simp add: algebra_simps) also have "\ = Ifm bbs ((- x)#bs) (Dvd j (CN 0 c e))" using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"] by simp @@ -1375,7 +1375,7 @@ by (simp only: zdvd_zminus_iff) also have "\ = (j dvd (c* (- x)) + ?e)" apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_def zadd_ac zminus_zadd_distrib) - by (simp add: ring_simps) + by (simp add: algebra_simps) also have "\ = Ifm bbs ((- x)#bs) (Dvd j (CN 0 c e))" using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"] by simp @@ -1443,7 +1443,7 @@ hence "(l*x + (l div c) * Inum (x # bs) e < 0) = ((c * (l div c)) * x + (l div c) * Inum (x # bs) e < 0)" by simp - also have "\ = ((l div c) * (c*x + Inum (x # bs) e) < (l div c) * 0)" by (simp add: ring_simps) + also have "\ = ((l div c) * (c*x + Inum (x # bs) e) < (l div c) * 0)" by (simp add: algebra_simps) also have "\ = (c*x + Inum (x # bs) e < 0)" using mult_less_0_iff [where a="(l div c)" and b="c*x + Inum (x # bs) e"] ldcp by simp finally show ?case using numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"] be by simp @@ -1461,7 +1461,7 @@ hence "(l*x + (l div c) * Inum (x# bs) e \ 0) = ((c * (l div c)) * x + (l div c) * Inum (x # bs) e \ 0)" by simp - also have "\ = ((l div c) * (c * x + Inum (x # bs) e) \ ((l div c)) * 0)" by (simp add: ring_simps) + also have "\ = ((l div c) * (c * x + Inum (x # bs) e) \ ((l div c)) * 0)" by (simp add: algebra_simps) also have "\ = (c*x + Inum (x # bs) e \ 0)" using mult_le_0_iff [where a="(l div c)" and b="c*x + Inum (x # bs) e"] ldcp by simp finally show ?case using numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"] be by simp @@ -1479,7 +1479,7 @@ hence "(l*x + (l div c)* Inum (x # bs) e > 0) = ((c * (l div c)) * x + (l div c) * Inum (x # bs) e > 0)" by simp - also have "\ = ((l div c) * (c * x + Inum (x # bs) e) > ((l div c)) * 0)" by (simp add: ring_simps) + also have "\ = ((l div c) * (c * x + Inum (x # bs) e) > ((l div c)) * 0)" by (simp add: algebra_simps) also have "\ = (c * x + Inum (x # bs) e > 0)" using zero_less_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp by simp finally show ?case using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be by simp @@ -1498,7 +1498,7 @@ ((c*(l div c))*x + (l div c)* Inum (x # bs) e \ 0)" by simp also have "\ = ((l div c)*(c*x + Inum (x # bs) e) \ ((l div c)) * 0)" - by (simp add: ring_simps) + by (simp add: algebra_simps) also have "\ = (c*x + Inum (x # bs) e \ 0)" using ldcp zero_le_mult_iff [where a="l div c" and b="c*x + Inum (x # bs) e"] by simp finally show ?case using be numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"] @@ -1517,7 +1517,7 @@ hence "(l * x + (l div c) * Inum (x # bs) e = 0) = ((c * (l div c)) * x + (l div c) * Inum (x # bs) e = 0)" by simp - also have "\ = ((l div c) * (c * x + Inum (x # bs) e) = ((l div c)) * 0)" by (simp add: ring_simps) + also have "\ = ((l div c) * (c * x + Inum (x # bs) e) = ((l div c)) * 0)" by (simp add: algebra_simps) also have "\ = (c * x + Inum (x # bs) e = 0)" using mult_eq_0_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp by simp finally show ?case using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be by simp @@ -1535,7 +1535,7 @@ hence "(l * x + (l div c) * Inum (x # bs) e \ 0) = ((c * (l div c)) * x + (l div c) * Inum (x # bs) e \ 0)" by simp - also have "\ = ((l div c) * (c * x + Inum (x # bs) e) \ ((l div c)) * 0)" by (simp add: ring_simps) + also have "\ = ((l div c) * (c * x + Inum (x # bs) e) \ ((l div c)) * 0)" by (simp add: algebra_simps) also have "\ = (c * x + Inum (x # bs) e \ 0)" using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp by simp finally show ?case using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be by simp @@ -1551,7 +1551,7 @@ hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp hence "(\ (k::int). l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) = (\ (k::int). (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)" by simp - also have "\ = (\ (k::int). (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c)*0)" by (simp add: ring_simps) + also have "\ = (\ (k::int). (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c)*0)" by (simp add: algebra_simps) also fix k have "\ = (\ (k::int). c * x + Inum (x # bs) e - j * k = 0)" using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e - j * k"] ldcp by simp also have "\ = (\ (k::int). c * x + Inum (x # bs) e = j * k)" by simp @@ -1568,7 +1568,7 @@ hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp hence "(\ (k::int). l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) = (\ (k::int). (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)" by simp - also have "\ = (\ (k::int). (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c)*0)" by (simp add: ring_simps) + also have "\ = (\ (k::int). (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c)*0)" by (simp add: algebra_simps) also fix k have "\ = (\ (k::int). c * x + Inum (x # bs) e - j * k = 0)" using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e - j * k"] ldcp by simp also have "\ = (\ (k::int). c * x + Inum (x # bs) e = j * k)" by simp @@ -1617,7 +1617,7 @@ hence "x + ?e \ 1 \ x + ?e \ d" by simp hence "\ (j::int) \ {1 .. d}. j = x + ?e" by simp hence "\ (j::int) \ {1 .. d}. x = (- ?e + j)" - by (simp add: ring_simps) + by (simp add: algebra_simps) with nob have ?case by auto} ultimately show ?case by blast next @@ -1636,7 +1636,7 @@ from H p have "x + ?e \ 0 \ x + ?e < d" by (simp add: c1) hence "x + ?e +1 \ 1 \ x + ?e + 1 \ d" by simp hence "\ (j::int) \ {1 .. d}. j = x + ?e + 1" by simp - hence "\ (j::int) \ {1 .. d}. x= - ?e - 1 + j" by (simp add: ring_simps) + hence "\ (j::int) \ {1 .. d}. x= - ?e - 1 + j" by (simp add: algebra_simps) with nob have ?case by simp } ultimately show ?case by blast next @@ -1646,7 +1646,7 @@ have vb: "?v \ set (\ (Eq (CN 0 c e)))" by simp from p have "x= - ?e" by (simp add: c1) with prems(11) show ?case using dp by simp (erule ballE[where x="1"], - simp_all add:ring_simps numbound0_I[OF bn,where b="x"and b'="a"and bs="bs"]) + simp_all add:algebra_simps numbound0_I[OF bn,where b="x"and b'="a"and bs="bs"]) next case (4 c e)hence p: "Ifm bbs (x #bs) (NEq (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+ let ?e = "Inum (x # bs) e" diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/ex/ReflectionEx.thy --- a/src/HOL/ex/ReflectionEx.thy Sun Jan 18 13:58:17 2009 +0100 +++ b/src/HOL/ex/ReflectionEx.thy Wed Jan 28 16:29:16 2009 +0100 @@ -183,7 +183,7 @@ lemma lin_add: "Inum (lin_add (t,s)) bs = Inum (Add t s) bs" apply (induct t s rule: lin_add.induct, simp_all add: Let_def) apply (case_tac "c1+c2 = 0",case_tac "n1 \ n2", simp_all) -by (case_tac "n1 = n2", simp_all add: ring_simps) +by (case_tac "n1 = n2", simp_all add: algebra_simps) consts lin_mul :: "num \ nat \ num" recdef lin_mul "measure size " @@ -192,7 +192,7 @@ "lin_mul t = (\ i. Mul i t)" lemma lin_mul: "Inum (lin_mul t i) bs = Inum (Mul i t) bs" -by (induct t arbitrary: i rule: lin_mul.induct, auto simp add: ring_simps) +by (induct t arbitrary: i rule: lin_mul.induct, auto simp add: algebra_simps) consts linum:: "num \ num" recdef linum "measure num_size"