--- 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\<Colon>'a\<Colon>ordered_field) < 0 \<Longrightarrow> ((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 "\<dots> = (0 < x)" by simp
finally show "(c*x < 0) == (x > 0)" by simp
qed
@@ -622,7 +622,7 @@
lemma pos_prod_lt:"(c\<Colon>'a\<Colon>ordered_field) > 0 \<Longrightarrow> ((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 "\<dots> = (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 "\<dots> = (-t/c < x)" by (simp only: neg_divide_less_eq[OF H] ring_eq_simps)
+ also have "\<dots> = (-t/c < x)" by (simp only: neg_divide_less_eq[OF H] ring_simps)
also have "\<dots> = ((- 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 "\<dots> = (-t/c > x)" by (simp only: pos_less_divide_eq[OF H] ring_eq_simps)
+ also have "\<dots> = (-t/c > x)" by (simp only: pos_less_divide_eq[OF H] ring_simps)
also have "\<dots> = ((- 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\<Colon>'a\<Colon>ordered_field) < 0 \<Longrightarrow> ((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 "\<dots> = (0 <= x)" by simp
finally show "(c*x <= 0) == (x >= 0)" by simp
qed
@@ -659,7 +659,7 @@
lemma pos_prod_le:"(c\<Colon>'a\<Colon>ordered_field) > 0 \<Longrightarrow> ((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 "\<dots> = (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 "\<dots> = (-t/c <= x)" by (simp only: neg_divide_le_eq[OF H] ring_eq_simps)
+ also have "\<dots> = (-t/c <= x)" by (simp only: neg_divide_le_eq[OF H] ring_simps)
also have "\<dots> = ((- 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 "\<dots> = (-t/c >= x)" by (simp only: pos_le_divide_eq[OF H] ring_eq_simps)
+ also have "\<dots> = (-t/c >= x)" by (simp only: pos_le_divide_eq[OF H] ring_simps)
also have "\<dots> = ((- 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 \<noteq> 0"
have "c*x + t = 0 = (c*x = -t)" by (subst eq_iff_diff_eq_0 [of "c*x" "-t"], simp)
- also have "\<dots> = (x = -t/c)" by (simp only: nonzero_eq_divide_eq[OF H] ring_eq_simps)
+ also have "\<dots> = (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)"
--- 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 \<noteq> (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 \<noteq> 0 \<Longrightarrow> 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"
--- 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 \<noteq> 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) \<le> (1000001 + 1) - 2"
- by simp
+by simp
lemma "(1234567::real) \<le> 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 "(\<not> x < y) = (y \<le> (x::real))"
- by arith
+by arith
lemma "\<not> (x < y \<and> y < (x::real))"
- by arith
+by arith
lemma "(x::real) < y ==> \<not> y < x"
- by arith
+by arith
lemma "((x::real) \<noteq> y) = (x < y \<or> y < x)"
- by arith
+by arith
lemma "(\<not> x \<le> y) = (y < (x::real))"
- by arith
+by arith
lemma "x \<le> y \<or> y \<le> (x::real)"
- by arith
+by arith
lemma "x \<le> y \<or> y < (x::real)"
- by arith
+by arith
lemma "x < y \<or> y \<le> (x::real)"
- by arith
+by arith
lemma "x \<le> (x::real)"
- by arith
+by arith
lemma "((x::real) \<le> y) = (x < y \<or> x = y)"
- by arith
+by arith
lemma "((x::real) \<le> y \<and> y \<le> x) = (x = y)"
- by arith
+by arith
lemma "\<not>(x < y \<and> y \<le> (x::real))"
- by arith
+by arith
lemma "\<not>(x \<le> y \<and> 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 \<le> (0::real)) = (0 \<le> x)"
- by arith
+by arith
lemma "((0::real) \<le> -x) = (x \<le> 0)"
- by arith
+by arith
lemma "(x::real) = y \<or> x < y \<or> y < x"
- by arith
+by arith
lemma "(x::real) = 0 \<or> 0 < x \<or> 0 < -x"
- by arith
+by arith
lemma "(0::real) \<le> x \<or> 0 \<le> -x"
- by arith
+by arith
lemma "((x::real) + y \<le> x + z) = (y \<le> z)"
- by arith
+by arith
lemma "((x::real) + z \<le> y + z) = (x \<le> y)"
- by arith
+by arith
lemma "(w::real) < x \<and> y < z ==> w + y < x + z"
- by arith
+by arith
lemma "(w::real) \<le> x \<and> y \<le> z ==> w + y \<le> x + z"
- by arith
+by arith
lemma "(0::real) \<le> x \<and> 0 \<le> y ==> 0 \<le> x + y"
- by arith
+by arith
lemma "(0::real) < x \<and> 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 \<le> 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) \<le> x + x) = (0 \<le> x)"
- by arith
+by arith
lemma "(-x \<le> x) = ((0::real) \<le> x)"
- by arith
+by arith
lemma "(x \<le> -x) = (x \<le> (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) \<le> x - y) = (y \<le> 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) ==> \<not>(x = y)"
- by arith
+by arith
lemma "(x \<le> x + y) = ((0::real) \<le> y)"
- by arith
+by arith
lemma "(y \<le> x + y) = ((0::real) \<le> 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 \<le> y - z) = (x + z \<le> (y::real))"
- by arith
+by arith
lemma "(x - y \<le> z) = (x \<le> z + (y::real))"
- by arith
+by arith
lemma "(-x < -y) = (y < (x::real))"
- by arith
+by arith
lemma "(-x \<le> -y) = (y \<le> (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 \<le> x \<and> y < z ==> w + y < x + (z::real)"
- by arith
+by arith
lemma "w < x \<and> y \<le> z ==> w + y < x + (z::real)"
- by arith
+by arith
lemma "(0::real) \<le> x \<and> 0 < y ==> 0 < x + (y::real)"
- by arith
+by arith
lemma "(0::real) < x \<and> 0 \<le> 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 \<le> (y::real)"
- by arith
+by arith
lemma "(0::real) < x ==> \<not>(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 \<le> b ==> c \<le> d ==> x + y < z ==> a + c \<le> b + d"
- by (tactic "fast_arith_tac 1")
+by (tactic "fast_arith_tac 1")
lemma "!!a::real. a < b ==> c < d ==> a - d \<le> b + (-c)"
- by (tactic "fast_arith_tac 1")
+by (tactic "fast_arith_tac 1")
lemma "!!a::real. a \<le> b ==> b + b \<le> c ==> a + a \<le> c"
- by (tactic "fast_arith_tac 1")
+by (tactic "fast_arith_tac 1")
lemma "!!a::real. a + b \<le> i + j ==> a \<le> b ==> i \<le> j ==> a + a \<le> 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 \<le> i + j + k \<and> a \<le> b \<and> b \<le> c \<and> i \<le> j \<and> j \<le> k --> a + a + a \<le> k + k + k"
- by arith
+by arith
lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a \<le> l"
- by (tactic "fast_arith_tac 1")
+by (tactic "fast_arith_tac 1")
lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a \<le> l + l + l + l"
- by (tactic "fast_arith_tac 1")
+by (tactic "fast_arith_tac 1")
lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a + a \<le> l + l + l + l + i"
- by (tactic "fast_arith_tac 1")
+by (tactic "fast_arith_tac 1")
lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a + a + a \<le> 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!*}
--- 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 \<noteq> 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 \<noteq> 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 \<Rightarrow> int \<Rightarrow> 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 \<le> 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 \<le> 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]: "\<lbrakk> numbound0 t ; numbound0 s\<rbrakk> \<Longrightarrow> numbound0 (numadd (t,s))"
by (induct t s rule: numadd.induct, auto simp add: Let_def)
@@ -874,7 +874,7 @@
"nummul t = (\<lambda> i. Mul i t)"
lemma nummul[simp]: "\<And> 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]: "\<And> i. numbound0 t \<Longrightarrow> 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 \<Longrightarrow> numbound0 (fst (split_int t)) \<and> 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 \<ge>0) = (real (-a) + (-b) \<le> 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 \<and> 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 "\<exists> (l::int). ?rt = ?ri * (real l)" by (simp add: rdvd_def)
hence "\<exists> (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 "\<exists> (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 "\<exists> (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 "\<exists> (l::int). ?rc*?rx+?e = ?ri * (real l)" by (simp add: rdvd_def)
hence "\<exists> (l::int). ?rc*?rx - real c * (real k * real d) +?e = ?ri * (real l) - real c * (real k * real d)" by simp
hence "\<exists> (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 "\<exists> (l::int). ?rc*?rx - real c * (real k * real d) +?e = ?ri * (real (l - c*k*di))" by (simp add: ring_eq_simps)
+ hence "\<exists> (l::int). ?rc*?rx - real c * (real k * real d) +?e = ?ri * (real (l - c*k*di))" by (simp add: ring_simps)
hence "\<exists> (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 "\<exists> (l::int). ?rt = ?ri * (real l)" by (simp add: rdvd_def)
hence "\<exists> (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 "\<exists> (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 "\<exists> (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 "\<exists> (l::int). ?rc*?rx+?e = ?ri * (real l)" by (simp add: rdvd_def)
hence "\<exists> (l::int). ?rc*?rx - real c * (real k * real d) +?e = ?ri * (real l) - real c * (real k * real d)" by simp
hence "\<exists> (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 "\<exists> (l::int). ?rc*?rx - real c * (real k * real d) +?e = ?ri * (real (l - c*k*di))" by (simp add: ring_eq_simps)
+ hence "\<exists> (l::int). ?rc*?rx - real c * (real k * real d) +?e = ?ri * (real (l - c*k*di))" by (simp add: ring_simps)
hence "\<exists> (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\<Colon>real)) =
(real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e < 0)"
by simp
- also have "\<dots> = (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 "\<dots> = (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 "\<dots> = (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 \<le> (0\<Colon>real)) =
(real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e \<le> 0)"
by simp
- also have "\<dots> = (real (l div c) * (real c * real x + Inum (real x # bs) e) \<le> (real (l div c)) * 0)" by (simp add: ring_eq_simps)
+ also have "\<dots> = (real (l div c) * (real c * real x + Inum (real x # bs) e) \<le> (real (l div c)) * 0)" by (simp add: ring_simps)
also have "\<dots> = (real c * real x + Inum (real x # bs) e \<le> 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\<Colon>real)) =
(real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e > 0)"
by simp
- also have "\<dots> = (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 "\<dots> = (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 "\<dots> = (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 \<ge> (0\<Colon>real)) =
(real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e \<ge> 0)"
by simp
- also have "\<dots> = (real (l div c) * (real c * real x + Inum (real x # bs) e) \<ge> (real (l div c)) * 0)" by (simp add: ring_eq_simps)
+ also have "\<dots> = (real (l div c) * (real c * real x + Inum (real x # bs) e) \<ge> (real (l div c)) * 0)" by (simp add: ring_simps)
also have "\<dots> = (real c * real x + Inum (real x # bs) e \<ge> 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\<Colon>real)) =
(real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e = 0)"
by simp
- also have "\<dots> = (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 "\<dots> = (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 "\<dots> = (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 \<noteq> (0\<Colon>real)) =
(real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e \<noteq> 0)"
by simp
- also have "\<dots> = (real (l div c) * (real c * real x + Inum (real x # bs) e) \<noteq> (real (l div c)) * 0)" by (simp add: ring_eq_simps)
+ also have "\<dots> = (real (l div c) * (real c * real x + Inum (real x # bs) e) \<noteq> (real (l div c)) * 0)" by (simp add: ring_simps)
also have "\<dots> = (real c * real x + Inum (real x # bs) e \<noteq> 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 "(\<exists> (k::int). real l * real x + real (l div c) * Inum (real x # bs) e = (real (l div c) * real j) * real k) = (\<exists> (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 "\<dots> = (\<exists> (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 "\<dots> = (\<exists> (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 "\<dots> = (\<exists> (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 "\<dots> = (\<exists> (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 "(\<exists> (k::int). real l * real x + real (l div c) * Inum (real x # bs) e = (real (l div c) * real j) * real k) = (\<exists> (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 "\<dots> = (\<exists> (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 "\<dots> = (\<exists> (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 "\<dots> = (\<exists> (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 "\<dots> = (\<exists> (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 \<ge> 1 \<and> x + floor ?e \<le> d" by simp
hence "\<exists> (j::int) \<in> {1 .. d}. j = x + floor ?e" by simp
hence "\<exists> (j::int) \<in> {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 "\<exists> (j::int) \<in> {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 \<ge> 1 \<and> x + floor ?e + 1 \<le> d" by simp
hence "\<exists> (j::int) \<in> {1 .. d}. j = x + floor ?e + 1" by simp
- hence "\<exists> (j::int) \<in> {1 .. d}. x= - floor ?e - 1 + j" by (simp add: ring_eq_simps)
+ hence "\<exists> (j::int) \<in> {1 .. d}. x= - floor ?e - 1 + j" by (simp add: ring_simps)
hence "\<exists> (j::int) \<in> {1 .. d}. real x= real (- floor ?e - 1 + j)"
by (simp only: real_of_int_inject)
hence "\<exists> (j::int) \<in> {1 .. d}. real x= - ?e - 1 + real j"
@@ -2758,7 +2758,7 @@
have vb: "?v \<in> set (\<beta> (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 "\<dots> = (?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 \<noteq> 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 "\<dots> = (?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 "\<dots> = (?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 \<le> 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 "\<dots> = (?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 "\<dots> = (?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 \<ge> 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 "\<dots> = (?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 "\<dots> = (?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))) = (\<not> (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 "\<dots> = (?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\<noteq>0" by simp hence knz': "real k \<noteq> 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: "\<not> 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: "\<not> 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\<noteq>0" by simp hence knz': "real k \<noteq> 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: "\<not> 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: "\<not> 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\<noteq>0" by simp hence knz': "real k \<noteq> 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: "\<not> 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: "\<not> 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\<noteq>0" by simp hence knz': "real k \<noteq> 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: "\<not> 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: "\<not> 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\<noteq>0" by simp hence knz': "real k \<noteq> 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: "\<not> 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: "\<not> 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\<noteq>0" by simp hence knz': "real k \<noteq> 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: "\<not> 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: "\<not> 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\<rho> (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 "\<dots> = (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\<rho> (NDvd i (CN 0 c e)) k) =
(\<not> (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 "\<dots> = (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 "(\<exists> x. ?D x \<and> ?P' x) = (\<exists> x. k dvd x \<and> ?P' x)" using int_rdvd_iff by simp
also have "\<dots> = (\<exists>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 "\<dots> = (\<exists> x. ?P x)" using a\<rho> iszlfm_gen[OF lp] kp by auto
finally show ?thesis .
qed
@@ -3296,7 +3296,7 @@
by simp+
{assume "real (c*i) \<noteq> - ?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) \<in> {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: "\<forall> j\<in> {1 .. c*d}. real (c*i) \<noteq> - ?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) \<or> real (c*i) + ?N i e \<le> 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 \<le> real (c*d)"
@@ -3336,7 +3336,7 @@
hence pid: "c*i + ?fe \<le> c*d" by (simp only: real_of_int_le_iff)
with pi' have "\<exists> j1\<in> {1 .. c*d}. c*i + ?fe = j1" by auto
hence "\<exists> j1\<in> {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 \<ge> 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 \<ge> 0" by (simp add: ring_eq_simps)
+ from pi cp have th:"(real i +?N i e / real c)*real c \<ge> 0" by (simp add: ring_simps)
from pi ei[simplified isint_iff] have "real (c*i + ?fe) \<ge> real (0::int)" by simp
hence pi': "c*i + 1 + ?fe \<ge> 1" by (simp only: real_of_int_le_iff[symmetric])
have "real (c*i) + ?N i e \<ge> real (c*d) \<or> real (c*i) + ?N i e < real (c*d)" by auto
moreover
{assume "real (c*i) + ?N i e \<ge> 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 \<le> c*d" by (simp only: real_of_int_le_iff)
with pi' have "\<exists> j1\<in> {1 .. c*d}. c*i + 1+ ?fe = j1" by auto
hence "\<exists> j1\<in> {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 "\<exists> j1\<in> {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 "\<exists> j1\<in> {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 "\<dots> = (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: "\<not> (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 "\<dots> = 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 \<sigma>_nb: assumes lp: "iszlfm p (a#bs)" and nb: "numbound0 t"
@@ -3648,7 +3648,7 @@
from H
have "?I (?p (p',n',s') j) \<longrightarrow>
(((?N ?nxs \<ge> real ?l) \<and> (?N ?nxs < real (?l + 1))) \<and> (?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 "\<dots> \<longrightarrow> ((floor (?N ?nxs) = ?l) \<and> (?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) \<longrightarrow>
(((?N ?nxs \<ge> real ?l) \<and> (?N ?nxs < real (?l + 1))) \<and> (?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 "\<dots> \<longrightarrow> ((floor (?N ?nxs) = ?l) \<and> (?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 \<le> x \<and> x < real ((n::int) + 1)"
@@ -3790,7 +3790,7 @@
hence "\<exists> j\<in> {0 .. n}. 0 \<le> real n *x + ?N s - ?N (Floor s) - real j \<and> 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 "\<exists> j\<in> {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\<in> {0 .. n} \<and> ?I (?p (p,n,s) j)" by blast
hence "\<exists>x \<in> {?p (p,n,s) j |j. 0\<le> j \<and> j \<le> n }. ?I x" by auto
hence ?case using pns
@@ -3808,7 +3808,7 @@
have "real n *x + ?N s \<ge> real n + ?N s" by simp
moreover from real_of_int_floor_le[where r="?N s"] have "real n + ?N s \<ge> real n + ?N (Floor s)" by simp
ultimately have "real n *x + ?N s \<ge> ?N (Floor s) + real n"
- by (simp only: ring_eq_simps)}
+ by (simp only: ring_simps)}
ultimately have "?N (Floor s) + real n \<le> real n *x + ?N s\<and> real n *x + ?N s < ?N (Floor s) + real (1::int)" by simp
hence th: "real n \<le> real n *x + ?N s - ?N (Floor s) \<and> real n *x + ?N s - ?N (Floor s) < real (1::int)" by simp
have th1: "\<forall> (a::real). (- a > 0) = (a < 0)" by auto
@@ -3911,7 +3911,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_eq_simps myless[rule_format, where b="0"])
+ (cases "n > 0", simp_all add: lt_def ring_simps myless[rule_format, where b="0"])
qed
lemma lt_l: "isrlfm (rsplit lt a)"
@@ -3923,7 +3923,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_eq_simps myl[rule_format, where b="0"])
+ (cases "n > 0", simp_all add: le_def ring_simps myl[rule_format, where b="0"])
qed
lemma le_l: "isrlfm (rsplit le a)"
@@ -3935,7 +3935,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_eq_simps myless[rule_format, where b="0"])
+ (cases "n > 0", simp_all add: gt_def ring_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)
@@ -3946,7 +3946,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_eq_simps myl[rule_format, where b="0"])
+ (cases "n > 0", simp_all add: ge_def ring_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)
@@ -3956,7 +3956,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_eq_simps)
+ show "?I (eq n s) = ?I (Eq a)" using H by (auto simp add: eq_def ring_simps)
qed
lemma eq_l: "isrlfm (rsplit eq a)"
by (rule rsplit_l[where f="eq" and a="a"], auto simp add: eq_def)
@@ -3966,7 +3966,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_eq_simps)
+ show "?I (neq n s) = ?I (NEq a)" using H by (auto simp add: neq_def ring_simps)
qed
lemma neq_l: "isrlfm (rsplit neq a)"
@@ -4010,10 +4010,10 @@
also have "\<dots> = (?DE \<and> ?a \<ge> 0 \<and> ?a < n)" by(simp only: small_le[OF ss0 ss1] small_lt[OF ss0 ss1])
also have "\<dots> = (?DE \<and> (\<exists> j\<in> {0 .. (n - 1)}. ?a = j))" by simp
also have "\<dots> = (?DE \<and> (\<exists> j\<in> {0 .. (n - 1)}. real (\<lfloor>real n * u - s\<rfloor>) = real j - real \<lfloor>s\<rfloor> ))"
- by (simp only: ring_eq_simps real_of_int_diff[symmetric] real_of_int_inject del: real_of_int_diff)
+ by (simp only: ring_simps real_of_int_diff[symmetric] real_of_int_inject del: real_of_int_diff)
also have "\<dots> = ((\<exists> j\<in> {0 .. (n - 1)}. real n * u - s = real j - real \<lfloor>s\<rfloor> \<and> real i rdvd real n * u - s))" using int_rdvd_iff[where i="i" and t="\<lfloor>real n * u - s\<rfloor>"]
by (auto cong: conj_cong)
- also have "\<dots> = ?rhs" by(simp cong: conj_cong) (simp add: ring_eq_simps )
+ also have "\<dots> = ?rhs" by(simp cong: conj_cong) (simp add: ring_simps )
finally show ?thesis .
qed
@@ -4029,7 +4029,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) = (\<exists> j\<in> {0 .. (n - 1)}. Ifm (x#bs) (?f j))"
by (simp add: iupt_set np DVDJ_def del: iupt.simps)
- also have "\<dots> = (\<exists> j\<in> {0 .. (n - 1)}. real n * x = (- ?s) - real (floor (- ?s)) + real j \<and> real i rdvd real (j - floor (- ?s)))" by (simp add: ring_eq_simps diff_def[symmetric])
+ also have "\<dots> = (\<exists> j\<in> {0 .. (n - 1)}. real n * x = (- ?s) - real (floor (- ?s)) + real j \<and> real i rdvd real (j - floor (- ?s)))" by (simp add: ring_simps diff_def[symmetric])
also from rdvd01_cs[OF xp x1 np, where i="i" and s="-?s"]
have "\<dots> = (real i rdvd real n * x - (-?s))" by simp
finally show ?thesis by simp
@@ -4044,7 +4044,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) = (\<forall> j\<in> {0 .. (n - 1)}. Ifm (x#bs) (?f j))"
by (simp add: iupt_set np NDVDJ_def del: iupt.simps)
- also have "\<dots> = (\<not> (\<exists> j\<in> {0 .. (n - 1)}. real n * x = (- ?s) - real (floor (- ?s)) + real j \<and> real i rdvd real (j - floor (- ?s))))" by (simp add: ring_eq_simps diff_def[symmetric])
+ also have "\<dots> = (\<not> (\<exists> j\<in> {0 .. (n - 1)}. real n * x = (- ?s) - real (floor (- ?s)) + real j \<and> real i rdvd real (j - floor (- ?s))))" by (simp add: ring_simps diff_def[symmetric])
also from rdvd01_cs[OF xp x1 np, where i="i" and s="-?s"]
have "\<dots> = (\<not> (real i rdvd real n * x - (-?s)))" by simp
finally show ?thesis by simp
@@ -4630,40 +4630,40 @@
using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
also have "\<dots> = (?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_eq_simps)
+ and b="0", simplified divide_zero_left]) (simp only: ring_simps)
also have "\<dots> = (real c *?t + ?n* (?N x e) < 0)"
using np by simp
- finally show ?case using nbt nb by (simp add: ring_eq_simps)
+ finally show ?case using nbt nb by (simp add: ring_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) \<le> 0)"
using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) \<le> 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_eq_simps)
+ and b="0", simplified divide_zero_left]) (simp only: ring_simps)
also have "\<dots> = (real c *?t + ?n* (?N x e) \<le> 0)"
using np by simp
- finally show ?case using nbt nb by (simp add: ring_eq_simps)
+ finally show ?case using nbt nb by (simp add: ring_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 "\<dots> = (?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_eq_simps)
+ and b="0", simplified divide_zero_left]) (simp only: ring_simps)
also have "\<dots> = (real c *?t + ?n* (?N x e) > 0)"
using np by simp
- finally show ?case using nbt nb by (simp add: ring_eq_simps)
+ finally show ?case using nbt nb by (simp add: ring_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) \<ge> 0)"
using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) \<ge> 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_eq_simps)
+ and b="0", simplified divide_zero_left]) (simp only: ring_simps)
also have "\<dots> = (real c *?t + ?n* (?N x e) \<ge> 0)"
using np by simp
- finally show ?case using nbt nb by (simp add: ring_eq_simps)
+ finally show ?case using nbt nb by (simp add: ring_simps)
next
case (3 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+
from np have np: "real n \<noteq> 0" by simp
@@ -4671,10 +4671,10 @@
using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
also have "\<dots> = (?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_eq_simps)
+ and b="0", simplified divide_zero_left]) (simp only: ring_simps)
also have "\<dots> = (real c *?t + ?n* (?N x e) = 0)"
using np by simp
- finally show ?case using nbt nb by (simp add: ring_eq_simps)
+ finally show ?case using nbt nb by (simp add: ring_simps)
next
case (4 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+
from np have np: "real n \<noteq> 0" by simp
@@ -4682,10 +4682,10 @@
using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) \<noteq> 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_eq_simps)
+ and b="0", simplified divide_zero_left]) (simp only: ring_simps)
also have "\<dots> = (real c *?t + ?n* (?N x e) \<noteq> 0)"
using np by simp
- finally show ?case using nbt nb by (simp add: ring_eq_simps)
+ finally show ?case using nbt nb by (simp add: ring_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 \<Upsilon>_l:
@@ -4736,7 +4736,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_eq_simps)
+ from prems have "x * real c + ?N x e < 0" by (simp add: ring_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:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
@@ -4745,7 +4745,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_eq_simps)
+ hence "real c * y + ?N x e < 0" by (simp add: ring_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
@@ -4755,7 +4755,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 \<le> 0" by (simp add: ring_eq_simps)
+ from prems have "x * real c + ?N x e \<le> 0" by (simp add: ring_simps)
hence pxc: "x \<le> (- ?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:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
@@ -4764,7 +4764,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_eq_simps)
+ hence "real c * y + ?N x e < 0" by (simp add: ring_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
@@ -4774,7 +4774,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_eq_simps)
+ from prems have "x * real c + ?N x e > 0" by (simp add: ring_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:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
@@ -4783,7 +4783,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_eq_simps)
+ hence "real c * y + ?N x e > 0" by (simp add: ring_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
@@ -4793,7 +4793,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 \<ge> 0" by (simp add: ring_eq_simps)
+ from prems have "x * real c + ?N x e \<ge> 0" by (simp add: ring_simps)
hence pxc: "x \<ge> (- ?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:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
@@ -4802,7 +4802,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_eq_simps)
+ hence "real c * y + ?N x e > 0" by (simp add: ring_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
@@ -4813,7 +4813,7 @@
next
case (3 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+
from cp have cnz: "real c \<noteq> 0" by simp
- from prems have "x * real c + ?N x e = 0" by (simp add: ring_eq_simps)
+ from prems have "x * real c + ?N x e = 0" by (simp add: ring_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:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
@@ -4826,9 +4826,9 @@
with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto
hence "y* real c \<noteq> -?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 \<noteq> 0" by (simp add: ring_eq_simps)
+ hence "y* real c + ?N x e \<noteq> 0" by (simp add: ring_simps)
thus ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"]
- by (simp add: ring_eq_simps)
+ by (simp add: ring_simps)
qed (auto simp add: nth_pos2 numbound0_I[where bs="bs" and b="y" and b'="x"])
lemma finite_set_intervals:
@@ -4991,7 +4991,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_eq_simps add_divide_distrib)
+ using mnp mp np by (simp add: ring_simps add_divide_distrib)
from \<upsilon>_I[OF lp mnp st_nb, where x="x" and bs="bs"]
have "?I x (\<upsilon> p (?st,2*n*m)) = ?I ((?N t / real n + ?N s / real m) /2) p" by (simp only: st[symmetric])}
with rinf_\<Upsilon>[OF lp nmi npi px] have "?F" by blast hence "?D" by blast}
@@ -5060,7 +5060,7 @@
lemma exsplitnum:
"Inum (x#y#bs) (exsplitnum t) = Inum ((x+y) #bs) t"
- by(induct t rule: exsplitnum.induct) (simp_all add: ring_eq_simps)
+ by(induct t rule: exsplitnum.induct) (simp_all add: ring_simps)
lemma exsplit:
assumes qfp: "qfree p"
@@ -5151,14 +5151,14 @@
from Ul th have mnz: "m \<noteq> 0" by auto
from Ul th have nnz: "n \<noteq> 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_eq_simps add_divide_distrib)
+ using mnz nnz by (simp add: ring_simps add_divide_distrib)
thus "(real m * Inum (x # bs) t + real n * Inum (x # bs) s) /
(2 * real n * real m)
\<in> (\<lambda>((t, n), s, m).
(Inum (x # bs) t / real n + Inum (x # bs) s / real m) / 2) `
(set U \<times> set U)"using mnz nnz th
- apply (auto simp add: th add_divide_distrib ring_eq_simps split_def image_def)
+ apply (auto simp add: th add_divide_distrib ring_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
@@ -5169,7 +5169,7 @@
from Ul smU have mnz: "m \<noteq> 0" by auto
from Ul tnU have nnz: "n \<noteq> 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_eq_simps add_divide_distrib)
+ using mnz nnz by (simp add: ring_simps add_divide_distrib)
let ?P = "\<lambda> (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:"\<forall> a b. ?P a b = ?P b a"
by auto
@@ -5182,7 +5182,7 @@
from ts'_U Up have mnz': "m' \<noteq> 0" and nnz': "n'\<noteq> 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_eq_simps add_divide_distrib)
+ using mnz' nnz' by (simp add: ring_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 "\<dots> = ((\<lambda>(t, n). Inum (x # bs) t / real n) ((\<lambda>((t, n), s, m). (Add (Mul m t) (Mul n s), 2 * n * m)) ((t',n'),(s',m'))))" by (simp add: st')
@@ -5212,7 +5212,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_eq_simps add_divide_distrib)
+ using mp np by (simp add: ring_simps add_divide_distrib)
from tnU smU UU' have "?g ((t,n),(s,m)) \<in> ?f ` U'" by blast
hence "\<exists> (t',n') \<in> U'. ?g ((t,n),(s,m)) = ?f (t',n')"
by auto (rule_tac x="(a,b)" in bexI, auto)
@@ -5240,7 +5240,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_eq_simps add_divide_distrib)
+ using mp np by (simp add: ring_simps add_divide_distrib)
from U' tnU' have tnb': "numbound0 t'" and np': "real n' > 0" by auto
from \<upsilon>_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
--- a/src/HOL/Complex/ex/ReflectedFerrack.thy Fri Jun 22 22:41:17 2007 +0200
+++ b/src/HOL/Complex/ex/ReflectedFerrack.thy Sat Jun 23 19:33:22 2007 +0200
@@ -533,7 +533,7 @@
next
case (2 n c t) hence gd: "g dvd c" by simp
from gp have gnz: "g \<noteq> 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 \<Rightarrow> int \<Rightarrow> bool"
recdef ismaxcoeff "measure size"
@@ -637,8 +637,8 @@
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 \<le> n2", simp_all)
-apply (case_tac "n1 = n2", simp_all add: ring_eq_simps)
-by (simp only: ring_eq_simps(1)[symmetric],simp)
+apply (case_tac "n1 = n2", simp_all add: ring_simps)
+by (simp only: left_distrib[symmetric],simp)
lemma numadd_nb[simp]: "\<lbrakk> numbound0 t ; numbound0 s\<rbrakk> \<Longrightarrow> numbound0 (numadd (t,s))"
by (induct t s rule: numadd.induct, auto simp add: Let_def)
@@ -649,7 +649,7 @@
"nummul t = (\<lambda> i. Mul i t)"
lemma nummul[simp]: "\<And> 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]: "\<And> i. numbound0 t \<Longrightarrow> numbound0 (nummul t i)"
by (induct t rule: nummul.induct, auto )
@@ -1002,10 +1002,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_eq_simps)
+ by (simp add: Let_def split_def ring_simps)
also have "\<dots> = 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_eq_simps , simp add: ring_eq_simps(2)[symmetric])
+qed(auto simp add: Let_def split_def ring_simps , simp add: right_distrib[symmetric])
(* Linearize a formula*)
consts
@@ -1370,40 +1370,40 @@
using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
also have "\<dots> = (?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_eq_simps)
+ and b="0", simplified divide_zero_left]) (simp only: ring_simps)
also have "\<dots> = (real c *?t + ?n* (?N x e) < 0)"
using np by simp
- finally show ?case using nbt nb by (simp add: ring_eq_simps)
+ finally show ?case using nbt nb by (simp add: ring_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) \<le> 0)"
using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) \<le> 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_eq_simps)
+ and b="0", simplified divide_zero_left]) (simp only: ring_simps)
also have "\<dots> = (real c *?t + ?n* (?N x e) \<le> 0)"
using np by simp
- finally show ?case using nbt nb by (simp add: ring_eq_simps)
+ finally show ?case using nbt nb by (simp add: ring_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 "\<dots> = (?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_eq_simps)
+ and b="0", simplified divide_zero_left]) (simp only: ring_simps)
also have "\<dots> = (real c *?t + ?n* (?N x e) > 0)"
using np by simp
- finally show ?case using nbt nb by (simp add: ring_eq_simps)
+ finally show ?case using nbt nb by (simp add: ring_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) \<ge> 0)"
using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) \<ge> 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_eq_simps)
+ and b="0", simplified divide_zero_left]) (simp only: ring_simps)
also have "\<dots> = (real c *?t + ?n* (?N x e) \<ge> 0)"
using np by simp
- finally show ?case using nbt nb by (simp add: ring_eq_simps)
+ finally show ?case using nbt nb by (simp add: ring_simps)
next
case (3 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+
from np have np: "real n \<noteq> 0" by simp
@@ -1411,10 +1411,10 @@
using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
also have "\<dots> = (?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_eq_simps)
+ and b="0", simplified divide_zero_left]) (simp only: ring_simps)
also have "\<dots> = (real c *?t + ?n* (?N x e) = 0)"
using np by simp
- finally show ?case using nbt nb by (simp add: ring_eq_simps)
+ finally show ?case using nbt nb by (simp add: ring_simps)
next
case (4 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+
from np have np: "real n \<noteq> 0" by simp
@@ -1422,10 +1422,10 @@
using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) \<noteq> 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_eq_simps)
+ and b="0", simplified divide_zero_left]) (simp only: ring_simps)
also have "\<dots> = (real c *?t + ?n* (?N x e) \<noteq> 0)"
using np by simp
- finally show ?case using nbt nb by (simp add: ring_eq_simps)
+ finally show ?case using nbt nb by (simp add: ring_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:
@@ -1476,7 +1476,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_eq_simps)
+ from prems have "x * real c + ?N x e < 0" by (simp add: ring_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:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
@@ -1485,7 +1485,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_eq_simps)
+ hence "real c * y + ?N x e < 0" by (simp add: ring_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
@@ -1495,7 +1495,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 \<le> 0" by (simp add: ring_eq_simps)
+ from prems have "x * real c + ?N x e \<le> 0" by (simp add: ring_simps)
hence pxc: "x \<le> (- ?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:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
@@ -1504,7 +1504,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_eq_simps)
+ hence "real c * y + ?N x e < 0" by (simp add: ring_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
@@ -1514,7 +1514,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_eq_simps)
+ from prems have "x * real c + ?N x e > 0" by (simp add: ring_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:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
@@ -1523,7 +1523,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_eq_simps)
+ hence "real c * y + ?N x e > 0" by (simp add: ring_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
@@ -1533,7 +1533,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 \<ge> 0" by (simp add: ring_eq_simps)
+ from prems have "x * real c + ?N x e \<ge> 0" by (simp add: ring_simps)
hence pxc: "x \<ge> (- ?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:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
@@ -1542,7 +1542,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_eq_simps)
+ hence "real c * y + ?N x e > 0" by (simp add: ring_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
@@ -1553,7 +1553,7 @@
next
case (3 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+
from cp have cnz: "real c \<noteq> 0" by simp
- from prems have "x * real c + ?N x e = 0" by (simp add: ring_eq_simps)
+ from prems have "x * real c + ?N x e = 0" by (simp add: ring_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:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
@@ -1566,9 +1566,9 @@
with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto
hence "y* real c \<noteq> -?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 \<noteq> 0" by (simp add: ring_eq_simps)
+ hence "y* real c + ?N x e \<noteq> 0" by (simp add: ring_simps)
thus ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"]
- by (simp add: ring_eq_simps)
+ by (simp add: ring_simps)
qed (auto simp add: nth_pos2 numbound0_I[where bs="bs" and b="y" and b'="x"])
lemma finite_set_intervals:
@@ -1731,7 +1731,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_eq_simps add_divide_distrib)
+ using mnp mp np by (simp add: ring_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}
@@ -1782,14 +1782,14 @@
from Ul th have mnz: "m \<noteq> 0" by auto
from Ul th have nnz: "n \<noteq> 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_eq_simps add_divide_distrib)
+ using mnz nnz by (simp add: ring_simps add_divide_distrib)
thus "(real m * Inum (x # bs) t + real n * Inum (x # bs) s) /
(2 * real n * real m)
\<in> (\<lambda>((t, n), s, m).
(Inum (x # bs) t / real n + Inum (x # bs) s / real m) / 2) `
(set U \<times> set U)"using mnz nnz th
- apply (auto simp add: th add_divide_distrib ring_eq_simps split_def image_def)
+ apply (auto simp add: th add_divide_distrib ring_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
@@ -1800,7 +1800,7 @@
from Ul smU have mnz: "m \<noteq> 0" by auto
from Ul tnU have nnz: "n \<noteq> 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_eq_simps add_divide_distrib)
+ using mnz nnz by (simp add: ring_simps add_divide_distrib)
let ?P = "\<lambda> (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:"\<forall> a b. ?P a b = ?P b a"
by auto
@@ -1813,7 +1813,7 @@
from ts'_U Up have mnz': "m' \<noteq> 0" and nnz': "n'\<noteq> 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_eq_simps add_divide_distrib)
+ using mnz' nnz' by (simp add: ring_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 "\<dots> = ((\<lambda>(t, n). Inum (x # bs) t / real n) ((\<lambda>((t, n), s, m). (Add (Mul m t) (Mul n s), 2 * n * m)) ((t',n'),(s',m'))))" by (simp add: st')
@@ -1843,7 +1843,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_eq_simps add_divide_distrib)
+ using mp np by (simp add: ring_simps add_divide_distrib)
from tnU smU UU' have "?g ((t,n),(s,m)) \<in> ?f ` U'" by blast
hence "\<exists> (t',n') \<in> U'. ?g ((t,n),(s,m)) = ?f (t',n')"
by auto (rule_tac x="(a,b)" in bexI, auto)
@@ -1871,7 +1871,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_eq_simps add_divide_distrib)
+ using mp np by (simp add: ring_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
@@ -1972,8 +1972,6 @@
using ferrack qelim_ci prep
unfolding linrqe_def by auto
-declare max_def [code unfold]
-
code_module Ferrack
file "generated_ferrack.ML"
contains linrqe = "linrqe"
--- a/src/HOL/Finite_Set.thy Fri Jun 22 22:41:17 2007 +0200
+++ b/src/HOL/Finite_Set.thy Sat Jun 23 19:33:22 2007 +0200
@@ -970,12 +970,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_eq_simps)
+ by (subst setsum_Un_Int [symmetric], auto simp add: ring_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_eq_simps)
+ by (subst setsum_Un_Int [symmetric], auto simp add: ring_simps)
lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) =
(if a:A then setsum f A - f a else setsum f A)"
@@ -1649,7 +1649,7 @@
lemma setsum_constant [simp]: "(\<Sum>x \<in> A. y) = of_nat(card A) * y"
apply (cases "finite A")
apply (erule finite_induct)
-apply (auto simp add: ring_distrib add_ac)
+apply (auto simp add: ring_simps)
done
lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{recpower, comm_monoid_mult})) = y^(card A)"
--- a/src/HOL/Groebner_Basis.thy Fri Jun 22 22:41:17 2007 +0200
+++ b/src/HOL/Groebner_Basis.thy Sat Jun 23 19:33:22 2007 +0200
@@ -168,7 +168,7 @@
interpretation class_semiring: gb_semiring
["op +" "op *" "op ^" "0::'a::{comm_semiring_1, recpower}" "1"]
- by unfold_locales (auto simp add: ring_eq_simps power_Suc)
+ by unfold_locales (auto simp add: ring_simps power_Suc)
lemmas nat_arith =
add_nat_number_of diff_nat_number_of mult_nat_number_of eq_nat_number_of less_nat_number_of
@@ -341,13 +341,13 @@
interpretation class_ringb: ringb
["op +" "op *" "op ^" "0::'a::{idom,recpower,number_ring}" "1" "op -" "uminus"]
-proof(unfold_locales, simp add: ring_eq_simps power_Suc, auto)
+proof(unfold_locales, simp add: ring_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 \<noteq> z"
hence ynz': "y - z \<noteq> 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_eq_simps)
- hence "(y - z) * (w - x) = 0" by (simp add: ring_eq_simps)
+ hence "w* (y - z) - x * (y - z) = 0" by (simp add: ring_simps)
+ hence "(y - z) * (w - x) = 0" by (simp add: ring_simps)
with no_zero_divirors_neq0 [OF ynz']
have "w - x = 0" by blast
thus "w = x" by simp
@@ -368,20 +368,20 @@
interpretation natgb: semiringb
["op +" "op *" "op ^" "0::nat" "1"]
-proof (unfold_locales, simp add: ring_eq_simps power_Suc)
+proof (unfold_locales, simp add: ring_simps power_Suc)
fix w x y z ::"nat"
{ assume p: "w * y + x * z = w * z + x * y" and ynz: "y \<noteq> z"
hence "y < z \<or> y > z" by arith
moreover {
assume lt:"y <z" hence "\<exists>k. z = y + k \<and> 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_eq_simps)
+ from p have "(w * y + x *y) + x*k = (w * y + x*y) + w*k" by (simp add: yz ring_simps)
hence "x*k = w*k" by simp
hence "w = x" using kp by (simp add: mult_cancel2) }
moreover {
assume lt: "y >z" hence "\<exists>k. y = z + k \<and> 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_eq_simps)
+ from p have "(w * z + x *z) + w*k = (w * z + x*z) + x*k" by (simp add: yz ring_simps)
hence "w*k = x*k" by simp
hence "w = x" using kp by (simp add: mult_cancel2)}
ultimately have "w=x" by blast }
--- a/src/HOL/Hyperreal/Deriv.thy Fri Jun 22 22:41:17 2007 +0200
+++ b/src/HOL/Hyperreal/Deriv.thy Sat Jun 23 19:33:22 2007 +0200
@@ -89,7 +89,7 @@
lemma DERIV_mult_lemma:
fixes a b c d :: "'a::real_field"
shows "(a * b - c * d) / h = a * ((b - d) / h) + ((a - c) / h) * d"
-by (simp add: diff_minus add_divide_distrib [symmetric] ring_distrib)
+by (simp add: diff_minus add_divide_distrib [symmetric] ring_distribs)
lemma DERIV_mult':
assumes f: "DERIV f x :> D"
@@ -147,7 +147,7 @@
lemma inverse_diff_inverse:
"\<lbrakk>(a::'a::division_ring) \<noteq> 0; b \<noteq> 0\<rbrakk>
\<Longrightarrow> inverse a - inverse b = - (inverse a * (a - b) * inverse b)"
-by (simp add: right_diff_distrib left_diff_distrib mult_assoc)
+by (simp add: ring_simps)
lemma DERIV_inverse_lemma:
"\<lbrakk>a \<noteq> 0; b \<noteq> (0::'a::real_normed_field)\<rbrakk>
@@ -198,7 +198,7 @@
apply (unfold divide_inverse)
apply (erule DERIV_mult')
apply (erule (1) DERIV_inverse')
-apply (simp add: left_diff_distrib nonzero_inverse_mult_distrib)
+apply (simp add: ring_distribs nonzero_inverse_mult_distrib)
apply (simp add: mult_ac)
done
@@ -211,7 +211,7 @@
show ?case by (simp add: power_Suc f)
case (Suc k)
from DERIV_mult' [OF f Suc] show ?case
- apply (simp only: of_nat_Suc left_distrib mult_1_left)
+ apply (simp only: of_nat_Suc ring_distribs mult_1_left)
apply (simp only: power_Suc right_distrib mult_ac add_ac)
done
qed
@@ -1050,7 +1050,7 @@
apply (rule linorder_cases [of a b], auto)
apply (drule_tac [!] f = f in MVT)
apply (auto dest: DERIV_isCont DERIV_unique simp add: differentiable_def)
-apply (auto dest: DERIV_unique simp add: left_distrib diff_minus)
+apply (auto dest: DERIV_unique simp add: ring_distribs diff_minus)
done
lemma DERIV_const_ratio_const2:
--- a/src/HOL/Hyperreal/Ln.thy Fri Jun 22 22:41:17 2007 +0200
+++ b/src/HOL/Hyperreal/Ln.thy Sat Jun 23 19:33:22 2007 +0200
@@ -150,7 +150,7 @@
lemma aux3: "(0::real) <= x ==> (1 + x + x^2)/(1 + x^2) <= 1 + x"
apply (subst pos_divide_le_eq)
apply (simp add: zero_compare_simps)
- apply (simp add: ring_eq_simps zero_compare_simps)
+ apply (simp add: ring_simps zero_compare_simps)
done
lemma aux4: "0 <= (x::real) ==> x <= 1 ==> exp (x - x^2) <= 1 + x"
@@ -199,7 +199,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_eq_simps power2_eq_square power3_eq_cube)
+ by (simp add: ring_simps power2_eq_square power3_eq_cube)
also have "... <= 1"
by (auto intro: zero_le_power simp add: a)
finally have "(1 - x) * (1 + x + x ^ 2) <= 1" .
@@ -283,12 +283,9 @@
have e: "-x - 2 * x^2 <= - x / (1 - x)"
apply (rule mult_imp_le_div_pos)
apply (insert prems, force)
- apply (auto simp add: ring_eq_simps power2_eq_square)
- apply (subgoal_tac "- (x * x) + x * (x * (x * 2)) = x^2 * (2 * x - 1)")
- apply (erule ssubst)
- apply (rule mult_nonneg_nonpos)
- apply auto
- apply (auto simp add: ring_eq_simps power2_eq_square)
+ apply (auto simp add: ring_simps power2_eq_square)
+ apply(insert mult_right_le_one_le[of "x*x" "2*x"])
+ apply (simp)
done
from e d show "- x - 2 * x^2 <= ln (1 - x)"
by (rule order_trans)
@@ -404,7 +401,7 @@
apply simp
apply (subst ln_div [THEN sym])
apply arith
- apply (auto simp add: ring_eq_simps add_frac_eq frac_eq_eq
+ apply (auto simp add: ring_simps add_frac_eq frac_eq_eq
add_divide_distrib power2_eq_square)
apply (rule mult_pos_pos, assumption)+
apply assumption
@@ -423,7 +420,7 @@
apply auto
done
have "x * ln y - x * ln x = x * (ln y - ln x)"
- by (simp add: ring_eq_simps)
+ by (simp add: ring_simps)
also have "... = x * ln(y / x)"
apply (subst ln_div)
apply (rule b, rule a, rule refl)
--- a/src/HOL/Hyperreal/NthRoot.thy Fri Jun 22 22:41:17 2007 +0200
+++ b/src/HOL/Hyperreal/NthRoot.thy Sat Jun 23 19:33:22 2007 +0200
@@ -571,12 +571,12 @@
lemma power2_sum:
fixes x y :: "'a::{number_ring,recpower}"
shows "(x + y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> + 2 * x * y"
-by (simp add: left_distrib right_distrib power2_eq_square)
+by (simp add: ring_distribs power2_eq_square)
lemma power2_diff:
fixes x y :: "'a::{number_ring,recpower}"
shows "(x - y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> - 2 * x * y"
-by (simp add: left_diff_distrib right_diff_distrib power2_eq_square)
+by (simp add: ring_distribs power2_eq_square)
lemma real_sqrt_sum_squares_triangle_ineq:
"sqrt ((a + c)\<twosuperior> + (b + d)\<twosuperior>) \<le> sqrt (a\<twosuperior> + b\<twosuperior>) + sqrt (c\<twosuperior> + d\<twosuperior>)"
@@ -586,7 +586,7 @@
apply (rule mult_left_mono)
apply (rule power2_le_imp_le)
apply (simp add: power2_sum power_mult_distrib)
-apply (simp add: ring_distrib)
+apply (simp add: ring_distribs)
apply (subgoal_tac "0 \<le> b\<twosuperior> * c\<twosuperior> + a\<twosuperior> * d\<twosuperior> - 2 * (a * c) * (b * d)", simp)
apply (rule_tac b="(a * d - b * c)\<twosuperior>" in ord_le_eq_trans)
apply (rule zero_le_power2)
--- a/src/HOL/Hyperreal/SEQ.thy Fri Jun 22 22:41:17 2007 +0200
+++ b/src/HOL/Hyperreal/SEQ.thy Sat Jun 23 19:33:22 2007 +0200
@@ -392,7 +392,7 @@
lemma inverse_diff_inverse:
"\<lbrakk>(a::'a::division_ring) \<noteq> 0; b \<noteq> 0\<rbrakk>
\<Longrightarrow> inverse a - inverse b = - (inverse a * (a - b) * inverse b)"
-by (simp add: right_diff_distrib left_diff_distrib mult_assoc)
+by (simp add: ring_simps)
lemma Bseq_inverse_lemma:
fixes x :: "'a::real_normed_div_algebra"
@@ -1065,7 +1065,7 @@
apply (erule mult_left_mono)
apply (rule add_increasing [OF x], simp)
apply (simp add: real_of_nat_Suc)
-apply (simp add: ring_distrib)
+apply (simp add: ring_distribs)
apply (simp add: mult_nonneg_nonneg x)
done
--- a/src/HOL/Hyperreal/Transcendental.thy Fri Jun 22 22:41:17 2007 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy Sat Jun 23 19:33:22 2007 +0200
@@ -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_eq_simps)
+apply (simp add: power_Suc ring_simps)
done
lemma lemma_realpow_rev_sumr:
@@ -423,7 +423,7 @@
apply (rule sums_summable [OF diffs_equiv [OF C]])
apply (rule_tac f="suminf" in arg_cong)
apply (rule ext)
- apply (simp add: ring_eq_simps)
+ apply (simp add: ring_simps)
done
next
show "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x ^ n) / h -
@@ -2031,7 +2031,7 @@
also have "\<dots> = (?c * ?c - ?s * ?s) * ?c - (?s * ?c + ?c * ?s) * ?s"
by (simp only: cos_add sin_add)
also have "\<dots> = ?c * (?c\<twosuperior> - 3 * ?s\<twosuperior>)"
- by (simp add: ring_eq_simps power2_eq_square)
+ by (simp add: ring_simps power2_eq_square)
finally have "?c\<twosuperior> = (sqrt 3 / 2)\<twosuperior>"
using pos_c by (simp add: sin_squared_eq power_divide)
thus ?thesis
--- a/src/HOL/IntDef.thy Fri Jun 22 22:41:17 2007 +0200
+++ b/src/HOL/IntDef.thy Sat Jun 23 19:33:22 2007 +0200
@@ -137,13 +137,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_eq_simps)
+ by (cases i, cases j, cases k) (simp add: mult ring_simps)
show "i * j = j * i"
- by (cases i, cases j) (simp add: mult ring_eq_simps)
+ by (cases i, cases j) (simp add: mult ring_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_eq_simps)
+ by (cases i, cases j, cases k) (simp add: add mult ring_simps)
show "0 \<noteq> (1::int)"
by (simp add: Zero_int_def One_int_def)
qed
@@ -358,7 +358,7 @@
also have "\<dots> = (\<exists>n. z - w = int n)"
by (auto elim: zero_le_imp_eq_int)
also have "\<dots> = (\<exists>n. z = w + int n)"
- by (simp only: group_eq_simps)
+ by (simp only: group_simps)
finally show ?thesis .
qed
--- a/src/HOL/IntDiv.thy Fri Jun 22 22:41:17 2007 +0200
+++ b/src/HOL/IntDiv.thy Sat Jun 23 19:33:22 2007 +0200
@@ -1210,7 +1210,7 @@
done
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_eq_simps)
+ by (simp add: ring_simps)
lemma zdvd_mult_div_cancel:"(n::int) dvd m \<Longrightarrow> n * (m div n) = m"
apply (subgoal_tac "m mod n = 0")
--- a/src/HOL/Library/BigO.thy Fri Jun 22 22:41:17 2007 +0200
+++ b/src/HOL/Library/BigO.thy Sat Jun 23 19:33:22 2007 +0200
@@ -103,7 +103,7 @@
apply (auto simp add: bigo_alt_def set_plus)
apply (rule_tac x = "c + ca" in exI)
apply auto
- apply (simp add: ring_distrib func_plus)
+ apply (simp add: ring_distribs func_plus)
apply (rule order_trans)
apply (rule abs_triangle_ineq)
apply (rule add_mono)
@@ -134,7 +134,7 @@
apply (simp)
apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))")
apply (erule order_trans)
- apply (simp add: ring_distrib)
+ apply (simp add: ring_distribs)
apply (rule mult_left_mono)
apply assumption
apply (simp add: order_less_le)
@@ -155,7 +155,7 @@
apply (simp)
apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))")
apply (erule order_trans)
- apply (simp add: ring_distrib)
+ apply (simp add: ring_distribs)
apply (rule mult_left_mono)
apply (simp add: order_less_le)
apply (simp add: order_less_le)
@@ -192,7 +192,7 @@
apply clarify
apply (drule_tac x = "xa" in spec)+
apply (subgoal_tac "0 <= f xa + g xa")
- apply (simp add: ring_distrib)
+ apply (simp add: ring_distribs)
apply (subgoal_tac "abs(a xa + b xa) <= abs(a xa) + abs(b xa)")
apply (subgoal_tac "abs(a xa) + abs(b xa) <=
max c ca * f xa + max c ca * g xa")
@@ -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_eq_simps mult_ac)
+ apply (auto simp add: ring_simps)
done
lemma bigo_mult5: "ALL x. f x ~= 0 ==>
--- a/src/HOL/Library/Commutative_Ring.thy Fri Jun 22 22:41:17 2007 +0200
+++ b/src/HOL/Library/Commutative_Ring.thy Sat Jun 23 19:33:22 2007 +0200
@@ -174,11 +174,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_eq_simps)
+ by (induct B) (auto simp add: mkPinj_def ring_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_eq_simps)
+ by (cases A) (auto simp add: mkPX_def mkPinj_ci power_add ring_simps)
text {* Correctness theorems for the implemented operations *}
@@ -193,13 +193,13 @@
show ?case
proof (rule linorder_cases)
assume "x < y"
- with 6 show ?case by (simp add: mkPinj_ci ring_eq_simps)
+ with 6 show ?case by (simp add: mkPinj_ci ring_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_eq_simps)
+ with 6 show ?case by (simp add: mkPinj_ci ring_simps)
qed
next
case (7 x P Q y R)
@@ -207,7 +207,7 @@
moreover
{ assume "x = 0" with 7 have ?case by simp }
moreover
- { assume "x = 1" with 7 have ?case by (simp add: ring_eq_simps) }
+ { assume "x = 1" with 7 have ?case by (simp add: ring_simps) }
moreover
{ assume "x > 1" from 7 have ?case by (cases x) simp_all }
ultimately show ?case by blast
@@ -226,20 +226,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_eq_simps)
+ with 9 a show ?case by (auto simp add: mkPX_ci power_add ring_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_eq_simps)
+ with 9 a show ?case by (auto simp add: power_add mkPX_ci ring_simps)
next
assume "x = y"
- with 9 show ?case by (simp add: mkPX_ci ring_eq_simps)
+ with 9 show ?case by (simp add: mkPX_ci ring_simps)
qed
-qed (auto simp add: ring_eq_simps)
+qed (auto simp add: ring_simps)
text {* Multiplication *}
lemma mul_ci: "Ipol l (P \<otimes> Q) = Ipol l P * Ipol l Q"
by (induct P Q arbitrary: l rule: mul.induct)
- (simp_all add: mkPX_ci mkPinj_ci ring_eq_simps add_ci power_add)
+ (simp_all add: mkPX_ci mkPinj_ci ring_simps add_ci power_add)
text {* Substraction *}
lemma sub_ci: "Ipol l (P \<ominus> Q) = Ipol l P - Ipol l Q"
@@ -248,7 +248,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_eq_simps power_add)
+ (simp_all add: add_ci mkPinj_ci mkPX_ci mul_ci ring_simps power_add)
text {* Power *}
lemma even_pow:"even n \<Longrightarrow> pow n P = pow (n div 2) (sqr P)"
--- a/src/HOL/Library/SetsAndFunctions.thy Fri Jun 22 22:41:17 2007 +0200
+++ b/src/HOL/Library/SetsAndFunctions.thy Sat Jun 23 19:33:22 2007 +0200
@@ -88,7 +88,7 @@
instance "fun" :: (type,comm_ring_1)comm_ring_1
apply default
apply (auto simp add: func_plus func_times func_minus func_diff ext
- func_one func_zero ring_eq_simps)
+ func_one func_zero ring_simps)
apply (drule fun_cong)
apply simp
done
@@ -328,21 +328,21 @@
lemma set_times_plus_distrib: "(a::'a::semiring) *o (b +o C)=
(a * b) +o (a *o C)"
- by (auto simp add: elt_set_plus_def elt_set_times_def ring_distrib)
+ by (auto simp add: elt_set_plus_def elt_set_times_def ring_distribs)
lemma set_times_plus_distrib2: "(a::'a::semiring) *o (B + C) =
(a *o B) + (a *o C)"
- apply (auto simp add: set_plus elt_set_times_def ring_distrib)
+ apply (auto simp add: set_plus elt_set_times_def ring_distribs)
apply blast
apply (rule_tac x = "b + bb" in exI)
- apply (auto simp add: ring_distrib)
+ apply (auto simp add: ring_distribs)
done
lemma set_times_plus_distrib3: "((a::'a::semiring) +o C) * D <=
a *o D + C * D"
apply (auto intro!: subsetI simp add:
elt_set_plus_def elt_set_times_def set_times
- set_plus ring_distrib)
+ set_plus ring_distribs)
apply auto
done
--- a/src/HOL/Library/Word.thy Fri Jun 22 22:41:17 2007 +0200
+++ b/src/HOL/Library/Word.thy Sat Jun 23 19:33:22 2007 +0200
@@ -443,7 +443,7 @@
bitval x * 2 ^ length xs * 2 ^ length l2 + bv_to_nat xs * 2 ^ length l2"
by simp
also have "... = (bitval x * 2 ^ length xs + bv_to_nat xs) * 2 ^ length l2"
- by (simp add: ring_distrib)
+ by (simp add: ring_distribs)
finally show ?thesis .
qed
qed
--- a/src/HOL/Matrix/LP.thy Fri Jun 22 22:41:17 2007 +0200
+++ b/src/HOL/Matrix/LP.thy Sat Jun 23 19:33:22 2007 +0200
@@ -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_eq_simps)
+ have 3: "y * (A * x) = c * x + (y * (A - A') + (y * A' - c') + (c'-c)) * x" by (simp add: ring_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_eq_simps)
+ have 10: "c'-c = -(c-c')" by (simp add: ring_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') + \<delta>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_eq_simps)
+ by (simp add: ring_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_eq_simps)
+ moreover have "y * (A * x) = c * x + (y * A - c) * x" by (simp add: ring_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_eq_simps)
+ then have cx: "c * x <= y * b + (c - y * A) * x" by (simp add: ring_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"
--- a/src/HOL/Matrix/Matrix.thy Fri Jun 22 22:41:17 2007 +0200
+++ b/src/HOL/Matrix/Matrix.thy Sat Jun 23 19:33:22 2007 +0200
@@ -59,17 +59,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_eq_simps)
+ apply (simp_all add: associative_def ring_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_eq_simps)
+ apply (simp_all add: associative_def commutative_def ring_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_eq_simps)
+ apply (simp_all add: associative_def commutative_def ring_simps)
done
show "abs A = sup A (-A)"
by (simp add: abs_matrix_def)
@@ -264,24 +264,24 @@
"scalar_mult a m == apply_matrix (op * a) m"
lemma scalar_mult_zero[simp]: "scalar_mult y 0 = 0"
- by (simp add: scalar_mult_def)
+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_eq_simps)
+by (simp add: scalar_mult_def apply_matrix_add ring_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)
+by (simp add: scalar_mult_def)
lemma scalar_mult_singleton[simp]: "scalar_mult y (singleton_matrix j i x) = singleton_matrix j i (y * x)"
- apply (subst Rep_matrix_inject[symmetric])
- apply (rule ext)+
- apply (auto)
- done
+apply (subst Rep_matrix_inject[symmetric])
+apply (rule ext)+
+apply (auto)
+done
lemma Rep_minus[simp]: "Rep_matrix (-(A::_::lordered_ab_group)) x y = - (Rep_matrix A x y)"
- by (simp add: minus_matrix_def)
+by (simp add: minus_matrix_def)
lemma Rep_abs[simp]: "Rep_matrix (abs (A::_::lordered_ring)) x y = abs (Rep_matrix A x y)"
- by (simp add: abs_lattice sup_matrix_def)
+by (simp add: abs_lattice sup_matrix_def)
end
--- a/src/HOL/Matrix/SparseMatrix.thy Fri Jun 22 22:41:17 2007 +0200
+++ b/src/HOL/Matrix/SparseMatrix.thy Sat Jun 23 19:33:22 2007 +0200
@@ -282,7 +282,7 @@
apply (rule conjI)
apply (intro strip)
apply (frule_tac as=brr in sorted_spvec_cons1)
- apply (simp add: ring_eq_simps sparse_row_matrix_cons)
+ apply (simp add: ring_simps sparse_row_matrix_cons)
apply (simplesubst Rep_matrix_zero_imp_mult_zero)
apply (simp)
apply (intro strip)
@@ -304,7 +304,7 @@
apply (intro strip | rule conjI)+
apply (frule_tac as=arr in sorted_spvec_cons1)
- apply (simp add: ring_eq_simps)
+ apply (simp add: ring_simps)
apply (subst Rep_matrix_zero_imp_mult_zero)
apply (simp)
apply (rule disjI2)
@@ -318,7 +318,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_eq_simps sparse_row_vector_addmult_spvec)
+ apply (simp add: sparse_row_matrix_cons ring_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)
@@ -368,7 +368,7 @@
lemma sparse_row_mult_spmat[rule_format]:
"sorted_spmat A \<longrightarrow> sorted_spvec B \<longrightarrow> 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_eq_simps move_matrix_mult)
+ apply (auto simp add: sparse_row_matrix_cons sparse_row_mult_spvec_spmat ring_simps move_matrix_mult)
done
lemma sorted_spvec_mult_spmat[rule_format]:
@@ -1146,8 +1146,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 prems)
- apply (simp add: sparse_row_matrix_op_simps ring_eq_simps)
- apply (rule mult_le_dual_prts[where A=A, simplified Let_def ring_eq_simps])
+ 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 (auto)
done
--- a/src/HOL/MetisExamples/BigO.thy Fri Jun 22 22:41:17 2007 +0200
+++ b/src/HOL/MetisExamples/BigO.thy Sat Jun 23 19:33:22 2007 +0200
@@ -476,7 +476,7 @@
apply (auto simp add: bigo_alt_def set_plus)
apply (rule_tac x = "c + ca" in exI)
apply auto
- apply (simp add: ring_distrib func_plus)
+ apply (simp add: ring_distribs func_plus)
apply (blast intro:order_trans abs_triangle_ineq add_mono elim:)
done
@@ -503,7 +503,7 @@
apply (simp)
apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))")
apply (erule order_trans)
- apply (simp add: ring_distrib)
+ apply (simp add: ring_distribs)
apply (rule mult_left_mono)
apply assumption
apply (simp add: order_less_le)
@@ -524,7 +524,7 @@
apply (simp)
apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))")
apply (erule order_trans)
- apply (simp add: ring_distrib)
+ apply (simp add: ring_distribs)
apply (rule mult_left_mono)
apply (simp add: order_less_le)
apply (simp add: order_less_le)
@@ -563,7 +563,7 @@
apply clarify
apply (drule_tac x = "xa" in spec)+
apply (subgoal_tac "0 <= f xa + g xa")
- apply (simp add: ring_distrib)
+ apply (simp add: ring_distribs)
apply (subgoal_tac "abs(a xa + b xa) <= abs(a xa) + abs(b xa)")
apply (subgoal_tac "abs(a xa) + abs(b xa) <=
max c ca * f xa + max c ca * g xa")
--- a/src/HOL/OrderedGroup.thy Fri Jun 22 22:41:17 2007 +0200
+++ b/src/HOL/OrderedGroup.thy Sat Jun 23 19:33:22 2007 +0200
@@ -171,6 +171,9 @@
lemma diff_minus_eq_add [simp]: "a - - b = a + (b::'a::group_add)"
by (simp add: diff_minus)
+lemma uminus_add_conv_diff: "-a + b = b - (a::'a::ab_group_add)"
+by(simp add:diff_minus add_commute)
+
lemma neg_equal_iff_equal [simp]: "(-a = -b) = (a = (b::'a::group_add))"
proof
assume "- a = - b"
@@ -1036,21 +1039,18 @@
apply (simp_all add: prems)
done
-lemmas group_eq_simps =
+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_eq_eq eq_diff_eq diff_minus[symmetric] uminus_add_conv_diff
+ diff_less_eq less_diff_eq diff_le_eq le_diff_eq
lemma estimate_by_abs:
"a + b <= (c::'a::lordered_ab_group_abs) \<Longrightarrow> a <= c + abs b"
proof -
- assume 1: "a+b <= c"
- have 2: "a <= c+(-b)"
- apply (insert 1)
- apply (drule_tac add_right_mono[where c="-b"])
- apply (simp add: group_eq_simps)
- done
+ assume "a+b <= c"
+ hence 2: "a <= c+(-b)" by (simp add: group_simps)
have 3: "(-b) <= abs b" by (rule abs_ge_minus_self)
show ?thesis by (rule le_add_right_mono[OF 2 3])
qed
--- a/src/HOL/Presburger.thy Fri Jun 22 22:41:17 2007 +0200
+++ b/src/HOL/Presburger.thy Sat Jun 23 19:33:22 2007 +0200
@@ -60,7 +60,7 @@
"\<forall>x k. F = F"
by simp_all
(clarsimp simp add: dvd_def, rule iffI, clarsimp,rule_tac x = "kb - ka*k" in exI,
- simp add: ring_eq_simps, clarsimp,rule_tac x = "kb + ka*k" in exI,simp add: ring_eq_simps)+
+ simp add: ring_simps, clarsimp,rule_tac x = "kb + ka*k" in exI,simp add: ring_simps)+
subsection{* The A and B sets *}
lemma bset:
@@ -98,7 +98,7 @@
{fix x assume nob: "\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j" and g: "x > t" and ng: "\<not> (x - D) > t"
hence "x -t \<le> D" and "1 \<le> x - t" by simp+
hence "\<exists>j \<in> {1 .. D}. x - t = j" by auto
- hence "\<exists>j \<in> {1 .. D}. x = t + j" by (simp add: ring_eq_simps)
+ hence "\<exists>j \<in> {1 .. D}. x = t + j" by (simp add: ring_simps)
with nob tB have "False" by simp}
thus "\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x > t) \<longrightarrow> (x - D > t)" by blast
next
@@ -106,18 +106,18 @@
{fix x assume nob: "\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j" and g: "x \<ge> t" and ng: "\<not> (x - D) \<ge> t"
hence "x - (t - 1) \<le> D" and "1 \<le> x - (t - 1)" by simp+
hence "\<exists>j \<in> {1 .. D}. x - (t - 1) = j" by auto
- hence "\<exists>j \<in> {1 .. D}. x = (t - 1) + j" by (simp add: ring_eq_simps)
+ hence "\<exists>j \<in> {1 .. D}. x = (t - 1) + j" by (simp add: ring_simps)
with nob tB have "False" by simp}
thus "\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x \<ge> t) \<longrightarrow> (x - D \<ge> 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_eq_simps)}
+ by (clarsimp simp add: dvd_def,rule_tac x= "ka - k" in exI,simp add: ring_simps)}
thus "\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (d dvd x+t) \<longrightarrow> (d dvd (x - D) + t)" by simp
next
assume d: "d dvd D"
{fix x assume H: "\<not>(d dvd x + t)" with d have "\<not>d dvd (x - D) + t"
- by (clarsimp simp add: dvd_def,erule_tac x= "ka + k" in allE,simp add: ring_eq_simps)}
+ by (clarsimp simp add: dvd_def,erule_tac x= "ka + k" in allE,simp add: ring_simps)}
thus "\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (\<not>d dvd x+t) \<longrightarrow> (\<not>d dvd (x - D) + t)" by auto
qed blast
@@ -156,26 +156,26 @@
{fix x assume nob: "\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j" and g: "x < t" and ng: "\<not> (x + D) < t"
hence "t - x \<le> D" and "1 \<le> t - x" by simp+
hence "\<exists>j \<in> {1 .. D}. t - x = j" by auto
- hence "\<exists>j \<in> {1 .. D}. x = t - j" by (auto simp add: ring_eq_simps)
+ hence "\<exists>j \<in> {1 .. D}. x = t - j" by (auto simp add: ring_simps)
with nob tA have "False" by simp}
thus "\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (x < t) \<longrightarrow> (x + D < t)" by blast
next
assume dp: "D > 0" and tA:"t + 1\<in> A"
{fix x assume nob: "\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j" and g: "x \<le> t" and ng: "\<not> (x + D) \<le> t"
- hence "(t + 1) - x \<le> D" and "1 \<le> (t + 1) - x" by (simp_all add: ring_eq_simps)
+ hence "(t + 1) - x \<le> D" and "1 \<le> (t + 1) - x" by (simp_all add: ring_simps)
hence "\<exists>j \<in> {1 .. D}. (t + 1) - x = j" by auto
- hence "\<exists>j \<in> {1 .. D}. x = (t + 1) - j" by (auto simp add: ring_eq_simps)
+ hence "\<exists>j \<in> {1 .. D}. x = (t + 1) - j" by (auto simp add: ring_simps)
with nob tA have "False" by simp}
thus "\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (x \<le> t) \<longrightarrow> (x + D \<le> 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_eq_simps)}
+ by (clarsimp simp add: dvd_def,rule_tac x= "ka + k" in exI,simp add: ring_simps)}
thus "\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (d dvd x+t) \<longrightarrow> (d dvd (x + D) + t)" by simp
next
assume d: "d dvd D"
{fix x assume H: "\<not>(d dvd x + t)" with d have "\<not>d dvd (x + D) + t"
- by (clarsimp simp add: dvd_def,erule_tac x= "ka - k" in allE,simp add: ring_eq_simps)}
+ by (clarsimp simp add: dvd_def,erule_tac x= "ka - k" in allE,simp add: ring_simps)}
thus "\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (\<not>d dvd x+t) \<longrightarrow> (\<not>d dvd (x + D) + t)" by auto
qed blast
@@ -302,7 +302,7 @@
from ePeqP1 obtain z where P1eqP: "\<forall>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_eq_simps)
+ have ww'[simp]: "?w = ?w'" by (simp add: ring_simps)
from dpos have w: "?w > z" by(simp only: ww' incr_lemma)
hence "P' x = P' ?w" using P1eqP1 by blast
also have "\<dots> = P(?w)" using w P1eqP by blast
--- a/src/HOL/Real/Float.thy Fri Jun 22 22:41:17 2007 +0200
+++ b/src/HOL/Real/Float.thy Sat Jun 23 19:33:22 2007 +0200
@@ -39,7 +39,7 @@
show ?thesis
proof (induct a)
case (1 n)
- from pos show ?case by (simp add: ring_eq_simps)
+ from pos show ?case by (simp add: ring_simps)
next
case (2 n)
show ?case
@@ -60,7 +60,7 @@
show ?case by simp
next
case (Suc m)
- show ?case by (auto simp add: ring_eq_simps pow2_add1 prems)
+ show ?case by (auto simp add: ring_simps pow2_add1 prems)
qed
next
case (2 n)
@@ -73,7 +73,7 @@
apply (subst pow2_neg[of "-1"])
apply (simp)
apply (insert pow2_add1[of "-a"])
- apply (simp add: ring_eq_simps)
+ apply (simp add: ring_simps)
apply (subst pow2_neg[of "-a"])
apply (simp)
done
@@ -84,7 +84,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_eq_simps)
+ apply (auto simp add: ring_simps)
apply (subst a)
apply (subst b)
apply (simp only: pow2_add1)
@@ -92,13 +92,13 @@
apply (subst pow2_neg[of "int m + 1"])
apply auto
apply (insert prems)
- apply (auto simp add: ring_eq_simps)
+ apply (auto simp add: ring_simps)
done
qed
qed
lemma "float (a, e) + float (b, e) = float (a + b, e)"
-by (simp add: float_def ring_eq_simps)
+by (simp add: float_def ring_simps)
definition
int_of_real :: "real \<Rightarrow> int" where
@@ -255,7 +255,7 @@
lemma float_transfer_even: "even a \<Longrightarrow> 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_eq_simps)
+ apply (simp_all add: pow2_def even_def real_is_int_def ring_simps)
apply (auto)
proof -
fix q::int
@@ -324,7 +324,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_eq_simps)
+ apply (simp add: float_def ring_simps)
apply (auto simp add: pow2_int[symmetric] pow2_add[symmetric])
done
--- a/src/HOL/Real/RComplete.thy Fri Jun 22 22:41:17 2007 +0200
+++ b/src/HOL/Real/RComplete.thy Sat Jun 23 19:33:22 2007 +0200
@@ -377,7 +377,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_eq_simps)
+ by (simp add: ring_simps)
thus "\<exists>(n::nat). x < real n" ..
qed
@@ -392,9 +392,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_eq_simps)
+ by (simp add: ring_simps)
hence "y < real (n::nat) * x"
- using x_not_zero by (simp add: ring_eq_simps)
+ using x_not_zero by (simp add: ring_simps)
thus "\<exists>(n::nat). y < real n * x" ..
qed
@@ -1226,7 +1226,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_distrib ring_eq_simps add_divide_distrib
+ by (auto simp add: ring_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) /
--- a/src/HOL/Real/RealDef.thy Fri Jun 22 22:41:17 2007 +0200
+++ b/src/HOL/Real/RealDef.thy Sat Jun 23 19:33:22 2007 +0200
@@ -253,8 +253,7 @@
apply (rule_tac [2]
x = "Abs_Real (realrel``{(inverse (D) + 1, 1)})"
in exI)
-apply (auto simp add: real_mult ring_distrib
- preal_mult_inverse_right add_ac mult_ac)
+apply (auto simp add: real_mult preal_mult_inverse_right ring_simps)
done
lemma real_mult_inverse_left: "x \<noteq> 0 ==> inverse(x)*x = (1::real)"
@@ -632,7 +631,7 @@
then have "real x / real d = ... / real d"
by simp
then show ?thesis
- by (auto simp add: add_divide_distrib ring_eq_simps prems)
+ by (auto simp add: add_divide_distrib ring_simps prems)
qed
lemma real_of_int_div: "(d::int) ~= 0 ==> d dvd n ==>
@@ -776,7 +775,7 @@
then have "real x / real d = \<dots> / real d"
by simp
then show ?thesis
- by (auto simp add: add_divide_distrib ring_eq_simps prems)
+ by (auto simp add: add_divide_distrib ring_simps prems)
qed
lemma real_of_nat_div: "0 < (d::nat) ==> d dvd n ==>
--- a/src/HOL/Real/RealPow.thy Fri Jun 22 22:41:17 2007 +0200
+++ b/src/HOL/Real/RealPow.thy Sat Jun 23 19:33:22 2007 +0200
@@ -57,7 +57,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: right_distrib left_distrib mult_ac)
+apply (simp add: ring_simps)
done
lemma realpow_two_disj:
--- a/src/HOL/Ring_and_Field.thy Fri Jun 22 22:41:17 2007 +0200
+++ b/src/HOL/Ring_and_Field.thy Sat Jun 23 19:33:22 2007 +0200
@@ -1,6 +1,6 @@
(* Title: HOL/Ring_and_Field.thy
ID: $Id$
- Author: Gertrud Bauer, Steven Obua, Lawrence C Paulson, and Markus Wenzel,
+ Author: Gertrud Bauer, Steven Obua, Tobias Nipkow, Lawrence C Paulson, and Markus Wenzel,
with contributions by Jeremy Avigad
*)
@@ -173,8 +173,6 @@
subsection {* Distribution rules *}
-theorems ring_distrib = right_distrib left_distrib
-
text{*For the @{text combine_numerals} simproc*}
lemma combine_common_factor:
"a*e + (b*e + c) = (a+b)*e + (c::'a::semiring)"
@@ -204,6 +202,15 @@
by (simp add: left_distrib diff_minus
minus_mult_left [symmetric] minus_mult_right [symmetric])
+lemmas ring_distribs =
+ right_distrib left_distrib left_diff_distrib right_diff_distrib
+
+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
+
class mult_mono = times + zero + ord +
assumes mult_left_mono: "a \<sqsubseteq> b \<Longrightarrow> \<^loc>0 \<sqsubseteq> c \<Longrightarrow> c \<^loc>* a \<sqsubseteq> c \<^loc>* b"
assumes mult_right_mono: "a \<sqsubseteq> b \<Longrightarrow> \<^loc>0 \<sqsubseteq> c \<Longrightarrow> a \<^loc>* c \<sqsubseteq> b \<^loc>* c"
@@ -308,81 +315,68 @@
linorder_neqE[where 'a = "?'b::ordered_idom"]
lemma eq_add_iff1:
- "(a*e + c = b*e + d) = ((a-b)*e + c = (d::'a::ring))"
-apply (simp add: diff_minus left_distrib)
-apply (simp add: diff_minus left_distrib add_ac)
-apply (simp add: compare_rls minus_mult_left [symmetric])
-done
+ "(a*e + c = b*e + d) = ((a-b)*e + c = (d::'a::ring))"
+by (simp add: ring_simps)
lemma eq_add_iff2:
- "(a*e + c = b*e + d) = (c = (b-a)*e + (d::'a::ring))"
-apply (simp add: diff_minus left_distrib add_ac)
-apply (simp add: compare_rls minus_mult_left [symmetric])
-done
+ "(a*e + c = b*e + d) = (c = (b-a)*e + (d::'a::ring))"
+by (simp add: ring_simps)
lemma less_add_iff1:
- "(a*e + c < b*e + d) = ((a-b)*e + c < (d::'a::pordered_ring))"
-apply (simp add: diff_minus left_distrib add_ac)
-apply (simp add: compare_rls minus_mult_left [symmetric])
-done
+ "(a*e + c < b*e + d) = ((a-b)*e + c < (d::'a::pordered_ring))"
+by (simp add: ring_simps)
lemma less_add_iff2:
- "(a*e + c < b*e + d) = (c < (b-a)*e + (d::'a::pordered_ring))"
-apply (simp add: diff_minus left_distrib add_ac)
-apply (simp add: compare_rls minus_mult_left [symmetric])
-done
+ "(a*e + c < b*e + d) = (c < (b-a)*e + (d::'a::pordered_ring))"
+by (simp add: ring_simps)
lemma le_add_iff1:
- "(a*e + c \<le> b*e + d) = ((a-b)*e + c \<le> (d::'a::pordered_ring))"
-apply (simp add: diff_minus left_distrib add_ac)
-apply (simp add: compare_rls minus_mult_left [symmetric])
-done
+ "(a*e + c \<le> b*e + d) = ((a-b)*e + c \<le> (d::'a::pordered_ring))"
+by (simp add: ring_simps)
lemma le_add_iff2:
- "(a*e + c \<le> b*e + d) = (c \<le> (b-a)*e + (d::'a::pordered_ring))"
-apply (simp add: diff_minus left_distrib add_ac)
-apply (simp add: compare_rls minus_mult_left [symmetric])
-done
+ "(a*e + c \<le> b*e + d) = (c \<le> (b-a)*e + (d::'a::pordered_ring))"
+by (simp add: ring_simps)
subsection {* Ordering Rules for Multiplication *}
lemma mult_left_le_imp_le:
- "[|c*a \<le> c*b; 0 < c|] ==> a \<le> (b::'a::ordered_semiring_strict)"
- by (force simp add: mult_strict_left_mono linorder_not_less [symmetric])
+ "[|c*a \<le> c*b; 0 < c|] ==> a \<le> (b::'a::ordered_semiring_strict)"
+by (force simp add: mult_strict_left_mono linorder_not_less [symmetric])
lemma mult_right_le_imp_le:
- "[|a*c \<le> b*c; 0 < c|] ==> a \<le> (b::'a::ordered_semiring_strict)"
- by (force simp add: mult_strict_right_mono linorder_not_less [symmetric])
+ "[|a*c \<le> b*c; 0 < c|] ==> a \<le> (b::'a::ordered_semiring_strict)"
+by (force simp add: mult_strict_right_mono linorder_not_less [symmetric])
lemma mult_left_less_imp_less:
- "[|c*a < c*b; 0 \<le> c|] ==> a < (b::'a::ordered_semiring_strict)"
- by (force simp add: mult_left_mono linorder_not_le [symmetric])
+ "[|c*a < c*b; 0 \<le> c|] ==> a < (b::'a::ordered_semiring_strict)"
+by (force simp add: mult_left_mono linorder_not_le [symmetric])
lemma mult_right_less_imp_less:
- "[|a*c < b*c; 0 \<le> c|] ==> a < (b::'a::ordered_semiring_strict)"
- by (force simp add: mult_right_mono linorder_not_le [symmetric])
+ "[|a*c < b*c; 0 \<le> c|] ==> a < (b::'a::ordered_semiring_strict)"
+by (force simp add: mult_right_mono linorder_not_le [symmetric])
lemma mult_strict_left_mono_neg:
- "[|b < a; c < 0|] ==> c * a < c * (b::'a::ordered_ring_strict)"
+ "[|b < a; c < 0|] ==> c * a < c * (b::'a::ordered_ring_strict)"
apply (drule mult_strict_left_mono [of _ _ "-c"])
apply (simp_all add: minus_mult_left [symmetric])
done
lemma mult_left_mono_neg:
- "[|b \<le> a; c \<le> 0|] ==> c * a \<le> c * (b::'a::pordered_ring)"
+ "[|b \<le> a; c \<le> 0|] ==> c * a \<le> c * (b::'a::pordered_ring)"
apply (drule mult_left_mono [of _ _ "-c"])
apply (simp_all add: minus_mult_left [symmetric])
done
lemma mult_strict_right_mono_neg:
- "[|b < a; c < 0|] ==> a * c < b * (c::'a::ordered_ring_strict)"
+ "[|b < a; c < 0|] ==> a * c < b * (c::'a::ordered_ring_strict)"
apply (drule mult_strict_right_mono [of _ _ "-c"])
apply (simp_all add: minus_mult_right [symmetric])
done
lemma mult_right_mono_neg:
- "[|b \<le> a; c \<le> 0|] ==> a * c \<le> (b::'a::pordered_ring) * c"
+ "[|b \<le> a; c \<le> 0|] ==> a * c \<le> (b::'a::pordered_ring) * c"
apply (drule mult_right_mono [of _ _ "-c"])
apply (simp)
apply (simp_all add: minus_mult_right [symmetric])
@@ -648,7 +642,7 @@
shows "(a * c = b * c) = (c = 0 \<or> a = b)"
proof -
have "(a * c = b * c) = ((a - b) * c = 0)"
- by (simp add: left_diff_distrib)
+ by (simp add: ring_distribs)
thus ?thesis
by (simp add: disj_commute)
qed
@@ -658,7 +652,7 @@
shows "(c * a = c * b) = (c = 0 \<or> a = b)"
proof -
have "(c * a = c * b) = (c * (a - b) = 0)"
- by (simp add: right_diff_distrib)
+ by (simp add: ring_distribs)
thus ?thesis
by simp
qed
@@ -742,16 +736,6 @@
mult_cancel_left1 mult_cancel_left2
-text{*This list of rewrites decides ring equalities by ordered rewriting.*}
-lemmas ring_eq_simps =
-(* mult_ac*)
- left_distrib right_distrib left_diff_distrib right_diff_distrib
- group_eq_simps
-(* add_ac
- add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2
- diff_eq_eq eq_diff_eq *)
-
-
subsection {* Fields *}
lemma right_inverse_eq: "b \<noteq> 0 ==> (a / b = 1) = (a = (b::'a::field))"
@@ -787,7 +771,7 @@
by (simp add: divide_inverse)
lemma add_divide_distrib: "(a+b)/(c::'a::field) = a/c + b/c"
-by (simp add: divide_inverse left_distrib)
+by (simp add: divide_inverse ring_distribs)
text{*Compared with @{text mult_eq_0_iff}, this version removes the requirement
@@ -957,22 +941,22 @@
lemma division_ring_inverse_add:
"[|(a::'a::division_ring) \<noteq> 0; b \<noteq> 0|]
==> inverse a + inverse b = inverse a * (a+b) * inverse b"
- by (simp add: right_distrib left_distrib mult_assoc)
+by (simp add: ring_simps)
lemma division_ring_inverse_diff:
"[|(a::'a::division_ring) \<noteq> 0; b \<noteq> 0|]
==> inverse a - inverse b = inverse a * (b-a) * inverse b"
-by (simp add: right_diff_distrib left_diff_distrib mult_assoc)
+by (simp add: ring_simps)
text{*There is no slick version using division by zero.*}
lemma inverse_add:
- "[|a \<noteq> 0; b \<noteq> 0|]
- ==> inverse a + inverse b = (a+b) * inverse a * inverse (b::'a::field)"
+ "[|a \<noteq> 0; b \<noteq> 0|]
+ ==> inverse a + inverse b = (a+b) * inverse a * inverse (b::'a::field)"
by (simp add: division_ring_inverse_add mult_ac)
lemma inverse_divide [simp]:
- "inverse (a/b) = b / (a::'a::{field,division_by_zero})"
- by (simp add: divide_inverse mult_commute)
+ "inverse (a/b) = b / (a::'a::{field,division_by_zero})"
+by (simp add: divide_inverse mult_commute)
subsection {* Calculations with fractions *}
@@ -982,8 +966,7 @@
because the latter are covered by a simproc. *}
lemma nonzero_mult_divide_mult_cancel_left[simp]:
- assumes [simp]: "b\<noteq>0" and [simp]: "c\<noteq>0"
- shows "(c*a)/(c*b) = a/(b::'a::field)"
+assumes [simp]: "b\<noteq>0" and [simp]: "c\<noteq>0" shows "(c*a)/(c*b) = a/(b::'a::field)"
proof -
have "(c*a)/(c*b) = c * a * (inverse b * inverse c)"
by (simp add: field_mult_eq_0_iff divide_inverse
@@ -997,23 +980,23 @@
qed
lemma mult_divide_mult_cancel_left:
- "c\<noteq>0 ==> (c*a) / (c*b) = a / (b::'a::{field,division_by_zero})"
+ "c\<noteq>0 ==> (c*a) / (c*b) = a / (b::'a::{field,division_by_zero})"
apply (cases "b = 0")
apply (simp_all add: nonzero_mult_divide_mult_cancel_left)
done
lemma nonzero_mult_divide_mult_cancel_right:
- "[|b\<noteq>0; c\<noteq>0|] ==> (a*c) / (b*c) = a/(b::'a::field)"
+ "[|b\<noteq>0; c\<noteq>0|] ==> (a*c) / (b*c) = a/(b::'a::field)"
by (simp add: mult_commute [of _ c] nonzero_mult_divide_mult_cancel_left)
lemma mult_divide_mult_cancel_right:
- "c\<noteq>0 ==> (a*c) / (b*c) = a / (b::'a::{field,division_by_zero})"
+ "c\<noteq>0 ==> (a*c) / (b*c) = a / (b::'a::{field,division_by_zero})"
apply (cases "b = 0")
apply (simp_all add: nonzero_mult_divide_mult_cancel_right)
done
lemma divide_1 [simp]: "a/1 = (a::'a::field)"
- by (simp add: divide_inverse)
+by (simp add: divide_inverse)
lemma times_divide_eq_right: "a * (b/c) = (a*b) / (c::'a::field)"
by (simp add: divide_inverse mult_assoc)
@@ -1022,33 +1005,33 @@
by (simp add: divide_inverse mult_ac)
lemma divide_divide_eq_right [simp]:
- "a / (b/c) = (a*c) / (b::'a::{field,division_by_zero})"
+ "a / (b/c) = (a*c) / (b::'a::{field,division_by_zero})"
by (simp add: divide_inverse mult_ac)
lemma divide_divide_eq_left [simp]:
- "(a / b) / (c::'a::{field,division_by_zero}) = a / (b*c)"
+ "(a / b) / (c::'a::{field,division_by_zero}) = a / (b*c)"
by (simp add: divide_inverse mult_assoc)
lemma add_frac_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==>
x / y + w / z = (x * z + w * y) / (y * z)"
- apply (subgoal_tac "x / y = (x * z) / (y * z)")
- apply (erule ssubst)
- apply (subgoal_tac "w / z = (w * y) / (y * z)")
- apply (erule ssubst)
- apply (rule add_divide_distrib [THEN sym])
- apply (subst mult_commute)
- apply (erule nonzero_mult_divide_mult_cancel_left [THEN sym])
- apply assumption
- apply (erule nonzero_mult_divide_mult_cancel_right [THEN sym])
- apply assumption
+apply (subgoal_tac "x / y = (x * z) / (y * z)")
+apply (erule ssubst)
+apply (subgoal_tac "w / z = (w * y) / (y * z)")
+apply (erule ssubst)
+apply (rule add_divide_distrib [THEN sym])
+apply (subst mult_commute)
+apply (erule nonzero_mult_divide_mult_cancel_left [THEN sym])
+apply assumption
+apply (erule nonzero_mult_divide_mult_cancel_right [THEN sym])
+apply assumption
done
subsubsection{*Special Cancellation Simprules for Division*}
lemma mult_divide_mult_cancel_left_if[simp]:
- fixes c :: "'a :: {field,division_by_zero}"
- shows "(c*a) / (c*b) = (if c=0 then 0 else a/b)"
+fixes c :: "'a :: {field,division_by_zero}"
+shows "(c*a) / (c*b) = (if c=0 then 0 else a/b)"
by (simp add: mult_divide_mult_cancel_left)
lemma nonzero_mult_divide_cancel_right[simp]:
@@ -1070,62 +1053,14 @@
lemma nonzero_mult_divide_mult_cancel_left2[simp]:
- "[|b\<noteq>0; c\<noteq>0|] ==> (c*a) / (b*c) = a/(b::'a::field)"
+ "[|b\<noteq>0; c\<noteq>0|] ==> (c*a) / (b*c) = a/(b::'a::field)"
using nonzero_mult_divide_mult_cancel_left[of b c a] by(simp add:mult_ac)
lemma nonzero_mult_divide_mult_cancel_right2[simp]:
- "[|b\<noteq>0; c\<noteq>0|] ==> (a*c) / (c*b) = a/(b::'a::field)"
+ "[|b\<noteq>0; c\<noteq>0|] ==> (a*c) / (c*b) = a/(b::'a::field)"
using nonzero_mult_divide_mult_cancel_right[of b c a] by(simp add:mult_ac)
-(* Not needed anymore because now subsumed by simproc "divide_cancel_factor"
-lemma mult_divide_cancel_right_if:
- fixes c :: "'a :: {field,division_by_zero}"
- shows "(a*c) / (b*c) = (if c=0 then 0 else a/b)"
-by (simp add: mult_divide_cancel_right)
-
-lemma mult_divide_cancel_left_if1 [simp]:
- fixes c :: "'a :: {field,division_by_zero}"
- shows "c / (c*b) = (if c=0 then 0 else 1/b)"
-apply (insert mult_divide_cancel_left_if [of c 1 b])
-apply (simp del: mult_divide_cancel_left_if)
-done
-
-lemma mult_divide_cancel_left_if2 [simp]:
- fixes c :: "'a :: {field,division_by_zero}"
- shows "(c*a) / c = (if c=0 then 0 else a)"
-apply (insert mult_divide_cancel_left_if [of c a 1])
-apply (simp del: mult_divide_cancel_left_if)
-done
-
-lemma mult_divide_cancel_right_if1 [simp]:
- fixes c :: "'a :: {field,division_by_zero}"
- shows "c / (b*c) = (if c=0 then 0 else 1/b)"
-apply (insert mult_divide_cancel_right_if [of 1 c b])
-apply (simp del: mult_divide_cancel_right_if)
-done
-
-lemma mult_divide_cancel_right_if2 [simp]:
- fixes c :: "'a :: {field,division_by_zero}"
- shows "(a*c) / c = (if c=0 then 0 else a)"
-apply (insert mult_divide_cancel_right_if [of a c 1])
-apply (simp del: mult_divide_cancel_right_if)
-done
-
-text{*Two lemmas for cancelling the denominator*}
-
-lemma times_divide_self_right [simp]:
- fixes a :: "'a :: {field,division_by_zero}"
- shows "a * (b/a) = (if a=0 then 0 else b)"
-by (simp add: times_divide_eq_right)
-
-lemma times_divide_self_left [simp]:
- fixes a :: "'a :: {field,division_by_zero}"
- shows "(b/a) * a = (if a=0 then 0 else b)"
-by (simp add: times_divide_eq_left)
-*)
-
-
subsection {* Division and Unary Minus *}
lemma nonzero_minus_divide_left: "b \<noteq> 0 ==> - (a/b) = (-a) / (b::'a::field)"
@@ -1155,7 +1090,7 @@
declare mult_minus_left [simp] mult_minus_right [simp]
lemma minus_divide_divide [simp]:
- "(-a)/(-b) = a / (b::'a::{field,division_by_zero})"
+ "(-a)/(-b) = a / (b::'a::{field,division_by_zero})"
apply (cases "b=0", simp)
apply (simp add: nonzero_minus_divide_divide)
done
@@ -1165,10 +1100,10 @@
lemma diff_frac_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==>
x / y - w / z = (x * z - w * y) / (y * z)"
- apply (subst diff_def)+
- apply (subst minus_divide_left)
- apply (subst add_frac_eq)
- apply simp_all
+apply (subst diff_def)+
+apply (subst minus_divide_left)
+apply (subst add_frac_eq)
+apply simp_all
done
@@ -1897,10 +1832,10 @@
by (blast intro: order_less_trans zero_less_one less_add_one)
lemma less_half_sum: "a < b ==> a < (a+b) / (1+1::'a::ordered_field)"
-by (simp add: zero_less_two pos_less_divide_eq right_distrib)
+by (simp add: zero_less_two pos_less_divide_eq ring_distribs)
lemma gt_half_sum: "a < b ==> (a+b)/(1+1::'a::ordered_field) < b"
-by (simp add: zero_less_two pos_divide_less_eq right_distrib)
+by (simp add: zero_less_two pos_divide_less_eq ring_distribs)
lemma dense: "a < b ==> \<exists>r::'a::ordered_field. a < r & r < b"
by (blast intro!: less_half_sum gt_half_sum)
@@ -1909,21 +1844,21 @@
subsection {* Absolute Value *}
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])
lemma abs_le_mult: "abs (a * b) \<le> (abs a) * (abs (b::'a::lordered_ring))"
proof -
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_eq_simps)
+ by (simp only: abs_prts[of a] abs_prts[of b] ring_simps)
{
fix u v :: 'a
have bh: "\<lbrakk>u = a; v = b\<rbrakk> \<Longrightarrow>
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: left_distrib right_distrib add_ac)
+ apply (simp add: ring_simps)
done
}
note b = this[OF refl[of a] refl[of b]]
@@ -1974,7 +1909,7 @@
apply (simp_all add: mulprts abs_prts)
apply (insert prems)
apply (auto simp add:
- ring_eq_simps
+ ring_simps
iff2imp[OF zero_le_iff_zero_nprt] iff2imp[OF le_zero_iff_zero_pprt]
iff2imp[OF le_zero_iff_pprt_id] iff2imp[OF zero_le_iff_nprt_id])
apply(drule (1) mult_nonneg_nonpos[of a b], simp)
@@ -1986,7 +1921,7 @@
then show ?thesis
apply (simp_all add: mulprts abs_prts)
apply (insert prems)
- apply (auto simp add: ring_eq_simps)
+ apply (auto simp add: ring_simps)
apply(drule (1) mult_nonneg_nonneg[of a b],simp)
apply(drule (1) mult_nonpos_nonpos[of a b],simp)
done
@@ -2073,7 +2008,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_eq_simps)
+ by (simp add: ring_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"
--- a/src/HOL/SetInterval.thy Fri Jun 22 22:41:17 2007 +0200
+++ b/src/HOL/SetInterval.thy Sat Jun 23 19:33:22 2007 +0200
@@ -756,7 +756,7 @@
show ?case by simp
next
case (Suc n)
- then show ?case by (simp add: ring_eq_simps)
+ then show ?case by (simp add: ring_simps)
qed
theorem arith_series_general:
--- a/src/HOL/ZF/LProd.thy Fri Jun 22 22:41:17 2007 +0200
+++ b/src/HOL/ZF/LProd.thy Sat Jun 23 19:33:22 2007 +0200
@@ -45,9 +45,9 @@
case (lprod_list ah at bh bt a b)
from prems have transR: "transP R" by auto
have as: "multiset_of (ah @ a # at) = multiset_of (ah @ at) + {#a#}" (is "_ = ?ma + _")
- by (simp add: ring_eq_simps)
+ by (simp add: ring_simps)
have bs: "multiset_of (bh @ b # bt) = multiset_of (bh @ bt) + {#b#}" (is "_ = ?mb + _")
- by (simp add: ring_eq_simps)
+ by (simp add: ring_simps)
from prems have "mult R ?ma ?mb"
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_eq_simps)
+ apply (simp add: ring_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_eq_simps)
+ apply (simp add: ring_simps)
done
qed
qed
--- a/src/HOL/ex/Adder.thy Fri Jun 22 22:41:17 2007 +0200
+++ b/src/HOL/ex/Adder.thy Sat Jun 23 19:33:22 2007 +0200
@@ -64,7 +64,7 @@
apply (induct as)
apply (cases c, simp_all add: Let_def bv_to_nat_dist_append)
apply (simp add: half_adder_correct bv_to_nat_helper' [OF cci_nonnull]
- ring_distrib bv_to_nat_helper)
+ ring_distribs bv_to_nat_helper)
done
consts
@@ -107,7 +107,7 @@
apply (simp add: Let_def)
apply (subst bv_to_nat_dist_append)
apply (simp add: full_adder_correct bv_to_nat_helper' [OF cca_nonnull]
- ring_distrib bv_to_nat_helper cca_length)
+ ring_distribs bv_to_nat_helper cca_length)
done
qed
qed
--- a/src/HOL/ex/Lagrange.thy Fri Jun 22 22:41:17 2007 +0200
+++ b/src/HOL/ex/Lagrange.thy Sat Jun 23 19:33:22 2007 +0200
@@ -16,37 +16,31 @@
The enterprising reader might consider proving all of Lagrange's
theorem. *}
-definition
- sq :: "'a::times => 'a" where
- "sq x == x*x"
+definition sq :: "'a::times => 'a" where "sq x == x*x"
text {* The following lemma essentially shows that every natural
number is the sum of four squares, provided all prime numbers are.
However, this is an abstract theorem about commutative rings. It has,
a priori, nothing to do with nat. *}
+(* These two simprocs are even less efficient than ordered rewriting
+ and kill the second example: *)
ML_setup {*
Delsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]
*}
-lemma Lagrange_lemma:
- fixes x1 :: "'a::comm_ring"
- shows
+lemma Lagrange_lemma: fixes x1 :: "'a::comm_ring" shows
"(sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) =
- sq (x1*y1 - x2*y2 - x3*y3 - x4*y4) +
- 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_eq_simps)
+ sq (x1*y1 - x2*y2 - x3*y3 - x4*y4) +
+ 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)
-text {*
- A challenge by John Harrison. Takes about 17s on a 1.6GHz machine.
-*}
+text {* A challenge by John Harrison. Takes about 17s on a 1.6GHz machine. *}
-lemma
- fixes p1 :: "'a::comm_ring"
- shows
+lemma fixes p1 :: "'a::comm_ring" shows
"(sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) *
(sq p2 + sq q2 + sq r2 + sq s2 + sq t2 + sq u2 + sq v2 + sq w2)
= sq (p1*p2 - q1*q2 - r1*r2 - s1*s2 - t1*t2 - u1*u2 - v1*v2 - w1*w2) +
@@ -57,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_eq_simps)
+by (simp add: sq_def ring_simps)
end
--- a/src/HOL/ex/NatSum.thy Fri Jun 22 22:41:17 2007 +0200
+++ b/src/HOL/ex/NatSum.thy Sat Jun 23 19:33:22 2007 +0200
@@ -15,8 +15,7 @@
*}
lemmas [simp] =
- left_distrib right_distrib
- left_diff_distrib right_diff_distrib --{*for true subtraction*}
+ ring_distribs
diff_mult_distrib diff_mult_distrib2 --{*for type nat*}
text {*
--- a/src/HOL/ex/Reflected_Presburger.thy Fri Jun 22 22:41:17 2007 +0200
+++ b/src/HOL/ex/Reflected_Presburger.thy Sat Jun 23 19:33:22 2007 +0200
@@ -1,7 +1,7 @@
theory Reflected_Presburger
- imports GCD Main EfficientNat
- uses ("coopereif.ML") ("coopertac.ML")
- begin
+imports GCD Main EfficientNat
+uses ("coopereif.ML") ("coopertac.ML")
+begin
lemma allpairs_set: "set (allpairs Pair xs ys) = {(x,y). x\<in> set xs \<and> y \<in> set ys}"
by (induct xs) auto
@@ -463,8 +463,10 @@
lemma numadd: "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 \<le> n2", simp_all)
-by (case_tac "n1 = n2", simp_all add: ring_eq_simps)
-(simp add: ring_eq_simps(1)[symmetric])
+ apply (case_tac "n1 = n2")
+ apply(simp_all add: ring_simps)
+apply(simp add: left_distrib[symmetric])
+done
lemma numadd_nb: "\<lbrakk> numbound0 t ; numbound0 s\<rbrakk> \<Longrightarrow> numbound0 (numadd (t,s))"
by (induct t s rule: numadd.induct, auto simp add: Let_def)
@@ -476,7 +478,7 @@
"nummul t = (\<lambda> i. Mul i t)"
lemma nummul: "\<And> i. Inum bs (nummul t i) = Inum bs (Mul i t)"
-by (induct t rule: nummul.induct, auto simp add: ring_eq_simps numadd)
+by (induct t rule: nummul.induct, auto simp add: ring_simps numadd)
lemma nummul_nb: "\<And> i. numbound0 t \<Longrightarrow> numbound0 (nummul t i)"
by (induct t rule: nummul.induct, auto simp add: numadd_nb)
@@ -907,7 +909,7 @@
have Ia:"Inum (i # bs) a = Inum (i #bs) (CX ?c ?r)" and nb: "numbound0 ?r" by auto
let ?N = "\<lambda> t. Inum (i#bs) t"
from prems Ia nb show ?case
- by (auto simp add: Let_def split_def ring_eq_simps) (cases "?r",auto)
+ by (auto simp add: Let_def split_def ring_simps) (cases "?r",auto)
next
case (6 a)
let ?c = "fst (zsplit0 a)"
@@ -917,7 +919,7 @@
have Ia:"Inum (i # bs) a = Inum (i #bs) (CX ?c ?r)" and nb: "numbound0 ?r" by auto
let ?N = "\<lambda> t. Inum (i#bs) t"
from prems Ia nb show ?case
- by (auto simp add: Let_def split_def ring_eq_simps) (cases "?r",auto)
+ by (auto simp add: Let_def split_def ring_simps) (cases "?r",auto)
next
case (7 a)
let ?c = "fst (zsplit0 a)"
@@ -927,7 +929,7 @@
have Ia:"Inum (i # bs) a = Inum (i #bs) (CX ?c ?r)" and nb: "numbound0 ?r" by auto
let ?N = "\<lambda> t. Inum (i#bs) t"
from prems Ia nb show ?case
- by (auto simp add: Let_def split_def ring_eq_simps) (cases "?r",auto)
+ by (auto simp add: Let_def split_def ring_simps) (cases "?r",auto)
next
case (8 a)
let ?c = "fst (zsplit0 a)"
@@ -937,7 +939,7 @@
have Ia:"Inum (i # bs) a = Inum (i #bs) (CX ?c ?r)" and nb: "numbound0 ?r" by auto
let ?N = "\<lambda> t. Inum (i#bs) t"
from prems Ia nb show ?case
- by (auto simp add: Let_def split_def ring_eq_simps) (cases "?r",auto)
+ by (auto simp add: Let_def split_def ring_simps) (cases "?r",auto)
next
case (9 a)
let ?c = "fst (zsplit0 a)"
@@ -947,7 +949,7 @@
have Ia:"Inum (i # bs) a = Inum (i #bs) (CX ?c ?r)" and nb: "numbound0 ?r" by auto
let ?N = "\<lambda> t. Inum (i#bs) t"
from prems Ia nb show ?case
- by (auto simp add: Let_def split_def ring_eq_simps) (cases "?r",auto)
+ by (auto simp add: Let_def split_def ring_simps) (cases "?r",auto)
next
case (10 a)
let ?c = "fst (zsplit0 a)"
@@ -957,7 +959,7 @@
have Ia:"Inum (i # bs) a = Inum (i #bs) (CX ?c ?r)" and nb: "numbound0 ?r" by auto
let ?N = "\<lambda> t. Inum (i#bs) t"
from prems Ia nb show ?case
- by (auto simp add: Let_def split_def ring_eq_simps) (cases "?r",auto)
+ by (auto simp add: Let_def split_def ring_simps) (cases "?r",auto)
next
case (11 j a)
let ?c = "fst (zsplit0 a)"
@@ -1264,9 +1266,9 @@
(is "?ri dvd ?rc*?rx - ?rc*(?rk*?rd) + ?I x e" is "?ri dvd ?rt")
hence "\<exists> (l::int). ?rt = i * l" by (simp add: dvd_def)
hence "\<exists> (l::int). c*x+ ?I x e = i*l+c*(k * i*di)"
- by (simp add: ring_eq_simps di_def)
+ by (simp add: ring_simps di_def)
hence "\<exists> (l::int). c*x+ ?I x e = i*(l + c*k*di)"
- by (simp add: ring_eq_simps)
+ by (simp add: ring_simps)
hence "\<exists> (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
@@ -1275,7 +1277,7 @@
hence "\<exists> (l::int). c*x+?e = i*l" by (simp add: dvd_def)
hence "\<exists> (l::int). c*x - c*(k*d) +?e = i*l - c*(k*d)" by simp
hence "\<exists> (l::int). c*x - c*(k*d) +?e = i*l - c*(k*i*di)" by (simp add: di_def)
- hence "\<exists> (l::int). c*x - c*(k*d) +?e = i*((l - c*k*di))" by (simp add: ring_eq_simps)
+ hence "\<exists> (l::int). c*x - c*(k*d) +?e = i*((l - c*k*di))" by (simp add: ring_simps)
hence "\<exists> (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)
@@ -1291,9 +1293,9 @@
(is "?ri dvd ?rc*?rx - ?rc*(?rk*?rd) + ?I x e" is "?ri dvd ?rt")
hence "\<exists> (l::int). ?rt = i * l" by (simp add: dvd_def)
hence "\<exists> (l::int). c*x+ ?I x e = i*l+c*(k * i*di)"
- by (simp add: ring_eq_simps di_def)
+ by (simp add: ring_simps di_def)
hence "\<exists> (l::int). c*x+ ?I x e = i*(l + c*k*di)"
- by (simp add: ring_eq_simps)
+ by (simp add: ring_simps)
hence "\<exists> (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
@@ -1302,7 +1304,7 @@
hence "\<exists> (l::int). c*x+?e = i*l" by (simp add: dvd_def)
hence "\<exists> (l::int). c*x - c*(k*d) +?e = i*l - c*(k*d)" by simp
hence "\<exists> (l::int). c*x - c*(k*d) +?e = i*l - c*(k*i*di)" by (simp add: di_def)
- hence "\<exists> (l::int). c*x - c*(k*d) +?e = i*((l - c*k*di))" by (simp add: ring_eq_simps)
+ hence "\<exists> (l::int). c*x - c*(k*d) +?e = i*((l - c*k*di))" by (simp add: ring_simps)
hence "\<exists> (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)
@@ -1355,7 +1357,7 @@
by (simp only: zdvd_zminus_iff)
also have "\<dots> = (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_eq_simps)
+ by (simp add: ring_simps)
also have "\<dots> = Ifm bbs ((- x)#bs) (Dvd j (CX c e))"
using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"]
by simp
@@ -1367,7 +1369,7 @@
by (simp only: zdvd_zminus_iff)
also have "\<dots> = (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_eq_simps)
+ by (simp add: ring_simps)
also have "\<dots> = Ifm bbs ((- x)#bs) (Dvd j (CX c e))"
using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"]
by simp
@@ -1439,7 +1441,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 "\<dots> = ((l div c) * (c*x + Inum (x # bs) e) < (l div c) * 0)" by (simp add: ring_eq_simps)
+ also have "\<dots> = ((l div c) * (c*x + Inum (x # bs) e) < (l div c) * 0)" by (simp add: ring_simps)
also have "\<dots> = (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
@@ -1457,7 +1459,7 @@
hence "(l*x + (l div c) * Inum (x# bs) e \<le> 0) =
((c * (l div c)) * x + (l div c) * Inum (x # bs) e \<le> 0)"
by simp
- also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) \<le> ((l div c)) * 0)" by (simp add: ring_eq_simps)
+ also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) \<le> ((l div c)) * 0)" by (simp add: ring_simps)
also have "\<dots> = (c*x + Inum (x # bs) e \<le> 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
@@ -1475,7 +1477,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 "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) > ((l div c)) * 0)" by (simp add: ring_eq_simps)
+ also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) > ((l div c)) * 0)" by (simp add: ring_simps)
also have "\<dots> = (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
@@ -1494,7 +1496,7 @@
((c*(l div c))*x + (l div c)* Inum (x # bs) e \<ge> 0)"
by simp
also have "\<dots> = ((l div c)*(c*x + Inum (x # bs) e) \<ge> ((l div c)) * 0)"
- by (simp add: ring_eq_simps)
+ by (simp add: ring_simps)
also have "\<dots> = (c*x + Inum (x # bs) e \<ge> 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"]
@@ -1513,7 +1515,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 "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) = ((l div c)) * 0)" by (simp add: ring_eq_simps)
+ also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) = ((l div c)) * 0)" by (simp add: ring_simps)
also have "\<dots> = (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
@@ -1531,7 +1533,7 @@
hence "(l * x + (l div c) * Inum (x # bs) e \<noteq> 0) =
((c * (l div c)) * x + (l div c) * Inum (x # bs) e \<noteq> 0)"
by simp
- also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) \<noteq> ((l div c)) * 0)" by (simp add: ring_eq_simps)
+ also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) \<noteq> ((l div c)) * 0)" by (simp add: ring_simps)
also have "\<dots> = (c * x + Inum (x # bs) e \<noteq> 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
@@ -1547,7 +1549,7 @@
hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
by simp
hence "(\<exists> (k::int). l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) = (\<exists> (k::int). (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)" by simp
- also have "\<dots> = (\<exists> (k::int). (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c)*0)" by (simp add: ring_eq_simps)
+ also have "\<dots> = (\<exists> (k::int). (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c)*0)" by (simp add: ring_simps)
also have "\<dots> = (\<exists> (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 "\<dots> = (\<exists> (k::int). c * x + Inum (x # bs) e = j * k)" by simp
@@ -1564,7 +1566,7 @@
hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
by simp
hence "(\<exists> (k::int). l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) = (\<exists> (k::int). (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)" by simp
- also have "\<dots> = (\<exists> (k::int). (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c)*0)" by (simp add: ring_eq_simps)
+ also have "\<dots> = (\<exists> (k::int). (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c)*0)" by (simp add: ring_simps)
also have "\<dots> = (\<exists> (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 "\<dots> = (\<exists> (k::int). c * x + Inum (x # bs) e = j * k)" by simp
@@ -1613,7 +1615,7 @@
hence "x + ?e \<ge> 1 \<and> x + ?e \<le> d" by simp
hence "\<exists> (j::int) \<in> {1 .. d}. j = x + ?e" by simp
hence "\<exists> (j::int) \<in> {1 .. d}. x = (- ?e + j)"
- by (simp add: ring_eq_simps)
+ by (simp add: ring_simps)
with nob have ?case by auto}
ultimately show ?case by blast
next
@@ -1632,7 +1634,7 @@
from H p have "x + ?e \<ge> 0 \<and> x + ?e < d" by (simp add: c1)
hence "x + ?e +1 \<ge> 1 \<and> x + ?e + 1 \<le> d" by simp
hence "\<exists> (j::int) \<in> {1 .. d}. j = x + ?e + 1" by simp
- hence "\<exists> (j::int) \<in> {1 .. d}. x= - ?e - 1 + j" by (simp add: ring_eq_simps)
+ hence "\<exists> (j::int) \<in> {1 .. d}. x= - ?e - 1 + j" by (simp add: ring_simps)
with nob have ?case by simp }
ultimately show ?case by blast
next
@@ -1642,7 +1644,7 @@
have vb: "?v \<in> set (\<beta> (Eq (CX 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_eq_simps numbound0_I[OF bn,where b="x"and b'="a"and bs="bs"])
+ simp_all add:ring_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 (CX 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"
--- a/src/HOL/ex/ReflectionEx.thy Fri Jun 22 22:41:17 2007 +0200
+++ b/src/HOL/ex/ReflectionEx.thy Sat Jun 23 19:33:22 2007 +0200
@@ -164,7 +164,7 @@
lemma lin_add: "Inum bs (lin_add (t,s)) = Inum bs (Add t s)"
apply (induct t s rule: lin_add.induct, simp_all add: Let_def)
apply (case_tac "c1+c2 = 0",case_tac "n1 \<le> n2", simp_all)
-by (case_tac "n1 = n2", simp_all add: ring_eq_simps)
+by (case_tac "n1 = n2", simp_all add: ring_simps)
consts lin_mul :: "num \<Rightarrow> nat \<Rightarrow> num"
recdef lin_mul "measure size "
@@ -173,7 +173,7 @@
"lin_mul t = (\<lambda> i. Mul i t)"
lemma lin_mul: "Inum bs (lin_mul t i) = Inum bs (Mul i t)"
-by (induct t arbitrary: i rule: lin_mul.induct, auto simp add: ring_eq_simps)
+by (induct t arbitrary: i rule: lin_mul.induct, auto simp add: ring_simps)
consts linum:: "num \<Rightarrow> num"
recdef linum "measure num_size"