--- a/NEWS Fri Jul 18 17:09:48 2008 +0200
+++ b/NEWS Fri Jul 18 18:25:53 2008 +0200
@@ -19,24 +19,11 @@
*** Pure ***
-* Command 'instance': attached definitions now longer accepted.
+* Command 'instance': attached definitions no longer accepted.
INCOMPATIBILITY, use proper 'instantiation' target.
* Keyword 'code_exception' now named 'code_abort'. INCOMPATIBILITY.
-* New ML antiquotation @{code}: takes constant as argument, generates
-corresponding code in background and inserts name of the corresponding
-resulting ML value/function/datatype constructor binding in place.
-All occurrences of @{code} with a single ML block are generated
-simultaneously. Provides a generic and safe interface for
-instrumentalizing code generation. See HOL/ex/Code_Antiq for a toy
-example, or HOL/Complex/ex/ReflectedFerrack for a more ambitious
-application. In future you ought refrain from ad-hoc compiling
-generated SML code on the ML toplevel. Note that (for technical
-reasons) @{code} cannot refer to constants for which user-defined
-serializations are set. Refer to the corresponding ML counterpart
-directly in that cases.
-
*** Document preparation ***
@@ -47,6 +34,19 @@
*** HOL ***
+* HOL/Ring_and_Field and HOL/Divides: Definition of "op dvd" has been moved
+to separate class dvd in Ring_and_Field; a couple of lemmas on dvd has been
+generalized to class comm_semiring_1. Likewise a bunch of lemmas from Divides
+has been generalized from nat to class semiring_div. INCOMPATIBILITY.
+This involves the following theorem renames resulting from duplicate elimination:
+
+ dvd_def_mod ~> dvd_eq_mod_eq_0
+ zero_dvd_iff ~> dvd_0_left_iff
+ DIVISION_BY_ZERO_DIV ~> div_by_0
+ DIVISION_BY_ZERO_MOD ~> mod_by_0
+ mult_div ~> div_mult_self2_is_id
+ mult_mod ~> mod_mult_self2_is_0
+
* HOL/Library/GCD: Curried operations gcd, lcm (for nat) and zgcd,
zlcm (for int); carried together from various gcd/lcm developements in
the HOL Distribution. zgcd and zlcm replace former igcd and ilcm;
@@ -63,6 +63,19 @@
* HOL/Real/Rational: 'Fract k 0' now equals '0'. INCOMPATIBILITY.
+* New ML antiquotation @{code}: takes constant as argument, generates
+corresponding code in background and inserts name of the corresponding
+resulting ML value/function/datatype constructor binding in place.
+All occurrences of @{code} with a single ML block are generated
+simultaneously. Provides a generic and safe interface for
+instrumentalizing code generation. See HOL/ex/Code_Antiq for a toy
+example, or HOL/Complex/ex/ReflectedFerrack for a more ambitious
+application. In future you ought refrain from ad-hoc compiling
+generated SML code on the ML toplevel. Note that (for technical
+reasons) @{code} cannot refer to constants for which user-defined
+serializations are set. Refer to the corresponding ML counterpart
+directly in that cases.
+
* Integrated image HOL-Complex with HOL. Entry points Main.thy and
Complex_Main.thy remain as they are.
--- a/src/HOL/Algebra/Exponent.thy Fri Jul 18 17:09:48 2008 +0200
+++ b/src/HOL/Algebra/Exponent.thy Fri Jul 18 18:25:53 2008 +0200
@@ -49,8 +49,7 @@
apply (erule disjE)
apply (rule disjI1)
apply (rule_tac [2] disjI2)
-apply (erule_tac n = m in dvdE)
-apply (erule_tac [2] n = n in dvdE, auto)
+apply (auto elim!: dvdE)
done
@@ -202,7 +201,7 @@
apply (drule contrapos_nn [OF _ leI, THEN notnotD], assumption)
apply (drule less_imp_le [of a])
apply (drule le_imp_power_dvd)
-apply (drule_tac n = "p ^ r" in dvd_trans, assumption)
+apply (drule_tac b = "p ^ r" in dvd_trans, assumption)
apply(metis dvd_diffD1 dvd_triv_right le_extend_mult linorder_linear linorder_not_less mult_commute nat_dvd_not_less neq0_conv)
done
--- a/src/HOL/Algebra/abstract/Ring2.thy Fri Jul 18 17:09:48 2008 +0200
+++ b/src/HOL/Algebra/abstract/Ring2.thy Fri Jul 18 18:25:53 2008 +0200
@@ -13,7 +13,7 @@
subsection {* Ring axioms *}
-class ring = zero + one + plus + minus + uminus + times + inverse + power + Divides.dvd +
+class ring = zero + one + plus + minus + uminus + times + inverse + power + Ring_and_Field.dvd +
assumes a_assoc: "(a + b) + c = a + (b + c)"
and l_zero: "0 + a = a"
and l_neg: "(-a) + a = 0"
--- a/src/HOL/Algebra/poly/UnivPoly2.thy Fri Jul 18 17:09:48 2008 +0200
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy Fri Jul 18 18:25:53 2008 +0200
@@ -140,7 +140,7 @@
end
-instance up :: ("{times, comm_monoid_add}") Divides.dvd ..
+instance up :: ("{times, comm_monoid_add}") Ring_and_Field.dvd ..
instantiation up :: ("{times, one, comm_monoid_add, uminus, minus}") inverse
begin
--- a/src/HOL/Complex/ex/Sqrt_Script.thy Fri Jul 18 17:09:48 2008 +0200
+++ b/src/HOL/Complex/ex/Sqrt_Script.thy Fri Jul 18 18:25:53 2008 +0200
@@ -23,7 +23,7 @@
lemma prime_dvd_other_side:
"n * n = p * (k * k) \<Longrightarrow> prime p \<Longrightarrow> p dvd n"
apply (subgoal_tac "p dvd n * n", blast dest: prime_dvd_mult)
- apply (rule_tac j = "k * k" in dvd_mult_left, simp)
+ apply auto
done
lemma reduction: "prime p \<Longrightarrow>
--- a/src/HOL/Divides.thy Fri Jul 18 17:09:48 2008 +0200
+++ b/src/HOL/Divides.thy Fri Jul 18 18:25:53 2008 +0200
@@ -4,7 +4,7 @@
Copyright 1999 University of Cambridge
*)
-header {* The division operators div, mod and the divides relation dvd *}
+header {* The division operators div and mod *}
theory Divides
imports Nat Power Product_Type
@@ -13,71 +13,22 @@
subsection {* Syntactic division operations *}
-class dvd = times
-begin
-
-definition
- dvd :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "dvd" 50)
-where
- [code func del]: "m dvd n \<longleftrightarrow> (\<exists>k. n = m * k)"
-
-end
-
-class div = times +
+class div = dvd +
fixes div :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "div" 70)
- fixes mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "mod" 70)
+ and mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "mod" 70)
-subsection {* Abstract divisibility in commutative semirings. *}
+subsection {* Abstract division in commutative semirings. *}
-class semiring_div = comm_semiring_1_cancel + dvd + div +
+class semiring_div = comm_semiring_1_cancel + div +
assumes mod_div_equality: "a div b * b + a mod b = a"
- and div_by_0: "a div 0 = 0"
- and mult_div: "b \<noteq> 0 \<Longrightarrow> a * b div b = a"
+ and div_by_0 [simp]: "a div 0 = 0"
+ and div_0 [simp]: "0 div a = 0"
+ and div_mult_self1 [simp]: "b \<noteq> 0 \<Longrightarrow> (a + c * b) div b = c + a div b"
begin
text {* @{const div} and @{const mod} *}
-lemma div_by_1: "a div 1 = a"
- using mult_div [of 1 a] zero_neq_one by simp
-
-lemma mod_by_1: "a mod 1 = 0"
-proof -
- from mod_div_equality [of a one] div_by_1 have "a + a mod 1 = a" by simp
- then have "a + a mod 1 = a + 0" by simp
- then show ?thesis by (rule add_left_imp_eq)
-qed
-
-lemma mod_by_0: "a mod 0 = a"
- using mod_div_equality [of a zero] by simp
-
-lemma mult_mod: "a * b mod b = 0"
-proof (cases "b = 0")
- case True then show ?thesis by (simp add: mod_by_0)
-next
- case False with mult_div have abb: "a * b div b = a" .
- from mod_div_equality have "a * b div b * b + a * b mod b = a * b" .
- with abb have "a * b + a * b mod b = a * b + 0" by simp
- then show ?thesis by (rule add_left_imp_eq)
-qed
-
-lemma mod_self: "a mod a = 0"
- using mult_mod [of one] by simp
-
-lemma div_self: "a \<noteq> 0 \<Longrightarrow> a div a = 1"
- using mult_div [of _ one] by simp
-
-lemma div_0: "0 div a = 0"
-proof (cases "a = 0")
- case True then show ?thesis by (simp add: div_by_0)
-next
- case False with mult_div have "0 * a div a = 0" .
- then show ?thesis by simp
-qed
-
-lemma mod_0: "0 mod a = 0"
- using mod_div_equality [of zero a] div_0 by simp
-
lemma mod_div_equality2: "b * (a div b) + a mod b = a"
unfolding mult_commute [of b]
by (rule mod_div_equality)
@@ -88,15 +39,95 @@
lemma div_mod_equality2: "(b * (a div b) + a mod b) + c = a + c"
by (simp add: mod_div_equality2)
-text {* The @{const dvd} relation *}
+lemma mod_by_0 [simp]: "a mod 0 = a"
+ using mod_div_equality [of a zero] by simp
+
+lemma mod_0 [simp]: "0 mod a = 0"
+ using mod_div_equality [of zero a] div_0 by simp
+
+lemma div_mult_self2 [simp]:
+ assumes "b \<noteq> 0"
+ shows "(a + b * c) div b = c + a div b"
+ using assms div_mult_self1 [of b a c] by (simp add: mult_commute)
-lemma dvdI [intro?]: "a = b * c \<Longrightarrow> b dvd a"
- unfolding dvd_def ..
+lemma mod_mult_self1 [simp]: "(a + c * b) mod b = a mod b"
+proof (cases "b = 0")
+ case True then show ?thesis by simp
+next
+ case False
+ have "a + c * b = (a + c * b) div b * b + (a + c * b) mod b"
+ by (simp add: mod_div_equality)
+ also from False div_mult_self1 [of b a c] have
+ "\<dots> = (c + a div b) * b + (a + c * b) mod b"
+ by (simp add: left_distrib add_ac)
+ finally have "a = a div b * b + (a + c * b) mod b"
+ by (simp add: add_commute [of a] add_assoc left_distrib)
+ then have "a div b * b + (a + c * b) mod b = a div b * b + a mod b"
+ by (simp add: mod_div_equality)
+ then show ?thesis by simp
+qed
+
+lemma mod_mult_self2 [simp]: "(a + b * c) mod b = a mod b"
+ by (simp add: mult_commute [of b])
+
+lemma div_mult_self1_is_id [simp]: "b \<noteq> 0 \<Longrightarrow> b * a div b = a"
+ using div_mult_self2 [of b 0 a] by simp
+
+lemma div_mult_self2_is_id [simp]: "b \<noteq> 0 \<Longrightarrow> a * b div b = a"
+ using div_mult_self1 [of b 0 a] by simp
+
+lemma mod_mult_self1_is_0 [simp]: "b * a mod b = 0"
+ using mod_mult_self2 [of 0 b a] by simp
+
+lemma mod_mult_self2_is_0 [simp]: "a * b mod b = 0"
+ using mod_mult_self1 [of 0 a b] by simp
-lemma dvdE [elim?]: "b dvd a \<Longrightarrow> (\<And>c. a = b * c \<Longrightarrow> P) \<Longrightarrow> P"
- unfolding dvd_def by blast
+lemma div_by_1 [simp]: "a div 1 = a"
+ using div_mult_self2_is_id [of 1 a] zero_neq_one by simp
+
+lemma mod_by_1 [simp]: "a mod 1 = 0"
+proof -
+ from mod_div_equality [of a one] div_by_1 have "a + a mod 1 = a" by simp
+ then have "a + a mod 1 = a + 0" by simp
+ then show ?thesis by (rule add_left_imp_eq)
+qed
+
+lemma mod_self [simp]: "a mod a = 0"
+ using mod_mult_self2_is_0 [of 1] by simp
+
+lemma div_self [simp]: "a \<noteq> 0 \<Longrightarrow> a div a = 1"
+ using div_mult_self2_is_id [of _ 1] by simp
+
+lemma div_add_self1:
+ assumes "b \<noteq> 0"
+ shows "(b + a) div b = a div b + 1"
+ using assms div_mult_self1 [of b a 1] by (simp add: add_commute)
-lemma dvd_def_mod [code func]: "a dvd b \<longleftrightarrow> b mod a = 0"
+lemma div_add_self2:
+ assumes "b \<noteq> 0"
+ shows "(a + b) div b = a div b + 1"
+ using assms div_add_self1 [of b a] by (simp add: add_commute)
+
+lemma mod_add_self1:
+ "(b + a) mod b = a mod b"
+ using mod_mult_self1 [of a 1 b] by (simp add: add_commute)
+
+lemma mod_add_self2:
+ "(a + b) mod b = a mod b"
+ using mod_mult_self1 [of a 1 b] by simp
+
+lemma mod_div_decomp:
+ fixes a b
+ obtains q r where "q = a div b" and "r = a mod b"
+ and "a = q * b + r"
+proof -
+ from mod_div_equality have "a = a div b * b + a mod b" by simp
+ moreover have "a div b = a div b" ..
+ moreover have "a mod b = a mod b" ..
+ note that ultimately show thesis by blast
+qed
+
+lemma dvd_eq_mod_eq_0 [code func]: "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
@@ -109,59 +140,9 @@
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 add: mult_mod)
-qed
-
-lemma dvd_refl: "a dvd a"
- unfolding dvd_def_mod mod_self ..
-
-lemma dvd_trans:
- assumes "a dvd b" and "b dvd c"
- shows "a dvd c"
-proof -
- from assms obtain v where "b = a * v" unfolding dvd_def by auto
- moreover from assms obtain w where "c = b * w" unfolding dvd_def by auto
- ultimately have "c = a * (v * w)" by (simp add: mult_assoc)
- then show ?thesis unfolding dvd_def ..
-qed
-
-lemma zero_dvd_iff [noatp]: "0 dvd a \<longleftrightarrow> a = 0"
- unfolding dvd_def by simp
-
-lemma dvd_0: "a dvd 0"
-unfolding dvd_def proof
- show "0 = a * 0" by simp
+ then show "b mod a = 0" by simp
qed
-lemma one_dvd: "1 dvd a"
- unfolding dvd_def by simp
-
-lemma dvd_mult: "a dvd c \<Longrightarrow> a dvd (b * c)"
- unfolding dvd_def by (blast intro: mult_left_commute)
-
-lemma dvd_mult2: "a dvd b \<Longrightarrow> a dvd (b * c)"
- apply (subst mult_commute)
- apply (erule dvd_mult)
- done
-
-lemma dvd_triv_right: "a dvd b * a"
- by (rule dvd_mult) (rule dvd_refl)
-
-lemma dvd_triv_left: "a dvd a * b"
- by (rule dvd_mult2) (rule dvd_refl)
-
-lemma mult_dvd_mono: "a dvd c \<Longrightarrow> b dvd d \<Longrightarrow> a * b dvd c * d"
- apply (unfold dvd_def, clarify)
- apply (rule_tac x = "k * ka" in exI)
- apply (simp add: mult_ac)
- done
-
-lemma dvd_mult_left: "a * b dvd c \<Longrightarrow> a dvd c"
- by (simp add: dvd_def mult_assoc, blast)
-
-lemma dvd_mult_right: "a * b dvd c \<Longrightarrow> b dvd c"
- unfolding mult_ac [of a] by (rule dvd_mult_left)
-
end
@@ -352,7 +333,10 @@
fix n :: nat show "n div 0 = 0"
using divmod_zero divmod_div_mod [of n 0] by simp
next
- fix m n :: nat assume "n \<noteq> 0" then show "m * n div n = m"
+ fix n :: nat show "0 div n = 0"
+ using divmod_rel [of 0 n] by (cases n) (simp_all add: divmod_rel_def)
+next
+ fix m n q :: nat assume "n \<noteq> 0" then show "(q + m * n) div n = m + q div n"
by (induct m) (simp_all add: le_div_geq)
qed
@@ -360,10 +344,8 @@
text {* Simproc for cancelling @{const div} and @{const mod} *}
-lemmas mod_div_equality = semiring_div_class.times_div_mod_plus_zero_one.mod_div_equality [of "m\<Colon>nat" n, standard]
-lemmas mod_div_equality2 = mod_div_equality2 [of "n\<Colon>nat" m, standard]
-lemmas div_mod_equality = div_mod_equality [of "m\<Colon>nat" n k, standard]
-lemmas div_mod_equality2 = div_mod_equality2 [of "m\<Colon>nat" n k, standard]
+(*lemmas mod_div_equality_nat = semiring_div_class.times_div_mod_plus_zero_one.mod_div_equality [of "m\<Colon>nat" n, standard]
+lemmas mod_div_equality2_nat = mod_div_equality2 [of "n\<Colon>nat" m, standard*)
ML {*
structure CancelDivModData =
@@ -414,9 +396,6 @@
subsubsection {* Quotient *}
-lemmas DIVISION_BY_ZERO_DIV [simp] = div_by_0 [of "a\<Colon>nat", standard]
-lemmas div_0 [simp] = semiring_div_class.div_0 [of "n\<Colon>nat", standard]
-
lemma div_geq: "0 < n \<Longrightarrow> \<not> m < n \<Longrightarrow> m div n = Suc ((m - n) div n)"
by (simp add: le_div_geq linorder_not_less)
@@ -424,17 +403,14 @@
by (simp add: div_geq)
lemma div_mult_self_is_m [simp]: "0<n ==> (m*n) div n = (m::nat)"
- by (rule mult_div) simp
+ by simp
lemma div_mult_self1_is_m [simp]: "0<n ==> (n*m) div n = (m::nat)"
- by (simp add: mult_commute)
+ by simp
subsubsection {* Remainder *}
-lemmas DIVISION_BY_ZERO_MOD [simp] = mod_by_0 [of "a\<Colon>nat", standard]
-lemmas mod_0 [simp] = semiring_div_class.mod_0 [of "n\<Colon>nat", standard]
-
lemma mod_less_divisor [simp]:
fixes m n :: nat
assumes "n > 0"
@@ -458,23 +434,6 @@
lemma mod_1 [simp]: "m mod Suc 0 = 0"
by (induct m) (simp_all add: mod_geq)
-lemmas mod_self [simp] = semiring_div_class.mod_self [of "n\<Colon>nat", standard]
-
-lemma mod_add_self2 [simp]: "(m+n) mod n = m mod (n::nat)"
- apply (subgoal_tac "(n + m) mod n = (n+m-n) mod n")
- apply (simp add: add_commute)
- apply (subst le_mod_geq [symmetric], simp_all)
- done
-
-lemma mod_add_self1 [simp]: "(n+m) mod n = m mod (n::nat)"
- by (simp add: add_commute mod_add_self2)
-
-lemma mod_mult_self1 [simp]: "(m + k*n) mod n = m mod (n::nat)"
- by (induct k) (simp_all add: add_left_commute [of _ n])
-
-lemma mod_mult_self2 [simp]: "(m + n*k) mod n = m mod (n::nat)"
- by (simp add: mult_commute mod_mult_self1)
-
lemma mod_mult_distrib: "(m mod n) * (k\<Colon>nat) = (m * k) mod (n * k)"
apply (cases "n = 0", simp)
apply (cases "k = 0", simp)
@@ -486,20 +445,9 @@
lemma mod_mult_distrib2: "(k::nat) * (m mod n) = (k*m) mod (k*n)"
by (simp add: mult_commute [of k] mod_mult_distrib)
-lemma mod_mult_self_is_0 [simp]: "(m*n) mod n = (0::nat)"
- apply (cases "n = 0", simp)
- apply (induct m, simp)
- apply (rename_tac k)
- apply (cut_tac m = "k * n" and n = n in mod_add_self2)
- apply (simp add: add_commute)
- done
-
-lemma mod_mult_self1_is_0 [simp]: "(n*m) mod n = (0::nat)"
- by (simp add: mult_commute mod_mult_self_is_0)
-
(* a simple rearrangement of mod_div_equality: *)
lemma mult_div_cancel: "(n::nat) * (m div n) = m - (m mod n)"
- by (cut_tac m = m and n = n in mod_div_equality2, arith)
+ by (cut_tac a = m and b = n in mod_div_equality2, arith)
lemma mod_le_divisor[simp]: "0 < n \<Longrightarrow> m mod n \<le> (n::nat)"
apply (drule mod_less_divisor [where m = m])
@@ -508,17 +456,6 @@
subsubsection {* Quotient and Remainder *}
-lemma mod_div_decomp:
- fixes n k :: nat
- obtains m q where "m = n div k" and "q = n mod k"
- and "n = m * k + q"
-proof -
- from mod_div_equality have "n = n div k * k + n mod k" by auto
- moreover have "n div k = n div k" ..
- moreover have "n mod k = n mod k" ..
- note that ultimately show thesis by blast
-qed
-
lemma divmod_rel_mult1_eq:
"[| divmod_rel b c q r; c > 0 |]
==> divmod_rel (a*b) c (a*q + a*r div c) (a*r mod c)"
@@ -610,25 +547,6 @@
lemma div_1 [simp]: "m div Suc 0 = m"
by (induct m) (simp_all add: div_geq)
-lemmas div_self [simp] = semiring_div_class.div_self [of "n\<Colon>nat", standard]
-
-lemma div_add_self2: "0<n ==> (m+n) div n = Suc (m div n)"
- apply (subgoal_tac "(n + m) div n = Suc ((n+m-n) div n) ")
- apply (simp add: add_commute)
- apply (subst div_geq [symmetric], simp_all)
- done
-
-lemma div_add_self1: "0<n ==> (n+m) div n = Suc (m div n)"
- by (simp add: add_commute div_add_self2)
-
-lemma div_mult_self1 [simp]: "!!n::nat. 0<n ==> (m + k*n) div n = k + m div n"
- apply (subst div_add1_eq)
- apply (subst div_mult1_eq, simp)
- done
-
-lemma div_mult_self2 [simp]: "0<n ==> (m + n*k) div n = k + m div (n::nat)"
- by (simp add: mult_commute div_mult_self1)
-
(* Monotonicity of div in first argument *)
lemma div_le_mono [rule_format (no_asm)]:
@@ -707,24 +625,7 @@
by (cases "n = 0") auto
-subsubsection{*The Divides Relation*}
-
-lemma dvdI [intro?]: "n = m * k ==> m dvd n"
- unfolding dvd_def by blast
-
-lemma dvdE [elim?]: "!!P. [|m dvd n; !!k. n = m*k ==> P|] ==> P"
- unfolding dvd_def by blast
-
-lemma dvd_0_right [iff]: "m dvd (0::nat)"
- unfolding dvd_def by (blast intro: mult_0_right [symmetric])
-
-lemma dvd_0_left: "0 dvd m ==> m = (0::nat)"
- by (force simp add: dvd_def)
-
-lemma dvd_0_left_iff [iff]: "(0 dvd (m::nat)) = (m = 0)"
- by (blast intro: dvd_0_left)
-
-declare dvd_0_left_iff [noatp]
+subsubsection {* The Divides Relation *}
lemma dvd_1_left [iff]: "Suc 0 dvd k"
unfolding dvd_def by simp
@@ -732,9 +633,6 @@
lemma dvd_1_iff_1 [simp]: "(m dvd Suc 0) = (m = Suc 0)"
by (simp add: dvd_def)
-lemmas dvd_refl [simp] = semiring_div_class.dvd_refl [of "m\<Colon>nat", standard]
-lemmas dvd_trans [trans] = semiring_div_class.dvd_trans [of "m\<Colon>nat" n p, standard]
-
lemma dvd_anti_sym: "[| m dvd n; n dvd m |] ==> m = (n::nat)"
unfolding dvd_def
by (force dest: mult_eq_self_implies_10 simp add: mult_assoc mult_eq_1_iff)
@@ -742,11 +640,7 @@
text {* @{term "op dvd"} is a partial order *}
interpretation dvd: order ["op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> n \<noteq> m"]
- by unfold_locales (auto intro: dvd_trans dvd_anti_sym)
-
-lemma dvd_add: "[| k dvd m; k dvd n |] ==> k dvd (m+n :: nat)"
- unfolding dvd_def
- by (blast intro: add_mult_distrib2 [symmetric])
+ by unfold_locales (auto intro: dvd_refl dvd_trans dvd_anti_sym)
lemma dvd_diff: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)"
unfolding dvd_def
@@ -760,20 +654,6 @@
lemma dvd_diffD1: "[| k dvd m-n; k dvd m; n\<le>m |] ==> k dvd (n::nat)"
by (drule_tac m = m in dvd_diff, auto)
-lemma dvd_mult: "k dvd n ==> k dvd (m*n :: nat)"
- unfolding dvd_def by (blast intro: mult_left_commute)
-
-lemma dvd_mult2: "k dvd m ==> k dvd (m*n :: nat)"
- apply (subst mult_commute)
- apply (erule dvd_mult)
- done
-
-lemma dvd_triv_right [iff]: "k dvd (m*k :: nat)"
- by (rule dvd_refl [THEN dvd_mult])
-
-lemma dvd_triv_left [iff]: "k dvd (k*m :: nat)"
- by (rule dvd_refl [THEN dvd_mult2])
-
lemma dvd_reduce: "(k dvd n + k) = (k dvd (n::nat))"
apply (rule iffI)
apply (erule_tac [2] dvd_add)
@@ -817,21 +697,6 @@
apply (erule dvd_mult_cancel1)
done
-lemma mult_dvd_mono: "[| i dvd m; j dvd n|] ==> i*j dvd (m*n :: nat)"
- apply (unfold dvd_def, clarify)
- apply (rule_tac x = "k*ka" in exI)
- apply (simp add: mult_ac)
- done
-
-lemma dvd_mult_left: "(i*j :: nat) dvd k ==> i dvd k"
- by (simp add: dvd_def mult_assoc, blast)
-
-lemma dvd_mult_right: "(i*j :: nat) dvd k ==> j dvd k"
- apply (unfold dvd_def, clarify)
- apply (rule_tac x = "i*k" in exI)
- apply (simp add: mult_ac)
- done
-
lemma dvd_imp_le: "[| k dvd n; 0 < n |] ==> k \<le> (n::nat)"
apply (unfold dvd_def, clarify)
apply (simp_all (no_asm_use) add: zero_less_mult_iff)
@@ -841,8 +706,6 @@
apply (erule_tac [2] Suc_leI, simp)
done
-lemmas dvd_eq_mod_eq_0 = dvd_def_mod [of "k\<Colon>nat" n, standard]
-
lemma dvd_mult_div_cancel: "n dvd m ==> n * (m div n) = (m::nat)"
apply (subgoal_tac "m mod n = 0")
apply (simp add: mult_div_cancel)
@@ -888,7 +751,7 @@
(*Loses information, namely we also have r<d provided d is nonzero*)
lemma mod_eqD: "(m mod d = r) ==> \<exists>q::nat. m = r + q*d"
- apply (cut_tac m = m in mod_div_equality)
+ apply (cut_tac a = m in mod_div_equality)
apply (simp only: add_ac)
apply (blast intro: sym)
done
@@ -902,7 +765,7 @@
show ?Q
proof (cases)
assume "k = 0"
- with P show ?Q by(simp add:DIVISION_BY_ZERO_DIV)
+ with P show ?Q by simp
next
assume not0: "k \<noteq> 0"
thus ?Q
@@ -924,7 +787,7 @@
show ?P
proof (cases)
assume "k = 0"
- with Q show ?P by(simp add:DIVISION_BY_ZERO_DIV)
+ with Q show ?P by simp
next
assume not0: "k \<noteq> 0"
with Q have R: ?R by simp
@@ -958,7 +821,7 @@
(\<exists>q. (n * q \<le> m \<and> m < n * (Suc q)) \<and> P q))"
apply (case_tac "0 < n")
apply (simp only: add: split_div_lemma)
- apply (simp_all add: DIVISION_BY_ZERO_DIV)
+ apply simp_all
done
lemma split_mod:
@@ -970,7 +833,7 @@
show ?Q
proof (cases)
assume "k = 0"
- with P show ?Q by(simp add:DIVISION_BY_ZERO_MOD)
+ with P show ?Q by simp
next
assume not0: "k \<noteq> 0"
thus ?Q
@@ -985,7 +848,7 @@
show ?P
proof (cases)
assume "k = 0"
- with Q show ?P by(simp add:DIVISION_BY_ZERO_MOD)
+ with Q show ?P by simp
next
assume not0: "k \<noteq> 0"
with Q have R: ?R by simp
--- a/src/HOL/HoareParallel/RG_Examples.thy Fri Jul 18 17:09:48 2008 +0200
+++ b/src/HOL/HoareParallel/RG_Examples.thy Fri Jul 18 18:25:53 2008 +0200
@@ -1,6 +1,8 @@
header {* \section{Examples} *}
-theory RG_Examples imports RG_Syntax begin
+theory RG_Examples
+imports RG_Syntax
+begin
lemmas definitions [simp]= stable_def Pre_def Rely_def Guar_def Post_def Com_def
@@ -291,18 +293,14 @@
apply force
apply force
apply(rule Basic)
- apply simp
+ apply (simp add: mod_add_self2)
apply clarify
apply simp
- apply(case_tac "X x (j mod n)\<le> j")
- apply(drule le_imp_less_or_eq)
- apply(erule disjE)
- apply(drule_tac j=j and n=n and i="j mod n" and a="X x (j mod n)" in mod_aux)
- apply assumption+
- apply simp+
- apply clarsimp
- apply fastsimp
-apply force+
+ apply (case_tac "X x (j mod n) \<le> j")
+ apply (drule le_imp_less_or_eq)
+ apply (erule disjE)
+ apply (drule_tac j=j and n=n and i="j mod n" and a="X x (j mod n)" in mod_aux)
+ apply auto
done
text {* Same but with a list as auxiliary variable: *}
@@ -348,16 +346,14 @@
apply(rule Basic)
apply simp
apply clarify
- apply simp
+ apply (simp add: mod_add_self2)
apply(rule allI)
apply(rule impI)+
apply(case_tac "X x ! i\<le> j")
apply(drule le_imp_less_or_eq)
apply(erule disjE)
apply(drule_tac j=j and n=n and i=i and a="X x ! i" in mod_aux)
- apply assumption+
- apply simp
-apply force+
+ apply auto
done
end
--- a/src/HOL/Import/HOL/divides.imp Fri Jul 18 17:09:48 2008 +0200
+++ b/src/HOL/Import/HOL/divides.imp Fri Jul 18 18:25:53 2008 +0200
@@ -9,16 +9,16 @@
"divides_def" > "HOL4Compat.divides_def"
"ONE_DIVIDES_ALL" > "HOL4Base.divides.ONE_DIVIDES_ALL"
"NOT_LT_DIV" > "NatSimprocs.nat_dvd_not_less"
- "DIVIDES_TRANS" > "Divides.dvd_trans"
- "DIVIDES_SUB" > "Divides.dvd_diff"
- "DIVIDES_REFL" > "Divides.dvd_refl"
+ "DIVIDES_TRANS" > "Ring_and_Field.dvd_trans"
+ "DIVIDES_SUB" > "Ring_and_Field.dvd_diff"
+ "DIVIDES_REFL" > "Ring_and_Field.dvd_refl"
"DIVIDES_MULT_LEFT" > "HOL4Base.divides.DIVIDES_MULT_LEFT"
"DIVIDES_MULT" > "Divides.dvd_mult2"
"DIVIDES_LE" > "Divides.dvd_imp_le"
"DIVIDES_FACT" > "HOL4Base.divides.DIVIDES_FACT"
"DIVIDES_ANTISYM" > "Divides.dvd_anti_sym"
"DIVIDES_ADD_2" > "HOL4Base.divides.DIVIDES_ADD_2"
- "DIVIDES_ADD_1" > "Divides.dvd_add"
+ "DIVIDES_ADD_1" > "Ring_and_Field.dvd_add"
"ALL_DIVIDES_0" > "Divides.dvd_0_right"
end
--- a/src/HOL/IntDiv.thy Fri Jul 18 17:09:48 2008 +0200
+++ b/src/HOL/IntDiv.thy Fri Jul 18 18:25:53 2008 +0200
@@ -747,8 +747,49 @@
lemma zdiv_zmult_self1 [simp]: "b \<noteq> (0::int) ==> (a*b) div b = a"
by (simp add: zdiv_zmult1_eq)
+lemma mod_div_trivial [simp]: "(a mod b) div b = (0::int)"
+apply (case_tac "b = 0", simp)
+apply (auto simp add: linorder_neq_iff div_pos_pos_trivial div_neg_neg_trivial)
+done
+
+lemma mod_mod_trivial [simp]: "(a mod b) mod b = a mod (b::int)"
+apply (case_tac "b = 0", simp)
+apply (force simp add: linorder_neq_iff mod_pos_pos_trivial mod_neg_neg_trivial)
+done
+
+text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *}
+
+lemma zadd1_lemma:
+ "[| quorem((a,c),(aq,ar)); quorem((b,c),(bq,br)); c \<noteq> 0 |]
+ ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))"
+by (force simp add: split_ifs quorem_def linorder_neq_iff right_distrib)
+
+(*NOT suitable for rewriting: the RHS has an instance of the LHS*)
+lemma zdiv_zadd1_eq:
+ "(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)"
+apply (case_tac "c = 0", simp)
+apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod] quorem_div)
+done
+
+lemma zmod_zadd1_eq: "(a+b) mod (c::int) = (a mod c + b mod c) mod c"
+apply (case_tac "c = 0", simp)
+apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod] quorem_mod)
+done
+
+lemma zdiv_zadd_self1[simp]: "a \<noteq> (0::int) ==> (a+b) div a = b div a + 1"
+by (simp add: zdiv_zadd1_eq)
+
+lemma zdiv_zadd_self2[simp]: "a \<noteq> (0::int) ==> (b+a) div a = b div a + 1"
+by (simp add: zdiv_zadd1_eq)
+
instance int :: semiring_div
- by intro_classes auto
+proof
+ fix a b c :: int
+ assume not0: "b \<noteq> 0"
+ show "(a + c * b) div b = c + a div b"
+ unfolding zdiv_zadd1_eq [of a "c * b"] using not0
+ by (simp add: zmod_zmult1_eq)
+qed auto
lemma zdiv_zmult_self2 [simp]: "b \<noteq> (0::int) ==> (b*a) div b = a"
by (subst mult_commute, erule zdiv_zmult_self1)
@@ -770,35 +811,6 @@
lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1]
-text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *}
-
-lemma zadd1_lemma:
- "[| quorem((a,c),(aq,ar)); quorem((b,c),(bq,br)); c \<noteq> 0 |]
- ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))"
-by (force simp add: split_ifs quorem_def linorder_neq_iff right_distrib)
-
-(*NOT suitable for rewriting: the RHS has an instance of the LHS*)
-lemma zdiv_zadd1_eq:
- "(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)"
-apply (case_tac "c = 0", simp)
-apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod] quorem_div)
-done
-
-lemma zmod_zadd1_eq: "(a+b) mod (c::int) = (a mod c + b mod c) mod c"
-apply (case_tac "c = 0", simp)
-apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod] quorem_mod)
-done
-
-lemma mod_div_trivial [simp]: "(a mod b) div b = (0::int)"
-apply (case_tac "b = 0", simp)
-apply (auto simp add: linorder_neq_iff div_pos_pos_trivial div_neg_neg_trivial)
-done
-
-lemma mod_mod_trivial [simp]: "(a mod b) mod b = a mod (b::int)"
-apply (case_tac "b = 0", simp)
-apply (force simp add: linorder_neq_iff mod_pos_pos_trivial mod_neg_neg_trivial)
-done
-
lemma zmod_zadd_left_eq: "(a+b) mod (c::int) = ((a mod c) + b) mod c"
apply (rule trans [symmetric])
apply (rule zmod_zadd1_eq, simp)
@@ -811,12 +823,6 @@
apply (rule zmod_zadd1_eq [symmetric])
done
-lemma zdiv_zadd_self1[simp]: "a \<noteq> (0::int) ==> (a+b) div a = b div a + 1"
-by (simp add: zdiv_zadd1_eq)
-
-lemma zdiv_zadd_self2[simp]: "a \<noteq> (0::int) ==> (b+a) div a = b div a + 1"
-by (simp add: zdiv_zadd1_eq)
-
lemma zmod_zadd_self1[simp]: "(a+b) mod a = b mod (a::int)"
apply (case_tac "a = 0", simp)
apply (simp add: zmod_zadd1_eq)
@@ -1183,33 +1189,36 @@
lemma zdvd_trans: "m dvd n ==> n dvd k ==> m dvd (k::int)"
by (auto simp add: dvd_def intro: mult_assoc)
-lemma zdvd_zminus_iff: "(m dvd -n) = (m dvd (n::int))"
- apply (simp add: dvd_def, auto)
- apply (rule_tac [!] x = "-k" in exI, auto)
- done
+lemma zdvd_zminus_iff: "m dvd -n \<longleftrightarrow> m dvd (n::int)"
+proof
+ assume "m dvd - n"
+ then obtain k where "- n = m * k" ..
+ then have "n = m * - k" by simp
+ then show "m dvd n" ..
+next
+ assume "m dvd n"
+ then have "m dvd n * -1" by (rule dvd_mult2)
+ then show "m dvd - n" by simp
+qed
-lemma zdvd_zminus2_iff: "(-m dvd n) = (m dvd (n::int))"
- apply (simp add: dvd_def, auto)
- apply (rule_tac [!] x = "-k" in exI, auto)
- done
+lemma zdvd_zminus2_iff: "-m dvd n \<longleftrightarrow> m dvd (n::int)"
+proof
+ assume "- m dvd n"
+ then obtain k where "n = - m * k" ..
+ then have "n = m * - k" by simp
+ then show "m dvd n" ..
+next
+ assume "m dvd n"
+ then obtain k where "n = m * k" ..
+ then have "n = - m * - k" by simp
+ then show "- m dvd n" ..
+qed
+
lemma zdvd_abs1: "( \<bar>i::int\<bar> dvd j) = (i dvd j)"
- apply (cases "i > 0", simp)
- apply (simp add: dvd_def)
- apply (rule iffI)
- apply (erule exE)
- apply (rule_tac x="- k" in exI, simp)
- apply (erule exE)
- apply (rule_tac x="- k" in exI, simp)
- done
+ by (cases "i > 0") (simp_all add: zdvd_zminus2_iff)
+
lemma zdvd_abs2: "( (i::int) dvd \<bar>j\<bar>) = (i dvd j)"
- apply (cases "j > 0", simp)
- apply (simp add: dvd_def)
- apply (rule iffI)
- apply (erule exE)
- apply (rule_tac x="- k" in exI, simp)
- apply (erule exE)
- apply (rule_tac x="- k" in exI, simp)
- done
+ by (cases "j > 0") (simp_all add: zdvd_zminus_iff)
lemma zdvd_anti_sym:
"0 < m ==> 0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)"
@@ -1276,10 +1285,7 @@
done
lemma zdvd_zmult_mono: "i dvd m ==> j dvd (n::int) ==> i * j dvd m * n"
- apply (simp add: dvd_def, clarify)
- apply (rule_tac x = "k * ka" in exI)
- apply (simp add: mult_ac)
- done
+ by (rule mult_dvd_mono)
lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))"
apply (rule iffI)
@@ -1301,7 +1307,7 @@
done
lemma zdvd_not_zless: "0 < m ==> m < n ==> \<not> n dvd (m::int)"
- apply (simp add: dvd_def, auto)
+ apply (auto elim!: dvdE)
apply (subgoal_tac "0 < n")
prefer 2
apply (blast intro: order_less_trans)
@@ -1309,6 +1315,7 @@
apply (subgoal_tac "n * k < n * 1")
apply (drule mult_less_cancel_left [THEN iffD1], auto)
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_simps)
@@ -1348,21 +1355,24 @@
done
theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
-apply (simp only: dvd_def ex_nat int_int_eq [symmetric] zmult_int [symmetric]
- nat_0_le cong add: conj_cong)
-apply (rule iffI)
-apply iprover
-apply (erule exE)
-apply (case_tac "x=0")
-apply (rule_tac x=0 in exI)
-apply simp
-apply (case_tac "0 \<le> k")
-apply iprover
-apply (simp add: neq0_conv linorder_not_le)
-apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])
-apply assumption
-apply (simp add: mult_ac)
-done
+proof -
+ have "\<And>k. int y = int x * k \<Longrightarrow> x dvd y"
+ proof -
+ fix k
+ assume A: "int y = int x * k"
+ then show "x dvd y" proof (cases k)
+ case (1 n) with A have "y = x * n" by (simp add: zmult_int)
+ then show ?thesis ..
+ next
+ case (2 n) with A have "int y = int x * (- int (Suc n))" by simp
+ also have "\<dots> = - (int x * int (Suc n))" by (simp only: mult_minus_right)
+ also have "\<dots> = - int (x * Suc n)" by (simp only: zmult_int)
+ finally have "- int (x * Suc n) = int y" ..
+ then show ?thesis by (simp only: negative_eq_positive) auto
+ qed
+ qed
+ then show ?thesis by (auto elim!: dvdE simp only: zmult_int [symmetric])
+qed
lemma zdvd1_eq[simp]: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)"
proof
@@ -1385,41 +1395,19 @@
qed
lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))"
- apply (auto simp add: dvd_def nat_abs_mult_distrib)
- apply (auto simp add: nat_eq_iff abs_if split add: split_if_asm)
- apply (rule_tac x = "-(int k)" in exI)
- apply (auto simp add: int_mult)
- done
+ unfolding zdvd_int by (cases "z \<ge> 0") (simp_all add: zdvd_zminus_iff)
lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
- apply (auto simp add: dvd_def abs_if int_mult)
- apply (rule_tac [3] x = "nat k" in exI)
- apply (rule_tac [2] x = "-(int k)" in exI)
- apply (rule_tac x = "nat (-k)" in exI)
- apply (cut_tac [3] k = m in int_less_0_conv)
- apply (cut_tac k = m in int_less_0_conv)
- apply (auto simp add: zero_le_mult_iff mult_less_0_iff
- nat_mult_distrib [symmetric] nat_eq_iff2)
- done
+ unfolding zdvd_int by (cases "z \<ge> 0") (simp_all add: zdvd_zminus2_iff)
lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)"
- apply (auto simp add: dvd_def int_mult)
- apply (rule_tac x = "nat k" in exI)
- apply (cut_tac k = m in int_less_0_conv)
- apply (auto simp add: zero_le_mult_iff mult_less_0_iff
- nat_mult_distrib [symmetric] nat_eq_iff2)
- done
+ by (auto simp add: dvd_int_iff)
lemma zminus_dvd_iff [iff]: "(-z dvd w) = (z dvd (w::int))"
- apply (auto simp add: dvd_def)
- apply (rule_tac [!] x = "-k" in exI, auto)
- done
+ by (simp add: zdvd_zminus2_iff)
lemma dvd_zminus_iff [iff]: "(z dvd -w) = (z dvd (w::int))"
- apply (auto simp add: dvd_def)
- apply (drule minus_equation_iff [THEN iffD1])
- apply (rule_tac [!] x = "-k" in exI, auto)
- done
+ by (simp add: zdvd_zminus_iff)
lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)"
apply (rule_tac z=n in int_cases)
--- a/src/HOL/Library/Char_nat.thy Fri Jul 18 17:09:48 2008 +0200
+++ b/src/HOL/Library/Char_nat.thy Fri Jul 18 18:25:53 2008 +0200
@@ -156,7 +156,7 @@
have l_div_256: "l div 16 * 16 mod 256 = l div 16 * 16"
using l by auto
have aux2: "(k * 256 mod 16 + l mod 16) div 16 = 0"
- unfolding 256 mult_assoc [symmetric] mod_mult_self_is_0 by simp
+ unfolding 256 mult_assoc [symmetric] mod_mult_self2_is_0 by simp
have aux3: "(k * 256 + l) div 16 = k * 16 + l div 16"
unfolding div_add1_eq [of "k * 256" l 16] aux2 256
mult_assoc [symmetric] div_mult_self_is_m [OF 16] by simp
--- a/src/HOL/Library/GCD.thy Fri Jul 18 17:09:48 2008 +0200
+++ b/src/HOL/Library/GCD.thy Fri Jul 18 18:25:53 2008 +0200
@@ -148,8 +148,7 @@
done
lemma relprime_dvd_mult_iff: "gcd k n = 1 ==> (k dvd m * n) = (k dvd m)"
- apply (blast intro: relprime_dvd_mult dvd_trans)
- done
+ by (auto intro: relprime_dvd_mult dvd_mult2)
lemma gcd_mult_cancel: "gcd k n = 1 ==> gcd (k * m) n = gcd m n"
apply (rule dvd_anti_sym)
@@ -158,7 +157,7 @@
apply (simp add: gcd_assoc)
apply (simp add: gcd_commute)
apply (simp_all add: mult_commute)
- apply (blast intro: dvd_trans)
+ apply (blast intro: dvd_mult)
done
@@ -167,6 +166,7 @@
lemma gcd_add1 [simp]: "gcd (m + n) n = gcd m n"
apply (case_tac "n = 0")
apply (simp_all add: gcd_non_0)
+ apply (simp add: mod_add_self2)
done
lemma gcd_add2 [simp]: "gcd m (m + n) = gcd m n"
@@ -549,4 +549,8 @@
thus ?thesis by (simp add: zlcm_def)
qed
+lemma zgcd_code [code func]:
+ "zgcd k l = \<bar>if l = 0 then k else zgcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>"
+ by (simp add: zgcd_def gcd.simps [of "nat \<bar>k\<bar>"] nat_mod_distrib)
+
end
--- a/src/HOL/Library/Parity.thy Fri Jul 18 17:09:48 2008 +0200
+++ b/src/HOL/Library/Parity.thy Fri Jul 18 18:25:53 2008 +0200
@@ -382,13 +382,14 @@
done
lemma lemma_odd_mod_4_div_2: "n mod 4 = (3::nat) ==> odd((n - 1) div 2)"
-apply (rule_tac t = n and n1 = 4 in mod_div_equality [THEN subst])
+apply (rule mod_div_equality [of n 4, THEN subst])
apply (simp add: even_num_iff)
done
lemma lemma_even_mod_4_div_2: "n mod 4 = (1::nat) ==> even ((n - 1) div 2)"
-by (rule_tac t = n and n1 = 4 in mod_div_equality [THEN subst], simp)
-
+apply (rule mod_div_equality [of n 4, THEN subst])
+apply simp
+done
text {* Simplify, when the exponent is a numeral *}
--- a/src/HOL/Library/Primes.thy Fri Jul 18 17:09:48 2008 +0200
+++ b/src/HOL/Library/Primes.thy Fri Jul 18 18:25:53 2008 +0200
@@ -789,21 +789,23 @@
from coprime_prime_dvd_ex[OF c] obtain p
where p: "prime p" "p dvd x*y" "p dvd x^2 + y^2" by blast
{assume px: "p dvd x"
- from dvd_mult[OF px, of x] p(3) have "p dvd y^2"
- unfolding dvd_def
- apply (auto simp add: power2_eq_square)
- apply (rule_tac x= "ka - k" in exI)
- by (simp add: diff_mult_distrib2)
+ from dvd_mult[OF px, of x] p(3)
+ obtain r s where "x * x = p * r" and "x^2 + y^2 = p * s"
+ by (auto elim!: dvdE)
+ then have "y^2 = p * (s - r)"
+ by (auto simp add: power2_eq_square diff_mult_distrib2)
+ then have "p dvd y^2" ..
with prime_divexp[OF p(1), of y 2] have py: "p dvd y" .
from p(1) px py xy[unfolded coprime, rule_format, of p] prime_1
have False by simp }
moreover
{assume py: "p dvd y"
- from dvd_mult[OF py, of y] p(3) have "p dvd x^2"
- unfolding dvd_def
- apply (auto simp add: power2_eq_square)
- apply (rule_tac x= "ka - k" in exI)
- by (simp add: diff_mult_distrib2)
+ from dvd_mult[OF py, of y] p(3)
+ obtain r s where "y * y = p * r" and "x^2 + y^2 = p * s"
+ by (auto elim!: dvdE)
+ then have "x^2 = p * (s - r)"
+ by (auto simp add: power2_eq_square diff_mult_distrib2)
+ then have "p dvd x^2" ..
with prime_divexp[OF p(1), of x 2] have px: "p dvd x" .
from p(1) px py xy[unfolded coprime, rule_format, of p] prime_1
have False by simp }
@@ -953,7 +955,18 @@
text {* More useful lemmas. *}
lemma prime_product:
- "prime (p*q) \<Longrightarrow> p = 1 \<or> q = 1" unfolding prime_def by auto
+ assumes "prime (p * q)"
+ shows "p = 1 \<or> q = 1"
+proof -
+ from assms have
+ "1 < p * q" and P: "\<And>m. m dvd p * q \<Longrightarrow> m = 1 \<or> m = p * q"
+ unfolding prime_def by auto
+ from `1 < p * q` have "p \<noteq> 0" by (cases p) auto
+ then have Q: "p = p * q \<longleftrightarrow> q = 1" by auto
+ have "p dvd p * q" by simp
+ then have "p = 1 \<or> p = p * q" by (rule P)
+ then show ?thesis by (simp add: Q)
+qed
lemma prime_exp: "prime (p^n) \<longleftrightarrow> prime p \<and> n = 1"
proof(induct n)
--- a/src/HOL/NSA/StarDef.thy Fri Jul 18 17:09:48 2008 +0200
+++ b/src/HOL/NSA/StarDef.thy Fri Jul 18 18:25:53 2008 +0200
@@ -531,6 +531,8 @@
end
+instance star :: (Ring_and_Field.dvd) Ring_and_Field.dvd ..
+
instantiation star :: (Divides.div) Divides.div
begin
--- a/src/HOL/NatBin.thy Fri Jul 18 17:09:48 2008 +0200
+++ b/src/HOL/NatBin.thy Fri Jul 18 18:25:53 2008 +0200
@@ -67,8 +67,8 @@
lemma nat_div_distrib: "(0::int) <= z ==> nat (z div z') = nat z div nat z'"
apply (case_tac "0 <= z'")
-apply (auto simp add: div_nonneg_neg_le0 DIVISION_BY_ZERO_DIV)
-apply (case_tac "z' = 0", simp add: DIVISION_BY_ZERO)
+apply (auto simp add: div_nonneg_neg_le0)
+apply (case_tac "z' = 0", simp)
apply (auto elim!: nonneg_eq_int)
apply (rename_tac m m')
apply (subgoal_tac "0 <= int m div int m'")
@@ -145,9 +145,7 @@
(if neg (number_of v :: int) then number_of v'
else if neg (number_of v' :: int) then number_of v
else number_of (v + v'))"
-by (force dest!: neg_nat
- simp del: nat_number_of
- simp add: nat_number_of_def nat_add_distrib [symmetric])
+by (simp add: neg_nat nat_number_of_def nat_add_distrib [symmetric] del: nat_number_of)
subsubsection{*Subtraction *}
@@ -157,8 +155,8 @@
(if neg z' then nat z
else let d = z-z' in
if neg d then 0 else nat d)"
-apply (simp add: Let_def nat_diff_distrib [symmetric] neg_eq_less_0 not_neg_eq_ge_0)
-done
+by (simp add: Let_def nat_diff_distrib [symmetric] neg_eq_less_0 not_neg_eq_ge_0)
+
lemma diff_nat_number_of [simp]:
"(number_of v :: nat) - number_of v' =
@@ -174,10 +172,7 @@
lemma mult_nat_number_of [simp]:
"(number_of v :: nat) * number_of v' =
(if neg (number_of v :: int) then 0 else number_of (v * v'))"
-by (force dest!: neg_nat
- simp del: nat_number_of
- simp add: nat_number_of_def nat_mult_distrib [symmetric])
-
+by (simp add: neg_nat nat_number_of_def nat_mult_distrib [symmetric] del: nat_number_of)
subsubsection{*Quotient *}
@@ -186,12 +181,10 @@
"(number_of v :: nat) div number_of v' =
(if neg (number_of v :: int) then 0
else nat (number_of v div number_of v'))"
-by (force dest!: neg_nat
- simp del: nat_number_of
- simp add: nat_number_of_def nat_div_distrib [symmetric])
+by (simp add: neg_nat nat_number_of_def nat_div_distrib [symmetric] del: nat_number_of)
lemma one_div_nat_number_of [simp]:
- "(Suc 0) div number_of v' = (nat (1 div number_of v'))"
+ "Suc 0 div number_of v' = nat (1 div number_of v')"
by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric])
@@ -202,12 +195,10 @@
(if neg (number_of v :: int) then 0
else if neg (number_of v' :: int) then number_of v
else nat (number_of v mod number_of v'))"
-by (force dest!: neg_nat
- simp del: nat_number_of
- simp add: nat_number_of_def nat_mod_distrib [symmetric])
+by (simp add: neg_nat nat_number_of_def nat_mod_distrib [symmetric] del: nat_number_of)
lemma one_mod_nat_number_of [simp]:
- "(Suc 0) mod number_of v' =
+ "Suc 0 mod number_of v' =
(if neg (number_of v' :: int) then Suc 0
else nat (1 mod number_of v'))"
by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric])
--- a/src/HOL/NumberTheory/EvenOdd.thy Fri Jul 18 17:09:48 2008 +0200
+++ b/src/HOL/NumberTheory/EvenOdd.thy Fri Jul 18 18:25:53 2008 +0200
@@ -5,7 +5,9 @@
header {*Parity: Even and Odd Integers*}
-theory EvenOdd imports Int2 begin
+theory EvenOdd
+imports Int2
+begin
definition
zOdd :: "int set" where
@@ -224,7 +226,7 @@
qed
lemma even_sum_div_2: "[| x \<in> zEven; y \<in> zEven |] ==> (x + y) div 2 = x div 2 + y div 2"
- by (auto simp add: zEven_def, auto simp add: zdiv_zadd1_eq)
+ by (auto simp add: zEven_def)
lemma even_prod_div_2: "[| x \<in> zEven |] ==> (x * y) div 2 = (x div 2) * y"
by (auto simp add: zEven_def)
--- a/src/HOL/NumberTheory/IntPrimes.thy Fri Jul 18 17:09:48 2008 +0200
+++ b/src/HOL/NumberTheory/IntPrimes.thy Fri Jul 18 18:25:53 2008 +0200
@@ -127,9 +127,7 @@
by (unfold zcong_def, auto)
lemma zcong_sym: "[a = b] (mod m) = [b = a] (mod m)"
- apply (unfold zcong_def dvd_def, auto)
- apply (rule_tac [!] x = "-k" in exI, auto)
- done
+ unfolding zcong_def minus_diff_eq [of a, symmetric] zdvd_zminus_iff ..
lemma zcong_zadd:
"[a = b] (mod m) ==> [c = d] (mod m) ==> [a + c = b + d] (mod m)"
@@ -147,9 +145,10 @@
lemma zcong_trans:
"[a = b] (mod m) ==> [b = c] (mod m) ==> [a = c] (mod m)"
- apply (unfold zcong_def dvd_def, auto)
- apply (rule_tac x = "k + ka" in exI)
- apply (simp add: zadd_ac zadd_zmult_distrib2)
+ unfolding zcong_def
+ apply (auto elim!: dvdE simp add: ring_simps)
+ unfolding left_distrib [symmetric]
+ apply (rule dvd_mult dvd_refl)+
done
lemma zcong_zmult:
@@ -207,7 +206,7 @@
lemma zcong_zgcd_zmult_zmod:
"[a = b] (mod m) ==> [a = b] (mod n) ==> zgcd m n = 1
==> [a = b] (mod m * n)"
- apply (unfold zcong_def dvd_def, auto)
+ apply (auto simp add: zcong_def dvd_def)
apply (subgoal_tac "m dvd n * ka")
apply (subgoal_tac "m dvd ka")
apply (case_tac [2] "0 \<le> ka")
@@ -255,8 +254,9 @@
done
lemma zcong_iff_lin: "([a = b] (mod m)) = (\<exists>k. b = a + m * k)"
- apply (unfold zcong_def dvd_def, auto)
- apply (rule_tac [!] x = "-k" in exI, auto)
+ unfolding zcong_def
+ apply (auto elim!: dvdE simp add: ring_simps)
+ apply (rule_tac x = "-k" in exI) apply simp
done
lemma zgcd_zcong_zgcd:
@@ -306,13 +306,7 @@
lemma zmod_zdvd_zmod:
"0 < (m::int) ==> m dvd b ==> (a mod b mod m) = (a mod m)"
- apply (unfold dvd_def, auto)
- apply (subst zcong_zmod_eq [symmetric])
- prefer 2
- apply (subst zcong_iff_lin)
- apply (rule_tac x = "k * (a div (m * k))" in exI)
- apply (simp add:zmult_assoc [symmetric], assumption)
- done
+ by (rule zmod_zmod_cancel)
subsection {* Extended GCD *}
--- a/src/HOL/Presburger.thy Fri Jul 18 17:09:48 2008 +0200
+++ b/src/HOL/Presburger.thy Fri Jul 18 18:25:53 2008 +0200
@@ -31,8 +31,8 @@
"\<exists>(z ::'a::{linorder}).\<forall>x<z.(x \<le> t) = True"
"\<exists>(z ::'a::{linorder}).\<forall>x<z.(x > t) = False"
"\<exists>(z ::'a::{linorder}).\<forall>x<z.(x \<ge> t) = False"
- "\<exists>z.\<forall>(x::'a::{linorder,plus,Divides.dvd})<z. (d dvd x + s) = (d dvd x + s)"
- "\<exists>z.\<forall>(x::'a::{linorder,plus,Divides.dvd})<z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
+ "\<exists>z.\<forall>(x::'a::{linorder,plus,Ring_and_Field.dvd})<z. (d dvd x + s) = (d dvd x + s)"
+ "\<exists>z.\<forall>(x::'a::{linorder,plus,Ring_and_Field.dvd})<z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
"\<exists>z.\<forall>x<z. F = F"
by ((erule exE, erule exE,rule_tac x="min z za" in exI,simp)+, (rule_tac x="t" in exI,fastsimp)+) simp_all
@@ -47,8 +47,8 @@
"\<exists>(z ::'a::{linorder}).\<forall>x>z.(x \<le> t) = False"
"\<exists>(z ::'a::{linorder}).\<forall>x>z.(x > t) = True"
"\<exists>(z ::'a::{linorder}).\<forall>x>z.(x \<ge> t) = True"
- "\<exists>z.\<forall>(x::'a::{linorder,plus,Divides.dvd})>z. (d dvd x + s) = (d dvd x + s)"
- "\<exists>z.\<forall>(x::'a::{linorder,plus,Divides.dvd})>z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
+ "\<exists>z.\<forall>(x::'a::{linorder,plus,Ring_and_Field.dvd})>z. (d dvd x + s) = (d dvd x + s)"
+ "\<exists>z.\<forall>(x::'a::{linorder,plus,Ring_and_Field.dvd})>z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
"\<exists>z.\<forall>x>z. F = F"
by ((erule exE, erule exE,rule_tac x="max z za" in exI,simp)+,(rule_tac x="t" in exI,fastsimp)+) simp_all
@@ -57,12 +57,12 @@
\<Longrightarrow> \<forall>x k. (P x \<and> Q x) = (P (x - k*D) \<and> Q (x - k*D))"
"\<lbrakk>\<forall>x k. P x = P (x - k*D); \<forall>x k. Q x = Q (x - k*D)\<rbrakk>
\<Longrightarrow> \<forall>x k. (P x \<or> Q x) = (P (x - k*D) \<or> Q (x - k*D))"
- "(d::'a::{comm_ring,Divides.dvd}) dvd D \<Longrightarrow> \<forall>x k. (d dvd x + t) = (d dvd (x - k*D) + t)"
- "(d::'a::{comm_ring,Divides.dvd}) dvd D \<Longrightarrow> \<forall>x k. (\<not>d dvd x + t) = (\<not>d dvd (x - k*D) + t)"
+ "(d::'a::{comm_ring,Ring_and_Field.dvd}) dvd D \<Longrightarrow> \<forall>x k. (d dvd x + t) = (d dvd (x - k*D) + t)"
+ "(d::'a::{comm_ring,Ring_and_Field.dvd}) dvd D \<Longrightarrow> \<forall>x k. (\<not>d dvd x + t) = (\<not>d dvd (x - k*D) + t)"
"\<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_simps, clarsimp,rule_tac x = "kb + ka*k" in exI,simp add: ring_simps)+
+apply (auto elim!: dvdE simp add: ring_simps)
+unfolding mult_assoc [symmetric] left_distrib [symmetric] left_diff_distrib [symmetric]
+unfolding dvd_def mult_commute [of d] by auto
subsection{* The A and B sets *}
lemma bset:
@@ -114,11 +114,12 @@
next
assume d: "d dvd D"
{fix x assume H: "d dvd x + t" with d have "d dvd (x - D) + t"
- by (clarsimp simp add: dvd_def,rule_tac x= "ka - k" in exI,simp add: ring_simps)}
+ by (auto elim!: dvdE simp add: ring_simps)
+ (auto simp only: left_diff_distrib [symmetric] dvd_def mult_commute)}
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"
+ {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_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
@@ -360,16 +361,17 @@
apply(fastsimp)
done
-theorem unity_coeff_ex: "(\<exists>(x::'a::{semiring_0,Divides.dvd}). P (l * x)) \<equiv> (\<exists>x. l dvd (x + 0) \<and> P x)"
- apply (rule eq_reflection[symmetric])
+theorem unity_coeff_ex: "(\<exists>(x::'a::{semiring_0,Ring_and_Field.dvd}). P (l * x)) \<equiv> (\<exists>x. l dvd (x + 0) \<and> P x)"
+ apply (rule eq_reflection [symmetric])
apply (rule iffI)
defer
apply (erule exE)
apply (rule_tac x = "l * x" in exI)
apply (simp add: dvd_def)
- apply (rule_tac x="x" in exI, simp)
+ apply (rule_tac x = x in exI, simp)
apply (erule exE)
apply (erule conjE)
+ apply simp
apply (erule dvdE)
apply (rule_tac x = k in exI)
apply simp
@@ -417,13 +419,13 @@
lemma zmod_eq0_zdvd_iff[presburger]: "(m::int) mod n = 0 \<longleftrightarrow> n dvd m"
unfolding zdvd_iff_zmod_eq_0[symmetric] ..
-declare mod_1[presburger]
+declare mod_1[presburger]
declare mod_0[presburger]
declare zmod_1[presburger]
declare zmod_zero[presburger]
declare zmod_self[presburger]
declare mod_self[presburger]
-declare DIVISION_BY_ZERO_MOD[presburger]
+declare mod_by_0[presburger]
declare nat_mod_div_trivial[presburger]
declare div_mod_equality2[presburger]
declare div_mod_equality[presburger]
@@ -435,7 +437,7 @@
declare zdiv_zmod_equality[presburger]
declare mod2_Suc_Suc[presburger]
lemma [presburger]: "(a::int) div 0 = 0" and [presburger]: "a mod 0 = a"
-using IntDiv.DIVISION_BY_ZERO by blast+
+by simp_all
use "Tools/Qelim/cooper.ML"
oracle linzqe_oracle ("term") = Coopereif.cooper_oracle
--- a/src/HOL/Ring_and_Field.thy Fri Jul 18 17:09:48 2008 +0200
+++ b/src/HOL/Ring_and_Field.thy Fri Jul 18 18:25:53 2008 +0200
@@ -102,12 +102,108 @@
class semiring_1 = zero_neq_one + semiring_0 + monoid_mult
-class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult
+text {* Abstract divisibility *}
+
+class dvd = times
+begin
+
+definition
+ dvd :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "dvd" 50)
+where
+ [code func del]: "b dvd a \<longleftrightarrow> (\<exists>k. a = b * k)"
+
+lemma dvdI [intro?]: "a = b * k \<Longrightarrow> b dvd a"
+ unfolding dvd_def ..
+
+lemma dvdE [elim?]: "b dvd a \<Longrightarrow> (\<And>k. a = b * k \<Longrightarrow> P) \<Longrightarrow> P"
+ unfolding dvd_def by blast
+
+end
+
+class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult + dvd
(*previously almost_semiring*)
begin
subclass semiring_1 ..
+lemma dvd_refl: "a dvd a"
+proof -
+ have "a = a * 1" by simp
+ then show ?thesis unfolding dvd_def ..
+qed
+
+lemma dvd_trans:
+ assumes "a dvd b" and "b dvd c"
+ shows "a dvd c"
+proof -
+ from assms obtain v where "b = a * v" unfolding dvd_def by auto
+ moreover from assms obtain w where "c = b * w" unfolding dvd_def by auto
+ ultimately have "c = a * (v * w)" by (simp add: mult_assoc)
+ then show ?thesis unfolding dvd_def ..
+qed
+
+lemma dvd_0_left_iff [noatp, simp]: "0 dvd a \<longleftrightarrow> a = 0"
+ unfolding dvd_def by simp
+
+lemma dvd_0 [simp]: "a dvd 0"
+unfolding dvd_def proof
+ show "0 = a * 0" by simp
+qed
+
+lemma one_dvd [simp]: "1 dvd a"
+ unfolding dvd_def by simp
+
+lemma dvd_mult: "a dvd c \<Longrightarrow> a dvd (b * c)"
+ unfolding dvd_def by (blast intro: mult_left_commute)
+
+lemma dvd_mult2: "a dvd b \<Longrightarrow> a dvd (b * c)"
+ apply (subst mult_commute)
+ apply (erule dvd_mult)
+ done
+
+lemma dvd_triv_right [simp]: "a dvd b * a"
+ by (rule dvd_mult) (rule dvd_refl)
+
+lemma dvd_triv_left [simp]: "a dvd a * b"
+ by (rule dvd_mult2) (rule dvd_refl)
+
+lemma mult_dvd_mono:
+ assumes ab: "a dvd b"
+ and "cd": "c dvd d"
+ shows "a * c dvd b * d"
+proof -
+ from ab obtain b' where "b = a * b'" ..
+ moreover from "cd" obtain d' where "d = c * d'" ..
+ ultimately have "b * d = (a * c) * (b' * d')" by (simp add: mult_ac)
+ then show ?thesis ..
+qed
+
+lemma dvd_mult_left: "a * b dvd c \<Longrightarrow> a dvd c"
+ by (simp add: dvd_def mult_assoc, blast)
+
+lemma dvd_mult_right: "a * b dvd c \<Longrightarrow> b dvd c"
+ unfolding mult_ac [of a] by (rule dvd_mult_left)
+
+lemma dvd_0_right [iff]: "a dvd 0"
+proof -
+ have "0 = a * 0" by simp
+ then show ?thesis unfolding dvd_def ..
+qed
+
+lemma dvd_0_left: "0 dvd a \<Longrightarrow> a = 0"
+ by simp
+
+lemma dvd_add:
+ assumes ab: "a dvd b"
+ and ac: "a dvd c"
+ shows "a dvd (b + c)"
+proof -
+ from ab obtain b' where "b = a * b'" ..
+ moreover from ac obtain c' where "c = a * c'" ..
+ ultimately have "b + c = a * (b' + c')" by (simp add: right_distrib)
+ then show ?thesis ..
+qed
+
end
class no_zero_divisors = zero + times +
@@ -973,6 +1069,26 @@
"c * a < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"
by (insert mult_less_cancel_left [of c a 1], simp)
+lemma sgn_sgn [simp]:
+ "sgn (sgn a) = sgn a"
+ unfolding sgn_if by simp
+
+lemma sgn_0_0:
+ "sgn a = 0 \<longleftrightarrow> a = 0"
+ unfolding sgn_if by simp
+
+lemma sgn_1_pos:
+ "sgn a = 1 \<longleftrightarrow> a > 0"
+ unfolding sgn_if by (simp add: neg_equal_zero)
+
+lemma sgn_1_neg:
+ "sgn a = - 1 \<longleftrightarrow> a < 0"
+ unfolding sgn_if by (auto simp add: equal_neg_zero)
+
+lemma sgn_times:
+ "sgn (a * b) = sgn a * sgn b"
+ by (auto simp add: sgn_if zero_less_mult_iff)
+
end
class ordered_field = field + ordered_idom
--- a/src/HOL/Tools/Qelim/cooper.ML Fri Jul 18 17:09:48 2008 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Fri Jul 18 18:25:53 2008 +0200
@@ -80,9 +80,9 @@
| Const (@{const_name HOL.less_eq}, _) $ y $ z =>
if term_of x aconv y then Le (Thm.dest_arg ct)
else if term_of x aconv z then Ge (Thm.dest_arg1 ct) else Nox
-| Const (@{const_name Divides.dvd},_)$_$(Const(@{const_name "HOL.plus"},_)$y$_) =>
+| Const (@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name HOL.plus},_)$y$_) =>
if term_of x aconv y then Dvd (Thm.dest_binop ct ||> Thm.dest_arg) else Nox
-| Const (@{const_name Not},_) $ (Const (@{const_name Divides.dvd},_)$_$(Const(@{const_name "HOL.plus"},_)$y$_)) =>
+| Const (@{const_name Not},_) $ (Const (@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name "HOL.plus"},_)$y$_)) =>
if term_of x aconv y then
NDvd (Thm.dest_binop (Thm.dest_arg ct) ||> Thm.dest_arg) else Nox
| _ => Nox)
@@ -223,8 +223,8 @@
| lin (vs as x::_) (Const (@{const_name Not},_) $ (Const(@{const_name HOL.less_eq}, T) $ s $ t)) =
lin vs (Const (@{const_name HOL.less}, T) $ t $ s)
| lin vs (Const (@{const_name Not},T)$t) = Const (@{const_name Not},T)$ (lin vs t)
- | lin (vs as x::_) (Const(@{const_name Divides.dvd},_)$d$t) =
- HOLogic.mk_binrel @{const_name Divides.dvd} (numeral1 abs d, lint vs t)
+ | lin (vs as x::_) (Const(@{const_name Ring_and_Field.dvd},_)$d$t) =
+ HOLogic.mk_binrel @{const_name Ring_and_Field.dvd} (numeral1 abs d, lint vs t)
| lin (vs as x::_) ((b as Const("op =",_))$s$t) =
(case lint vs (subC$t$s) of
(t as a$(m$c$y)$r) =>
@@ -252,7 +252,7 @@
| is_intrel _ = false;
fun linearize_conv ctxt vs ct = case term_of ct of
- Const(@{const_name Divides.dvd},_)$d$t =>
+ Const(@{const_name Ring_and_Field.dvd},_)$d$t =>
let
val th = binop_conv (lint_conv ctxt vs) ct
val (d',t') = Thm.dest_binop (Thm.rhs_of th)
@@ -277,7 +277,7 @@
| _ => dth
end
end
-| Const (@{const_name Not},_)$(Const(@{const_name Divides.dvd},_)$_$_) => arg_conv (linearize_conv ctxt vs) ct
+| Const (@{const_name Not},_)$(Const(@{const_name Ring_and_Field.dvd},_)$_$_) => arg_conv (linearize_conv ctxt vs) ct
| t => if is_intrel t
then (provelin ctxt ((HOLogic.eq_const bT)$t$(lin vs t) |> HOLogic.mk_Trueprop))
RS eq_reflection
@@ -300,7 +300,7 @@
if x aconv y andalso member (op =)
[@{const_name HOL.less}, @{const_name HOL.less_eq}] s
then (ins (dest_numeral c) acc, dacc) else (acc,dacc)
- | Const(@{const_name Divides.dvd},_)$_$(Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$c$y)$_) =>
+ | Const(@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$c$y)$_) =>
if x aconv y then (acc,ins (dest_numeral c) dacc) else (acc,dacc)
| Const("op &",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
| Const("op |",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
@@ -340,7 +340,7 @@
if x=y andalso member (op =)
[@{const_name HOL.less}, @{const_name HOL.less_eq}] s
then cv (l div dest_numeral c) t else Thm.reflexive t
- | Const(@{const_name Divides.dvd},_)$d$(r as (Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$c$y)$_)) =>
+ | Const(@{const_name Ring_and_Field.dvd},_)$d$(r as (Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$c$y)$_)) =>
if x=y then
let
val k = l div dest_numeral c
@@ -556,7 +556,7 @@
| Const("False",_) => F
| Const(@{const_name HOL.less},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2))
| Const(@{const_name HOL.less_eq},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2))
- | Const(@{const_name Divides.dvd},_)$t1$t2 =>
+ | Const(@{const_name Ring_and_Field.dvd},_)$t1$t2 =>
(Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => cooper "Reification: unsupported dvd")
| @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2))
| @{term "op = :: bool => _ "}$t1$t2 => Iffa(qf_of_term ps vs t1,qf_of_term ps vs t2)
--- a/src/HOL/Tools/Qelim/presburger.ML Fri Jul 18 17:09:48 2008 +0200
+++ b/src/HOL/Tools/Qelim/presburger.ML Fri Jul 18 18:25:53 2008 +0200
@@ -127,8 +127,8 @@
@{thm "mod_add_left_eq"}, @{thm "mod_add_right_eq"},
@{thm "zmod_zadd1_eq"}, @{thm "zmod_zadd_left_eq"},
@{thm "zmod_zadd_right_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}]
- @ [@{thm "mod_self"}, @{thm "zmod_self"}, @{thm "DIVISION_BY_ZERO_MOD"},
- @{thm "DIVISION_BY_ZERO_DIV"}, @{thm "DIVISION_BY_ZERO"} RS conjunct1,
+ @ [@{thm "mod_self"}, @{thm "zmod_self"}, @{thm "mod_by_0"},
+ @{thm "div_by_0"}, @{thm "DIVISION_BY_ZERO"} RS conjunct1,
@{thm "DIVISION_BY_ZERO"} RS conjunct2, @{thm "zdiv_zero"}, @{thm "zmod_zero"},
@{thm "div_0"}, @{thm "mod_0"}, @{thm "zdiv_1"}, @{thm "zmod_1"}, @{thm "div_1"},
@{thm "mod_1"}, @{thm "Suc_plus1"}]
--- a/src/HOL/Word/BinBoolList.thy Fri Jul 18 17:09:48 2008 +0200
+++ b/src/HOL/Word/BinBoolList.thy Fri Jul 18 18:25:53 2008 +0200
@@ -1099,11 +1099,10 @@
apply (subst bin_rsplit_aux.simps)
apply (clarsimp simp: Let_def split: ls_splits)
apply (erule thin_rl)
+ apply (case_tac m)
+ apply simp
apply (case_tac "m <= n")
- prefer 2
- apply (simp add: div_add_self2 [symmetric])
- apply (case_tac m, clarsimp)
- apply (simp add: div_add_self2)
+ apply (auto simp add: div_add_self2)
done
lemma bin_rsplit_len:
--- a/src/HOL/Word/Num_Lemmas.thy Fri Jul 18 17:09:48 2008 +0200
+++ b/src/HOL/Word/Num_Lemmas.thy Fri Jul 18 18:25:53 2008 +0200
@@ -256,7 +256,6 @@
prefer 2
apply (erule asm_rl)
apply (simp add: zmde ring_distribs)
- apply (simp add: push_mods)
done
(** Rep_Integ **)
--- a/src/HOL/ex/coopertac.ML Fri Jul 18 17:09:48 2008 +0200
+++ b/src/HOL/ex/coopertac.ML Fri Jul 18 18:25:53 2008 +0200
@@ -10,33 +10,28 @@
val binarith = @{thms normalize_bin_simps};
val comp_arith = binarith @ simp_thms
-val zdvd_int = thm "zdvd_int";
-val zdiff_int_split = thm "zdiff_int_split";
-val all_nat = thm "all_nat";
-val ex_nat = thm "ex_nat";
-val number_of1 = thm "number_of1";
-val number_of2 = thm "number_of2";
-val split_zdiv = thm "split_zdiv";
-val split_zmod = thm "split_zmod";
-val mod_div_equality' = thm "mod_div_equality'";
-val split_div' = thm "split_div'";
-val Suc_plus1 = thm "Suc_plus1";
-val imp_le_cong = thm "imp_le_cong";
-val conj_le_cong = thm "conj_le_cong";
+val zdvd_int = @{thm zdvd_int};
+val zdiff_int_split = @{thm zdiff_int_split};
+val all_nat = @{thm all_nat};
+val ex_nat = @{thm ex_nat};
+val number_of1 = @{thm number_of1};
+val number_of2 = @{thm number_of2};
+val split_zdiv = @{thm split_zdiv};
+val split_zmod = @{thm split_zmod};
+val mod_div_equality' = @{thm mod_div_equality'};
+val split_div' = @{thm split_div'};
+val Suc_plus1 = @{thm Suc_plus1};
+val imp_le_cong = @{thm imp_le_cong};
+val conj_le_cong = @{thm conj_le_cong};
val nat_mod_add_eq = @{thm mod_add1_eq} RS sym;
val nat_mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
val nat_mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
-val int_mod_add_eq = @{thm "zmod_zadd1_eq"} RS sym;
-val int_mod_add_left_eq = @{thm "zmod_zadd_left_eq"} RS sym;
-val int_mod_add_right_eq = @{thm "zmod_zadd_right_eq"} RS sym;
-val nat_div_add_eq = @{thm "div_add1_eq"} RS sym;
-val int_div_add_eq = @{thm "zdiv_zadd1_eq"} RS sym;
-val ZDIVISION_BY_ZERO_MOD = @{thm "DIVISION_BY_ZERO"} RS conjunct2;
-val ZDIVISION_BY_ZERO_DIV = @{thm "DIVISION_BY_ZERO"} RS conjunct1;
+val int_mod_add_eq = @{thm zmod_zadd1_eq} RS sym;
+val int_mod_add_left_eq = @{thm zmod_zadd_left_eq} RS sym;
+val int_mod_add_right_eq = @{thm zmod_zadd_right_eq} RS sym;
+val nat_div_add_eq = @{thm div_add1_eq} RS sym;
+val int_div_add_eq = @{thm zdiv_zadd1_eq} RS sym;
-(*
-val fn_rews = List.concat (map thms ["allpairs.simps","iupt.simps","decr.simps", "decrnum.simps","disjuncts.simps","simpnum.simps", "simpfm.simps","numadd.simps","nummul.simps","numneg_def","numsub","simp_num_pair_def","not.simps","prep.simps","qelim.simps","minusinf.simps","plusinf.simps","rsplit0.simps","rlfm.simps","\<Upsilon>.simps","\<upsilon>.simps","linrqe_def", "ferrack_def", "Let_def", "numsub_def", "numneg_def","DJ_def", "imp_def", "evaldjf_def", "djf_def", "split_def", "eq_def", "disj_def", "simp_num_pair_def", "conj_def", "lt_def", "neq_def","gt_def"]);
-*)
fun prepare_for_linz q fm =
let
val ps = Logic.strip_params fm
@@ -47,8 +42,7 @@
(HOLogic.all_const T $ Abs (s, T, P), n)
else (incr_boundvars ~1 P, n-1)
fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t;
- val rhs = hs
-(* val (rhs,irhs) = List.partition (relevant (rev ps)) hs *)
+ val rhs = hs
val np = length ps
val (fm',np) = foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
(foldr HOLogic.mk_imp c rhs, np) ps
@@ -77,8 +71,7 @@
int_mod_add_right_eq, int_mod_add_left_eq,
nat_div_add_eq, int_div_add_eq,
@{thm mod_self}, @{thm "zmod_self"},
- @{thm DIVISION_BY_ZERO_MOD}, @{thm DIVISION_BY_ZERO_DIV},
- ZDIVISION_BY_ZERO_MOD,ZDIVISION_BY_ZERO_DIV,
+ @{thm mod_by_0}, @{thm div_by_0},
@{thm "zdiv_zero"}, @{thm "zmod_zero"}, @{thm "div_0"}, @{thm "mod_0"},
@{thm "zdiv_1"}, @{thm "zmod_1"}, @{thm "div_1"}, @{thm "mod_1"},
Suc_plus1]
--- a/src/HOL/int_factor_simprocs.ML Fri Jul 18 17:09:48 2008 +0200
+++ b/src/HOL/int_factor_simprocs.ML Fri Jul 18 18:25:53 2008 +0200
@@ -262,8 +262,8 @@
structure IntDvdCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binrel @{const_name Divides.dvd}
- val dest_bal = HOLogic.dest_bin @{const_name Divides.dvd} HOLogic.intT
+ val mk_bal = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd}
+ val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} HOLogic.intT
val simplify_meta_eq = cancel_simplify_meta_eq @{thm zdvd_zmult_cancel_disj}
);
--- a/src/HOL/nat_simprocs.ML Fri Jul 18 17:09:48 2008 +0200
+++ b/src/HOL/nat_simprocs.ML Fri Jul 18 18:25:53 2008 +0200
@@ -294,8 +294,8 @@
structure DvdCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binrel @{const_name Divides.dvd}
- val dest_bal = HOLogic.dest_bin @{const_name Divides.dvd} HOLogic.natT
+ val mk_bal = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd}
+ val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} HOLogic.natT
val cancel = @{thm nat_mult_dvd_cancel1} RS trans
val neg_exchanges = false
)
@@ -414,8 +414,8 @@
structure DvdCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binrel @{const_name Divides.dvd}
- val dest_bal = HOLogic.dest_bin @{const_name Divides.dvd} HOLogic.natT
+ val mk_bal = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd}
+ val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} HOLogic.natT
val simplify_meta_eq = cancel_simplify_meta_eq @{thm nat_mult_dvd_cancel_disj}
);