# HG changeset patch # User haftmann # Date 1560501267 0 # Node ID 972c0c744e7ca19ca2a6c7bc4b8056814e23ecb6 # Parent 7383930fc94618d9b3e615f4819c3bf1ba71bd70 generalized type classes for parity to cover word types also, which contain zero divisors diff -r 7383930fc946 -r 972c0c744e7c src/HOL/Groebner_Basis.thy --- a/src/HOL/Groebner_Basis.thy Fri Jun 14 08:34:27 2019 +0000 +++ b/src/HOL/Groebner_Basis.thy Fri Jun 14 08:34:27 2019 +0000 @@ -75,7 +75,7 @@ declare mod_eq_dvd_iff[algebra] declare nat_mod_eq_iff[algebra] -context unique_euclidean_semiring_with_nat +context semiring_parity begin declare even_mult_iff [algebra] @@ -83,7 +83,7 @@ end -context unique_euclidean_ring_with_nat +context ring_parity begin declare even_minus [algebra] diff -r 7383930fc946 -r 972c0c744e7c src/HOL/Parity.thy --- a/src/HOL/Parity.thy Fri Jun 14 08:34:27 2019 +0000 +++ b/src/HOL/Parity.thy Fri Jun 14 08:34:27 2019 +0000 @@ -11,165 +11,35 @@ subsection \Ring structures with parity and \even\/\odd\ predicates\ -class unique_euclidean_semiring_with_nat = semidom + semiring_char_0 + unique_euclidean_semiring + - assumes of_nat_div: "of_nat (m div n) = of_nat m div of_nat n" - and division_segment_of_nat [simp]: "division_segment (of_nat n) = 1" - and division_segment_euclidean_size [simp]: "division_segment a * of_nat (euclidean_size a) = a" +class semiring_parity = comm_semiring_1 + semiring_modulo + + assumes even_iff_mod_2_eq_zero: "2 dvd a \ a mod 2 = 0" + and odd_iff_mod_2_eq_one: "\ 2 dvd a \ a mod 2 = 1" + and odd_one [simp]: "\ 2 dvd 1" begin -lemma division_segment_eq_iff: - "a = b" if "division_segment a = division_segment b" - and "euclidean_size a = euclidean_size b" - using that division_segment_euclidean_size [of a] by simp - -lemma euclidean_size_of_nat [simp]: - "euclidean_size (of_nat n) = n" -proof - - have "division_segment (of_nat n) * of_nat (euclidean_size (of_nat n)) = of_nat n" - by (fact division_segment_euclidean_size) - then show ?thesis by simp -qed - -lemma of_nat_euclidean_size: - "of_nat (euclidean_size a) = a div division_segment a" -proof - - have "of_nat (euclidean_size a) = division_segment a * of_nat (euclidean_size a) div division_segment a" - by (subst nonzero_mult_div_cancel_left) simp_all - also have "\ = a div division_segment a" - by simp - finally show ?thesis . -qed - -lemma division_segment_1 [simp]: - "division_segment 1 = 1" - using division_segment_of_nat [of 1] by simp - -lemma division_segment_numeral [simp]: - "division_segment (numeral k) = 1" - using division_segment_of_nat [of "numeral k"] by simp - -lemma euclidean_size_1 [simp]: - "euclidean_size 1 = 1" - using euclidean_size_of_nat [of 1] by simp - -lemma euclidean_size_numeral [simp]: - "euclidean_size (numeral k) = numeral k" - using euclidean_size_of_nat [of "numeral k"] by simp - -lemma of_nat_dvd_iff: - "of_nat m dvd of_nat n \ m dvd n" (is "?P \ ?Q") -proof (cases "m = 0") - case True - then show ?thesis - by simp -next - case False - show ?thesis - proof - assume ?Q - then show ?P - by (auto elim: dvd_class.dvdE) - next - assume ?P - with False have "of_nat n = of_nat n div of_nat m * of_nat m" - by simp - then have "of_nat n = of_nat (n div m * m)" - by (simp add: of_nat_div) - then have "n = n div m * m" - by (simp only: of_nat_eq_iff) - then have "n = m * (n div m)" - by (simp add: ac_simps) - then show ?Q .. - qed -qed - -lemma of_nat_mod: - "of_nat (m mod n) = of_nat m mod of_nat n" -proof - - have "of_nat m div of_nat n * of_nat n + of_nat m mod of_nat n = of_nat m" - by (simp add: div_mult_mod_eq) - also have "of_nat m = of_nat (m div n * n + m mod n)" - by simp - finally show ?thesis - by (simp only: of_nat_div of_nat_mult of_nat_add) simp -qed - -lemma one_div_two_eq_zero [simp]: - "1 div 2 = 0" -proof - - from of_nat_div [symmetric] have "of_nat 1 div of_nat 2 = of_nat 0" - by (simp only:) simp - then show ?thesis - by simp -qed - -lemma one_mod_two_eq_one [simp]: - "1 mod 2 = 1" -proof - - from of_nat_mod [symmetric] have "of_nat 1 mod of_nat 2 = of_nat 1" - by (simp only:) simp - then show ?thesis - by simp -qed - abbreviation even :: "'a \ bool" where "even a \ 2 dvd a" abbreviation odd :: "'a \ bool" where "odd a \ \ 2 dvd a" -lemma even_iff_mod_2_eq_zero: - "even a \ a mod 2 = 0" - by (fact dvd_eq_mod_eq_0) - -lemma odd_iff_mod_2_eq_one: - "odd a \ a mod 2 = 1" -proof - assume "a mod 2 = 1" - then show "odd a" - by auto -next - assume "odd a" - have eucl: "euclidean_size (a mod 2) = 1" - proof (rule order_antisym) - show "euclidean_size (a mod 2) \ 1" - using mod_size_less [of 2 a] by simp - show "1 \ euclidean_size (a mod 2)" - using \odd a\ by (simp add: Suc_le_eq dvd_eq_mod_eq_0) - qed - from \odd a\ have "\ of_nat 2 dvd division_segment a * of_nat (euclidean_size a)" - by simp - then have "\ of_nat 2 dvd of_nat (euclidean_size a)" - by (auto simp only: dvd_mult_unit_iff' is_unit_division_segment) - then have "\ 2 dvd euclidean_size a" - using of_nat_dvd_iff [of 2] by simp - then have "euclidean_size a mod 2 = 1" - by (simp add: semidom_modulo_class.dvd_eq_mod_eq_0) - then have "of_nat (euclidean_size a mod 2) = of_nat 1" - by simp - then have "of_nat (euclidean_size a) mod 2 = 1" - by (simp add: of_nat_mod) - from \odd a\ eucl - show "a mod 2 = 1" - by (auto intro: division_segment_eq_iff simp add: division_segment_mod) -qed - -lemma mod2_eq_if: "x mod 2 = (if even x then 0 else 1)" -by (simp add: odd_iff_mod_2_eq_one) - lemma parity_cases [case_names even odd]: assumes "even a \ a mod 2 = 0 \ P" assumes "odd a \ a mod 2 = 1 \ P" shows P - using assms by (cases "even a") (simp_all add: odd_iff_mod_2_eq_one) + using assms by (cases "even a") + (simp_all add: even_iff_mod_2_eq_zero [symmetric] odd_iff_mod_2_eq_one [symmetric]) + +lemma not_mod_2_eq_0_eq_1 [simp]: + "a mod 2 \ 0 \ a mod 2 = 1" + by (cases a rule: parity_cases) simp_all lemma not_mod_2_eq_1_eq_0 [simp]: "a mod 2 \ 1 \ a mod 2 = 0" by (cases a rule: parity_cases) simp_all -lemma not_mod_2_eq_0_eq_1 [simp]: - "a mod 2 \ 0 \ a mod 2 = 1" - by (cases a rule: parity_cases) simp_all +lemma mod2_eq_if: "a mod 2 = (if 2 dvd a then 0 else 1)" + by (simp add: even_iff_mod_2_eq_zero odd_iff_mod_2_eq_one) lemma evenE [elim?]: assumes "even a" @@ -189,51 +59,16 @@ lemma mod_2_eq_odd: "a mod 2 = of_bool (odd a)" - by (auto elim: oddE) + by (auto elim: oddE simp add: even_iff_mod_2_eq_zero) lemma of_bool_odd_eq_mod_2: "of_bool (odd a) = a mod 2" by (simp add: mod_2_eq_odd) -lemma one_mod_2_pow_eq [simp]: - "1 mod (2 ^ n) = of_bool (n > 0)" -proof - - have "1 mod (2 ^ n) = of_nat (1 mod (2 ^ n))" - using of_nat_mod [of 1 "2 ^ n"] by simp - also have "\ = of_bool (n > 0)" - by simp - finally show ?thesis . -qed - -lemma one_div_2_pow_eq [simp]: - "1 div (2 ^ n) = of_bool (n = 0)" - using div_mult_mod_eq [of 1 "2 ^ n"] by auto - -lemma even_of_nat [simp]: - "even (of_nat a) \ even a" -proof - - have "even (of_nat a) \ of_nat 2 dvd of_nat a" - by simp - also have "\ \ even a" - by (simp only: of_nat_dvd_iff) - finally show ?thesis . -qed - lemma even_zero [simp]: "even 0" by (fact dvd_0_right) -lemma odd_one [simp]: - "odd 1" -proof - - have "\ (2 :: nat) dvd 1" - by simp - then have "\ of_nat 2 dvd of_nat 1" - unfolding of_nat_dvd_iff by simp - then show ?thesis - by simp -qed - lemma odd_even_add: "even (a + b)" if "odd a" and "odd b" proof - @@ -311,6 +146,197 @@ lemma even_power [simp]: "even (a ^ n) \ even a \ n > 0" by (induct n) auto +end + +class ring_parity = ring + semiring_parity +begin + +subclass comm_ring_1 .. + +lemma even_minus: + "even (- a) \ even a" + by (fact dvd_minus_iff) + +lemma even_diff [simp]: + "even (a - b) \ even (a + b)" + using even_add [of a "- b"] by simp + +end + + +subsection \Special case: euclidean rings containing the natural numbers\ + +class unique_euclidean_semiring_with_nat = semidom + semiring_char_0 + unique_euclidean_semiring + + assumes of_nat_div: "of_nat (m div n) = of_nat m div of_nat n" + and division_segment_of_nat [simp]: "division_segment (of_nat n) = 1" + and division_segment_euclidean_size [simp]: "division_segment a * of_nat (euclidean_size a) = a" +begin + +lemma division_segment_eq_iff: + "a = b" if "division_segment a = division_segment b" + and "euclidean_size a = euclidean_size b" + using that division_segment_euclidean_size [of a] by simp + +lemma euclidean_size_of_nat [simp]: + "euclidean_size (of_nat n) = n" +proof - + have "division_segment (of_nat n) * of_nat (euclidean_size (of_nat n)) = of_nat n" + by (fact division_segment_euclidean_size) + then show ?thesis by simp +qed + +lemma of_nat_euclidean_size: + "of_nat (euclidean_size a) = a div division_segment a" +proof - + have "of_nat (euclidean_size a) = division_segment a * of_nat (euclidean_size a) div division_segment a" + by (subst nonzero_mult_div_cancel_left) simp_all + also have "\ = a div division_segment a" + by simp + finally show ?thesis . +qed + +lemma division_segment_1 [simp]: + "division_segment 1 = 1" + using division_segment_of_nat [of 1] by simp + +lemma division_segment_numeral [simp]: + "division_segment (numeral k) = 1" + using division_segment_of_nat [of "numeral k"] by simp + +lemma euclidean_size_1 [simp]: + "euclidean_size 1 = 1" + using euclidean_size_of_nat [of 1] by simp + +lemma euclidean_size_numeral [simp]: + "euclidean_size (numeral k) = numeral k" + using euclidean_size_of_nat [of "numeral k"] by simp + +lemma of_nat_dvd_iff: + "of_nat m dvd of_nat n \ m dvd n" (is "?P \ ?Q") +proof (cases "m = 0") + case True + then show ?thesis + by simp +next + case False + show ?thesis + proof + assume ?Q + then show ?P + by auto + next + assume ?P + with False have "of_nat n = of_nat n div of_nat m * of_nat m" + by simp + then have "of_nat n = of_nat (n div m * m)" + by (simp add: of_nat_div) + then have "n = n div m * m" + by (simp only: of_nat_eq_iff) + then have "n = m * (n div m)" + by (simp add: ac_simps) + then show ?Q .. + qed +qed + +lemma of_nat_mod: + "of_nat (m mod n) = of_nat m mod of_nat n" +proof - + have "of_nat m div of_nat n * of_nat n + of_nat m mod of_nat n = of_nat m" + by (simp add: div_mult_mod_eq) + also have "of_nat m = of_nat (m div n * n + m mod n)" + by simp + finally show ?thesis + by (simp only: of_nat_div of_nat_mult of_nat_add) simp +qed + +lemma one_div_two_eq_zero [simp]: + "1 div 2 = 0" +proof - + from of_nat_div [symmetric] have "of_nat 1 div of_nat 2 = of_nat 0" + by (simp only:) simp + then show ?thesis + by simp +qed + +lemma one_mod_two_eq_one [simp]: + "1 mod 2 = 1" +proof - + from of_nat_mod [symmetric] have "of_nat 1 mod of_nat 2 = of_nat 1" + by (simp only:) simp + then show ?thesis + by simp +qed + +subclass semiring_parity +proof + show "2 dvd a \ a mod 2 = 0" for a + by (fact dvd_eq_mod_eq_0) + show "\ 2 dvd a \ a mod 2 = 1" for a + proof + assume "a mod 2 = 1" + then show "\ 2 dvd a" + by auto + next + assume "\ 2 dvd a" + have eucl: "euclidean_size (a mod 2) = 1" + proof (rule order_antisym) + show "euclidean_size (a mod 2) \ 1" + using mod_size_less [of 2 a] by simp + show "1 \ euclidean_size (a mod 2)" + using \\ 2 dvd a\ by (simp add: Suc_le_eq dvd_eq_mod_eq_0) + qed + from \\ 2 dvd a\ have "\ of_nat 2 dvd division_segment a * of_nat (euclidean_size a)" + by simp + then have "\ of_nat 2 dvd of_nat (euclidean_size a)" + by (auto simp only: dvd_mult_unit_iff' is_unit_division_segment) + then have "\ 2 dvd euclidean_size a" + using of_nat_dvd_iff [of 2] by simp + then have "euclidean_size a mod 2 = 1" + by (simp add: semidom_modulo_class.dvd_eq_mod_eq_0) + then have "of_nat (euclidean_size a mod 2) = of_nat 1" + by simp + then have "of_nat (euclidean_size a) mod 2 = 1" + by (simp add: of_nat_mod) + from \\ 2 dvd a\ eucl + show "a mod 2 = 1" + by (auto intro: division_segment_eq_iff simp add: division_segment_mod) + qed + show "\ is_unit 2" + proof (rule notI) + assume "is_unit 2" + then have "of_nat 2 dvd of_nat 1" + by simp + then have "is_unit (2::nat)" + by (simp only: of_nat_dvd_iff) + then show False + by simp + qed +qed + +lemma even_of_nat [simp]: + "even (of_nat a) \ even a" +proof - + have "even (of_nat a) \ of_nat 2 dvd of_nat a" + by simp + also have "\ \ even a" + by (simp only: of_nat_dvd_iff) + finally show ?thesis . +qed + +lemma one_mod_2_pow_eq [simp]: + "1 mod (2 ^ n) = of_bool (n > 0)" +proof - + have "1 mod (2 ^ n) = of_nat (1 mod (2 ^ n))" + using of_nat_mod [of 1 "2 ^ n"] by simp + also have "\ = of_bool (n > 0)" + by simp + finally show ?thesis . +qed + +lemma one_div_2_pow_eq [simp]: + "1 div (2 ^ n) = of_bool (n = 0)" + using div_mult_mod_eq [of 1 "2 ^ n"] by auto + lemma even_succ_div_two [simp]: "even a \ (a + 1) div 2 = a div 2" by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero) @@ -427,15 +453,7 @@ class unique_euclidean_ring_with_nat = ring + unique_euclidean_semiring_with_nat begin -subclass comm_ring_1 .. - -lemma even_minus: - "even (- a) \ even a" - by (fact dvd_minus_iff) - -lemma even_diff [simp]: - "even (a - b) \ even (a + b)" - using even_add [of a "- b"] by simp +subclass ring_parity .. lemma minus_1_mod_2_eq [simp]: "- 1 mod 2 = 1" @@ -446,7 +464,7 @@ proof - from div_mult_mod_eq [of "- 1" 2] have "- 1 div 2 * 2 = - 1 * 2" - using local.add_implies_diff by fastforce + using add_implies_diff by fastforce then show ?thesis using mult_right_cancel [of 2 "- 1 div 2" "- 1"] by simp qed @@ -519,6 +537,10 @@ by simp qed +lemma not_mod2_eq_Suc_0_eq_0 [simp]: + "n mod 2 \ Suc 0 \ n mod 2 = 0" + using not_mod_2_eq_1_eq_0 [of n] by simp + lemma nat_parity_induct [case_names zero even odd]: "P n" if zero: "P 0" and even: "\n. P n \ n > 0 \ P (2 * n)" @@ -548,10 +570,6 @@ qed qed -lemma not_mod2_eq_Suc_0_eq_0 [simp]: - "n mod 2 \ Suc 0 \ n mod 2 = 0" - using not_mod_2_eq_1_eq_0 [of n] by simp - lemma odd_card_imp_not_empty: \A \ {}\ if \odd (card A)\ using that by auto @@ -762,7 +780,7 @@ subsection \Abstract bit operations\ -context unique_euclidean_semiring_with_nat +context semiring_parity begin text \The primary purpose of the following operations is @@ -777,6 +795,11 @@ definition drop_bit :: "nat \ 'a \ 'a" where drop_bit_eq_div: "drop_bit n a = a div 2 ^ n" +end + +context unique_euclidean_semiring_with_nat +begin + lemma bit_ident: "push_bit n (drop_bit n a) + take_bit n a = a" using div_mult_mod_eq by (simp add: push_bit_eq_mult take_bit_eq_mod drop_bit_eq_div) diff -r 7383930fc946 -r 972c0c744e7c src/HOL/Presburger.thy --- a/src/HOL/Presburger.thy Fri Jun 14 08:34:27 2019 +0000 +++ b/src/HOL/Presburger.thy Fri Jun 14 08:34:27 2019 +0000 @@ -432,7 +432,7 @@ lemma [presburger, algebra]: "m mod (Suc (Suc 0)) = Suc 0 \ \ 2 dvd m " by presburger lemma [presburger, algebra]: "m mod 2 = (1::int) \ \ 2 dvd m " by presburger -context unique_euclidean_semiring_with_nat +context semiring_parity begin declare even_mult_iff [presburger] @@ -445,7 +445,7 @@ end -context unique_euclidean_ring_with_nat +context ring_parity begin declare even_minus [presburger]