src/HOL/Parity.thy
author haftmann
Fri Jun 14 08:34:27 2019 +0000 (2 months ago)
changeset 70338 c832d431636b
parent 70226 accbd801fefa
child 70339 e939ea997f5f
permissions -rw-r--r--
slightly more stringent ordering of theorems
wenzelm@41959
     1
(*  Title:      HOL/Parity.thy
wenzelm@41959
     2
    Author:     Jeremy Avigad
wenzelm@41959
     3
    Author:     Jacques D. Fleuriot
wenzelm@21256
     4
*)
wenzelm@21256
     5
wenzelm@60758
     6
section \<open>Parity in rings and semirings\<close>
wenzelm@21256
     7
wenzelm@21256
     8
theory Parity
haftmann@66815
     9
  imports Euclidean_Division
wenzelm@21256
    10
begin
wenzelm@21256
    11
wenzelm@61799
    12
subsection \<open>Ring structures with parity and \<open>even\<close>/\<open>odd\<close> predicates\<close>
haftmann@58678
    13
haftmann@67905
    14
class semiring_parity = semidom + semiring_char_0 + unique_euclidean_semiring +
haftmann@66815
    15
  assumes of_nat_div: "of_nat (m div n) = of_nat m div of_nat n"
haftmann@66839
    16
    and division_segment_of_nat [simp]: "division_segment (of_nat n) = 1"
haftmann@66839
    17
    and division_segment_euclidean_size [simp]: "division_segment a * of_nat (euclidean_size a) = a"
haftmann@66839
    18
begin
haftmann@66839
    19
haftmann@66839
    20
lemma division_segment_eq_iff:
haftmann@66839
    21
  "a = b" if "division_segment a = division_segment b"
haftmann@66839
    22
    and "euclidean_size a = euclidean_size b"
haftmann@66839
    23
  using that division_segment_euclidean_size [of a] by simp
haftmann@66839
    24
haftmann@66839
    25
lemma euclidean_size_of_nat [simp]:
haftmann@66839
    26
  "euclidean_size (of_nat n) = n"
haftmann@66839
    27
proof -
haftmann@66839
    28
  have "division_segment (of_nat n) * of_nat (euclidean_size (of_nat n)) = of_nat n"
haftmann@66839
    29
    by (fact division_segment_euclidean_size)
haftmann@66839
    30
  then show ?thesis by simp
haftmann@66839
    31
qed
haftmann@66815
    32
haftmann@66839
    33
lemma of_nat_euclidean_size:
haftmann@66839
    34
  "of_nat (euclidean_size a) = a div division_segment a"
haftmann@66839
    35
proof -
haftmann@66839
    36
  have "of_nat (euclidean_size a) = division_segment a * of_nat (euclidean_size a) div division_segment a"
haftmann@66839
    37
    by (subst nonzero_mult_div_cancel_left) simp_all
haftmann@66839
    38
  also have "\<dots> = a div division_segment a"
haftmann@66839
    39
    by simp
haftmann@66839
    40
  finally show ?thesis .
haftmann@66839
    41
qed
haftmann@66839
    42
haftmann@66839
    43
lemma division_segment_1 [simp]:
haftmann@66839
    44
  "division_segment 1 = 1"
haftmann@66839
    45
  using division_segment_of_nat [of 1] by simp
haftmann@66839
    46
haftmann@66839
    47
lemma division_segment_numeral [simp]:
haftmann@66839
    48
  "division_segment (numeral k) = 1"
haftmann@66839
    49
  using division_segment_of_nat [of "numeral k"] by simp
haftmann@66839
    50
haftmann@66839
    51
lemma euclidean_size_1 [simp]:
haftmann@66839
    52
  "euclidean_size 1 = 1"
haftmann@66839
    53
  using euclidean_size_of_nat [of 1] by simp
haftmann@66839
    54
haftmann@66839
    55
lemma euclidean_size_numeral [simp]:
haftmann@66839
    56
  "euclidean_size (numeral k) = numeral k"
haftmann@66839
    57
  using euclidean_size_of_nat [of "numeral k"] by simp
wenzelm@21256
    58
haftmann@66815
    59
lemma of_nat_dvd_iff:
haftmann@66815
    60
  "of_nat m dvd of_nat n \<longleftrightarrow> m dvd n" (is "?P \<longleftrightarrow> ?Q")
haftmann@66815
    61
proof (cases "m = 0")
haftmann@66815
    62
  case True
haftmann@66815
    63
  then show ?thesis
haftmann@66815
    64
    by simp
haftmann@66815
    65
next
haftmann@66815
    66
  case False
haftmann@66815
    67
  show ?thesis
haftmann@66815
    68
  proof
haftmann@66815
    69
    assume ?Q
haftmann@66815
    70
    then show ?P
haftmann@66815
    71
      by (auto elim: dvd_class.dvdE)
haftmann@66815
    72
  next
haftmann@66815
    73
    assume ?P
haftmann@66815
    74
    with False have "of_nat n = of_nat n div of_nat m * of_nat m"
haftmann@66815
    75
      by simp
haftmann@66815
    76
    then have "of_nat n = of_nat (n div m * m)"
haftmann@66815
    77
      by (simp add: of_nat_div)
haftmann@66815
    78
    then have "n = n div m * m"
haftmann@66815
    79
      by (simp only: of_nat_eq_iff)
haftmann@66815
    80
    then have "n = m * (n div m)"
haftmann@66815
    81
      by (simp add: ac_simps)
haftmann@66815
    82
    then show ?Q ..
haftmann@66815
    83
  qed
haftmann@66815
    84
qed
haftmann@66815
    85
haftmann@66815
    86
lemma of_nat_mod:
haftmann@66815
    87
  "of_nat (m mod n) = of_nat m mod of_nat n"
haftmann@66815
    88
proof -
haftmann@66815
    89
  have "of_nat m div of_nat n * of_nat n + of_nat m mod of_nat n = of_nat m"
haftmann@66815
    90
    by (simp add: div_mult_mod_eq)
haftmann@66815
    91
  also have "of_nat m = of_nat (m div n * n + m mod n)"
haftmann@66815
    92
    by simp
haftmann@66815
    93
  finally show ?thesis
haftmann@66815
    94
    by (simp only: of_nat_div of_nat_mult of_nat_add) simp
haftmann@66815
    95
qed
haftmann@66815
    96
haftmann@66815
    97
lemma one_div_two_eq_zero [simp]:
haftmann@66815
    98
  "1 div 2 = 0"
haftmann@66815
    99
proof -
haftmann@66815
   100
  from of_nat_div [symmetric] have "of_nat 1 div of_nat 2 = of_nat 0"
haftmann@66815
   101
    by (simp only:) simp
haftmann@66815
   102
  then show ?thesis
haftmann@66815
   103
    by simp
haftmann@66815
   104
qed
haftmann@66815
   105
haftmann@66815
   106
lemma one_mod_two_eq_one [simp]:
haftmann@66815
   107
  "1 mod 2 = 1"
haftmann@66815
   108
proof -
haftmann@66815
   109
  from of_nat_mod [symmetric] have "of_nat 1 mod of_nat 2 = of_nat 1"
haftmann@66815
   110
    by (simp only:) simp
haftmann@66815
   111
  then show ?thesis
haftmann@66815
   112
    by simp
haftmann@66815
   113
qed
haftmann@59816
   114
haftmann@58740
   115
abbreviation even :: "'a \<Rightarrow> bool"
wenzelm@63654
   116
  where "even a \<equiv> 2 dvd a"
haftmann@54228
   117
haftmann@58678
   118
abbreviation odd :: "'a \<Rightarrow> bool"
wenzelm@63654
   119
  where "odd a \<equiv> \<not> 2 dvd a"
haftmann@58678
   120
haftmann@66815
   121
lemma even_iff_mod_2_eq_zero:
haftmann@66815
   122
  "even a \<longleftrightarrow> a mod 2 = 0"
haftmann@66815
   123
  by (fact dvd_eq_mod_eq_0)
haftmann@66815
   124
haftmann@66815
   125
lemma odd_iff_mod_2_eq_one:
haftmann@66815
   126
  "odd a \<longleftrightarrow> a mod 2 = 1"
haftmann@66839
   127
proof
haftmann@66839
   128
  assume "a mod 2 = 1"
haftmann@66839
   129
  then show "odd a"
haftmann@66839
   130
    by auto
haftmann@66839
   131
next
haftmann@66839
   132
  assume "odd a"
haftmann@66839
   133
  have eucl: "euclidean_size (a mod 2) = 1"
haftmann@66839
   134
  proof (rule order_antisym)
haftmann@66839
   135
    show "euclidean_size (a mod 2) \<le> 1"
haftmann@66839
   136
      using mod_size_less [of 2 a] by simp
haftmann@66839
   137
    show "1 \<le> euclidean_size (a mod 2)"
haftmann@66840
   138
      using \<open>odd a\<close> by (simp add: Suc_le_eq dvd_eq_mod_eq_0)
haftmann@66839
   139
  qed 
haftmann@66839
   140
  from \<open>odd a\<close> have "\<not> of_nat 2 dvd division_segment a * of_nat (euclidean_size a)"
haftmann@66839
   141
    by simp
haftmann@66839
   142
  then have "\<not> of_nat 2 dvd of_nat (euclidean_size a)"
haftmann@66839
   143
    by (auto simp only: dvd_mult_unit_iff' is_unit_division_segment)
haftmann@66839
   144
  then have "\<not> 2 dvd euclidean_size a"
haftmann@66839
   145
    using of_nat_dvd_iff [of 2] by simp
haftmann@66839
   146
  then have "euclidean_size a mod 2 = 1"
haftmann@66839
   147
    by (simp add: semidom_modulo_class.dvd_eq_mod_eq_0)
haftmann@66839
   148
  then have "of_nat (euclidean_size a mod 2) = of_nat 1"
haftmann@66839
   149
    by simp
haftmann@66839
   150
  then have "of_nat (euclidean_size a) mod 2 = 1"
haftmann@66839
   151
    by (simp add: of_nat_mod)
haftmann@66839
   152
  from \<open>odd a\<close> eucl
haftmann@66839
   153
  show "a mod 2 = 1"
haftmann@66839
   154
    by (auto intro: division_segment_eq_iff simp add: division_segment_mod)
haftmann@66839
   155
qed
haftmann@58787
   156
nipkow@69198
   157
lemma mod2_eq_if: "x mod 2 = (if even x then 0 else 1)"
nipkow@69198
   158
by (simp add: odd_iff_mod_2_eq_one)
nipkow@69198
   159
haftmann@66815
   160
lemma parity_cases [case_names even odd]:
haftmann@66815
   161
  assumes "even a \<Longrightarrow> a mod 2 = 0 \<Longrightarrow> P"
haftmann@66815
   162
  assumes "odd a \<Longrightarrow> a mod 2 = 1 \<Longrightarrow> P"
haftmann@66815
   163
  shows P
haftmann@66815
   164
  using assms by (cases "even a") (simp_all add: odd_iff_mod_2_eq_one)
haftmann@66815
   165
haftmann@66815
   166
lemma not_mod_2_eq_1_eq_0 [simp]:
haftmann@66815
   167
  "a mod 2 \<noteq> 1 \<longleftrightarrow> a mod 2 = 0"
haftmann@66815
   168
  by (cases a rule: parity_cases) simp_all
haftmann@66815
   169
haftmann@66815
   170
lemma not_mod_2_eq_0_eq_1 [simp]:
haftmann@66815
   171
  "a mod 2 \<noteq> 0 \<longleftrightarrow> a mod 2 = 1"
haftmann@66815
   172
  by (cases a rule: parity_cases) simp_all
haftmann@58787
   173
haftmann@58690
   174
lemma evenE [elim?]:
haftmann@58690
   175
  assumes "even a"
haftmann@58690
   176
  obtains b where "a = 2 * b"
haftmann@58740
   177
  using assms by (rule dvdE)
haftmann@58690
   178
haftmann@58681
   179
lemma oddE [elim?]:
haftmann@58680
   180
  assumes "odd a"
haftmann@58680
   181
  obtains b where "a = 2 * b + 1"
haftmann@58787
   182
proof -
haftmann@66815
   183
  have "a = 2 * (a div 2) + a mod 2"
haftmann@66815
   184
    by (simp add: mult_div_mod_eq)
haftmann@66815
   185
  with assms have "a = 2 * (a div 2) + 1"
haftmann@66815
   186
    by (simp add: odd_iff_mod_2_eq_one)
haftmann@66815
   187
  then show ?thesis ..
haftmann@66815
   188
qed
haftmann@66815
   189
haftmann@66815
   190
lemma mod_2_eq_odd:
haftmann@66815
   191
  "a mod 2 = of_bool (odd a)"
haftmann@66815
   192
  by (auto elim: oddE)
haftmann@66815
   193
haftmann@67816
   194
lemma of_bool_odd_eq_mod_2:
haftmann@67816
   195
  "of_bool (odd a) = a mod 2"
haftmann@67816
   196
  by (simp add: mod_2_eq_odd)
haftmann@67816
   197
haftmann@66815
   198
lemma one_mod_2_pow_eq [simp]:
haftmann@66815
   199
  "1 mod (2 ^ n) = of_bool (n > 0)"
haftmann@66815
   200
proof -
haftmann@67083
   201
  have "1 mod (2 ^ n) = of_nat (1 mod (2 ^ n))"
haftmann@67083
   202
    using of_nat_mod [of 1 "2 ^ n"] by simp
haftmann@67083
   203
  also have "\<dots> = of_bool (n > 0)"
haftmann@66815
   204
    by simp
haftmann@67083
   205
  finally show ?thesis .
haftmann@66815
   206
qed
haftmann@66815
   207
haftmann@67816
   208
lemma one_div_2_pow_eq [simp]:
haftmann@67816
   209
  "1 div (2 ^ n) = of_bool (n = 0)"
haftmann@67816
   210
  using div_mult_mod_eq [of 1 "2 ^ n"] by auto
haftmann@67816
   211
haftmann@66815
   212
lemma even_of_nat [simp]:
haftmann@66815
   213
  "even (of_nat a) \<longleftrightarrow> even a"
haftmann@66815
   214
proof -
haftmann@66815
   215
  have "even (of_nat a) \<longleftrightarrow> of_nat 2 dvd of_nat a"
haftmann@66815
   216
    by simp
haftmann@66815
   217
  also have "\<dots> \<longleftrightarrow> even a"
haftmann@66815
   218
    by (simp only: of_nat_dvd_iff)
haftmann@66815
   219
  finally show ?thesis .
haftmann@66815
   220
qed
haftmann@66815
   221
haftmann@66815
   222
lemma even_zero [simp]:
haftmann@66815
   223
  "even 0"
haftmann@66815
   224
  by (fact dvd_0_right)
haftmann@66815
   225
haftmann@66815
   226
lemma odd_one [simp]:
haftmann@66815
   227
  "odd 1"
haftmann@66815
   228
proof -
haftmann@66815
   229
  have "\<not> (2 :: nat) dvd 1"
haftmann@66815
   230
    by simp
haftmann@66815
   231
  then have "\<not> of_nat 2 dvd of_nat 1"
haftmann@66815
   232
    unfolding of_nat_dvd_iff by simp
haftmann@66815
   233
  then show ?thesis
haftmann@66815
   234
    by simp
haftmann@58787
   235
qed
wenzelm@63654
   236
haftmann@66815
   237
lemma odd_even_add:
haftmann@66815
   238
  "even (a + b)" if "odd a" and "odd b"
haftmann@66815
   239
proof -
haftmann@66815
   240
  from that obtain c d where "a = 2 * c + 1" and "b = 2 * d + 1"
haftmann@66815
   241
    by (blast elim: oddE)
haftmann@66815
   242
  then have "a + b = 2 * c + 2 * d + (1 + 1)"
haftmann@66815
   243
    by (simp only: ac_simps)
haftmann@66815
   244
  also have "\<dots> = 2 * (c + d + 1)"
haftmann@66815
   245
    by (simp add: algebra_simps)
haftmann@66815
   246
  finally show ?thesis ..
haftmann@66815
   247
qed
haftmann@66815
   248
haftmann@66815
   249
lemma even_add [simp]:
haftmann@66815
   250
  "even (a + b) \<longleftrightarrow> (even a \<longleftrightarrow> even b)"
haftmann@66815
   251
  by (auto simp add: dvd_add_right_iff dvd_add_left_iff odd_even_add)
haftmann@66815
   252
haftmann@66815
   253
lemma odd_add [simp]:
haftmann@66815
   254
  "odd (a + b) \<longleftrightarrow> \<not> (odd a \<longleftrightarrow> odd b)"
haftmann@66815
   255
  by simp
haftmann@66815
   256
haftmann@66815
   257
lemma even_plus_one_iff [simp]:
haftmann@66815
   258
  "even (a + 1) \<longleftrightarrow> odd a"
haftmann@66815
   259
  by (auto simp add: dvd_add_right_iff intro: odd_even_add)
haftmann@66815
   260
haftmann@66815
   261
lemma even_mult_iff [simp]:
haftmann@66815
   262
  "even (a * b) \<longleftrightarrow> even a \<or> even b" (is "?P \<longleftrightarrow> ?Q")
haftmann@66815
   263
proof
haftmann@66815
   264
  assume ?Q
haftmann@66815
   265
  then show ?P
haftmann@66815
   266
    by auto
haftmann@66815
   267
next
haftmann@66815
   268
  assume ?P
haftmann@66815
   269
  show ?Q
haftmann@66815
   270
  proof (rule ccontr)
haftmann@66815
   271
    assume "\<not> (even a \<or> even b)"
haftmann@66815
   272
    then have "odd a" and "odd b"
haftmann@66815
   273
      by auto
haftmann@66815
   274
    then obtain r s where "a = 2 * r + 1" and "b = 2 * s + 1"
haftmann@66815
   275
      by (blast elim: oddE)
haftmann@66815
   276
    then have "a * b = (2 * r + 1) * (2 * s + 1)"
haftmann@66815
   277
      by simp
haftmann@66815
   278
    also have "\<dots> = 2 * (2 * r * s + r + s) + 1"
haftmann@66815
   279
      by (simp add: algebra_simps)
haftmann@66815
   280
    finally have "odd (a * b)"
haftmann@66815
   281
      by simp
haftmann@66815
   282
    with \<open>?P\<close> show False
haftmann@66815
   283
      by auto
haftmann@66815
   284
  qed
haftmann@66815
   285
qed
haftmann@58678
   286
wenzelm@63654
   287
lemma even_numeral [simp]: "even (numeral (Num.Bit0 n))"
haftmann@58678
   288
proof -
haftmann@58678
   289
  have "even (2 * numeral n)"
haftmann@66815
   290
    unfolding even_mult_iff by simp
haftmann@58678
   291
  then have "even (numeral n + numeral n)"
haftmann@58678
   292
    unfolding mult_2 .
haftmann@58678
   293
  then show ?thesis
haftmann@58678
   294
    unfolding numeral.simps .
haftmann@58678
   295
qed
haftmann@58678
   296
wenzelm@63654
   297
lemma odd_numeral [simp]: "odd (numeral (Num.Bit1 n))"
haftmann@58678
   298
proof
haftmann@58678
   299
  assume "even (numeral (num.Bit1 n))"
haftmann@58678
   300
  then have "even (numeral n + numeral n + 1)"
haftmann@58678
   301
    unfolding numeral.simps .
haftmann@58678
   302
  then have "even (2 * numeral n + 1)"
haftmann@58678
   303
    unfolding mult_2 .
haftmann@58678
   304
  then have "2 dvd numeral n * 2 + 1"
haftmann@58740
   305
    by (simp add: ac_simps)
wenzelm@63654
   306
  then have "2 dvd 1"
wenzelm@63654
   307
    using dvd_add_times_triv_left_iff [of 2 "numeral n" 1] by simp
haftmann@58678
   308
  then show False by simp
haftmann@58678
   309
qed
haftmann@58678
   310
wenzelm@63654
   311
lemma even_power [simp]: "even (a ^ n) \<longleftrightarrow> even a \<and> n > 0"
haftmann@58680
   312
  by (induct n) auto
haftmann@58680
   313
haftmann@66815
   314
lemma even_succ_div_two [simp]:
haftmann@66815
   315
  "even a \<Longrightarrow> (a + 1) div 2 = a div 2"
haftmann@66815
   316
  by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero)
haftmann@66815
   317
haftmann@66815
   318
lemma odd_succ_div_two [simp]:
haftmann@66815
   319
  "odd a \<Longrightarrow> (a + 1) div 2 = a div 2 + 1"
haftmann@66815
   320
  by (auto elim!: oddE simp add: add.assoc)
haftmann@66815
   321
haftmann@66815
   322
lemma even_two_times_div_two:
haftmann@66815
   323
  "even a \<Longrightarrow> 2 * (a div 2) = a"
haftmann@66815
   324
  by (fact dvd_mult_div_cancel)
haftmann@66815
   325
haftmann@66815
   326
lemma odd_two_times_div_two_succ [simp]:
haftmann@66815
   327
  "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
haftmann@66815
   328
  using mult_div_mod_eq [of 2 a]
haftmann@66815
   329
  by (simp add: even_iff_mod_2_eq_zero)
haftmann@66815
   330
haftmann@67051
   331
lemma coprime_left_2_iff_odd [simp]:
haftmann@67051
   332
  "coprime 2 a \<longleftrightarrow> odd a"
haftmann@67051
   333
proof
haftmann@67051
   334
  assume "odd a"
haftmann@67051
   335
  show "coprime 2 a"
haftmann@67051
   336
  proof (rule coprimeI)
haftmann@67051
   337
    fix b
haftmann@67051
   338
    assume "b dvd 2" "b dvd a"
haftmann@67051
   339
    then have "b dvd a mod 2"
haftmann@67051
   340
      by (auto intro: dvd_mod)
haftmann@67051
   341
    with \<open>odd a\<close> show "is_unit b"
haftmann@67051
   342
      by (simp add: mod_2_eq_odd)
haftmann@67051
   343
  qed
haftmann@67051
   344
next
haftmann@67051
   345
  assume "coprime 2 a"
haftmann@67051
   346
  show "odd a"
haftmann@67051
   347
  proof (rule notI)
haftmann@67051
   348
    assume "even a"
haftmann@67051
   349
    then obtain b where "a = 2 * b" ..
haftmann@67051
   350
    with \<open>coprime 2 a\<close> have "coprime 2 (2 * b)"
haftmann@67051
   351
      by simp
haftmann@67051
   352
    moreover have "\<not> coprime 2 (2 * b)"
haftmann@67051
   353
      by (rule not_coprimeI [of 2]) simp_all
haftmann@67051
   354
    ultimately show False
haftmann@67051
   355
      by blast
haftmann@67051
   356
  qed
haftmann@67051
   357
qed
haftmann@67051
   358
haftmann@67051
   359
lemma coprime_right_2_iff_odd [simp]:
haftmann@67051
   360
  "coprime a 2 \<longleftrightarrow> odd a"
haftmann@67051
   361
  using coprime_left_2_iff_odd [of a] by (simp add: ac_simps)
haftmann@67051
   362
haftmann@67828
   363
lemma div_mult2_eq':
haftmann@67828
   364
  "a div (of_nat m * of_nat n) = a div of_nat m div of_nat n"
haftmann@67828
   365
proof (cases a "of_nat m * of_nat n" rule: divmod_cases)
haftmann@67828
   366
  case (divides q)
haftmann@67828
   367
  then show ?thesis
haftmann@67828
   368
    using nonzero_mult_div_cancel_right [of "of_nat m" "q * of_nat n"]
haftmann@67828
   369
    by (simp add: ac_simps)
haftmann@67828
   370
next
haftmann@67828
   371
  case (remainder q r)
haftmann@67828
   372
  then have "division_segment r = 1"
haftmann@67828
   373
    using division_segment_of_nat [of "m * n"] by simp
haftmann@67828
   374
  with division_segment_euclidean_size [of r]
haftmann@67828
   375
  have "of_nat (euclidean_size r) = r"
haftmann@67828
   376
    by simp
haftmann@67908
   377
  have "a mod (of_nat m * of_nat n) div (of_nat m * of_nat n) = 0"
haftmann@67908
   378
    by simp
haftmann@67908
   379
  with remainder(6) have "r div (of_nat m * of_nat n) = 0"
haftmann@67828
   380
    by simp
haftmann@67908
   381
  with \<open>of_nat (euclidean_size r) = r\<close>
haftmann@67908
   382
  have "of_nat (euclidean_size r) div (of_nat m * of_nat n) = 0"
haftmann@67908
   383
    by simp
haftmann@67908
   384
  then have "of_nat (euclidean_size r div (m * n)) = 0"
haftmann@67828
   385
    by (simp add: of_nat_div)
haftmann@67908
   386
  then have "of_nat (euclidean_size r div m div n) = 0"
haftmann@67908
   387
    by (simp add: div_mult2_eq)
haftmann@67908
   388
  with \<open>of_nat (euclidean_size r) = r\<close> have "r div of_nat m div of_nat n = 0"
haftmann@67908
   389
    by (simp add: of_nat_div)
haftmann@67828
   390
  with remainder(1)
haftmann@67828
   391
  have "q = (r div of_nat m + q * of_nat n * of_nat m div of_nat m) div of_nat n"
haftmann@67828
   392
    by simp
haftmann@67908
   393
  with remainder(5) remainder(7) show ?thesis
haftmann@67828
   394
    using div_plus_div_distrib_dvd_right [of "of_nat m" "q * (of_nat m * of_nat n)" r]
haftmann@67828
   395
    by (simp add: ac_simps)
haftmann@67828
   396
next
haftmann@67828
   397
  case by0
haftmann@67828
   398
  then show ?thesis
haftmann@67828
   399
    by auto
haftmann@67828
   400
qed
haftmann@67828
   401
haftmann@67828
   402
lemma mod_mult2_eq':
haftmann@67828
   403
  "a mod (of_nat m * of_nat n) = of_nat m * (a div of_nat m mod of_nat n) + a mod of_nat m"
haftmann@67828
   404
proof -
haftmann@67828
   405
  have "a div (of_nat m * of_nat n) * (of_nat m * of_nat n) + a mod (of_nat m * of_nat n) = a div of_nat m div of_nat n * of_nat n * of_nat m + (a div of_nat m mod of_nat n * of_nat m + a mod of_nat m)"
haftmann@67828
   406
    by (simp add: combine_common_factor div_mult_mod_eq)
haftmann@67828
   407
  moreover have "a div of_nat m div of_nat n * of_nat n * of_nat m = of_nat n * of_nat m * (a div of_nat m div of_nat n)"
haftmann@67828
   408
    by (simp add: ac_simps)
haftmann@67828
   409
  ultimately show ?thesis
haftmann@67828
   410
    by (simp add: div_mult2_eq' mult_commute)
haftmann@67828
   411
qed
haftmann@67828
   412
haftmann@68028
   413
lemma div_mult2_numeral_eq:
haftmann@68028
   414
  "a div numeral k div numeral l = a div numeral (k * l)" (is "?A = ?B")
haftmann@68028
   415
proof -
haftmann@68028
   416
  have "?A = a div of_nat (numeral k) div of_nat (numeral l)"
haftmann@68028
   417
    by simp
haftmann@68028
   418
  also have "\<dots> = a div (of_nat (numeral k) * of_nat (numeral l))"
haftmann@68028
   419
    by (fact div_mult2_eq' [symmetric])
haftmann@68028
   420
  also have "\<dots> = ?B"
haftmann@68028
   421
    by simp
haftmann@68028
   422
  finally show ?thesis .
haftmann@68028
   423
qed
haftmann@68028
   424
haftmann@58678
   425
end
haftmann@58678
   426
haftmann@59816
   427
class ring_parity = ring + semiring_parity
haftmann@58679
   428
begin
haftmann@58679
   429
haftmann@59816
   430
subclass comm_ring_1 ..
haftmann@59816
   431
haftmann@67816
   432
lemma even_minus:
haftmann@66815
   433
  "even (- a) \<longleftrightarrow> even a"
haftmann@58740
   434
  by (fact dvd_minus_iff)
haftmann@58679
   435
haftmann@66815
   436
lemma even_diff [simp]:
haftmann@66815
   437
  "even (a - b) \<longleftrightarrow> even (a + b)"
haftmann@58680
   438
  using even_add [of a "- b"] by simp
haftmann@58680
   439
haftmann@67906
   440
lemma minus_1_mod_2_eq [simp]:
haftmann@67906
   441
  "- 1 mod 2 = 1"
haftmann@67906
   442
  by (simp add: mod_2_eq_odd)
haftmann@67906
   443
haftmann@67906
   444
lemma minus_1_div_2_eq [simp]:
haftmann@67906
   445
  "- 1 div 2 = - 1"
haftmann@67906
   446
proof -
haftmann@67906
   447
  from div_mult_mod_eq [of "- 1" 2]
haftmann@67906
   448
  have "- 1 div 2 * 2 = - 1 * 2"
haftmann@67906
   449
    using local.add_implies_diff by fastforce
haftmann@67906
   450
  then show ?thesis
haftmann@67906
   451
    using mult_right_cancel [of 2 "- 1 div 2" "- 1"] by simp
haftmann@67906
   452
qed
haftmann@67906
   453
haftmann@58679
   454
end
haftmann@58679
   455
haftmann@66808
   456
wenzelm@69593
   457
subsection \<open>Instance for \<^typ>\<open>nat\<close>\<close>
haftmann@66808
   458
haftmann@66815
   459
instance nat :: semiring_parity
haftmann@66815
   460
  by standard (simp_all add: dvd_eq_mod_eq_0)
haftmann@66808
   461
haftmann@66815
   462
lemma even_Suc_Suc_iff [simp]:
haftmann@66815
   463
  "even (Suc (Suc n)) \<longleftrightarrow> even n"
haftmann@58787
   464
  using dvd_add_triv_right_iff [of 2 n] by simp
haftmann@58687
   465
haftmann@66815
   466
lemma even_Suc [simp]: "even (Suc n) \<longleftrightarrow> odd n"
haftmann@66815
   467
  using even_plus_one_iff [of n] by simp
haftmann@58787
   468
haftmann@66815
   469
lemma even_diff_nat [simp]:
haftmann@66815
   470
  "even (m - n) \<longleftrightarrow> m < n \<or> even (m + n)" for m n :: nat
haftmann@58787
   471
proof (cases "n \<le> m")
haftmann@58787
   472
  case True
haftmann@58787
   473
  then have "m - n + n * 2 = m + n" by (simp add: mult_2_right)
haftmann@66815
   474
  moreover have "even (m - n) \<longleftrightarrow> even (m - n + n * 2)" by simp
haftmann@66815
   475
  ultimately have "even (m - n) \<longleftrightarrow> even (m + n)" by (simp only:)
haftmann@58787
   476
  then show ?thesis by auto
haftmann@58787
   477
next
haftmann@58787
   478
  case False
haftmann@58787
   479
  then show ?thesis by simp
wenzelm@63654
   480
qed
wenzelm@63654
   481
haftmann@66815
   482
lemma odd_pos:
haftmann@66815
   483
  "odd n \<Longrightarrow> 0 < n" for n :: nat
haftmann@58690
   484
  by (auto elim: oddE)
haftmann@60343
   485
haftmann@66815
   486
lemma Suc_double_not_eq_double:
haftmann@66815
   487
  "Suc (2 * m) \<noteq> 2 * n"
haftmann@62597
   488
proof
haftmann@62597
   489
  assume "Suc (2 * m) = 2 * n"
haftmann@62597
   490
  moreover have "odd (Suc (2 * m))" and "even (2 * n)"
haftmann@62597
   491
    by simp_all
haftmann@62597
   492
  ultimately show False by simp
haftmann@62597
   493
qed
haftmann@62597
   494
haftmann@66815
   495
lemma double_not_eq_Suc_double:
haftmann@66815
   496
  "2 * m \<noteq> Suc (2 * n)"
haftmann@62597
   497
  using Suc_double_not_eq_double [of n m] by simp
haftmann@62597
   498
haftmann@66815
   499
lemma odd_Suc_minus_one [simp]: "odd n \<Longrightarrow> Suc (n - Suc 0) = n"
haftmann@66815
   500
  by (auto elim: oddE)
haftmann@60343
   501
haftmann@66815
   502
lemma even_Suc_div_two [simp]:
haftmann@66815
   503
  "even n \<Longrightarrow> Suc n div 2 = n div 2"
haftmann@66815
   504
  using even_succ_div_two [of n] by simp
haftmann@60343
   505
haftmann@66815
   506
lemma odd_Suc_div_two [simp]:
haftmann@66815
   507
  "odd n \<Longrightarrow> Suc n div 2 = Suc (n div 2)"
haftmann@66815
   508
  using odd_succ_div_two [of n] by simp
haftmann@60343
   509
haftmann@66815
   510
lemma odd_two_times_div_two_nat [simp]:
haftmann@66815
   511
  assumes "odd n"
haftmann@66815
   512
  shows "2 * (n div 2) = n - (1 :: nat)"
haftmann@66815
   513
proof -
haftmann@66815
   514
  from assms have "2 * (n div 2) + 1 = n"
haftmann@66815
   515
    by (rule odd_two_times_div_two_succ)
haftmann@66815
   516
  then have "Suc (2 * (n div 2)) - 1 = n - 1"
haftmann@58787
   517
    by simp
haftmann@66815
   518
  then show ?thesis
haftmann@66815
   519
    by simp
haftmann@58787
   520
qed
haftmann@58680
   521
haftmann@70226
   522
lemma nat_parity_induct [case_names zero even odd]:
haftmann@70226
   523
  "P n" if zero: "P 0"
haftmann@70226
   524
    and even: "\<And>n. P n \<Longrightarrow> n > 0 \<Longrightarrow> P (2 * n)"
haftmann@70226
   525
    and odd: "\<And>n. P n \<Longrightarrow> P (Suc (2 * n))"
haftmann@70226
   526
proof (induction n rule: less_induct)
haftmann@66815
   527
  case (less n)
haftmann@66815
   528
  show "P n"
haftmann@66815
   529
  proof (cases "n = 0")
haftmann@66815
   530
    case True with zero show ?thesis by simp
haftmann@66815
   531
  next
haftmann@66815
   532
    case False
haftmann@66815
   533
    with less have hyp: "P (n div 2)" by simp
haftmann@66815
   534
    show ?thesis
haftmann@66815
   535
    proof (cases "even n")
haftmann@66815
   536
      case True
haftmann@70226
   537
      then have "n \<noteq> 1"
haftmann@70226
   538
        by auto
haftmann@70226
   539
      with \<open>n \<noteq> 0\<close> have "n div 2 > 0"
haftmann@70226
   540
        by simp
haftmann@70226
   541
      with \<open>even n\<close> hyp even [of "n div 2"] show ?thesis
haftmann@66815
   542
        by simp
haftmann@66815
   543
    next
haftmann@66815
   544
      case False
haftmann@66815
   545
      with hyp odd [of "n div 2"] show ?thesis
haftmann@66815
   546
        by simp
haftmann@66815
   547
    qed
haftmann@66815
   548
  qed
haftmann@66815
   549
qed
haftmann@58687
   550
haftmann@68157
   551
lemma not_mod2_eq_Suc_0_eq_0 [simp]:
haftmann@68157
   552
  "n mod 2 \<noteq> Suc 0 \<longleftrightarrow> n mod 2 = 0"
haftmann@68157
   553
  using not_mod_2_eq_1_eq_0 [of n] by simp
haftmann@68157
   554
haftmann@69502
   555
lemma odd_card_imp_not_empty:
haftmann@69502
   556
  \<open>A \<noteq> {}\<close> if \<open>odd (card A)\<close>
haftmann@69502
   557
  using that by auto
haftmann@69502
   558
haftmann@58687
   559
wenzelm@60758
   560
subsection \<open>Parity and powers\<close>
haftmann@58689
   561
eberlm@61531
   562
context ring_1
haftmann@58689
   563
begin
haftmann@58689
   564
wenzelm@63654
   565
lemma power_minus_even [simp]: "even n \<Longrightarrow> (- a) ^ n = a ^ n"
haftmann@58690
   566
  by (auto elim: evenE)
haftmann@58689
   567
wenzelm@63654
   568
lemma power_minus_odd [simp]: "odd n \<Longrightarrow> (- a) ^ n = - (a ^ n)"
haftmann@58690
   569
  by (auto elim: oddE)
haftmann@58690
   570
haftmann@66815
   571
lemma uminus_power_if:
haftmann@66815
   572
  "(- a) ^ n = (if even n then a ^ n else - (a ^ n))"
haftmann@66815
   573
  by auto
haftmann@66815
   574
wenzelm@63654
   575
lemma neg_one_even_power [simp]: "even n \<Longrightarrow> (- 1) ^ n = 1"
haftmann@58690
   576
  by simp
haftmann@58689
   577
wenzelm@63654
   578
lemma neg_one_odd_power [simp]: "odd n \<Longrightarrow> (- 1) ^ n = - 1"
haftmann@58690
   579
  by simp
haftmann@58689
   580
bulwahn@66582
   581
lemma neg_one_power_add_eq_neg_one_power_diff: "k \<le> n \<Longrightarrow> (- 1) ^ (n + k) = (- 1) ^ (n - k)"
bulwahn@66582
   582
  by (cases "even (n + k)") auto
bulwahn@66582
   583
lp15@67371
   584
lemma minus_one_power_iff: "(- 1) ^ n = (if even n then 1 else - 1)"
lp15@67371
   585
  by (induct n) auto
lp15@67371
   586
wenzelm@63654
   587
end
haftmann@58689
   588
haftmann@58689
   589
context linordered_idom
haftmann@58689
   590
begin
haftmann@58689
   591
wenzelm@63654
   592
lemma zero_le_even_power: "even n \<Longrightarrow> 0 \<le> a ^ n"
haftmann@58690
   593
  by (auto elim: evenE)
haftmann@58689
   594
wenzelm@63654
   595
lemma zero_le_odd_power: "odd n \<Longrightarrow> 0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a"
haftmann@58689
   596
  by (auto simp add: power_even_eq zero_le_mult_iff elim: oddE)
haftmann@58689
   597
wenzelm@63654
   598
lemma zero_le_power_eq: "0 \<le> a ^ n \<longleftrightarrow> even n \<or> odd n \<and> 0 \<le> a"
haftmann@58787
   599
  by (auto simp add: zero_le_even_power zero_le_odd_power)
wenzelm@63654
   600
wenzelm@63654
   601
lemma zero_less_power_eq: "0 < a ^ n \<longleftrightarrow> n = 0 \<or> even n \<and> a \<noteq> 0 \<or> odd n \<and> 0 < a"
haftmann@58689
   602
proof -
haftmann@58689
   603
  have [simp]: "0 = a ^ n \<longleftrightarrow> a = 0 \<and> n > 0"
haftmann@58787
   604
    unfolding power_eq_0_iff [of a n, symmetric] by blast
haftmann@58689
   605
  show ?thesis
wenzelm@63654
   606
    unfolding less_le zero_le_power_eq by auto
haftmann@58689
   607
qed
haftmann@58689
   608
wenzelm@63654
   609
lemma power_less_zero_eq [simp]: "a ^ n < 0 \<longleftrightarrow> odd n \<and> a < 0"
haftmann@58689
   610
  unfolding not_le [symmetric] zero_le_power_eq by auto
haftmann@58689
   611
wenzelm@63654
   612
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)"
wenzelm@63654
   613
  unfolding not_less [symmetric] zero_less_power_eq by auto
wenzelm@63654
   614
wenzelm@63654
   615
lemma power_even_abs: "even n \<Longrightarrow> \<bar>a\<bar> ^ n = a ^ n"
haftmann@58689
   616
  using power_abs [of a n] by (simp add: zero_le_even_power)
haftmann@58689
   617
haftmann@58689
   618
lemma power_mono_even:
haftmann@58689
   619
  assumes "even n" and "\<bar>a\<bar> \<le> \<bar>b\<bar>"
haftmann@58689
   620
  shows "a ^ n \<le> b ^ n"
haftmann@58689
   621
proof -
haftmann@58689
   622
  have "0 \<le> \<bar>a\<bar>" by auto
wenzelm@63654
   623
  with \<open>\<bar>a\<bar> \<le> \<bar>b\<bar>\<close> have "\<bar>a\<bar> ^ n \<le> \<bar>b\<bar> ^ n"
wenzelm@63654
   624
    by (rule power_mono)
wenzelm@63654
   625
  with \<open>even n\<close> show ?thesis
wenzelm@63654
   626
    by (simp add: power_even_abs)
haftmann@58689
   627
qed
haftmann@58689
   628
haftmann@58689
   629
lemma power_mono_odd:
haftmann@58689
   630
  assumes "odd n" and "a \<le> b"
haftmann@58689
   631
  shows "a ^ n \<le> b ^ n"
haftmann@58689
   632
proof (cases "b < 0")
wenzelm@63654
   633
  case True
wenzelm@63654
   634
  with \<open>a \<le> b\<close> have "- b \<le> - a" and "0 \<le> - b" by auto
wenzelm@63654
   635
  then have "(- b) ^ n \<le> (- a) ^ n" by (rule power_mono)
wenzelm@60758
   636
  with \<open>odd n\<close> show ?thesis by simp
haftmann@58689
   637
next
wenzelm@63654
   638
  case False
wenzelm@63654
   639
  then have "0 \<le> b" by auto
haftmann@58689
   640
  show ?thesis
haftmann@58689
   641
  proof (cases "a < 0")
wenzelm@63654
   642
    case True
wenzelm@63654
   643
    then have "n \<noteq> 0" and "a \<le> 0" using \<open>odd n\<close> [THEN odd_pos] by auto
wenzelm@60758
   644
    then have "a ^ n \<le> 0" unfolding power_le_zero_eq using \<open>odd n\<close> by auto
wenzelm@63654
   645
    moreover from \<open>0 \<le> b\<close> have "0 \<le> b ^ n" by auto
haftmann@58689
   646
    ultimately show ?thesis by auto
haftmann@58689
   647
  next
wenzelm@63654
   648
    case False
wenzelm@63654
   649
    then have "0 \<le> a" by auto
wenzelm@63654
   650
    with \<open>a \<le> b\<close> show ?thesis
wenzelm@63654
   651
      using power_mono by auto
haftmann@58689
   652
  qed
haftmann@58689
   653
qed
hoelzl@62083
   654
wenzelm@60758
   655
text \<open>Simplify, when the exponent is a numeral\<close>
haftmann@58689
   656
haftmann@58689
   657
lemma zero_le_power_eq_numeral [simp]:
haftmann@58689
   658
  "0 \<le> a ^ numeral w \<longleftrightarrow> even (numeral w :: nat) \<or> odd (numeral w :: nat) \<and> 0 \<le> a"
haftmann@58689
   659
  by (fact zero_le_power_eq)
haftmann@58689
   660
haftmann@58689
   661
lemma zero_less_power_eq_numeral [simp]:
wenzelm@63654
   662
  "0 < a ^ numeral w \<longleftrightarrow>
wenzelm@63654
   663
    numeral w = (0 :: nat) \<or>
wenzelm@63654
   664
    even (numeral w :: nat) \<and> a \<noteq> 0 \<or>
wenzelm@63654
   665
    odd (numeral w :: nat) \<and> 0 < a"
haftmann@58689
   666
  by (fact zero_less_power_eq)
haftmann@58689
   667
haftmann@58689
   668
lemma power_le_zero_eq_numeral [simp]:
wenzelm@63654
   669
  "a ^ numeral w \<le> 0 \<longleftrightarrow>
wenzelm@63654
   670
    (0 :: nat) < numeral w \<and>
wenzelm@63654
   671
    (odd (numeral w :: nat) \<and> a \<le> 0 \<or> even (numeral w :: nat) \<and> a = 0)"
haftmann@58689
   672
  by (fact power_le_zero_eq)
haftmann@58689
   673
haftmann@58689
   674
lemma power_less_zero_eq_numeral [simp]:
haftmann@58689
   675
  "a ^ numeral w < 0 \<longleftrightarrow> odd (numeral w :: nat) \<and> a < 0"
haftmann@58689
   676
  by (fact power_less_zero_eq)
haftmann@58689
   677
haftmann@58689
   678
lemma power_even_abs_numeral [simp]:
haftmann@58689
   679
  "even (numeral w :: nat) \<Longrightarrow> \<bar>a\<bar> ^ numeral w = a ^ numeral w"
haftmann@58689
   680
  by (fact power_even_abs)
haftmann@58689
   681
haftmann@58689
   682
end
haftmann@58689
   683
haftmann@66816
   684
wenzelm@69593
   685
subsection \<open>Instance for \<^typ>\<open>int\<close>\<close>
haftmann@66816
   686
haftmann@66816
   687
instance int :: ring_parity
haftmann@66839
   688
  by standard (simp_all add: dvd_eq_mod_eq_0 divide_int_def division_segment_int_def)
haftmann@66816
   689
haftmann@67816
   690
lemma even_diff_iff:
haftmann@66816
   691
  "even (k - l) \<longleftrightarrow> even (k + l)" for k l :: int
haftmann@67816
   692
  by (fact even_diff)
haftmann@66816
   693
haftmann@67816
   694
lemma even_abs_add_iff:
haftmann@66816
   695
  "even (\<bar>k\<bar> + l) \<longleftrightarrow> even (k + l)" for k l :: int
haftmann@67816
   696
  by simp
haftmann@66816
   697
haftmann@67816
   698
lemma even_add_abs_iff:
haftmann@66816
   699
  "even (k + \<bar>l\<bar>) \<longleftrightarrow> even (k + l)" for k l :: int
haftmann@67816
   700
  by simp
haftmann@66816
   701
haftmann@66816
   702
lemma even_nat_iff: "0 \<le> k \<Longrightarrow> even (nat k) \<longleftrightarrow> even k"
haftmann@66816
   703
  by (simp add: even_of_nat [of "nat k", where ?'a = int, symmetric])
haftmann@66816
   704
haftmann@70338
   705
lemma int_parity_induct [case_names zero minus even odd]:
haftmann@70338
   706
  "P k" if zero_int: "P 0"
haftmann@70338
   707
    and minus_int: "P (- 1)"
haftmann@70338
   708
    and even_int: "\<And>k. P k \<Longrightarrow> k \<noteq> 0 \<Longrightarrow> P (k * 2)"
haftmann@70338
   709
    and odd_int: "\<And>k. P k \<Longrightarrow> k \<noteq> - 1 \<Longrightarrow> P (1 + (k * 2))" for k :: int
haftmann@70338
   710
proof (cases "k \<ge> 0")
haftmann@70338
   711
  case True
haftmann@70338
   712
  define n where "n = nat k"
haftmann@70338
   713
  with True have "k = int n"
haftmann@70338
   714
    by simp
haftmann@70338
   715
  then show "P k"
haftmann@70338
   716
  proof (induction n arbitrary: k rule: nat_parity_induct)
haftmann@70338
   717
    case zero
haftmann@70338
   718
    then show ?case
haftmann@70338
   719
      by (simp add: zero_int)
haftmann@70338
   720
  next
haftmann@70338
   721
    case (even n)
haftmann@70338
   722
    have "P (int n * 2)"
haftmann@70338
   723
      by (rule even_int) (use even in simp_all)
haftmann@70338
   724
    with even show ?case
haftmann@70338
   725
      by (simp add: ac_simps)
haftmann@70338
   726
  next
haftmann@70338
   727
    case (odd n)
haftmann@70338
   728
    have "P (1 + (int n * 2))"
haftmann@70338
   729
      by (rule odd_int) (use odd in simp_all)
haftmann@70338
   730
    with odd show ?case
haftmann@70338
   731
      by (simp add: ac_simps)
haftmann@70338
   732
  qed
haftmann@70338
   733
next
haftmann@70338
   734
  case False
haftmann@70338
   735
  define n where "n = nat (- k - 1)"
haftmann@70338
   736
  with False have "k = - int n - 1"
haftmann@70338
   737
    by simp
haftmann@70338
   738
  then show "P k"
haftmann@70338
   739
  proof (induction n arbitrary: k rule: nat_parity_induct)
haftmann@70338
   740
    case zero
haftmann@70338
   741
    then show ?case
haftmann@70338
   742
      by (simp add: minus_int)
haftmann@70338
   743
  next
haftmann@70338
   744
    case (even n)
haftmann@70338
   745
    have "P (1 + (- int (Suc n) * 2))"
haftmann@70338
   746
      by (rule odd_int) (use even in \<open>simp_all add: algebra_simps\<close>)
haftmann@70338
   747
    also have "\<dots> = - int (2 * n) - 1"
haftmann@70338
   748
      by (simp add: algebra_simps)
haftmann@70338
   749
    finally show ?case
haftmann@70338
   750
      using even by simp
haftmann@70338
   751
  next
haftmann@70338
   752
    case (odd n)
haftmann@70338
   753
    have "P (- int (Suc n) * 2)"
haftmann@70338
   754
      by (rule even_int) (use odd in \<open>simp_all add: algebra_simps\<close>)
haftmann@70338
   755
    also have "\<dots> = - int (Suc (2 * n)) - 1"
haftmann@70338
   756
      by (simp add: algebra_simps)
haftmann@70338
   757
    finally show ?case
haftmann@70338
   758
      using odd by simp
haftmann@70338
   759
  qed
haftmann@70338
   760
qed
haftmann@70338
   761
haftmann@67816
   762
haftmann@67828
   763
subsection \<open>Abstract bit operations\<close>
haftmann@67828
   764
haftmann@67828
   765
context semiring_parity
haftmann@67816
   766
begin
haftmann@67816
   767
haftmann@67816
   768
text \<open>The primary purpose of the following operations is
wenzelm@69593
   769
  to avoid ad-hoc simplification of concrete expressions \<^term>\<open>2 ^ n\<close>\<close>
haftmann@67816
   770
haftmann@67907
   771
definition push_bit :: "nat \<Rightarrow> 'a \<Rightarrow> 'a"
haftmann@67907
   772
  where push_bit_eq_mult: "push_bit n a = a * 2 ^ n"
haftmann@67816
   773
 
haftmann@67907
   774
definition take_bit :: "nat \<Rightarrow> 'a \<Rightarrow> 'a"
haftmann@68010
   775
  where take_bit_eq_mod: "take_bit n a = a mod 2 ^ n"
haftmann@67816
   776
haftmann@67907
   777
definition drop_bit :: "nat \<Rightarrow> 'a \<Rightarrow> 'a"
haftmann@68010
   778
  where drop_bit_eq_div: "drop_bit n a = a div 2 ^ n"
haftmann@67816
   779
haftmann@67816
   780
lemma bit_ident:
haftmann@67907
   781
  "push_bit n (drop_bit n a) + take_bit n a = a"
haftmann@67907
   782
  using div_mult_mod_eq by (simp add: push_bit_eq_mult take_bit_eq_mod drop_bit_eq_div)
haftmann@67816
   783
haftmann@67960
   784
lemma push_bit_push_bit [simp]:
haftmann@67960
   785
  "push_bit m (push_bit n a) = push_bit (m + n) a"
haftmann@67960
   786
  by (simp add: push_bit_eq_mult power_add ac_simps)
haftmann@67960
   787
haftmann@67907
   788
lemma take_bit_take_bit [simp]:
haftmann@67960
   789
  "take_bit m (take_bit n a) = take_bit (min m n) a"
haftmann@67960
   790
proof (cases "m \<le> n")
haftmann@67960
   791
  case True
haftmann@67960
   792
  then show ?thesis
haftmann@67960
   793
    by (simp add: take_bit_eq_mod not_le min_def mod_mod_cancel le_imp_power_dvd)
haftmann@67960
   794
next
haftmann@67960
   795
  case False
haftmann@67960
   796
  then have "n < m" and "min m n = n"
haftmann@67960
   797
    by simp_all
haftmann@67960
   798
  then have "2 ^ m = of_nat (2 ^ n) * of_nat (2 ^ (m - n))"
haftmann@67960
   799
    by (simp add: power_add [symmetric])
haftmann@67960
   800
  then have "a mod 2 ^ n mod 2 ^ m = a mod 2 ^ n mod (of_nat (2 ^ n) * of_nat (2 ^ (m - n)))"
haftmann@67960
   801
    by simp
haftmann@67960
   802
  also have "\<dots> = of_nat (2 ^ n) * (a mod 2 ^ n div of_nat (2 ^ n) mod of_nat (2 ^ (m - n))) + a mod 2 ^ n mod of_nat (2 ^ n)"
haftmann@67960
   803
    by (simp only: mod_mult2_eq')
haftmann@67960
   804
  finally show ?thesis
haftmann@67960
   805
    using \<open>min m n = n\<close> by (simp add: take_bit_eq_mod)
haftmann@67960
   806
qed
haftmann@67960
   807
haftmann@67960
   808
lemma drop_bit_drop_bit [simp]:
haftmann@67960
   809
  "drop_bit m (drop_bit n a) = drop_bit (m + n) a"
haftmann@67960
   810
proof -
haftmann@67960
   811
  have "a div (2 ^ m * 2 ^ n) = a div (of_nat (2 ^ n) * of_nat (2 ^ m))"
haftmann@67960
   812
    by (simp add: ac_simps)
haftmann@67960
   813
  also have "\<dots> = a div of_nat (2 ^ n) div of_nat (2 ^ m)"
haftmann@67960
   814
    by (simp only: div_mult2_eq')
haftmann@67960
   815
  finally show ?thesis
haftmann@67960
   816
    by (simp add: drop_bit_eq_div power_add)
haftmann@67960
   817
qed
haftmann@67960
   818
haftmann@67960
   819
lemma push_bit_take_bit:
haftmann@67960
   820
  "push_bit m (take_bit n a) = take_bit (m + n) (push_bit m a)"
haftmann@67960
   821
  by (simp add: push_bit_eq_mult take_bit_eq_mod power_add mult_mod_right ac_simps)
haftmann@67960
   822
haftmann@67960
   823
lemma take_bit_push_bit:
haftmann@67960
   824
  "take_bit m (push_bit n a) = push_bit n (take_bit (m - n) a)"
haftmann@67960
   825
proof (cases "m \<le> n")
haftmann@67960
   826
  case True
haftmann@67960
   827
  then show ?thesis
haftmann@67960
   828
    by (simp_all add: push_bit_eq_mult take_bit_eq_mod mod_eq_0_iff_dvd dvd_power_le)
haftmann@67960
   829
next
haftmann@67960
   830
  case False
haftmann@67960
   831
  then show ?thesis
haftmann@67960
   832
    using push_bit_take_bit [of n "m - n" a]
haftmann@67960
   833
    by simp
haftmann@67960
   834
qed
haftmann@67960
   835
haftmann@67960
   836
lemma take_bit_drop_bit:
haftmann@67960
   837
  "take_bit m (drop_bit n a) = drop_bit n (take_bit (m + n) a)"
haftmann@67960
   838
  using mod_mult2_eq' [of a "2 ^ n" "2 ^ m"]
haftmann@67960
   839
  by (simp add: drop_bit_eq_div take_bit_eq_mod power_add ac_simps)
haftmann@67960
   840
haftmann@67960
   841
lemma drop_bit_take_bit:
haftmann@67960
   842
  "drop_bit m (take_bit n a) = take_bit (n - m) (drop_bit m a)"
haftmann@67960
   843
proof (cases "m \<le> n")
haftmann@67960
   844
  case True
haftmann@67960
   845
  then show ?thesis
haftmann@67960
   846
    using take_bit_drop_bit [of "n - m" m a] by simp
haftmann@67960
   847
next
haftmann@67960
   848
  case False
haftmann@67960
   849
  then have "a mod 2 ^ n div 2 ^ m = a mod 2 ^ n div 2 ^ (n + (m - n))"
haftmann@67960
   850
    by simp
haftmann@67960
   851
  also have "\<dots> = a mod 2 ^ n div (2 ^ n * 2 ^ (m - n))"
haftmann@67960
   852
    by (simp add: power_add)
haftmann@67960
   853
  also have "\<dots> = a mod 2 ^ n div (of_nat (2 ^ n) * of_nat (2 ^ (m - n)))"
haftmann@67960
   854
    by simp
haftmann@67960
   855
  also have "\<dots> = a mod 2 ^ n div of_nat (2 ^ n) div of_nat (2 ^ (m - n))"
haftmann@67960
   856
    by (simp only: div_mult2_eq')
haftmann@67960
   857
  finally show ?thesis
haftmann@67960
   858
    using False by (simp add: take_bit_eq_mod drop_bit_eq_div)
haftmann@67960
   859
qed
haftmann@67960
   860
haftmann@67988
   861
lemma push_bit_0_id [simp]:
haftmann@67988
   862
  "push_bit 0 = id"
haftmann@67988
   863
  by (simp add: fun_eq_iff push_bit_eq_mult)
haftmann@67988
   864
haftmann@67988
   865
lemma push_bit_of_0 [simp]:
haftmann@67988
   866
  "push_bit n 0 = 0"
haftmann@67988
   867
  by (simp add: push_bit_eq_mult)
haftmann@67988
   868
haftmann@67988
   869
lemma push_bit_of_1:
haftmann@67988
   870
  "push_bit n 1 = 2 ^ n"
haftmann@67988
   871
  by (simp add: push_bit_eq_mult)
haftmann@67988
   872
haftmann@67988
   873
lemma push_bit_Suc [simp]:
haftmann@67988
   874
  "push_bit (Suc n) a = push_bit n (a * 2)"
haftmann@67988
   875
  by (simp add: push_bit_eq_mult ac_simps)
haftmann@67988
   876
haftmann@67988
   877
lemma push_bit_double:
haftmann@67988
   878
  "push_bit n (a * 2) = push_bit n a * 2"
haftmann@67988
   879
  by (simp add: push_bit_eq_mult ac_simps)
haftmann@67988
   880
haftmann@67988
   881
lemma push_bit_eq_0_iff [simp]:
haftmann@67988
   882
  "push_bit n a = 0 \<longleftrightarrow> a = 0"
haftmann@67988
   883
  by (simp add: push_bit_eq_mult)
haftmann@67988
   884
haftmann@67988
   885
lemma push_bit_add:
haftmann@67988
   886
  "push_bit n (a + b) = push_bit n a + push_bit n b"
haftmann@67988
   887
  by (simp add: push_bit_eq_mult algebra_simps)
haftmann@67988
   888
haftmann@67988
   889
lemma push_bit_numeral [simp]:
haftmann@67988
   890
  "push_bit (numeral l) (numeral k) = push_bit (pred_numeral l) (numeral (Num.Bit0 k))"
haftmann@67988
   891
  by (simp only: numeral_eq_Suc power_Suc numeral_Bit0 [of k] mult_2 [symmetric]) (simp add: ac_simps)
haftmann@67988
   892
haftmann@68010
   893
lemma push_bit_of_nat:
haftmann@68010
   894
  "push_bit n (of_nat m) = of_nat (push_bit n m)"
haftmann@68010
   895
  by (simp add: push_bit_eq_mult Parity.push_bit_eq_mult)
haftmann@68010
   896
haftmann@67907
   897
lemma take_bit_0 [simp]:
haftmann@67907
   898
  "take_bit 0 a = 0"
haftmann@67907
   899
  by (simp add: take_bit_eq_mod)
haftmann@67816
   900
haftmann@67907
   901
lemma take_bit_Suc [simp]:
haftmann@67907
   902
  "take_bit (Suc n) a = take_bit n (a div 2) * 2 + of_bool (odd a)"
haftmann@67816
   903
proof -
haftmann@67816
   904
  have "1 + 2 * (a div 2) mod (2 * 2 ^ n) = (a div 2 * 2 + a mod 2) mod (2 * 2 ^ n)"
haftmann@67816
   905
    if "odd a"
haftmann@67816
   906
    using that mod_mult2_eq' [of "1 + 2 * (a div 2)" 2 "2 ^ n"]
haftmann@67816
   907
    by (simp add: ac_simps odd_iff_mod_2_eq_one mult_mod_right)
haftmann@67816
   908
  also have "\<dots> = a mod (2 * 2 ^ n)"
haftmann@67816
   909
    by (simp only: div_mult_mod_eq)
haftmann@67816
   910
  finally show ?thesis
haftmann@67907
   911
    by (simp add: take_bit_eq_mod algebra_simps mult_mod_right)
haftmann@67816
   912
qed
haftmann@67816
   913
haftmann@67907
   914
lemma take_bit_of_0 [simp]:
haftmann@67907
   915
  "take_bit n 0 = 0"
haftmann@67907
   916
  by (simp add: take_bit_eq_mod)
haftmann@67816
   917
haftmann@67988
   918
lemma take_bit_of_1 [simp]:
haftmann@67988
   919
  "take_bit n 1 = of_bool (n > 0)"
haftmann@67988
   920
  by (simp add: take_bit_eq_mod)
haftmann@67988
   921
haftmann@67961
   922
lemma take_bit_add:
haftmann@67907
   923
  "take_bit n (take_bit n a + take_bit n b) = take_bit n (a + b)"
haftmann@67907
   924
  by (simp add: take_bit_eq_mod mod_simps)
haftmann@67816
   925
haftmann@67961
   926
lemma take_bit_eq_0_iff:
haftmann@67961
   927
  "take_bit n a = 0 \<longleftrightarrow> 2 ^ n dvd a"
haftmann@67961
   928
  by (simp add: take_bit_eq_mod mod_eq_0_iff_dvd)
haftmann@67961
   929
haftmann@67907
   930
lemma take_bit_of_1_eq_0_iff [simp]:
haftmann@67907
   931
  "take_bit n 1 = 0 \<longleftrightarrow> n = 0"
haftmann@67907
   932
  by (simp add: take_bit_eq_mod)
haftmann@67816
   933
haftmann@67988
   934
lemma even_take_bit_eq [simp]:
haftmann@67988
   935
  "even (take_bit n a) \<longleftrightarrow> n = 0 \<or> even a"
haftmann@67988
   936
  by (cases n) (simp_all add: take_bit_eq_mod dvd_mod_iff)
haftmann@67816
   937
haftmann@67988
   938
lemma take_bit_numeral_bit0 [simp]:
haftmann@67988
   939
  "take_bit (numeral l) (numeral (Num.Bit0 k)) = take_bit (pred_numeral l) (numeral k) * 2"
haftmann@67988
   940
  by (simp only: numeral_eq_Suc power_Suc numeral_Bit0 [of k] mult_2 [symmetric] take_bit_Suc
haftmann@67988
   941
    ac_simps even_mult_iff nonzero_mult_div_cancel_right [OF numeral_neq_zero]) simp
haftmann@67988
   942
haftmann@67988
   943
lemma take_bit_numeral_bit1 [simp]:
haftmann@67988
   944
  "take_bit (numeral l) (numeral (Num.Bit1 k)) = take_bit (pred_numeral l) (numeral k) * 2 + 1"
haftmann@67988
   945
  by (simp only: numeral_eq_Suc power_Suc numeral_Bit1 [of k] mult_2 [symmetric] take_bit_Suc
haftmann@67988
   946
    ac_simps even_add even_mult_iff div_mult_self1 [OF numeral_neq_zero]) (simp add: ac_simps)
haftmann@67961
   947
haftmann@68010
   948
lemma take_bit_of_nat:
haftmann@68010
   949
  "take_bit n (of_nat m) = of_nat (take_bit n m)"
haftmann@68010
   950
  by (simp add: take_bit_eq_mod Parity.take_bit_eq_mod of_nat_mod [of m "2 ^ n"])
haftmann@68010
   951
haftmann@67907
   952
lemma drop_bit_0 [simp]:
haftmann@67907
   953
  "drop_bit 0 = id"
haftmann@67907
   954
  by (simp add: fun_eq_iff drop_bit_eq_div)
haftmann@67816
   955
haftmann@67907
   956
lemma drop_bit_of_0 [simp]:
haftmann@67907
   957
  "drop_bit n 0 = 0"
haftmann@67907
   958
  by (simp add: drop_bit_eq_div)
haftmann@67816
   959
haftmann@67988
   960
lemma drop_bit_of_1 [simp]:
haftmann@67988
   961
  "drop_bit n 1 = of_bool (n = 0)"
haftmann@67988
   962
  by (simp add: drop_bit_eq_div)
haftmann@67988
   963
haftmann@67907
   964
lemma drop_bit_Suc [simp]:
haftmann@67907
   965
  "drop_bit (Suc n) a = drop_bit n (a div 2)"
haftmann@67816
   966
proof (cases "even a")
haftmann@67816
   967
  case True
haftmann@67816
   968
  then obtain b where "a = 2 * b" ..
haftmann@67907
   969
  moreover have "drop_bit (Suc n) (2 * b) = drop_bit n b"
haftmann@67907
   970
    by (simp add: drop_bit_eq_div)
haftmann@67816
   971
  ultimately show ?thesis
haftmann@67816
   972
    by simp
haftmann@67816
   973
next
haftmann@67816
   974
  case False
haftmann@67816
   975
  then obtain b where "a = 2 * b + 1" ..
haftmann@67907
   976
  moreover have "drop_bit (Suc n) (2 * b + 1) = drop_bit n b"
haftmann@67816
   977
    using div_mult2_eq' [of "1 + b * 2" 2 "2 ^ n"]
haftmann@67907
   978
    by (auto simp add: drop_bit_eq_div ac_simps)
haftmann@67816
   979
  ultimately show ?thesis
haftmann@67816
   980
    by simp
haftmann@67816
   981
qed
haftmann@67816
   982
haftmann@67907
   983
lemma drop_bit_half:
haftmann@67907
   984
  "drop_bit n (a div 2) = drop_bit n a div 2"
haftmann@67816
   985
  by (induction n arbitrary: a) simp_all
haftmann@67816
   986
haftmann@67907
   987
lemma drop_bit_of_bool [simp]:
haftmann@67907
   988
  "drop_bit n (of_bool d) = of_bool (n = 0 \<and> d)"
haftmann@67816
   989
  by (cases n) simp_all
haftmann@67816
   990
haftmann@67988
   991
lemma drop_bit_numeral_bit0 [simp]:
haftmann@67988
   992
  "drop_bit (numeral l) (numeral (Num.Bit0 k)) = drop_bit (pred_numeral l) (numeral k)"
haftmann@67988
   993
  by (simp only: numeral_eq_Suc power_Suc numeral_Bit0 [of k] mult_2 [symmetric] drop_bit_Suc
haftmann@67988
   994
    nonzero_mult_div_cancel_left [OF numeral_neq_zero])
haftmann@67816
   995
haftmann@67988
   996
lemma drop_bit_numeral_bit1 [simp]:
haftmann@67988
   997
  "drop_bit (numeral l) (numeral (Num.Bit1 k)) = drop_bit (pred_numeral l) (numeral k)"
haftmann@67988
   998
  by (simp only: numeral_eq_Suc power_Suc numeral_Bit1 [of k] mult_2 [symmetric] drop_bit_Suc
haftmann@67988
   999
    div_mult_self4 [OF numeral_neq_zero]) simp
haftmann@67816
  1000
haftmann@68010
  1001
lemma drop_bit_of_nat:
haftmann@68010
  1002
  "drop_bit n (of_nat m) = of_nat (drop_bit n m)"
wenzelm@68389
  1003
  by (simp add: drop_bit_eq_div Parity.drop_bit_eq_div of_nat_div [of m "2 ^ n"])
haftmann@68010
  1004
haftmann@58770
  1005
end
haftmann@67816
  1006
haftmann@67988
  1007
lemma push_bit_of_Suc_0 [simp]:
haftmann@67988
  1008
  "push_bit n (Suc 0) = 2 ^ n"
haftmann@67988
  1009
  using push_bit_of_1 [where ?'a = nat] by simp
haftmann@67988
  1010
haftmann@67988
  1011
lemma take_bit_of_Suc_0 [simp]:
haftmann@67988
  1012
  "take_bit n (Suc 0) = of_bool (0 < n)"
haftmann@67988
  1013
  using take_bit_of_1 [where ?'a = nat] by simp
haftmann@67988
  1014
haftmann@67988
  1015
lemma drop_bit_of_Suc_0 [simp]:
haftmann@67988
  1016
  "drop_bit n (Suc 0) = of_bool (n = 0)"
haftmann@67988
  1017
  using drop_bit_of_1 [where ?'a = nat] by simp
haftmann@67988
  1018
haftmann@70226
  1019
haftmann@70226
  1020
subsection \<open>Legacy\<close>
haftmann@70226
  1021
haftmann@70226
  1022
lemma parity_induct [case_names zero even odd]:
haftmann@70226
  1023
  assumes zero: "P 0"
haftmann@70226
  1024
  assumes even: "\<And>n. P n \<Longrightarrow> P (2 * n)"
haftmann@70226
  1025
  assumes odd: "\<And>n. P n \<Longrightarrow> P (Suc (2 * n))"
haftmann@70226
  1026
  shows "P n"
haftmann@70226
  1027
  using assms by (rule nat_parity_induct)
haftmann@70226
  1028
haftmann@67816
  1029
end