src/HOL/Parity.thy
author haftmann
Sun Oct 08 22:28:22 2017 +0200 (21 months ago)
changeset 66816 212a3334e7da
parent 66815 93c6632ddf44
child 66839 909ba5ed93dd
permissions -rw-r--r--
more fundamental definition of div and mod on int
     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 
   487 subsection \<open>Instance for @{typ int}\<close>
   488 
   489 instance int :: ring_parity
   490 proof
   491   fix k l :: int
   492   show "k mod 2 = 1" if "\<not> 2 dvd k"
   493   proof (rule order_antisym)
   494     have "0 \<le> k mod 2" and "k mod 2 < 2"
   495       by auto
   496     moreover have "k mod 2 \<noteq> 0"
   497       using that by (simp add: dvd_eq_mod_eq_0)
   498     ultimately have "0 < k mod 2"
   499       by (simp only: less_le) simp
   500     then show "1 \<le> k mod 2"
   501       by simp
   502     from \<open>k mod 2 < 2\<close> show "k mod 2 \<le> 1"
   503       by (simp only: less_le) simp
   504   qed
   505 qed (simp_all add: dvd_eq_mod_eq_0 divide_int_def)
   506 
   507 lemma even_diff_iff [simp]:
   508   "even (k - l) \<longleftrightarrow> even (k + l)" for k l :: int
   509   using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: mult_2_right)
   510 
   511 lemma even_abs_add_iff [simp]:
   512   "even (\<bar>k\<bar> + l) \<longleftrightarrow> even (k + l)" for k l :: int
   513   by (cases "k \<ge> 0") (simp_all add: ac_simps)
   514 
   515 lemma even_add_abs_iff [simp]:
   516   "even (k + \<bar>l\<bar>) \<longleftrightarrow> even (k + l)" for k l :: int
   517   using even_abs_add_iff [of l k] by (simp add: ac_simps)
   518 
   519 lemma even_nat_iff: "0 \<le> k \<Longrightarrow> even (nat k) \<longleftrightarrow> even k"
   520   by (simp add: even_of_nat [of "nat k", where ?'a = int, symmetric])
   521 
   522 end