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.81 +  by (auto elim!: oddE simp add: zero_not_eq_two [symmetric] add.assoc)
    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
    1.98    using even_abs_add_iff [of l k] by (simp add: ac_simps)
    1.99  
   1.100 -lemma odd_Suc_minus_one [simp]: "odd n \<Longrightarrow> Suc (n - Suc 0) = n"
   1.101 -  by (auto elim: oddE)
   1.102 -
   1.103  instance int :: ring_parity
   1.104  proof
   1.105    show "\<not> 2 dvd (1 :: int)"