src/HOL/Word/Bits_Int.thy
author paulson <lp15@cam.ac.uk>
Tue Apr 25 16:39:54 2017 +0100 (2017-04-25)
changeset 65578 e4997c181cce
parent 65363 5eb619751b14
child 67120 491fd7f0b5df
permissions -rw-r--r--
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
wenzelm@65363
     1
(*  Title:      HOL/Word/Bits_Int.thy
wenzelm@65363
     2
    Author:     Jeremy Dawson and Gerwin Klein, NICTA
kleing@24333
     3
wenzelm@65363
     4
Definitions and basic theorems for bit-wise logical operations
wenzelm@65363
     5
for integers expressed using Pls, Min, BIT,
wenzelm@65363
     6
and converting them to and from lists of bools.
wenzelm@65363
     7
*)
kleing@24333
     8
wenzelm@61799
     9
section \<open>Bitwise Operations on Binary Integers\<close>
huffman@24350
    10
haftmann@54854
    11
theory Bits_Int
wenzelm@65363
    12
  imports Bits Bit_Representation
kleing@24333
    13
begin
kleing@24333
    14
wenzelm@61799
    15
subsection \<open>Logical operations\<close>
huffman@24353
    16
huffman@24353
    17
text "bit-wise logical operations on the int type"
huffman@24353
    18
haftmann@25762
    19
instantiation int :: bit
haftmann@25762
    20
begin
haftmann@25762
    21
wenzelm@65363
    22
definition int_not_def: "bitNOT = (\<lambda>x::int. - x - 1)"
huffman@46019
    23
wenzelm@65363
    24
function bitAND_int
wenzelm@65363
    25
  where "bitAND_int x y =
wenzelm@65363
    26
    (if x = 0 then 0 else if x = -1 then y
wenzelm@65363
    27
     else (bin_rest x AND bin_rest y) BIT (bin_last x \<and> bin_last y))"
huffman@46019
    28
  by pat_completeness simp
haftmann@25762
    29
huffman@46019
    30
termination
wenzelm@65363
    31
  by (relation "measure (nat \<circ> abs \<circ> fst)", simp_all add: bin_rest_def)
huffman@46019
    32
huffman@46019
    33
declare bitAND_int.simps [simp del]
haftmann@25762
    34
huffman@46019
    35
definition int_or_def:
huffman@46019
    36
  "bitOR = (\<lambda>x y::int. NOT (NOT x AND NOT y))"
haftmann@25762
    37
huffman@46019
    38
definition int_xor_def:
huffman@46019
    39
  "bitXOR = (\<lambda>x y::int. (x AND NOT y) OR (NOT x AND y))"
haftmann@25762
    40
haftmann@25762
    41
instance ..
haftmann@25762
    42
haftmann@25762
    43
end
huffman@24353
    44
wenzelm@61799
    45
subsubsection \<open>Basic simplification rules\<close>
huffman@45543
    46
huffman@46016
    47
lemma int_not_BIT [simp]:
haftmann@54847
    48
  "NOT (w BIT b) = (NOT w) BIT (\<not> b)"
huffman@46016
    49
  unfolding int_not_def Bit_def by (cases b, simp_all)
huffman@46016
    50
kleing@24333
    51
lemma int_not_simps [simp]:
huffman@47108
    52
  "NOT (0::int) = -1"
huffman@47108
    53
  "NOT (1::int) = -2"
haftmann@54489
    54
  "NOT (- 1::int) = 0"
haftmann@54489
    55
  "NOT (numeral w::int) = - numeral (w + Num.One)"
haftmann@54489
    56
  "NOT (- numeral (Num.Bit0 w)::int) = numeral (Num.BitM w)"
haftmann@54489
    57
  "NOT (- numeral (Num.Bit1 w)::int) = numeral (Num.Bit0 w)"
huffman@47108
    58
  unfolding int_not_def by simp_all
kleing@24333
    59
huffman@46017
    60
lemma int_not_not [simp]: "NOT (NOT (x::int)) = x"
huffman@46017
    61
  unfolding int_not_def by simp
huffman@46017
    62
huffman@46019
    63
lemma int_and_0 [simp]: "(0::int) AND x = 0"
huffman@46019
    64
  by (simp add: bitAND_int.simps)
huffman@46019
    65
huffman@46019
    66
lemma int_and_m1 [simp]: "(-1::int) AND x = x"
huffman@46019
    67
  by (simp add: bitAND_int.simps)
huffman@46019
    68
wenzelm@65363
    69
lemma int_and_Bits [simp]:
wenzelm@65363
    70
  "(x BIT b) AND (y BIT c) = (x AND y) BIT (b \<and> c)"
huffman@46019
    71
  by (subst bitAND_int.simps, simp add: Bit_eq_0_iff Bit_eq_m1_iff)
huffman@46017
    72
huffman@47108
    73
lemma int_or_zero [simp]: "(0::int) OR x = x"
huffman@46017
    74
  unfolding int_or_def by simp
huffman@46018
    75
huffman@47108
    76
lemma int_or_minus1 [simp]: "(-1::int) OR x = -1"
huffman@46017
    77
  unfolding int_or_def by simp
huffman@46017
    78
wenzelm@65363
    79
lemma int_or_Bits [simp]:
haftmann@54847
    80
  "(x BIT b) OR (y BIT c) = (x OR y) BIT (b \<or> c)"
haftmann@54847
    81
  unfolding int_or_def by simp
kleing@24333
    82
huffman@47108
    83
lemma int_xor_zero [simp]: "(0::int) XOR x = x"
huffman@46018
    84
  unfolding int_xor_def by simp
huffman@46018
    85
wenzelm@65363
    86
lemma int_xor_Bits [simp]:
haftmann@54847
    87
  "(x BIT b) XOR (y BIT c) = (x XOR y) BIT ((b \<or> c) \<and> \<not> (b \<and> c))"
haftmann@54847
    88
  unfolding int_xor_def by auto
huffman@46018
    89
wenzelm@61799
    90
subsubsection \<open>Binary destructors\<close>
huffman@45543
    91
huffman@45543
    92
lemma bin_rest_NOT [simp]: "bin_rest (NOT x) = NOT (bin_rest x)"
huffman@45543
    93
  by (cases x rule: bin_exhaust, simp)
huffman@45543
    94
haftmann@54847
    95
lemma bin_last_NOT [simp]: "bin_last (NOT x) \<longleftrightarrow> \<not> bin_last x"
huffman@45543
    96
  by (cases x rule: bin_exhaust, simp)
huffman@45543
    97
huffman@45543
    98
lemma bin_rest_AND [simp]: "bin_rest (x AND y) = bin_rest x AND bin_rest y"
huffman@45543
    99
  by (cases x rule: bin_exhaust, cases y rule: bin_exhaust, simp)
huffman@45543
   100
haftmann@54847
   101
lemma bin_last_AND [simp]: "bin_last (x AND y) \<longleftrightarrow> bin_last x \<and> bin_last y"
huffman@45543
   102
  by (cases x rule: bin_exhaust, cases y rule: bin_exhaust, simp)
huffman@45543
   103
huffman@45543
   104
lemma bin_rest_OR [simp]: "bin_rest (x OR y) = bin_rest x OR bin_rest y"
huffman@45543
   105
  by (cases x rule: bin_exhaust, cases y rule: bin_exhaust, simp)
huffman@45543
   106
haftmann@54847
   107
lemma bin_last_OR [simp]: "bin_last (x OR y) \<longleftrightarrow> bin_last x \<or> bin_last y"
huffman@45543
   108
  by (cases x rule: bin_exhaust, cases y rule: bin_exhaust, simp)
huffman@45543
   109
huffman@45543
   110
lemma bin_rest_XOR [simp]: "bin_rest (x XOR y) = bin_rest x XOR bin_rest y"
huffman@45543
   111
  by (cases x rule: bin_exhaust, cases y rule: bin_exhaust, simp)
huffman@45543
   112
haftmann@54847
   113
lemma bin_last_XOR [simp]: "bin_last (x XOR y) \<longleftrightarrow> (bin_last x \<or> bin_last y) \<and> \<not> (bin_last x \<and> bin_last y)"
huffman@45543
   114
  by (cases x rule: bin_exhaust, cases y rule: bin_exhaust, simp)
huffman@45543
   115
huffman@45543
   116
lemma bin_nth_ops:
wenzelm@65363
   117
  "!!x y. bin_nth (x AND y) n = (bin_nth x n & bin_nth y n)"
huffman@45543
   118
  "!!x y. bin_nth (x OR y) n = (bin_nth x n | bin_nth y n)"
wenzelm@65363
   119
  "!!x y. bin_nth (x XOR y) n = (bin_nth x n ~= bin_nth y n)"
huffman@45543
   120
  "!!x. bin_nth (NOT x) n = (~ bin_nth x n)"
huffman@45543
   121
  by (induct n) auto
huffman@45543
   122
wenzelm@61799
   123
subsubsection \<open>Derived properties\<close>
huffman@45543
   124
huffman@47108
   125
lemma int_xor_minus1 [simp]: "(-1::int) XOR x = NOT x"
huffman@46018
   126
  by (auto simp add: bin_eq_iff bin_nth_ops)
huffman@46018
   127
huffman@45543
   128
lemma int_xor_extra_simps [simp]:
huffman@47108
   129
  "w XOR (0::int) = w"
huffman@47108
   130
  "w XOR (-1::int) = NOT w"
huffman@45543
   131
  by (auto simp add: bin_eq_iff bin_nth_ops)
huffman@45543
   132
huffman@45543
   133
lemma int_or_extra_simps [simp]:
huffman@47108
   134
  "w OR (0::int) = w"
huffman@47108
   135
  "w OR (-1::int) = -1"
huffman@45543
   136
  by (auto simp add: bin_eq_iff bin_nth_ops)
kleing@24333
   137
haftmann@37667
   138
lemma int_and_extra_simps [simp]:
huffman@47108
   139
  "w AND (0::int) = 0"
huffman@47108
   140
  "w AND (-1::int) = w"
huffman@45543
   141
  by (auto simp add: bin_eq_iff bin_nth_ops)
kleing@24333
   142
kleing@24333
   143
(* commutativity of the above *)
kleing@24333
   144
lemma bin_ops_comm:
kleing@24333
   145
  shows
huffman@24353
   146
  int_and_comm: "!!y::int. x AND y = y AND x" and
huffman@24353
   147
  int_or_comm:  "!!y::int. x OR y = y OR x" and
huffman@24353
   148
  int_xor_comm: "!!y::int. x XOR y = y XOR x"
huffman@45543
   149
  by (auto simp add: bin_eq_iff bin_nth_ops)
kleing@24333
   150
kleing@24333
   151
lemma bin_ops_same [simp]:
wenzelm@65363
   152
  "(x::int) AND x = x"
wenzelm@65363
   153
  "(x::int) OR x = x"
huffman@47108
   154
  "(x::int) XOR x = 0"
huffman@45543
   155
  by (auto simp add: bin_eq_iff bin_nth_ops)
kleing@24333
   156
wenzelm@65363
   157
lemmas bin_log_esimps =
kleing@24333
   158
  int_and_extra_simps  int_or_extra_simps  int_xor_extra_simps
huffman@47108
   159
  int_and_0 int_and_m1 int_or_zero int_or_minus1 int_xor_zero int_xor_minus1
kleing@24333
   160
kleing@24333
   161
(* basic properties of logical (bit-wise) operations *)
kleing@24333
   162
wenzelm@65363
   163
lemma bbw_ao_absorb:
huffman@24353
   164
  "!!y::int. x AND (y OR x) = x & x OR (y AND x) = x"
huffman@45543
   165
  by (auto simp add: bin_eq_iff bin_nth_ops)
kleing@24333
   166
kleing@24333
   167
lemma bbw_ao_absorbs_other:
huffman@24353
   168
  "x AND (x OR y) = x \<and> (y AND x) OR x = (x::int)"
huffman@24353
   169
  "(y OR x) AND x = x \<and> x OR (x AND y) = (x::int)"
huffman@24353
   170
  "(x OR y) AND x = x \<and> (x AND y) OR x = (x::int)"
huffman@45543
   171
  by (auto simp add: bin_eq_iff bin_nth_ops)
huffman@24353
   172
kleing@24333
   173
lemmas bbw_ao_absorbs [simp] = bbw_ao_absorb bbw_ao_absorbs_other
kleing@24333
   174
kleing@24333
   175
lemma int_xor_not:
wenzelm@65363
   176
  "!!y::int. (NOT x) XOR y = NOT (x XOR y) &
huffman@24353
   177
        x XOR (NOT y) = NOT (x XOR y)"
huffman@45543
   178
  by (auto simp add: bin_eq_iff bin_nth_ops)
kleing@24333
   179
kleing@24333
   180
lemma int_and_assoc:
huffman@24353
   181
  "(x AND y) AND (z::int) = x AND (y AND z)"
huffman@45543
   182
  by (auto simp add: bin_eq_iff bin_nth_ops)
kleing@24333
   183
kleing@24333
   184
lemma int_or_assoc:
huffman@24353
   185
  "(x OR y) OR (z::int) = x OR (y OR z)"
huffman@45543
   186
  by (auto simp add: bin_eq_iff bin_nth_ops)
kleing@24333
   187
kleing@24333
   188
lemma int_xor_assoc:
huffman@24353
   189
  "(x XOR y) XOR (z::int) = x XOR (y XOR z)"
huffman@45543
   190
  by (auto simp add: bin_eq_iff bin_nth_ops)
kleing@24333
   191
kleing@24333
   192
lemmas bbw_assocs = int_and_assoc int_or_assoc int_xor_assoc
kleing@24333
   193
huffman@45543
   194
(* BH: Why are these declared as simp rules??? *)
wenzelm@65363
   195
lemma bbw_lcs [simp]:
huffman@24353
   196
  "(y::int) AND (x AND z) = x AND (y AND z)"
huffman@24353
   197
  "(y::int) OR (x OR z) = x OR (y OR z)"
wenzelm@65363
   198
  "(y::int) XOR (x XOR z) = x XOR (y XOR z)"
huffman@45543
   199
  by (auto simp add: bin_eq_iff bin_nth_ops)
kleing@24333
   200
wenzelm@65363
   201
lemma bbw_not_dist:
wenzelm@65363
   202
  "!!y::int. NOT (x OR y) = (NOT x) AND (NOT y)"
huffman@24353
   203
  "!!y::int. NOT (x AND y) = (NOT x) OR (NOT y)"
huffman@45543
   204
  by (auto simp add: bin_eq_iff bin_nth_ops)
kleing@24333
   205
wenzelm@65363
   206
lemma bbw_oa_dist:
wenzelm@65363
   207
  "!!y z::int. (x AND y) OR z =
huffman@24353
   208
          (x OR z) AND (y OR z)"
huffman@45543
   209
  by (auto simp add: bin_eq_iff bin_nth_ops)
kleing@24333
   210
wenzelm@65363
   211
lemma bbw_ao_dist:
wenzelm@65363
   212
  "!!y z::int. (x OR y) AND z =
huffman@24353
   213
          (x AND z) OR (y AND z)"
huffman@45543
   214
  by (auto simp add: bin_eq_iff bin_nth_ops)
kleing@24333
   215
huffman@24367
   216
(*
huffman@24367
   217
Why were these declared simp???
wenzelm@65363
   218
declare bin_ops_comm [simp] bbw_assocs [simp]
huffman@24367
   219
*)
kleing@24333
   220
wenzelm@61799
   221
subsubsection \<open>Simplification with numerals\<close>
huffman@47108
   222
wenzelm@61799
   223
text \<open>Cases for \<open>0\<close> and \<open>-1\<close> are already covered by
wenzelm@61799
   224
  other simp rules.\<close>
huffman@47108
   225
huffman@47108
   226
lemma bin_rl_eqI: "\<lbrakk>bin_rest x = bin_rest y; bin_last x = bin_last y\<rbrakk> \<Longrightarrow> x = y"
haftmann@54847
   227
  by (metis (mono_tags) BIT_eq_iff bin_ex_rl bin_last_BIT bin_rest_BIT)
huffman@47108
   228
huffman@47108
   229
lemma bin_rest_neg_numeral_BitM [simp]:
haftmann@54489
   230
  "bin_rest (- numeral (Num.BitM w)) = - numeral w"
huffman@47108
   231
  by (simp only: BIT_bin_simps [symmetric] bin_rest_BIT)
huffman@47108
   232
huffman@47108
   233
lemma bin_last_neg_numeral_BitM [simp]:
haftmann@54847
   234
  "bin_last (- numeral (Num.BitM w))"
huffman@47108
   235
  by (simp only: BIT_bin_simps [symmetric] bin_last_BIT)
huffman@47108
   236
wenzelm@61799
   237
text \<open>FIXME: The rule sets below are very large (24 rules for each
wenzelm@61799
   238
  operator). Is there a simpler way to do this?\<close>
huffman@47108
   239
huffman@47108
   240
lemma int_and_numerals [simp]:
haftmann@54847
   241
  "numeral (Num.Bit0 x) AND numeral (Num.Bit0 y) = (numeral x AND numeral y) BIT False"
haftmann@54847
   242
  "numeral (Num.Bit0 x) AND numeral (Num.Bit1 y) = (numeral x AND numeral y) BIT False"
haftmann@54847
   243
  "numeral (Num.Bit1 x) AND numeral (Num.Bit0 y) = (numeral x AND numeral y) BIT False"
haftmann@54847
   244
  "numeral (Num.Bit1 x) AND numeral (Num.Bit1 y) = (numeral x AND numeral y) BIT True"
haftmann@54847
   245
  "numeral (Num.Bit0 x) AND - numeral (Num.Bit0 y) = (numeral x AND - numeral y) BIT False"
haftmann@54847
   246
  "numeral (Num.Bit0 x) AND - numeral (Num.Bit1 y) = (numeral x AND - numeral (y + Num.One)) BIT False"
haftmann@54847
   247
  "numeral (Num.Bit1 x) AND - numeral (Num.Bit0 y) = (numeral x AND - numeral y) BIT False"
haftmann@54847
   248
  "numeral (Num.Bit1 x) AND - numeral (Num.Bit1 y) = (numeral x AND - numeral (y + Num.One)) BIT True"
haftmann@54847
   249
  "- numeral (Num.Bit0 x) AND numeral (Num.Bit0 y) = (- numeral x AND numeral y) BIT False"
haftmann@54847
   250
  "- numeral (Num.Bit0 x) AND numeral (Num.Bit1 y) = (- numeral x AND numeral y) BIT False"
haftmann@54847
   251
  "- numeral (Num.Bit1 x) AND numeral (Num.Bit0 y) = (- numeral (x + Num.One) AND numeral y) BIT False"
haftmann@54847
   252
  "- numeral (Num.Bit1 x) AND numeral (Num.Bit1 y) = (- numeral (x + Num.One) AND numeral y) BIT True"
haftmann@54847
   253
  "- numeral (Num.Bit0 x) AND - numeral (Num.Bit0 y) = (- numeral x AND - numeral y) BIT False"
haftmann@54847
   254
  "- numeral (Num.Bit0 x) AND - numeral (Num.Bit1 y) = (- numeral x AND - numeral (y + Num.One)) BIT False"
haftmann@54847
   255
  "- numeral (Num.Bit1 x) AND - numeral (Num.Bit0 y) = (- numeral (x + Num.One) AND - numeral y) BIT False"
haftmann@54847
   256
  "- numeral (Num.Bit1 x) AND - numeral (Num.Bit1 y) = (- numeral (x + Num.One) AND - numeral (y + Num.One)) BIT True"
huffman@47108
   257
  "(1::int) AND numeral (Num.Bit0 y) = 0"
huffman@47108
   258
  "(1::int) AND numeral (Num.Bit1 y) = 1"
haftmann@54489
   259
  "(1::int) AND - numeral (Num.Bit0 y) = 0"
haftmann@54489
   260
  "(1::int) AND - numeral (Num.Bit1 y) = 1"
huffman@47108
   261
  "numeral (Num.Bit0 x) AND (1::int) = 0"
huffman@47108
   262
  "numeral (Num.Bit1 x) AND (1::int) = 1"
haftmann@54489
   263
  "- numeral (Num.Bit0 x) AND (1::int) = 0"
haftmann@54489
   264
  "- numeral (Num.Bit1 x) AND (1::int) = 1"
huffman@47108
   265
  by (rule bin_rl_eqI, simp, simp)+
huffman@47108
   266
huffman@47108
   267
lemma int_or_numerals [simp]:
haftmann@54847
   268
  "numeral (Num.Bit0 x) OR numeral (Num.Bit0 y) = (numeral x OR numeral y) BIT False"
haftmann@54847
   269
  "numeral (Num.Bit0 x) OR numeral (Num.Bit1 y) = (numeral x OR numeral y) BIT True"
haftmann@54847
   270
  "numeral (Num.Bit1 x) OR numeral (Num.Bit0 y) = (numeral x OR numeral y) BIT True"
haftmann@54847
   271
  "numeral (Num.Bit1 x) OR numeral (Num.Bit1 y) = (numeral x OR numeral y) BIT True"
haftmann@54847
   272
  "numeral (Num.Bit0 x) OR - numeral (Num.Bit0 y) = (numeral x OR - numeral y) BIT False"
haftmann@54847
   273
  "numeral (Num.Bit0 x) OR - numeral (Num.Bit1 y) = (numeral x OR - numeral (y + Num.One)) BIT True"
haftmann@54847
   274
  "numeral (Num.Bit1 x) OR - numeral (Num.Bit0 y) = (numeral x OR - numeral y) BIT True"
haftmann@54847
   275
  "numeral (Num.Bit1 x) OR - numeral (Num.Bit1 y) = (numeral x OR - numeral (y + Num.One)) BIT True"
haftmann@54847
   276
  "- numeral (Num.Bit0 x) OR numeral (Num.Bit0 y) = (- numeral x OR numeral y) BIT False"
haftmann@54847
   277
  "- numeral (Num.Bit0 x) OR numeral (Num.Bit1 y) = (- numeral x OR numeral y) BIT True"
haftmann@54847
   278
  "- numeral (Num.Bit1 x) OR numeral (Num.Bit0 y) = (- numeral (x + Num.One) OR numeral y) BIT True"
haftmann@54847
   279
  "- numeral (Num.Bit1 x) OR numeral (Num.Bit1 y) = (- numeral (x + Num.One) OR numeral y) BIT True"
haftmann@54847
   280
  "- numeral (Num.Bit0 x) OR - numeral (Num.Bit0 y) = (- numeral x OR - numeral y) BIT False"
haftmann@54847
   281
  "- numeral (Num.Bit0 x) OR - numeral (Num.Bit1 y) = (- numeral x OR - numeral (y + Num.One)) BIT True"
haftmann@54847
   282
  "- numeral (Num.Bit1 x) OR - numeral (Num.Bit0 y) = (- numeral (x + Num.One) OR - numeral y) BIT True"
haftmann@54847
   283
  "- numeral (Num.Bit1 x) OR - numeral (Num.Bit1 y) = (- numeral (x + Num.One) OR - numeral (y + Num.One)) BIT True"
huffman@47108
   284
  "(1::int) OR numeral (Num.Bit0 y) = numeral (Num.Bit1 y)"
huffman@47108
   285
  "(1::int) OR numeral (Num.Bit1 y) = numeral (Num.Bit1 y)"
haftmann@54489
   286
  "(1::int) OR - numeral (Num.Bit0 y) = - numeral (Num.BitM y)"
haftmann@54489
   287
  "(1::int) OR - numeral (Num.Bit1 y) = - numeral (Num.Bit1 y)"
huffman@47108
   288
  "numeral (Num.Bit0 x) OR (1::int) = numeral (Num.Bit1 x)"
huffman@47108
   289
  "numeral (Num.Bit1 x) OR (1::int) = numeral (Num.Bit1 x)"
haftmann@54489
   290
  "- numeral (Num.Bit0 x) OR (1::int) = - numeral (Num.BitM x)"
haftmann@54489
   291
  "- numeral (Num.Bit1 x) OR (1::int) = - numeral (Num.Bit1 x)"
huffman@47108
   292
  by (rule bin_rl_eqI, simp, simp)+
huffman@47108
   293
huffman@47108
   294
lemma int_xor_numerals [simp]:
haftmann@54847
   295
  "numeral (Num.Bit0 x) XOR numeral (Num.Bit0 y) = (numeral x XOR numeral y) BIT False"
haftmann@54847
   296
  "numeral (Num.Bit0 x) XOR numeral (Num.Bit1 y) = (numeral x XOR numeral y) BIT True"
haftmann@54847
   297
  "numeral (Num.Bit1 x) XOR numeral (Num.Bit0 y) = (numeral x XOR numeral y) BIT True"
haftmann@54847
   298
  "numeral (Num.Bit1 x) XOR numeral (Num.Bit1 y) = (numeral x XOR numeral y) BIT False"
haftmann@54847
   299
  "numeral (Num.Bit0 x) XOR - numeral (Num.Bit0 y) = (numeral x XOR - numeral y) BIT False"
haftmann@54847
   300
  "numeral (Num.Bit0 x) XOR - numeral (Num.Bit1 y) = (numeral x XOR - numeral (y + Num.One)) BIT True"
haftmann@54847
   301
  "numeral (Num.Bit1 x) XOR - numeral (Num.Bit0 y) = (numeral x XOR - numeral y) BIT True"
haftmann@54847
   302
  "numeral (Num.Bit1 x) XOR - numeral (Num.Bit1 y) = (numeral x XOR - numeral (y + Num.One)) BIT False"
haftmann@54847
   303
  "- numeral (Num.Bit0 x) XOR numeral (Num.Bit0 y) = (- numeral x XOR numeral y) BIT False"
haftmann@54847
   304
  "- numeral (Num.Bit0 x) XOR numeral (Num.Bit1 y) = (- numeral x XOR numeral y) BIT True"
haftmann@54847
   305
  "- numeral (Num.Bit1 x) XOR numeral (Num.Bit0 y) = (- numeral (x + Num.One) XOR numeral y) BIT True"
haftmann@54847
   306
  "- numeral (Num.Bit1 x) XOR numeral (Num.Bit1 y) = (- numeral (x + Num.One) XOR numeral y) BIT False"
haftmann@54847
   307
  "- numeral (Num.Bit0 x) XOR - numeral (Num.Bit0 y) = (- numeral x XOR - numeral y) BIT False"
haftmann@54847
   308
  "- numeral (Num.Bit0 x) XOR - numeral (Num.Bit1 y) = (- numeral x XOR - numeral (y + Num.One)) BIT True"
haftmann@54847
   309
  "- numeral (Num.Bit1 x) XOR - numeral (Num.Bit0 y) = (- numeral (x + Num.One) XOR - numeral y) BIT True"
haftmann@54847
   310
  "- numeral (Num.Bit1 x) XOR - numeral (Num.Bit1 y) = (- numeral (x + Num.One) XOR - numeral (y + Num.One)) BIT False"
huffman@47108
   311
  "(1::int) XOR numeral (Num.Bit0 y) = numeral (Num.Bit1 y)"
huffman@47108
   312
  "(1::int) XOR numeral (Num.Bit1 y) = numeral (Num.Bit0 y)"
haftmann@54489
   313
  "(1::int) XOR - numeral (Num.Bit0 y) = - numeral (Num.BitM y)"
haftmann@54489
   314
  "(1::int) XOR - numeral (Num.Bit1 y) = - numeral (Num.Bit0 (y + Num.One))"
huffman@47108
   315
  "numeral (Num.Bit0 x) XOR (1::int) = numeral (Num.Bit1 x)"
huffman@47108
   316
  "numeral (Num.Bit1 x) XOR (1::int) = numeral (Num.Bit0 x)"
haftmann@54489
   317
  "- numeral (Num.Bit0 x) XOR (1::int) = - numeral (Num.BitM x)"
haftmann@54489
   318
  "- numeral (Num.Bit1 x) XOR (1::int) = - numeral (Num.Bit0 (x + Num.One))"
huffman@47108
   319
  by (rule bin_rl_eqI, simp, simp)+
huffman@47108
   320
wenzelm@61799
   321
subsubsection \<open>Interactions with arithmetic\<close>
huffman@45543
   322
kleing@24333
   323
lemma plus_and_or [rule_format]:
huffman@24353
   324
  "ALL y::int. (x AND y) + (x OR y) = x + y"
kleing@24333
   325
  apply (induct x rule: bin_induct)
kleing@24333
   326
    apply clarsimp
kleing@24333
   327
   apply clarsimp
kleing@24333
   328
  apply clarsimp
kleing@24333
   329
  apply (case_tac y rule: bin_exhaust)
kleing@24333
   330
  apply clarsimp
kleing@24333
   331
  apply (unfold Bit_def)
kleing@24333
   332
  apply clarsimp
kleing@24333
   333
  apply (erule_tac x = "x" in allE)
haftmann@54847
   334
  apply simp
kleing@24333
   335
  done
kleing@24333
   336
kleing@24333
   337
lemma le_int_or:
huffman@46604
   338
  "bin_sign (y::int) = 0 ==> x <= x OR y"
haftmann@37667
   339
  apply (induct y arbitrary: x rule: bin_induct)
kleing@24333
   340
    apply clarsimp
kleing@24333
   341
   apply clarsimp
kleing@24333
   342
  apply (case_tac x rule: bin_exhaust)
kleing@24333
   343
  apply (case_tac b)
kleing@24333
   344
   apply (case_tac [!] bit)
huffman@46604
   345
     apply (auto simp: le_Bits)
kleing@24333
   346
  done
kleing@24333
   347
kleing@24333
   348
lemmas int_and_le =
haftmann@53062
   349
  xtrans(3) [OF bbw_ao_absorbs (2) [THEN conjunct2, symmetric] le_int_or]
kleing@24333
   350
huffman@24364
   351
(* interaction between bit-wise and arithmetic *)
huffman@24364
   352
(* good example of bin_induction *)
huffman@47108
   353
lemma bin_add_not: "x + NOT x = (-1::int)"
huffman@24364
   354
  apply (induct x rule: bin_induct)
huffman@24364
   355
    apply clarsimp
huffman@24364
   356
   apply clarsimp
huffman@47108
   357
  apply (case_tac bit, auto)
huffman@24364
   358
  done
huffman@24364
   359
wenzelm@61799
   360
subsubsection \<open>Truncating results of bit-wise operations\<close>
huffman@45543
   361
wenzelm@65363
   362
lemma bin_trunc_ao:
wenzelm@65363
   363
  "!!x y. (bintrunc n x) AND (bintrunc n y) = bintrunc n (x AND y)"
huffman@24364
   364
  "!!x y. (bintrunc n x) OR (bintrunc n y) = bintrunc n (x OR y)"
huffman@45543
   365
  by (auto simp add: bin_eq_iff bin_nth_ops nth_bintr)
huffman@24364
   366
wenzelm@65363
   367
lemma bin_trunc_xor:
wenzelm@65363
   368
  "!!x y. bintrunc n (bintrunc n x XOR bintrunc n y) =
huffman@24364
   369
          bintrunc n (x XOR y)"
huffman@45543
   370
  by (auto simp add: bin_eq_iff bin_nth_ops nth_bintr)
huffman@24364
   371
wenzelm@65363
   372
lemma bin_trunc_not:
huffman@24364
   373
  "!!x. bintrunc n (NOT (bintrunc n x)) = bintrunc n (NOT x)"
huffman@45543
   374
  by (auto simp add: bin_eq_iff bin_nth_ops nth_bintr)
huffman@24364
   375
huffman@24364
   376
(* want theorems of the form of bin_trunc_xor *)
huffman@24364
   377
lemma bintr_bintr_i:
huffman@24364
   378
  "x = bintrunc n y ==> bintrunc n x = bintrunc n y"
huffman@24364
   379
  by auto
huffman@24364
   380
huffman@24364
   381
lemmas bin_trunc_and = bin_trunc_ao(1) [THEN bintr_bintr_i]
huffman@24364
   382
lemmas bin_trunc_or = bin_trunc_ao(2) [THEN bintr_bintr_i]
huffman@24364
   383
wenzelm@61799
   384
subsection \<open>Setting and clearing bits\<close>
huffman@24364
   385
haftmann@54874
   386
(** nth bit, set/clear **)
haftmann@54874
   387
haftmann@26558
   388
primrec
haftmann@54847
   389
  bin_sc :: "nat => bool => int => int"
haftmann@26558
   390
where
haftmann@26558
   391
  Z: "bin_sc 0 b w = bin_rest w BIT b"
haftmann@26558
   392
  | Suc: "bin_sc (Suc n) b w = bin_sc n b (bin_rest w) BIT bin_last w"
huffman@24364
   393
wenzelm@65363
   394
lemma bin_nth_sc [simp]:
haftmann@54847
   395
  "bin_nth (bin_sc n b w) n \<longleftrightarrow> b"
huffman@45955
   396
  by (induct n arbitrary: w) auto
kleing@24333
   397
wenzelm@65363
   398
lemma bin_sc_sc_same [simp]:
huffman@45955
   399
  "bin_sc n c (bin_sc n b w) = bin_sc n c w"
huffman@45955
   400
  by (induct n arbitrary: w) auto
kleing@24333
   401
kleing@24333
   402
lemma bin_sc_sc_diff:
wenzelm@65363
   403
  "m ~= n ==>
kleing@24333
   404
    bin_sc m c (bin_sc n b w) = bin_sc n b (bin_sc m c w)"
huffman@45955
   405
  apply (induct n arbitrary: w m)
kleing@24333
   406
   apply (case_tac [!] m)
kleing@24333
   407
     apply auto
kleing@24333
   408
  done
kleing@24333
   409
wenzelm@65363
   410
lemma bin_nth_sc_gen:
haftmann@54847
   411
  "bin_nth (bin_sc n b w) m = (if m = n then b else bin_nth w m)"
huffman@45955
   412
  by (induct n arbitrary: w m) (case_tac [!] m, auto)
wenzelm@65363
   413
kleing@24333
   414
lemma bin_sc_nth [simp]:
haftmann@54847
   415
  "(bin_sc n (bin_nth w n) w) = w"
huffman@45955
   416
  by (induct n arbitrary: w) auto
kleing@24333
   417
kleing@24333
   418
lemma bin_sign_sc [simp]:
huffman@45955
   419
  "bin_sign (bin_sc n b w) = bin_sign w"
huffman@45955
   420
  by (induct n arbitrary: w) auto
wenzelm@65363
   421
wenzelm@65363
   422
lemma bin_sc_bintr [simp]:
huffman@45955
   423
  "bintrunc m (bin_sc n x (bintrunc m (w))) = bintrunc m (bin_sc n x w)"
huffman@45955
   424
  apply (induct n arbitrary: w m)
kleing@24333
   425
   apply (case_tac [!] w rule: bin_exhaust)
kleing@24333
   426
   apply (case_tac [!] m, auto)
kleing@24333
   427
  done
kleing@24333
   428
kleing@24333
   429
lemma bin_clr_le:
haftmann@54847
   430
  "bin_sc n False w <= w"
huffman@45955
   431
  apply (induct n arbitrary: w)
kleing@24333
   432
   apply (case_tac [!] w rule: bin_exhaust)
huffman@46605
   433
   apply (auto simp: le_Bits)
kleing@24333
   434
  done
kleing@24333
   435
kleing@24333
   436
lemma bin_set_ge:
haftmann@54847
   437
  "bin_sc n True w >= w"
huffman@45955
   438
  apply (induct n arbitrary: w)
kleing@24333
   439
   apply (case_tac [!] w rule: bin_exhaust)
huffman@46605
   440
   apply (auto simp: le_Bits)
kleing@24333
   441
  done
kleing@24333
   442
kleing@24333
   443
lemma bintr_bin_clr_le:
haftmann@54847
   444
  "bintrunc n (bin_sc m False w) <= bintrunc n w"
huffman@45955
   445
  apply (induct n arbitrary: w m)
kleing@24333
   446
   apply simp
kleing@24333
   447
  apply (case_tac w rule: bin_exhaust)
kleing@24333
   448
  apply (case_tac m)
huffman@46605
   449
   apply (auto simp: le_Bits)
kleing@24333
   450
  done
kleing@24333
   451
kleing@24333
   452
lemma bintr_bin_set_ge:
haftmann@54847
   453
  "bintrunc n (bin_sc m True w) >= bintrunc n w"
huffman@45955
   454
  apply (induct n arbitrary: w m)
kleing@24333
   455
   apply simp
kleing@24333
   456
  apply (case_tac w rule: bin_exhaust)
kleing@24333
   457
  apply (case_tac m)
huffman@46605
   458
   apply (auto simp: le_Bits)
kleing@24333
   459
  done
kleing@24333
   460
haftmann@54847
   461
lemma bin_sc_FP [simp]: "bin_sc n False 0 = 0"
huffman@46608
   462
  by (induct n) auto
kleing@24333
   463
haftmann@58410
   464
lemma bin_sc_TM [simp]: "bin_sc n True (- 1) = - 1"
huffman@46608
   465
  by (induct n) auto
wenzelm@65363
   466
kleing@24333
   467
lemmas bin_sc_simps = bin_sc.Z bin_sc.Suc bin_sc_TM bin_sc_FP
kleing@24333
   468
kleing@24333
   469
lemma bin_sc_minus:
kleing@24333
   470
  "0 < n ==> bin_sc (Suc (n - 1)) b w = bin_sc n b w"
kleing@24333
   471
  by auto
kleing@24333
   472
wenzelm@65363
   473
lemmas bin_sc_Suc_minus =
wenzelm@45604
   474
  trans [OF bin_sc_minus [symmetric] bin_sc.Suc]
kleing@24333
   475
huffman@47108
   476
lemma bin_sc_numeral [simp]:
huffman@47108
   477
  "bin_sc (numeral k) b w =
huffman@47219
   478
    bin_sc (pred_numeral k) b (bin_rest w) BIT bin_last w"
huffman@47219
   479
  by (simp add: numeral_eq_Suc)
kleing@24333
   480
huffman@24465
   481
wenzelm@61799
   482
subsection \<open>Splitting and concatenation\<close>
kleing@24333
   483
haftmann@54848
   484
definition bin_rcat :: "nat \<Rightarrow> int list \<Rightarrow> int"
haftmann@54848
   485
where
haftmann@37667
   486
  "bin_rcat n = foldl (\<lambda>u v. bin_cat u n v) 0"
haftmann@37667
   487
haftmann@54848
   488
fun bin_rsplit_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list"
haftmann@54848
   489
where
haftmann@26558
   490
  "bin_rsplit_aux n m c bs =
huffman@24364
   491
    (if m = 0 | n = 0 then bs else
wenzelm@65363
   492
      let (a, b) = bin_split n c
haftmann@26558
   493
      in bin_rsplit_aux n (m - n) a (b # bs))"
huffman@24364
   494
haftmann@54848
   495
definition bin_rsplit :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list"
haftmann@54848
   496
where
haftmann@26558
   497
  "bin_rsplit n w = bin_rsplit_aux n (fst w) (snd w) []"
haftmann@26558
   498
haftmann@54848
   499
fun bin_rsplitl_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list"
haftmann@54848
   500
where
haftmann@26558
   501
  "bin_rsplitl_aux n m c bs =
huffman@24364
   502
    (if m = 0 | n = 0 then bs else
wenzelm@65363
   503
      let (a, b) = bin_split (min m n) c
haftmann@26558
   504
      in bin_rsplitl_aux n (m - n) a (b # bs))"
huffman@24364
   505
haftmann@54848
   506
definition bin_rsplitl :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list"
haftmann@54848
   507
where
haftmann@26558
   508
  "bin_rsplitl n w = bin_rsplitl_aux n (fst w) (snd w) []"
haftmann@26558
   509
huffman@24364
   510
declare bin_rsplit_aux.simps [simp del]
huffman@24364
   511
declare bin_rsplitl_aux.simps [simp del]
huffman@24364
   512
wenzelm@65363
   513
lemma bin_sign_cat:
huffman@45955
   514
  "bin_sign (bin_cat x n y) = bin_sign x"
huffman@45955
   515
  by (induct n arbitrary: y) auto
huffman@24364
   516
huffman@24364
   517
lemma bin_cat_Suc_Bit:
huffman@24364
   518
  "bin_cat w (Suc n) (v BIT b) = bin_cat w n v BIT b"
huffman@24364
   519
  by auto
huffman@24364
   520
wenzelm@65363
   521
lemma bin_nth_cat:
wenzelm@65363
   522
  "bin_nth (bin_cat x k y) n =
huffman@24364
   523
    (if n < k then bin_nth y n else bin_nth x (n - k))"
huffman@45955
   524
  apply (induct k arbitrary: n y)
huffman@24364
   525
   apply clarsimp
huffman@24364
   526
  apply (case_tac n, auto)
kleing@24333
   527
  done
kleing@24333
   528
huffman@24364
   529
lemma bin_nth_split:
wenzelm@65363
   530
  "bin_split n c = (a, b) ==>
wenzelm@65363
   531
    (ALL k. bin_nth a k = bin_nth c (n + k)) &
huffman@24364
   532
    (ALL k. bin_nth b k = (k < n & bin_nth c k))"
huffman@45955
   533
  apply (induct n arbitrary: b c)
huffman@24364
   534
   apply clarsimp
haftmann@53062
   535
  apply (clarsimp simp: Let_def split: prod.split_asm)
huffman@24364
   536
  apply (case_tac k)
huffman@24364
   537
  apply auto
huffman@24364
   538
  done
huffman@24364
   539
wenzelm@65363
   540
lemma bin_cat_assoc:
wenzelm@65363
   541
  "bin_cat (bin_cat x m y) n z = bin_cat x (m + n) (bin_cat y n z)"
huffman@45955
   542
  by (induct n arbitrary: z) auto
huffman@24364
   543
huffman@45955
   544
lemma bin_cat_assoc_sym:
huffman@45955
   545
  "bin_cat x m (bin_cat y n z) = bin_cat (bin_cat x (m - n) y) (min m n) z"
huffman@45955
   546
  apply (induct n arbitrary: z m, clarsimp)
huffman@24364
   547
  apply (case_tac m, auto)
kleing@24333
   548
  done
kleing@24333
   549
huffman@45956
   550
lemma bin_cat_zero [simp]: "bin_cat 0 n w = bintrunc n w"
huffman@46001
   551
  by (induct n arbitrary: w) auto
huffman@45956
   552
wenzelm@65363
   553
lemma bintr_cat1:
huffman@45955
   554
  "bintrunc (k + n) (bin_cat a n b) = bin_cat (bintrunc k a) n b"
huffman@45955
   555
  by (induct n arbitrary: b) auto
wenzelm@65363
   556
wenzelm@65363
   557
lemma bintr_cat: "bintrunc m (bin_cat a n b) =
huffman@24364
   558
    bin_cat (bintrunc (m - n) a) n (bintrunc (min m n) b)"
huffman@24364
   559
  by (rule bin_eqI) (auto simp: bin_nth_cat nth_bintr)
wenzelm@65363
   560
wenzelm@65363
   561
lemma bintr_cat_same [simp]:
huffman@24364
   562
  "bintrunc n (bin_cat a n b) = bintrunc n b"
huffman@24364
   563
  by (auto simp add : bintr_cat)
huffman@24364
   564
wenzelm@65363
   565
lemma cat_bintr [simp]:
huffman@45955
   566
  "bin_cat a n (bintrunc n b) = bin_cat a n b"
huffman@45955
   567
  by (induct n arbitrary: b) auto
huffman@24364
   568
wenzelm@65363
   569
lemma split_bintrunc:
huffman@45955
   570
  "bin_split n c = (a, b) ==> b = bintrunc n c"
haftmann@53062
   571
  by (induct n arbitrary: b c) (auto simp: Let_def split: prod.split_asm)
huffman@24364
   572
huffman@24364
   573
lemma bin_cat_split:
huffman@45955
   574
  "bin_split n w = (u, v) ==> w = bin_cat u n v"
haftmann@53062
   575
  by (induct n arbitrary: v w) (auto simp: Let_def split: prod.split_asm)
huffman@24364
   576
huffman@24364
   577
lemma bin_split_cat:
huffman@45955
   578
  "bin_split n (bin_cat v n w) = (v, bintrunc n w)"
huffman@45955
   579
  by (induct n arbitrary: w) auto
huffman@24364
   580
huffman@45956
   581
lemma bin_split_zero [simp]: "bin_split n 0 = (0, 0)"
huffman@46001
   582
  by (induct n) auto
huffman@45956
   583
huffman@46610
   584
lemma bin_split_minus1 [simp]:
haftmann@58410
   585
  "bin_split n (- 1) = (- 1, bintrunc n (- 1))"
huffman@46610
   586
  by (induct n) auto
huffman@24364
   587
huffman@24364
   588
lemma bin_split_trunc:
wenzelm@65363
   589
  "bin_split (min m n) c = (a, b) ==>
huffman@24364
   590
    bin_split n (bintrunc m c) = (bintrunc (m - n) a, b)"
huffman@45955
   591
  apply (induct n arbitrary: m b c, clarsimp)
haftmann@53062
   592
  apply (simp add: bin_rest_trunc Let_def split: prod.split_asm)
huffman@24364
   593
  apply (case_tac m)
haftmann@53062
   594
   apply (auto simp: Let_def split: prod.split_asm)
kleing@24333
   595
  done
kleing@24333
   596
huffman@24364
   597
lemma bin_split_trunc1:
wenzelm@65363
   598
  "bin_split n c = (a, b) ==>
huffman@24364
   599
    bin_split n (bintrunc m c) = (bintrunc (m - n) a, bintrunc m b)"
huffman@45955
   600
  apply (induct n arbitrary: m b c, clarsimp)
haftmann@53062
   601
  apply (simp add: bin_rest_trunc Let_def split: prod.split_asm)
huffman@24364
   602
  apply (case_tac m)
haftmann@53062
   603
   apply (auto simp: Let_def split: prod.split_asm)
huffman@24364
   604
  done
kleing@24333
   605
huffman@24364
   606
lemma bin_cat_num:
huffman@45955
   607
  "bin_cat a n b = a * 2 ^ n + bintrunc n b"
huffman@45955
   608
  apply (induct n arbitrary: b, clarsimp)
huffman@46001
   609
  apply (simp add: Bit_def)
huffman@24364
   610
  done
huffman@24364
   611
huffman@24364
   612
lemma bin_split_num:
huffman@45955
   613
  "bin_split n b = (b div 2 ^ n, b mod 2 ^ n)"
huffman@46610
   614
  apply (induct n arbitrary: b, simp)
huffman@45529
   615
  apply (simp add: bin_rest_def zdiv_zmult2_eq)
huffman@24364
   616
  apply (case_tac b rule: bin_exhaust)
huffman@24364
   617
  apply simp
haftmann@54847
   618
  apply (simp add: Bit_def mod_mult_mult1 p1mod22k)
huffman@45955
   619
  done
huffman@24364
   620
wenzelm@61799
   621
subsection \<open>Miscellaneous lemmas\<close>
kleing@24333
   622
wenzelm@65363
   623
lemma nth_2p_bin:
huffman@45955
   624
  "bin_nth (2 ^ n) m = (m = n)"
huffman@45955
   625
  apply (induct n arbitrary: m)
kleing@24333
   626
   apply clarsimp
kleing@24333
   627
   apply safe
wenzelm@65363
   628
   apply (case_tac m)
kleing@24333
   629
    apply (auto simp: Bit_B0_2t [symmetric])
kleing@24333
   630
  done
kleing@24333
   631
kleing@24333
   632
(* for use when simplifying with bin_nth_Bit *)
kleing@24333
   633
kleing@24333
   634
lemma ex_eq_or:
kleing@24333
   635
  "(EX m. n = Suc m & (m = k | P m)) = (n = Suc k | (EX m. n = Suc m & P m))"
kleing@24333
   636
  by auto
kleing@24333
   637
haftmann@54847
   638
lemma power_BIT: "2 ^ (Suc n) - 1 = (2 ^ n - 1) BIT True"
haftmann@54427
   639
  unfolding Bit_B1
haftmann@54427
   640
  by (induct n) simp_all
haftmann@54427
   641
haftmann@54427
   642
lemma mod_BIT:
haftmann@54427
   643
  "bin BIT bit mod 2 ^ Suc n = (bin mod 2 ^ n) BIT bit"
haftmann@54427
   644
proof -
haftmann@64593
   645
  have "2 * (bin mod 2 ^ n) + 1 = (2 * bin mod 2 ^ Suc n) + 1"
haftmann@64593
   646
    by (simp add: mod_mult_mult1)
haftmann@64593
   647
  also have "\<dots> = ((2 * bin mod 2 ^ Suc n) + 1) mod 2 ^ Suc n"
haftmann@64593
   648
    by (simp add: ac_simps p1mod22k')
haftmann@64593
   649
  also have "\<dots> = (2 * bin + 1) mod 2 ^ Suc n"
haftmann@64593
   650
    by (simp only: mod_simps)
haftmann@64593
   651
  finally show ?thesis
haftmann@64593
   652
    by (auto simp add: Bit_def)
haftmann@54427
   653
qed
haftmann@54427
   654
haftmann@54427
   655
lemma AND_mod:
haftmann@54427
   656
  fixes x :: int
haftmann@54427
   657
  shows "x AND 2 ^ n - 1 = x mod 2 ^ n"
haftmann@54427
   658
proof (induct x arbitrary: n rule: bin_induct)
haftmann@54427
   659
  case 1
haftmann@54427
   660
  then show ?case
haftmann@54427
   661
    by simp
haftmann@54427
   662
next
haftmann@54427
   663
  case 2
haftmann@54427
   664
  then show ?case
haftmann@54427
   665
    by (simp, simp add: m1mod2k)
haftmann@54427
   666
next
haftmann@54427
   667
  case (3 bin bit)
haftmann@54427
   668
  show ?case
haftmann@54427
   669
  proof (cases n)
haftmann@54427
   670
    case 0
haftmann@54847
   671
    then show ?thesis by simp
haftmann@54427
   672
  next
haftmann@54427
   673
    case (Suc m)
haftmann@54427
   674
    with 3 show ?thesis
haftmann@54427
   675
      by (simp only: power_BIT mod_BIT int_and_Bits) simp
haftmann@54427
   676
  qed
haftmann@54427
   677
qed
haftmann@54427
   678
kleing@24333
   679
end
haftmann@53062
   680