src/HOL/Word/WordBitwise.thy
author wenzelm
Fri Mar 06 15:58:56 2015 +0100 (2015-03-06)
changeset 59621 291934bac95e
parent 59582 0fbed69ff081
child 59643 f3be9235503d
permissions -rw-r--r--
Thm.cterm_of and Thm.ctyp_of operate on local context;
thomas@47567
     1
(*  Title:      HOL/Word/WordBitwise.thy
thomas@47567
     2
    Authors:    Thomas Sewell, NICTA and Sascha Boehme, TU Muenchen
thomas@47567
     3
*)
thomas@47567
     4
thomas@47567
     5
thomas@47567
     6
theory WordBitwise
thomas@47567
     7
thomas@47567
     8
imports Word
thomas@47567
     9
thomas@47567
    10
begin
thomas@47567
    11
thomas@47567
    12
text {* Helper constants used in defining addition *}
thomas@47567
    13
thomas@47567
    14
definition
thomas@47567
    15
  xor3 :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool"
thomas@47567
    16
where
thomas@47567
    17
 "xor3 a b c = (a = (b = c))"
thomas@47567
    18
thomas@47567
    19
definition
thomas@47567
    20
  carry :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool"
thomas@47567
    21
where
thomas@47567
    22
 "carry a b c = ((a \<and> (b \<or> c)) \<or> (b \<and> c))"
thomas@47567
    23
thomas@47567
    24
lemma carry_simps:
thomas@47567
    25
  "carry True a b = (a \<or> b)"
thomas@47567
    26
  "carry a True b = (a \<or> b)"
thomas@47567
    27
  "carry a b True = (a \<or> b)"
thomas@47567
    28
  "carry False a b = (a \<and> b)"
thomas@47567
    29
  "carry a False b = (a \<and> b)"
thomas@47567
    30
  "carry a b False = (a \<and> b)"
thomas@47567
    31
  by (auto simp add: carry_def)
thomas@47567
    32
thomas@47567
    33
lemma xor3_simps:
thomas@47567
    34
  "xor3 True a b = (a = b)"
thomas@47567
    35
  "xor3 a True b = (a = b)"
thomas@47567
    36
  "xor3 a b True = (a = b)"
thomas@47567
    37
  "xor3 False a b = (a \<noteq> b)"
thomas@47567
    38
  "xor3 a False b = (a \<noteq> b)"
thomas@47567
    39
  "xor3 a b False = (a \<noteq> b)"
thomas@47567
    40
  by (simp_all add: xor3_def)
thomas@47567
    41
thomas@47567
    42
text {* Breaking up word equalities into equalities on their
thomas@47567
    43
bit lists. Equalities are generated and manipulated in the
thomas@47567
    44
reverse order to to_bl. *}
thomas@47567
    45
thomas@47567
    46
lemma word_eq_rbl_eq:
thomas@47567
    47
  "(x = y) = (rev (to_bl x) = rev (to_bl y))"
thomas@47567
    48
  by simp
thomas@47567
    49
thomas@47567
    50
lemma rbl_word_or:
thomas@47567
    51
  "rev (to_bl (x OR y)) = map2 op \<or> (rev (to_bl x)) (rev (to_bl y))"
thomas@47567
    52
  by (simp add: map2_def zip_rev bl_word_or rev_map)
thomas@47567
    53
thomas@47567
    54
lemma rbl_word_and:
thomas@47567
    55
  "rev (to_bl (x AND y)) = map2 op \<and> (rev (to_bl x)) (rev (to_bl y))"
thomas@47567
    56
  by (simp add: map2_def zip_rev bl_word_and rev_map)
thomas@47567
    57
thomas@47567
    58
lemma rbl_word_xor:
thomas@47567
    59
  "rev (to_bl (x XOR y)) = map2 op \<noteq> (rev (to_bl x)) (rev (to_bl y))"
thomas@47567
    60
  by (simp add: map2_def zip_rev bl_word_xor rev_map)
thomas@47567
    61
thomas@47567
    62
lemma rbl_word_not:
thomas@47567
    63
  "rev (to_bl (NOT x)) = map Not (rev (to_bl x))"
thomas@47567
    64
  by (simp add: bl_word_not rev_map)
thomas@47567
    65
thomas@47567
    66
lemma bl_word_sub:
thomas@47567
    67
  "to_bl (x - y) = to_bl (x + (- y))"
haftmann@54230
    68
  by simp
thomas@47567
    69
thomas@47567
    70
lemma rbl_word_1:
thomas@47567
    71
  "rev (to_bl (1 :: ('a :: len0) word))
thomas@47567
    72
     = takefill False (len_of TYPE('a)) [True]"
thomas@47567
    73
  apply (rule_tac s="rev (to_bl (word_succ (0 :: 'a word)))" in trans)
thomas@47567
    74
   apply simp
thomas@47567
    75
  apply (simp only: rtb_rbl_ariths(1)[OF refl])
thomas@47567
    76
  apply simp
thomas@47567
    77
  apply (case_tac "len_of TYPE('a)")
thomas@47567
    78
   apply simp
thomas@47567
    79
  apply (simp add: takefill_alt)
thomas@47567
    80
  done
thomas@47567
    81
thomas@47567
    82
lemma rbl_word_if:
thomas@47567
    83
  "rev (to_bl (if P then x else y))
thomas@47567
    84
      = map2 (If P) (rev (to_bl x)) (rev (to_bl y))"
thomas@47567
    85
  by (simp add: map2_def split_def)
thomas@47567
    86
thomas@47567
    87
lemma rbl_add_carry_Cons:
thomas@47567
    88
  "(if car then rbl_succ else id) (rbl_add (x # xs) (y # ys))
thomas@47567
    89
        = xor3 x y car # (if carry x y car then rbl_succ else id)
thomas@47567
    90
             (rbl_add xs ys)"
thomas@47567
    91
  by (simp add: carry_def xor3_def)
thomas@47567
    92
thomas@47567
    93
lemma rbl_add_suc_carry_fold:
thomas@47567
    94
  "length xs = length ys \<Longrightarrow>
thomas@47567
    95
   \<forall>car. (if car then rbl_succ else id) (rbl_add xs ys)
thomas@47567
    96
        = (foldr (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car))
thomas@47567
    97
                 (zip xs ys) (\<lambda>_. [])) car"
thomas@47567
    98
  apply (erule list_induct2)
thomas@47567
    99
   apply simp
thomas@47567
   100
  apply (simp only: rbl_add_carry_Cons)
thomas@47567
   101
  apply simp
thomas@47567
   102
  done
thomas@47567
   103
thomas@47567
   104
lemma to_bl_plus_carry:
thomas@47567
   105
  "to_bl (x + y)
thomas@47567
   106
     = rev (foldr (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car))
thomas@47567
   107
                 (rev (zip (to_bl x) (to_bl y))) (\<lambda>_. []) False)"
thomas@47567
   108
  using rbl_add_suc_carry_fold[where xs="rev (to_bl x)" and ys="rev (to_bl y)"]
thomas@47567
   109
  apply (simp add: word_add_rbl[OF refl refl])
thomas@47567
   110
  apply (drule_tac x=False in spec)
thomas@47567
   111
  apply (simp add: zip_rev)
thomas@47567
   112
  done
thomas@47567
   113
thomas@47567
   114
definition
thomas@47567
   115
 "rbl_plus cin xs ys = foldr
thomas@47567
   116
       (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car))
thomas@47567
   117
       (zip xs ys) (\<lambda>_. []) cin"
thomas@47567
   118
thomas@47567
   119
lemma rbl_plus_simps:
thomas@47567
   120
  "rbl_plus cin (x # xs) (y # ys)
thomas@47567
   121
      = xor3 x y cin # rbl_plus (carry x y cin) xs ys"
thomas@47567
   122
  "rbl_plus cin [] ys = []"
thomas@47567
   123
  "rbl_plus cin xs [] = []"
thomas@47567
   124
  by (simp_all add: rbl_plus_def)
thomas@47567
   125
thomas@47567
   126
lemma rbl_word_plus:
thomas@47567
   127
  "rev (to_bl (x + y)) = rbl_plus False (rev (to_bl x)) (rev (to_bl y))"
thomas@47567
   128
  by (simp add: rbl_plus_def to_bl_plus_carry zip_rev)
thomas@47567
   129
thomas@47567
   130
definition
thomas@47567
   131
 "rbl_succ2 b xs = (if b then rbl_succ xs else xs)"
thomas@47567
   132
thomas@47567
   133
lemma rbl_succ2_simps:
thomas@47567
   134
  "rbl_succ2 b [] = []"
thomas@47567
   135
  "rbl_succ2 b (x # xs) = (b \<noteq> x) # rbl_succ2 (x \<and> b) xs"
thomas@47567
   136
  by (simp_all add: rbl_succ2_def)
thomas@47567
   137
thomas@47567
   138
lemma twos_complement:
thomas@47567
   139
  "- x = word_succ (NOT x)"
thomas@47567
   140
  using arg_cong[OF word_add_not[where x=x], where f="\<lambda>a. a - x + 1"]
thomas@47567
   141
  by (simp add: word_succ_p1 word_sp_01[unfolded word_succ_p1]
thomas@47567
   142
           del: word_add_not)
thomas@47567
   143
thomas@47567
   144
lemma rbl_word_neg:
thomas@47567
   145
  "rev (to_bl (- x)) = rbl_succ2 True (map Not (rev (to_bl x)))"
thomas@47567
   146
  by (simp add: twos_complement word_succ_rbl[OF refl]
thomas@47567
   147
                bl_word_not rev_map rbl_succ2_def)
thomas@47567
   148
thomas@47567
   149
lemma rbl_word_cat:
thomas@47567
   150
  "rev (to_bl (word_cat x y :: ('a :: len0) word))
thomas@47567
   151
     = takefill False (len_of TYPE('a)) (rev (to_bl y) @ rev (to_bl x))"
thomas@47567
   152
  by (simp add: word_cat_bl word_rev_tf)
thomas@47567
   153
thomas@47567
   154
lemma rbl_word_slice:
thomas@47567
   155
  "rev (to_bl (slice n w :: ('a :: len0) word))
thomas@47567
   156
     = takefill False (len_of TYPE('a)) (drop n (rev (to_bl w)))"
thomas@47567
   157
  apply (simp add: slice_take word_rev_tf rev_take)
thomas@47567
   158
  apply (cases "n < len_of TYPE('b)", simp_all)
thomas@47567
   159
  done
thomas@47567
   160
thomas@47567
   161
lemma rbl_word_ucast:
thomas@47567
   162
  "rev (to_bl (ucast x :: ('a :: len0) word))
thomas@47567
   163
     = takefill False (len_of TYPE('a)) (rev (to_bl x))"
thomas@47567
   164
  apply (simp add: to_bl_ucast takefill_alt)
thomas@47567
   165
  apply (simp add: rev_drop)
thomas@47567
   166
  apply (case_tac "len_of TYPE('a) < len_of TYPE('b)")
thomas@47567
   167
   apply simp_all
thomas@47567
   168
  done
thomas@47567
   169
thomas@47567
   170
lemma rbl_shiftl:
thomas@47567
   171
  "rev (to_bl (w << n)) = takefill False (size w)
thomas@47567
   172
     (replicate n False @ rev (to_bl w))"
thomas@47567
   173
  by (simp add: bl_shiftl takefill_alt word_size rev_drop)
thomas@47567
   174
thomas@47567
   175
lemma rbl_shiftr:
thomas@47567
   176
  "rev (to_bl (w >> n)) = takefill False (size w)
thomas@47567
   177
     (drop n (rev (to_bl w)))"
thomas@47567
   178
  by (simp add: shiftr_slice rbl_word_slice word_size)
thomas@47567
   179
thomas@47567
   180
definition
thomas@47567
   181
 "drop_nonempty v n xs
thomas@47567
   182
     = (if n < length xs then drop n xs else [last (v # xs)])"
thomas@47567
   183
thomas@47567
   184
lemma drop_nonempty_simps:
thomas@47567
   185
  "drop_nonempty v (Suc n) (x # xs) = drop_nonempty x n xs"
thomas@47567
   186
  "drop_nonempty v 0 (x # xs) = (x # xs)"
thomas@47567
   187
  "drop_nonempty v n [] = [v]"
thomas@47567
   188
  by (simp_all add: drop_nonempty_def)
thomas@47567
   189
thomas@47567
   190
definition
thomas@47567
   191
  "takefill_last x n xs = takefill (last (x # xs)) n xs"
thomas@47567
   192
thomas@47567
   193
lemma takefill_last_simps:
thomas@47567
   194
  "takefill_last z (Suc n) (x # xs) = x # takefill_last x n xs"
thomas@47567
   195
  "takefill_last z 0 xs = []"
thomas@47567
   196
  "takefill_last z n [] = replicate n z"
thomas@47567
   197
  apply (simp_all add: takefill_last_def)
thomas@47567
   198
  apply (simp_all add: takefill_alt)
thomas@47567
   199
  done
thomas@47567
   200
thomas@47567
   201
lemma rbl_sshiftr:
thomas@47567
   202
  "rev (to_bl (w >>> n)) = 
thomas@47567
   203
     takefill_last False (size w) 
thomas@47567
   204
        (drop_nonempty False n (rev (to_bl w)))"
thomas@47567
   205
  apply (cases "n < size w")
thomas@47567
   206
   apply (simp add: bl_sshiftr takefill_last_def word_size
thomas@47567
   207
                    takefill_alt rev_take last_rev
thomas@47567
   208
                    drop_nonempty_def)
thomas@47567
   209
  apply (subgoal_tac "(w >>> n) = of_bl (replicate (size w) (msb w))")
thomas@47567
   210
   apply (simp add: word_size takefill_last_def takefill_alt
thomas@47567
   211
                    last_rev word_msb_alt word_rev_tf
thomas@47567
   212
                    drop_nonempty_def take_Cons')
thomas@47567
   213
   apply (case_tac "len_of TYPE('a)", simp_all)
thomas@47567
   214
  apply (rule word_eqI)
thomas@47567
   215
  apply (simp add: nth_sshiftr word_size test_bit_of_bl
thomas@47567
   216
                   msb_nth)
thomas@47567
   217
  done
thomas@47567
   218
thomas@47567
   219
lemma nth_word_of_int:
thomas@47567
   220
  "(word_of_int x :: ('a :: len0) word) !! n
thomas@47567
   221
      = (n < len_of TYPE('a) \<and> bin_nth x n)"
thomas@47567
   222
  apply (simp add: test_bit_bl word_size to_bl_of_bin)
thomas@47567
   223
  apply (subst conj_cong[OF refl], erule bin_nth_bl)
thomas@47567
   224
  apply (auto)
thomas@47567
   225
  done
thomas@47567
   226
thomas@47567
   227
lemma nth_scast:
thomas@47567
   228
  "(scast (x :: ('a :: len) word) :: ('b :: len) word) !! n
thomas@47567
   229
     = (n < len_of TYPE('b) \<and>
thomas@47567
   230
          (if n < len_of TYPE('a) - 1 then x !! n
thomas@47567
   231
           else x !! (len_of TYPE('a) - 1)))"
thomas@47567
   232
  by (simp add: scast_def nth_word_of_int nth_sint)
thomas@47567
   233
thomas@47567
   234
lemma rbl_word_scast:
thomas@47567
   235
  "rev (to_bl (scast x :: ('a :: len) word))
thomas@47567
   236
     = takefill_last False (len_of TYPE('a))
thomas@47567
   237
           (rev (to_bl x))"
thomas@47567
   238
  apply (rule nth_equalityI)
thomas@47567
   239
   apply (simp add: word_size takefill_last_def)
thomas@47567
   240
  apply (clarsimp simp: nth_scast takefill_last_def
thomas@47567
   241
                        nth_takefill word_size nth_rev to_bl_nth)
thomas@47567
   242
  apply (cases "len_of TYPE('b)")
thomas@47567
   243
   apply simp
thomas@47567
   244
  apply (clarsimp simp: less_Suc_eq_le linorder_not_less
thomas@47567
   245
                        last_rev word_msb_alt[symmetric]
thomas@47567
   246
                        msb_nth)
thomas@47567
   247
  done
thomas@47567
   248
thomas@47567
   249
definition
thomas@47567
   250
  rbl_mul :: "bool list \<Rightarrow> bool list \<Rightarrow> bool list"
thomas@47567
   251
where
thomas@47567
   252
 "rbl_mul xs ys = foldr (\<lambda>x sm. rbl_plus False (map (op \<and> x) ys) (False # sm))
thomas@47567
   253
    xs []"
thomas@47567
   254
thomas@47567
   255
lemma rbl_mul_simps:
thomas@47567
   256
  "rbl_mul (x # xs) ys
thomas@47567
   257
     = rbl_plus False (map (op \<and> x) ys) (False # rbl_mul xs ys)"
thomas@47567
   258
  "rbl_mul [] ys = []"
thomas@47567
   259
  by (simp_all add: rbl_mul_def)
thomas@47567
   260
thomas@47567
   261
lemma takefill_le2:
thomas@47567
   262
  "length xs \<le> n \<Longrightarrow>
thomas@47567
   263
   takefill x m (takefill x n xs)
thomas@47567
   264
     = takefill x m xs"
thomas@47567
   265
  by (simp add: takefill_alt replicate_add[symmetric])
thomas@47567
   266
thomas@47567
   267
lemma take_rbl_plus:
thomas@47567
   268
  "\<forall>n b. take n (rbl_plus b xs ys)
thomas@47567
   269
    = rbl_plus b (take n xs) (take n ys)"
thomas@47567
   270
  apply (simp add: rbl_plus_def take_zip[symmetric])
thomas@47567
   271
  apply (rule_tac list="zip xs ys" in list.induct)
thomas@47567
   272
   apply simp
thomas@47567
   273
  apply (clarsimp simp: split_def)
thomas@47567
   274
  apply (case_tac n, simp_all)
thomas@47567
   275
  done
thomas@47567
   276
thomas@47567
   277
lemma word_rbl_mul_induct:
thomas@47567
   278
  fixes y :: "'a :: len word" shows
thomas@47567
   279
  "length xs \<le> size y
thomas@47567
   280
   \<Longrightarrow> rbl_mul xs (rev (to_bl y))
thomas@47567
   281
     = take (length xs) (rev (to_bl (of_bl (rev xs) * y)))"
thomas@47567
   282
proof (induct xs)
thomas@47567
   283
  case Nil
thomas@47567
   284
  show ?case
thomas@47567
   285
    by (simp add: rbl_mul_simps)
thomas@47567
   286
next
thomas@47567
   287
  case (Cons z zs)
thomas@47567
   288
thomas@47567
   289
  have rbl_word_plus':
thomas@47567
   290
    "\<And>(x :: 'a word) y.
thomas@47567
   291
      to_bl (x + y) = rev (rbl_plus False (rev (to_bl x)) (rev (to_bl y)))"
thomas@47567
   292
    by (simp add: rbl_word_plus[symmetric])
thomas@47567
   293
  
thomas@47567
   294
  have mult_bit: "to_bl (of_bl [z] * y) = map (op \<and> z) (to_bl y)"
thomas@47567
   295
    apply (cases z)
thomas@47567
   296
     apply (simp cong: map_cong)
thomas@47567
   297
    apply (simp add: map_replicate_const cong: map_cong)
thomas@47567
   298
    done
thomas@47567
   299
 
thomas@47567
   300
  have shiftl: "\<And>xs. of_bl xs * 2 * y = (of_bl xs * y) << 1"
thomas@47567
   301
    by (simp add: shiftl_t2n)
thomas@47567
   302
thomas@47567
   303
  have zip_take_triv: "\<And>xs ys n. n = length ys
thomas@47567
   304
      \<Longrightarrow> zip (take n xs) ys = zip xs ys"
thomas@47567
   305
    by (rule nth_equalityI, simp_all)
thomas@47567
   306
thomas@47567
   307
  show ?case
thomas@47567
   308
    using Cons
haftmann@57512
   309
    apply (simp add: trans [OF of_bl_append add.commute]
thomas@47567
   310
                     rbl_mul_simps rbl_word_plus'
webertj@49962
   311
                     Cons.hyps distrib_right mult_bit
thomas@47567
   312
                     shiftl rbl_shiftl)
thomas@47567
   313
    apply (simp add: takefill_alt word_size rev_map take_rbl_plus
thomas@47567
   314
                     min_def)
thomas@47567
   315
    apply (simp add: rbl_plus_def zip_take_triv)
thomas@47567
   316
    done
thomas@47567
   317
qed
thomas@47567
   318
thomas@47567
   319
lemma rbl_word_mul:
thomas@47567
   320
  fixes x :: "'a :: len word"
thomas@47567
   321
  shows "rev (to_bl (x * y)) = rbl_mul (rev (to_bl x)) (rev (to_bl y))"
thomas@47567
   322
  using word_rbl_mul_induct[where xs="rev (to_bl x)" and y=y]
thomas@47567
   323
  by (simp add: word_size)
thomas@47567
   324
thomas@47567
   325
text {* Breaking up inequalities into bitlist properties. *}
thomas@47567
   326
thomas@47567
   327
definition
thomas@47567
   328
  "rev_bl_order F xs ys =
thomas@47567
   329
     (length xs = length ys \<and>
thomas@47567
   330
       ((xs = ys \<and> F)
thomas@47567
   331
          \<or> (\<exists>n < length xs. drop (Suc n) xs = drop (Suc n) ys
thomas@47567
   332
                   \<and> \<not> xs ! n \<and> ys ! n)))"
thomas@47567
   333
thomas@47567
   334
lemma rev_bl_order_simps:
thomas@47567
   335
  "rev_bl_order F [] [] = F"
thomas@47567
   336
  "rev_bl_order F (x # xs) (y # ys)
thomas@47567
   337
     = rev_bl_order ((y \<and> \<not> x) \<or> ((y \<or> \<not> x) \<and> F)) xs ys"
thomas@47567
   338
  apply (simp_all add: rev_bl_order_def)
thomas@47567
   339
  apply (rule conj_cong[OF refl])
thomas@47567
   340
  apply (cases "xs = ys")
thomas@47567
   341
   apply (simp add: nth_Cons')
thomas@47567
   342
   apply blast
thomas@47567
   343
  apply (simp add: nth_Cons')
thomas@47567
   344
  apply safe
thomas@47567
   345
   apply (rule_tac x="n - 1" in exI)
thomas@47567
   346
   apply simp
thomas@47567
   347
  apply (rule_tac x="Suc n" in exI)
thomas@47567
   348
  apply simp
thomas@47567
   349
  done
thomas@47567
   350
thomas@47567
   351
lemma rev_bl_order_rev_simp:
thomas@47567
   352
  "length xs = length ys \<Longrightarrow>
thomas@47567
   353
   rev_bl_order F (xs @ [x]) (ys @ [y])
thomas@47567
   354
     = ((y \<and> \<not> x) \<or> ((y \<or> \<not> x) \<and> rev_bl_order F xs ys))"
thomas@47567
   355
  apply (induct arbitrary: F rule: list_induct2)
thomas@47567
   356
   apply (auto simp add: rev_bl_order_simps)
thomas@47567
   357
  done
thomas@47567
   358
thomas@47567
   359
lemma rev_bl_order_bl_to_bin:
thomas@47567
   360
  "length xs = length ys
thomas@47567
   361
     \<Longrightarrow> rev_bl_order True xs ys
thomas@47567
   362
            = (bl_to_bin (rev xs) \<le> bl_to_bin (rev ys))
thomas@47567
   363
       \<and> rev_bl_order False xs ys
thomas@47567
   364
            = (bl_to_bin (rev xs) < bl_to_bin (rev ys))"
thomas@47567
   365
  apply (induct xs ys rule: list_induct2)
thomas@47567
   366
   apply (simp_all add: rev_bl_order_simps bl_to_bin_app_cat)
haftmann@54847
   367
  apply (auto simp add: bl_to_bin_def Bit_B0 Bit_B1 add1_zle_eq Bit_def)
thomas@47567
   368
  done
thomas@47567
   369
thomas@47567
   370
lemma word_le_rbl:
thomas@47567
   371
  fixes x :: "('a :: len0) word"
thomas@47567
   372
  shows "(x \<le> y) = rev_bl_order True (rev (to_bl x)) (rev (to_bl y))"
thomas@47567
   373
  by (simp add: rev_bl_order_bl_to_bin word_le_def)
thomas@47567
   374
thomas@47567
   375
lemma word_less_rbl:
thomas@47567
   376
  fixes x :: "('a :: len0) word"
thomas@47567
   377
  shows "(x < y) = rev_bl_order False (rev (to_bl x)) (rev (to_bl y))"
thomas@47567
   378
  by (simp add: word_less_alt rev_bl_order_bl_to_bin)
thomas@47567
   379
thomas@47567
   380
lemma word_sint_msb_eq:
thomas@47567
   381
  "sint x = uint x - (if msb x then 2 ^ size x else 0)"
thomas@47567
   382
  apply (cases "msb x")
thomas@47567
   383
   apply (rule word_sint.Abs_eqD[where 'a='a], simp_all)
thomas@47567
   384
    apply (simp add: word_size wi_hom_syms
thomas@47567
   385
                     word_of_int_2p_len)
thomas@47567
   386
   apply (simp add: sints_num word_size)
thomas@47567
   387
   apply (rule conjI)
thomas@47567
   388
    apply (simp add: le_diff_eq')
thomas@47567
   389
    apply (rule order_trans[where y="2 ^ (len_of TYPE('a) - 1)"])
thomas@47567
   390
     apply (simp add: power_Suc[symmetric])
thomas@47567
   391
    apply (simp add: linorder_not_less[symmetric] mask_eq_iff[symmetric])
thomas@47567
   392
    apply (rule notI, drule word_eqD[where x="size x - 1"])
thomas@47567
   393
    apply (simp add: msb_nth word_ops_nth_size word_size)
thomas@47567
   394
   apply (simp add: order_less_le_trans[where y=0])
thomas@47567
   395
  apply (rule word_uint.Abs_eqD[where 'a='a], simp_all)
thomas@47567
   396
  apply (simp add: linorder_not_less uints_num word_msb_sint)
thomas@47567
   397
  apply (rule order_less_le_trans[OF sint_lt])
thomas@47567
   398
  apply simp
thomas@47567
   399
  done
thomas@47567
   400
thomas@47567
   401
lemma word_sle_msb_le:
thomas@47567
   402
  "(x <=s y) = ((msb y --> msb x) \<and> 
thomas@47567
   403
                  ((msb x \<and> \<not> msb y) \<or> (x <= y)))"
thomas@47567
   404
  apply (simp add: word_sle_def word_sint_msb_eq word_size
thomas@47567
   405
                   word_le_def)
thomas@47567
   406
  apply safe
thomas@47567
   407
   apply (rule order_trans[OF _ uint_ge_0])
thomas@47567
   408
   apply (simp add: order_less_imp_le)
thomas@47567
   409
  apply (erule notE[OF leD])
thomas@47567
   410
  apply (rule order_less_le_trans[OF _ uint_ge_0])
thomas@47567
   411
  apply simp
thomas@47567
   412
  done
thomas@47567
   413
thomas@47567
   414
lemma word_sless_msb_less:
thomas@47567
   415
  "(x <s y) = ((msb y --> msb x) \<and> 
thomas@47567
   416
                  ((msb x \<and> \<not> msb y) \<or> (x < y)))"
thomas@47567
   417
  by (auto simp add: word_sless_def word_sle_msb_le)
thomas@47567
   418
thomas@47567
   419
definition
thomas@47567
   420
  "map_last f xs = (if xs = [] then [] else butlast xs @ [f (last xs)])"
thomas@47567
   421
thomas@47567
   422
lemma map_last_simps:
thomas@47567
   423
  "map_last f [] = []"
thomas@47567
   424
  "map_last f [x] = [f x]"
thomas@47567
   425
  "map_last f (x # y # zs) = x # map_last f (y # zs)"
thomas@47567
   426
  by (simp_all add: map_last_def)
thomas@47567
   427
thomas@47567
   428
lemma word_sle_rbl:
thomas@47567
   429
  "(x <=s y) = rev_bl_order True (map_last Not (rev (to_bl x)))
thomas@47567
   430
     (map_last Not (rev (to_bl y)))"
thomas@47567
   431
  using word_msb_alt[where w=x] word_msb_alt[where w=y]
thomas@47567
   432
  apply (simp add: word_sle_msb_le word_le_rbl)
thomas@47567
   433
  apply (subgoal_tac "length (to_bl x) = length (to_bl y)")
thomas@47567
   434
   apply (cases "to_bl x", simp)
thomas@47567
   435
   apply (cases "to_bl y", simp)
thomas@47567
   436
   apply (clarsimp simp: map_last_def rev_bl_order_rev_simp)
thomas@47567
   437
   apply auto
thomas@47567
   438
  done
thomas@47567
   439
thomas@47567
   440
lemma word_sless_rbl:
thomas@47567
   441
  "(x <s y) = rev_bl_order False (map_last Not (rev (to_bl x)))
thomas@47567
   442
     (map_last Not (rev (to_bl y)))"
thomas@47567
   443
  using word_msb_alt[where w=x] word_msb_alt[where w=y]
thomas@47567
   444
  apply (simp add: word_sless_msb_less word_less_rbl)
thomas@47567
   445
  apply (subgoal_tac "length (to_bl x) = length (to_bl y)")
thomas@47567
   446
   apply (cases "to_bl x", simp)
thomas@47567
   447
   apply (cases "to_bl y", simp)
thomas@47567
   448
   apply (clarsimp simp: map_last_def rev_bl_order_rev_simp)
thomas@47567
   449
   apply auto
thomas@47567
   450
  done
thomas@47567
   451
thomas@47567
   452
text {* Lemmas for unpacking rev (to_bl n) for numerals n and also
thomas@47567
   453
for irreducible values and expressions. *}
thomas@47567
   454
thomas@47567
   455
lemma rev_bin_to_bl_simps:
thomas@47567
   456
  "rev (bin_to_bl 0 x) = []"
thomas@47567
   457
  "rev (bin_to_bl (Suc n) (numeral (num.Bit0 nm)))
thomas@47567
   458
    = False # rev (bin_to_bl n (numeral nm))"
thomas@47567
   459
  "rev (bin_to_bl (Suc n) (numeral (num.Bit1 nm)))
thomas@47567
   460
    = True # rev (bin_to_bl n (numeral nm))"
thomas@47567
   461
  "rev (bin_to_bl (Suc n) (numeral (num.One)))
thomas@47567
   462
    = True # replicate n False"
haftmann@54489
   463
  "rev (bin_to_bl (Suc n) (- numeral (num.Bit0 nm)))
haftmann@54489
   464
    = False # rev (bin_to_bl n (- numeral nm))"
haftmann@54489
   465
  "rev (bin_to_bl (Suc n) (- numeral (num.Bit1 nm)))
haftmann@54489
   466
    = True # rev (bin_to_bl n (- numeral (nm + num.One)))"
haftmann@54489
   467
  "rev (bin_to_bl (Suc n) (- numeral (num.One)))
thomas@47567
   468
    = True # replicate n True"
haftmann@54489
   469
  "rev (bin_to_bl (Suc n) (- numeral (num.Bit0 nm + num.One)))
haftmann@54489
   470
    = True # rev (bin_to_bl n (- numeral (nm + num.One)))"
haftmann@54489
   471
  "rev (bin_to_bl (Suc n) (- numeral (num.Bit1 nm + num.One)))
haftmann@54489
   472
    = False # rev (bin_to_bl n (- numeral (nm + num.One)))"
haftmann@54489
   473
  "rev (bin_to_bl (Suc n) (- numeral (num.One + num.One)))
haftmann@54489
   474
    = False # rev (bin_to_bl n (- numeral num.One))"
thomas@47567
   475
  apply (simp_all add: bin_to_bl_def)
thomas@47567
   476
  apply (simp_all only: bin_to_bl_aux_alt)
thomas@47567
   477
  apply (simp_all)
thomas@47567
   478
  apply (simp_all add: bin_to_bl_zero_aux bin_to_bl_minus1_aux)
thomas@47567
   479
  done
thomas@47567
   480
thomas@47567
   481
lemma to_bl_upt:
thomas@47567
   482
  "to_bl x = rev (map (op !! x) [0 ..< size x])"
thomas@47567
   483
  apply (rule nth_equalityI)
thomas@47567
   484
   apply (simp add: word_size)
thomas@47567
   485
  apply (clarsimp simp: to_bl_nth word_size nth_rev)
thomas@47567
   486
  done
thomas@47567
   487
thomas@47567
   488
lemma rev_to_bl_upt:
thomas@47567
   489
  "rev (to_bl x) = map (op !! x) [0 ..< size x]"
thomas@47567
   490
  by (simp add: to_bl_upt)
thomas@47567
   491
thomas@47567
   492
lemma upt_eq_list_intros:
thomas@47567
   493
  "j <= i \<Longrightarrow> [i ..< j] = []"
thomas@47567
   494
  "\<lbrakk> i = x; x < j; [x + 1 ..< j] = xs \<rbrakk> \<Longrightarrow> [i ..< j] = (x # xs)"
thomas@47567
   495
  by (simp_all add: upt_eq_Nil_conv upt_eq_Cons_conv)
thomas@47567
   496
thomas@47567
   497
text {* Tactic definition *}
thomas@47567
   498
thomas@47567
   499
ML {*
thomas@47567
   500
thomas@47567
   501
structure Word_Bitwise_Tac = struct
thomas@47567
   502
wenzelm@51686
   503
val word_ss = simpset_of @{theory_context Word};
thomas@47567
   504
thomas@47567
   505
fun mk_nat_clist ns = List.foldr
thomas@47567
   506
  (uncurry (Thm.mk_binop @{cterm "Cons :: nat => _"}))
thomas@47567
   507
  @{cterm "[] :: nat list"} ns;
thomas@47567
   508
wenzelm@51717
   509
fun upt_conv ctxt ct =
wenzelm@59582
   510
  case Thm.term_of ct of
wenzelm@51717
   511
    (@{const upt} $ n $ m) =>
wenzelm@51717
   512
      let
wenzelm@59058
   513
        val (i, j) = apply2 (snd o HOLogic.dest_number) (n, m);
wenzelm@51717
   514
        val ns = map (Numeral.mk_cnumber @{ctyp nat}) (i upto (j - 1))
wenzelm@51717
   515
          |> mk_nat_clist;
wenzelm@51717
   516
        val prop = Thm.mk_binop @{cterm "op = :: nat list => _"} ct ns
wenzelm@51717
   517
                     |> Thm.apply @{cterm Trueprop};
wenzelm@51717
   518
      in
wenzelm@51717
   519
        try (fn () =>
wenzelm@54883
   520
          Goal.prove_internal ctxt [] prop 
wenzelm@59498
   521
            (K (REPEAT_DETERM (resolve_tac ctxt @{thms upt_eq_list_intros} 1
wenzelm@51717
   522
                ORELSE simp_tac (put_simpset word_ss ctxt) 1))) |> mk_meta_eq) ()
wenzelm@51717
   523
      end
thomas@47567
   524
  | _ => NONE;
thomas@47567
   525
thomas@47567
   526
val expand_upt_simproc = Simplifier.make_simproc
thomas@47567
   527
  {lhss = [@{cpat "upt _ _"}],
thomas@47567
   528
   name = "expand_upt", identifier = [],
wenzelm@51717
   529
   proc = K upt_conv};
thomas@47567
   530
wenzelm@51717
   531
fun word_len_simproc_fn ctxt ct =
wenzelm@59582
   532
  case Thm.term_of ct of
thomas@47567
   533
    Const (@{const_name len_of}, _) $ t => (let
thomas@47567
   534
        val T = fastype_of t |> dest_Type |> snd |> the_single
thomas@47567
   535
        val n = Numeral.mk_cnumber @{ctyp nat} (Word_Lib.dest_binT T);
thomas@47567
   536
        val prop = Thm.mk_binop @{cterm "op = :: nat => _"} ct n
thomas@47567
   537
                 |> Thm.apply @{cterm Trueprop};
wenzelm@54883
   538
      in Goal.prove_internal ctxt [] prop (K (simp_tac (put_simpset word_ss ctxt) 1))
thomas@47567
   539
             |> mk_meta_eq |> SOME end
thomas@47567
   540
    handle TERM _ => NONE | TYPE _ => NONE)
thomas@47567
   541
  | _ => NONE;
thomas@47567
   542
thomas@47567
   543
val word_len_simproc = Simplifier.make_simproc
thomas@47567
   544
  {lhss = [@{cpat "len_of _"}],
thomas@47567
   545
   name = "word_len", identifier = [],
wenzelm@51717
   546
   proc = K word_len_simproc_fn};
thomas@47567
   547
thomas@47567
   548
(* convert 5 or nat 5 to Suc 4 when n_sucs = 1, Suc (Suc 4) when n_sucs = 2,
thomas@47567
   549
   or just 5 (discarding nat) when n_sucs = 0 *)
thomas@47567
   550
wenzelm@51717
   551
fun nat_get_Suc_simproc_fn n_sucs ctxt ct =
wenzelm@51717
   552
  let
wenzelm@51717
   553
    val thy = Proof_Context.theory_of ctxt;
wenzelm@59582
   554
    val (f $ arg) = Thm.term_of ct;
thomas@47567
   555
    val n = (case arg of @{term nat} $ n => n | n => n)
thomas@47567
   556
      |> HOLogic.dest_number |> snd;
thomas@47567
   557
    val (i, j) = if n > n_sucs then (n_sucs, n - n_sucs)
thomas@47567
   558
      else (n, 0);
thomas@47567
   559
    val arg' = List.foldr (op $) (HOLogic.mk_number @{typ nat} j)
thomas@47567
   560
        (replicate i @{term Suc});
thomas@47567
   561
    val _ = if arg = arg' then raise TERM ("", []) else ();
thomas@47567
   562
    fun propfn g = HOLogic.mk_eq (g arg, g arg')
wenzelm@59621
   563
      |> HOLogic.mk_Trueprop |> Thm.global_cterm_of thy;
wenzelm@54883
   564
    val eq1 = Goal.prove_internal ctxt [] (propfn I)
wenzelm@51717
   565
      (K (simp_tac (put_simpset word_ss ctxt) 1));
wenzelm@54883
   566
  in Goal.prove_internal ctxt [] (propfn (curry (op $) f))
wenzelm@51717
   567
      (K (simp_tac (put_simpset HOL_ss ctxt addsimps [eq1]) 1))
thomas@47567
   568
       |> mk_meta_eq |> SOME end
thomas@47567
   569
    handle TERM _ => NONE;
thomas@47567
   570
wenzelm@54883
   571
fun nat_get_Suc_simproc n_sucs cts = Simplifier.make_simproc
thomas@47567
   572
  {lhss = map (fn t => Thm.apply t @{cpat "?n :: nat"}) cts,
thomas@47567
   573
   name = "nat_get_Suc", identifier = [],
wenzelm@51717
   574
   proc = K (nat_get_Suc_simproc_fn n_sucs)};
thomas@47567
   575
wenzelm@51717
   576
val no_split_ss =
wenzelm@51717
   577
  simpset_of (put_simpset HOL_ss @{context}
wenzelm@51717
   578
    |> Splitter.del_split @{thm split_if});
thomas@47567
   579
wenzelm@51717
   580
val expand_word_eq_sss =
wenzelm@51717
   581
  (simpset_of (put_simpset HOL_basic_ss @{context} addsimps
wenzelm@51717
   582
       @{thms word_eq_rbl_eq word_le_rbl word_less_rbl word_sle_rbl word_sless_rbl}),
wenzelm@51717
   583
  map simpset_of [
wenzelm@51717
   584
   put_simpset no_split_ss @{context} addsimps
wenzelm@51717
   585
    @{thms rbl_word_plus rbl_word_and rbl_word_or rbl_word_not
thomas@47567
   586
                                rbl_word_neg bl_word_sub rbl_word_xor
thomas@47567
   587
                                rbl_word_cat rbl_word_slice rbl_word_scast
thomas@47567
   588
                                rbl_word_ucast rbl_shiftl rbl_shiftr rbl_sshiftr
thomas@47567
   589
                                rbl_word_if},
wenzelm@51717
   590
   put_simpset no_split_ss @{context} addsimps
wenzelm@51717
   591
    @{thms to_bl_numeral to_bl_neg_numeral to_bl_0 rbl_word_1},
wenzelm@51717
   592
   put_simpset no_split_ss @{context} addsimps
wenzelm@51717
   593
    @{thms rev_rev_ident rev_replicate rev_map to_bl_upt word_size}
thomas@47567
   594
          addsimprocs [word_len_simproc],
wenzelm@51717
   595
   put_simpset no_split_ss @{context} addsimps
blanchet@55465
   596
    @{thms list.simps split_conv replicate.simps list.map
thomas@47567
   597
                                zip_Cons_Cons zip_Nil drop_Suc_Cons drop_0 drop_Nil
thomas@47567
   598
                                foldr.simps map2_Cons map2_Nil takefill_Suc_Cons
thomas@47567
   599
                                takefill_Suc_Nil takefill.Z rbl_succ2_simps
thomas@47567
   600
                                rbl_plus_simps rev_bin_to_bl_simps append.simps
thomas@47567
   601
                                takefill_last_simps drop_nonempty_simps
thomas@47567
   602
                                rev_bl_order_simps}
thomas@47567
   603
          addsimprocs [expand_upt_simproc,
wenzelm@54883
   604
                       nat_get_Suc_simproc 4
thomas@47567
   605
                         [@{cpat replicate}, @{cpat "takefill ?x"},
thomas@47567
   606
                          @{cpat drop}, @{cpat "bin_to_bl"},
thomas@47567
   607
                          @{cpat "takefill_last ?x"},
thomas@47567
   608
                          @{cpat "drop_nonempty ?x"}]],
wenzelm@51717
   609
    put_simpset no_split_ss @{context} addsimps @{thms xor3_simps carry_simps if_bool_simps}
thomas@47567
   610
  ])
thomas@47567
   611
wenzelm@51717
   612
fun tac ctxt =
wenzelm@50107
   613
  let
thomas@47567
   614
    val (ss, sss) = expand_word_eq_sss;
wenzelm@51717
   615
  in
wenzelm@51717
   616
    foldr1 (op THEN_ALL_NEW)
wenzelm@51717
   617
      ((CHANGED o safe_full_simp_tac (put_simpset ss ctxt)) ::
wenzelm@51717
   618
        map (fn ss => safe_full_simp_tac (put_simpset ss ctxt)) sss)
wenzelm@51717
   619
  end;
thomas@47567
   620
thomas@47567
   621
end
thomas@47567
   622
thomas@47567
   623
*}
thomas@47567
   624
thomas@47567
   625
method_setup word_bitwise =
wenzelm@51717
   626
  {* Scan.succeed (fn ctxt => Method.SIMPLE_METHOD (Word_Bitwise_Tac.tac ctxt 1))  *}
thomas@47567
   627
  "decomposer for word equalities and inequalities into bit propositions"
thomas@47567
   628
thomas@47567
   629
end