# HG changeset patch # User haftmann # Date 1216398353 -7200 # Node ID 16a26996c30e2bfa55b8f169f8b906036b27001e # Parent 7a4baad0549507b71e28c010b95b65abeea8c154 moved op dvd to theory Ring_and_Field; generalized a couple of lemmas diff -r 7a4baad05495 -r 16a26996c30e NEWS --- 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. diff -r 7a4baad05495 -r 16a26996c30e src/HOL/Algebra/Exponent.thy --- 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 diff -r 7a4baad05495 -r 16a26996c30e src/HOL/Algebra/abstract/Ring2.thy --- 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" diff -r 7a4baad05495 -r 16a26996c30e src/HOL/Algebra/poly/UnivPoly2.thy --- 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 diff -r 7a4baad05495 -r 16a26996c30e src/HOL/Complex/ex/Sqrt_Script.thy --- 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) \ prime p \ 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 \ diff -r 7a4baad05495 -r 16a26996c30e src/HOL/Divides.thy --- 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 \ 'a \ bool" (infixl "dvd" 50) -where - [code func del]: "m dvd n \ (\k. n = m * k)" - -end - -class div = times + +class div = dvd + fixes div :: "'a \ 'a \ 'a" (infixl "div" 70) - fixes mod :: "'a \ 'a \ 'a" (infixl "mod" 70) + and mod :: "'a \ 'a \ '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 \ 0 \ 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 \ 0 \ (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 \ 0 \ 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 \ 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 \ 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 + "\ = (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 \ 0 \ b * a div b = a" + using div_mult_self2 [of b 0 a] by simp + +lemma div_mult_self2_is_id [simp]: "b \ 0 \ 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 \ (\c. a = b * c \ P) \ 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 \ 0 \ a div a = 1" + using div_mult_self2_is_id [of _ 1] by simp + +lemma div_add_self1: + assumes "b \ 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 \ b mod a = 0" +lemma div_add_self2: + assumes "b \ 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 \ 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 \ 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 \ a dvd (b * c)" - unfolding dvd_def by (blast intro: mult_left_commute) - -lemma dvd_mult2: "a dvd b \ 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 \ b dvd d \ 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 \ a dvd c" - by (simp add: dvd_def mult_assoc, blast) - -lemma dvd_mult_right: "a * b dvd c \ b dvd c" - unfolding mult_ac [of a] by (rule dvd_mult_left) - 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 \ 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 \ 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\nat" n, standard] -lemmas mod_div_equality2 = mod_div_equality2 [of "n\nat" m, standard] -lemmas div_mod_equality = div_mod_equality [of "m\nat" n k, standard] -lemmas div_mod_equality2 = div_mod_equality2 [of "m\nat" n k, standard] +(*lemmas mod_div_equality_nat = semiring_div_class.times_div_mod_plus_zero_one.mod_div_equality [of "m\nat" n, standard] +lemmas mod_div_equality2_nat = mod_div_equality2 [of "n\nat" m, standard*) ML {* structure CancelDivModData = @@ -414,9 +396,6 @@ subsubsection {* Quotient *} -lemmas DIVISION_BY_ZERO_DIV [simp] = div_by_0 [of "a\nat", standard] -lemmas div_0 [simp] = semiring_div_class.div_0 [of "n\nat", standard] - lemma div_geq: "0 < n \ \ m < n \ 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 (m*n) div n = (m::nat)" - by (rule mult_div) simp + by simp lemma div_mult_self1_is_m [simp]: "0 (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\nat", standard] -lemmas mod_0 [simp] = semiring_div_class.mod_0 [of "n\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\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\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 \ m mod n \ (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\nat", standard] - -lemma div_add_self2: "0 (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+m) div n = Suc (m div n)" - by (simp add: add_commute div_add_self2) - -lemma div_mult_self1 [simp]: "!!n::nat. 0 (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 (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\nat", standard] -lemmas dvd_trans [trans] = semiring_div_class.dvd_trans [of "m\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" "\n m \ nat. n dvd m \ n \ 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\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 \ (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\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 \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 \ 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 \ 0" with Q have R: ?R by simp @@ -958,7 +821,7 @@ (\q. (n * q \ m \ m < n * (Suc q)) \ 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 \ 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 \ 0" with Q have R: ?R by simp diff -r 7a4baad05495 -r 16a26996c30e src/HOL/HoareParallel/RG_Examples.thy --- 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)\ 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) \ 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\ 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 diff -r 7a4baad05495 -r 16a26996c30e src/HOL/Import/HOL/divides.imp --- 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 diff -r 7a4baad05495 -r 16a26996c30e src/HOL/IntDiv.thy --- 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 \ (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 \ 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 \ (0::int) ==> (a+b) div a = b div a + 1" +by (simp add: zdiv_zadd1_eq) + +lemma zdiv_zadd_self2[simp]: "a \ (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 \ 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 \ (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 \ 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 \ (0::int) ==> (a+b) div a = b div a + 1" -by (simp add: zdiv_zadd1_eq) - -lemma zdiv_zadd_self2[simp]: "a \ (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 \ 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 \ 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: "( \i::int\ 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 \j\) = (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 ==> \ 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 \ 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 "\k. int y = int x * k \ 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 "\ = - (int x * int (Suc n))" by (simp only: mult_minus_right) + also have "\ = - 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 = ( \x\ = 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 \ 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 \ 0") (simp_all add: zdvd_zminus2_iff) lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \ 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 \ (n::int)" apply (rule_tac z=n in int_cases) diff -r 7a4baad05495 -r 16a26996c30e src/HOL/Library/Char_nat.thy --- 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 diff -r 7a4baad05495 -r 16a26996c30e src/HOL/Library/GCD.thy --- 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 = \if l = 0 then k else zgcd l (\k\ mod \l\)\" + by (simp add: zgcd_def gcd.simps [of "nat \k\"] nat_mod_distrib) + end diff -r 7a4baad05495 -r 16a26996c30e src/HOL/Library/Parity.thy --- 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 *} diff -r 7a4baad05495 -r 16a26996c30e src/HOL/Library/Primes.thy --- 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) \ p = 1 \ q = 1" unfolding prime_def by auto + assumes "prime (p * q)" + shows "p = 1 \ q = 1" +proof - + from assms have + "1 < p * q" and P: "\m. m dvd p * q \ m = 1 \ m = p * q" + unfolding prime_def by auto + from `1 < p * q` have "p \ 0" by (cases p) auto + then have Q: "p = p * q \ q = 1" by auto + have "p dvd p * q" by simp + then have "p = 1 \ p = p * q" by (rule P) + then show ?thesis by (simp add: Q) +qed lemma prime_exp: "prime (p^n) \ prime p \ n = 1" proof(induct n) diff -r 7a4baad05495 -r 16a26996c30e src/HOL/NSA/StarDef.thy --- 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 diff -r 7a4baad05495 -r 16a26996c30e src/HOL/NatBin.thy --- 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]) diff -r 7a4baad05495 -r 16a26996c30e src/HOL/NumberTheory/EvenOdd.thy --- 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 \ zEven; y \ 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 \ zEven |] ==> (x * y) div 2 = (x div 2) * y" by (auto simp add: zEven_def) diff -r 7a4baad05495 -r 16a26996c30e src/HOL/NumberTheory/IntPrimes.thy --- 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 \ ka") @@ -255,8 +254,9 @@ done lemma zcong_iff_lin: "([a = b] (mod m)) = (\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 *} diff -r 7a4baad05495 -r 16a26996c30e src/HOL/Presburger.thy --- 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 @@ "\(z ::'a::{linorder}).\x t) = True" "\(z ::'a::{linorder}).\x t) = False" "\(z ::'a::{linorder}).\x t) = False" - "\z.\(x::'a::{linorder,plus,Divides.dvd})z.\(x::'a::{linorder,plus,Divides.dvd}) d dvd x + s) = (\ d dvd x + s)" + "\z.\(x::'a::{linorder,plus,Ring_and_Field.dvd})z.\(x::'a::{linorder,plus,Ring_and_Field.dvd}) d dvd x + s) = (\ d dvd x + s)" "\z.\x(z ::'a::{linorder}).\x>z.(x \ t) = False" "\(z ::'a::{linorder}).\x>z.(x > t) = True" "\(z ::'a::{linorder}).\x>z.(x \ t) = True" - "\z.\(x::'a::{linorder,plus,Divides.dvd})>z. (d dvd x + s) = (d dvd x + s)" - "\z.\(x::'a::{linorder,plus,Divides.dvd})>z. (\ d dvd x + s) = (\ d dvd x + s)" + "\z.\(x::'a::{linorder,plus,Ring_and_Field.dvd})>z. (d dvd x + s) = (d dvd x + s)" + "\z.\(x::'a::{linorder,plus,Ring_and_Field.dvd})>z. (\ d dvd x + s) = (\ d dvd x + s)" "\z.\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 @@ \ \x k. (P x \ Q x) = (P (x - k*D) \ Q (x - k*D))" "\\x k. P x = P (x - k*D); \x k. Q x = Q (x - k*D)\ \ \x k. (P x \ Q x) = (P (x - k*D) \ Q (x - k*D))" - "(d::'a::{comm_ring,Divides.dvd}) dvd D \ \x k. (d dvd x + t) = (d dvd (x - k*D) + t)" - "(d::'a::{comm_ring,Divides.dvd}) dvd D \ \x k. (\d dvd x + t) = (\d dvd (x - k*D) + t)" + "(d::'a::{comm_ring,Ring_and_Field.dvd}) dvd D \ \x k. (d dvd x + t) = (d dvd (x - k*D) + t)" + "(d::'a::{comm_ring,Ring_and_Field.dvd}) dvd D \ \x k. (\d dvd x + t) = (\d dvd (x - k*D) + t)" "\x k. F = F" -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 "\(x::int).(\j\{1 .. D}. \b\B. x \ b + j)\ (d dvd x+t) \ (d dvd (x - D) + t)" by simp next assume d: "d dvd D" - {fix x assume H: "\(d dvd x + t)" with d have "\d dvd (x - D) + t" + {fix x assume H: "\(d dvd x + t)" with d have "\ d dvd (x - D) + t" by (clarsimp simp add: dvd_def,erule_tac x= "ka + k" in allE,simp add: ring_simps)} thus "\(x::int).(\j\{1 .. D}. \b\B. x \ b + j)\ (\d dvd x+t) \ (\d dvd (x - D) + t)" by auto qed blast @@ -360,16 +361,17 @@ apply(fastsimp) done -theorem unity_coeff_ex: "(\(x::'a::{semiring_0,Divides.dvd}). P (l * x)) \ (\x. l dvd (x + 0) \ P x)" - apply (rule eq_reflection[symmetric]) +theorem unity_coeff_ex: "(\(x::'a::{semiring_0,Ring_and_Field.dvd}). P (l * x)) \ (\x. l dvd (x + 0) \ 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 \ 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 diff -r 7a4baad05495 -r 16a26996c30e src/HOL/Ring_and_Field.thy --- 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 \ 'a \ bool" (infixl "dvd" 50) +where + [code func del]: "b dvd a \ (\k. a = b * k)" + +lemma dvdI [intro?]: "a = b * k \ b dvd a" + unfolding dvd_def .. + +lemma dvdE [elim?]: "b dvd a \ (\k. a = b * k \ P) \ 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 \ 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 \ a dvd (b * c)" + unfolding dvd_def by (blast intro: mult_left_commute) + +lemma dvd_mult2: "a dvd b \ 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 \ a dvd c" + by (simp add: dvd_def mult_assoc, blast) + +lemma dvd_mult_right: "a * b dvd c \ b dvd c" + unfolding mult_ac [of a] by (rule dvd_mult_left) + +lemma dvd_0_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 \ 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 \ (0 \ c \ a < 1) \ (c \ 0 \ 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 \ a = 0" + unfolding sgn_if by simp + +lemma sgn_1_pos: + "sgn a = 1 \ a > 0" + unfolding sgn_if by (simp add: neg_equal_zero) + +lemma sgn_1_neg: + "sgn a = - 1 \ 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 diff -r 7a4baad05495 -r 16a26996c30e src/HOL/Tools/Qelim/cooper.ML --- 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) diff -r 7a4baad05495 -r 16a26996c30e src/HOL/Tools/Qelim/presburger.ML --- 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"}] diff -r 7a4baad05495 -r 16a26996c30e src/HOL/Word/BinBoolList.thy --- 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: diff -r 7a4baad05495 -r 16a26996c30e src/HOL/Word/Num_Lemmas.thy --- 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 **) diff -r 7a4baad05495 -r 16a26996c30e src/HOL/ex/coopertac.ML --- 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","\.simps","\.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] diff -r 7a4baad05495 -r 16a26996c30e src/HOL/int_factor_simprocs.ML --- 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} ); diff -r 7a4baad05495 -r 16a26996c30e src/HOL/nat_simprocs.ML --- 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} );