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.93 -  by (auto elim!: oddE simp add: zero_not_eq_two [symmetric] add.assoc)
    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