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