src/HOL/Parity.thy
 author haftmann Sun Oct 08 22:28:22 2017 +0200 (21 months ago) changeset 66815 93c6632ddf44 parent 66808 1907167b6038 child 66816 212a3334e7da permissions -rw-r--r--
one uniform type class for parity structures
```     1 (*  Title:      HOL/Parity.thy
```
```     2     Author:     Jeremy Avigad
```
```     3     Author:     Jacques D. Fleuriot
```
```     4 *)
```
```     5
```
```     6 section \<open>Parity in rings and semirings\<close>
```
```     7
```
```     8 theory Parity
```
```     9   imports Euclidean_Division
```
```    10 begin
```
```    11
```
```    12 subsection \<open>Ring structures with parity and \<open>even\<close>/\<open>odd\<close> predicates\<close>
```
```    13
```
```    14 class semiring_parity = linordered_semidom + unique_euclidean_semiring +
```
```    15   assumes of_nat_div: "of_nat (m div n) = of_nat m div of_nat n"
```
```    16     and odd_imp_mod_2_eq_1: "\<not> 2 dvd a \<Longrightarrow> a mod 2 = 1"
```
```    17
```
```    18 context semiring_parity
```
```    19 begin
```
```    20
```
```    21 lemma of_nat_dvd_iff:
```
```    22   "of_nat m dvd of_nat n \<longleftrightarrow> m dvd n" (is "?P \<longleftrightarrow> ?Q")
```
```    23 proof (cases "m = 0")
```
```    24   case True
```
```    25   then show ?thesis
```
```    26     by simp
```
```    27 next
```
```    28   case False
```
```    29   show ?thesis
```
```    30   proof
```
```    31     assume ?Q
```
```    32     then show ?P
```
```    33       by (auto elim: dvd_class.dvdE)
```
```    34   next
```
```    35     assume ?P
```
```    36     with False have "of_nat n = of_nat n div of_nat m * of_nat m"
```
```    37       by simp
```
```    38     then have "of_nat n = of_nat (n div m * m)"
```
```    39       by (simp add: of_nat_div)
```
```    40     then have "n = n div m * m"
```
```    41       by (simp only: of_nat_eq_iff)
```
```    42     then have "n = m * (n div m)"
```
```    43       by (simp add: ac_simps)
```
```    44     then show ?Q ..
```
```    45   qed
```
```    46 qed
```
```    47
```
```    48 lemma of_nat_mod:
```
```    49   "of_nat (m mod n) = of_nat m mod of_nat n"
```
```    50 proof -
```
```    51   have "of_nat m div of_nat n * of_nat n + of_nat m mod of_nat n = of_nat m"
```
```    52     by (simp add: div_mult_mod_eq)
```
```    53   also have "of_nat m = of_nat (m div n * n + m mod n)"
```
```    54     by simp
```
```    55   finally show ?thesis
```
```    56     by (simp only: of_nat_div of_nat_mult of_nat_add) simp
```
```    57 qed
```
```    58
```
```    59 lemma one_div_two_eq_zero [simp]:
```
```    60   "1 div 2 = 0"
```
```    61 proof -
```
```    62   from of_nat_div [symmetric] have "of_nat 1 div of_nat 2 = of_nat 0"
```
```    63     by (simp only:) simp
```
```    64   then show ?thesis
```
```    65     by simp
```
```    66 qed
```
```    67
```
```    68 lemma one_mod_two_eq_one [simp]:
```
```    69   "1 mod 2 = 1"
```
```    70 proof -
```
```    71   from of_nat_mod [symmetric] have "of_nat 1 mod of_nat 2 = of_nat 1"
```
```    72     by (simp only:) simp
```
```    73   then show ?thesis
```
```    74     by simp
```
```    75 qed
```
```    76
```
```    77 abbreviation even :: "'a \<Rightarrow> bool"
```
```    78   where "even a \<equiv> 2 dvd a"
```
```    79
```
```    80 abbreviation odd :: "'a \<Rightarrow> bool"
```
```    81   where "odd a \<equiv> \<not> 2 dvd a"
```
```    82
```
```    83 lemma even_iff_mod_2_eq_zero:
```
```    84   "even a \<longleftrightarrow> a mod 2 = 0"
```
```    85   by (fact dvd_eq_mod_eq_0)
```
```    86
```
```    87 lemma odd_iff_mod_2_eq_one:
```
```    88   "odd a \<longleftrightarrow> a mod 2 = 1"
```
```    89   by (auto dest: odd_imp_mod_2_eq_1)
```
```    90
```
```    91 lemma parity_cases [case_names even odd]:
```
```    92   assumes "even a \<Longrightarrow> a mod 2 = 0 \<Longrightarrow> P"
```
```    93   assumes "odd a \<Longrightarrow> a mod 2 = 1 \<Longrightarrow> P"
```
```    94   shows P
```
```    95   using assms by (cases "even a") (simp_all add: odd_iff_mod_2_eq_one)
```
```    96
```
```    97 lemma not_mod_2_eq_1_eq_0 [simp]:
```
```    98   "a mod 2 \<noteq> 1 \<longleftrightarrow> a mod 2 = 0"
```
```    99   by (cases a rule: parity_cases) simp_all
```
```   100
```
```   101 lemma not_mod_2_eq_0_eq_1 [simp]:
```
```   102   "a mod 2 \<noteq> 0 \<longleftrightarrow> a mod 2 = 1"
```
```   103   by (cases a rule: parity_cases) simp_all
```
```   104
```
```   105 lemma evenE [elim?]:
```
```   106   assumes "even a"
```
```   107   obtains b where "a = 2 * b"
```
```   108   using assms by (rule dvdE)
```
```   109
```
```   110 lemma oddE [elim?]:
```
```   111   assumes "odd a"
```
```   112   obtains b where "a = 2 * b + 1"
```
```   113 proof -
```
```   114   have "a = 2 * (a div 2) + a mod 2"
```
```   115     by (simp add: mult_div_mod_eq)
```
```   116   with assms have "a = 2 * (a div 2) + 1"
```
```   117     by (simp add: odd_iff_mod_2_eq_one)
```
```   118   then show ?thesis ..
```
```   119 qed
```
```   120
```
```   121 lemma mod_2_eq_odd:
```
```   122   "a mod 2 = of_bool (odd a)"
```
```   123   by (auto elim: oddE)
```
```   124
```
```   125 lemma one_mod_2_pow_eq [simp]:
```
```   126   "1 mod (2 ^ n) = of_bool (n > 0)"
```
```   127 proof -
```
```   128   have "1 mod (2 ^ n) = (of_bool (n > 0) :: nat)"
```
```   129     by (induct n) (simp_all add: mod_mult2_eq)
```
```   130   then have "of_nat (1 mod (2 ^ n)) = of_bool (n > 0)"
```
```   131     by simp
```
```   132   then show ?thesis
```
```   133     by (simp add: of_nat_mod)
```
```   134 qed
```
```   135
```
```   136 lemma even_of_nat [simp]:
```
```   137   "even (of_nat a) \<longleftrightarrow> even a"
```
```   138 proof -
```
```   139   have "even (of_nat a) \<longleftrightarrow> of_nat 2 dvd of_nat a"
```
```   140     by simp
```
```   141   also have "\<dots> \<longleftrightarrow> even a"
```
```   142     by (simp only: of_nat_dvd_iff)
```
```   143   finally show ?thesis .
```
```   144 qed
```
```   145
```
```   146 lemma even_zero [simp]:
```
```   147   "even 0"
```
```   148   by (fact dvd_0_right)
```
```   149
```
```   150 lemma odd_one [simp]:
```
```   151   "odd 1"
```
```   152 proof -
```
```   153   have "\<not> (2 :: nat) dvd 1"
```
```   154     by simp
```
```   155   then have "\<not> of_nat 2 dvd of_nat 1"
```
```   156     unfolding of_nat_dvd_iff by simp
```
```   157   then show ?thesis
```
```   158     by simp
```
```   159 qed
```
```   160
```
```   161 lemma odd_even_add:
```
```   162   "even (a + b)" if "odd a" and "odd b"
```
```   163 proof -
```
```   164   from that obtain c d where "a = 2 * c + 1" and "b = 2 * d + 1"
```
```   165     by (blast elim: oddE)
```
```   166   then have "a + b = 2 * c + 2 * d + (1 + 1)"
```
```   167     by (simp only: ac_simps)
```
```   168   also have "\<dots> = 2 * (c + d + 1)"
```
```   169     by (simp add: algebra_simps)
```
```   170   finally show ?thesis ..
```
```   171 qed
```
```   172
```
```   173 lemma even_add [simp]:
```
```   174   "even (a + b) \<longleftrightarrow> (even a \<longleftrightarrow> even b)"
```
```   175   by (auto simp add: dvd_add_right_iff dvd_add_left_iff odd_even_add)
```
```   176
```
```   177 lemma odd_add [simp]:
```
```   178   "odd (a + b) \<longleftrightarrow> \<not> (odd a \<longleftrightarrow> odd b)"
```
```   179   by simp
```
```   180
```
```   181 lemma even_plus_one_iff [simp]:
```
```   182   "even (a + 1) \<longleftrightarrow> odd a"
```
```   183   by (auto simp add: dvd_add_right_iff intro: odd_even_add)
```
```   184
```
```   185 lemma even_mult_iff [simp]:
```
```   186   "even (a * b) \<longleftrightarrow> even a \<or> even b" (is "?P \<longleftrightarrow> ?Q")
```
```   187 proof
```
```   188   assume ?Q
```
```   189   then show ?P
```
```   190     by auto
```
```   191 next
```
```   192   assume ?P
```
```   193   show ?Q
```
```   194   proof (rule ccontr)
```
```   195     assume "\<not> (even a \<or> even b)"
```
```   196     then have "odd a" and "odd b"
```
```   197       by auto
```
```   198     then obtain r s where "a = 2 * r + 1" and "b = 2 * s + 1"
```
```   199       by (blast elim: oddE)
```
```   200     then have "a * b = (2 * r + 1) * (2 * s + 1)"
```
```   201       by simp
```
```   202     also have "\<dots> = 2 * (2 * r * s + r + s) + 1"
```
```   203       by (simp add: algebra_simps)
```
```   204     finally have "odd (a * b)"
```
```   205       by simp
```
```   206     with \<open>?P\<close> show False
```
```   207       by auto
```
```   208   qed
```
```   209 qed
```
```   210
```
```   211 lemma even_numeral [simp]: "even (numeral (Num.Bit0 n))"
```
```   212 proof -
```
```   213   have "even (2 * numeral n)"
```
```   214     unfolding even_mult_iff by simp
```
```   215   then have "even (numeral n + numeral n)"
```
```   216     unfolding mult_2 .
```
```   217   then show ?thesis
```
```   218     unfolding numeral.simps .
```
```   219 qed
```
```   220
```
```   221 lemma odd_numeral [simp]: "odd (numeral (Num.Bit1 n))"
```
```   222 proof
```
```   223   assume "even (numeral (num.Bit1 n))"
```
```   224   then have "even (numeral n + numeral n + 1)"
```
```   225     unfolding numeral.simps .
```
```   226   then have "even (2 * numeral n + 1)"
```
```   227     unfolding mult_2 .
```
```   228   then have "2 dvd numeral n * 2 + 1"
```
```   229     by (simp add: ac_simps)
```
```   230   then have "2 dvd 1"
```
```   231     using dvd_add_times_triv_left_iff [of 2 "numeral n" 1] by simp
```
```   232   then show False by simp
```
```   233 qed
```
```   234
```
```   235 lemma even_power [simp]: "even (a ^ n) \<longleftrightarrow> even a \<and> n > 0"
```
```   236   by (induct n) auto
```
```   237
```
```   238 lemma even_succ_div_two [simp]:
```
```   239   "even a \<Longrightarrow> (a + 1) div 2 = a div 2"
```
```   240   by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero)
```
```   241
```
```   242 lemma odd_succ_div_two [simp]:
```
```   243   "odd a \<Longrightarrow> (a + 1) div 2 = a div 2 + 1"
```
```   244   by (auto elim!: oddE simp add: add.assoc)
```
```   245
```
```   246 lemma even_two_times_div_two:
```
```   247   "even a \<Longrightarrow> 2 * (a div 2) = a"
```
```   248   by (fact dvd_mult_div_cancel)
```
```   249
```
```   250 lemma odd_two_times_div_two_succ [simp]:
```
```   251   "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
```
```   252   using mult_div_mod_eq [of 2 a]
```
```   253   by (simp add: even_iff_mod_2_eq_zero)
```
```   254
```
```   255 end
```
```   256
```
```   257 class ring_parity = ring + semiring_parity
```
```   258 begin
```
```   259
```
```   260 subclass comm_ring_1 ..
```
```   261
```
```   262 lemma even_minus [simp]:
```
```   263   "even (- a) \<longleftrightarrow> even a"
```
```   264   by (fact dvd_minus_iff)
```
```   265
```
```   266 lemma even_diff [simp]:
```
```   267   "even (a - b) \<longleftrightarrow> even (a + b)"
```
```   268   using even_add [of a "- b"] by simp
```
```   269
```
```   270 end
```
```   271
```
```   272
```
```   273 subsection \<open>Instance for @{typ nat}\<close>
```
```   274
```
```   275 instance nat :: semiring_parity
```
```   276   by standard (simp_all add: dvd_eq_mod_eq_0)
```
```   277
```
```   278 lemma even_Suc_Suc_iff [simp]:
```
```   279   "even (Suc (Suc n)) \<longleftrightarrow> even n"
```
```   280   using dvd_add_triv_right_iff [of 2 n] by simp
```
```   281
```
```   282 lemma even_Suc [simp]: "even (Suc n) \<longleftrightarrow> odd n"
```
```   283   using even_plus_one_iff [of n] by simp
```
```   284
```
```   285 lemma even_diff_nat [simp]:
```
```   286   "even (m - n) \<longleftrightarrow> m < n \<or> even (m + n)" for m n :: nat
```
```   287 proof (cases "n \<le> m")
```
```   288   case True
```
```   289   then have "m - n + n * 2 = m + n" by (simp add: mult_2_right)
```
```   290   moreover have "even (m - n) \<longleftrightarrow> even (m - n + n * 2)" by simp
```
```   291   ultimately have "even (m - n) \<longleftrightarrow> even (m + n)" by (simp only:)
```
```   292   then show ?thesis by auto
```
```   293 next
```
```   294   case False
```
```   295   then show ?thesis by simp
```
```   296 qed
```
```   297
```
```   298 lemma odd_pos:
```
```   299   "odd n \<Longrightarrow> 0 < n" for n :: nat
```
```   300   by (auto elim: oddE)
```
```   301
```
```   302 lemma Suc_double_not_eq_double:
```
```   303   "Suc (2 * m) \<noteq> 2 * n"
```
```   304 proof
```
```   305   assume "Suc (2 * m) = 2 * n"
```
```   306   moreover have "odd (Suc (2 * m))" and "even (2 * n)"
```
```   307     by simp_all
```
```   308   ultimately show False by simp
```
```   309 qed
```
```   310
```
```   311 lemma double_not_eq_Suc_double:
```
```   312   "2 * m \<noteq> Suc (2 * n)"
```
```   313   using Suc_double_not_eq_double [of n m] by simp
```
```   314
```
```   315 lemma odd_Suc_minus_one [simp]: "odd n \<Longrightarrow> Suc (n - Suc 0) = n"
```
```   316   by (auto elim: oddE)
```
```   317
```
```   318 lemma even_Suc_div_two [simp]:
```
```   319   "even n \<Longrightarrow> Suc n div 2 = n div 2"
```
```   320   using even_succ_div_two [of n] by simp
```
```   321
```
```   322 lemma odd_Suc_div_two [simp]:
```
```   323   "odd n \<Longrightarrow> Suc n div 2 = Suc (n div 2)"
```
```   324   using odd_succ_div_two [of n] by simp
```
```   325
```
```   326 lemma odd_two_times_div_two_nat [simp]:
```
```   327   assumes "odd n"
```
```   328   shows "2 * (n div 2) = n - (1 :: nat)"
```
```   329 proof -
```
```   330   from assms have "2 * (n div 2) + 1 = n"
```
```   331     by (rule odd_two_times_div_two_succ)
```
```   332   then have "Suc (2 * (n div 2)) - 1 = n - 1"
```
```   333     by simp
```
```   334   then show ?thesis
```
```   335     by simp
```
```   336 qed
```
```   337
```
```   338 lemma parity_induct [case_names zero even odd]:
```
```   339   assumes zero: "P 0"
```
```   340   assumes even: "\<And>n. P n \<Longrightarrow> P (2 * n)"
```
```   341   assumes odd: "\<And>n. P n \<Longrightarrow> P (Suc (2 * n))"
```
```   342   shows "P n"
```
```   343 proof (induct n rule: less_induct)
```
```   344   case (less n)
```
```   345   show "P n"
```
```   346   proof (cases "n = 0")
```
```   347     case True with zero show ?thesis by simp
```
```   348   next
```
```   349     case False
```
```   350     with less have hyp: "P (n div 2)" by simp
```
```   351     show ?thesis
```
```   352     proof (cases "even n")
```
```   353       case True
```
```   354       with hyp even [of "n div 2"] show ?thesis
```
```   355         by simp
```
```   356     next
```
```   357       case False
```
```   358       with hyp odd [of "n div 2"] show ?thesis
```
```   359         by simp
```
```   360     qed
```
```   361   qed
```
```   362 qed
```
```   363
```
```   364
```
```   365 subsection \<open>Parity and powers\<close>
```
```   366
```
```   367 context ring_1
```
```   368 begin
```
```   369
```
```   370 lemma power_minus_even [simp]: "even n \<Longrightarrow> (- a) ^ n = a ^ n"
```
```   371   by (auto elim: evenE)
```
```   372
```
```   373 lemma power_minus_odd [simp]: "odd n \<Longrightarrow> (- a) ^ n = - (a ^ n)"
```
```   374   by (auto elim: oddE)
```
```   375
```
```   376 lemma uminus_power_if:
```
```   377   "(- a) ^ n = (if even n then a ^ n else - (a ^ n))"
```
```   378   by auto
```
```   379
```
```   380 lemma neg_one_even_power [simp]: "even n \<Longrightarrow> (- 1) ^ n = 1"
```
```   381   by simp
```
```   382
```
```   383 lemma neg_one_odd_power [simp]: "odd n \<Longrightarrow> (- 1) ^ n = - 1"
```
```   384   by simp
```
```   385
```
```   386 lemma neg_one_power_add_eq_neg_one_power_diff: "k \<le> n \<Longrightarrow> (- 1) ^ (n + k) = (- 1) ^ (n - k)"
```
```   387   by (cases "even (n + k)") auto
```
```   388
```
```   389 end
```
```   390
```
```   391 context linordered_idom
```
```   392 begin
```
```   393
```
```   394 lemma zero_le_even_power: "even n \<Longrightarrow> 0 \<le> a ^ n"
```
```   395   by (auto elim: evenE)
```
```   396
```
```   397 lemma zero_le_odd_power: "odd n \<Longrightarrow> 0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a"
```
```   398   by (auto simp add: power_even_eq zero_le_mult_iff elim: oddE)
```
```   399
```
```   400 lemma zero_le_power_eq: "0 \<le> a ^ n \<longleftrightarrow> even n \<or> odd n \<and> 0 \<le> a"
```
```   401   by (auto simp add: zero_le_even_power zero_le_odd_power)
```
```   402
```
```   403 lemma zero_less_power_eq: "0 < a ^ n \<longleftrightarrow> n = 0 \<or> even n \<and> a \<noteq> 0 \<or> odd n \<and> 0 < a"
```
```   404 proof -
```
```   405   have [simp]: "0 = a ^ n \<longleftrightarrow> a = 0 \<and> n > 0"
```
```   406     unfolding power_eq_0_iff [of a n, symmetric] by blast
```
```   407   show ?thesis
```
```   408     unfolding less_le zero_le_power_eq by auto
```
```   409 qed
```
```   410
```
```   411 lemma power_less_zero_eq [simp]: "a ^ n < 0 \<longleftrightarrow> odd n \<and> a < 0"
```
```   412   unfolding not_le [symmetric] zero_le_power_eq by auto
```
```   413
```
```   414 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)"
```
```   415   unfolding not_less [symmetric] zero_less_power_eq by auto
```
```   416
```
```   417 lemma power_even_abs: "even n \<Longrightarrow> \<bar>a\<bar> ^ n = a ^ n"
```
```   418   using power_abs [of a n] by (simp add: zero_le_even_power)
```
```   419
```
```   420 lemma power_mono_even:
```
```   421   assumes "even n" and "\<bar>a\<bar> \<le> \<bar>b\<bar>"
```
```   422   shows "a ^ n \<le> b ^ n"
```
```   423 proof -
```
```   424   have "0 \<le> \<bar>a\<bar>" by auto
```
```   425   with \<open>\<bar>a\<bar> \<le> \<bar>b\<bar>\<close> have "\<bar>a\<bar> ^ n \<le> \<bar>b\<bar> ^ n"
```
```   426     by (rule power_mono)
```
```   427   with \<open>even n\<close> show ?thesis
```
```   428     by (simp add: power_even_abs)
```
```   429 qed
```
```   430
```
```   431 lemma power_mono_odd:
```
```   432   assumes "odd n" and "a \<le> b"
```
```   433   shows "a ^ n \<le> b ^ n"
```
```   434 proof (cases "b < 0")
```
```   435   case True
```
```   436   with \<open>a \<le> b\<close> have "- b \<le> - a" and "0 \<le> - b" by auto
```
```   437   then have "(- b) ^ n \<le> (- a) ^ n" by (rule power_mono)
```
```   438   with \<open>odd n\<close> show ?thesis by simp
```
```   439 next
```
```   440   case False
```
```   441   then have "0 \<le> b" by auto
```
```   442   show ?thesis
```
```   443   proof (cases "a < 0")
```
```   444     case True
```
```   445     then have "n \<noteq> 0" and "a \<le> 0" using \<open>odd n\<close> [THEN odd_pos] by auto
```
```   446     then have "a ^ n \<le> 0" unfolding power_le_zero_eq using \<open>odd n\<close> by auto
```
```   447     moreover from \<open>0 \<le> b\<close> have "0 \<le> b ^ n" by auto
```
```   448     ultimately show ?thesis by auto
```
```   449   next
```
```   450     case False
```
```   451     then have "0 \<le> a" by auto
```
```   452     with \<open>a \<le> b\<close> show ?thesis
```
```   453       using power_mono by auto
```
```   454   qed
```
```   455 qed
```
```   456
```
```   457 text \<open>Simplify, when the exponent is a numeral\<close>
```
```   458
```
```   459 lemma zero_le_power_eq_numeral [simp]:
```
```   460   "0 \<le> a ^ numeral w \<longleftrightarrow> even (numeral w :: nat) \<or> odd (numeral w :: nat) \<and> 0 \<le> a"
```
```   461   by (fact zero_le_power_eq)
```
```   462
```
```   463 lemma zero_less_power_eq_numeral [simp]:
```
```   464   "0 < a ^ numeral w \<longleftrightarrow>
```
```   465     numeral w = (0 :: nat) \<or>
```
```   466     even (numeral w :: nat) \<and> a \<noteq> 0 \<or>
```
```   467     odd (numeral w :: nat) \<and> 0 < a"
```
```   468   by (fact zero_less_power_eq)
```
```   469
```
```   470 lemma power_le_zero_eq_numeral [simp]:
```
```   471   "a ^ numeral w \<le> 0 \<longleftrightarrow>
```
```   472     (0 :: nat) < numeral w \<and>
```
```   473     (odd (numeral w :: nat) \<and> a \<le> 0 \<or> even (numeral w :: nat) \<and> a = 0)"
```
```   474   by (fact power_le_zero_eq)
```
```   475
```
```   476 lemma power_less_zero_eq_numeral [simp]:
```
```   477   "a ^ numeral w < 0 \<longleftrightarrow> odd (numeral w :: nat) \<and> a < 0"
```
```   478   by (fact power_less_zero_eq)
```
```   479
```
```   480 lemma power_even_abs_numeral [simp]:
```
```   481   "even (numeral w :: nat) \<Longrightarrow> \<bar>a\<bar> ^ numeral w = a ^ numeral w"
```
```   482   by (fact power_even_abs)
```
```   483
```
```   484 end
```
```   485
```
```   486 end
```