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