src/HOL/Parity.thy
changeset 58770 ae5e9b4f8daf
parent 58769 70fff47875cd
child 58771 0997ea62e868
     1.1 --- a/src/HOL/Parity.thy	Thu Oct 23 14:04:05 2014 +0200
     1.2 +++ b/src/HOL/Parity.thy	Thu Oct 23 14:04:05 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 Main
     1.8 +imports Presburger
     1.9  begin
    1.10  
    1.11  subsection {* Preliminaries about divisibility on @{typ nat} and @{typ int} *}
    1.12 @@ -24,7 +24,7 @@
    1.13    shows "2 dvd m - n \<longleftrightarrow> m < n \<or> 2 dvd m + n"
    1.14  proof (cases "n \<le> m")
    1.15    case True
    1.16 -  then have "m - n + n * 2 = m + n" by simp
    1.17 +  then have "m - n + n * 2 = m + n" by (simp add: mult_2_right)
    1.18    moreover have "2 dvd m - n \<longleftrightarrow> 2 dvd m - n + n * 2" by simp
    1.19    ultimately have "2 dvd m - n \<longleftrightarrow> 2 dvd m + n" by (simp only:)
    1.20    then show ?thesis by auto
    1.21 @@ -103,7 +103,7 @@
    1.22      then obtain r where "Suc n = 2 * r" ..
    1.23      moreover from * obtain s where "m * n = 2 * s" ..
    1.24      then have "2 * s + m = m * Suc n" by simp
    1.25 -    ultimately have " 2 * s + m = 2 * (m * r)" by simp
    1.26 +    ultimately have " 2 * s + m = 2 * (m * r)" by (simp add: algebra_simps)
    1.27      then have "m = 2 * (m * r - s)" by simp
    1.28      then show "2 dvd m" ..
    1.29    qed
    1.30 @@ -207,7 +207,7 @@
    1.31    obtains b where "a = 2 * b + 1"
    1.32    using assms by (rule not_two_dvdE)
    1.33    
    1.34 -lemma even_times_iff [simp, presburger, algebra]:
    1.35 +lemma even_times_iff [simp]:
    1.36    "even (a * b) \<longleftrightarrow> even a \<or> even b"
    1.37    by (auto simp add: dest: two_is_prime)
    1.38  
    1.39 @@ -254,7 +254,7 @@
    1.40    "odd (a + b) \<longleftrightarrow> (\<not> (odd a \<longleftrightarrow> odd b))"
    1.41    by simp
    1.42  
    1.43 -lemma even_power [simp, presburger]:
    1.44 +lemma even_power [simp]:
    1.45    "even (a ^ n) \<longleftrightarrow> even a \<and> n \<noteq> 0"
    1.46    by (induct n) auto
    1.47  
    1.48 @@ -263,7 +263,7 @@
    1.49  context ring_parity
    1.50  begin
    1.51  
    1.52 -lemma even_minus [simp, presburger, algebra]:
    1.53 +lemma even_minus [simp]:
    1.54    "even (- a) \<longleftrightarrow> even a"
    1.55    by (fact dvd_minus_iff)
    1.56  
    1.57 @@ -317,7 +317,7 @@
    1.58  
    1.59  subsubsection {* Particularities for @{typ nat} and @{typ int} *}
    1.60  
    1.61 -lemma even_Suc [simp, presburger, algebra]:
    1.62 +lemma even_Suc [simp]:
    1.63    "even (Suc n) = odd n"
    1.64    by (fact two_dvd_Suc_iff)
    1.65  
    1.66 @@ -380,20 +380,6 @@
    1.67    qed
    1.68  qed
    1.69    
    1.70 -text {* Nice facts about division by @{term 4} *}  
    1.71 -
    1.72 -lemma even_even_mod_4_iff:
    1.73 -  "even (n::nat) \<longleftrightarrow> even (n mod 4)"
    1.74 -  by presburger
    1.75 -
    1.76 -lemma odd_mod_4_div_2:
    1.77 -  "n mod 4 = (3::nat) \<Longrightarrow> odd ((n - 1) div 2)"
    1.78 -  by presburger
    1.79 -
    1.80 -lemma even_mod_4_div_2:
    1.81 -  "n mod 4 = (1::nat) \<Longrightarrow> even ((n - 1) div 2)"
    1.82 -  by presburger
    1.83 -  
    1.84  text {* Parity and powers *}
    1.85  
    1.86  context comm_ring_1
    1.87 @@ -451,7 +437,7 @@
    1.88    "odd n \<Longrightarrow> 0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a"
    1.89    by (auto simp add: power_even_eq zero_le_mult_iff elim: oddE)
    1.90  
    1.91 -lemma zero_le_power_iff [presburger]: -- \<open>FIXME cf. @{text zero_le_power_eq}\<close>
    1.92 +lemma zero_le_power_iff: -- \<open>FIXME cf. @{text zero_le_power_eq}\<close>
    1.93    "0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a \<or> even n"
    1.94  proof (cases "even n")
    1.95    case True
    1.96 @@ -466,11 +452,11 @@
    1.97      by (auto simp add: zero_le_mult_iff zero_le_even_power)
    1.98  qed
    1.99  
   1.100 -lemma zero_le_power_eq [presburger]:
   1.101 +lemma zero_le_power_eq:
   1.102    "0 \<le> a ^ n \<longleftrightarrow> even n \<or> odd n \<and> 0 \<le> a"
   1.103    using zero_le_power_iff [of a n] by auto
   1.104  
   1.105 -lemma zero_less_power_eq [presburger]:
   1.106 +lemma zero_less_power_eq:
   1.107    "0 < a ^ n \<longleftrightarrow> n = 0 \<or> even n \<and> a \<noteq> 0 \<or> odd n \<and> 0 < a"
   1.108  proof -
   1.109    have [simp]: "0 = a ^ n \<longleftrightarrow> a = 0 \<and> n > 0"
   1.110 @@ -479,11 +465,11 @@
   1.111    unfolding less_le zero_le_power_eq by auto
   1.112  qed
   1.113  
   1.114 -lemma power_less_zero_eq [presburger]:
   1.115 +lemma power_less_zero_eq:
   1.116    "a ^ n < 0 \<longleftrightarrow> odd n \<and> a < 0"
   1.117    unfolding not_le [symmetric] zero_le_power_eq by auto
   1.118    
   1.119 -lemma power_le_zero_eq [presburger]:
   1.120 +lemma power_le_zero_eq:
   1.121    "a ^ n \<le> 0 \<longleftrightarrow> n > 0 \<and> (odd n \<and> a \<le> 0 \<or> even n \<and> a = 0)"
   1.122    unfolding not_less [symmetric] zero_less_power_eq by auto 
   1.123  
   1.124 @@ -560,14 +546,47 @@
   1.125    even_int_iff
   1.126  ]
   1.127  
   1.128 +context semiring_parity
   1.129 +begin
   1.130 +
   1.131 +declare even_times_iff [presburger, algebra]
   1.132 +
   1.133 +declare even_power [presburger]
   1.134 +
   1.135  lemma [presburger]:
   1.136 -  "even n \<longleftrightarrow> even (int n)"
   1.137 -  using even_int_iff [of n] by simp
   1.138 -
   1.139 -lemma (in semiring_parity) [presburger]:
   1.140    "even (a + b) \<longleftrightarrow> even a \<and> even b \<or> odd a \<and> odd b"
   1.141    by auto
   1.142  
   1.143 +end
   1.144 +
   1.145 +context ring_parity
   1.146 +begin
   1.147 +
   1.148 +declare even_minus [presburger, algebra]
   1.149 +
   1.150 +end
   1.151 +
   1.152 +context linordered_idom
   1.153 +begin
   1.154 +
   1.155 +declare zero_le_power_iff [presburger]
   1.156 +
   1.157 +declare zero_le_power_eq [presburger]
   1.158 +
   1.159 +declare zero_less_power_eq [presburger]
   1.160 +
   1.161 +declare power_less_zero_eq [presburger]
   1.162 +  
   1.163 +declare power_le_zero_eq [presburger]
   1.164 +
   1.165 +end
   1.166 +
   1.167 +declare even_Suc [presburger, algebra]
   1.168 +
   1.169 +lemma [presburger]:
   1.170 +  "Suc n div Suc (Suc 0) = n div Suc (Suc 0) \<longleftrightarrow> even n"
   1.171 +  by presburger
   1.172 +
   1.173  lemma [presburger, algebra]:
   1.174    fixes m n :: nat
   1.175    shows "even (m - n) \<longleftrightarrow> m < n \<or> even m \<and> even n \<or> odd m \<and> odd n"
   1.176 @@ -587,10 +606,25 @@
   1.177    fixes k :: int
   1.178    shows "(k + 1) div 2 = k div 2 + 1 \<longleftrightarrow> odd k"
   1.179    by presburger
   1.180 -  
   1.181 +
   1.182  lemma [presburger]:
   1.183 -  "Suc n div Suc (Suc 0) = n div Suc (Suc 0) \<longleftrightarrow> even n"
   1.184 +  "even n \<longleftrightarrow> even (int n)"
   1.185 +  using even_int_iff [of n] by simp
   1.186 +  
   1.187 +
   1.188 +subsubsection {* Nice facts about division by @{term 4} *}  
   1.189 +
   1.190 +lemma even_even_mod_4_iff:
   1.191 +  "even (n::nat) \<longleftrightarrow> even (n mod 4)"
   1.192    by presburger
   1.193  
   1.194 +lemma odd_mod_4_div_2:
   1.195 +  "n mod 4 = (3::nat) \<Longrightarrow> odd ((n - 1) div 2)"
   1.196 +  by presburger
   1.197 +
   1.198 +lemma even_mod_4_div_2:
   1.199 +  "n mod 4 = (1::nat) \<Longrightarrow> even ((n - 1) div 2)"
   1.200 +  by presburger
   1.201 +  
   1.202  end
   1.203