src/HOL/Parity.thy
changeset 63654 f90e3926e627
parent 62597 b3f2b8c906a6
child 64785 ae0bbc8e45ad
     1.1 --- a/src/HOL/Parity.thy	Wed Aug 10 22:05:00 2016 +0200
     1.2 +++ b/src/HOL/Parity.thy	Wed Aug 10 22:05:36 2016 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  section \<open>Parity in rings and semirings\<close>
     1.5  
     1.6  theory Parity
     1.7 -imports Nat_Transfer
     1.8 +  imports Nat_Transfer
     1.9  begin
    1.10  
    1.11  subsection \<open>Ring structures with parity and \<open>even\<close>/\<open>odd\<close> predicates\<close>
    1.12 @@ -21,19 +21,15 @@
    1.13  subclass semiring_numeral ..
    1.14  
    1.15  abbreviation even :: "'a \<Rightarrow> bool"
    1.16 -where
    1.17 -  "even a \<equiv> 2 dvd a"
    1.18 +  where "even a \<equiv> 2 dvd a"
    1.19  
    1.20  abbreviation odd :: "'a \<Rightarrow> bool"
    1.21 -where
    1.22 -  "odd a \<equiv> \<not> 2 dvd a"
    1.23 +  where "odd a \<equiv> \<not> 2 dvd a"
    1.24  
    1.25 -lemma even_zero [simp]:
    1.26 -  "even 0"
    1.27 +lemma even_zero [simp]: "even 0"
    1.28    by (fact dvd_0_right)
    1.29  
    1.30 -lemma even_plus_one_iff [simp]:
    1.31 -  "even (a + 1) \<longleftrightarrow> odd a"
    1.32 +lemma even_plus_one_iff [simp]: "even (a + 1) \<longleftrightarrow> odd a"
    1.33    by (auto simp add: dvd_add_right_iff intro: odd_even_add)
    1.34  
    1.35  lemma evenE [elim?]:
    1.36 @@ -53,13 +49,11 @@
    1.37    with * have "a = 2 * c + 1" by simp
    1.38    with that show thesis .
    1.39  qed
    1.40 - 
    1.41 -lemma even_times_iff [simp]:
    1.42 -  "even (a * b) \<longleftrightarrow> even a \<or> even b"
    1.43 +
    1.44 +lemma even_times_iff [simp]: "even (a * b) \<longleftrightarrow> even a \<or> even b"
    1.45    by (auto dest: even_multD)
    1.46  
    1.47 -lemma even_numeral [simp]:
    1.48 -  "even (numeral (Num.Bit0 n))"
    1.49 +lemma even_numeral [simp]: "even (numeral (Num.Bit0 n))"
    1.50  proof -
    1.51    have "even (2 * numeral n)"
    1.52      unfolding even_times_iff by simp
    1.53 @@ -69,8 +63,7 @@
    1.54      unfolding numeral.simps .
    1.55  qed
    1.56  
    1.57 -lemma odd_numeral [simp]:
    1.58 -  "odd (numeral (Num.Bit1 n))"
    1.59 +lemma odd_numeral [simp]: "odd (numeral (Num.Bit1 n))"
    1.60  proof
    1.61    assume "even (numeral (num.Bit1 n))"
    1.62    then have "even (numeral n + numeral n + 1)"
    1.63 @@ -79,22 +72,18 @@
    1.64      unfolding mult_2 .
    1.65    then have "2 dvd numeral n * 2 + 1"
    1.66      by (simp add: ac_simps)
    1.67 -  with dvd_add_times_triv_left_iff [of 2 "numeral n" 1]
    1.68 -    have "2 dvd 1"
    1.69 -    by simp
    1.70 +  then have "2 dvd 1"
    1.71 +    using dvd_add_times_triv_left_iff [of 2 "numeral n" 1] by simp
    1.72    then show False by simp
    1.73  qed
    1.74  
    1.75 -lemma even_add [simp]:
    1.76 -  "even (a + b) \<longleftrightarrow> (even a \<longleftrightarrow> even b)"
    1.77 +lemma even_add [simp]: "even (a + b) \<longleftrightarrow> (even a \<longleftrightarrow> even b)"
    1.78    by (auto simp add: dvd_add_right_iff dvd_add_left_iff odd_even_add)
    1.79  
    1.80 -lemma odd_add [simp]:
    1.81 -  "odd (a + b) \<longleftrightarrow> (\<not> (odd a \<longleftrightarrow> odd b))"
    1.82 +lemma odd_add [simp]: "odd (a + b) \<longleftrightarrow> (\<not> (odd a \<longleftrightarrow> odd b))"
    1.83    by simp
    1.84  
    1.85 -lemma even_power [simp]:
    1.86 -  "even (a ^ n) \<longleftrightarrow> even a \<and> n > 0"
    1.87 +lemma even_power [simp]: "even (a ^ n) \<longleftrightarrow> even a \<and> n > 0"
    1.88    by (induct n) auto
    1.89  
    1.90  end
    1.91 @@ -104,12 +93,10 @@
    1.92  
    1.93  subclass comm_ring_1 ..
    1.94  
    1.95 -lemma even_minus [simp]:
    1.96 -  "even (- a) \<longleftrightarrow> even a"
    1.97 +lemma even_minus [simp]: "even (- a) \<longleftrightarrow> even a"
    1.98    by (fact dvd_minus_iff)
    1.99  
   1.100 -lemma even_diff [simp]:
   1.101 -  "even (a - b) \<longleftrightarrow> even (a + b)"
   1.102 +lemma even_diff [simp]: "even (a - b) \<longleftrightarrow> even (a + b)"
   1.103    using even_add [of a "- b"] by simp
   1.104  
   1.105  end
   1.106 @@ -117,17 +104,14 @@
   1.107  
   1.108  subsection \<open>Instances for @{typ nat} and @{typ int}\<close>
   1.109  
   1.110 -lemma even_Suc_Suc_iff [simp]:
   1.111 -  "2 dvd Suc (Suc n) \<longleftrightarrow> 2 dvd n"
   1.112 +lemma even_Suc_Suc_iff [simp]: "2 dvd Suc (Suc n) \<longleftrightarrow> 2 dvd n"
   1.113    using dvd_add_triv_right_iff [of 2 n] by simp
   1.114  
   1.115 -lemma even_Suc [simp]:
   1.116 -  "2 dvd Suc n \<longleftrightarrow> \<not> 2 dvd n"
   1.117 +lemma even_Suc [simp]: "2 dvd Suc n \<longleftrightarrow> \<not> 2 dvd n"
   1.118    by (induct n) auto
   1.119  
   1.120 -lemma even_diff_nat [simp]:
   1.121 -  fixes m n :: nat
   1.122 -  shows "2 dvd (m - n) \<longleftrightarrow> m < n \<or> 2 dvd (m + n)"
   1.123 +lemma even_diff_nat [simp]: "2 dvd (m - n) \<longleftrightarrow> m < n \<or> 2 dvd (m + n)"
   1.124 +  for m n :: nat
   1.125  proof (cases "n \<le> m")
   1.126    case True
   1.127    then have "m - n + n * 2 = m + n" by (simp add: mult_2_right)
   1.128 @@ -137,8 +121,8 @@
   1.129  next
   1.130    case False
   1.131    then show ?thesis by simp
   1.132 -qed 
   1.133 -  
   1.134 +qed
   1.135 +
   1.136  instance nat :: semiring_parity
   1.137  proof
   1.138    show "\<not> 2 dvd (1 :: nat)"
   1.139 @@ -165,7 +149,8 @@
   1.140      then obtain r where "Suc n = 2 * r" ..
   1.141      moreover from * obtain s where "m * n = 2 * s" ..
   1.142      then have "2 * s + m = m * Suc n" by simp
   1.143 -    ultimately have " 2 * s + m = 2 * (m * r)" by (simp add: algebra_simps)
   1.144 +    ultimately have " 2 * s + m = 2 * (m * r)"
   1.145 +      by (simp add: algebra_simps)
   1.146      then have "m = 2 * (m * r - s)" by simp
   1.147      then show "2 dvd m" ..
   1.148    qed
   1.149 @@ -176,13 +161,12 @@
   1.150      by (cases n) simp_all
   1.151  qed
   1.152  
   1.153 -lemma odd_pos: 
   1.154 -  "odd (n :: nat) \<Longrightarrow> 0 < n"
   1.155 +lemma odd_pos: "odd n \<Longrightarrow> 0 < n"
   1.156 +  for n :: nat
   1.157    by (auto elim: oddE)
   1.158  
   1.159 -lemma Suc_double_not_eq_double:
   1.160 -  fixes m n :: nat
   1.161 -  shows "Suc (2 * m) \<noteq> 2 * n"
   1.162 +lemma Suc_double_not_eq_double: "Suc (2 * m) \<noteq> 2 * n"
   1.163 +  for m n :: nat
   1.164  proof
   1.165    assume "Suc (2 * m) = 2 * n"
   1.166    moreover have "odd (Suc (2 * m))" and "even (2 * n)"
   1.167 @@ -190,37 +174,34 @@
   1.168    ultimately show False by simp
   1.169  qed
   1.170  
   1.171 -lemma double_not_eq_Suc_double:
   1.172 -  fixes m n :: nat
   1.173 -  shows "2 * m \<noteq> Suc (2 * n)"
   1.174 +lemma double_not_eq_Suc_double: "2 * m \<noteq> Suc (2 * n)"
   1.175 +  for m n :: nat
   1.176    using Suc_double_not_eq_double [of n m] by simp
   1.177  
   1.178 -lemma even_diff_iff [simp]:
   1.179 -  fixes k l :: int
   1.180 -  shows "2 dvd (k - l) \<longleftrightarrow> 2 dvd (k + l)"
   1.181 +lemma even_diff_iff [simp]: "2 dvd (k - l) \<longleftrightarrow> 2 dvd (k + l)"
   1.182 +  for k l :: int
   1.183    using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: mult_2_right)
   1.184  
   1.185 -lemma even_abs_add_iff [simp]:
   1.186 -  fixes k l :: int
   1.187 -  shows "2 dvd (\<bar>k\<bar> + l) \<longleftrightarrow> 2 dvd (k + l)"
   1.188 +lemma even_abs_add_iff [simp]: "2 dvd (\<bar>k\<bar> + l) \<longleftrightarrow> 2 dvd (k + l)"
   1.189 +  for k l :: int
   1.190    by (cases "k \<ge> 0") (simp_all add: ac_simps)
   1.191  
   1.192 -lemma even_add_abs_iff [simp]:
   1.193 -  fixes k l :: int
   1.194 -  shows "2 dvd (k + \<bar>l\<bar>) \<longleftrightarrow> 2 dvd (k + l)"
   1.195 +lemma even_add_abs_iff [simp]: "2 dvd (k + \<bar>l\<bar>) \<longleftrightarrow> 2 dvd (k + l)"
   1.196 +  for k l :: int
   1.197    using even_abs_add_iff [of l k] by (simp add: ac_simps)
   1.198  
   1.199 -lemma odd_Suc_minus_one [simp]:
   1.200 -  "odd n \<Longrightarrow> Suc (n - Suc 0) = n"
   1.201 +lemma odd_Suc_minus_one [simp]: "odd n \<Longrightarrow> Suc (n - Suc 0) = n"
   1.202    by (auto elim: oddE)
   1.203  
   1.204  instance int :: ring_parity
   1.205  proof
   1.206 -  show "\<not> 2 dvd (1 :: int)" by (simp add: dvd_int_unfold_dvd_nat)
   1.207 +  show "\<not> 2 dvd (1 :: int)"
   1.208 +    by (simp add: dvd_int_unfold_dvd_nat)
   1.209 +next
   1.210    fix k l :: int
   1.211    assume "\<not> 2 dvd k"
   1.212    moreover assume "\<not> 2 dvd l"
   1.213 -  ultimately have "2 dvd (nat \<bar>k\<bar> + nat \<bar>l\<bar>)" 
   1.214 +  ultimately have "2 dvd (nat \<bar>k\<bar> + nat \<bar>l\<bar>)"
   1.215      by (auto simp add: dvd_int_unfold_dvd_nat intro: odd_even_add)
   1.216    then have "2 dvd (\<bar>k\<bar> + \<bar>l\<bar>)"
   1.217      by (simp add: dvd_int_unfold_dvd_nat nat_add_distrib)
   1.218 @@ -237,12 +218,10 @@
   1.219    then show "\<exists>l. k = l + 1" ..
   1.220  qed
   1.221  
   1.222 -lemma even_int_iff [simp]:
   1.223 -  "even (int n) \<longleftrightarrow> even n"
   1.224 +lemma even_int_iff [simp]: "even (int n) \<longleftrightarrow> even n"
   1.225    by (simp add: dvd_int_iff)
   1.226  
   1.227 -lemma even_nat_iff:
   1.228 -  "0 \<le> k \<Longrightarrow> even (nat k) \<longleftrightarrow> even k"
   1.229 +lemma even_nat_iff: "0 \<le> k \<Longrightarrow> even (nat k) \<longleftrightarrow> even k"
   1.230    by (simp add: even_int_iff [symmetric])
   1.231  
   1.232  
   1.233 @@ -251,58 +230,47 @@
   1.234  context ring_1
   1.235  begin
   1.236  
   1.237 -lemma power_minus_even [simp]:
   1.238 -  "even n \<Longrightarrow> (- a) ^ n = a ^ n"
   1.239 +lemma power_minus_even [simp]: "even n \<Longrightarrow> (- a) ^ n = a ^ n"
   1.240    by (auto elim: evenE)
   1.241  
   1.242 -lemma power_minus_odd [simp]:
   1.243 -  "odd n \<Longrightarrow> (- a) ^ n = - (a ^ n)"
   1.244 +lemma power_minus_odd [simp]: "odd n \<Longrightarrow> (- a) ^ n = - (a ^ n)"
   1.245    by (auto elim: oddE)
   1.246  
   1.247 -lemma neg_one_even_power [simp]:
   1.248 -  "even n \<Longrightarrow> (- 1) ^ n = 1"
   1.249 +lemma neg_one_even_power [simp]: "even n \<Longrightarrow> (- 1) ^ n = 1"
   1.250    by simp
   1.251  
   1.252 -lemma neg_one_odd_power [simp]:
   1.253 -  "odd n \<Longrightarrow> (- 1) ^ n = - 1"
   1.254 +lemma neg_one_odd_power [simp]: "odd n \<Longrightarrow> (- 1) ^ n = - 1"
   1.255    by simp
   1.256  
   1.257 -end  
   1.258 +end
   1.259  
   1.260  context linordered_idom
   1.261  begin
   1.262  
   1.263 -lemma zero_le_even_power:
   1.264 -  "even n \<Longrightarrow> 0 \<le> a ^ n"
   1.265 +lemma zero_le_even_power: "even n \<Longrightarrow> 0 \<le> a ^ n"
   1.266    by (auto elim: evenE)
   1.267  
   1.268 -lemma zero_le_odd_power:
   1.269 -  "odd n \<Longrightarrow> 0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a"
   1.270 +lemma zero_le_odd_power: "odd n \<Longrightarrow> 0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a"
   1.271    by (auto simp add: power_even_eq zero_le_mult_iff elim: oddE)
   1.272  
   1.273 -lemma zero_le_power_eq:
   1.274 -  "0 \<le> a ^ n \<longleftrightarrow> even n \<or> odd n \<and> 0 \<le> a"
   1.275 +lemma zero_le_power_eq: "0 \<le> a ^ n \<longleftrightarrow> even n \<or> odd n \<and> 0 \<le> a"
   1.276    by (auto simp add: zero_le_even_power zero_le_odd_power)
   1.277 -  
   1.278 -lemma zero_less_power_eq:
   1.279 -  "0 < a ^ n \<longleftrightarrow> n = 0 \<or> even n \<and> a \<noteq> 0 \<or> odd n \<and> 0 < a"
   1.280 +
   1.281 +lemma zero_less_power_eq: "0 < a ^ n \<longleftrightarrow> n = 0 \<or> even n \<and> a \<noteq> 0 \<or> odd n \<and> 0 < a"
   1.282  proof -
   1.283    have [simp]: "0 = a ^ n \<longleftrightarrow> a = 0 \<and> n > 0"
   1.284      unfolding power_eq_0_iff [of a n, symmetric] by blast
   1.285    show ?thesis
   1.286 -  unfolding less_le zero_le_power_eq by auto
   1.287 +    unfolding less_le zero_le_power_eq by auto
   1.288  qed
   1.289  
   1.290 -lemma power_less_zero_eq [simp]:
   1.291 -  "a ^ n < 0 \<longleftrightarrow> odd n \<and> a < 0"
   1.292 +lemma power_less_zero_eq [simp]: "a ^ n < 0 \<longleftrightarrow> odd n \<and> a < 0"
   1.293    unfolding not_le [symmetric] zero_le_power_eq by auto
   1.294 -  
   1.295 -lemma power_le_zero_eq:
   1.296 -  "a ^ n \<le> 0 \<longleftrightarrow> n > 0 \<and> (odd n \<and> a \<le> 0 \<or> even n \<and> a = 0)"
   1.297 -  unfolding not_less [symmetric] zero_less_power_eq by auto 
   1.298  
   1.299 -lemma power_even_abs:
   1.300 -  "even n \<Longrightarrow> \<bar>a\<bar> ^ n = a ^ n"
   1.301 +lemma power_le_zero_eq: "a ^ n \<le> 0 \<longleftrightarrow> n > 0 \<and> (odd n \<and> a \<le> 0 \<or> even n \<and> a = 0)"
   1.302 +  unfolding not_less [symmetric] zero_less_power_eq by auto
   1.303 +
   1.304 +lemma power_even_abs: "even n \<Longrightarrow> \<bar>a\<bar> ^ n = a ^ n"
   1.305    using power_abs [of a n] by (simp add: zero_le_even_power)
   1.306  
   1.307  lemma power_mono_even:
   1.308 @@ -310,30 +278,35 @@
   1.309    shows "a ^ n \<le> b ^ n"
   1.310  proof -
   1.311    have "0 \<le> \<bar>a\<bar>" by auto
   1.312 -  with \<open>\<bar>a\<bar> \<le> \<bar>b\<bar>\<close>
   1.313 -  have "\<bar>a\<bar> ^ n \<le> \<bar>b\<bar> ^ n" by (rule power_mono)
   1.314 -  with \<open>even n\<close> show ?thesis by (simp add: power_even_abs)  
   1.315 +  with \<open>\<bar>a\<bar> \<le> \<bar>b\<bar>\<close> have "\<bar>a\<bar> ^ n \<le> \<bar>b\<bar> ^ n"
   1.316 +    by (rule power_mono)
   1.317 +  with \<open>even n\<close> show ?thesis
   1.318 +    by (simp add: power_even_abs)
   1.319  qed
   1.320  
   1.321  lemma power_mono_odd:
   1.322    assumes "odd n" and "a \<le> b"
   1.323    shows "a ^ n \<le> b ^ n"
   1.324  proof (cases "b < 0")
   1.325 -  case True with \<open>a \<le> b\<close> have "- b \<le> - a" and "0 \<le> - b" by auto
   1.326 -  hence "(- b) ^ n \<le> (- a) ^ n" by (rule power_mono)
   1.327 +  case True
   1.328 +  with \<open>a \<le> b\<close> have "- b \<le> - a" and "0 \<le> - b" by auto
   1.329 +  then have "(- b) ^ n \<le> (- a) ^ n" by (rule power_mono)
   1.330    with \<open>odd n\<close> show ?thesis by simp
   1.331  next
   1.332 -  case False then have "0 \<le> b" by auto
   1.333 +  case False
   1.334 +  then have "0 \<le> b" by auto
   1.335    show ?thesis
   1.336    proof (cases "a < 0")
   1.337 -    case True then have "n \<noteq> 0" and "a \<le> 0" using \<open>odd n\<close> [THEN odd_pos] by auto
   1.338 +    case True
   1.339 +    then have "n \<noteq> 0" and "a \<le> 0" using \<open>odd n\<close> [THEN odd_pos] by auto
   1.340      then have "a ^ n \<le> 0" unfolding power_le_zero_eq using \<open>odd n\<close> by auto
   1.341 -    moreover
   1.342 -    from \<open>0 \<le> b\<close> have "0 \<le> b ^ n" by auto
   1.343 +    moreover from \<open>0 \<le> b\<close> have "0 \<le> b ^ n" by auto
   1.344      ultimately show ?thesis by auto
   1.345    next
   1.346 -    case False then have "0 \<le> a" by auto
   1.347 -    with \<open>a \<le> b\<close> show ?thesis using power_mono by auto
   1.348 +    case False
   1.349 +    then have "0 \<le> a" by auto
   1.350 +    with \<open>a \<le> b\<close> show ?thesis
   1.351 +      using power_mono by auto
   1.352    qed
   1.353  qed
   1.354  
   1.355 @@ -347,13 +320,16 @@
   1.356    by (fact zero_le_power_eq)
   1.357  
   1.358  lemma zero_less_power_eq_numeral [simp]:
   1.359 -  "0 < a ^ numeral w \<longleftrightarrow> numeral w = (0 :: nat)
   1.360 -    \<or> even (numeral w :: nat) \<and> a \<noteq> 0 \<or> odd (numeral w :: nat) \<and> 0 < a"
   1.361 +  "0 < a ^ numeral w \<longleftrightarrow>
   1.362 +    numeral w = (0 :: nat) \<or>
   1.363 +    even (numeral w :: nat) \<and> a \<noteq> 0 \<or>
   1.364 +    odd (numeral w :: nat) \<and> 0 < a"
   1.365    by (fact zero_less_power_eq)
   1.366  
   1.367  lemma power_le_zero_eq_numeral [simp]:
   1.368 -  "a ^ numeral w \<le> 0 \<longleftrightarrow> (0 :: nat) < numeral w
   1.369 -    \<and> (odd (numeral w :: nat) \<and> a \<le> 0 \<or> even (numeral w :: nat) \<and> a = 0)"
   1.370 +  "a ^ numeral w \<le> 0 \<longleftrightarrow>
   1.371 +    (0 :: nat) < numeral w \<and>
   1.372 +    (odd (numeral w :: nat) \<and> a \<le> 0 \<or> even (numeral w :: nat) \<and> a = 0)"
   1.373    by (fact power_le_zero_eq)
   1.374  
   1.375  lemma power_less_zero_eq_numeral [simp]:
   1.376 @@ -367,10 +343,8 @@
   1.377  end
   1.378  
   1.379  
   1.380 -subsubsection \<open>Tools setup\<close>
   1.381 +subsubsection \<open>Tool setup\<close>
   1.382  
   1.383 -declare transfer_morphism_int_nat [transfer add return:
   1.384 -  even_int_iff
   1.385 -]
   1.386 +declare transfer_morphism_int_nat [transfer add return: even_int_iff]
   1.387  
   1.388  end