src/HOL/Parity.thy
changeset 60343 063698416239
parent 59816 034b13f4efae
child 60562 24af00b010cf
     1.1 --- a/src/HOL/Parity.thy	Mon Jun 01 18:59:20 2015 +0200
     1.2 +++ b/src/HOL/Parity.thy	Mon Jun 01 18:59:20 2015 +0200
     1.3 @@ -118,75 +118,60 @@
     1.4  subsection {* Instances for @{typ nat} and @{typ int} *}
     1.5  
     1.6  lemma even_Suc_Suc_iff [simp]:
     1.7 -  "even (Suc (Suc n)) \<longleftrightarrow> even n"
     1.8 +  "2 dvd Suc (Suc n) \<longleftrightarrow> 2 dvd n"
     1.9    using dvd_add_triv_right_iff [of 2 n] by simp
    1.10  
    1.11  lemma even_Suc [simp]:
    1.12 -  "even (Suc n) \<longleftrightarrow> odd n"
    1.13 +  "2 dvd Suc n \<longleftrightarrow> \<not> 2 dvd n"
    1.14    by (induct n) auto
    1.15  
    1.16  lemma even_diff_nat [simp]:
    1.17    fixes m n :: nat
    1.18 -  shows "even (m - n) \<longleftrightarrow> m < n \<or> even (m + n)"
    1.19 +  shows "2 dvd (m - n) \<longleftrightarrow> m < n \<or> 2 dvd (m + n)"
    1.20  proof (cases "n \<le> m")
    1.21    case True
    1.22    then have "m - n + n * 2 = m + n" by (simp add: mult_2_right)
    1.23 -  moreover have "even (m - n) \<longleftrightarrow> even (m - n + n * 2)" by simp
    1.24 -  ultimately have "even (m - n) \<longleftrightarrow> even (m + n)" by (simp only:)
    1.25 +  moreover have "2 dvd (m - n) \<longleftrightarrow> 2 dvd (m - n + n * 2)" by simp
    1.26 +  ultimately have "2 dvd (m - n) \<longleftrightarrow> 2 dvd (m + n)" by (simp only:)
    1.27    then show ?thesis by auto
    1.28  next
    1.29    case False
    1.30    then show ?thesis by simp
    1.31  qed 
    1.32    
    1.33 -lemma even_diff_iff [simp]:
    1.34 -  fixes k l :: int
    1.35 -  shows "even (k - l) \<longleftrightarrow> even (k + l)"
    1.36 -  using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: mult_2_right)
    1.37 -
    1.38 -lemma even_abs_add_iff [simp]:
    1.39 -  fixes k l :: int
    1.40 -  shows "even (\<bar>k\<bar> + l) \<longleftrightarrow> even (k + l)"
    1.41 -  by (cases "k \<ge> 0") (simp_all add: ac_simps)
    1.42 -
    1.43 -lemma even_add_abs_iff [simp]:
    1.44 -  fixes k l :: int
    1.45 -  shows "even (k + \<bar>l\<bar>) \<longleftrightarrow> even (k + l)"
    1.46 -  using even_abs_add_iff [of l k] by (simp add: ac_simps)
    1.47 -
    1.48  instance nat :: semiring_parity
    1.49  proof
    1.50 -  show "odd (1 :: nat)"
    1.51 +  show "\<not> 2 dvd (1 :: nat)"
    1.52      by (rule notI, erule dvdE) simp
    1.53  next
    1.54    fix m n :: nat
    1.55 -  assume "odd m"
    1.56 -  moreover assume "odd n"
    1.57 -  ultimately have *: "even (Suc m) \<and> even (Suc n)"
    1.58 +  assume "\<not> 2 dvd m"
    1.59 +  moreover assume "\<not> 2 dvd n"
    1.60 +  ultimately have *: "2 dvd Suc m \<and> 2 dvd Suc n"
    1.61      by simp
    1.62 -  then have "even (Suc m + Suc n)"
    1.63 +  then have "2 dvd (Suc m + Suc n)"
    1.64      by (blast intro: dvd_add)
    1.65    also have "Suc m + Suc n = m + n + 2"
    1.66      by simp
    1.67 -  finally show "even (m + n)"
    1.68 +  finally show "2 dvd (m + n)"
    1.69      using dvd_add_triv_right_iff [of 2 "m + n"] by simp
    1.70  next
    1.71    fix m n :: nat
    1.72 -  assume *: "even (m * n)"
    1.73 -  show "even m \<or> even n"
    1.74 +  assume *: "2 dvd (m * n)"
    1.75 +  show "2 dvd m \<or> 2 dvd n"
    1.76    proof (rule disjCI)
    1.77 -    assume "odd n"
    1.78 -    then have "even (Suc n)" by simp
    1.79 +    assume "\<not> 2 dvd n"
    1.80 +    then have "2 dvd (Suc n)" by simp
    1.81      then obtain r where "Suc n = 2 * r" ..
    1.82      moreover from * obtain s where "m * n = 2 * s" ..
    1.83      then have "2 * s + m = m * Suc n" by simp
    1.84      ultimately have " 2 * s + m = 2 * (m * r)" by (simp add: algebra_simps)
    1.85      then have "m = 2 * (m * r - s)" by simp
    1.86 -    then show "even m" ..
    1.87 +    then show "2 dvd m" ..
    1.88    qed
    1.89  next
    1.90    fix n :: nat
    1.91 -  assume "odd n"
    1.92 +  assume "\<not> 2 dvd n"
    1.93    then show "\<exists>m. n = m + 1"
    1.94      by (cases n) simp_all
    1.95  qed
    1.96 @@ -194,23 +179,38 @@
    1.97  lemma odd_pos: 
    1.98    "odd (n :: nat) \<Longrightarrow> 0 < n"
    1.99    by (auto elim: oddE)
   1.100 -  
   1.101 +
   1.102 +lemma even_diff_iff [simp]:
   1.103 +  fixes k l :: int
   1.104 +  shows "2 dvd (k - l) \<longleftrightarrow> 2 dvd (k + l)"
   1.105 +  using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: mult_2_right)
   1.106 +
   1.107 +lemma even_abs_add_iff [simp]:
   1.108 +  fixes k l :: int
   1.109 +  shows "2 dvd (\<bar>k\<bar> + l) \<longleftrightarrow> 2 dvd (k + l)"
   1.110 +  by (cases "k \<ge> 0") (simp_all add: ac_simps)
   1.111 +
   1.112 +lemma even_add_abs_iff [simp]:
   1.113 +  fixes k l :: int
   1.114 +  shows "2 dvd (k + \<bar>l\<bar>) \<longleftrightarrow> 2 dvd (k + l)"
   1.115 +  using even_abs_add_iff [of l k] by (simp add: ac_simps)
   1.116 +
   1.117  instance int :: ring_parity
   1.118  proof
   1.119 -  show "odd (1 :: int)" by (simp add: dvd_int_unfold_dvd_nat)
   1.120 +  show "\<not> 2 dvd (1 :: int)" by (simp add: dvd_int_unfold_dvd_nat)
   1.121    fix k l :: int
   1.122 -  assume "odd k"
   1.123 -  moreover assume "odd l"
   1.124 -  ultimately have "even (nat \<bar>k\<bar> + nat \<bar>l\<bar>)" 
   1.125 +  assume "\<not> 2 dvd k"
   1.126 +  moreover assume "\<not> 2 dvd l"
   1.127 +  ultimately have "2 dvd (nat \<bar>k\<bar> + nat \<bar>l\<bar>)" 
   1.128      by (auto simp add: dvd_int_unfold_dvd_nat intro: odd_even_add)
   1.129 -  then have "even (\<bar>k\<bar> + \<bar>l\<bar>)"
   1.130 +  then have "2 dvd (\<bar>k\<bar> + \<bar>l\<bar>)"
   1.131      by (simp add: dvd_int_unfold_dvd_nat nat_add_distrib)
   1.132 -  then show "even (k + l)"
   1.133 +  then show "2 dvd (k + l)"
   1.134      by simp
   1.135  next
   1.136    fix k l :: int
   1.137 -  assume "even (k * l)"
   1.138 -  then show "even k \<or> even l"
   1.139 +  assume "2 dvd (k * l)"
   1.140 +  then show "2 dvd k \<or> 2 dvd l"
   1.141      by (simp add: dvd_int_unfold_dvd_nat even_multD nat_abs_mult_distrib)
   1.142  next
   1.143    fix k :: int
   1.144 @@ -352,4 +352,3 @@
   1.145  ]
   1.146  
   1.147  end
   1.148 -