src/HOL/Parity.thy
author haftmann
Sat May 12 22:20:46 2018 +0200 (21 months ago ago)
changeset 68157 057d5b4ce47e
parent 68028 1f9f973eed2a
child 68390 1c84a8c513af
permissions -rw-r--r--
removed some non-essential rules
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
haftmann@66815
   157
lemma parity_cases [case_names even odd]:
haftmann@66815
   158
  assumes "even a \<Longrightarrow> a mod 2 = 0 \<Longrightarrow> P"
haftmann@66815
   159
  assumes "odd a \<Longrightarrow> a mod 2 = 1 \<Longrightarrow> P"
haftmann@66815
   160
  shows P
haftmann@66815
   161
  using assms by (cases "even a") (simp_all add: odd_iff_mod_2_eq_one)
haftmann@66815
   162
haftmann@66815
   163
lemma not_mod_2_eq_1_eq_0 [simp]:
haftmann@66815
   164
  "a mod 2 \<noteq> 1 \<longleftrightarrow> a mod 2 = 0"
haftmann@66815
   165
  by (cases a rule: parity_cases) simp_all
haftmann@66815
   166
haftmann@66815
   167
lemma not_mod_2_eq_0_eq_1 [simp]:
haftmann@66815
   168
  "a mod 2 \<noteq> 0 \<longleftrightarrow> a mod 2 = 1"
haftmann@66815
   169
  by (cases a rule: parity_cases) simp_all
haftmann@58787
   170
haftmann@58690
   171
lemma evenE [elim?]:
haftmann@58690
   172
  assumes "even a"
haftmann@58690
   173
  obtains b where "a = 2 * b"
haftmann@58740
   174
  using assms by (rule dvdE)
haftmann@58690
   175
haftmann@58681
   176
lemma oddE [elim?]:
haftmann@58680
   177
  assumes "odd a"
haftmann@58680
   178
  obtains b where "a = 2 * b + 1"
haftmann@58787
   179
proof -
haftmann@66815
   180
  have "a = 2 * (a div 2) + a mod 2"
haftmann@66815
   181
    by (simp add: mult_div_mod_eq)
haftmann@66815
   182
  with assms have "a = 2 * (a div 2) + 1"
haftmann@66815
   183
    by (simp add: odd_iff_mod_2_eq_one)
haftmann@66815
   184
  then show ?thesis ..
haftmann@66815
   185
qed
haftmann@66815
   186
haftmann@66815
   187
lemma mod_2_eq_odd:
haftmann@66815
   188
  "a mod 2 = of_bool (odd a)"
haftmann@66815
   189
  by (auto elim: oddE)
haftmann@66815
   190
haftmann@67816
   191
lemma of_bool_odd_eq_mod_2:
haftmann@67816
   192
  "of_bool (odd a) = a mod 2"
haftmann@67816
   193
  by (simp add: mod_2_eq_odd)
haftmann@67816
   194
haftmann@66815
   195
lemma one_mod_2_pow_eq [simp]:
haftmann@66815
   196
  "1 mod (2 ^ n) = of_bool (n > 0)"
haftmann@66815
   197
proof -
haftmann@67083
   198
  have "1 mod (2 ^ n) = of_nat (1 mod (2 ^ n))"
haftmann@67083
   199
    using of_nat_mod [of 1 "2 ^ n"] by simp
haftmann@67083
   200
  also have "\<dots> = of_bool (n > 0)"
haftmann@66815
   201
    by simp
haftmann@67083
   202
  finally show ?thesis .
haftmann@66815
   203
qed
haftmann@66815
   204
haftmann@67816
   205
lemma one_div_2_pow_eq [simp]:
haftmann@67816
   206
  "1 div (2 ^ n) = of_bool (n = 0)"
haftmann@67816
   207
  using div_mult_mod_eq [of 1 "2 ^ n"] by auto
haftmann@67816
   208
haftmann@66815
   209
lemma even_of_nat [simp]:
haftmann@66815
   210
  "even (of_nat a) \<longleftrightarrow> even a"
haftmann@66815
   211
proof -
haftmann@66815
   212
  have "even (of_nat a) \<longleftrightarrow> of_nat 2 dvd of_nat a"
haftmann@66815
   213
    by simp
haftmann@66815
   214
  also have "\<dots> \<longleftrightarrow> even a"
haftmann@66815
   215
    by (simp only: of_nat_dvd_iff)
haftmann@66815
   216
  finally show ?thesis .
haftmann@66815
   217
qed
haftmann@66815
   218
haftmann@66815
   219
lemma even_zero [simp]:
haftmann@66815
   220
  "even 0"
haftmann@66815
   221
  by (fact dvd_0_right)
haftmann@66815
   222
haftmann@66815
   223
lemma odd_one [simp]:
haftmann@66815
   224
  "odd 1"
haftmann@66815
   225
proof -
haftmann@66815
   226
  have "\<not> (2 :: nat) dvd 1"
haftmann@66815
   227
    by simp
haftmann@66815
   228
  then have "\<not> of_nat 2 dvd of_nat 1"
haftmann@66815
   229
    unfolding of_nat_dvd_iff by simp
haftmann@66815
   230
  then show ?thesis
haftmann@66815
   231
    by simp
haftmann@58787
   232
qed
wenzelm@63654
   233
haftmann@66815
   234
lemma odd_even_add:
haftmann@66815
   235
  "even (a + b)" if "odd a" and "odd b"
haftmann@66815
   236
proof -
haftmann@66815
   237
  from that obtain c d where "a = 2 * c + 1" and "b = 2 * d + 1"
haftmann@66815
   238
    by (blast elim: oddE)
haftmann@66815
   239
  then have "a + b = 2 * c + 2 * d + (1 + 1)"
haftmann@66815
   240
    by (simp only: ac_simps)
haftmann@66815
   241
  also have "\<dots> = 2 * (c + d + 1)"
haftmann@66815
   242
    by (simp add: algebra_simps)
haftmann@66815
   243
  finally show ?thesis ..
haftmann@66815
   244
qed
haftmann@66815
   245
haftmann@66815
   246
lemma even_add [simp]:
haftmann@66815
   247
  "even (a + b) \<longleftrightarrow> (even a \<longleftrightarrow> even b)"
haftmann@66815
   248
  by (auto simp add: dvd_add_right_iff dvd_add_left_iff odd_even_add)
haftmann@66815
   249
haftmann@66815
   250
lemma odd_add [simp]:
haftmann@66815
   251
  "odd (a + b) \<longleftrightarrow> \<not> (odd a \<longleftrightarrow> odd b)"
haftmann@66815
   252
  by simp
haftmann@66815
   253
haftmann@66815
   254
lemma even_plus_one_iff [simp]:
haftmann@66815
   255
  "even (a + 1) \<longleftrightarrow> odd a"
haftmann@66815
   256
  by (auto simp add: dvd_add_right_iff intro: odd_even_add)
haftmann@66815
   257
haftmann@66815
   258
lemma even_mult_iff [simp]:
haftmann@66815
   259
  "even (a * b) \<longleftrightarrow> even a \<or> even b" (is "?P \<longleftrightarrow> ?Q")
haftmann@66815
   260
proof
haftmann@66815
   261
  assume ?Q
haftmann@66815
   262
  then show ?P
haftmann@66815
   263
    by auto
haftmann@66815
   264
next
haftmann@66815
   265
  assume ?P
haftmann@66815
   266
  show ?Q
haftmann@66815
   267
  proof (rule ccontr)
haftmann@66815
   268
    assume "\<not> (even a \<or> even b)"
haftmann@66815
   269
    then have "odd a" and "odd b"
haftmann@66815
   270
      by auto
haftmann@66815
   271
    then obtain r s where "a = 2 * r + 1" and "b = 2 * s + 1"
haftmann@66815
   272
      by (blast elim: oddE)
haftmann@66815
   273
    then have "a * b = (2 * r + 1) * (2 * s + 1)"
haftmann@66815
   274
      by simp
haftmann@66815
   275
    also have "\<dots> = 2 * (2 * r * s + r + s) + 1"
haftmann@66815
   276
      by (simp add: algebra_simps)
haftmann@66815
   277
    finally have "odd (a * b)"
haftmann@66815
   278
      by simp
haftmann@66815
   279
    with \<open>?P\<close> show False
haftmann@66815
   280
      by auto
haftmann@66815
   281
  qed
haftmann@66815
   282
qed
haftmann@58678
   283
wenzelm@63654
   284
lemma even_numeral [simp]: "even (numeral (Num.Bit0 n))"
haftmann@58678
   285
proof -
haftmann@58678
   286
  have "even (2 * numeral n)"
haftmann@66815
   287
    unfolding even_mult_iff by simp
haftmann@58678
   288
  then have "even (numeral n + numeral n)"
haftmann@58678
   289
    unfolding mult_2 .
haftmann@58678
   290
  then show ?thesis
haftmann@58678
   291
    unfolding numeral.simps .
haftmann@58678
   292
qed
haftmann@58678
   293
wenzelm@63654
   294
lemma odd_numeral [simp]: "odd (numeral (Num.Bit1 n))"
haftmann@58678
   295
proof
haftmann@58678
   296
  assume "even (numeral (num.Bit1 n))"
haftmann@58678
   297
  then have "even (numeral n + numeral n + 1)"
haftmann@58678
   298
    unfolding numeral.simps .
haftmann@58678
   299
  then have "even (2 * numeral n + 1)"
haftmann@58678
   300
    unfolding mult_2 .
haftmann@58678
   301
  then have "2 dvd numeral n * 2 + 1"
haftmann@58740
   302
    by (simp add: ac_simps)
wenzelm@63654
   303
  then have "2 dvd 1"
wenzelm@63654
   304
    using dvd_add_times_triv_left_iff [of 2 "numeral n" 1] by simp
haftmann@58678
   305
  then show False by simp
haftmann@58678
   306
qed
haftmann@58678
   307
wenzelm@63654
   308
lemma even_power [simp]: "even (a ^ n) \<longleftrightarrow> even a \<and> n > 0"
haftmann@58680
   309
  by (induct n) auto
haftmann@58680
   310
haftmann@66815
   311
lemma even_succ_div_two [simp]:
haftmann@66815
   312
  "even a \<Longrightarrow> (a + 1) div 2 = a div 2"
haftmann@66815
   313
  by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero)
haftmann@66815
   314
haftmann@66815
   315
lemma odd_succ_div_two [simp]:
haftmann@66815
   316
  "odd a \<Longrightarrow> (a + 1) div 2 = a div 2 + 1"
haftmann@66815
   317
  by (auto elim!: oddE simp add: add.assoc)
haftmann@66815
   318
haftmann@66815
   319
lemma even_two_times_div_two:
haftmann@66815
   320
  "even a \<Longrightarrow> 2 * (a div 2) = a"
haftmann@66815
   321
  by (fact dvd_mult_div_cancel)
haftmann@66815
   322
haftmann@66815
   323
lemma odd_two_times_div_two_succ [simp]:
haftmann@66815
   324
  "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
haftmann@66815
   325
  using mult_div_mod_eq [of 2 a]
haftmann@66815
   326
  by (simp add: even_iff_mod_2_eq_zero)
haftmann@66815
   327
haftmann@67051
   328
lemma coprime_left_2_iff_odd [simp]:
haftmann@67051
   329
  "coprime 2 a \<longleftrightarrow> odd a"
haftmann@67051
   330
proof
haftmann@67051
   331
  assume "odd a"
haftmann@67051
   332
  show "coprime 2 a"
haftmann@67051
   333
  proof (rule coprimeI)
haftmann@67051
   334
    fix b
haftmann@67051
   335
    assume "b dvd 2" "b dvd a"
haftmann@67051
   336
    then have "b dvd a mod 2"
haftmann@67051
   337
      by (auto intro: dvd_mod)
haftmann@67051
   338
    with \<open>odd a\<close> show "is_unit b"
haftmann@67051
   339
      by (simp add: mod_2_eq_odd)
haftmann@67051
   340
  qed
haftmann@67051
   341
next
haftmann@67051
   342
  assume "coprime 2 a"
haftmann@67051
   343
  show "odd a"
haftmann@67051
   344
  proof (rule notI)
haftmann@67051
   345
    assume "even a"
haftmann@67051
   346
    then obtain b where "a = 2 * b" ..
haftmann@67051
   347
    with \<open>coprime 2 a\<close> have "coprime 2 (2 * b)"
haftmann@67051
   348
      by simp
haftmann@67051
   349
    moreover have "\<not> coprime 2 (2 * b)"
haftmann@67051
   350
      by (rule not_coprimeI [of 2]) simp_all
haftmann@67051
   351
    ultimately show False
haftmann@67051
   352
      by blast
haftmann@67051
   353
  qed
haftmann@67051
   354
qed
haftmann@67051
   355
haftmann@67051
   356
lemma coprime_right_2_iff_odd [simp]:
haftmann@67051
   357
  "coprime a 2 \<longleftrightarrow> odd a"
haftmann@67051
   358
  using coprime_left_2_iff_odd [of a] by (simp add: ac_simps)
haftmann@67051
   359
haftmann@67828
   360
lemma div_mult2_eq':
haftmann@67828
   361
  "a div (of_nat m * of_nat n) = a div of_nat m div of_nat n"
haftmann@67828
   362
proof (cases a "of_nat m * of_nat n" rule: divmod_cases)
haftmann@67828
   363
  case (divides q)
haftmann@67828
   364
  then show ?thesis
haftmann@67828
   365
    using nonzero_mult_div_cancel_right [of "of_nat m" "q * of_nat n"]
haftmann@67828
   366
    by (simp add: ac_simps)
haftmann@67828
   367
next
haftmann@67828
   368
  case (remainder q r)
haftmann@67828
   369
  then have "division_segment r = 1"
haftmann@67828
   370
    using division_segment_of_nat [of "m * n"] by simp
haftmann@67828
   371
  with division_segment_euclidean_size [of r]
haftmann@67828
   372
  have "of_nat (euclidean_size r) = r"
haftmann@67828
   373
    by simp
haftmann@67908
   374
  have "a mod (of_nat m * of_nat n) div (of_nat m * of_nat n) = 0"
haftmann@67908
   375
    by simp
haftmann@67908
   376
  with remainder(6) have "r div (of_nat m * of_nat n) = 0"
haftmann@67828
   377
    by simp
haftmann@67908
   378
  with \<open>of_nat (euclidean_size r) = r\<close>
haftmann@67908
   379
  have "of_nat (euclidean_size r) div (of_nat m * of_nat n) = 0"
haftmann@67908
   380
    by simp
haftmann@67908
   381
  then have "of_nat (euclidean_size r div (m * n)) = 0"
haftmann@67828
   382
    by (simp add: of_nat_div)
haftmann@67908
   383
  then have "of_nat (euclidean_size r div m div n) = 0"
haftmann@67908
   384
    by (simp add: div_mult2_eq)
haftmann@67908
   385
  with \<open>of_nat (euclidean_size r) = r\<close> have "r div of_nat m div of_nat n = 0"
haftmann@67908
   386
    by (simp add: of_nat_div)
haftmann@67828
   387
  with remainder(1)
haftmann@67828
   388
  have "q = (r div of_nat m + q * of_nat n * of_nat m div of_nat m) div of_nat n"
haftmann@67828
   389
    by simp
haftmann@67908
   390
  with remainder(5) remainder(7) show ?thesis
haftmann@67828
   391
    using div_plus_div_distrib_dvd_right [of "of_nat m" "q * (of_nat m * of_nat n)" r]
haftmann@67828
   392
    by (simp add: ac_simps)
haftmann@67828
   393
next
haftmann@67828
   394
  case by0
haftmann@67828
   395
  then show ?thesis
haftmann@67828
   396
    by auto
haftmann@67828
   397
qed
haftmann@67828
   398
haftmann@67828
   399
lemma mod_mult2_eq':
haftmann@67828
   400
  "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
   401
proof -
haftmann@67828
   402
  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
   403
    by (simp add: combine_common_factor div_mult_mod_eq)
haftmann@67828
   404
  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
   405
    by (simp add: ac_simps)
haftmann@67828
   406
  ultimately show ?thesis
haftmann@67828
   407
    by (simp add: div_mult2_eq' mult_commute)
haftmann@67828
   408
qed
haftmann@67828
   409
haftmann@68028
   410
lemma div_mult2_numeral_eq:
haftmann@68028
   411
  "a div numeral k div numeral l = a div numeral (k * l)" (is "?A = ?B")
haftmann@68028
   412
proof -
haftmann@68028
   413
  have "?A = a div of_nat (numeral k) div of_nat (numeral l)"
haftmann@68028
   414
    by simp
haftmann@68028
   415
  also have "\<dots> = a div (of_nat (numeral k) * of_nat (numeral l))"
haftmann@68028
   416
    by (fact div_mult2_eq' [symmetric])
haftmann@68028
   417
  also have "\<dots> = ?B"
haftmann@68028
   418
    by simp
haftmann@68028
   419
  finally show ?thesis .
haftmann@68028
   420
qed
haftmann@68028
   421
haftmann@58678
   422
end
haftmann@58678
   423
haftmann@59816
   424
class ring_parity = ring + semiring_parity
haftmann@58679
   425
begin
haftmann@58679
   426
haftmann@59816
   427
subclass comm_ring_1 ..
haftmann@59816
   428
haftmann@67816
   429
lemma even_minus:
haftmann@66815
   430
  "even (- a) \<longleftrightarrow> even a"
haftmann@58740
   431
  by (fact dvd_minus_iff)
haftmann@58679
   432
haftmann@66815
   433
lemma even_diff [simp]:
haftmann@66815
   434
  "even (a - b) \<longleftrightarrow> even (a + b)"
haftmann@58680
   435
  using even_add [of a "- b"] by simp
haftmann@58680
   436
haftmann@67906
   437
lemma minus_1_mod_2_eq [simp]:
haftmann@67906
   438
  "- 1 mod 2 = 1"
haftmann@67906
   439
  by (simp add: mod_2_eq_odd)
haftmann@67906
   440
haftmann@67906
   441
lemma minus_1_div_2_eq [simp]:
haftmann@67906
   442
  "- 1 div 2 = - 1"
haftmann@67906
   443
proof -
haftmann@67906
   444
  from div_mult_mod_eq [of "- 1" 2]
haftmann@67906
   445
  have "- 1 div 2 * 2 = - 1 * 2"
haftmann@67906
   446
    using local.add_implies_diff by fastforce
haftmann@67906
   447
  then show ?thesis
haftmann@67906
   448
    using mult_right_cancel [of 2 "- 1 div 2" "- 1"] by simp
haftmann@67906
   449
qed
haftmann@67906
   450
haftmann@58679
   451
end
haftmann@58679
   452
haftmann@66808
   453
haftmann@66815
   454
subsection \<open>Instance for @{typ nat}\<close>
haftmann@66808
   455
haftmann@66815
   456
instance nat :: semiring_parity
haftmann@66815
   457
  by standard (simp_all add: dvd_eq_mod_eq_0)
haftmann@66808
   458
haftmann@66815
   459
lemma even_Suc_Suc_iff [simp]:
haftmann@66815
   460
  "even (Suc (Suc n)) \<longleftrightarrow> even n"
haftmann@58787
   461
  using dvd_add_triv_right_iff [of 2 n] by simp
haftmann@58687
   462
haftmann@66815
   463
lemma even_Suc [simp]: "even (Suc n) \<longleftrightarrow> odd n"
haftmann@66815
   464
  using even_plus_one_iff [of n] by simp
haftmann@58787
   465
haftmann@66815
   466
lemma even_diff_nat [simp]:
haftmann@66815
   467
  "even (m - n) \<longleftrightarrow> m < n \<or> even (m + n)" for m n :: nat
haftmann@58787
   468
proof (cases "n \<le> m")
haftmann@58787
   469
  case True
haftmann@58787
   470
  then have "m - n + n * 2 = m + n" by (simp add: mult_2_right)
haftmann@66815
   471
  moreover have "even (m - n) \<longleftrightarrow> even (m - n + n * 2)" by simp
haftmann@66815
   472
  ultimately have "even (m - n) \<longleftrightarrow> even (m + n)" by (simp only:)
haftmann@58787
   473
  then show ?thesis by auto
haftmann@58787
   474
next
haftmann@58787
   475
  case False
haftmann@58787
   476
  then show ?thesis by simp
wenzelm@63654
   477
qed
wenzelm@63654
   478
haftmann@66815
   479
lemma odd_pos:
haftmann@66815
   480
  "odd n \<Longrightarrow> 0 < n" for n :: nat
haftmann@58690
   481
  by (auto elim: oddE)
haftmann@60345
   482
haftmann@66815
   483
lemma Suc_double_not_eq_double:
haftmann@66815
   484
  "Suc (2 * m) \<noteq> 2 * n"
haftmann@62597
   485
proof
haftmann@62597
   486
  assume "Suc (2 * m) = 2 * n"
haftmann@62597
   487
  moreover have "odd (Suc (2 * m))" and "even (2 * n)"
haftmann@62597
   488
    by simp_all
haftmann@62597
   489
  ultimately show False by simp
haftmann@62597
   490
qed
haftmann@62597
   491
haftmann@66815
   492
lemma double_not_eq_Suc_double:
haftmann@66815
   493
  "2 * m \<noteq> Suc (2 * n)"
haftmann@62597
   494
  using Suc_double_not_eq_double [of n m] by simp
haftmann@62597
   495
haftmann@66815
   496
lemma odd_Suc_minus_one [simp]: "odd n \<Longrightarrow> Suc (n - Suc 0) = n"
haftmann@66815
   497
  by (auto elim: oddE)
haftmann@60345
   498
haftmann@66815
   499
lemma even_Suc_div_two [simp]:
haftmann@66815
   500
  "even n \<Longrightarrow> Suc n div 2 = n div 2"
haftmann@66815
   501
  using even_succ_div_two [of n] by simp
haftmann@60345
   502
haftmann@66815
   503
lemma odd_Suc_div_two [simp]:
haftmann@66815
   504
  "odd n \<Longrightarrow> Suc n div 2 = Suc (n div 2)"
haftmann@66815
   505
  using odd_succ_div_two [of n] by simp
haftmann@60345
   506
haftmann@66815
   507
lemma odd_two_times_div_two_nat [simp]:
haftmann@66815
   508
  assumes "odd n"
haftmann@66815
   509
  shows "2 * (n div 2) = n - (1 :: nat)"
haftmann@66815
   510
proof -
haftmann@66815
   511
  from assms have "2 * (n div 2) + 1 = n"
haftmann@66815
   512
    by (rule odd_two_times_div_two_succ)
haftmann@66815
   513
  then have "Suc (2 * (n div 2)) - 1 = n - 1"
haftmann@58787
   514
    by simp
haftmann@66815
   515
  then show ?thesis
haftmann@66815
   516
    by simp
haftmann@58787
   517
qed
haftmann@58680
   518
haftmann@66815
   519
lemma parity_induct [case_names zero even odd]:
haftmann@66815
   520
  assumes zero: "P 0"
haftmann@66815
   521
  assumes even: "\<And>n. P n \<Longrightarrow> P (2 * n)"
haftmann@66815
   522
  assumes odd: "\<And>n. P n \<Longrightarrow> P (Suc (2 * n))"
haftmann@66815
   523
  shows "P n"
haftmann@66815
   524
proof (induct n rule: less_induct)
haftmann@66815
   525
  case (less n)
haftmann@66815
   526
  show "P n"
haftmann@66815
   527
  proof (cases "n = 0")
haftmann@66815
   528
    case True with zero show ?thesis by simp
haftmann@66815
   529
  next
haftmann@66815
   530
    case False
haftmann@66815
   531
    with less have hyp: "P (n div 2)" by simp
haftmann@66815
   532
    show ?thesis
haftmann@66815
   533
    proof (cases "even n")
haftmann@66815
   534
      case True
haftmann@66815
   535
      with hyp even [of "n div 2"] show ?thesis
haftmann@66815
   536
        by simp
haftmann@66815
   537
    next
haftmann@66815
   538
      case False
haftmann@66815
   539
      with hyp odd [of "n div 2"] show ?thesis
haftmann@66815
   540
        by simp
haftmann@66815
   541
    qed
haftmann@66815
   542
  qed
haftmann@66815
   543
qed
haftmann@58687
   544
haftmann@68157
   545
lemma not_mod2_eq_Suc_0_eq_0 [simp]:
haftmann@68157
   546
  "n mod 2 \<noteq> Suc 0 \<longleftrightarrow> n mod 2 = 0"
haftmann@68157
   547
  using not_mod_2_eq_1_eq_0 [of n] by simp
haftmann@68157
   548
haftmann@58687
   549
wenzelm@60758
   550
subsection \<open>Parity and powers\<close>
haftmann@58689
   551
eberlm@61525
   552
context ring_1
haftmann@58689
   553
begin
haftmann@58689
   554
wenzelm@63654
   555
lemma power_minus_even [simp]: "even n \<Longrightarrow> (- a) ^ n = a ^ n"
haftmann@58690
   556
  by (auto elim: evenE)
haftmann@58689
   557
wenzelm@63654
   558
lemma power_minus_odd [simp]: "odd n \<Longrightarrow> (- a) ^ n = - (a ^ n)"
haftmann@58690
   559
  by (auto elim: oddE)
haftmann@58690
   560
haftmann@66815
   561
lemma uminus_power_if:
haftmann@66815
   562
  "(- a) ^ n = (if even n then a ^ n else - (a ^ n))"
haftmann@66815
   563
  by auto
haftmann@66815
   564
wenzelm@63654
   565
lemma neg_one_even_power [simp]: "even n \<Longrightarrow> (- 1) ^ n = 1"
haftmann@58690
   566
  by simp
haftmann@58689
   567
wenzelm@63654
   568
lemma neg_one_odd_power [simp]: "odd n \<Longrightarrow> (- 1) ^ n = - 1"
haftmann@58690
   569
  by simp
haftmann@58689
   570
bulwahn@66584
   571
lemma neg_one_power_add_eq_neg_one_power_diff: "k \<le> n \<Longrightarrow> (- 1) ^ (n + k) = (- 1) ^ (n - k)"
bulwahn@66584
   572
  by (cases "even (n + k)") auto
bulwahn@66584
   573
lp15@67371
   574
lemma minus_one_power_iff: "(- 1) ^ n = (if even n then 1 else - 1)"
lp15@67371
   575
  by (induct n) auto
lp15@67371
   576
wenzelm@63654
   577
end
haftmann@58689
   578
haftmann@58689
   579
context linordered_idom
haftmann@58689
   580
begin
haftmann@58689
   581
wenzelm@63654
   582
lemma zero_le_even_power: "even n \<Longrightarrow> 0 \<le> a ^ n"
haftmann@58690
   583
  by (auto elim: evenE)
haftmann@58689
   584
wenzelm@63654
   585
lemma zero_le_odd_power: "odd n \<Longrightarrow> 0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a"
haftmann@58689
   586
  by (auto simp add: power_even_eq zero_le_mult_iff elim: oddE)
haftmann@58689
   587
wenzelm@63654
   588
lemma zero_le_power_eq: "0 \<le> a ^ n \<longleftrightarrow> even n \<or> odd n \<and> 0 \<le> a"
haftmann@58787
   589
  by (auto simp add: zero_le_even_power zero_le_odd_power)
wenzelm@63654
   590
wenzelm@63654
   591
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
   592
proof -
haftmann@58689
   593
  have [simp]: "0 = a ^ n \<longleftrightarrow> a = 0 \<and> n > 0"
haftmann@58787
   594
    unfolding power_eq_0_iff [of a n, symmetric] by blast
haftmann@58689
   595
  show ?thesis
wenzelm@63654
   596
    unfolding less_le zero_le_power_eq by auto
haftmann@58689
   597
qed
haftmann@58689
   598
wenzelm@63654
   599
lemma power_less_zero_eq [simp]: "a ^ n < 0 \<longleftrightarrow> odd n \<and> a < 0"
haftmann@58689
   600
  unfolding not_le [symmetric] zero_le_power_eq by auto
haftmann@58689
   601
wenzelm@63654
   602
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
   603
  unfolding not_less [symmetric] zero_less_power_eq by auto
wenzelm@63654
   604
wenzelm@63654
   605
lemma power_even_abs: "even n \<Longrightarrow> \<bar>a\<bar> ^ n = a ^ n"
haftmann@58689
   606
  using power_abs [of a n] by (simp add: zero_le_even_power)
haftmann@58689
   607
haftmann@58689
   608
lemma power_mono_even:
haftmann@58689
   609
  assumes "even n" and "\<bar>a\<bar> \<le> \<bar>b\<bar>"
haftmann@58689
   610
  shows "a ^ n \<le> b ^ n"
haftmann@58689
   611
proof -
haftmann@58689
   612
  have "0 \<le> \<bar>a\<bar>" by auto
wenzelm@63654
   613
  with \<open>\<bar>a\<bar> \<le> \<bar>b\<bar>\<close> have "\<bar>a\<bar> ^ n \<le> \<bar>b\<bar> ^ n"
wenzelm@63654
   614
    by (rule power_mono)
wenzelm@63654
   615
  with \<open>even n\<close> show ?thesis
wenzelm@63654
   616
    by (simp add: power_even_abs)
haftmann@58689
   617
qed
haftmann@58689
   618
haftmann@58689
   619
lemma power_mono_odd:
haftmann@58689
   620
  assumes "odd n" and "a \<le> b"
haftmann@58689
   621
  shows "a ^ n \<le> b ^ n"
haftmann@58689
   622
proof (cases "b < 0")
wenzelm@63654
   623
  case True
wenzelm@63654
   624
  with \<open>a \<le> b\<close> have "- b \<le> - a" and "0 \<le> - b" by auto
wenzelm@63654
   625
  then have "(- b) ^ n \<le> (- a) ^ n" by (rule power_mono)
wenzelm@60758
   626
  with \<open>odd n\<close> show ?thesis by simp
haftmann@58689
   627
next
wenzelm@63654
   628
  case False
wenzelm@63654
   629
  then have "0 \<le> b" by auto
haftmann@58689
   630
  show ?thesis
haftmann@58689
   631
  proof (cases "a < 0")
wenzelm@63654
   632
    case True
wenzelm@63654
   633
    then have "n \<noteq> 0" and "a \<le> 0" using \<open>odd n\<close> [THEN odd_pos] by auto
wenzelm@60758
   634
    then have "a ^ n \<le> 0" unfolding power_le_zero_eq using \<open>odd n\<close> by auto
wenzelm@63654
   635
    moreover from \<open>0 \<le> b\<close> have "0 \<le> b ^ n" by auto
haftmann@58689
   636
    ultimately show ?thesis by auto
haftmann@58689
   637
  next
wenzelm@63654
   638
    case False
wenzelm@63654
   639
    then have "0 \<le> a" by auto
wenzelm@63654
   640
    with \<open>a \<le> b\<close> show ?thesis
wenzelm@63654
   641
      using power_mono by auto
haftmann@58689
   642
  qed
haftmann@58689
   643
qed
hoelzl@62083
   644
wenzelm@60758
   645
text \<open>Simplify, when the exponent is a numeral\<close>
haftmann@58689
   646
haftmann@58689
   647
lemma zero_le_power_eq_numeral [simp]:
haftmann@58689
   648
  "0 \<le> a ^ numeral w \<longleftrightarrow> even (numeral w :: nat) \<or> odd (numeral w :: nat) \<and> 0 \<le> a"
haftmann@58689
   649
  by (fact zero_le_power_eq)
haftmann@58689
   650
haftmann@58689
   651
lemma zero_less_power_eq_numeral [simp]:
wenzelm@63654
   652
  "0 < a ^ numeral w \<longleftrightarrow>
wenzelm@63654
   653
    numeral w = (0 :: nat) \<or>
wenzelm@63654
   654
    even (numeral w :: nat) \<and> a \<noteq> 0 \<or>
wenzelm@63654
   655
    odd (numeral w :: nat) \<and> 0 < a"
haftmann@58689
   656
  by (fact zero_less_power_eq)
haftmann@58689
   657
haftmann@58689
   658
lemma power_le_zero_eq_numeral [simp]:
wenzelm@63654
   659
  "a ^ numeral w \<le> 0 \<longleftrightarrow>
wenzelm@63654
   660
    (0 :: nat) < numeral w \<and>
wenzelm@63654
   661
    (odd (numeral w :: nat) \<and> a \<le> 0 \<or> even (numeral w :: nat) \<and> a = 0)"
haftmann@58689
   662
  by (fact power_le_zero_eq)
haftmann@58689
   663
haftmann@58689
   664
lemma power_less_zero_eq_numeral [simp]:
haftmann@58689
   665
  "a ^ numeral w < 0 \<longleftrightarrow> odd (numeral w :: nat) \<and> a < 0"
haftmann@58689
   666
  by (fact power_less_zero_eq)
haftmann@58689
   667
haftmann@58689
   668
lemma power_even_abs_numeral [simp]:
haftmann@58689
   669
  "even (numeral w :: nat) \<Longrightarrow> \<bar>a\<bar> ^ numeral w = a ^ numeral w"
haftmann@58689
   670
  by (fact power_even_abs)
haftmann@58689
   671
haftmann@58689
   672
end
haftmann@58689
   673
haftmann@66816
   674
haftmann@66816
   675
subsection \<open>Instance for @{typ int}\<close>
haftmann@66816
   676
haftmann@66816
   677
instance int :: ring_parity
haftmann@66839
   678
  by standard (simp_all add: dvd_eq_mod_eq_0 divide_int_def division_segment_int_def)
haftmann@66816
   679
haftmann@67816
   680
lemma even_diff_iff:
haftmann@66816
   681
  "even (k - l) \<longleftrightarrow> even (k + l)" for k l :: int
haftmann@67816
   682
  by (fact even_diff)
haftmann@66816
   683
haftmann@67816
   684
lemma even_abs_add_iff:
haftmann@66816
   685
  "even (\<bar>k\<bar> + l) \<longleftrightarrow> even (k + l)" for k l :: int
haftmann@67816
   686
  by simp
haftmann@66816
   687
haftmann@67816
   688
lemma even_add_abs_iff:
haftmann@66816
   689
  "even (k + \<bar>l\<bar>) \<longleftrightarrow> even (k + l)" for k l :: int
haftmann@67816
   690
  by simp
haftmann@66816
   691
haftmann@66816
   692
lemma even_nat_iff: "0 \<le> k \<Longrightarrow> even (nat k) \<longleftrightarrow> even k"
haftmann@66816
   693
  by (simp add: even_of_nat [of "nat k", where ?'a = int, symmetric])
haftmann@66816
   694
haftmann@67816
   695
haftmann@67828
   696
subsection \<open>Abstract bit operations\<close>
haftmann@67828
   697
haftmann@67828
   698
context semiring_parity
haftmann@67816
   699
begin
haftmann@67816
   700
haftmann@67816
   701
text \<open>The primary purpose of the following operations is
haftmann@67816
   702
  to avoid ad-hoc simplification of concrete expressions @{term "2 ^ n"}\<close>
haftmann@67816
   703
haftmann@67907
   704
definition push_bit :: "nat \<Rightarrow> 'a \<Rightarrow> 'a"
haftmann@67907
   705
  where push_bit_eq_mult: "push_bit n a = a * 2 ^ n"
haftmann@67816
   706
 
haftmann@67907
   707
definition take_bit :: "nat \<Rightarrow> 'a \<Rightarrow> 'a"
haftmann@68010
   708
  where take_bit_eq_mod: "take_bit n a = a mod 2 ^ n"
haftmann@67816
   709
haftmann@67907
   710
definition drop_bit :: "nat \<Rightarrow> 'a \<Rightarrow> 'a"
haftmann@68010
   711
  where drop_bit_eq_div: "drop_bit n a = a div 2 ^ n"
haftmann@67816
   712
haftmann@67816
   713
lemma bit_ident:
haftmann@67907
   714
  "push_bit n (drop_bit n a) + take_bit n a = a"
haftmann@67907
   715
  using div_mult_mod_eq by (simp add: push_bit_eq_mult take_bit_eq_mod drop_bit_eq_div)
haftmann@67816
   716
haftmann@67960
   717
lemma push_bit_push_bit [simp]:
haftmann@67960
   718
  "push_bit m (push_bit n a) = push_bit (m + n) a"
haftmann@67960
   719
  by (simp add: push_bit_eq_mult power_add ac_simps)
haftmann@67960
   720
haftmann@67907
   721
lemma take_bit_take_bit [simp]:
haftmann@67960
   722
  "take_bit m (take_bit n a) = take_bit (min m n) a"
haftmann@67960
   723
proof (cases "m \<le> n")
haftmann@67960
   724
  case True
haftmann@67960
   725
  then show ?thesis
haftmann@67960
   726
    by (simp add: take_bit_eq_mod not_le min_def mod_mod_cancel le_imp_power_dvd)
haftmann@67960
   727
next
haftmann@67960
   728
  case False
haftmann@67960
   729
  then have "n < m" and "min m n = n"
haftmann@67960
   730
    by simp_all
haftmann@67960
   731
  then have "2 ^ m = of_nat (2 ^ n) * of_nat (2 ^ (m - n))"
haftmann@67960
   732
    by (simp add: power_add [symmetric])
haftmann@67960
   733
  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
   734
    by simp
haftmann@67960
   735
  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
   736
    by (simp only: mod_mult2_eq')
haftmann@67960
   737
  finally show ?thesis
haftmann@67960
   738
    using \<open>min m n = n\<close> by (simp add: take_bit_eq_mod)
haftmann@67960
   739
qed
haftmann@67960
   740
haftmann@67960
   741
lemma drop_bit_drop_bit [simp]:
haftmann@67960
   742
  "drop_bit m (drop_bit n a) = drop_bit (m + n) a"
haftmann@67960
   743
proof -
haftmann@67960
   744
  have "a div (2 ^ m * 2 ^ n) = a div (of_nat (2 ^ n) * of_nat (2 ^ m))"
haftmann@67960
   745
    by (simp add: ac_simps)
haftmann@67960
   746
  also have "\<dots> = a div of_nat (2 ^ n) div of_nat (2 ^ m)"
haftmann@67960
   747
    by (simp only: div_mult2_eq')
haftmann@67960
   748
  finally show ?thesis
haftmann@67960
   749
    by (simp add: drop_bit_eq_div power_add)
haftmann@67960
   750
qed
haftmann@67960
   751
haftmann@67960
   752
lemma push_bit_take_bit:
haftmann@67960
   753
  "push_bit m (take_bit n a) = take_bit (m + n) (push_bit m a)"
haftmann@67960
   754
  by (simp add: push_bit_eq_mult take_bit_eq_mod power_add mult_mod_right ac_simps)
haftmann@67960
   755
haftmann@67960
   756
lemma take_bit_push_bit:
haftmann@67960
   757
  "take_bit m (push_bit n a) = push_bit n (take_bit (m - n) a)"
haftmann@67960
   758
proof (cases "m \<le> n")
haftmann@67960
   759
  case True
haftmann@67960
   760
  then show ?thesis
haftmann@67960
   761
    by (simp_all add: push_bit_eq_mult take_bit_eq_mod mod_eq_0_iff_dvd dvd_power_le)
haftmann@67960
   762
next
haftmann@67960
   763
  case False
haftmann@67960
   764
  then show ?thesis
haftmann@67960
   765
    using push_bit_take_bit [of n "m - n" a]
haftmann@67960
   766
    by simp
haftmann@67960
   767
qed
haftmann@67960
   768
haftmann@67960
   769
lemma take_bit_drop_bit:
haftmann@67960
   770
  "take_bit m (drop_bit n a) = drop_bit n (take_bit (m + n) a)"
haftmann@67960
   771
  using mod_mult2_eq' [of a "2 ^ n" "2 ^ m"]
haftmann@67960
   772
  by (simp add: drop_bit_eq_div take_bit_eq_mod power_add ac_simps)
haftmann@67960
   773
haftmann@67960
   774
lemma drop_bit_take_bit:
haftmann@67960
   775
  "drop_bit m (take_bit n a) = take_bit (n - m) (drop_bit m a)"
haftmann@67960
   776
proof (cases "m \<le> n")
haftmann@67960
   777
  case True
haftmann@67960
   778
  then show ?thesis
haftmann@67960
   779
    using take_bit_drop_bit [of "n - m" m a] by simp
haftmann@67960
   780
next
haftmann@67960
   781
  case False
haftmann@67960
   782
  then have "a mod 2 ^ n div 2 ^ m = a mod 2 ^ n div 2 ^ (n + (m - n))"
haftmann@67960
   783
    by simp
haftmann@67960
   784
  also have "\<dots> = a mod 2 ^ n div (2 ^ n * 2 ^ (m - n))"
haftmann@67960
   785
    by (simp add: power_add)
haftmann@67960
   786
  also have "\<dots> = a mod 2 ^ n div (of_nat (2 ^ n) * of_nat (2 ^ (m - n)))"
haftmann@67960
   787
    by simp
haftmann@67960
   788
  also have "\<dots> = a mod 2 ^ n div of_nat (2 ^ n) div of_nat (2 ^ (m - n))"
haftmann@67960
   789
    by (simp only: div_mult2_eq')
haftmann@67960
   790
  finally show ?thesis
haftmann@67960
   791
    using False by (simp add: take_bit_eq_mod drop_bit_eq_div)
haftmann@67960
   792
qed
haftmann@67960
   793
haftmann@67988
   794
lemma push_bit_0_id [simp]:
haftmann@67988
   795
  "push_bit 0 = id"
haftmann@67988
   796
  by (simp add: fun_eq_iff push_bit_eq_mult)
haftmann@67988
   797
haftmann@67988
   798
lemma push_bit_of_0 [simp]:
haftmann@67988
   799
  "push_bit n 0 = 0"
haftmann@67988
   800
  by (simp add: push_bit_eq_mult)
haftmann@67988
   801
haftmann@67988
   802
lemma push_bit_of_1:
haftmann@67988
   803
  "push_bit n 1 = 2 ^ n"
haftmann@67988
   804
  by (simp add: push_bit_eq_mult)
haftmann@67988
   805
haftmann@67988
   806
lemma push_bit_Suc [simp]:
haftmann@67988
   807
  "push_bit (Suc n) a = push_bit n (a * 2)"
haftmann@67988
   808
  by (simp add: push_bit_eq_mult ac_simps)
haftmann@67988
   809
haftmann@67988
   810
lemma push_bit_double:
haftmann@67988
   811
  "push_bit n (a * 2) = push_bit n a * 2"
haftmann@67988
   812
  by (simp add: push_bit_eq_mult ac_simps)
haftmann@67988
   813
haftmann@67988
   814
lemma push_bit_eq_0_iff [simp]:
haftmann@67988
   815
  "push_bit n a = 0 \<longleftrightarrow> a = 0"
haftmann@67988
   816
  by (simp add: push_bit_eq_mult)
haftmann@67988
   817
haftmann@67988
   818
lemma push_bit_add:
haftmann@67988
   819
  "push_bit n (a + b) = push_bit n a + push_bit n b"
haftmann@67988
   820
  by (simp add: push_bit_eq_mult algebra_simps)
haftmann@67988
   821
haftmann@67988
   822
lemma push_bit_numeral [simp]:
haftmann@67988
   823
  "push_bit (numeral l) (numeral k) = push_bit (pred_numeral l) (numeral (Num.Bit0 k))"
haftmann@67988
   824
  by (simp only: numeral_eq_Suc power_Suc numeral_Bit0 [of k] mult_2 [symmetric]) (simp add: ac_simps)
haftmann@67988
   825
haftmann@68010
   826
lemma push_bit_of_nat:
haftmann@68010
   827
  "push_bit n (of_nat m) = of_nat (push_bit n m)"
haftmann@68010
   828
  by (simp add: push_bit_eq_mult Parity.push_bit_eq_mult)
haftmann@68010
   829
haftmann@67907
   830
lemma take_bit_0 [simp]:
haftmann@67907
   831
  "take_bit 0 a = 0"
haftmann@67907
   832
  by (simp add: take_bit_eq_mod)
haftmann@67816
   833
haftmann@67907
   834
lemma take_bit_Suc [simp]:
haftmann@67907
   835
  "take_bit (Suc n) a = take_bit n (a div 2) * 2 + of_bool (odd a)"
haftmann@67816
   836
proof -
haftmann@67816
   837
  have "1 + 2 * (a div 2) mod (2 * 2 ^ n) = (a div 2 * 2 + a mod 2) mod (2 * 2 ^ n)"
haftmann@67816
   838
    if "odd a"
haftmann@67816
   839
    using that mod_mult2_eq' [of "1 + 2 * (a div 2)" 2 "2 ^ n"]
haftmann@67816
   840
    by (simp add: ac_simps odd_iff_mod_2_eq_one mult_mod_right)
haftmann@67816
   841
  also have "\<dots> = a mod (2 * 2 ^ n)"
haftmann@67816
   842
    by (simp only: div_mult_mod_eq)
haftmann@67816
   843
  finally show ?thesis
haftmann@67907
   844
    by (simp add: take_bit_eq_mod algebra_simps mult_mod_right)
haftmann@67816
   845
qed
haftmann@67816
   846
haftmann@67907
   847
lemma take_bit_of_0 [simp]:
haftmann@67907
   848
  "take_bit n 0 = 0"
haftmann@67907
   849
  by (simp add: take_bit_eq_mod)
haftmann@67816
   850
haftmann@67988
   851
lemma take_bit_of_1 [simp]:
haftmann@67988
   852
  "take_bit n 1 = of_bool (n > 0)"
haftmann@67988
   853
  by (simp add: take_bit_eq_mod)
haftmann@67988
   854
haftmann@67961
   855
lemma take_bit_add:
haftmann@67907
   856
  "take_bit n (take_bit n a + take_bit n b) = take_bit n (a + b)"
haftmann@67907
   857
  by (simp add: take_bit_eq_mod mod_simps)
haftmann@67816
   858
haftmann@67961
   859
lemma take_bit_eq_0_iff:
haftmann@67961
   860
  "take_bit n a = 0 \<longleftrightarrow> 2 ^ n dvd a"
haftmann@67961
   861
  by (simp add: take_bit_eq_mod mod_eq_0_iff_dvd)
haftmann@67961
   862
haftmann@67907
   863
lemma take_bit_of_1_eq_0_iff [simp]:
haftmann@67907
   864
  "take_bit n 1 = 0 \<longleftrightarrow> n = 0"
haftmann@67907
   865
  by (simp add: take_bit_eq_mod)
haftmann@67816
   866
haftmann@67988
   867
lemma even_take_bit_eq [simp]:
haftmann@67988
   868
  "even (take_bit n a) \<longleftrightarrow> n = 0 \<or> even a"
haftmann@67988
   869
  by (cases n) (simp_all add: take_bit_eq_mod dvd_mod_iff)
haftmann@67816
   870
haftmann@67988
   871
lemma take_bit_numeral_bit0 [simp]:
haftmann@67988
   872
  "take_bit (numeral l) (numeral (Num.Bit0 k)) = take_bit (pred_numeral l) (numeral k) * 2"
haftmann@67988
   873
  by (simp only: numeral_eq_Suc power_Suc numeral_Bit0 [of k] mult_2 [symmetric] take_bit_Suc
haftmann@67988
   874
    ac_simps even_mult_iff nonzero_mult_div_cancel_right [OF numeral_neq_zero]) simp
haftmann@67988
   875
haftmann@67988
   876
lemma take_bit_numeral_bit1 [simp]:
haftmann@67988
   877
  "take_bit (numeral l) (numeral (Num.Bit1 k)) = take_bit (pred_numeral l) (numeral k) * 2 + 1"
haftmann@67988
   878
  by (simp only: numeral_eq_Suc power_Suc numeral_Bit1 [of k] mult_2 [symmetric] take_bit_Suc
haftmann@67988
   879
    ac_simps even_add even_mult_iff div_mult_self1 [OF numeral_neq_zero]) (simp add: ac_simps)
haftmann@67961
   880
haftmann@68010
   881
lemma take_bit_of_nat:
haftmann@68010
   882
  "take_bit n (of_nat m) = of_nat (take_bit n m)"
haftmann@68010
   883
  by (simp add: take_bit_eq_mod Parity.take_bit_eq_mod of_nat_mod [of m "2 ^ n"])
haftmann@68010
   884
haftmann@67907
   885
lemma drop_bit_0 [simp]:
haftmann@67907
   886
  "drop_bit 0 = id"
haftmann@67907
   887
  by (simp add: fun_eq_iff drop_bit_eq_div)
haftmann@67816
   888
haftmann@67907
   889
lemma drop_bit_of_0 [simp]:
haftmann@67907
   890
  "drop_bit n 0 = 0"
haftmann@67907
   891
  by (simp add: drop_bit_eq_div)
haftmann@67816
   892
haftmann@67988
   893
lemma drop_bit_of_1 [simp]:
haftmann@67988
   894
  "drop_bit n 1 = of_bool (n = 0)"
haftmann@67988
   895
  by (simp add: drop_bit_eq_div)
haftmann@67988
   896
haftmann@67907
   897
lemma drop_bit_Suc [simp]:
haftmann@67907
   898
  "drop_bit (Suc n) a = drop_bit n (a div 2)"
haftmann@67816
   899
proof (cases "even a")
haftmann@67816
   900
  case True
haftmann@67816
   901
  then obtain b where "a = 2 * b" ..
haftmann@67907
   902
  moreover have "drop_bit (Suc n) (2 * b) = drop_bit n b"
haftmann@67907
   903
    by (simp add: drop_bit_eq_div)
haftmann@67816
   904
  ultimately show ?thesis
haftmann@67816
   905
    by simp
haftmann@67816
   906
next
haftmann@67816
   907
  case False
haftmann@67816
   908
  then obtain b where "a = 2 * b + 1" ..
haftmann@67907
   909
  moreover have "drop_bit (Suc n) (2 * b + 1) = drop_bit n b"
haftmann@67816
   910
    using div_mult2_eq' [of "1 + b * 2" 2 "2 ^ n"]
haftmann@67907
   911
    by (auto simp add: drop_bit_eq_div ac_simps)
haftmann@67816
   912
  ultimately show ?thesis
haftmann@67816
   913
    by simp
haftmann@67816
   914
qed
haftmann@67816
   915
haftmann@67907
   916
lemma drop_bit_half:
haftmann@67907
   917
  "drop_bit n (a div 2) = drop_bit n a div 2"
haftmann@67816
   918
  by (induction n arbitrary: a) simp_all
haftmann@67816
   919
haftmann@67907
   920
lemma drop_bit_of_bool [simp]:
haftmann@67907
   921
  "drop_bit n (of_bool d) = of_bool (n = 0 \<and> d)"
haftmann@67816
   922
  by (cases n) simp_all
haftmann@67816
   923
haftmann@67988
   924
lemma drop_bit_numeral_bit0 [simp]:
haftmann@67988
   925
  "drop_bit (numeral l) (numeral (Num.Bit0 k)) = drop_bit (pred_numeral l) (numeral k)"
haftmann@67988
   926
  by (simp only: numeral_eq_Suc power_Suc numeral_Bit0 [of k] mult_2 [symmetric] drop_bit_Suc
haftmann@67988
   927
    nonzero_mult_div_cancel_left [OF numeral_neq_zero])
haftmann@67816
   928
haftmann@67988
   929
lemma drop_bit_numeral_bit1 [simp]:
haftmann@67988
   930
  "drop_bit (numeral l) (numeral (Num.Bit1 k)) = drop_bit (pred_numeral l) (numeral k)"
haftmann@67988
   931
  by (simp only: numeral_eq_Suc power_Suc numeral_Bit1 [of k] mult_2 [symmetric] drop_bit_Suc
haftmann@67988
   932
    div_mult_self4 [OF numeral_neq_zero]) simp
haftmann@67816
   933
haftmann@68010
   934
lemma drop_bit_of_nat:
haftmann@68010
   935
  "drop_bit n (of_nat m) = of_nat (drop_bit n m)"
haftmann@68010
   936
	by (simp add: drop_bit_eq_div Parity.drop_bit_eq_div of_nat_div [of m "2 ^ n"])
haftmann@68010
   937
haftmann@58770
   938
end
haftmann@67816
   939
haftmann@67988
   940
lemma push_bit_of_Suc_0 [simp]:
haftmann@67988
   941
  "push_bit n (Suc 0) = 2 ^ n"
haftmann@67988
   942
  using push_bit_of_1 [where ?'a = nat] by simp
haftmann@67988
   943
haftmann@67988
   944
lemma take_bit_of_Suc_0 [simp]:
haftmann@67988
   945
  "take_bit n (Suc 0) = of_bool (0 < n)"
haftmann@67988
   946
  using take_bit_of_1 [where ?'a = nat] by simp
haftmann@67988
   947
haftmann@67988
   948
lemma drop_bit_of_Suc_0 [simp]:
haftmann@67988
   949
  "drop_bit n (Suc 0) = of_bool (n = 0)"
haftmann@67988
   950
  using drop_bit_of_1 [where ?'a = nat] by simp
haftmann@67988
   951
haftmann@67816
   952
end