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