src/HOL/Parity.thy
 changeset 58778 e29cae8eab1f parent 58777 6ba2f1fa243b child 58787 af9eb5e566dd
```     1.1 --- a/src/HOL/Parity.thy	Thu Oct 23 19:40:39 2014 +0200
1.2 +++ b/src/HOL/Parity.thy	Thu Oct 23 19:40:41 2014 +0200
1.3 @@ -6,7 +6,7 @@
1.4  header {* Even and Odd for int and nat *}
1.5
1.6  theory Parity
1.7 -imports Divides
1.8 +imports Nat_Transfer
1.9  begin
1.10
1.11  subsection {* Preliminaries about divisibility on @{typ nat} and @{typ int} *}
1.12 @@ -139,48 +139,6 @@
1.13    then show "\<exists>l. k = l + 1" ..
1.14  qed
1.15
1.16 -context semiring_div_parity
1.17 -begin
1.18 -
1.19 -subclass semiring_parity
1.20 -proof (unfold_locales, unfold dvd_eq_mod_eq_0 not_mod_2_eq_0_eq_1)
1.21 -  fix a b c
1.22 -  show "(c * a + b) mod a = 0 \<longleftrightarrow> b mod a = 0"
1.23 -    by simp
1.24 -next
1.25 -  fix a b c
1.26 -  assume "(b + c) mod a = 0"
1.27 -  with mod_add_eq [of b c a]
1.28 -  have "(b mod a + c mod a) mod a = 0"
1.29 -    by simp
1.30 -  moreover assume "b mod a = 0"
1.31 -  ultimately show "c mod a = 0"
1.32 -    by simp
1.33 -next
1.34 -  show "1 mod 2 = 1"
1.35 -    by (fact one_mod_two_eq_one)
1.36 -next
1.37 -  fix a b
1.38 -  assume "a mod 2 = 1"
1.39 -  moreover assume "b mod 2 = 1"
1.40 -  ultimately show "(a + b) mod 2 = 0"
1.41 -    using mod_add_eq [of a b 2] by simp
1.42 -next
1.43 -  fix a b
1.44 -  assume "(a * b) mod 2 = 0"
1.45 -  then have "(a mod 2) * (b mod 2) = 0"
1.46 -    by (cases "a mod 2 = 0") (simp_all add: mod_mult_eq [of a b 2])
1.47 -  then show "a mod 2 = 0 \<or> b mod 2 = 0"
1.48 -    by (rule divisors_zero)
1.49 -next
1.50 -  fix a
1.51 -  assume "a mod 2 = 1"
1.52 -  then have "a = a div 2 * 2 + 1" using mod_div_equality [of a 2] by simp
1.53 -  then show "\<exists>b. a = b + 1" ..
1.54 -qed
1.55 -
1.56 -end
1.57 -
1.58
1.59  subsection {* Dedicated @{text even}/@{text odd} predicate *}
1.60
1.61 @@ -274,47 +232,6 @@
1.62  end
1.63
1.64
1.65 -subsubsection {* Parity and division *}
1.66 -
1.67 -context semiring_div_parity
1.68 -begin
1.69 -
1.70 -lemma one_div_two_eq_zero [simp]: -- \<open>FIXME move\<close>
1.71 -  "1 div 2 = 0"
1.72 -proof (cases "2 = 0")
1.73 -  case True then show ?thesis by simp
1.74 -next
1.75 -  case False
1.76 -  from mod_div_equality have "1 div 2 * 2 + 1 mod 2 = 1" .
1.77 -  with one_mod_two_eq_one have "1 div 2 * 2 + 1 = 1" by simp
1.78 -  then have "1 div 2 * 2 = 0" by (simp add: ac_simps add_left_imp_eq)
1.79 -  then have "1 div 2 = 0 \<or> 2 = 0" by (rule divisors_zero)
1.80 -  with False show ?thesis by auto
1.81 -qed
1.82 -
1.83 -lemma even_iff_mod_2_eq_zero:
1.84 -  "even a \<longleftrightarrow> a mod 2 = 0"
1.85 -  by (fact dvd_eq_mod_eq_0)
1.86 -
1.87 -lemma even_succ_div_two [simp]:
1.88 -  "even a \<Longrightarrow> (a + 1) div 2 = a div 2"
1.89 -  by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero)
1.90 -
1.91 -lemma odd_succ_div_two [simp]:
1.92 -  "odd a \<Longrightarrow> (a + 1) div 2 = a div 2 + 1"
1.94 -
1.95 -lemma even_two_times_div_two:
1.96 -  "even a \<Longrightarrow> 2 * (a div 2) = a"
1.97 -  by (fact dvd_mult_div_cancel)
1.98 -
1.99 -lemma odd_two_times_div_two_succ:
1.100 -  "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
1.101 -  using mod_div_equality2 [of 2 a] by (simp add: even_iff_mod_2_eq_zero)
1.102 -
1.103 -end
1.104 -
1.105 -
1.106  subsubsection {* Particularities for @{typ nat} and @{typ int} *}
1.107
1.108  lemma even_Suc [simp]:
1.109 @@ -342,44 +259,6 @@
1.110    "0 < n \<Longrightarrow> even n = odd (n - 1 :: nat)"
1.111    by simp
1.112
1.113 -lemma even_Suc_div_two [simp]:
1.114 -  "even n \<Longrightarrow> Suc n div 2 = n div 2"
1.115 -  using even_succ_div_two [of n] by simp
1.116 -
1.117 -lemma odd_Suc_div_two [simp]:
1.118 -  "odd n \<Longrightarrow> Suc n div 2 = Suc (n div 2)"
1.119 -  using odd_succ_div_two [of n] by simp
1.120 -
1.121 -lemma odd_two_times_div_two_Suc:
1.122 -  "odd n \<Longrightarrow> Suc (2 * (n div 2)) = n"
1.123 -  using odd_two_times_div_two_succ [of n] by simp
1.124 -
1.125 -lemma parity_induct [case_names zero even odd]:
1.126 -  assumes zero: "P 0"
1.127 -  assumes even: "\<And>n. P n \<Longrightarrow> P (2 * n)"
1.128 -  assumes odd: "\<And>n. P n \<Longrightarrow> P (Suc (2 * n))"
1.129 -  shows "P n"
1.130 -proof (induct n rule: less_induct)
1.131 -  case (less n)
1.132 -  show "P n"
1.133 -  proof (cases "n = 0")
1.134 -    case True with zero show ?thesis by simp
1.135 -  next
1.136 -    case False
1.137 -    with less have hyp: "P (n div 2)" by simp
1.138 -    show ?thesis
1.139 -    proof (cases "even n")
1.140 -      case True
1.141 -      with hyp even [of "n div 2"] show ?thesis
1.142 -        by (simp add: dvd_mult_div_cancel)
1.143 -    next
1.144 -      case False
1.145 -      with hyp odd [of "n div 2"] show ?thesis
1.146 -        by (simp add: odd_two_times_div_two_Suc)
1.147 -    qed
1.148 -  qed
1.149 -qed
1.150 -
1.151  text {* Parity and powers *}
1.152
1.153  context comm_ring_1
```