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.6  theory Parity
1.7 -imports Nat_Transfer
1.8 +  imports Nat_Transfer
1.9  begin
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.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.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.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.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.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.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.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.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.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.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.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.90  end
1.91 @@ -104,12 +93,10 @@
1.93  subclass comm_ring_1 ..
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.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.105  end
1.106 @@ -117,17 +104,14 @@
1.108  subsection \<open>Instances for @{typ nat} and @{typ int}\<close>
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.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.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.134 +qed
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.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.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.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.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.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.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.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.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.216    then have "2 dvd (\<bar>k\<bar> + \<bar>l\<bar>)"
1.218 @@ -237,12 +218,10 @@
1.219    then show "\<exists>l. k = l + 1" ..
1.220  qed
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.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.233 @@ -251,58 +230,47 @@
1.234  context ring_1
1.235  begin
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.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.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.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.257 -end
1.258 +end
1.260  context linordered_idom
1.261  begin
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.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.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.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.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.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.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.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.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.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.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.355 @@ -347,13 +320,16 @@
1.356    by (fact zero_le_power_eq)
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.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.375  lemma power_less_zero_eq_numeral [simp]:
1.376 @@ -367,10 +343,8 @@
1.377  end
1.380 -subsubsection \<open>Tools setup\<close>
1.381 +subsubsection \<open>Tool setup\<close>
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.388  end