src/HOL/Word/WordBitwise.thy
author wenzelm
Wed Sep 17 21:27:14 2008 +0200 (2008-09-17)
changeset 28263 69eaa97e7e96
parent 26827 a62f8db42f4a
child 29235 2d62b637fa80
permissions -rw-r--r--
moved global ML bindings to global place;
kleing@24333
     1
(* 
kleing@24333
     2
    ID:         $Id$
kleing@24333
     3
    Author:     Jeremy Dawson and Gerwin Klein, NICTA
kleing@24333
     4
kleing@24333
     5
  contains theorems to do with bit-wise (logical) operations on words
kleing@24333
     6
*)
huffman@24350
     7
huffman@24350
     8
header {* Bitwise Operations on Words *}
huffman@24350
     9
haftmann@26558
    10
theory WordBitwise
haftmann@26558
    11
imports WordArith
haftmann@26558
    12
begin
kleing@24333
    13
kleing@24333
    14
lemmas bin_log_bintrs = bin_trunc_not bin_trunc_xor bin_trunc_and bin_trunc_or
kleing@24333
    15
  
kleing@24333
    16
(* following definitions require both arithmetic and bit-wise word operations *)
kleing@24333
    17
kleing@24333
    18
(* to get word_no_log_defs from word_log_defs, using bin_log_bintrs *)
kleing@24333
    19
lemmas wils1 = bin_log_bintrs [THEN word_ubin.norm_eq_iff [THEN iffD1],
kleing@24333
    20
  folded word_ubin.eq_norm, THEN eq_reflection, standard]
kleing@24333
    21
kleing@24333
    22
(* the binary operations only *)
kleing@24333
    23
lemmas word_log_binary_defs = 
kleing@24333
    24
  word_and_def word_or_def word_xor_def
kleing@24333
    25
kleing@24333
    26
lemmas word_no_log_defs [simp] = 
wenzelm@25350
    27
  word_not_def  [where a="number_of a", 
wenzelm@25350
    28
                 unfolded word_no_wi wils1, folded word_no_wi, standard]
wenzelm@25350
    29
  word_log_binary_defs [where a="number_of a" and b="number_of b",
wenzelm@25350
    30
                        unfolded word_no_wi wils1, folded word_no_wi, standard]
kleing@24333
    31
kleing@24333
    32
lemmas word_wi_log_defs = word_no_log_defs [unfolded word_no_wi]
kleing@24333
    33
huffman@24353
    34
lemma uint_or: "uint (x OR y) = (uint x) OR (uint y)"
huffman@24368
    35
  by (simp add: word_or_def word_no_wi [symmetric] number_of_is_id
kleing@24333
    36
                bin_trunc_ao(2) [symmetric])
kleing@24333
    37
huffman@24353
    38
lemma uint_and: "uint (x AND y) = (uint x) AND (uint y)"
huffman@24368
    39
  by (simp add: word_and_def number_of_is_id word_no_wi [symmetric]
kleing@24333
    40
                bin_trunc_ao(1) [symmetric]) 
kleing@24333
    41
kleing@24333
    42
lemma word_ops_nth_size:
huffman@24465
    43
  "n < size (x::'a::len0 word) ==> 
kleing@24333
    44
    (x OR y) !! n = (x !! n | y !! n) & 
kleing@24333
    45
    (x AND y) !! n = (x !! n & y !! n) & 
kleing@24333
    46
    (x XOR y) !! n = (x !! n ~= y !! n) & 
kleing@24333
    47
    (NOT x) !! n = (~ x !! n)"
kleing@24333
    48
  unfolding word_size word_no_wi word_test_bit_def word_log_defs
kleing@24333
    49
  by (clarsimp simp add : word_ubin.eq_norm nth_bintr bin_nth_ops)
kleing@24333
    50
kleing@24333
    51
lemma word_ao_nth:
huffman@24465
    52
  fixes x :: "'a::len0 word"
kleing@24333
    53
  shows "(x OR y) !! n = (x !! n | y !! n) & 
kleing@24333
    54
         (x AND y) !! n = (x !! n & y !! n)"
kleing@24333
    55
  apply (cases "n < size x")
kleing@24333
    56
   apply (drule_tac y = "y" in word_ops_nth_size)
kleing@24333
    57
   apply simp
kleing@24333
    58
  apply (simp add : test_bit_bin word_size)
kleing@24333
    59
  done
kleing@24333
    60
kleing@24333
    61
(* get from commutativity, associativity etc of int_and etc
kleing@24333
    62
  to same for word_and etc *)
kleing@24333
    63
kleing@24333
    64
lemmas bwsimps = 
kleing@24333
    65
  word_of_int_homs(2) 
kleing@24333
    66
  word_0_wi_Pls
kleing@24333
    67
  word_m1_wi_Min
kleing@24333
    68
  word_wi_log_defs
kleing@24333
    69
kleing@24333
    70
lemma word_bw_assocs:
huffman@24465
    71
  fixes x :: "'a::len0 word"
kleing@24333
    72
  shows
kleing@24333
    73
  "(x AND y) AND z = x AND y AND z"
kleing@24333
    74
  "(x OR y) OR z = x OR y OR z"
kleing@24333
    75
  "(x XOR y) XOR z = x XOR y XOR z"
kleing@24333
    76
  using word_of_int_Ex [where x=x] 
kleing@24333
    77
        word_of_int_Ex [where x=y] 
kleing@24333
    78
        word_of_int_Ex [where x=z]
huffman@24367
    79
  by (auto simp: bwsimps bbw_assocs)
kleing@24333
    80
  
kleing@24333
    81
lemma word_bw_comms:
huffman@24465
    82
  fixes x :: "'a::len0 word"
kleing@24333
    83
  shows
kleing@24333
    84
  "x AND y = y AND x"
kleing@24333
    85
  "x OR y = y OR x"
kleing@24333
    86
  "x XOR y = y XOR x"
kleing@24333
    87
  using word_of_int_Ex [where x=x] 
kleing@24333
    88
        word_of_int_Ex [where x=y] 
huffman@24367
    89
  by (auto simp: bwsimps bin_ops_comm)
kleing@24333
    90
  
kleing@24333
    91
lemma word_bw_lcs:
huffman@24465
    92
  fixes x :: "'a::len0 word"
kleing@24333
    93
  shows
kleing@24333
    94
  "y AND x AND z = x AND y AND z"
kleing@24333
    95
  "y OR x OR z = x OR y OR z"
kleing@24333
    96
  "y XOR x XOR z = x XOR y XOR z"
kleing@24333
    97
  using word_of_int_Ex [where x=x] 
kleing@24333
    98
        word_of_int_Ex [where x=y] 
kleing@24333
    99
        word_of_int_Ex [where x=z]
kleing@24333
   100
  by (auto simp: bwsimps)
kleing@24333
   101
kleing@24333
   102
lemma word_log_esimps [simp]:
huffman@24465
   103
  fixes x :: "'a::len0 word"
kleing@24333
   104
  shows
kleing@24333
   105
  "x AND 0 = 0"
kleing@24333
   106
  "x AND -1 = x"
kleing@24333
   107
  "x OR 0 = x"
kleing@24333
   108
  "x OR -1 = -1"
kleing@24333
   109
  "x XOR 0 = x"
kleing@24333
   110
  "x XOR -1 = NOT x"
kleing@24333
   111
  "0 AND x = 0"
kleing@24333
   112
  "-1 AND x = x"
kleing@24333
   113
  "0 OR x = x"
kleing@24333
   114
  "-1 OR x = -1"
kleing@24333
   115
  "0 XOR x = x"
kleing@24333
   116
  "-1 XOR x = NOT x"
kleing@24333
   117
  using word_of_int_Ex [where x=x] 
kleing@24333
   118
  by (auto simp: bwsimps)
kleing@24333
   119
kleing@24333
   120
lemma word_not_dist:
huffman@24465
   121
  fixes x :: "'a::len0 word"
kleing@24333
   122
  shows
kleing@24333
   123
  "NOT (x OR y) = NOT x AND NOT y"
kleing@24333
   124
  "NOT (x AND y) = NOT x OR NOT y"
kleing@24333
   125
  using word_of_int_Ex [where x=x] 
kleing@24333
   126
        word_of_int_Ex [where x=y] 
kleing@24333
   127
  by (auto simp: bwsimps bbw_not_dist)
kleing@24333
   128
kleing@24333
   129
lemma word_bw_same:
huffman@24465
   130
  fixes x :: "'a::len0 word"
kleing@24333
   131
  shows
kleing@24333
   132
  "x AND x = x"
kleing@24333
   133
  "x OR x = x"
kleing@24333
   134
  "x XOR x = 0"
kleing@24333
   135
  using word_of_int_Ex [where x=x] 
kleing@24333
   136
  by (auto simp: bwsimps)
kleing@24333
   137
kleing@24333
   138
lemma word_ao_absorbs [simp]:
huffman@24465
   139
  fixes x :: "'a::len0 word"
kleing@24333
   140
  shows
kleing@24333
   141
  "x AND (y OR x) = x"
kleing@24333
   142
  "x OR y AND x = x"
kleing@24333
   143
  "x AND (x OR y) = x"
kleing@24333
   144
  "y AND x OR x = x"
kleing@24333
   145
  "(y OR x) AND x = x"
kleing@24333
   146
  "x OR x AND y = x"
kleing@24333
   147
  "(x OR y) AND x = x"
kleing@24333
   148
  "x AND y OR x = x"
kleing@24333
   149
  using word_of_int_Ex [where x=x] 
kleing@24333
   150
        word_of_int_Ex [where x=y] 
kleing@24333
   151
  by (auto simp: bwsimps)
kleing@24333
   152
kleing@24333
   153
lemma word_not_not [simp]:
huffman@24465
   154
  "NOT NOT (x::'a::len0 word) = x"
kleing@24333
   155
  using word_of_int_Ex [where x=x] 
kleing@24333
   156
  by (auto simp: bwsimps)
kleing@24333
   157
kleing@24333
   158
lemma word_ao_dist:
huffman@24465
   159
  fixes x :: "'a::len0 word"
kleing@24333
   160
  shows "(x OR y) AND z = x AND z OR y AND z"
kleing@24333
   161
  using word_of_int_Ex [where x=x] 
kleing@24333
   162
        word_of_int_Ex [where x=y] 
kleing@24333
   163
        word_of_int_Ex [where x=z]   
kleing@24333
   164
  by (auto simp: bwsimps bbw_ao_dist simp del: bin_ops_comm)
kleing@24333
   165
kleing@24333
   166
lemma word_oa_dist:
huffman@24465
   167
  fixes x :: "'a::len0 word"
kleing@24333
   168
  shows "x AND y OR z = (x OR z) AND (y OR z)"
kleing@24333
   169
  using word_of_int_Ex [where x=x] 
kleing@24333
   170
        word_of_int_Ex [where x=y] 
kleing@24333
   171
        word_of_int_Ex [where x=z]   
kleing@24333
   172
  by (auto simp: bwsimps bbw_oa_dist simp del: bin_ops_comm)
kleing@24333
   173
kleing@24333
   174
lemma word_add_not [simp]: 
huffman@24465
   175
  fixes x :: "'a::len0 word"
kleing@24333
   176
  shows "x + NOT x = -1"
kleing@24333
   177
  using word_of_int_Ex [where x=x] 
kleing@24333
   178
  by (auto simp: bwsimps bin_add_not)
kleing@24333
   179
kleing@24333
   180
lemma word_plus_and_or [simp]:
huffman@24465
   181
  fixes x :: "'a::len0 word"
kleing@24333
   182
  shows "(x AND y) + (x OR y) = x + y"
kleing@24333
   183
  using word_of_int_Ex [where x=x] 
kleing@24333
   184
        word_of_int_Ex [where x=y] 
kleing@24333
   185
  by (auto simp: bwsimps plus_and_or)
kleing@24333
   186
kleing@24333
   187
lemma leoa:   
huffman@24465
   188
  fixes x :: "'a::len0 word"
kleing@24333
   189
  shows "(w = (x OR y)) ==> (y = (w AND y))" by auto
kleing@24333
   190
lemma leao: 
huffman@24465
   191
  fixes x' :: "'a::len0 word"
kleing@24333
   192
  shows "(w' = (x' AND y')) ==> (x' = (x' OR w'))" by auto 
kleing@24333
   193
kleing@24333
   194
lemmas word_ao_equiv = leao [COMP leoa [COMP iffI]]
kleing@24333
   195
huffman@24465
   196
lemma le_word_or2: "x <= x OR (y::'a::len0 word)"
kleing@24333
   197
  unfolding word_le_def uint_or
kleing@24333
   198
  by (auto intro: le_int_or) 
kleing@24333
   199
kleing@24333
   200
lemmas le_word_or1 = xtr3 [OF word_bw_comms (2) le_word_or2, standard]
kleing@24333
   201
lemmas word_and_le1 =
kleing@24333
   202
  xtr3 [OF word_ao_absorbs (4) [symmetric] le_word_or2, standard]
kleing@24333
   203
lemmas word_and_le2 =
kleing@24333
   204
  xtr3 [OF word_ao_absorbs (8) [symmetric] le_word_or2, standard]
kleing@24333
   205
huffman@24465
   206
lemma bl_word_not: "to_bl (NOT w) = map Not (to_bl w)" 
huffman@24465
   207
  unfolding to_bl_def word_log_defs
huffman@24465
   208
  by (simp add: bl_not_bin number_of_is_id word_no_wi [symmetric])
huffman@24465
   209
haftmann@26558
   210
lemma bl_word_xor: "to_bl (v XOR w) = map2 op ~= (to_bl v) (to_bl w)" 
huffman@24465
   211
  unfolding to_bl_def word_log_defs bl_xor_bin
huffman@24465
   212
  by (simp add: number_of_is_id word_no_wi [symmetric])
huffman@24465
   213
haftmann@26558
   214
lemma bl_word_or: "to_bl (v OR w) = map2 op | (to_bl v) (to_bl w)" 
huffman@24465
   215
  unfolding to_bl_def word_log_defs
huffman@24465
   216
  by (simp add: bl_or_bin number_of_is_id word_no_wi [symmetric])
huffman@24465
   217
haftmann@26558
   218
lemma bl_word_and: "to_bl (v AND w) = map2 op & (to_bl v) (to_bl w)" 
huffman@24465
   219
  unfolding to_bl_def word_log_defs
huffman@24465
   220
  by (simp add: bl_and_bin number_of_is_id word_no_wi [symmetric])
huffman@24465
   221
huffman@24465
   222
lemma word_lsb_alt: "lsb (w::'a::len0 word) = test_bit w 0"
kleing@24333
   223
  by (auto simp: word_test_bit_def word_lsb_def)
kleing@24333
   224
huffman@24465
   225
lemma word_lsb_1_0: "lsb (1::'a::len word) & ~ lsb (0::'b::len0 word)"
kleing@24333
   226
  unfolding word_lsb_def word_1_no word_0_no by auto
kleing@24333
   227
huffman@24465
   228
lemma word_lsb_last: "lsb (w::'a::len word) = last (to_bl w)"
huffman@24465
   229
  apply (unfold word_lsb_def uint_bl bin_to_bl_def) 
huffman@24465
   230
  apply (rule_tac bin="uint w" in bin_exhaust)
huffman@24465
   231
  apply (cases "size w")
huffman@24465
   232
   apply auto
huffman@24465
   233
   apply (auto simp add: bin_to_bl_aux_alt)
huffman@24465
   234
  done
huffman@24465
   235
kleing@24333
   236
lemma word_lsb_int: "lsb w = (uint w mod 2 = 1)"
kleing@24333
   237
  unfolding word_lsb_def bin_last_mod by auto
kleing@24333
   238
kleing@24333
   239
lemma word_msb_sint: "msb w = (sint w < 0)" 
kleing@24333
   240
  unfolding word_msb_def
huffman@24368
   241
  by (simp add : sign_Min_lt_0 number_of_is_id)
kleing@24333
   242
  
kleing@24333
   243
lemma word_msb_no': 
huffman@24465
   244
  "w = number_of bin ==> msb (w::'a::len word) = bin_nth bin (size w - 1)"
kleing@24333
   245
  unfolding word_msb_def word_number_of_def
kleing@24333
   246
  by (clarsimp simp add: word_sbin.eq_norm word_size bin_sign_lem)
kleing@24333
   247
kleing@24333
   248
lemmas word_msb_no = refl [THEN word_msb_no', unfolded word_size]
kleing@24333
   249
huffman@24465
   250
lemma word_msb_nth': "msb (w::'a::len word) = bin_nth (uint w) (size w - 1)"
kleing@24333
   251
  apply (unfold word_size)
kleing@24333
   252
  apply (rule trans [OF _ word_msb_no])
kleing@24333
   253
  apply (simp add : word_number_of_def)
kleing@24333
   254
  done
kleing@24333
   255
kleing@24333
   256
lemmas word_msb_nth = word_msb_nth' [unfolded word_size]
kleing@24333
   257
huffman@24465
   258
lemma word_msb_alt: "msb (w::'a::len word) = hd (to_bl w)"
huffman@24465
   259
  apply (unfold word_msb_nth uint_bl)
huffman@24465
   260
  apply (subst hd_conv_nth)
huffman@24465
   261
  apply (rule length_greater_0_conv [THEN iffD1])
huffman@24465
   262
   apply simp
huffman@24465
   263
  apply (simp add : nth_bin_to_bl word_size)
huffman@24465
   264
  done
huffman@24465
   265
kleing@24333
   266
lemma word_set_nth:
huffman@24465
   267
  "set_bit w n (test_bit w n) = (w::'a::len0 word)"
kleing@24333
   268
  unfolding word_test_bit_def word_set_bit_def by auto
kleing@24333
   269
huffman@24465
   270
lemma bin_nth_uint':
huffman@24465
   271
  "bin_nth (uint w) n = (rev (bin_to_bl (size w) (uint w)) ! n & n < size w)"
huffman@24465
   272
  apply (unfold word_size)
huffman@24465
   273
  apply (safe elim!: bin_nth_uint_imp)
huffman@24465
   274
   apply (frule bin_nth_uint_imp)
huffman@24465
   275
   apply (fast dest!: bin_nth_bl)+
huffman@24465
   276
  done
huffman@24465
   277
huffman@24465
   278
lemmas bin_nth_uint = bin_nth_uint' [unfolded word_size]
huffman@24465
   279
huffman@24465
   280
lemma test_bit_bl: "w !! n = (rev (to_bl w) ! n & n < size w)"
huffman@24465
   281
  unfolding to_bl_def word_test_bit_def word_size
huffman@24465
   282
  by (rule bin_nth_uint)
huffman@24465
   283
huffman@24465
   284
lemma to_bl_nth: "n < size w ==> to_bl w ! n = w !! (size w - Suc n)"
huffman@24465
   285
  apply (unfold test_bit_bl)
huffman@24465
   286
  apply clarsimp
huffman@24465
   287
  apply (rule trans)
huffman@24465
   288
   apply (rule nth_rev_alt)
huffman@24465
   289
   apply (auto simp add: word_size)
huffman@24465
   290
  done
huffman@24465
   291
kleing@24333
   292
lemma test_bit_set: 
huffman@24465
   293
  fixes w :: "'a::len0 word"
kleing@24333
   294
  shows "(set_bit w n x) !! n = (n < size w & x)"
kleing@24333
   295
  unfolding word_size word_test_bit_def word_set_bit_def
kleing@24333
   296
  by (clarsimp simp add : word_ubin.eq_norm nth_bintr)
kleing@24333
   297
kleing@24333
   298
lemma test_bit_set_gen: 
huffman@24465
   299
  fixes w :: "'a::len0 word"
kleing@24333
   300
  shows "test_bit (set_bit w n x) m = 
kleing@24333
   301
         (if m = n then n < size w & x else test_bit w m)"
kleing@24333
   302
  apply (unfold word_size word_test_bit_def word_set_bit_def)
kleing@24333
   303
  apply (clarsimp simp add: word_ubin.eq_norm nth_bintr bin_nth_sc_gen)
kleing@24333
   304
  apply (auto elim!: test_bit_size [unfolded word_size]
kleing@24333
   305
              simp add: word_test_bit_def [symmetric])
kleing@24333
   306
  done
kleing@24333
   307
huffman@24465
   308
lemma of_bl_rep_False: "of_bl (replicate n False @ bs) = of_bl bs"
huffman@24465
   309
  unfolding of_bl_def bl_to_bin_rep_F by auto
huffman@24465
   310
  
kleing@24333
   311
lemma msb_nth':
huffman@24465
   312
  fixes w :: "'a::len word"
kleing@24333
   313
  shows "msb w = w !! (size w - 1)"
kleing@24333
   314
  unfolding word_msb_nth' word_test_bit_def by simp
kleing@24333
   315
kleing@24333
   316
lemmas msb_nth = msb_nth' [unfolded word_size]
kleing@24333
   317
huffman@24465
   318
lemmas msb0 = len_gt_0 [THEN diff_Suc_less, THEN
kleing@24333
   319
  word_ops_nth_size [unfolded word_size], standard]
kleing@24333
   320
lemmas msb1 = msb0 [where i = 0]
kleing@24333
   321
lemmas word_ops_msb = msb1 [unfolded msb_nth [symmetric, unfolded One_nat_def]]
kleing@24333
   322
huffman@24465
   323
lemmas lsb0 = len_gt_0 [THEN word_ops_nth_size [unfolded word_size], standard]
kleing@24333
   324
lemmas word_ops_lsb = lsb0 [unfolded word_lsb_alt]
kleing@24333
   325
huffman@24465
   326
lemma td_ext_nth':
huffman@24465
   327
  "n = size (w::'a::len0 word) ==> ofn = set_bits ==> [w, ofn g] = l ==> 
huffman@24465
   328
    td_ext test_bit ofn {f. ALL i. f i --> i < n} (%h i. h i & i < n)"
huffman@24465
   329
  apply (unfold word_size td_ext_def')
berghofe@26827
   330
  apply (safe del: subset_antisym)
huffman@24465
   331
     apply (rule_tac [3] ext)
huffman@24465
   332
     apply (rule_tac [4] ext)
huffman@24465
   333
     apply (unfold word_size of_nth_def test_bit_bl)
huffman@24465
   334
     apply safe
huffman@24465
   335
       defer
huffman@24465
   336
       apply (clarsimp simp: word_bl.Abs_inverse)+
huffman@24465
   337
  apply (rule word_bl.Rep_inverse')
huffman@24465
   338
  apply (rule sym [THEN trans])
huffman@24465
   339
  apply (rule bl_of_nth_nth)
huffman@24465
   340
  apply simp
huffman@24465
   341
  apply (rule bl_of_nth_inj)
huffman@24465
   342
  apply (clarsimp simp add : test_bit_bl word_size)
huffman@24465
   343
  done
huffman@24465
   344
huffman@24465
   345
lemmas td_ext_nth = td_ext_nth' [OF refl refl refl, unfolded word_size]
huffman@24465
   346
huffman@24465
   347
interpretation test_bit:
huffman@24465
   348
  td_ext ["op !! :: 'a::len0 word => nat => bool"
huffman@24465
   349
          set_bits
huffman@24465
   350
          "{f. \<forall>i. f i \<longrightarrow> i < len_of TYPE('a::len0)}"
huffman@24465
   351
          "(\<lambda>h i. h i \<and> i < len_of TYPE('a::len0))"]
huffman@24465
   352
  by (rule td_ext_nth)
huffman@24465
   353
huffman@24465
   354
declare test_bit.Rep' [simp del]
huffman@24465
   355
declare test_bit.Rep' [rule del]
huffman@24465
   356
huffman@24465
   357
lemmas td_nth = test_bit.td_thm
huffman@24465
   358
kleing@24333
   359
lemma word_set_set_same: 
huffman@24465
   360
  fixes w :: "'a::len0 word"
kleing@24333
   361
  shows "set_bit (set_bit w n x) n y = set_bit w n y" 
kleing@24333
   362
  by (rule word_eqI) (simp add : test_bit_set_gen word_size)
kleing@24333
   363
    
kleing@24333
   364
lemma word_set_set_diff: 
huffman@24465
   365
  fixes w :: "'a::len0 word"
kleing@24333
   366
  assumes "m ~= n"
kleing@24333
   367
  shows "set_bit (set_bit w m x) n y = set_bit (set_bit w n y) m x" 
kleing@24333
   368
  by (rule word_eqI) (clarsimp simp add : test_bit_set_gen word_size prems)
kleing@24333
   369
    
kleing@24333
   370
lemma test_bit_no': 
huffman@24465
   371
  fixes w :: "'a::len0 word"
kleing@24333
   372
  shows "w = number_of bin ==> test_bit w n = (n < size w & bin_nth bin n)"
kleing@24333
   373
  unfolding word_test_bit_def word_number_of_def word_size
kleing@24333
   374
  by (simp add : nth_bintr [symmetric] word_ubin.eq_norm)
kleing@24333
   375
kleing@24333
   376
lemmas test_bit_no = 
kleing@24333
   377
  refl [THEN test_bit_no', unfolded word_size, THEN eq_reflection, standard]
kleing@24333
   378
huffman@24465
   379
lemma nth_0: "~ (0::'a::len0 word) !! n"
kleing@24333
   380
  unfolding test_bit_no word_0_no by auto
kleing@24333
   381
kleing@24333
   382
lemma nth_sint: 
huffman@24465
   383
  fixes w :: "'a::len word"
huffman@24465
   384
  defines "l \<equiv> len_of TYPE ('a)"
kleing@24333
   385
  shows "bin_nth (sint w) n = (if n < l - 1 then w !! n else w !! (l - 1))"
kleing@24333
   386
  unfolding sint_uint l_def
kleing@24333
   387
  by (clarsimp simp add: nth_sbintr word_test_bit_def [symmetric])
kleing@24333
   388
kleing@24333
   389
lemma word_lsb_no: 
huffman@24465
   390
  "lsb (number_of bin :: 'a :: len word) = (bin_last bin = bit.B1)"
kleing@24333
   391
  unfolding word_lsb_alt test_bit_no by auto
kleing@24333
   392
kleing@24333
   393
lemma word_set_no: 
huffman@24465
   394
  "set_bit (number_of bin::'a::len0 word) n b = 
kleing@24333
   395
    number_of (bin_sc n (if b then bit.B1 else bit.B0) bin)"
kleing@24333
   396
  apply (unfold word_set_bit_def word_number_of_def [symmetric])
kleing@24333
   397
  apply (rule word_eqI)
huffman@24368
   398
  apply (clarsimp simp: word_size bin_nth_sc_gen number_of_is_id 
kleing@24333
   399
                        test_bit_no nth_bintr)
kleing@24333
   400
  done
kleing@24333
   401
kleing@24333
   402
lemmas setBit_no = setBit_def [THEN trans [OF meta_eq_to_obj_eq word_set_no],
kleing@24333
   403
  simplified if_simps, THEN eq_reflection, standard]
kleing@24333
   404
lemmas clearBit_no = clearBit_def [THEN trans [OF meta_eq_to_obj_eq word_set_no],
kleing@24333
   405
  simplified if_simps, THEN eq_reflection, standard]
kleing@24333
   406
huffman@24465
   407
lemma to_bl_n1: 
huffman@24465
   408
  "to_bl (-1::'a::len0 word) = replicate (len_of TYPE ('a)) True"
huffman@24465
   409
  apply (rule word_bl.Abs_inverse')
huffman@24465
   410
   apply simp
huffman@24465
   411
  apply (rule word_eqI)
huffman@24465
   412
  apply (clarsimp simp add: word_size test_bit_no)
huffman@24465
   413
  apply (auto simp add: word_bl.Abs_inverse test_bit_bl word_size)
huffman@24465
   414
  done
huffman@24465
   415
huffman@24465
   416
lemma word_msb_n1: "msb (-1::'a::len word)"
huffman@24465
   417
  unfolding word_msb_alt word_msb_alt to_bl_n1 by simp
kleing@24333
   418
kleing@24333
   419
declare word_set_set_same [simp] word_set_nth [simp]
kleing@24333
   420
  test_bit_no [simp] word_set_no [simp] nth_0 [simp]
kleing@24333
   421
  setBit_no [simp] clearBit_no [simp]
kleing@24333
   422
  word_lsb_no [simp] word_msb_no [simp] word_msb_n1 [simp] word_lsb_1_0 [simp]
kleing@24333
   423
kleing@24333
   424
lemma word_set_nth_iff: 
huffman@24465
   425
  "(set_bit w n b = w) = (w !! n = b | n >= size (w::'a::len0 word))"
kleing@24333
   426
  apply (rule iffI)
kleing@24333
   427
   apply (rule disjCI)
kleing@24333
   428
   apply (drule word_eqD)
kleing@24333
   429
   apply (erule sym [THEN trans])
kleing@24333
   430
   apply (simp add: test_bit_set)
kleing@24333
   431
  apply (erule disjE)
kleing@24333
   432
   apply clarsimp
kleing@24333
   433
  apply (rule word_eqI)
kleing@24333
   434
  apply (clarsimp simp add : test_bit_set_gen)
kleing@24333
   435
  apply (drule test_bit_size)
kleing@24333
   436
  apply force
kleing@24333
   437
  done
kleing@24333
   438
kleing@24333
   439
lemma test_bit_2p': 
kleing@24333
   440
  "w = word_of_int (2 ^ n) ==> 
huffman@24465
   441
    w !! m = (m = n & m < size (w :: 'a :: len word))"
kleing@24333
   442
  unfolding word_test_bit_def word_size
kleing@24333
   443
  by (auto simp add: word_ubin.eq_norm nth_bintr nth_2p_bin)
kleing@24333
   444
kleing@24333
   445
lemmas test_bit_2p = refl [THEN test_bit_2p', unfolded word_size]
kleing@24333
   446
kleing@24333
   447
lemmas nth_w2p = test_bit_2p [unfolded of_int_number_of_eq
wenzelm@26289
   448
  word_of_int [symmetric] Int.of_int_power]
kleing@24333
   449
kleing@24333
   450
lemma uint_2p: 
huffman@24465
   451
  "(0::'a::len word) < 2 ^ n ==> uint (2 ^ n::'a::len word) = 2 ^ n"
kleing@24333
   452
  apply (unfold word_arith_power_alt)
huffman@24465
   453
  apply (case_tac "len_of TYPE ('a)")
kleing@24333
   454
   apply clarsimp
kleing@24333
   455
  apply (case_tac "nat")
kleing@24333
   456
   apply clarsimp
kleing@24333
   457
   apply (case_tac "n")
kleing@24333
   458
    apply (clarsimp simp add : word_1_wi [symmetric])
kleing@24333
   459
   apply (clarsimp simp add : word_0_wi [symmetric])
kleing@24333
   460
  apply (drule word_gt_0 [THEN iffD1])
kleing@24333
   461
  apply (safe intro!: word_eqI bin_nth_lem ext)
kleing@24333
   462
     apply (auto simp add: test_bit_2p nth_2p_bin word_test_bit_def [symmetric])
kleing@24333
   463
  done
kleing@24333
   464
huffman@24465
   465
lemma word_of_int_2p: "(word_of_int (2 ^ n) :: 'a :: len word) = 2 ^ n" 
kleing@24333
   466
  apply (unfold word_arith_power_alt)
huffman@24465
   467
  apply (case_tac "len_of TYPE ('a)")
kleing@24333
   468
   apply clarsimp
kleing@24333
   469
  apply (case_tac "nat")
kleing@24333
   470
   apply (rule word_ubin.norm_eq_iff [THEN iffD1]) 
kleing@24333
   471
   apply (rule box_equals) 
kleing@24333
   472
     apply (rule_tac [2] bintr_ariths (1))+ 
huffman@24368
   473
   apply (clarsimp simp add : number_of_is_id)
kleing@24333
   474
  apply simp 
kleing@24333
   475
  done
kleing@24333
   476
huffman@24465
   477
lemma bang_is_le: "x !! m ==> 2 ^ m <= (x :: 'a :: len word)" 
kleing@24333
   478
  apply (rule xtr3) 
kleing@24333
   479
  apply (rule_tac [2] y = "x" in le_word_or2)
kleing@24333
   480
  apply (rule word_eqI)
kleing@24333
   481
  apply (auto simp add: word_ao_nth nth_w2p word_size)
kleing@24333
   482
  done
kleing@24333
   483
kleing@24333
   484
lemma word_clr_le: 
huffman@24465
   485
  fixes w :: "'a::len0 word"
kleing@24333
   486
  shows "w >= set_bit w n False"
kleing@24333
   487
  apply (unfold word_set_bit_def word_le_def word_ubin.eq_norm)
kleing@24333
   488
  apply simp
kleing@24333
   489
  apply (rule order_trans)
kleing@24333
   490
   apply (rule bintr_bin_clr_le)
kleing@24333
   491
  apply simp
kleing@24333
   492
  done
kleing@24333
   493
kleing@24333
   494
lemma word_set_ge: 
huffman@24465
   495
  fixes w :: "'a::len word"
kleing@24333
   496
  shows "w <= set_bit w n True"
kleing@24333
   497
  apply (unfold word_set_bit_def word_le_def word_ubin.eq_norm)
kleing@24333
   498
  apply simp
kleing@24333
   499
  apply (rule order_trans [OF _ bintr_bin_set_ge])
kleing@24333
   500
  apply simp
kleing@24333
   501
  done
kleing@24333
   502
kleing@24333
   503
end
kleing@24333
   504