# HG changeset patch # User haftmann # Date 1427133914 -3600 # Node ID 034b13f4efae78f50f44d89a857b477f1e2fc7b4 # Parent cce82e360c2f6af1c567f2acf40f436627f59211 distributivity of partial minus establishes desired properties of dvd in semirings diff -r cce82e360c2f -r 034b13f4efae src/HOL/Code_Numeral.thy --- a/src/HOL/Code_Numeral.thy Mon Mar 23 19:05:14 2015 +0100 +++ b/src/HOL/Code_Numeral.thy Mon Mar 23 19:05:14 2015 +0100 @@ -217,9 +217,7 @@ instance integer :: semiring_numeral_div by intro_classes (transfer, - fact semiring_numeral_div_class.diff_invert_add1 - semiring_numeral_div_class.le_add_diff_inverse2 - semiring_numeral_div_class.mult_div_cancel + fact semiring_numeral_div_class.le_add_diff_inverse2 semiring_numeral_div_class.div_less semiring_numeral_div_class.mod_less semiring_numeral_div_class.div_positive diff -r cce82e360c2f -r 034b13f4efae src/HOL/Divides.thy --- a/src/HOL/Divides.thy Mon Mar 23 19:05:14 2015 +0100 +++ b/src/HOL/Divides.thy Mon Mar 23 19:05:14 2015 +0100 @@ -548,7 +548,7 @@ subsubsection {* Parity and division *} -class semiring_div_parity = semiring_div + semiring_numeral + +class semiring_div_parity = comm_semiring_1_diff_distrib + numeral + semiring_div + assumes parity: "a mod 2 = 0 \ a mod 2 = 1" assumes one_mod_two_eq_one [simp]: "1 mod 2 = 1" assumes zero_not_eq_two: "0 \ 2" @@ -583,19 +583,6 @@ subclass semiring_parity proof (unfold_locales, unfold dvd_eq_mod_eq_0 not_mod_2_eq_0_eq_1) - fix a b c - show "(c * a + b) mod a = 0 \ b mod a = 0" - by simp -next - fix a b c - assume "(b + c) mod a = 0" - with mod_add_eq [of b c a] - have "(b mod a + c mod a) mod a = 0" - by simp - moreover assume "b mod a = 0" - ultimately show "c mod a = 0" - by simp -next show "1 mod 2 = 1" by (fact one_mod_two_eq_one) next @@ -651,11 +638,9 @@ and less technical class hierarchy. *} -class semiring_numeral_div = linordered_semidom + minus + semiring_div + - assumes diff_invert_add1: "a + b = c \ a = c - b" - and le_add_diff_inverse2: "b \ a \ a - b + b = a" - assumes mult_div_cancel: "b * (a div b) = a - a mod b" - and div_less: "0 \ a \ a < b \ a div b = 0" +class semiring_numeral_div = comm_semiring_1_diff_distrib + linordered_semidom + semiring_div + + assumes le_add_diff_inverse2: "b \ a \ a - b + b = a" + assumes div_less: "0 \ a \ a < b \ a div b = 0" and mod_less: " 0 \ a \ a < b \ a mod b = a" and div_positive: "0 < b \ b \ a \ a div b > 0" and mod_less_eq_dividend: "0 \ a \ a mod b \ a" @@ -666,9 +651,16 @@ assumes discrete: "a < b \ a + 1 \ b" begin -lemma diff_zero [simp]: - "a - 0 = a" - by (rule diff_invert_add1 [symmetric]) simp +lemma mult_div_cancel: + "b * (a div b) = a - a mod b" +proof - + have "b * (a div b) + a mod b = a" + using mod_div_equality [of a b] by (simp add: ac_simps) + then have "b * (a div b) + a mod b - a mod b = a - a mod b" + by simp + then show ?thesis + by simp +qed subclass semiring_div_parity proof @@ -713,7 +705,7 @@ by (simp add: w_def div_mult2_eq mult_div_cancel ac_simps) with `w = 1` have div: "2 * (a div (2 * b)) = a div b - 1" by simp then show ?P and ?Q - by (simp_all add: div mod diff_invert_add1 [symmetric] le_add_diff_inverse2) + by (simp_all add: div mod add_implies_diff [symmetric] le_add_diff_inverse2) qed lemma divmod_digit_0: @@ -862,7 +854,7 @@ end -hide_fact (open) diff_invert_add1 le_add_diff_inverse2 diff_zero +hide_fact (open) le_add_diff_inverse2 -- {* restore simple accesses for more general variants of theorems *} diff -r cce82e360c2f -r 034b13f4efae src/HOL/NSA/StarDef.thy --- a/src/HOL/NSA/StarDef.thy Mon Mar 23 19:05:14 2015 +0100 +++ b/src/HOL/NSA/StarDef.thy Mon Mar 23 19:05:14 2015 +0100 @@ -698,7 +698,7 @@ star_inf_def [transfer_unfold]: "inf \ *f2* inf" instance - by default (transfer star_inf_def, auto)+ + by default (transfer, auto)+ end @@ -709,7 +709,7 @@ star_sup_def [transfer_unfold]: "sup \ *f2* sup" instance - by default (transfer star_sup_def, auto)+ + by default (transfer, auto)+ end @@ -850,11 +850,8 @@ declare dvd_def [transfer_refold] -instance star :: (semiring_dvd) semiring_dvd -apply intro_classes -apply(transfer, rule dvd_add_times_triv_left_iff) -apply(transfer, erule (1) dvd_addD) -done +instance star :: (comm_semiring_1_diff_distrib) comm_semiring_1_diff_distrib +by intro_classes (transfer, fact right_diff_distrib') instance star :: (no_zero_divisors) no_zero_divisors by (intro_classes, transfer, rule no_zero_divisors) @@ -1040,18 +1037,16 @@ instance star :: (semiring_numeral_div) semiring_numeral_div apply intro_classes -apply(transfer, erule semiring_numeral_div_class.diff_invert_add1) -apply(transfer, erule semiring_numeral_div_class.le_add_diff_inverse2) -apply(transfer, rule semiring_numeral_div_class.mult_div_cancel) -apply(transfer, erule (1) semiring_numeral_div_class.div_less) -apply(transfer, erule (1) semiring_numeral_div_class.mod_less) -apply(transfer, erule (1) semiring_numeral_div_class.div_positive) -apply(transfer, erule semiring_numeral_div_class.mod_less_eq_dividend) -apply(transfer, erule semiring_numeral_div_class.pos_mod_bound) -apply(transfer, erule semiring_numeral_div_class.pos_mod_sign) -apply(transfer, erule semiring_numeral_div_class.mod_mult2_eq) -apply(transfer, erule semiring_numeral_div_class.div_mult2_eq) -apply(transfer, rule discrete) +apply(transfer, fact semiring_numeral_div_class.le_add_diff_inverse2) +apply(transfer, fact semiring_numeral_div_class.div_less) +apply(transfer, fact semiring_numeral_div_class.mod_less) +apply(transfer, fact semiring_numeral_div_class.div_positive) +apply(transfer, fact semiring_numeral_div_class.mod_less_eq_dividend) +apply(transfer, fact semiring_numeral_div_class.pos_mod_bound) +apply(transfer, fact semiring_numeral_div_class.pos_mod_sign) +apply(transfer, fact semiring_numeral_div_class.mod_mult2_eq) +apply(transfer, fact semiring_numeral_div_class.div_mult2_eq) +apply(transfer, fact discrete) done subsection {* Finite class *} diff -r cce82e360c2f -r 034b13f4efae src/HOL/NSA/transfer.ML --- a/src/HOL/NSA/transfer.ML Mon Mar 23 19:05:14 2015 +0100 +++ b/src/HOL/NSA/transfer.ML Mon Mar 23 19:05:14 2015 +0100 @@ -68,7 +68,7 @@ in Goal.prove ctxt [] [] (Logic.mk_equals (t,u)) (K tac) end fun transfer_tac ctxt ths = - SUBGOAL (fn (t,i) => + SUBGOAL (fn (t, _) => (fn th => let val tr = transfer_thm_of ctxt ths t diff -r cce82e360c2f -r 034b13f4efae src/HOL/Nat.thy --- a/src/HOL/Nat.thy Mon Mar 23 19:05:14 2015 +0100 +++ b/src/HOL/Nat.thy Mon Mar 23 19:05:14 2015 +0100 @@ -366,12 +366,20 @@ text {* Difference distributes over multiplication *} -lemma diff_mult_distrib: "((m::nat) - n) * k = (m * k) - (n * k)" -by (induct m n rule: diff_induct) (simp_all add: diff_cancel) - -lemma diff_mult_distrib2: "k * ((m::nat) - n) = (k * m) - (k * n)" -by (simp add: diff_mult_distrib mult.commute [of k]) - -- {* NOT added as rewrites, since sometimes they are used from right-to-left *} +instance nat :: comm_semiring_1_diff_distrib +proof + fix k m n :: nat + show "k * ((m::nat) - n) = (k * m) - (k * n)" + by (induct m n rule: diff_induct) simp_all +qed + +lemma diff_mult_distrib: + "((m::nat) - n) * k = (m * k) - (n * k)" + by (fact left_diff_distrib') + +lemma diff_mult_distrib2: + "k * ((m::nat) - n) = (k * m) - (k * n)" + by (fact right_diff_distrib') subsubsection {* Multiplication *} @@ -1876,48 +1884,6 @@ subsection {* The divides relation on @{typ nat} *} -instance nat :: semiring_dvd -proof - fix m n q :: nat - show "m dvd q * m + n \ m dvd n" (is "?P \ ?Q") - proof - assume ?Q then show ?P by simp - next - assume ?P then obtain d where *: "q * m + n = m * d" .. - show ?Q - proof (cases "n = 0") - case True then show ?Q by simp - next - case False - with * have "q * m < m * d" - using less_add_eq_less [of 0 n "q * m" "m * d"] by simp - then have "q \ d" by (auto intro: ccontr simp add: mult.commute [of m]) - with * [symmetric] have "n = m * (d - q)" - by (simp add: diff_mult_distrib2 mult.commute [of m]) - then show ?Q .. - qed - qed - assume "m dvd n + q" and "m dvd n" - show "m dvd q" - proof - - from `m dvd n` obtain d where "n = m * d" .. - moreover from `m dvd n + q` obtain e where "n + q = m * e" .. - ultimately have *: "m * d + q = m * e" by simp - show "m dvd q" - proof (cases "q = 0") - case True then show ?thesis by simp - next - case False - with * have "m * d < m * e" - using less_add_eq_less [of 0 q "m * d" "m * e"] by simp - then have "d \ e" by (auto intro: ccontr) - with * have "q = m * (e - d)" - by (simp add: diff_mult_distrib2) - then show ?thesis .. - qed - qed -qed - lemma dvd_1_left [iff]: "Suc 0 dvd k" unfolding dvd_def by simp diff -r cce82e360c2f -r 034b13f4efae src/HOL/Number_Theory/Cong.thy --- a/src/HOL/Number_Theory/Cong.thy Mon Mar 23 19:05:14 2015 +0100 +++ b/src/HOL/Number_Theory/Cong.thy Mon Mar 23 19:05:14 2015 +0100 @@ -443,7 +443,7 @@ apply (erule ssubst) apply (subst zmod_zmult2_eq) apply (auto simp add: mod_add_left_eq mod_minus_right div_minus_right) - apply (metis mod_diff_left_eq mod_diff_right_eq mod_mult_self1_is_0 semiring_numeral_div_class.diff_zero)+ + apply (metis mod_diff_left_eq mod_diff_right_eq mod_mult_self1_is_0 diff_zero)+ done lemma cong_to_1_nat: "([(a::nat) = 1] (mod n)) \ (n dvd (a - 1))" diff -r cce82e360c2f -r 034b13f4efae src/HOL/Parity.thy --- a/src/HOL/Parity.thy Mon Mar 23 19:05:14 2015 +0100 +++ b/src/HOL/Parity.thy Mon Mar 23 19:05:14 2015 +0100 @@ -11,13 +11,15 @@ subsection {* Ring structures with parity and @{text even}/@{text odd} predicates *} -class semiring_parity = semiring_dvd + semiring_numeral + +class semiring_parity = comm_semiring_1_diff_distrib + numeral + assumes odd_one [simp]: "\ 2 dvd 1" assumes odd_even_add: "\ 2 dvd a \ \ 2 dvd b \ 2 dvd a + b" assumes even_multD: "2 dvd a * b \ 2 dvd a \ 2 dvd b" assumes odd_ex_decrement: "\ 2 dvd a \ \b. a = b + 1" begin +subclass semiring_numeral .. + abbreviation even :: "'a \ bool" where "even a \ 2 dvd a" @@ -97,9 +99,11 @@ end -class ring_parity = comm_ring_1 + semiring_parity +class ring_parity = ring + semiring_parity begin +subclass comm_ring_1 .. + lemma even_minus [simp]: "even (- a) \ even a" by (fact dvd_minus_iff) diff -r cce82e360c2f -r 034b13f4efae src/HOL/Rings.thy --- a/src/HOL/Rings.thy Mon Mar 23 19:05:14 2015 +0100 +++ b/src/HOL/Rings.thy Mon Mar 23 19:05:14 2015 +0100 @@ -228,35 +228,6 @@ end -class semiring_dvd = comm_semiring_1 + - assumes dvd_add_times_triv_left_iff [simp]: "a dvd c * a + b \ a dvd b" - assumes dvd_addD: "a dvd b + c \ a dvd b \ a dvd c" -begin - -lemma dvd_add_times_triv_right_iff [simp]: - "a dvd b + c * a \ a dvd b" - using dvd_add_times_triv_left_iff [of a c b] by (simp add: ac_simps) - -lemma dvd_add_triv_left_iff [simp]: - "a dvd a + b \ a dvd b" - using dvd_add_times_triv_left_iff [of a 1 b] by simp - -lemma dvd_add_triv_right_iff [simp]: - "a dvd b + a \ a dvd b" - using dvd_add_times_triv_right_iff [of a b 1] by simp - -lemma dvd_add_right_iff: - assumes "a dvd b" - shows "a dvd b + c \ a dvd c" - using assms by (auto dest: dvd_addD) - -lemma dvd_add_left_iff: - assumes "a dvd c" - shows "a dvd b + c \ a dvd b" - using assms dvd_add_right_iff [of a c b] by (simp add: ac_simps) - -end - class no_zero_divisors = zero + times + assumes no_zero_divisors: "a \ 0 \ b \ 0 \ a * b \ 0" begin @@ -293,6 +264,65 @@ end +class comm_semiring_1_diff_distrib = comm_semiring_1_cancel + + assumes right_diff_distrib' [algebra_simps]: "a * (b - c) = a * b - a * c" +begin + +lemma left_diff_distrib' [algebra_simps]: + "(b - c) * a = b * a - c * a" + by (simp add: algebra_simps) + +lemma dvd_add_times_triv_left_iff [simp]: + "a dvd c * a + b \ a dvd b" +proof - + have "a dvd a * c + b \ a dvd b" (is "?P \ ?Q") + proof + assume ?Q then show ?P by simp + next + assume ?P + then obtain d where "a * c + b = a * d" .. + then have "a * c + b - a * c = a * d - a * c" by simp + then have "b = a * d - a * c" by simp + then have "b = a * (d - c)" by (simp add: algebra_simps) + then show ?Q .. + qed + then show "a dvd c * a + b \ a dvd b" by (simp add: ac_simps) +qed + +lemma dvd_add_times_triv_right_iff [simp]: + "a dvd b + c * a \ a dvd b" + using dvd_add_times_triv_left_iff [of a c b] by (simp add: ac_simps) + +lemma dvd_add_triv_left_iff [simp]: + "a dvd a + b \ a dvd b" + using dvd_add_times_triv_left_iff [of a 1 b] by simp + +lemma dvd_add_triv_right_iff [simp]: + "a dvd b + a \ a dvd b" + using dvd_add_times_triv_right_iff [of a b 1] by simp + +lemma dvd_add_right_iff: + assumes "a dvd b" + shows "a dvd b + c \ a dvd c" (is "?P \ ?Q") +proof + assume ?P then obtain d where "b + c = a * d" .. + moreover from `a dvd b` obtain e where "b = a * e" .. + ultimately have "a * e + c = a * d" by simp + then have "a * e + c - a * e = a * d - a * e" by simp + then have "c = a * d - a * e" by simp + then have "c = a * (d - e)" by (simp add: algebra_simps) + then show ?Q .. +next + assume ?Q with assms show ?P by simp +qed + +lemma dvd_add_left_iff: + assumes "a dvd c" + shows "a dvd b + c \ a dvd b" + using assms dvd_add_right_iff [of a c b] by (simp add: ac_simps) + +end + class ring = semiring + ab_group_add begin @@ -370,27 +400,8 @@ subclass ring_1 .. subclass comm_semiring_1_cancel .. -subclass semiring_dvd -proof - fix a b c - show "a dvd c * a + b \ a dvd b" (is "?P \ ?Q") - proof - assume ?Q then show ?P by simp - next - assume ?P then obtain d where "c * a + b = a * d" .. - then have "b = a * (d - c)" by (simp add: algebra_simps) - then show ?Q .. - qed - assume "a dvd b + c" and "a dvd b" - show "a dvd c" - proof - - from `a dvd b` obtain d where "b = a * d" .. - moreover from `a dvd b + c` obtain e where "b + c = a * e" .. - ultimately have "a * d + c = a * e" by simp - then have "c = a * (e - d)" by (simp add: algebra_simps) - then show "a dvd c" .. - qed -qed +subclass comm_semiring_1_diff_distrib + by unfold_locales (simp add: algebra_simps) lemma dvd_minus_iff [simp]: "x dvd - y \ x dvd y" proof @@ -1265,4 +1276,3 @@ code_module Rings \ (SML) Arith and (OCaml) Arith and (Haskell) Arith end -