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