# HG changeset patch # User haftmann # Date 1507569051 -7200 # Node ID 909ba5ed93ddc0d771a99f5d53cfe77422a0b4d6 # Parent 17989f6bc7b2717c969151157f88afedb9354909 clarified parity diff -r 17989f6bc7b2 -r 909ba5ed93dd src/HOL/Code_Numeral.thy --- a/src/HOL/Code_Numeral.thy Mon Oct 09 19:10:49 2017 +0200 +++ b/src/HOL/Code_Numeral.thy Mon Oct 09 19:10:51 2017 +0200 @@ -263,7 +263,7 @@ by transfer (simp add: division_segment_int_def) instance integer :: ring_parity - by (standard; transfer) (simp_all add: of_nat_div odd_iff_mod_2_eq_one) + by (standard; transfer) (simp_all add: of_nat_div division_segment_int_def) instantiation integer :: unique_euclidean_semiring_numeral begin @@ -891,7 +891,7 @@ by (simp add: natural_eq_iff) instance natural :: semiring_parity - by (standard; transfer) (simp_all add: of_nat_div odd_iff_mod_2_eq_one) + by (standard; transfer) simp_all lift_definition natural_of_integer :: "integer \ natural" is "nat :: int \ nat" diff -r 17989f6bc7b2 -r 909ba5ed93dd src/HOL/Euclidean_Division.thy --- a/src/HOL/Euclidean_Division.thy Mon Oct 09 19:10:49 2017 +0200 +++ b/src/HOL/Euclidean_Division.thy Mon Oct 09 19:10:51 2017 +0200 @@ -511,7 +511,7 @@ \ euclidean_size (a * b) < euclidean_size (c * b)" -- \FIXME justify\ fixes division_segment :: "'a \ 'a" - assumes is_unit_division_segment: "is_unit (division_segment a)" + assumes is_unit_division_segment [simp]: "is_unit (division_segment a)" and division_segment_mult: "a \ 0 \ b \ 0 \ division_segment (a * b) = division_segment a * division_segment b" and division_segment_mod: @@ -522,6 +522,10 @@ \ (q * b + r) div b = q" begin +lemma division_segment_not_0 [simp]: + "division_segment a \ 0" + using is_unit_division_segment [of a] is_unitE [of "division_segment a"] by blast + lemma divmod_cases [case_names divides remainder by0]: obtains (divides) q where "b \ 0" diff -r 17989f6bc7b2 -r 909ba5ed93dd src/HOL/Parity.thy --- a/src/HOL/Parity.thy Mon Oct 09 19:10:49 2017 +0200 +++ b/src/HOL/Parity.thy Mon Oct 09 19:10:51 2017 +0200 @@ -13,10 +13,48 @@ class semiring_parity = linordered_semidom + unique_euclidean_semiring + assumes of_nat_div: "of_nat (m div n) = of_nat m div of_nat n" - and odd_imp_mod_2_eq_1: "\ 2 dvd a \ a mod 2 = 1" + 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 -context semiring_parity -begin +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") @@ -86,7 +124,43 @@ lemma odd_iff_mod_2_eq_one: "odd a \ a mod 2 = 1" - by (auto dest: odd_imp_mod_2_eq_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)" + proof (rule ccontr) + assume "\ 1 \ euclidean_size (a mod 2)" + then have "euclidean_size (a mod 2) = 0" + by simp + then have "division_segment (a mod 2) * of_nat (euclidean_size (a mod 2)) = division_segment (a mod 2) * of_nat 0" + by simp + with \odd a\ show False + by (simp add: dvd_eq_mod_eq_0) + qed + 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 parity_cases [case_names even odd]: assumes "even a \ a mod 2 = 0 \ P" @@ -487,22 +561,7 @@ subsection \Instance for @{typ int}\ instance int :: ring_parity -proof - fix k l :: int - show "k mod 2 = 1" if "\ 2 dvd k" - proof (rule order_antisym) - have "0 \ k mod 2" and "k mod 2 < 2" - by auto - moreover have "k mod 2 \ 0" - using that by (simp add: dvd_eq_mod_eq_0) - ultimately have "0 < k mod 2" - by (simp only: less_le) simp - then show "1 \ k mod 2" - by simp - from \k mod 2 < 2\ show "k mod 2 \ 1" - by (simp only: less_le) simp - qed -qed (simp_all add: dvd_eq_mod_eq_0 divide_int_def) + by standard (simp_all add: dvd_eq_mod_eq_0 divide_int_def division_segment_int_def) lemma even_diff_iff [simp]: "even (k - l) \ even (k + l)" for k l :: int