--- a/src/HOL/Decision_Procs/Approximation.thy Thu Oct 30 16:36:44 2014 +0000
+++ b/src/HOL/Decision_Procs/Approximation.thy Thu Oct 30 21:02:01 2014 +0100
@@ -1,4 +1,4 @@
-(* Author: Johannes Hoelzl, TU Muenchen
+ (* Author: Johannes Hoelzl, TU Muenchen
Coercions removed by Dmitriy Traytel *)
header {* Prove Real Valued Inequalities by Computation *}
--- a/src/HOL/Decision_Procs/Commutative_Ring.thy Thu Oct 30 16:36:44 2014 +0000
+++ b/src/HOL/Decision_Procs/Commutative_Ring.thy Thu Oct 30 21:02:01 2014 +0100
@@ -269,7 +269,7 @@
by (simp add: even_pow sqr_ci power_mult_distrib power_add [symmetric] mult_2 [symmetric] even_two_times_div_two)
next
case False with * show ?thesis
- by (simp add: odd_pow mul_ci sqr_ci power_mult_distrib power_add [symmetric] mult_2 [symmetric] power_Suc [symmetric] odd_two_times_div_two_Suc)
+ by (simp add: odd_pow mul_ci sqr_ci power_mult_distrib power_add [symmetric] mult_2 [symmetric] power_Suc [symmetric])
qed
qed
qed
--- a/src/HOL/Decision_Procs/Rat_Pair.thy Thu Oct 30 16:36:44 2014 +0000
+++ b/src/HOL/Decision_Procs/Rat_Pair.thy Thu Oct 30 21:02:01 2014 +0100
@@ -211,11 +211,7 @@
lemma of_int_div: "(d::int) ~= 0 ==> d dvd n ==>
(of_int(n div d)::'a::field_char_0) = of_int n / of_int d"
- apply (frule of_int_div_aux [of d n, where ?'a = 'a])
- apply simp
- apply (simp add: dvd_eq_mod_eq_0)
- done
-
+ using of_int_div_aux [of d n, where ?'a = 'a] by simp
lemma normNum[simp]: "INum (normNum x) = (INum x :: 'a::{field_char_0, field_inverse_zero})"
proof -
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Thu Oct 30 16:36:44 2014 +0000
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Thu Oct 30 21:02:01 2014 +0100
@@ -790,7 +790,7 @@
also have "\<dots> = (Ipoly bs p) ^ (Suc (Suc (Suc 0) * (Suc n div Suc (Suc 0))))"
by (simp only: th)
finally have ?case unfolding numeral_2_eq_2 [symmetric]
- using odd_two_times_div_two_Suc [OF odd] by simp
+ using odd_two_times_div_two_nat [OF odd] by simp
}
moreover
{
--- a/src/HOL/Divides.thy Thu Oct 30 16:36:44 2014 +0000
+++ b/src/HOL/Divides.thy Thu Oct 30 21:02:01 2014 +0100
@@ -149,20 +149,24 @@
note that ultimately show thesis by blast
qed
-lemma dvd_eq_mod_eq_0 [code]: "a dvd b \<longleftrightarrow> b mod a = 0"
+lemma dvd_imp_mod_0 [simp]:
+ assumes "a dvd b"
+ shows "b mod a = 0"
+proof -
+ from assms obtain c where "b = a * c" ..
+ then have "b mod a = a * c mod a" by simp
+ then show "b mod a = 0" by simp
+qed
+
+lemma dvd_eq_mod_eq_0 [code]:
+ "a dvd b \<longleftrightarrow> b mod a = 0"
proof
assume "b mod a = 0"
with mod_div_equality [of b a] have "b div a * a = b" by simp
then have "b = a * (b div a)" unfolding mult.commute ..
- then have "\<exists>c. b = a * c" ..
- then show "a dvd b" unfolding dvd_def .
+ then show "a dvd b" ..
next
- assume "a dvd b"
- then have "\<exists>c. b = a * c" unfolding dvd_def .
- then obtain c where "b = a * c" ..
- then have "b mod a = a * c mod a" by simp
- then have "b mod a = c * a mod a" by (simp add: mult.commute)
- then show "b mod a = 0" by simp
+ assume "a dvd b" then show "b mod a = 0" by simp
qed
lemma mod_div_trivial [simp]: "a mod b div b = 0"
@@ -190,36 +194,37 @@
finally show ?thesis .
qed
-lemma dvd_imp_mod_0: "a dvd b \<Longrightarrow> b mod a = 0"
-by (rule dvd_eq_mod_eq_0[THEN iffD1])
-
-lemma dvd_div_mult_self: "a dvd b \<Longrightarrow> (b div a) * a = b"
-by (subst (2) mod_div_equality [of b a, symmetric]) (simp add:dvd_imp_mod_0)
-
-lemma dvd_mult_div_cancel: "a dvd b \<Longrightarrow> a * (b div a) = b"
-by (drule dvd_div_mult_self) (simp add: mult.commute)
-
-lemma dvd_div_mult: "a dvd b \<Longrightarrow> (b div a) * c = b * c div a"
-apply (cases "a = 0")
- apply simp
-apply (auto simp: dvd_def mult.assoc)
-done
-
-lemma div_dvd_div[simp]:
- "a dvd b \<Longrightarrow> a dvd c \<Longrightarrow> (b div a dvd c div a) = (b dvd c)"
-apply (cases "a = 0")
- apply simp
+lemma dvd_div_mult_self [simp]:
+ "a dvd b \<Longrightarrow> (b div a) * a = b"
+ using mod_div_equality [of b a, symmetric] by simp
+
+lemma dvd_mult_div_cancel [simp]:
+ "a dvd b \<Longrightarrow> a * (b div a) = b"
+ using dvd_div_mult_self by (simp add: ac_simps)
+
+lemma dvd_div_mult:
+ "a dvd b \<Longrightarrow> (b div a) * c = (b * c) div a"
+ by (cases "a = 0") (auto elim!: dvdE simp add: mult.assoc)
+
+lemma div_dvd_div [simp]:
+ assumes "a dvd b" and "a dvd c"
+ shows "b div a dvd c div a \<longleftrightarrow> b dvd c"
+using assms apply (cases "a = 0")
+apply auto
apply (unfold dvd_def)
apply auto
apply(blast intro:mult.assoc[symmetric])
apply(fastforce simp add: mult.assoc)
done
-lemma dvd_mod_imp_dvd: "[| k dvd m mod n; k dvd n |] ==> k dvd m"
- apply (subgoal_tac "k dvd (m div n) *n + m mod n")
- apply (simp add: mod_div_equality)
- apply (simp only: dvd_add dvd_mult)
- done
+lemma dvd_mod_imp_dvd:
+ assumes "k dvd m mod n" and "k dvd n"
+ shows "k dvd m"
+proof -
+ from assms have "k dvd (m div n) * n + m mod n"
+ by (simp only: dvd_add dvd_mult)
+ then show ?thesis by (simp add: mod_div_equality)
+qed
text {* Addition respects modular equivalence. *}
@@ -593,7 +598,7 @@
"even a \<Longrightarrow> 2 * (a div 2) = a"
by (fact dvd_mult_div_cancel)
-lemma odd_two_times_div_two_succ:
+lemma odd_two_times_div_two_succ [simp]:
"odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
using mod_div_equality2 [of 2 a] by (simp add: even_iff_mod_2_eq_zero)
@@ -1528,10 +1533,14 @@
"odd n \<Longrightarrow> Suc n div 2 = Suc (n div 2)"
using odd_succ_div_two [of n] by simp
-lemma odd_two_times_div_two_Suc:
- "odd n \<Longrightarrow> Suc (2 * (n div 2)) = n"
+lemma odd_two_times_div_two_nat [simp]:
+ "odd n \<Longrightarrow> 2 * (n div 2) = n - (1 :: nat)"
using odd_two_times_div_two_succ [of n] by simp
+lemma odd_Suc_minus_one [simp]:
+ "odd n \<Longrightarrow> Suc (n - Suc 0) = n"
+ by (auto elim: oddE)
+
lemma parity_induct [case_names zero even odd]:
assumes zero: "P 0"
assumes even: "\<And>n. P n \<Longrightarrow> P (2 * n)"
@@ -1549,11 +1558,11 @@
proof (cases "even n")
case True
with hyp even [of "n div 2"] show ?thesis
- by (simp add: dvd_mult_div_cancel)
+ by simp
next
case False
with hyp odd [of "n div 2"] show ?thesis
- by (simp add: odd_two_times_div_two_Suc)
+ by simp
qed
qed
qed
--- a/src/HOL/GCD.thy Thu Oct 30 16:36:44 2014 +0000
+++ b/src/HOL/GCD.thy Thu Oct 30 21:02:01 2014 +0100
@@ -584,8 +584,8 @@
from dvdg dvdg' obtain ka kb ka' kb' where
kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'"
unfolding dvd_def by blast
- then have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'"
- by simp_all
+ from this [symmetric] have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'"
+ by (simp_all add: mult.assoc mult.left_commute [of "gcd a b"])
then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)]
dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
--- a/src/HOL/Library/Float.thy Thu Oct 30 16:36:44 2014 +0000
+++ b/src/HOL/Library/Float.thy Thu Oct 30 21:02:01 2014 +0100
@@ -935,8 +935,7 @@
unfolding normfloat_def
using ceil_divide_floor_conv[of y x'] powr_realpow[of 2 "nat l"] `0 \<le> l` `y \<noteq> 0`
l_def[symmetric, THEN meta_eq_to_obj_eq]
- by transfer
- (simp add: floor_divide_eq_div[symmetric] dvd_eq_mod_eq_0 round_up_def)
+ by transfer (auto simp add: floor_divide_eq_div [symmetric] round_up_def)
next
assume "\<not> 0 \<le> l"
def y' \<equiv> "y * 2 ^ nat (- l)"
@@ -950,7 +949,7 @@
using ceil_divide_floor_conv[of y' x] `\<not> 0 \<le> l` `y' \<noteq> 0` `y \<noteq> 0`
l_def[symmetric, THEN meta_eq_to_obj_eq]
by transfer
- (simp add: round_up_def ceil_divide_floor_conv floor_divide_eq_div[symmetric] dvd_eq_mod_eq_0)
+ (auto simp add: round_up_def ceil_divide_floor_conv floor_divide_eq_div [symmetric])
qed
qed
hide_fact (open) compute_rapprox_posrat
--- a/src/HOL/Library/Nat_Bijection.thy Thu Oct 30 16:36:44 2014 +0000
+++ b/src/HOL/Library/Nat_Bijection.thy Thu Oct 30 21:02:01 2014 +0100
@@ -122,7 +122,7 @@
by (induct x) simp_all
lemma sum_decode_inverse [simp]: "sum_encode (sum_decode n) = n"
- by (simp add: even_two_times_div_two odd_two_times_div_two_Suc sum_decode_def sum_encode_def)
+ by (simp add: even_two_times_div_two sum_decode_def sum_encode_def)
lemma inj_sum_encode: "inj_on sum_encode A"
by (rule inj_on_inverseI, rule sum_encode_inverse)
@@ -269,12 +269,18 @@
by auto
lemma div2_even_ext_nat:
- "x div 2 = y div 2 \<Longrightarrow> even x \<longleftrightarrow> even y \<Longrightarrow> (x::nat) = y"
-apply (rule mod_div_equality [of x 2, THEN subst])
-apply (rule mod_div_equality [of y 2, THEN subst])
-apply (cases "even x")
-apply (simp_all add: even_iff_mod_2_eq_zero)
-done
+ fixes x y :: nat
+ assumes "x div 2 = y div 2"
+ and "even x \<longleftrightarrow> even y"
+ shows "x = y"
+proof -
+ from `even x \<longleftrightarrow> even y` have "x mod 2 = y mod 2"
+ by (simp only: even_iff_mod_2_eq_zero) auto
+ with assms have "x div 2 * 2 + x mod 2 = y div 2 * 2 + y mod 2"
+ by simp
+ then show ?thesis
+ by simp
+qed
subsubsection {* From sets to naturals *}
--- a/src/HOL/Number_Theory/Gauss.thy Thu Oct 30 16:36:44 2014 +0000
+++ b/src/HOL/Number_Theory/Gauss.thy Thu Oct 30 21:02:01 2014 +0100
@@ -53,7 +53,7 @@
lemma p_eq2: "int p = (2 * ((int p - 1) div 2)) + 1"
using odd_p p_ge_2 div_mult_self1_is_id [of 2 "p - 1"]
- by auto presburger
+ by simp
lemma p_odd_int: obtains z::int where "int p = 2*z+1" "0<z"
using odd_p p_ge_2
--- a/src/HOL/Number_Theory/Pocklington.thy Thu Oct 30 16:36:44 2014 +0000
+++ b/src/HOL/Number_Theory/Pocklington.thy Thu Oct 30 21:02:01 2014 +0100
@@ -774,8 +774,8 @@
unfolding mod_eq_0_iff by blast
hence eq0: "(a^((n - 1) div p))^p = (n*s)^p" by simp
from qrn[symmetric] have qn1: "q dvd n - 1" unfolding dvd_def by auto
- from dvd_trans[OF p(2) qn1] div_mod_equality'[of "n - 1" p]
- have npp: "(n - 1) div p * p = n - 1" by (simp add: dvd_eq_mod_eq_0)
+ from dvd_trans[OF p(2) qn1]
+ have npp: "(n - 1) div p * p = n - 1" by simp
with eq0 have "a^ (n - 1) = (n*s)^p"
by (simp add: power_mult[symmetric])
hence "1 = (n*s)^(Suc (p - 1)) mod n" using bqn p01 by simp
--- a/src/HOL/Old_Number_Theory/Legacy_GCD.thy Thu Oct 30 16:36:44 2014 +0000
+++ b/src/HOL/Old_Number_Theory/Legacy_GCD.thy Thu Oct 30 21:02:01 2014 +0100
@@ -207,7 +207,8 @@
from dvdg dvdg' obtain ka kb ka' kb' where
kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'"
unfolding dvd_def by blast
- then have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'" by simp_all
+ from this(3-4) [symmetric] have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'"
+ by (simp_all only: ac_simps mult.left_commute [of _ "gcd a b"])
then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)]
dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
@@ -351,7 +352,7 @@
hence "a * ((b - 1) * y) = d + (x*b*(b - 1) - d*b)"
by (simp only: diff_add_assoc[OF dble, of d, symmetric])
hence "a * ((b - 1) * y) = b*(x*(b - 1) - d) + d"
- by (simp only: diff_mult_distrib2 add.commute ac_simps)
+ by (simp only: diff_mult_distrib2 ac_simps)
hence ?thesis using H(1,2)
apply -
apply (rule exI[where x=d], simp)
@@ -641,7 +642,8 @@
from dvdg dvdg' obtain ka kb ka' kb' where
kab: "a = ?g*ka" "b = ?g*kb" "?a' = ?g'*ka'" "?b' = ?g' * kb'"
unfolding dvd_def by blast
- then have "?g* ?a' = (?g * ?g') * ka'" "?g* ?b' = (?g * ?g') * kb'" by simp_all
+ from this(3-4) [symmetric] have "?g* ?a' = (?g * ?g') * ka'" "?g* ?b' = (?g * ?g') * kb'"
+ by (simp_all only: ac_simps mult.left_commute [of _ "zgcd a b"])
then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)]
dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
--- a/src/HOL/Rat.thy Thu Oct 30 16:36:44 2014 +0000
+++ b/src/HOL/Rat.thy Thu Oct 30 21:02:01 2014 +0100
@@ -73,8 +73,8 @@
let ?a = "a div gcd a b"
let ?b = "b div gcd a b"
from `b \<noteq> 0` have "?b * gcd a b = b"
- by (simp add: dvd_div_mult_self)
- with `b \<noteq> 0` have "?b \<noteq> 0" by auto
+ by simp
+ with `b \<noteq> 0` have "?b \<noteq> 0" by fastforce
from `q = Fract a b` `b \<noteq> 0` `?b \<noteq> 0` have q: "q = Fract ?a ?b"
by (simp add: eq_rat dvd_div_mult mult.commute [of a])
from `b \<noteq> 0` have coprime: "coprime ?a ?b"
@@ -253,7 +253,8 @@
case False
moreover have "b div gcd a b * gcd a b = b"
by (rule dvd_div_mult_self) simp
- ultimately have "b div gcd a b \<noteq> 0" by auto
+ ultimately have "b div gcd a b * gcd a b \<noteq> 0" by simp
+ then have "b div gcd a b \<noteq> 0" by fastforce
with False show ?thesis by (simp add: eq_rat dvd_div_mult mult.commute [of a])
qed
--- a/src/HOL/Real.thy Thu Oct 30 16:36:44 2014 +0000
+++ b/src/HOL/Real.thy Thu Oct 30 21:02:01 2014 +0100
@@ -1132,12 +1132,10 @@
by (auto simp add: add_divide_distrib algebra_simps)
qed
-lemma real_of_int_div: "(d :: int) dvd n ==>
- real(n div d) = real n / real d"
- apply (subst real_of_int_div_aux)
- apply simp
- apply (simp add: dvd_eq_mod_eq_0)
-done
+lemma real_of_int_div:
+ fixes d n :: int
+ shows "d dvd n \<Longrightarrow> real (n div d) = real n / real d"
+ by (simp add: real_of_int_div_aux)
lemma real_of_int_div2:
"0 <= real (n::int) / real (x) - real (n div x)"
@@ -1391,12 +1389,15 @@
by (rule dvd_mult_div_cancel)
have "?gcd dvd n" .. then have gcd_l: "?gcd * ?l = n"
by (rule dvd_mult_div_cancel)
- from `n\<noteq>0` and gcd_l have "?l \<noteq> 0" by (auto iff del: neq0_conv)
+ from `n \<noteq> 0` and gcd_l
+ have "?gcd * ?l \<noteq> 0" by simp
+ then have "?l \<noteq> 0" by (blast dest!: mult_not_zero)
moreover
have "\<bar>x\<bar> = real ?k / real ?l"
proof -
from gcd have "real ?k / real ?l =
- real (?gcd * ?k) / real (?gcd * ?l)" by simp
+ real (?gcd * ?k) / real (?gcd * ?l)"
+ by (simp only: real_of_nat_mult) simp
also from gcd_k and gcd_l have "\<dots> = real m / real n" by simp
also from x_rat have "\<dots> = \<bar>x\<bar>" ..
finally show ?thesis ..
--- a/src/HOL/Transcendental.thy Thu Oct 30 16:36:44 2014 +0000
+++ b/src/HOL/Transcendental.thy Thu Oct 30 21:02:01 2014 +0100
@@ -203,7 +203,7 @@
then show ?thesis by (auto simp add: even_two_times_div_two)
next
case False
- then have eq: "Suc (2 * (m div 2)) = m" by (simp add: odd_two_times_div_two_Suc)
+ then have eq: "Suc (2 * (m div 2)) = m" by simp
hence "even (2 * (m div 2))" using `odd m` by auto
have "?SUM m = ?SUM (Suc (2 * (m div 2)))" unfolding eq ..
also have "\<dots> = ?SUM (2 * (m div 2))" using `even (2 * (m div 2))` by auto
--- a/src/HOL/Word/Bit_Representation.thy Thu Oct 30 16:36:44 2014 +0000
+++ b/src/HOL/Word/Bit_Representation.thy Thu Oct 30 21:02:01 2014 +0100
@@ -316,8 +316,7 @@
apply (clarsimp simp: mod_mult_mult1 [symmetric]
zmod_zdiv_equality [THEN diff_eq_eq [THEN iffD2 [THEN sym]]])
apply (rule trans [symmetric, OF _ emep1])
- apply auto
- apply (auto simp: even_iff_mod_2_eq_zero)
+ apply auto
done
subsection "Simplifications for (s)bintrunc"