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