# HG changeset patch # User nipkow # Date 1182620002 -7200 # Node ID f4b83f03cac90d25397b33deb98ad7a35600d7d1 # Parent 839db6346cc844c3c52f005c56164ea786fb4be2 tuned and renamed group_eq_simps and ring_eq_simps diff -r 839db6346cc8 -r f4b83f03cac9 src/HOL/Arith_Tools.thy --- a/src/HOL/Arith_Tools.thy Fri Jun 22 22:41:17 2007 +0200 +++ b/src/HOL/Arith_Tools.thy Sat Jun 23 19:33:22 2007 +0200 @@ -614,7 +614,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_eq_simps) + have "c*x < 0 = (0/c < x)" by (simp only: neg_divide_less_eq[OF H] ring_simps) also have "\ = (0 < x)" by simp finally show "(c*x < 0) == (x > 0)" by simp qed @@ -622,7 +622,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_eq_simps) + hence "c*x < 0 = (0/c > x)" by (simp only: pos_less_divide_eq[OF H] ring_simps) also have "\ = (0 > x)" by simp finally show "(c*x < 0) == (x < 0)" by simp qed @@ -631,7 +631,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_eq_simps) + also have "\ = (-t/c < x)" by (simp only: neg_divide_less_eq[OF H] ring_simps) also have "\ = ((- 1/c)*t < x)" by simp finally show "(c*x + t < 0) == (x > (- 1/c)*t)" by simp qed @@ -640,7 +640,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_eq_simps) + also have "\ = (-t/c > x)" by (simp only: pos_less_divide_eq[OF H] ring_simps) also have "\ = ((- 1/c)*t > x)" by simp finally show "(c*x + t < 0) == (x < (- 1/c)*t)" by simp qed @@ -651,7 +651,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_eq_simps) + have "c*x <= 0 = (0/c <= x)" by (simp only: neg_divide_le_eq[OF H] ring_simps) also have "\ = (0 <= x)" by simp finally show "(c*x <= 0) == (x >= 0)" by simp qed @@ -659,7 +659,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_eq_simps) + hence "c*x <= 0 = (0/c >= x)" by (simp only: pos_le_divide_eq[OF H] ring_simps) also have "\ = (0 >= x)" by simp finally show "(c*x <= 0) == (x <= 0)" by simp qed @@ -668,7 +668,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_eq_simps) + also have "\ = (-t/c <= x)" by (simp only: neg_divide_le_eq[OF H] ring_simps) also have "\ = ((- 1/c)*t <= x)" by simp finally show "(c*x + t <= 0) == (x >= (- 1/c)*t)" by simp qed @@ -677,7 +677,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_eq_simps) + also have "\ = (-t/c >= x)" by (simp only: pos_le_divide_eq[OF H] ring_simps) also have "\ = ((- 1/c)*t >= x)" by simp finally show "(c*x + t <= 0) == (x <= (- 1/c)*t)" by simp qed @@ -690,7 +690,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_eq_simps) + also have "\ = (x = -t/c)" by (simp only: nonzero_eq_divide_eq[OF H] ring_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 839db6346cc8 -r f4b83f03cac9 src/HOL/Complex/Complex.thy --- a/src/HOL/Complex/Complex.thy Fri Jun 22 22:41:17 2007 +0200 +++ b/src/HOL/Complex/Complex.thy Sat Jun 23 19:33:22 2007 +0200 @@ -153,7 +153,7 @@ proof fix x y z :: complex show "(x * y) * z = x * (y * z)" - by (simp add: expand_complex_eq ring_eq_simps) + by (simp add: expand_complex_eq ring_simps) show "x * y = y * x" by (simp add: expand_complex_eq mult_commute add_commute) show "1 * x = x" @@ -161,7 +161,7 @@ show "0 \ (1::complex)" by (simp add: expand_complex_eq) show "(x + y) * z = x * z + y * z" - by (simp add: expand_complex_eq ring_eq_simps) + by (simp add: expand_complex_eq ring_simps) show "x / y = x * inverse y" by (simp only: complex_divide_def) show "x \ 0 \ inverse x * x = 1" @@ -251,9 +251,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_eq_simps) + by (simp add: expand_complex_eq ring_simps) show "x * scaleR a y = scaleR a (x * y)" - by (simp add: expand_complex_eq ring_eq_simps) + by (simp add: expand_complex_eq ring_simps) qed @@ -319,7 +319,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_eq_simps) + (simp add: real_sqrt_mult [symmetric] power2_eq_square ring_simps) qed lemma cmod_unit_one [simp]: "cmod (Complex (cos a) (sin a)) = 1" diff -r 839db6346cc8 -r f4b83f03cac9 src/HOL/Complex/ex/BinEx.thy --- a/src/HOL/Complex/ex/BinEx.thy Fri Jun 22 22:41:17 2007 +0200 +++ b/src/HOL/Complex/ex/BinEx.thy Sat Jun 23 19:33:22 2007 +0200 @@ -20,379 +20,377 @@ subsubsection {*Addition *} lemma "(1359::real) + -2468 = -1109" - by simp +by simp lemma "(93746::real) + -46375 = 47371" - by simp +by simp subsubsection {*Negation *} lemma "- (65745::real) = -65745" - by simp +by simp lemma "- (-54321::real) = 54321" - by simp +by simp subsubsection {*Multiplication *} lemma "(-84::real) * 51 = -4284" - by simp +by simp lemma "(255::real) * 255 = 65025" - by simp +by simp lemma "(1359::real) * -2468 = -3354012" - by simp +by simp subsubsection {*Inequalities *} lemma "(89::real) * 10 \ 889" - by simp +by simp lemma "(13::real) < 18 - 4" - by simp +by simp lemma "(-345::real) < -242 + -100" - by simp +by simp lemma "(13557456::real) < 18678654" - by simp +by simp lemma "(999999::real) \ (1000001 + 1) - 2" - by simp +by simp lemma "(1234567::real) \ 1234567" - by simp +by simp subsubsection {*Powers *} lemma "2 ^ 15 = (32768::real)" - by simp +by simp lemma "-3 ^ 7 = (-2187::real)" - by simp +by simp lemma "13 ^ 7 = (62748517::real)" - by simp +by simp lemma "3 ^ 15 = (14348907::real)" - by simp +by simp lemma "-5 ^ 11 = (-48828125::real)" - by simp +by simp subsubsection {*Tests *} lemma "(x + y = x) = (y = (0::real))" - by arith +by arith lemma "(x + y = y) = (x = (0::real))" - by arith +by arith lemma "(x + y = (0::real)) = (x = -y)" - by arith +by arith lemma "(x + y = (0::real)) = (y = -x)" - by arith +by arith lemma "((x + y) < (x + z)) = (y < (z::real))" - by arith +by arith lemma "((x + z) < (y + z)) = (x < (y::real))" - by arith +by arith lemma "(\ x < y) = (y \ (x::real))" - by arith +by arith lemma "\ (x < y \ y < (x::real))" - by arith +by arith lemma "(x::real) < y ==> \ y < x" - by arith +by arith lemma "((x::real) \ y) = (x < y \ y < x)" - by arith +by arith lemma "(\ x \ y) = (y < (x::real))" - by arith +by arith lemma "x \ y \ y \ (x::real)" - by arith +by arith lemma "x \ y \ y < (x::real)" - by arith +by arith lemma "x < y \ y \ (x::real)" - by arith +by arith lemma "x \ (x::real)" - by arith +by arith lemma "((x::real) \ y) = (x < y \ x = y)" - by arith +by arith lemma "((x::real) \ y \ y \ x) = (x = y)" - by arith +by arith lemma "\(x < y \ y \ (x::real))" - by arith +by arith lemma "\(x \ y \ y < (x::real))" - by arith +by arith lemma "(-x < (0::real)) = (0 < x)" - by arith +by arith lemma "((0::real) < -x) = (x < 0)" - by arith +by arith lemma "(-x \ (0::real)) = (0 \ x)" - by arith +by arith lemma "((0::real) \ -x) = (x \ 0)" - by arith +by arith lemma "(x::real) = y \ x < y \ y < x" - by arith +by arith lemma "(x::real) = 0 \ 0 < x \ 0 < -x" - by arith +by arith lemma "(0::real) \ x \ 0 \ -x" - by arith +by arith lemma "((x::real) + y \ x + z) = (y \ z)" - by arith +by arith lemma "((x::real) + z \ y + z) = (x \ y)" - by arith +by arith lemma "(w::real) < x \ y < z ==> w + y < x + z" - by arith +by arith lemma "(w::real) \ x \ y \ z ==> w + y \ x + z" - by arith +by arith lemma "(0::real) \ x \ 0 \ y ==> 0 \ x + y" - by arith +by arith lemma "(0::real) < x \ 0 < y ==> 0 < x + y" - by arith +by arith lemma "(-x < y) = (0 < x + (y::real))" - by arith +by arith lemma "(x < -y) = (x + y < (0::real))" - by arith +by arith lemma "(y < x + -z) = (y + z < (x::real))" - by arith +by arith lemma "(x + -y < z) = (x < z + (y::real))" - by arith +by arith lemma "x \ y ==> x < y + (1::real)" - by arith +by arith lemma "(x - y) + y = (x::real)" - by arith +by arith lemma "y + (x - y) = (x::real)" - by arith +by arith lemma "x - x = (0::real)" - by arith +by arith lemma "(x - y = 0) = (x = (y::real))" - by arith +by arith lemma "((0::real) \ x + x) = (0 \ x)" - by arith +by arith lemma "(-x \ x) = ((0::real) \ x)" - by arith +by arith lemma "(x \ -x) = (x \ (0::real))" - by arith +by arith lemma "(-x = (0::real)) = (x = 0)" - by arith +by arith lemma "-(x - y) = y - (x::real)" - by arith +by arith lemma "((0::real) < x - y) = (y < x)" - by arith +by arith lemma "((0::real) \ x - y) = (y \ x)" - by arith +by arith lemma "(x + y) - x = (y::real)" - by arith +by arith lemma "(-x = y) = (x = (-y::real))" - by arith +by arith lemma "x < (y::real) ==> \(x = y)" - by arith +by arith lemma "(x \ x + y) = ((0::real) \ y)" - by arith +by arith lemma "(y \ x + y) = ((0::real) \ x)" - by arith +by arith lemma "(x < x + y) = ((0::real) < y)" - by arith +by arith lemma "(y < x + y) = ((0::real) < x)" - by arith +by arith lemma "(x - y) - x = (-y::real)" - by arith +by arith lemma "(x + y < z) = (x < z - (y::real))" - by arith +by arith lemma "(x - y < z) = (x < z + (y::real))" - by arith +by arith lemma "(x < y - z) = (x + z < (y::real))" - by arith +by arith lemma "(x \ y - z) = (x + z \ (y::real))" - by arith +by arith lemma "(x - y \ z) = (x \ z + (y::real))" - by arith +by arith lemma "(-x < -y) = (y < (x::real))" - by arith +by arith lemma "(-x \ -y) = (y \ (x::real))" - by arith +by arith lemma "(a + b) - (c + d) = (a - c) + (b - (d::real))" - by arith +by arith lemma "(0::real) - x = -x" - by arith +by arith lemma "x - (0::real) = x" - by arith +by arith lemma "w \ x \ y < z ==> w + y < x + (z::real)" - by arith +by arith lemma "w < x \ y \ z ==> w + y < x + (z::real)" - by arith +by arith lemma "(0::real) \ x \ 0 < y ==> 0 < x + (y::real)" - by arith +by arith lemma "(0::real) < x \ 0 \ y ==> 0 < x + y" - by arith +by arith lemma "-x - y = -(x + (y::real))" - by arith +by arith lemma "x - (-y) = x + (y::real)" - by arith +by arith lemma "-x - -y = y - (x::real)" - by arith +by arith lemma "(a - b) + (b - c) = a - (c::real)" - by arith +by arith lemma "(x = y - z) = (x + z = (y::real))" - by arith +by arith lemma "(x - y = z) = (x = z + (y::real))" - by arith +by arith lemma "x - (x - y) = (y::real)" - by arith +by arith lemma "x - (x + y) = -(y::real)" - by arith +by arith lemma "x = y ==> x \ (y::real)" - by arith +by arith lemma "(0::real) < x ==> \(x = 0)" - by arith +by arith lemma "(x + y) * (x - y) = (x * x) - (y * y)" oops lemma "(-x = -y) = (x = (y::real))" - by arith +by arith lemma "(-x < -y) = (y < (x::real))" - by arith +by arith lemma "!!a::real. a \ b ==> c \ d ==> x + y < z ==> a + c \ b + d" - by (tactic "fast_arith_tac 1") +by (tactic "fast_arith_tac 1") lemma "!!a::real. a < b ==> c < d ==> a - d \ b + (-c)" - by (tactic "fast_arith_tac 1") +by (tactic "fast_arith_tac 1") lemma "!!a::real. a \ b ==> b + b \ c ==> a + a \ c" - by (tactic "fast_arith_tac 1") +by (tactic "fast_arith_tac 1") lemma "!!a::real. a + b \ i + j ==> a \ b ==> i \ j ==> a + a \ j + j" - by (tactic "fast_arith_tac 1") +by (tactic "fast_arith_tac 1") lemma "!!a::real. a + b < i + j ==> a < b ==> i < j ==> a + a < j + j" - by (tactic "fast_arith_tac 1") +by (tactic "fast_arith_tac 1") lemma "!!a::real. a + b + c \ i + j + k \ a \ b \ b \ c \ i \ j \ j \ k --> a + a + a \ k + k + k" - by arith +by arith lemma "!!a::real. a + b + c + d \ i + j + k + l ==> a \ b ==> b \ c ==> c \ d ==> i \ j ==> j \ k ==> k \ l ==> a \ l" - by (tactic "fast_arith_tac 1") +by (tactic "fast_arith_tac 1") lemma "!!a::real. a + b + c + d \ i + j + k + l ==> a \ b ==> b \ c ==> c \ d ==> i \ j ==> j \ k ==> k \ l ==> a + a + a + a \ l + l + l + l" - by (tactic "fast_arith_tac 1") +by (tactic "fast_arith_tac 1") lemma "!!a::real. a + b + c + d \ i + j + k + l ==> a \ b ==> b \ c ==> c \ d ==> i \ j ==> j \ k ==> k \ l ==> a + a + a + a + a \ l + l + l + l + i" - by (tactic "fast_arith_tac 1") +by (tactic "fast_arith_tac 1") lemma "!!a::real. a + b + c + d \ i + j + k + l ==> a \ b ==> b \ c ==> c \ d ==> i \ j ==> j \ k ==> k \ l ==> a + a + a + a + a + a \ l + l + l + l + i + l" - by (tactic "fast_arith_tac 1") +by (tactic "fast_arith_tac 1") subsection{*Complex Arithmetic*} lemma "(1359 + 93746*ii) - (2468 + 46375*ii) = -1109 + 47371*ii" - by simp +by simp lemma "- (65745 + -47371*ii) = -65745 + 47371*ii" - by simp +by simp text{*Multiplication requires distributive laws. Perhaps versions instantiated to literal constants should be added to the simpset.*} -lemmas distrib = left_distrib right_distrib left_diff_distrib right_diff_distrib - lemma "(1 + ii) * (1 - ii) = 2" -by (simp add: distrib) +by (simp add: ring_distribs) lemma "(1 + 2*ii) * (1 + 3*ii) = -5 + 5*ii" -by (simp add: distrib) +by (simp add: ring_distribs) lemma "(-84 + 255*ii) + (51 * 255*ii) = -84 + 13260 * ii" -by (simp add: distrib) +by (simp add: ring_distribs) text{*No inequalities or linear arithmetic: the complex numbers are unordered!*} diff -r 839db6346cc8 -r f4b83f03cac9 src/HOL/Complex/ex/MIR.thy --- a/src/HOL/Complex/ex/MIR.thy Fri Jun 22 22:41:17 2007 +0200 +++ b/src/HOL/Complex/ex/MIR.thy Sat Jun 23 19:33:22 2007 +0200 @@ -714,11 +714,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_eq_simps) + from prems show ?case by (simp add: real_of_int_div[OF gnz gd] ring_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_eq_simps) + from prems show ?case by (simp add: real_of_int_div[OF gnz gd] ring_simps) qed (auto simp add: numgcd_def gp) consts ismaxcoeff:: "num \ int \ bool" recdef ismaxcoeff "measure size" @@ -855,13 +855,13 @@ 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_eq_simps) -apply (simp only: ring_eq_simps(1)[symmetric]) -apply simp + apply (case_tac "c1+c2 = 0",case_tac "n1 \ n2", simp_all) + apply (case_tac "n1 = n2", simp_all add: ring_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_eq_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) + 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) lemma numadd_nb[simp]: "\ numbound0 t ; numbound0 s\ \ numbound0 (numadd (t,s))" by (induct t s rule: numadd.induct, auto simp add: Let_def) @@ -874,7 +874,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_eq_simps) +by (induct t rule: nummul.induct, auto simp add: ring_simps) lemma nummul_nb[simp]: "\ i. numbound0 t \ numbound0 (nummul t i)" by (induct t rule: nummul.induct, auto) @@ -934,7 +934,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_eq_simps) +qed (auto simp add: Let_def isint_iff isint_Floor isint_add isint_Mul split_def ring_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) @@ -1771,7 +1771,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_eq_simps diff_def[symmetric],arith) + (simp add: ring_simps diff_def[symmetric],arith) qed lemma split_int_le_real: @@ -1798,7 +1798,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_eq_simps diff_def[symmetric],arith) + (simp add: ring_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") @@ -2276,9 +2276,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_eq_simps di_def) + by (simp add: ring_simps di_def) hence "\ (l::int). ?rc*?rx+ ?I x e = ?ri*(real (l + c*k*di))" - by (simp add: ring_eq_simps) + by (simp add: ring_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 @@ -2287,7 +2287,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_eq_simps) + 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)" 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 @@ -2303,9 +2303,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_eq_simps di_def) + by (simp add: ring_simps di_def) hence "\ (l::int). ?rc*?rx+ ?I x e = ?ri*(real (l + c*k*di))" - by (simp add: ring_eq_simps) + by (simp add: ring_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 @@ -2314,7 +2314,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_eq_simps) + 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)" 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 @@ -2446,7 +2446,7 @@ (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_eq_simps th[simplified ring_eq_simps diff_def] + by (simp add: ring_simps th[simplified ring_simps] numbound0_I[where bs="bs" and b'="real x" and b="- real x"]) next case (10 j c e) @@ -2454,7 +2454,7 @@ (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_eq_simps th[simplified ring_eq_simps diff_def] + by (simp add: ring_simps th[simplified ring_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) @@ -2540,7 +2540,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_eq_simps) + 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 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 @@ -2558,7 +2558,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_eq_simps) + 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 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 @@ -2576,7 +2576,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_eq_simps) + 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 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 @@ -2594,7 +2594,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_eq_simps) + 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 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 @@ -2612,7 +2612,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_eq_simps) + 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 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 @@ -2630,7 +2630,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_eq_simps) + 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 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 @@ -2646,7 +2646,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_eq_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: ring_simps) also 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 @@ -2663,7 +2663,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_eq_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: ring_simps) also 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 @@ -2718,7 +2718,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_eq_simps) + by (simp only: real_of_int_inject) (simp add: ring_simps) hence "\ (j::int) \ {1 .. d}. real x = - ?e + real j" by (simp add: ie[simplified isint_iff]) with nob have ?case by auto} @@ -2743,7 +2743,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_eq_simps) + hence "\ (j::int) \ {1 .. d}. x= - floor ?e - 1 + j" by (simp add: ring_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" @@ -2758,7 +2758,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_eq_simps numbound0_I[OF bn,where b="real x"and b'="a"and bs="bs"]) + simp_all add:ring_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+ @@ -2982,7 +2982,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_eq_simps) + numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti ring_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) @@ -3004,7 +3004,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_eq_simps) + numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti ring_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) @@ -3026,7 +3026,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_eq_simps) + numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti ring_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) @@ -3048,7 +3048,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_eq_simps) + numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti ring_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) @@ -3070,7 +3070,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_eq_simps) + numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti ring_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) @@ -3092,7 +3092,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_eq_simps) + numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti ring_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) @@ -3113,7 +3113,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_eq_simps) + numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti ring_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) @@ -3134,7 +3134,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_eq_simps) + numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti ring_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) @@ -3153,7 +3153,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_eq_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: ring_simps)} ultimately show ?case by blast next case (4 c e) @@ -3161,7 +3161,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_eq_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: ring_simps)} ultimately show ?case by blast next case (5 c e) @@ -3169,7 +3169,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_eq_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: ring_simps)} ultimately show ?case by blast next case (6 c e) @@ -3177,7 +3177,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_eq_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: ring_simps)} ultimately show ?case by blast next case (7 c e) @@ -3185,7 +3185,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_eq_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: ring_simps)} ultimately show ?case by blast next case (8 c e) @@ -3193,7 +3193,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_eq_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: ring_simps)} ultimately show ?case by blast next case (9 i c e) @@ -3205,7 +3205,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_eq_simps) + by (simp add: ring_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 @@ -3219,7 +3219,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_eq_simps) + by (simp add: ring_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 @@ -3232,7 +3232,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_eq_simps) + by (simp add: ring_simps) also have "\ = (\ x. ?P x)" using a\ iszlfm_gen[OF lp] kp by auto finally show ?thesis . qed @@ -3296,7 +3296,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_eq_simps)} + have ?case by (simp add: ring_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 @@ -3308,27 +3308,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_eq_simps) + ring_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_eq_simps) + ring_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_eq_simps) + from pi cp have th:"(real i +?N i e / real c)*real c > 0" by (simp add: ring_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_eq_simps + by (simp add: ring_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)" @@ -3336,7 +3336,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_eq_simps) + 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) with nob have ?case by blast } ultimately show ?case by blast next @@ -3345,13 +3345,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_eq_simps) + from pi cp have th:"(real i +?N i e / real c)*real c \ 0" by (simp add: ring_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_eq_simps + by (simp add: ring_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)" @@ -3359,9 +3359,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_eq_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] ring_simps real_of_one) hence "\ j1\ {1 .. c*d}. real (c*i) = (- ?N i e + real j1) - 1" - by (simp only: ring_eq_simps diff_def[symmetric]) + by (simp only: ring_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 } @@ -3382,10 +3382,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_eq_simps) + using ie by (simp add:ring_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_eq_simps) + by (simp add: ring_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" @@ -3402,10 +3402,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_eq_simps) + using ie by (simp add:ring_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_eq_simps) + by (simp add: ring_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" @@ -3648,7 +3648,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_eq_simps numsub numadd numfloor) + by (simp add: fp_def np ring_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 @@ -3674,7 +3674,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_eq_simps numneg numfloor numadd numsub) + by (simp add: np fp_def ring_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 @@ -3686,7 +3686,7 @@ qed next case (3 a b) thus ?case by auto -qed (auto simp add: Let_def allpairs_set split_def ring_eq_simps conj_rl) +qed (auto simp add: Let_def allpairs_set split_def ring_simps conj_rl) lemma real_in_int_intervals: assumes xb: "real m \ x \ x < real ((n::int) + 1)" @@ -3790,7 +3790,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_eq_simps numsub numadd) + using pns by (simp add: fp_def np ring_simps numsub numadd) then obtain "j" where j_def: "j\