src/HOL/Parity.thy
 changeset 66808 1907167b6038 parent 66582 2b49d4888cb8 child 66815 93c6632ddf44
```     1.1 --- a/src/HOL/Parity.thy	Sun Oct 08 22:28:21 2017 +0200
1.2 +++ b/src/HOL/Parity.thy	Sun Oct 08 22:28:21 2017 +0200
1.3 @@ -101,6 +101,92 @@
1.4
1.5  end
1.6
1.7 +class unique_euclidean_semiring_parity = unique_euclidean_semiring +
1.8 +  assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"
1.9 +  assumes one_mod_two_eq_one [simp]: "1 mod 2 = 1"
1.10 +  assumes zero_not_eq_two: "0 \<noteq> 2"
1.11 +begin
1.12 +
1.13 +lemma parity_cases [case_names even odd]:
1.14 +  assumes "a mod 2 = 0 \<Longrightarrow> P"
1.15 +  assumes "a mod 2 = 1 \<Longrightarrow> P"
1.16 +  shows P
1.17 +  using assms parity by blast
1.18 +
1.19 +lemma one_div_two_eq_zero [simp]:
1.20 +  "1 div 2 = 0"
1.21 +proof (cases "2 = 0")
1.22 +  case True then show ?thesis by simp
1.23 +next
1.24 +  case False
1.25 +  from div_mult_mod_eq have "1 div 2 * 2 + 1 mod 2 = 1" .
1.26 +  with one_mod_two_eq_one have "1 div 2 * 2 + 1 = 1" by simp
1.27 +  then have "1 div 2 * 2 = 0" by (simp add: ac_simps add_left_imp_eq del: mult_eq_0_iff)
1.28 +  then have "1 div 2 = 0 \<or> 2 = 0" by simp
1.29 +  with False show ?thesis by auto
1.30 +qed
1.31 +
1.32 +lemma not_mod_2_eq_0_eq_1 [simp]:
1.33 +  "a mod 2 \<noteq> 0 \<longleftrightarrow> a mod 2 = 1"
1.34 +  by (cases a rule: parity_cases) simp_all
1.35 +
1.36 +lemma not_mod_2_eq_1_eq_0 [simp]:
1.37 +  "a mod 2 \<noteq> 1 \<longleftrightarrow> a mod 2 = 0"
1.38 +  by (cases a rule: parity_cases) simp_all
1.39 +
1.40 +subclass semiring_parity
1.41 +proof (unfold_locales, unfold dvd_eq_mod_eq_0 not_mod_2_eq_0_eq_1)
1.42 +  show "1 mod 2 = 1"
1.43 +    by (fact one_mod_two_eq_one)
1.44 +next
1.45 +  fix a b
1.46 +  assume "a mod 2 = 1"
1.47 +  moreover assume "b mod 2 = 1"
1.48 +  ultimately show "(a + b) mod 2 = 0"
1.49 +    using mod_add_eq [of a 2 b] by simp
1.50 +next
1.51 +  fix a b
1.52 +  assume "(a * b) mod 2 = 0"
1.53 +  then have "(a mod 2) * (b mod 2) mod 2 = 0"
1.54 +    by (simp add: mod_mult_eq)
1.55 +  then have "(a mod 2) * (b mod 2) = 0"
1.56 +    by (cases "a mod 2 = 0") simp_all
1.57 +  then show "a mod 2 = 0 \<or> b mod 2 = 0"
1.58 +    by (rule divisors_zero)
1.59 +next
1.60 +  fix a
1.61 +  assume "a mod 2 = 1"
1.62 +  then have "a = a div 2 * 2 + 1"
1.63 +    using div_mult_mod_eq [of a 2] by simp
1.64 +  then show "\<exists>b. a = b + 1" ..
1.65 +qed
1.66 +
1.67 +lemma even_iff_mod_2_eq_zero:
1.68 +  "even a \<longleftrightarrow> a mod 2 = 0"
1.69 +  by (fact dvd_eq_mod_eq_0)
1.70 +
1.71 +lemma odd_iff_mod_2_eq_one:
1.72 +  "odd a \<longleftrightarrow> a mod 2 = 1"
1.73 +  by (simp add: even_iff_mod_2_eq_zero)
1.74 +
1.75 +lemma even_succ_div_two [simp]:
1.76 +  "even a \<Longrightarrow> (a + 1) div 2 = a div 2"
1.77 +  by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero)
1.78 +
1.79 +lemma odd_succ_div_two [simp]:
1.80 +  "odd a \<Longrightarrow> (a + 1) div 2 = a div 2 + 1"
1.82 +
1.83 +lemma even_two_times_div_two:
1.84 +  "even a \<Longrightarrow> 2 * (a div 2) = a"
1.85 +  by (fact dvd_mult_div_cancel)
1.86 +
1.87 +lemma odd_two_times_div_two_succ [simp]:
1.88 +  "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
1.89 +  using mult_div_mod_eq [of 2 a] by (simp add: even_iff_mod_2_eq_zero)
1.90 +
1.91 +end
1.92 +
1.93
1.94  subsection \<open>Instances for @{typ nat} and @{typ int}\<close>
1.95
1.96 @@ -190,9 +276,6 @@
1.97    for k l :: int