even more cleanup
authorhaftmann
Thu Oct 16 19:26:13 2014 +0200 (2014-10-16)
changeset 586875469874b0228
parent 58686 15e5b44d5ed2
child 58688 ddd124805260
even more cleanup
src/HOL/Parity.thy
     1.1 --- a/src/HOL/Parity.thy	Thu Oct 16 11:56:46 2014 +0200
     1.2 +++ b/src/HOL/Parity.thy	Thu Oct 16 19:26:13 2014 +0200
     1.3 @@ -19,6 +19,20 @@
     1.4    "2 dvd Suc n \<longleftrightarrow> \<not> 2 dvd n"
     1.5    by (induct n) auto
     1.6  
     1.7 +lemma two_dvd_diff_nat_iff:
     1.8 +  fixes m n :: nat
     1.9 +  shows "2 dvd m - n \<longleftrightarrow> m < n \<or> 2 dvd m + n"
    1.10 +proof (cases "n \<le> m")
    1.11 +  case True
    1.12 +  then have "m - n + n * 2 = m + n" by simp
    1.13 +  moreover have "2 dvd m - n \<longleftrightarrow> 2 dvd m - n + n * 2" by simp
    1.14 +  ultimately have "2 dvd m - n \<longleftrightarrow> 2 dvd m + n" by (simp only:)
    1.15 +  then show ?thesis by auto
    1.16 +next
    1.17 +  case False
    1.18 +  then show ?thesis by simp
    1.19 +qed 
    1.20 +  
    1.21  lemma two_dvd_diff_iff:
    1.22    fixes k l :: int
    1.23    shows "2 dvd k - l \<longleftrightarrow> 2 dvd k + l"
    1.24 @@ -267,79 +281,93 @@
    1.25  end
    1.26  
    1.27  
    1.28 -subsubsection {* Particularities for @{typ nat}/@{typ int} *}
    1.29 +subsubsection {* Particularities for @{typ nat} and @{typ int} *}
    1.30 +
    1.31 +lemma even_Suc [simp, presburger, algebra]:
    1.32 +  "even (Suc n) = odd n"
    1.33 +  by (simp add: even_def two_dvd_Suc_iff)
    1.34 +
    1.35 +lemma even_diff_nat [simp]:
    1.36 +  fixes m n :: nat
    1.37 +  shows "even (m - n) \<longleftrightarrow> m < n \<or> even (m + n)"
    1.38 +  by (simp add: even_def two_dvd_diff_nat_iff)
    1.39  
    1.40  lemma even_int_iff:
    1.41    "even (int n) \<longleftrightarrow> even n"
    1.42    by (simp add: even_def dvd_int_iff)
    1.43  
    1.44 +lemma even_nat_iff:
    1.45 +  "0 \<le> k \<Longrightarrow> even (nat k) \<longleftrightarrow> even k"
    1.46 +  by (simp add: even_int_iff [symmetric])
    1.47 +
    1.48 +
    1.49 +subsubsection {* Tools setup *}
    1.50 +
    1.51  declare transfer_morphism_int_nat [transfer add return:
    1.52    even_int_iff
    1.53  ]
    1.54  
    1.55 -
    1.56 -subsubsection {* Tools setup *}
    1.57 -
    1.58  lemma [presburger]:
    1.59    "even n \<longleftrightarrow> even (int n)"
    1.60    using even_int_iff [of n] by simp
    1.61  
    1.62 -lemma [presburger]:
    1.63 +lemma (in semiring_parity) [presburger]:
    1.64    "even (a + b) \<longleftrightarrow> even a \<and> even b \<or> odd a \<and> odd b"
    1.65    by auto
    1.66  
    1.67 +lemma [presburger, algebra]:
    1.68 +  fixes m n :: nat
    1.69 +  shows "even (m - n) \<longleftrightarrow> m < n \<or> even m \<and> even n \<or> odd m \<and> odd n"
    1.70 +  by auto
    1.71 +
    1.72 +lemma [presburger, algebra]:
    1.73 +  fixes m n :: nat
    1.74 +  shows "even (m ^ n) \<longleftrightarrow> even m \<and> 0 < n"
    1.75 +  by simp
    1.76 +
    1.77 +lemma [presburger]:
    1.78 +  fixes k :: int
    1.79 +  shows "(k + 1) div 2 = k div 2 \<longleftrightarrow> even k"
    1.80 +  by presburger
    1.81 +
    1.82 +lemma [presburger]:
    1.83 +  fixes k :: int
    1.84 +  shows "(k + 1) div 2 = k div 2 + 1 \<longleftrightarrow> odd k"
    1.85 +  by presburger
    1.86 +  
    1.87 +lemma [presburger]:
    1.88 +  "Suc n div Suc (Suc 0) = n div Suc (Suc 0) \<longleftrightarrow> even n"
    1.89 +  by presburger
    1.90 +
    1.91  
    1.92  subsubsection {* Legacy cruft *}
    1.93  
    1.94  
    1.95  subsubsection {* Equivalent definitions *}
    1.96  
    1.97 -lemma two_times_even_div_two:
    1.98 -  "even (x::int) ==> 2 * (x div 2) = x" 
    1.99 +lemma even_nat_mod_two_eq_zero:
   1.100 +  "even (x::nat) ==> x mod Suc (Suc 0) = 0"
   1.101    by presburger
   1.102  
   1.103 -lemma two_times_odd_div_two_plus_one:
   1.104 -  "odd (x::int) ==> 2 * (x div 2) + 1 = x"
   1.105 -  by presburger
   1.106 -  
   1.107 -
   1.108 -subsubsection {* even and odd for nats *}
   1.109 -
   1.110 -lemma pos_int_even_equiv_nat_even: "0 \<le> x ==> even x = even (nat x)"
   1.111 -by (simp add: even_int_iff [symmetric])
   1.112 -
   1.113 -lemma even_difference_nat [simp,presburger,algebra]:
   1.114 -  "even ((x::nat) - y) = (x < y | (even x & even y) | (odd x & odd y))"
   1.115 +lemma odd_nat_mod_two_eq_one:
   1.116 +  "odd (x::nat) ==> x mod Suc (Suc 0) = Suc 0"
   1.117    by presburger
   1.118  
   1.119 -lemma even_Suc [simp ,presburger, algebra]:
   1.120 -  "even (Suc x) = odd x"
   1.121 +lemma even_nat_equiv_def:
   1.122 +  "even (x::nat) = (x mod Suc (Suc 0) = 0)"
   1.123    by presburger
   1.124  
   1.125 -lemma even_power_nat[simp,presburger,algebra]:
   1.126 -  "even ((x::nat)^y) = (even x & 0 < y)"
   1.127 -  by simp
   1.128 -
   1.129 -
   1.130 -subsubsection {* Equivalent definitions *}
   1.131 -
   1.132 -lemma even_nat_mod_two_eq_zero: "even (x::nat) ==> x mod (Suc (Suc 0)) = 0"
   1.133 -by presburger
   1.134 +lemma odd_nat_equiv_def:
   1.135 +  "odd (x::nat) = (x mod Suc (Suc 0) = Suc 0)"
   1.136 +  by presburger
   1.137  
   1.138 -lemma odd_nat_mod_two_eq_one: "odd (x::nat) ==> x mod (Suc (Suc 0)) = Suc 0"
   1.139 -by presburger
   1.140 -
   1.141 -lemma even_nat_equiv_def: "even (x::nat) = (x mod Suc (Suc 0) = 0)"
   1.142 -by presburger
   1.143 +lemma even_nat_div_two_times_two:
   1.144 +  "even (x::nat) ==> Suc (Suc 0) * (x div Suc (Suc 0)) = x"
   1.145 +  by presburger
   1.146  
   1.147 -lemma odd_nat_equiv_def: "odd (x::nat) = (x mod Suc (Suc 0) = Suc 0)"
   1.148 -by presburger
   1.149 -
   1.150 -lemma even_nat_div_two_times_two: "even (x::nat) ==>
   1.151 -    Suc (Suc 0) * (x div Suc (Suc 0)) = x" by presburger
   1.152 -
   1.153 -lemma odd_nat_div_two_times_two_plus_one: "odd (x::nat) ==>
   1.154 -    Suc( Suc (Suc 0) * (x div Suc (Suc 0))) = x" by presburger
   1.155 +lemma odd_nat_div_two_times_two_plus_one:
   1.156 +  "odd (x::nat) ==> Suc (Suc (Suc 0) * (x div Suc (Suc 0))) = x"
   1.157 +  by presburger
   1.158  
   1.159  
   1.160  subsubsection {* Parity and powers *}
   1.161 @@ -452,12 +480,13 @@
   1.162  lemma even_mult_two_ex: "even(n) = (\<exists>m::nat. n = 2*m)" by presburger
   1.163  lemma odd_Suc_mult_two_ex: "odd(n) = (\<exists>m. n = Suc (2*m))" by presburger
   1.164  
   1.165 -lemma lemma_even_div2 [simp]: "even (n::nat) ==> (n + 1) div 2 = n div 2" by presburger
   1.166 +lemma lemma_even_div2 [simp]: "even (n::nat) ==> (n + 1) div 2 = n div 2"
   1.167 +  by presburger
   1.168  
   1.169 -lemma lemma_not_even_div2 [simp]: "~even n ==> (n + 1) div 2 = Suc (n div 2)"
   1.170 -by presburger
   1.171 +lemma lemma_odd_div2 [simp]: "odd n ==> (n + 1) div 2 = Suc (n div 2)"
   1.172 +  by presburger
   1.173  
   1.174 -lemma even_num_iff: "0 < n ==> even n = (~ even(n - 1 :: nat))"  by presburger
   1.175 +lemma even_num_iff: "0 < n ==> even n = (odd (n - 1 :: nat))" by presburger
   1.176  lemma even_even_mod_4_iff: "even (n::nat) = even (n mod 4)" by presburger
   1.177  
   1.178  lemma lemma_odd_mod_4_div_2: "n mod 4 = (3::nat) ==> odd((n - 1) div 2)" by presburger
   1.179 @@ -510,17 +539,13 @@
   1.180  
   1.181  subsubsection {* Miscellaneous *}
   1.182  
   1.183 -lemma [presburger]:"(x + 1) div 2 = x div 2 \<longleftrightarrow> even (x::int)" by presburger
   1.184 -lemma [presburger]: "(x + 1) div 2 = x div 2 + 1 \<longleftrightarrow> odd (x::int)" by presburger
   1.185 -lemma even_plus_one_div_two: "even (x::int) ==> (x + 1) div 2 = x div 2"  by presburger
   1.186 -lemma odd_plus_one_div_two: "odd (x::int) ==> (x + 1) div 2 = x div 2 + 1" by presburger
   1.187 +lemma even_nat_plus_one_div_two:
   1.188 +  "even (x::nat) ==> (Suc x) div Suc (Suc 0) = x div Suc (Suc 0)"
   1.189 +  by presburger
   1.190  
   1.191 -lemma [presburger]: "(Suc x) div Suc (Suc 0) = x div Suc (Suc 0) \<longleftrightarrow> even x" by presburger
   1.192 -lemma even_nat_plus_one_div_two: "even (x::nat) ==>
   1.193 -    (Suc x) div Suc (Suc 0) = x div Suc (Suc 0)" by presburger
   1.194 -
   1.195 -lemma odd_nat_plus_one_div_two: "odd (x::nat) ==>
   1.196 -    (Suc x) div Suc (Suc 0) = Suc (x div Suc (Suc 0))" by presburger
   1.197 +lemma odd_nat_plus_one_div_two:
   1.198 +  "odd (x::nat) ==> (Suc x) div Suc (Suc 0) = Suc (x div Suc (Suc 0))"
   1.199 +  by presburger
   1.200  
   1.201  end
   1.202