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