tuned theory names
authorhaftmann
Tue Apr 16 19:50:18 2019 +0000 (7 days ago)
changeset 70173c2786fe88064
parent 70172 c247bf924d25
child 70174 40fdd74b75f3
tuned theory names
src/HOL/ROOT
src/HOL/Word/Word.thy
src/HOL/Word/WordBitwise.thy
src/HOL/Word/WordExamples.thy
src/HOL/Word/Word_Bitwise.thy
src/HOL/Word/Word_Examples.thy
     1.1 --- a/src/HOL/ROOT	Tue Apr 16 19:50:09 2019 +0000
     1.2 +++ b/src/HOL/ROOT	Tue Apr 16 19:50:18 2019 +0000
     1.3 @@ -829,8 +829,8 @@
     1.4      "HOL-Library"
     1.5    theories
     1.6      Word
     1.7 -    WordBitwise
     1.8 -    WordExamples
     1.9 +    Word_Bitwise
    1.10 +    Word_Examples
    1.11    document_files "root.bib" "root.tex"
    1.12  
    1.13  session "HOL-Statespace" in Statespace = HOL +
     2.1 --- a/src/HOL/Word/Word.thy	Tue Apr 16 19:50:09 2019 +0000
     2.2 +++ b/src/HOL/Word/Word.thy	Tue Apr 16 19:50:18 2019 +0000
     2.3 @@ -14,7 +14,7 @@
     2.4    Misc_Arithmetic
     2.5  begin
     2.6  
     2.7 -text \<open>See \<^file>\<open>WordExamples.thy\<close> for examples.\<close>
     2.8 +text \<open>See \<^file>\<open>Word_Examples.thy\<close> for examples.\<close>
     2.9  
    2.10  subsection \<open>Type definition\<close>
    2.11  
     3.1 --- a/src/HOL/Word/WordBitwise.thy	Tue Apr 16 19:50:09 2019 +0000
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,544 +0,0 @@
     3.4 -(*  Title:      HOL/Word/WordBitwise.thy
     3.5 -    Authors:    Thomas Sewell, NICTA and Sascha Boehme, TU Muenchen
     3.6 -*)
     3.7 -
     3.8 -theory WordBitwise
     3.9 -  imports Word
    3.10 -begin
    3.11 -
    3.12 -text \<open>Helper constants used in defining addition\<close>
    3.13 -
    3.14 -definition xor3 :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool"
    3.15 -  where "xor3 a b c = (a = (b = c))"
    3.16 -
    3.17 -definition carry :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool"
    3.18 -  where "carry a b c = ((a \<and> (b \<or> c)) \<or> (b \<and> c))"
    3.19 -
    3.20 -lemma carry_simps:
    3.21 -  "carry True a b = (a \<or> b)"
    3.22 -  "carry a True b = (a \<or> b)"
    3.23 -  "carry a b True = (a \<or> b)"
    3.24 -  "carry False a b = (a \<and> b)"
    3.25 -  "carry a False b = (a \<and> b)"
    3.26 -  "carry a b False = (a \<and> b)"
    3.27 -  by (auto simp add: carry_def)
    3.28 -
    3.29 -lemma xor3_simps:
    3.30 -  "xor3 True a b = (a = b)"
    3.31 -  "xor3 a True b = (a = b)"
    3.32 -  "xor3 a b True = (a = b)"
    3.33 -  "xor3 False a b = (a \<noteq> b)"
    3.34 -  "xor3 a False b = (a \<noteq> b)"
    3.35 -  "xor3 a b False = (a \<noteq> b)"
    3.36 -  by (simp_all add: xor3_def)
    3.37 -
    3.38 -text \<open>Breaking up word equalities into equalities on their
    3.39 -  bit lists. Equalities are generated and manipulated in the
    3.40 -  reverse order to \<^const>\<open>to_bl\<close>.\<close>
    3.41 -
    3.42 -lemma word_eq_rbl_eq: "x = y \<longleftrightarrow> rev (to_bl x) = rev (to_bl y)"
    3.43 -  by simp
    3.44 -
    3.45 -lemma rbl_word_or: "rev (to_bl (x OR y)) = map2 (\<or>) (rev (to_bl x)) (rev (to_bl y))"
    3.46 -  by (simp add: map2_def zip_rev bl_word_or rev_map)
    3.47 -
    3.48 -lemma rbl_word_and: "rev (to_bl (x AND y)) = map2 (\<and>) (rev (to_bl x)) (rev (to_bl y))"
    3.49 -  by (simp add: map2_def zip_rev bl_word_and rev_map)
    3.50 -
    3.51 -lemma rbl_word_xor: "rev (to_bl (x XOR y)) = map2 (\<noteq>) (rev (to_bl x)) (rev (to_bl y))"
    3.52 -  by (simp add: map2_def zip_rev bl_word_xor rev_map)
    3.53 -
    3.54 -lemma rbl_word_not: "rev (to_bl (NOT x)) = map Not (rev (to_bl x))"
    3.55 -  by (simp add: bl_word_not rev_map)
    3.56 -
    3.57 -lemma bl_word_sub: "to_bl (x - y) = to_bl (x + (- y))"
    3.58 -  by simp
    3.59 -
    3.60 -lemma rbl_word_1: "rev (to_bl (1 :: 'a::len0 word)) = takefill False (len_of TYPE('a)) [True]"
    3.61 -  apply (rule_tac s="rev (to_bl (word_succ (0 :: 'a word)))" in trans)
    3.62 -   apply simp
    3.63 -  apply (simp only: rtb_rbl_ariths(1)[OF refl])
    3.64 -  apply simp
    3.65 -  apply (case_tac "len_of TYPE('a)")
    3.66 -   apply simp
    3.67 -  apply (simp add: takefill_alt)
    3.68 -  done
    3.69 -
    3.70 -lemma rbl_word_if: "rev (to_bl (if P then x else y)) = map2 (If P) (rev (to_bl x)) (rev (to_bl y))"
    3.71 -  by (simp add: map2_def split_def)
    3.72 -
    3.73 -lemma rbl_add_carry_Cons:
    3.74 -  "(if car then rbl_succ else id) (rbl_add (x # xs) (y # ys)) =
    3.75 -    xor3 x y car # (if carry x y car then rbl_succ else id) (rbl_add xs ys)"
    3.76 -  by (simp add: carry_def xor3_def)
    3.77 -
    3.78 -lemma rbl_add_suc_carry_fold:
    3.79 -  "length xs = length ys \<Longrightarrow>
    3.80 -    \<forall>car. (if car then rbl_succ else id) (rbl_add xs ys) =
    3.81 -      (foldr (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car)) (zip xs ys) (\<lambda>_. [])) car"
    3.82 -  apply (erule list_induct2)
    3.83 -   apply simp
    3.84 -  apply (simp only: rbl_add_carry_Cons)
    3.85 -  apply simp
    3.86 -  done
    3.87 -
    3.88 -lemma to_bl_plus_carry:
    3.89 -  "to_bl (x + y) =
    3.90 -    rev (foldr (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car))
    3.91 -      (rev (zip (to_bl x) (to_bl y))) (\<lambda>_. []) False)"
    3.92 -  using rbl_add_suc_carry_fold[where xs="rev (to_bl x)" and ys="rev (to_bl y)"]
    3.93 -  apply (simp add: word_add_rbl[OF refl refl])
    3.94 -  apply (drule_tac x=False in spec)
    3.95 -  apply (simp add: zip_rev)
    3.96 -  done
    3.97 -
    3.98 -definition "rbl_plus cin xs ys =
    3.99 -  foldr (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car)) (zip xs ys) (\<lambda>_. []) cin"
   3.100 -
   3.101 -lemma rbl_plus_simps:
   3.102 -  "rbl_plus cin (x # xs) (y # ys) = xor3 x y cin # rbl_plus (carry x y cin) xs ys"
   3.103 -  "rbl_plus cin [] ys = []"
   3.104 -  "rbl_plus cin xs [] = []"
   3.105 -  by (simp_all add: rbl_plus_def)
   3.106 -
   3.107 -lemma rbl_word_plus: "rev (to_bl (x + y)) = rbl_plus False (rev (to_bl x)) (rev (to_bl y))"
   3.108 -  by (simp add: rbl_plus_def to_bl_plus_carry zip_rev)
   3.109 -
   3.110 -definition "rbl_succ2 b xs = (if b then rbl_succ xs else xs)"
   3.111 -
   3.112 -lemma rbl_succ2_simps:
   3.113 -  "rbl_succ2 b [] = []"
   3.114 -  "rbl_succ2 b (x # xs) = (b \<noteq> x) # rbl_succ2 (x \<and> b) xs"
   3.115 -  by (simp_all add: rbl_succ2_def)
   3.116 -
   3.117 -lemma twos_complement: "- x = word_succ (NOT x)"
   3.118 -  using arg_cong[OF word_add_not[where x=x], where f="\<lambda>a. a - x + 1"]
   3.119 -  by (simp add: word_succ_p1 word_sp_01[unfolded word_succ_p1] del: word_add_not)
   3.120 -
   3.121 -lemma rbl_word_neg: "rev (to_bl (- x)) = rbl_succ2 True (map Not (rev (to_bl x)))"
   3.122 -  by (simp add: twos_complement word_succ_rbl[OF refl] bl_word_not rev_map rbl_succ2_def)
   3.123 -
   3.124 -lemma rbl_word_cat:
   3.125 -  "rev (to_bl (word_cat x y :: 'a::len0 word)) =
   3.126 -    takefill False (len_of TYPE('a)) (rev (to_bl y) @ rev (to_bl x))"
   3.127 -  by (simp add: word_cat_bl word_rev_tf)
   3.128 -
   3.129 -lemma rbl_word_slice:
   3.130 -  "rev (to_bl (slice n w :: 'a::len0 word)) =
   3.131 -    takefill False (len_of TYPE('a)) (drop n (rev (to_bl w)))"
   3.132 -  apply (simp add: slice_take word_rev_tf rev_take)
   3.133 -  apply (cases "n < len_of TYPE('b)", simp_all)
   3.134 -  done
   3.135 -
   3.136 -lemma rbl_word_ucast:
   3.137 -  "rev (to_bl (ucast x :: 'a::len0 word)) = takefill False (len_of TYPE('a)) (rev (to_bl x))"
   3.138 -  apply (simp add: to_bl_ucast takefill_alt)
   3.139 -  apply (simp add: rev_drop)
   3.140 -  apply (cases "len_of TYPE('a) < len_of TYPE('b)")
   3.141 -   apply simp_all
   3.142 -  done
   3.143 -
   3.144 -lemma rbl_shiftl:
   3.145 -  "rev (to_bl (w << n)) = takefill False (size w) (replicate n False @ rev (to_bl w))"
   3.146 -  by (simp add: bl_shiftl takefill_alt word_size rev_drop)
   3.147 -
   3.148 -lemma rbl_shiftr:
   3.149 -  "rev (to_bl (w >> n)) = takefill False (size w) (drop n (rev (to_bl w)))"
   3.150 -  by (simp add: shiftr_slice rbl_word_slice word_size)
   3.151 -
   3.152 -definition "drop_nonempty v n xs = (if n < length xs then drop n xs else [last (v # xs)])"
   3.153 -
   3.154 -lemma drop_nonempty_simps:
   3.155 -  "drop_nonempty v (Suc n) (x # xs) = drop_nonempty x n xs"
   3.156 -  "drop_nonempty v 0 (x # xs) = (x # xs)"
   3.157 -  "drop_nonempty v n [] = [v]"
   3.158 -  by (simp_all add: drop_nonempty_def)
   3.159 -
   3.160 -definition "takefill_last x n xs = takefill (last (x # xs)) n xs"
   3.161 -
   3.162 -lemma takefill_last_simps:
   3.163 -  "takefill_last z (Suc n) (x # xs) = x # takefill_last x n xs"
   3.164 -  "takefill_last z 0 xs = []"
   3.165 -  "takefill_last z n [] = replicate n z"
   3.166 -  by (simp_all add: takefill_last_def) (simp_all add: takefill_alt)
   3.167 -
   3.168 -lemma rbl_sshiftr:
   3.169 -  "rev (to_bl (w >>> n)) = takefill_last False (size w) (drop_nonempty False n (rev (to_bl w)))"
   3.170 -  apply (cases "n < size w")
   3.171 -   apply (simp add: bl_sshiftr takefill_last_def word_size
   3.172 -      takefill_alt rev_take last_rev
   3.173 -      drop_nonempty_def)
   3.174 -  apply (subgoal_tac "(w >>> n) = of_bl (replicate (size w) (msb w))")
   3.175 -   apply (simp add: word_size takefill_last_def takefill_alt
   3.176 -      last_rev word_msb_alt word_rev_tf
   3.177 -      drop_nonempty_def take_Cons')
   3.178 -   apply (case_tac "len_of TYPE('a)", simp_all)
   3.179 -  apply (rule word_eqI)
   3.180 -  apply (simp add: nth_sshiftr word_size test_bit_of_bl
   3.181 -      msb_nth)
   3.182 -  done
   3.183 -
   3.184 -lemma nth_word_of_int:
   3.185 -  "(word_of_int x :: 'a::len0 word) !! n = (n < len_of TYPE('a) \<and> bin_nth x n)"
   3.186 -  apply (simp add: test_bit_bl word_size to_bl_of_bin)
   3.187 -  apply (subst conj_cong[OF refl], erule bin_nth_bl)
   3.188 -  apply auto
   3.189 -  done
   3.190 -
   3.191 -lemma nth_scast:
   3.192 -  "(scast (x :: 'a::len word) :: 'b::len word) !! n =
   3.193 -    (n < len_of TYPE('b) \<and>
   3.194 -    (if n < len_of TYPE('a) - 1 then x !! n
   3.195 -     else x !! (len_of TYPE('a) - 1)))"
   3.196 -  by (simp add: scast_def nth_sint)
   3.197 -
   3.198 -lemma rbl_word_scast:
   3.199 -  "rev (to_bl (scast x :: 'a::len word)) = takefill_last False (len_of TYPE('a)) (rev (to_bl x))"
   3.200 -  apply (rule nth_equalityI)
   3.201 -   apply (simp add: word_size takefill_last_def)
   3.202 -  apply (clarsimp simp: nth_scast takefill_last_def
   3.203 -      nth_takefill word_size nth_rev to_bl_nth)
   3.204 -  apply (cases "len_of TYPE('b)")
   3.205 -   apply simp
   3.206 -  apply (clarsimp simp: less_Suc_eq_le linorder_not_less
   3.207 -      last_rev word_msb_alt[symmetric]
   3.208 -      msb_nth)
   3.209 -  done
   3.210 -
   3.211 -definition rbl_mul :: "bool list \<Rightarrow> bool list \<Rightarrow> bool list"
   3.212 -  where "rbl_mul xs ys = foldr (\<lambda>x sm. rbl_plus False (map ((\<and>) x) ys) (False # sm)) xs []"
   3.213 -
   3.214 -lemma rbl_mul_simps:
   3.215 -  "rbl_mul (x # xs) ys = rbl_plus False (map ((\<and>) x) ys) (False # rbl_mul xs ys)"
   3.216 -  "rbl_mul [] ys = []"
   3.217 -  by (simp_all add: rbl_mul_def)
   3.218 -
   3.219 -lemma takefill_le2: "length xs \<le> n \<Longrightarrow> takefill x m (takefill x n xs) = takefill x m xs"
   3.220 -  by (simp add: takefill_alt replicate_add[symmetric])
   3.221 -
   3.222 -lemma take_rbl_plus: "\<forall>n b. take n (rbl_plus b xs ys) = rbl_plus b (take n xs) (take n ys)"
   3.223 -  apply (simp add: rbl_plus_def take_zip[symmetric])
   3.224 -  apply (rule_tac list="zip xs ys" in list.induct)
   3.225 -   apply simp
   3.226 -  apply (clarsimp simp: split_def)
   3.227 -  apply (case_tac n, simp_all)
   3.228 -  done
   3.229 -
   3.230 -lemma word_rbl_mul_induct:
   3.231 -  "length xs \<le> size y \<Longrightarrow>
   3.232 -    rbl_mul xs (rev (to_bl y)) = take (length xs) (rev (to_bl (of_bl (rev xs) * y)))"
   3.233 -  for y :: "'a::len word"
   3.234 -proof (induct xs)
   3.235 -  case Nil
   3.236 -  show ?case by (simp add: rbl_mul_simps)
   3.237 -next
   3.238 -  case (Cons z zs)
   3.239 -
   3.240 -  have rbl_word_plus': "to_bl (x + y) = rev (rbl_plus False (rev (to_bl x)) (rev (to_bl y)))"
   3.241 -    for x y :: "'a word"
   3.242 -    by (simp add: rbl_word_plus[symmetric])
   3.243 -
   3.244 -  have mult_bit: "to_bl (of_bl [z] * y) = map ((\<and>) z) (to_bl y)"
   3.245 -    by (cases z) (simp cong: map_cong, simp add: map_replicate_const cong: map_cong)
   3.246 -
   3.247 -  have shiftl: "of_bl xs * 2 * y = (of_bl xs * y) << 1" for xs
   3.248 -    by (simp add: shiftl_t2n)
   3.249 -
   3.250 -  have zip_take_triv: "\<And>xs ys n. n = length ys \<Longrightarrow> zip (take n xs) ys = zip xs ys"
   3.251 -    by (rule nth_equalityI) simp_all
   3.252 -
   3.253 -  from Cons show ?case
   3.254 -    apply (simp add: trans [OF of_bl_append add.commute]
   3.255 -        rbl_mul_simps rbl_word_plus' distrib_right mult_bit shiftl rbl_shiftl)
   3.256 -    apply (simp add: takefill_alt word_size rev_map take_rbl_plus min_def)
   3.257 -    apply (simp add: rbl_plus_def zip_take_triv)
   3.258 -    done
   3.259 -qed
   3.260 -
   3.261 -lemma rbl_word_mul: "rev (to_bl (x * y)) = rbl_mul (rev (to_bl x)) (rev (to_bl y))"
   3.262 -  for x :: "'a::len word"
   3.263 -  using word_rbl_mul_induct[where xs="rev (to_bl x)" and y=y] by (simp add: word_size)
   3.264 -
   3.265 -text \<open>Breaking up inequalities into bitlist properties.\<close>
   3.266 -
   3.267 -definition
   3.268 -  "rev_bl_order F xs ys =
   3.269 -     (length xs = length ys \<and>
   3.270 -       ((xs = ys \<and> F)
   3.271 -          \<or> (\<exists>n < length xs. drop (Suc n) xs = drop (Suc n) ys
   3.272 -                   \<and> \<not> xs ! n \<and> ys ! n)))"
   3.273 -
   3.274 -lemma rev_bl_order_simps:
   3.275 -  "rev_bl_order F [] [] = F"
   3.276 -  "rev_bl_order F (x # xs) (y # ys) = rev_bl_order ((y \<and> \<not> x) \<or> ((y \<or> \<not> x) \<and> F)) xs ys"
   3.277 -   apply (simp_all add: rev_bl_order_def)
   3.278 -  apply (rule conj_cong[OF refl])
   3.279 -  apply (cases "xs = ys")
   3.280 -   apply (simp add: nth_Cons')
   3.281 -   apply blast
   3.282 -  apply (simp add: nth_Cons')
   3.283 -  apply safe
   3.284 -   apply (rule_tac x="n - 1" in exI)
   3.285 -   apply simp
   3.286 -  apply (rule_tac x="Suc n" in exI)
   3.287 -  apply simp
   3.288 -  done
   3.289 -
   3.290 -lemma rev_bl_order_rev_simp:
   3.291 -  "length xs = length ys \<Longrightarrow>
   3.292 -   rev_bl_order F (xs @ [x]) (ys @ [y]) = ((y \<and> \<not> x) \<or> ((y \<or> \<not> x) \<and> rev_bl_order F xs ys))"
   3.293 -  by (induct arbitrary: F rule: list_induct2) (auto simp: rev_bl_order_simps)
   3.294 -
   3.295 -lemma rev_bl_order_bl_to_bin:
   3.296 -  "length xs = length ys \<Longrightarrow>
   3.297 -    rev_bl_order True xs ys = (bl_to_bin (rev xs) \<le> bl_to_bin (rev ys)) \<and>
   3.298 -    rev_bl_order False xs ys = (bl_to_bin (rev xs) < bl_to_bin (rev ys))"
   3.299 -  apply (induct xs ys rule: list_induct2)
   3.300 -   apply (simp_all add: rev_bl_order_simps bl_to_bin_app_cat)
   3.301 -  apply (auto simp add: bl_to_bin_def Bit_B0 Bit_B1 add1_zle_eq Bit_def)
   3.302 -  done
   3.303 -
   3.304 -lemma word_le_rbl: "x \<le> y \<longleftrightarrow> rev_bl_order True (rev (to_bl x)) (rev (to_bl y))"
   3.305 -  for x y :: "'a::len0 word"
   3.306 -  by (simp add: rev_bl_order_bl_to_bin word_le_def)
   3.307 -
   3.308 -lemma word_less_rbl: "x < y \<longleftrightarrow> rev_bl_order False (rev (to_bl x)) (rev (to_bl y))"
   3.309 -  for x y :: "'a::len0 word"
   3.310 -  by (simp add: word_less_alt rev_bl_order_bl_to_bin)
   3.311 -
   3.312 -lemma word_sint_msb_eq: "sint x = uint x - (if msb x then 2 ^ size x else 0)"
   3.313 -  apply (cases "msb x")
   3.314 -   apply (rule word_sint.Abs_eqD[where 'a='a], simp_all)
   3.315 -    apply (simp add: word_size wi_hom_syms word_of_int_2p_len)
   3.316 -   apply (simp add: sints_num word_size)
   3.317 -   apply (rule conjI)
   3.318 -    apply (simp add: le_diff_eq')
   3.319 -    apply (rule order_trans[where y="2 ^ (len_of TYPE('a) - 1)"])
   3.320 -     apply (simp add: power_Suc[symmetric])
   3.321 -    apply (simp add: linorder_not_less[symmetric] mask_eq_iff[symmetric])
   3.322 -    apply (rule notI, drule word_eqD[where x="size x - 1"])
   3.323 -    apply (simp add: msb_nth word_ops_nth_size word_size)
   3.324 -   apply (simp add: order_less_le_trans[where y=0])
   3.325 -  apply (rule word_uint.Abs_eqD[where 'a='a], simp_all)
   3.326 -  apply (simp add: linorder_not_less uints_num word_msb_sint)
   3.327 -  apply (rule order_less_le_trans[OF sint_lt])
   3.328 -  apply simp
   3.329 -  done
   3.330 -
   3.331 -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)"
   3.332 -  apply (simp add: word_sle_def word_sint_msb_eq word_size word_le_def)
   3.333 -  apply safe
   3.334 -   apply (rule order_trans[OF _ uint_ge_0])
   3.335 -   apply (simp add: order_less_imp_le)
   3.336 -  apply (erule notE[OF leD])
   3.337 -  apply (rule order_less_le_trans[OF _ uint_ge_0])
   3.338 -  apply simp
   3.339 -  done
   3.340 -
   3.341 -lemma word_sless_msb_less: "x <s y \<longleftrightarrow> (msb y \<longrightarrow> msb x) \<and> ((msb x \<and> \<not> msb y) \<or> x < y)"
   3.342 -  by (auto simp add: word_sless_def word_sle_msb_le)
   3.343 -
   3.344 -definition "map_last f xs = (if xs = [] then [] else butlast xs @ [f (last xs)])"
   3.345 -
   3.346 -lemma map_last_simps:
   3.347 -  "map_last f [] = []"
   3.348 -  "map_last f [x] = [f x]"
   3.349 -  "map_last f (x # y # zs) = x # map_last f (y # zs)"
   3.350 -  by (simp_all add: map_last_def)
   3.351 -
   3.352 -lemma word_sle_rbl:
   3.353 -  "x <=s y \<longleftrightarrow> rev_bl_order True (map_last Not (rev (to_bl x))) (map_last Not (rev (to_bl y)))"
   3.354 -  using word_msb_alt[where w=x] word_msb_alt[where w=y]
   3.355 -  apply (simp add: word_sle_msb_le word_le_rbl)
   3.356 -  apply (subgoal_tac "length (to_bl x) = length (to_bl y)")
   3.357 -   apply (cases "to_bl x", simp)
   3.358 -   apply (cases "to_bl y", simp)
   3.359 -   apply (clarsimp simp: map_last_def rev_bl_order_rev_simp)
   3.360 -   apply auto
   3.361 -  done
   3.362 -
   3.363 -lemma word_sless_rbl:
   3.364 -  "x <s y \<longleftrightarrow> rev_bl_order False (map_last Not (rev (to_bl x))) (map_last Not (rev (to_bl y)))"
   3.365 -  using word_msb_alt[where w=x] word_msb_alt[where w=y]
   3.366 -  apply (simp add: word_sless_msb_less word_less_rbl)
   3.367 -  apply (subgoal_tac "length (to_bl x) = length (to_bl y)")
   3.368 -   apply (cases "to_bl x", simp)
   3.369 -   apply (cases "to_bl y", simp)
   3.370 -   apply (clarsimp simp: map_last_def rev_bl_order_rev_simp)
   3.371 -   apply auto
   3.372 -  done
   3.373 -
   3.374 -text \<open>Lemmas for unpacking \<^term>\<open>rev (to_bl n)\<close> for numerals n and also
   3.375 -  for irreducible values and expressions.\<close>
   3.376 -
   3.377 -lemma rev_bin_to_bl_simps:
   3.378 -  "rev (bin_to_bl 0 x) = []"
   3.379 -  "rev (bin_to_bl (Suc n) (numeral (num.Bit0 nm))) = False # rev (bin_to_bl n (numeral nm))"
   3.380 -  "rev (bin_to_bl (Suc n) (numeral (num.Bit1 nm))) = True # rev (bin_to_bl n (numeral nm))"
   3.381 -  "rev (bin_to_bl (Suc n) (numeral (num.One))) = True # replicate n False"
   3.382 -  "rev (bin_to_bl (Suc n) (- numeral (num.Bit0 nm))) = False # rev (bin_to_bl n (- numeral nm))"
   3.383 -  "rev (bin_to_bl (Suc n) (- numeral (num.Bit1 nm))) =
   3.384 -    True # rev (bin_to_bl n (- numeral (nm + num.One)))"
   3.385 -  "rev (bin_to_bl (Suc n) (- numeral (num.One))) = True # replicate n True"
   3.386 -  "rev (bin_to_bl (Suc n) (- numeral (num.Bit0 nm + num.One))) =
   3.387 -    True # rev (bin_to_bl n (- numeral (nm + num.One)))"
   3.388 -  "rev (bin_to_bl (Suc n) (- numeral (num.Bit1 nm + num.One))) =
   3.389 -    False # rev (bin_to_bl n (- numeral (nm + num.One)))"
   3.390 -  "rev (bin_to_bl (Suc n) (- numeral (num.One + num.One))) =
   3.391 -    False # rev (bin_to_bl n (- numeral num.One))"
   3.392 -  apply simp_all
   3.393 -  apply (simp_all only: bin_to_bl_aux_alt)
   3.394 -  apply (simp_all)
   3.395 -  apply (simp_all add: bin_to_bl_zero_aux bin_to_bl_minus1_aux)
   3.396 -  done
   3.397 -
   3.398 -lemma to_bl_upt: "to_bl x = rev (map ((!!) x) [0 ..< size x])"
   3.399 -  apply (rule nth_equalityI)
   3.400 -   apply (simp add: word_size)
   3.401 -  apply (auto simp: to_bl_nth word_size nth_rev)
   3.402 -  done
   3.403 -
   3.404 -lemma rev_to_bl_upt: "rev (to_bl x) = map ((!!) x) [0 ..< size x]"
   3.405 -  by (simp add: to_bl_upt)
   3.406 -
   3.407 -lemma upt_eq_list_intros:
   3.408 -  "j \<le> i \<Longrightarrow> [i ..< j] = []"
   3.409 -  "i = x \<Longrightarrow> x < j \<Longrightarrow> [x + 1 ..< j] = xs \<Longrightarrow> [i ..< j] = (x # xs)"
   3.410 -  by (simp_all add: upt_eq_Cons_conv)
   3.411 -
   3.412 -
   3.413 -subsection \<open>Tactic definition\<close>
   3.414 -
   3.415 -ML \<open>
   3.416 -structure Word_Bitwise_Tac =
   3.417 -struct
   3.418 -
   3.419 -val word_ss = simpset_of \<^theory_context>\<open>Word\<close>;
   3.420 -
   3.421 -fun mk_nat_clist ns =
   3.422 -  fold_rev (Thm.mk_binop \<^cterm>\<open>Cons :: nat \<Rightarrow> _\<close>)
   3.423 -    ns \<^cterm>\<open>[] :: nat list\<close>;
   3.424 -
   3.425 -fun upt_conv ctxt ct =
   3.426 -  case Thm.term_of ct of
   3.427 -    (\<^const>\<open>upt\<close> $ n $ m) =>
   3.428 -      let
   3.429 -        val (i, j) = apply2 (snd o HOLogic.dest_number) (n, m);
   3.430 -        val ns = map (Numeral.mk_cnumber \<^ctyp>\<open>nat\<close>) (i upto (j - 1))
   3.431 -          |> mk_nat_clist;
   3.432 -        val prop =
   3.433 -          Thm.mk_binop \<^cterm>\<open>(=) :: nat list \<Rightarrow> _\<close> ct ns
   3.434 -          |> Thm.apply \<^cterm>\<open>Trueprop\<close>;
   3.435 -      in
   3.436 -        try (fn () =>
   3.437 -          Goal.prove_internal ctxt [] prop
   3.438 -            (K (REPEAT_DETERM (resolve_tac ctxt @{thms upt_eq_list_intros} 1
   3.439 -                ORELSE simp_tac (put_simpset word_ss ctxt) 1))) |> mk_meta_eq) ()
   3.440 -      end
   3.441 -  | _ => NONE;
   3.442 -
   3.443 -val expand_upt_simproc =
   3.444 -  Simplifier.make_simproc \<^context> "expand_upt"
   3.445 -   {lhss = [\<^term>\<open>upt x y\<close>], proc = K upt_conv};
   3.446 -
   3.447 -fun word_len_simproc_fn ctxt ct =
   3.448 -  (case Thm.term_of ct of
   3.449 -    Const (\<^const_name>\<open>len_of\<close>, _) $ t =>
   3.450 -     (let
   3.451 -        val T = fastype_of t |> dest_Type |> snd |> the_single
   3.452 -        val n = Numeral.mk_cnumber \<^ctyp>\<open>nat\<close> (Word_Lib.dest_binT T);
   3.453 -        val prop =
   3.454 -          Thm.mk_binop \<^cterm>\<open>(=) :: nat \<Rightarrow> _\<close> ct n
   3.455 -          |> Thm.apply \<^cterm>\<open>Trueprop\<close>;
   3.456 -      in
   3.457 -        Goal.prove_internal ctxt [] prop (K (simp_tac (put_simpset word_ss ctxt) 1))
   3.458 -        |> mk_meta_eq |> SOME
   3.459 -      end handle TERM _ => NONE | TYPE _ => NONE)
   3.460 -  | _ => NONE);
   3.461 -
   3.462 -val word_len_simproc =
   3.463 -  Simplifier.make_simproc \<^context> "word_len"
   3.464 -   {lhss = [\<^term>\<open>len_of x\<close>], proc = K word_len_simproc_fn};
   3.465 -
   3.466 -(* convert 5 or nat 5 to Suc 4 when n_sucs = 1, Suc (Suc 4) when n_sucs = 2,
   3.467 -   or just 5 (discarding nat) when n_sucs = 0 *)
   3.468 -
   3.469 -fun nat_get_Suc_simproc_fn n_sucs ctxt ct =
   3.470 -  let
   3.471 -    val (f $ arg) = Thm.term_of ct;
   3.472 -    val n =
   3.473 -      (case arg of \<^term>\<open>nat\<close> $ n => n | n => n)
   3.474 -      |> HOLogic.dest_number |> snd;
   3.475 -    val (i, j) = if n > n_sucs then (n_sucs, n - n_sucs) else (n, 0);
   3.476 -    val arg' = funpow i HOLogic.mk_Suc (HOLogic.mk_number \<^typ>\<open>nat\<close> j);
   3.477 -    val _ = if arg = arg' then raise TERM ("", []) else ();
   3.478 -    fun propfn g =
   3.479 -      HOLogic.mk_eq (g arg, g arg')
   3.480 -      |> HOLogic.mk_Trueprop |> Thm.cterm_of ctxt;
   3.481 -    val eq1 =
   3.482 -      Goal.prove_internal ctxt [] (propfn I)
   3.483 -        (K (simp_tac (put_simpset word_ss ctxt) 1));
   3.484 -  in
   3.485 -    Goal.prove_internal ctxt [] (propfn (curry (op $) f))
   3.486 -      (K (simp_tac (put_simpset HOL_ss ctxt addsimps [eq1]) 1))
   3.487 -    |> mk_meta_eq |> SOME
   3.488 -  end handle TERM _ => NONE;
   3.489 -
   3.490 -fun nat_get_Suc_simproc n_sucs ts =
   3.491 -  Simplifier.make_simproc \<^context> "nat_get_Suc"
   3.492 -   {lhss = map (fn t => t $ \<^term>\<open>n :: nat\<close>) ts,
   3.493 -    proc = K (nat_get_Suc_simproc_fn n_sucs)};
   3.494 -
   3.495 -val no_split_ss =
   3.496 -  simpset_of (put_simpset HOL_ss \<^context>
   3.497 -    |> Splitter.del_split @{thm if_split});
   3.498 -
   3.499 -val expand_word_eq_sss =
   3.500 -  (simpset_of (put_simpset HOL_basic_ss \<^context> addsimps
   3.501 -       @{thms word_eq_rbl_eq word_le_rbl word_less_rbl word_sle_rbl word_sless_rbl}),
   3.502 -  map simpset_of [
   3.503 -   put_simpset no_split_ss \<^context> addsimps
   3.504 -    @{thms rbl_word_plus rbl_word_and rbl_word_or rbl_word_not
   3.505 -                                rbl_word_neg bl_word_sub rbl_word_xor
   3.506 -                                rbl_word_cat rbl_word_slice rbl_word_scast
   3.507 -                                rbl_word_ucast rbl_shiftl rbl_shiftr rbl_sshiftr
   3.508 -                                rbl_word_if},
   3.509 -   put_simpset no_split_ss \<^context> addsimps
   3.510 -    @{thms to_bl_numeral to_bl_neg_numeral to_bl_0 rbl_word_1},
   3.511 -   put_simpset no_split_ss \<^context> addsimps
   3.512 -    @{thms rev_rev_ident rev_replicate rev_map to_bl_upt word_size}
   3.513 -          addsimprocs [word_len_simproc],
   3.514 -   put_simpset no_split_ss \<^context> addsimps
   3.515 -    @{thms list.simps split_conv replicate.simps list.map
   3.516 -                                zip_Cons_Cons zip_Nil drop_Suc_Cons drop_0 drop_Nil
   3.517 -                                foldr.simps map2_Cons map2_Nil takefill_Suc_Cons
   3.518 -                                takefill_Suc_Nil takefill.Z rbl_succ2_simps
   3.519 -                                rbl_plus_simps rev_bin_to_bl_simps append.simps
   3.520 -                                takefill_last_simps drop_nonempty_simps
   3.521 -                                rev_bl_order_simps}
   3.522 -          addsimprocs [expand_upt_simproc,
   3.523 -                       nat_get_Suc_simproc 4
   3.524 -                         [\<^term>\<open>replicate\<close>, \<^term>\<open>takefill x\<close>,
   3.525 -                          \<^term>\<open>drop\<close>, \<^term>\<open>bin_to_bl\<close>,
   3.526 -                          \<^term>\<open>takefill_last x\<close>,
   3.527 -                          \<^term>\<open>drop_nonempty x\<close>]],
   3.528 -    put_simpset no_split_ss \<^context> addsimps @{thms xor3_simps carry_simps if_bool_simps}
   3.529 -  ])
   3.530 -
   3.531 -fun tac ctxt =
   3.532 -  let
   3.533 -    val (ss, sss) = expand_word_eq_sss;
   3.534 -  in
   3.535 -    foldr1 (op THEN_ALL_NEW)
   3.536 -      ((CHANGED o safe_full_simp_tac (put_simpset ss ctxt)) ::
   3.537 -        map (fn ss => safe_full_simp_tac (put_simpset ss ctxt)) sss)
   3.538 -  end;
   3.539 -
   3.540 -end
   3.541 -\<close>
   3.542 -
   3.543 -method_setup word_bitwise =
   3.544 -  \<open>Scan.succeed (fn ctxt => Method.SIMPLE_METHOD (Word_Bitwise_Tac.tac ctxt 1))\<close>
   3.545 -  "decomposer for word equalities and inequalities into bit propositions"
   3.546 -
   3.547 -end
     4.1 --- a/src/HOL/Word/WordExamples.thy	Tue Apr 16 19:50:09 2019 +0000
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,207 +0,0 @@
     4.4 -(*  Title:      HOL/Word/WordExamples.thy
     4.5 -    Authors:    Gerwin Klein and Thomas Sewell, NICTA
     4.6 -
     4.7 -Examples demonstrating and testing various word operations.
     4.8 -*)
     4.9 -
    4.10 -section "Examples of word operations"
    4.11 -
    4.12 -theory WordExamples
    4.13 -  imports WordBitwise
    4.14 -begin
    4.15 -
    4.16 -type_synonym word32 = "32 word"
    4.17 -type_synonym word8 = "8 word"
    4.18 -type_synonym byte = word8
    4.19 -
    4.20 -text "modulus"
    4.21 -
    4.22 -lemma "(27 :: 4 word) = -5" by simp
    4.23 -
    4.24 -lemma "(27 :: 4 word) = 11" by simp
    4.25 -
    4.26 -lemma "27 \<noteq> (11 :: 6 word)" by simp
    4.27 -
    4.28 -text "signed"
    4.29 -
    4.30 -lemma "(127 :: 6 word) = -1" by simp
    4.31 -
    4.32 -text "number ring simps"
    4.33 -
    4.34 -lemma
    4.35 -  "27 + 11 = (38::'a::len word)"
    4.36 -  "27 + 11 = (6::5 word)"
    4.37 -  "7 * 3 = (21::'a::len word)"
    4.38 -  "11 - 27 = (-16::'a::len word)"
    4.39 -  "- (- 11) = (11::'a::len word)"
    4.40 -  "-40 + 1 = (-39::'a::len word)"
    4.41 -  by simp_all
    4.42 -
    4.43 -lemma "word_pred 2 = 1" by simp
    4.44 -
    4.45 -lemma "word_succ (- 3) = -2" by simp
    4.46 -
    4.47 -lemma "23 < (27::8 word)" by simp
    4.48 -lemma "23 \<le> (27::8 word)" by simp
    4.49 -lemma "\<not> 23 < (27::2 word)" by simp
    4.50 -lemma "0 < (4::3 word)" by simp
    4.51 -lemma "1 < (4::3 word)" by simp
    4.52 -lemma "0 < (1::3 word)" by simp
    4.53 -
    4.54 -text "ring operations"
    4.55 -
    4.56 -lemma "a + 2 * b + c - b = (b + c) + (a :: 32 word)" by simp
    4.57 -
    4.58 -text "casting"
    4.59 -
    4.60 -lemma "uint (234567 :: 10 word) = 71" by simp
    4.61 -lemma "uint (-234567 :: 10 word) = 953" by simp
    4.62 -lemma "sint (234567 :: 10 word) = 71" by simp
    4.63 -lemma "sint (-234567 :: 10 word) = -71" by simp
    4.64 -lemma "uint (1 :: 10 word) = 1" by simp
    4.65 -
    4.66 -lemma "unat (-234567 :: 10 word) = 953" by simp
    4.67 -lemma "unat (1 :: 10 word) = 1" by simp
    4.68 -
    4.69 -lemma "ucast (0b1010 :: 4 word) = (0b10 :: 2 word)" by simp
    4.70 -lemma "ucast (0b1010 :: 4 word) = (0b1010 :: 10 word)" by simp
    4.71 -lemma "scast (0b1010 :: 4 word) = (0b111010 :: 6 word)" by simp
    4.72 -lemma "ucast (1 :: 4 word) = (1 :: 2 word)" by simp
    4.73 -
    4.74 -text "reducing goals to nat or int and arith:"
    4.75 -lemma "i < x \<Longrightarrow> i < i + 1" for i x :: "'a::len word"
    4.76 -  by unat_arith
    4.77 -lemma "i < x \<Longrightarrow> i < i + 1" for i x :: "'a::len word"
    4.78 -  by unat_arith
    4.79 -
    4.80 -text "bool lists"
    4.81 -
    4.82 -lemma "of_bl [True, False, True, True] = (0b1011::'a::len word)" by simp
    4.83 -
    4.84 -lemma "to_bl (0b110::4 word) = [False, True, True, False]" by simp
    4.85 -
    4.86 -text "this is not exactly fast, but bearable"
    4.87 -lemma "of_bl (replicate 32 True) = (0xFFFFFFFF::32 word)" by simp
    4.88 -
    4.89 -text "this works only for replicate n True"
    4.90 -lemma "of_bl (replicate 32 True) = (0xFFFFFFFF::32 word)"
    4.91 -  by (unfold mask_bl [symmetric]) (simp add: mask_def)
    4.92 -
    4.93 -
    4.94 -text "bit operations"
    4.95 -
    4.96 -lemma "0b110 AND 0b101 = (0b100 :: 32 word)" by simp
    4.97 -lemma "0b110 OR 0b011 = (0b111 :: 8 word)" by simp
    4.98 -lemma "0xF0 XOR 0xFF = (0x0F :: byte)" by simp
    4.99 -lemma "NOT (0xF0 :: 16 word) = 0xFF0F" by simp
   4.100 -lemma "0 AND 5 = (0 :: byte)" by simp
   4.101 -lemma "1 AND 1 = (1 :: byte)" by simp
   4.102 -lemma "1 AND 0 = (0 :: byte)" by simp
   4.103 -lemma "1 AND 5 = (1 :: byte)" by simp
   4.104 -lemma "1 OR 6 = (7 :: byte)" by simp
   4.105 -lemma "1 OR 1 = (1 :: byte)" by simp
   4.106 -lemma "1 XOR 7 = (6 :: byte)" by simp
   4.107 -lemma "1 XOR 1 = (0 :: byte)" by simp
   4.108 -lemma "NOT 1 = (254 :: byte)" by simp
   4.109 -lemma "NOT 0 = (255 :: byte)" apply simp oops
   4.110 -(* FIXME: "NOT 0" rewrites to "max_word" instead of "-1" *)
   4.111 -
   4.112 -lemma "(-1 :: 32 word) = 0xFFFFFFFF" by simp
   4.113 -
   4.114 -lemma "(0b0010 :: 4 word) !! 1" by simp
   4.115 -lemma "\<not> (0b0010 :: 4 word) !! 0" by simp
   4.116 -lemma "\<not> (0b1000 :: 3 word) !! 4" by simp
   4.117 -lemma "\<not> (1 :: 3 word) !! 2" by simp
   4.118 -
   4.119 -lemma "(0b11000 :: 10 word) !! n = (n = 4 \<or> n = 3)"
   4.120 -  by (auto simp add: bin_nth_Bit0 bin_nth_Bit1)
   4.121 -
   4.122 -lemma "set_bit 55 7 True = (183::'a::len0 word)" by simp
   4.123 -lemma "set_bit 0b0010 7 True = (0b10000010::'a::len0 word)" by simp
   4.124 -lemma "set_bit 0b0010 1 False = (0::'a::len0 word)" by simp
   4.125 -lemma "set_bit 1 3 True = (0b1001::'a::len0 word)" by simp
   4.126 -lemma "set_bit 1 0 False = (0::'a::len0 word)" by simp
   4.127 -lemma "set_bit 0 3 True = (0b1000::'a::len0 word)" by simp
   4.128 -lemma "set_bit 0 3 False = (0::'a::len0 word)" by simp
   4.129 -
   4.130 -lemma "lsb (0b0101::'a::len word)" by simp
   4.131 -lemma "\<not> lsb (0b1000::'a::len word)" by simp
   4.132 -lemma "lsb (1::'a::len word)" by simp
   4.133 -lemma "\<not> lsb (0::'a::len word)" by simp
   4.134 -
   4.135 -lemma "\<not> msb (0b0101::4 word)" by simp
   4.136 -lemma   "msb (0b1000::4 word)" by simp
   4.137 -lemma "\<not> msb (1::4 word)" by simp
   4.138 -lemma "\<not> msb (0::4 word)" by simp
   4.139 -
   4.140 -lemma "word_cat (27::4 word) (27::8 word) = (2843::'a::len word)" by simp
   4.141 -lemma "word_cat (0b0011::4 word) (0b1111::6word) = (0b0011001111 :: 10 word)"
   4.142 -  by simp
   4.143 -
   4.144 -lemma "0b1011 << 2 = (0b101100::'a::len0 word)" by simp
   4.145 -lemma "0b1011 >> 2 = (0b10::8 word)" by simp
   4.146 -lemma "0b1011 >>> 2 = (0b10::8 word)" by simp
   4.147 -lemma "1 << 2 = (0b100::'a::len0 word)" apply simp? oops
   4.148 -
   4.149 -lemma "slice 3 (0b101111::6 word) = (0b101::3 word)" by simp
   4.150 -lemma "slice 3 (1::6 word) = (0::3 word)" apply simp? oops
   4.151 -
   4.152 -lemma "word_rotr 2 0b0110 = (0b1001::4 word)" by simp
   4.153 -lemma "word_rotl 1 0b1110 = (0b1101::4 word)" by simp
   4.154 -lemma "word_roti 2 0b1110 = (0b1011::4 word)" by simp
   4.155 -lemma "word_roti (- 2) 0b0110 = (0b1001::4 word)" by simp
   4.156 -lemma "word_rotr 2 0 = (0::4 word)" by simp
   4.157 -lemma "word_rotr 2 1 = (0b0100::4 word)" apply simp? oops
   4.158 -lemma "word_rotl 2 1 = (0b0100::4 word)" apply simp? oops
   4.159 -lemma "word_roti (- 2) 1 = (0b0100::4 word)" apply simp? oops
   4.160 -
   4.161 -lemma "(x AND 0xff00) OR (x AND 0x00ff) = (x::16 word)"
   4.162 -proof -
   4.163 -  have "(x AND 0xff00) OR (x AND 0x00ff) = x AND (0xff00 OR 0x00ff)"
   4.164 -    by (simp only: word_ao_dist2)
   4.165 -  also have "0xff00 OR 0x00ff = (-1::16 word)"
   4.166 -    by simp
   4.167 -  also have "x AND -1 = x"
   4.168 -    by simp
   4.169 -  finally show ?thesis .
   4.170 -qed
   4.171 -
   4.172 -text "alternative proof using bitwise expansion"
   4.173 -
   4.174 -lemma "(x AND 0xff00) OR (x AND 0x00ff) = (x::16 word)"
   4.175 -  by word_bitwise
   4.176 -
   4.177 -text "more proofs using bitwise expansion"
   4.178 -
   4.179 -lemma "(x AND NOT 3) >> 4 << 2 = ((x >> 2) AND NOT 3)"
   4.180 -  for x :: "10 word"
   4.181 -  by word_bitwise
   4.182 -
   4.183 -lemma "((x AND -8) >> 3) AND 7 = (x AND 56) >> 3"
   4.184 -  for x :: "12 word"
   4.185 -  by word_bitwise
   4.186 -
   4.187 -text "some problems require further reasoning after bit expansion"
   4.188 -
   4.189 -lemma "x \<le> 42 \<Longrightarrow> x \<le> 89"
   4.190 -  for x :: "8 word"
   4.191 -  apply word_bitwise
   4.192 -  apply blast
   4.193 -  done
   4.194 -
   4.195 -lemma "(x AND 1023) = 0 \<Longrightarrow> x \<le> -1024"
   4.196 -  for x :: word32
   4.197 -  apply word_bitwise
   4.198 -  apply clarsimp
   4.199 -  done
   4.200 -
   4.201 -text "operations like shifts by non-numerals will expose some internal list
   4.202 - representations but may still be easy to solve"
   4.203 -
   4.204 -lemma shiftr_overflow: "32 \<le> a \<Longrightarrow> b >> a = 0"
   4.205 -  for b :: word32
   4.206 -  apply word_bitwise
   4.207 -  apply simp
   4.208 -  done
   4.209 -
   4.210 -end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Word/Word_Bitwise.thy	Tue Apr 16 19:50:18 2019 +0000
     5.3 @@ -0,0 +1,544 @@
     5.4 +(*  Title:      HOL/Word/Word_Bitwise.thy
     5.5 +    Authors:    Thomas Sewell, NICTA and Sascha Boehme, TU Muenchen
     5.6 +*)
     5.7 +
     5.8 +theory Word_Bitwise
     5.9 +  imports Word
    5.10 +begin
    5.11 +
    5.12 +text \<open>Helper constants used in defining addition\<close>
    5.13 +
    5.14 +definition xor3 :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool"
    5.15 +  where "xor3 a b c = (a = (b = c))"
    5.16 +
    5.17 +definition carry :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool"
    5.18 +  where "carry a b c = ((a \<and> (b \<or> c)) \<or> (b \<and> c))"
    5.19 +
    5.20 +lemma carry_simps:
    5.21 +  "carry True a b = (a \<or> b)"
    5.22 +  "carry a True b = (a \<or> b)"
    5.23 +  "carry a b True = (a \<or> b)"
    5.24 +  "carry False a b = (a \<and> b)"
    5.25 +  "carry a False b = (a \<and> b)"
    5.26 +  "carry a b False = (a \<and> b)"
    5.27 +  by (auto simp add: carry_def)
    5.28 +
    5.29 +lemma xor3_simps:
    5.30 +  "xor3 True a b = (a = b)"
    5.31 +  "xor3 a True b = (a = b)"
    5.32 +  "xor3 a b True = (a = b)"
    5.33 +  "xor3 False a b = (a \<noteq> b)"
    5.34 +  "xor3 a False b = (a \<noteq> b)"
    5.35 +  "xor3 a b False = (a \<noteq> b)"
    5.36 +  by (simp_all add: xor3_def)
    5.37 +
    5.38 +text \<open>Breaking up word equalities into equalities on their
    5.39 +  bit lists. Equalities are generated and manipulated in the
    5.40 +  reverse order to \<^const>\<open>to_bl\<close>.\<close>
    5.41 +
    5.42 +lemma word_eq_rbl_eq: "x = y \<longleftrightarrow> rev (to_bl x) = rev (to_bl y)"
    5.43 +  by simp
    5.44 +
    5.45 +lemma rbl_word_or: "rev (to_bl (x OR y)) = map2 (\<or>) (rev (to_bl x)) (rev (to_bl y))"
    5.46 +  by (simp add: map2_def zip_rev bl_word_or rev_map)
    5.47 +
    5.48 +lemma rbl_word_and: "rev (to_bl (x AND y)) = map2 (\<and>) (rev (to_bl x)) (rev (to_bl y))"
    5.49 +  by (simp add: map2_def zip_rev bl_word_and rev_map)
    5.50 +
    5.51 +lemma rbl_word_xor: "rev (to_bl (x XOR y)) = map2 (\<noteq>) (rev (to_bl x)) (rev (to_bl y))"
    5.52 +  by (simp add: map2_def zip_rev bl_word_xor rev_map)
    5.53 +
    5.54 +lemma rbl_word_not: "rev (to_bl (NOT x)) = map Not (rev (to_bl x))"
    5.55 +  by (simp add: bl_word_not rev_map)
    5.56 +
    5.57 +lemma bl_word_sub: "to_bl (x - y) = to_bl (x + (- y))"
    5.58 +  by simp
    5.59 +
    5.60 +lemma rbl_word_1: "rev (to_bl (1 :: 'a::len0 word)) = takefill False (len_of TYPE('a)) [True]"
    5.61 +  apply (rule_tac s="rev (to_bl (word_succ (0 :: 'a word)))" in trans)
    5.62 +   apply simp
    5.63 +  apply (simp only: rtb_rbl_ariths(1)[OF refl])
    5.64 +  apply simp
    5.65 +  apply (case_tac "len_of TYPE('a)")
    5.66 +   apply simp
    5.67 +  apply (simp add: takefill_alt)
    5.68 +  done
    5.69 +
    5.70 +lemma rbl_word_if: "rev (to_bl (if P then x else y)) = map2 (If P) (rev (to_bl x)) (rev (to_bl y))"
    5.71 +  by (simp add: map2_def split_def)
    5.72 +
    5.73 +lemma rbl_add_carry_Cons:
    5.74 +  "(if car then rbl_succ else id) (rbl_add (x # xs) (y # ys)) =
    5.75 +    xor3 x y car # (if carry x y car then rbl_succ else id) (rbl_add xs ys)"
    5.76 +  by (simp add: carry_def xor3_def)
    5.77 +
    5.78 +lemma rbl_add_suc_carry_fold:
    5.79 +  "length xs = length ys \<Longrightarrow>
    5.80 +    \<forall>car. (if car then rbl_succ else id) (rbl_add xs ys) =
    5.81 +      (foldr (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car)) (zip xs ys) (\<lambda>_. [])) car"
    5.82 +  apply (erule list_induct2)
    5.83 +   apply simp
    5.84 +  apply (simp only: rbl_add_carry_Cons)
    5.85 +  apply simp
    5.86 +  done
    5.87 +
    5.88 +lemma to_bl_plus_carry:
    5.89 +  "to_bl (x + y) =
    5.90 +    rev (foldr (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car))
    5.91 +      (rev (zip (to_bl x) (to_bl y))) (\<lambda>_. []) False)"
    5.92 +  using rbl_add_suc_carry_fold[where xs="rev (to_bl x)" and ys="rev (to_bl y)"]
    5.93 +  apply (simp add: word_add_rbl[OF refl refl])
    5.94 +  apply (drule_tac x=False in spec)
    5.95 +  apply (simp add: zip_rev)
    5.96 +  done
    5.97 +
    5.98 +definition "rbl_plus cin xs ys =
    5.99 +  foldr (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car)) (zip xs ys) (\<lambda>_. []) cin"
   5.100 +
   5.101 +lemma rbl_plus_simps:
   5.102 +  "rbl_plus cin (x # xs) (y # ys) = xor3 x y cin # rbl_plus (carry x y cin) xs ys"
   5.103 +  "rbl_plus cin [] ys = []"
   5.104 +  "rbl_plus cin xs [] = []"
   5.105 +  by (simp_all add: rbl_plus_def)
   5.106 +
   5.107 +lemma rbl_word_plus: "rev (to_bl (x + y)) = rbl_plus False (rev (to_bl x)) (rev (to_bl y))"
   5.108 +  by (simp add: rbl_plus_def to_bl_plus_carry zip_rev)
   5.109 +
   5.110 +definition "rbl_succ2 b xs = (if b then rbl_succ xs else xs)"
   5.111 +
   5.112 +lemma rbl_succ2_simps:
   5.113 +  "rbl_succ2 b [] = []"
   5.114 +  "rbl_succ2 b (x # xs) = (b \<noteq> x) # rbl_succ2 (x \<and> b) xs"
   5.115 +  by (simp_all add: rbl_succ2_def)
   5.116 +
   5.117 +lemma twos_complement: "- x = word_succ (NOT x)"
   5.118 +  using arg_cong[OF word_add_not[where x=x], where f="\<lambda>a. a - x + 1"]
   5.119 +  by (simp add: word_succ_p1 word_sp_01[unfolded word_succ_p1] del: word_add_not)
   5.120 +
   5.121 +lemma rbl_word_neg: "rev (to_bl (- x)) = rbl_succ2 True (map Not (rev (to_bl x)))"
   5.122 +  by (simp add: twos_complement word_succ_rbl[OF refl] bl_word_not rev_map rbl_succ2_def)
   5.123 +
   5.124 +lemma rbl_word_cat:
   5.125 +  "rev (to_bl (word_cat x y :: 'a::len0 word)) =
   5.126 +    takefill False (len_of TYPE('a)) (rev (to_bl y) @ rev (to_bl x))"
   5.127 +  by (simp add: word_cat_bl word_rev_tf)
   5.128 +
   5.129 +lemma rbl_word_slice:
   5.130 +  "rev (to_bl (slice n w :: 'a::len0 word)) =
   5.131 +    takefill False (len_of TYPE('a)) (drop n (rev (to_bl w)))"
   5.132 +  apply (simp add: slice_take word_rev_tf rev_take)
   5.133 +  apply (cases "n < len_of TYPE('b)", simp_all)
   5.134 +  done
   5.135 +
   5.136 +lemma rbl_word_ucast:
   5.137 +  "rev (to_bl (ucast x :: 'a::len0 word)) = takefill False (len_of TYPE('a)) (rev (to_bl x))"
   5.138 +  apply (simp add: to_bl_ucast takefill_alt)
   5.139 +  apply (simp add: rev_drop)
   5.140 +  apply (cases "len_of TYPE('a) < len_of TYPE('b)")
   5.141 +   apply simp_all
   5.142 +  done
   5.143 +
   5.144 +lemma rbl_shiftl:
   5.145 +  "rev (to_bl (w << n)) = takefill False (size w) (replicate n False @ rev (to_bl w))"
   5.146 +  by (simp add: bl_shiftl takefill_alt word_size rev_drop)
   5.147 +
   5.148 +lemma rbl_shiftr:
   5.149 +  "rev (to_bl (w >> n)) = takefill False (size w) (drop n (rev (to_bl w)))"
   5.150 +  by (simp add: shiftr_slice rbl_word_slice word_size)
   5.151 +
   5.152 +definition "drop_nonempty v n xs = (if n < length xs then drop n xs else [last (v # xs)])"
   5.153 +
   5.154 +lemma drop_nonempty_simps:
   5.155 +  "drop_nonempty v (Suc n) (x # xs) = drop_nonempty x n xs"
   5.156 +  "drop_nonempty v 0 (x # xs) = (x # xs)"
   5.157 +  "drop_nonempty v n [] = [v]"
   5.158 +  by (simp_all add: drop_nonempty_def)
   5.159 +
   5.160 +definition "takefill_last x n xs = takefill (last (x # xs)) n xs"
   5.161 +
   5.162 +lemma takefill_last_simps:
   5.163 +  "takefill_last z (Suc n) (x # xs) = x # takefill_last x n xs"
   5.164 +  "takefill_last z 0 xs = []"
   5.165 +  "takefill_last z n [] = replicate n z"
   5.166 +  by (simp_all add: takefill_last_def) (simp_all add: takefill_alt)
   5.167 +
   5.168 +lemma rbl_sshiftr:
   5.169 +  "rev (to_bl (w >>> n)) = takefill_last False (size w) (drop_nonempty False n (rev (to_bl w)))"
   5.170 +  apply (cases "n < size w")
   5.171 +   apply (simp add: bl_sshiftr takefill_last_def word_size
   5.172 +      takefill_alt rev_take last_rev
   5.173 +      drop_nonempty_def)
   5.174 +  apply (subgoal_tac "(w >>> n) = of_bl (replicate (size w) (msb w))")
   5.175 +   apply (simp add: word_size takefill_last_def takefill_alt
   5.176 +      last_rev word_msb_alt word_rev_tf
   5.177 +      drop_nonempty_def take_Cons')
   5.178 +   apply (case_tac "len_of TYPE('a)", simp_all)
   5.179 +  apply (rule word_eqI)
   5.180 +  apply (simp add: nth_sshiftr word_size test_bit_of_bl
   5.181 +      msb_nth)
   5.182 +  done
   5.183 +
   5.184 +lemma nth_word_of_int:
   5.185 +  "(word_of_int x :: 'a::len0 word) !! n = (n < len_of TYPE('a) \<and> bin_nth x n)"
   5.186 +  apply (simp add: test_bit_bl word_size to_bl_of_bin)
   5.187 +  apply (subst conj_cong[OF refl], erule bin_nth_bl)
   5.188 +  apply auto
   5.189 +  done
   5.190 +
   5.191 +lemma nth_scast:
   5.192 +  "(scast (x :: 'a::len word) :: 'b::len word) !! n =
   5.193 +    (n < len_of TYPE('b) \<and>
   5.194 +    (if n < len_of TYPE('a) - 1 then x !! n
   5.195 +     else x !! (len_of TYPE('a) - 1)))"
   5.196 +  by (simp add: scast_def nth_sint)
   5.197 +
   5.198 +lemma rbl_word_scast:
   5.199 +  "rev (to_bl (scast x :: 'a::len word)) = takefill_last False (len_of TYPE('a)) (rev (to_bl x))"
   5.200 +  apply (rule nth_equalityI)
   5.201 +   apply (simp add: word_size takefill_last_def)
   5.202 +  apply (clarsimp simp: nth_scast takefill_last_def
   5.203 +      nth_takefill word_size nth_rev to_bl_nth)
   5.204 +  apply (cases "len_of TYPE('b)")
   5.205 +   apply simp
   5.206 +  apply (clarsimp simp: less_Suc_eq_le linorder_not_less
   5.207 +      last_rev word_msb_alt[symmetric]
   5.208 +      msb_nth)
   5.209 +  done
   5.210 +
   5.211 +definition rbl_mul :: "bool list \<Rightarrow> bool list \<Rightarrow> bool list"
   5.212 +  where "rbl_mul xs ys = foldr (\<lambda>x sm. rbl_plus False (map ((\<and>) x) ys) (False # sm)) xs []"
   5.213 +
   5.214 +lemma rbl_mul_simps:
   5.215 +  "rbl_mul (x # xs) ys = rbl_plus False (map ((\<and>) x) ys) (False # rbl_mul xs ys)"
   5.216 +  "rbl_mul [] ys = []"
   5.217 +  by (simp_all add: rbl_mul_def)
   5.218 +
   5.219 +lemma takefill_le2: "length xs \<le> n \<Longrightarrow> takefill x m (takefill x n xs) = takefill x m xs"
   5.220 +  by (simp add: takefill_alt replicate_add[symmetric])
   5.221 +
   5.222 +lemma take_rbl_plus: "\<forall>n b. take n (rbl_plus b xs ys) = rbl_plus b (take n xs) (take n ys)"
   5.223 +  apply (simp add: rbl_plus_def take_zip[symmetric])
   5.224 +  apply (rule_tac list="zip xs ys" in list.induct)
   5.225 +   apply simp
   5.226 +  apply (clarsimp simp: split_def)
   5.227 +  apply (case_tac n, simp_all)
   5.228 +  done
   5.229 +
   5.230 +lemma word_rbl_mul_induct:
   5.231 +  "length xs \<le> size y \<Longrightarrow>
   5.232 +    rbl_mul xs (rev (to_bl y)) = take (length xs) (rev (to_bl (of_bl (rev xs) * y)))"
   5.233 +  for y :: "'a::len word"
   5.234 +proof (induct xs)
   5.235 +  case Nil
   5.236 +  show ?case by (simp add: rbl_mul_simps)
   5.237 +next
   5.238 +  case (Cons z zs)
   5.239 +
   5.240 +  have rbl_word_plus': "to_bl (x + y) = rev (rbl_plus False (rev (to_bl x)) (rev (to_bl y)))"
   5.241 +    for x y :: "'a word"
   5.242 +    by (simp add: rbl_word_plus[symmetric])
   5.243 +
   5.244 +  have mult_bit: "to_bl (of_bl [z] * y) = map ((\<and>) z) (to_bl y)"
   5.245 +    by (cases z) (simp cong: map_cong, simp add: map_replicate_const cong: map_cong)
   5.246 +
   5.247 +  have shiftl: "of_bl xs * 2 * y = (of_bl xs * y) << 1" for xs
   5.248 +    by (simp add: shiftl_t2n)
   5.249 +
   5.250 +  have zip_take_triv: "\<And>xs ys n. n = length ys \<Longrightarrow> zip (take n xs) ys = zip xs ys"
   5.251 +    by (rule nth_equalityI) simp_all
   5.252 +
   5.253 +  from Cons show ?case
   5.254 +    apply (simp add: trans [OF of_bl_append add.commute]
   5.255 +        rbl_mul_simps rbl_word_plus' distrib_right mult_bit shiftl rbl_shiftl)
   5.256 +    apply (simp add: takefill_alt word_size rev_map take_rbl_plus min_def)
   5.257 +    apply (simp add: rbl_plus_def zip_take_triv)
   5.258 +    done
   5.259 +qed
   5.260 +
   5.261 +lemma rbl_word_mul: "rev (to_bl (x * y)) = rbl_mul (rev (to_bl x)) (rev (to_bl y))"
   5.262 +  for x :: "'a::len word"
   5.263 +  using word_rbl_mul_induct[where xs="rev (to_bl x)" and y=y] by (simp add: word_size)
   5.264 +
   5.265 +text \<open>Breaking up inequalities into bitlist properties.\<close>
   5.266 +
   5.267 +definition
   5.268 +  "rev_bl_order F xs ys =
   5.269 +     (length xs = length ys \<and>
   5.270 +       ((xs = ys \<and> F)
   5.271 +          \<or> (\<exists>n < length xs. drop (Suc n) xs = drop (Suc n) ys
   5.272 +                   \<and> \<not> xs ! n \<and> ys ! n)))"
   5.273 +
   5.274 +lemma rev_bl_order_simps:
   5.275 +  "rev_bl_order F [] [] = F"
   5.276 +  "rev_bl_order F (x # xs) (y # ys) = rev_bl_order ((y \<and> \<not> x) \<or> ((y \<or> \<not> x) \<and> F)) xs ys"
   5.277 +   apply (simp_all add: rev_bl_order_def)
   5.278 +  apply (rule conj_cong[OF refl])
   5.279 +  apply (cases "xs = ys")
   5.280 +   apply (simp add: nth_Cons')
   5.281 +   apply blast
   5.282 +  apply (simp add: nth_Cons')
   5.283 +  apply safe
   5.284 +   apply (rule_tac x="n - 1" in exI)
   5.285 +   apply simp
   5.286 +  apply (rule_tac x="Suc n" in exI)
   5.287 +  apply simp
   5.288 +  done
   5.289 +
   5.290 +lemma rev_bl_order_rev_simp:
   5.291 +  "length xs = length ys \<Longrightarrow>
   5.292 +   rev_bl_order F (xs @ [x]) (ys @ [y]) = ((y \<and> \<not> x) \<or> ((y \<or> \<not> x) \<and> rev_bl_order F xs ys))"
   5.293 +  by (induct arbitrary: F rule: list_induct2) (auto simp: rev_bl_order_simps)
   5.294 +
   5.295 +lemma rev_bl_order_bl_to_bin:
   5.296 +  "length xs = length ys \<Longrightarrow>
   5.297 +    rev_bl_order True xs ys = (bl_to_bin (rev xs) \<le> bl_to_bin (rev ys)) \<and>
   5.298 +    rev_bl_order False xs ys = (bl_to_bin (rev xs) < bl_to_bin (rev ys))"
   5.299 +  apply (induct xs ys rule: list_induct2)
   5.300 +   apply (simp_all add: rev_bl_order_simps bl_to_bin_app_cat)
   5.301 +  apply (auto simp add: bl_to_bin_def Bit_B0 Bit_B1 add1_zle_eq Bit_def)
   5.302 +  done
   5.303 +
   5.304 +lemma word_le_rbl: "x \<le> y \<longleftrightarrow> rev_bl_order True (rev (to_bl x)) (rev (to_bl y))"
   5.305 +  for x y :: "'a::len0 word"
   5.306 +  by (simp add: rev_bl_order_bl_to_bin word_le_def)
   5.307 +
   5.308 +lemma word_less_rbl: "x < y \<longleftrightarrow> rev_bl_order False (rev (to_bl x)) (rev (to_bl y))"
   5.309 +  for x y :: "'a::len0 word"
   5.310 +  by (simp add: word_less_alt rev_bl_order_bl_to_bin)
   5.311 +
   5.312 +lemma word_sint_msb_eq: "sint x = uint x - (if msb x then 2 ^ size x else 0)"
   5.313 +  apply (cases "msb x")
   5.314 +   apply (rule word_sint.Abs_eqD[where 'a='a], simp_all)
   5.315 +    apply (simp add: word_size wi_hom_syms word_of_int_2p_len)
   5.316 +   apply (simp add: sints_num word_size)
   5.317 +   apply (rule conjI)
   5.318 +    apply (simp add: le_diff_eq')
   5.319 +    apply (rule order_trans[where y="2 ^ (len_of TYPE('a) - 1)"])
   5.320 +     apply (simp add: power_Suc[symmetric])
   5.321 +    apply (simp add: linorder_not_less[symmetric] mask_eq_iff[symmetric])
   5.322 +    apply (rule notI, drule word_eqD[where x="size x - 1"])
   5.323 +    apply (simp add: msb_nth word_ops_nth_size word_size)
   5.324 +   apply (simp add: order_less_le_trans[where y=0])
   5.325 +  apply (rule word_uint.Abs_eqD[where 'a='a], simp_all)
   5.326 +  apply (simp add: linorder_not_less uints_num word_msb_sint)
   5.327 +  apply (rule order_less_le_trans[OF sint_lt])
   5.328 +  apply simp
   5.329 +  done
   5.330 +
   5.331 +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)"
   5.332 +  apply (simp add: word_sle_def word_sint_msb_eq word_size word_le_def)
   5.333 +  apply safe
   5.334 +   apply (rule order_trans[OF _ uint_ge_0])
   5.335 +   apply (simp add: order_less_imp_le)
   5.336 +  apply (erule notE[OF leD])
   5.337 +  apply (rule order_less_le_trans[OF _ uint_ge_0])
   5.338 +  apply simp
   5.339 +  done
   5.340 +
   5.341 +lemma word_sless_msb_less: "x <s y \<longleftrightarrow> (msb y \<longrightarrow> msb x) \<and> ((msb x \<and> \<not> msb y) \<or> x < y)"
   5.342 +  by (auto simp add: word_sless_def word_sle_msb_le)
   5.343 +
   5.344 +definition "map_last f xs = (if xs = [] then [] else butlast xs @ [f (last xs)])"
   5.345 +
   5.346 +lemma map_last_simps:
   5.347 +  "map_last f [] = []"
   5.348 +  "map_last f [x] = [f x]"
   5.349 +  "map_last f (x # y # zs) = x # map_last f (y # zs)"
   5.350 +  by (simp_all add: map_last_def)
   5.351 +
   5.352 +lemma word_sle_rbl:
   5.353 +  "x <=s y \<longleftrightarrow> rev_bl_order True (map_last Not (rev (to_bl x))) (map_last Not (rev (to_bl y)))"
   5.354 +  using word_msb_alt[where w=x] word_msb_alt[where w=y]
   5.355 +  apply (simp add: word_sle_msb_le word_le_rbl)
   5.356 +  apply (subgoal_tac "length (to_bl x) = length (to_bl y)")
   5.357 +   apply (cases "to_bl x", simp)
   5.358 +   apply (cases "to_bl y", simp)
   5.359 +   apply (clarsimp simp: map_last_def rev_bl_order_rev_simp)
   5.360 +   apply auto
   5.361 +  done
   5.362 +
   5.363 +lemma word_sless_rbl:
   5.364 +  "x <s y \<longleftrightarrow> rev_bl_order False (map_last Not (rev (to_bl x))) (map_last Not (rev (to_bl y)))"
   5.365 +  using word_msb_alt[where w=x] word_msb_alt[where w=y]
   5.366 +  apply (simp add: word_sless_msb_less word_less_rbl)
   5.367 +  apply (subgoal_tac "length (to_bl x) = length (to_bl y)")
   5.368 +   apply (cases "to_bl x", simp)
   5.369 +   apply (cases "to_bl y", simp)
   5.370 +   apply (clarsimp simp: map_last_def rev_bl_order_rev_simp)
   5.371 +   apply auto
   5.372 +  done
   5.373 +
   5.374 +text \<open>Lemmas for unpacking \<^term>\<open>rev (to_bl n)\<close> for numerals n and also
   5.375 +  for irreducible values and expressions.\<close>
   5.376 +
   5.377 +lemma rev_bin_to_bl_simps:
   5.378 +  "rev (bin_to_bl 0 x) = []"
   5.379 +  "rev (bin_to_bl (Suc n) (numeral (num.Bit0 nm))) = False # rev (bin_to_bl n (numeral nm))"
   5.380 +  "rev (bin_to_bl (Suc n) (numeral (num.Bit1 nm))) = True # rev (bin_to_bl n (numeral nm))"
   5.381 +  "rev (bin_to_bl (Suc n) (numeral (num.One))) = True # replicate n False"
   5.382 +  "rev (bin_to_bl (Suc n) (- numeral (num.Bit0 nm))) = False # rev (bin_to_bl n (- numeral nm))"
   5.383 +  "rev (bin_to_bl (Suc n) (- numeral (num.Bit1 nm))) =
   5.384 +    True # rev (bin_to_bl n (- numeral (nm + num.One)))"
   5.385 +  "rev (bin_to_bl (Suc n) (- numeral (num.One))) = True # replicate n True"
   5.386 +  "rev (bin_to_bl (Suc n) (- numeral (num.Bit0 nm + num.One))) =
   5.387 +    True # rev (bin_to_bl n (- numeral (nm + num.One)))"
   5.388 +  "rev (bin_to_bl (Suc n) (- numeral (num.Bit1 nm + num.One))) =
   5.389 +    False # rev (bin_to_bl n (- numeral (nm + num.One)))"
   5.390 +  "rev (bin_to_bl (Suc n) (- numeral (num.One + num.One))) =
   5.391 +    False # rev (bin_to_bl n (- numeral num.One))"
   5.392 +  apply simp_all
   5.393 +  apply (simp_all only: bin_to_bl_aux_alt)
   5.394 +  apply (simp_all)
   5.395 +  apply (simp_all add: bin_to_bl_zero_aux bin_to_bl_minus1_aux)
   5.396 +  done
   5.397 +
   5.398 +lemma to_bl_upt: "to_bl x = rev (map ((!!) x) [0 ..< size x])"
   5.399 +  apply (rule nth_equalityI)
   5.400 +   apply (simp add: word_size)
   5.401 +  apply (auto simp: to_bl_nth word_size nth_rev)
   5.402 +  done
   5.403 +
   5.404 +lemma rev_to_bl_upt: "rev (to_bl x) = map ((!!) x) [0 ..< size x]"
   5.405 +  by (simp add: to_bl_upt)
   5.406 +
   5.407 +lemma upt_eq_list_intros:
   5.408 +  "j \<le> i \<Longrightarrow> [i ..< j] = []"
   5.409 +  "i = x \<Longrightarrow> x < j \<Longrightarrow> [x + 1 ..< j] = xs \<Longrightarrow> [i ..< j] = (x # xs)"
   5.410 +  by (simp_all add: upt_eq_Cons_conv)
   5.411 +
   5.412 +
   5.413 +subsection \<open>Tactic definition\<close>
   5.414 +
   5.415 +ML \<open>
   5.416 +structure Word_Bitwise_Tac =
   5.417 +struct
   5.418 +
   5.419 +val word_ss = simpset_of \<^theory_context>\<open>Word\<close>;
   5.420 +
   5.421 +fun mk_nat_clist ns =
   5.422 +  fold_rev (Thm.mk_binop \<^cterm>\<open>Cons :: nat \<Rightarrow> _\<close>)
   5.423 +    ns \<^cterm>\<open>[] :: nat list\<close>;
   5.424 +
   5.425 +fun upt_conv ctxt ct =
   5.426 +  case Thm.term_of ct of
   5.427 +    (\<^const>\<open>upt\<close> $ n $ m) =>
   5.428 +      let
   5.429 +        val (i, j) = apply2 (snd o HOLogic.dest_number) (n, m);
   5.430 +        val ns = map (Numeral.mk_cnumber \<^ctyp>\<open>nat\<close>) (i upto (j - 1))
   5.431 +          |> mk_nat_clist;
   5.432 +        val prop =
   5.433 +          Thm.mk_binop \<^cterm>\<open>(=) :: nat list \<Rightarrow> _\<close> ct ns
   5.434 +          |> Thm.apply \<^cterm>\<open>Trueprop\<close>;
   5.435 +      in
   5.436 +        try (fn () =>
   5.437 +          Goal.prove_internal ctxt [] prop
   5.438 +            (K (REPEAT_DETERM (resolve_tac ctxt @{thms upt_eq_list_intros} 1
   5.439 +                ORELSE simp_tac (put_simpset word_ss ctxt) 1))) |> mk_meta_eq) ()
   5.440 +      end
   5.441 +  | _ => NONE;
   5.442 +
   5.443 +val expand_upt_simproc =
   5.444 +  Simplifier.make_simproc \<^context> "expand_upt"
   5.445 +   {lhss = [\<^term>\<open>upt x y\<close>], proc = K upt_conv};
   5.446 +
   5.447 +fun word_len_simproc_fn ctxt ct =
   5.448 +  (case Thm.term_of ct of
   5.449 +    Const (\<^const_name>\<open>len_of\<close>, _) $ t =>
   5.450 +     (let
   5.451 +        val T = fastype_of t |> dest_Type |> snd |> the_single
   5.452 +        val n = Numeral.mk_cnumber \<^ctyp>\<open>nat\<close> (Word_Lib.dest_binT T);
   5.453 +        val prop =
   5.454 +          Thm.mk_binop \<^cterm>\<open>(=) :: nat \<Rightarrow> _\<close> ct n
   5.455 +          |> Thm.apply \<^cterm>\<open>Trueprop\<close>;
   5.456 +      in
   5.457 +        Goal.prove_internal ctxt [] prop (K (simp_tac (put_simpset word_ss ctxt) 1))
   5.458 +        |> mk_meta_eq |> SOME
   5.459 +      end handle TERM _ => NONE | TYPE _ => NONE)
   5.460 +  | _ => NONE);
   5.461 +
   5.462 +val word_len_simproc =
   5.463 +  Simplifier.make_simproc \<^context> "word_len"
   5.464 +   {lhss = [\<^term>\<open>len_of x\<close>], proc = K word_len_simproc_fn};
   5.465 +
   5.466 +(* convert 5 or nat 5 to Suc 4 when n_sucs = 1, Suc (Suc 4) when n_sucs = 2,
   5.467 +   or just 5 (discarding nat) when n_sucs = 0 *)
   5.468 +
   5.469 +fun nat_get_Suc_simproc_fn n_sucs ctxt ct =
   5.470 +  let
   5.471 +    val (f $ arg) = Thm.term_of ct;
   5.472 +    val n =
   5.473 +      (case arg of \<^term>\<open>nat\<close> $ n => n | n => n)
   5.474 +      |> HOLogic.dest_number |> snd;
   5.475 +    val (i, j) = if n > n_sucs then (n_sucs, n - n_sucs) else (n, 0);
   5.476 +    val arg' = funpow i HOLogic.mk_Suc (HOLogic.mk_number \<^typ>\<open>nat\<close> j);
   5.477 +    val _ = if arg = arg' then raise TERM ("", []) else ();
   5.478 +    fun propfn g =
   5.479 +      HOLogic.mk_eq (g arg, g arg')
   5.480 +      |> HOLogic.mk_Trueprop |> Thm.cterm_of ctxt;
   5.481 +    val eq1 =
   5.482 +      Goal.prove_internal ctxt [] (propfn I)
   5.483 +        (K (simp_tac (put_simpset word_ss ctxt) 1));
   5.484 +  in
   5.485 +    Goal.prove_internal ctxt [] (propfn (curry (op $) f))
   5.486 +      (K (simp_tac (put_simpset HOL_ss ctxt addsimps [eq1]) 1))
   5.487 +    |> mk_meta_eq |> SOME
   5.488 +  end handle TERM _ => NONE;
   5.489 +
   5.490 +fun nat_get_Suc_simproc n_sucs ts =
   5.491 +  Simplifier.make_simproc \<^context> "nat_get_Suc"
   5.492 +   {lhss = map (fn t => t $ \<^term>\<open>n :: nat\<close>) ts,
   5.493 +    proc = K (nat_get_Suc_simproc_fn n_sucs)};
   5.494 +
   5.495 +val no_split_ss =
   5.496 +  simpset_of (put_simpset HOL_ss \<^context>
   5.497 +    |> Splitter.del_split @{thm if_split});
   5.498 +
   5.499 +val expand_word_eq_sss =
   5.500 +  (simpset_of (put_simpset HOL_basic_ss \<^context> addsimps
   5.501 +       @{thms word_eq_rbl_eq word_le_rbl word_less_rbl word_sle_rbl word_sless_rbl}),
   5.502 +  map simpset_of [
   5.503 +   put_simpset no_split_ss \<^context> addsimps
   5.504 +    @{thms rbl_word_plus rbl_word_and rbl_word_or rbl_word_not
   5.505 +                                rbl_word_neg bl_word_sub rbl_word_xor
   5.506 +                                rbl_word_cat rbl_word_slice rbl_word_scast
   5.507 +                                rbl_word_ucast rbl_shiftl rbl_shiftr rbl_sshiftr
   5.508 +                                rbl_word_if},
   5.509 +   put_simpset no_split_ss \<^context> addsimps
   5.510 +    @{thms to_bl_numeral to_bl_neg_numeral to_bl_0 rbl_word_1},
   5.511 +   put_simpset no_split_ss \<^context> addsimps
   5.512 +    @{thms rev_rev_ident rev_replicate rev_map to_bl_upt word_size}
   5.513 +          addsimprocs [word_len_simproc],
   5.514 +   put_simpset no_split_ss \<^context> addsimps
   5.515 +    @{thms list.simps split_conv replicate.simps list.map
   5.516 +                                zip_Cons_Cons zip_Nil drop_Suc_Cons drop_0 drop_Nil
   5.517 +                                foldr.simps map2_Cons map2_Nil takefill_Suc_Cons
   5.518 +                                takefill_Suc_Nil takefill.Z rbl_succ2_simps
   5.519 +                                rbl_plus_simps rev_bin_to_bl_simps append.simps
   5.520 +                                takefill_last_simps drop_nonempty_simps
   5.521 +                                rev_bl_order_simps}
   5.522 +          addsimprocs [expand_upt_simproc,
   5.523 +                       nat_get_Suc_simproc 4
   5.524 +                         [\<^term>\<open>replicate\<close>, \<^term>\<open>takefill x\<close>,
   5.525 +                          \<^term>\<open>drop\<close>, \<^term>\<open>bin_to_bl\<close>,
   5.526 +                          \<^term>\<open>takefill_last x\<close>,
   5.527 +                          \<^term>\<open>drop_nonempty x\<close>]],
   5.528 +    put_simpset no_split_ss \<^context> addsimps @{thms xor3_simps carry_simps if_bool_simps}
   5.529 +  ])
   5.530 +
   5.531 +fun tac ctxt =
   5.532 +  let
   5.533 +    val (ss, sss) = expand_word_eq_sss;
   5.534 +  in
   5.535 +    foldr1 (op THEN_ALL_NEW)
   5.536 +      ((CHANGED o safe_full_simp_tac (put_simpset ss ctxt)) ::
   5.537 +        map (fn ss => safe_full_simp_tac (put_simpset ss ctxt)) sss)
   5.538 +  end;
   5.539 +
   5.540 +end
   5.541 +\<close>
   5.542 +
   5.543 +method_setup word_bitwise =
   5.544 +  \<open>Scan.succeed (fn ctxt => Method.SIMPLE_METHOD (Word_Bitwise_Tac.tac ctxt 1))\<close>
   5.545 +  "decomposer for word equalities and inequalities into bit propositions"
   5.546 +
   5.547 +end
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Word/Word_Examples.thy	Tue Apr 16 19:50:18 2019 +0000
     6.3 @@ -0,0 +1,207 @@
     6.4 +(*  Title:      HOL/Word/Word_Examples.thy
     6.5 +    Authors:    Gerwin Klein and Thomas Sewell, NICTA
     6.6 +
     6.7 +Examples demonstrating and testing various word operations.
     6.8 +*)
     6.9 +
    6.10 +section "Examples of word operations"
    6.11 +
    6.12 +theory Word_Examples
    6.13 +  imports Word_Bitwise
    6.14 +begin
    6.15 +
    6.16 +type_synonym word32 = "32 word"
    6.17 +type_synonym word8 = "8 word"
    6.18 +type_synonym byte = word8
    6.19 +
    6.20 +text "modulus"
    6.21 +
    6.22 +lemma "(27 :: 4 word) = -5" by simp
    6.23 +
    6.24 +lemma "(27 :: 4 word) = 11" by simp
    6.25 +
    6.26 +lemma "27 \<noteq> (11 :: 6 word)" by simp
    6.27 +
    6.28 +text "signed"
    6.29 +
    6.30 +lemma "(127 :: 6 word) = -1" by simp
    6.31 +
    6.32 +text "number ring simps"
    6.33 +
    6.34 +lemma
    6.35 +  "27 + 11 = (38::'a::len word)"
    6.36 +  "27 + 11 = (6::5 word)"
    6.37 +  "7 * 3 = (21::'a::len word)"
    6.38 +  "11 - 27 = (-16::'a::len word)"
    6.39 +  "- (- 11) = (11::'a::len word)"
    6.40 +  "-40 + 1 = (-39::'a::len word)"
    6.41 +  by simp_all
    6.42 +
    6.43 +lemma "word_pred 2 = 1" by simp
    6.44 +
    6.45 +lemma "word_succ (- 3) = -2" by simp
    6.46 +
    6.47 +lemma "23 < (27::8 word)" by simp
    6.48 +lemma "23 \<le> (27::8 word)" by simp
    6.49 +lemma "\<not> 23 < (27::2 word)" by simp
    6.50 +lemma "0 < (4::3 word)" by simp
    6.51 +lemma "1 < (4::3 word)" by simp
    6.52 +lemma "0 < (1::3 word)" by simp
    6.53 +
    6.54 +text "ring operations"
    6.55 +
    6.56 +lemma "a + 2 * b + c - b = (b + c) + (a :: 32 word)" by simp
    6.57 +
    6.58 +text "casting"
    6.59 +
    6.60 +lemma "uint (234567 :: 10 word) = 71" by simp
    6.61 +lemma "uint (-234567 :: 10 word) = 953" by simp
    6.62 +lemma "sint (234567 :: 10 word) = 71" by simp
    6.63 +lemma "sint (-234567 :: 10 word) = -71" by simp
    6.64 +lemma "uint (1 :: 10 word) = 1" by simp
    6.65 +
    6.66 +lemma "unat (-234567 :: 10 word) = 953" by simp
    6.67 +lemma "unat (1 :: 10 word) = 1" by simp
    6.68 +
    6.69 +lemma "ucast (0b1010 :: 4 word) = (0b10 :: 2 word)" by simp
    6.70 +lemma "ucast (0b1010 :: 4 word) = (0b1010 :: 10 word)" by simp
    6.71 +lemma "scast (0b1010 :: 4 word) = (0b111010 :: 6 word)" by simp
    6.72 +lemma "ucast (1 :: 4 word) = (1 :: 2 word)" by simp
    6.73 +
    6.74 +text "reducing goals to nat or int and arith:"
    6.75 +lemma "i < x \<Longrightarrow> i < i + 1" for i x :: "'a::len word"
    6.76 +  by unat_arith
    6.77 +lemma "i < x \<Longrightarrow> i < i + 1" for i x :: "'a::len word"
    6.78 +  by unat_arith
    6.79 +
    6.80 +text "bool lists"
    6.81 +
    6.82 +lemma "of_bl [True, False, True, True] = (0b1011::'a::len word)" by simp
    6.83 +
    6.84 +lemma "to_bl (0b110::4 word) = [False, True, True, False]" by simp
    6.85 +
    6.86 +text "this is not exactly fast, but bearable"
    6.87 +lemma "of_bl (replicate 32 True) = (0xFFFFFFFF::32 word)" by simp
    6.88 +
    6.89 +text "this works only for replicate n True"
    6.90 +lemma "of_bl (replicate 32 True) = (0xFFFFFFFF::32 word)"
    6.91 +  by (unfold mask_bl [symmetric]) (simp add: mask_def)
    6.92 +
    6.93 +
    6.94 +text "bit operations"
    6.95 +
    6.96 +lemma "0b110 AND 0b101 = (0b100 :: 32 word)" by simp
    6.97 +lemma "0b110 OR 0b011 = (0b111 :: 8 word)" by simp
    6.98 +lemma "0xF0 XOR 0xFF = (0x0F :: byte)" by simp
    6.99 +lemma "NOT (0xF0 :: 16 word) = 0xFF0F" by simp
   6.100 +lemma "0 AND 5 = (0 :: byte)" by simp
   6.101 +lemma "1 AND 1 = (1 :: byte)" by simp
   6.102 +lemma "1 AND 0 = (0 :: byte)" by simp
   6.103 +lemma "1 AND 5 = (1 :: byte)" by simp
   6.104 +lemma "1 OR 6 = (7 :: byte)" by simp
   6.105 +lemma "1 OR 1 = (1 :: byte)" by simp
   6.106 +lemma "1 XOR 7 = (6 :: byte)" by simp
   6.107 +lemma "1 XOR 1 = (0 :: byte)" by simp
   6.108 +lemma "NOT 1 = (254 :: byte)" by simp
   6.109 +lemma "NOT 0 = (255 :: byte)" apply simp oops
   6.110 +(* FIXME: "NOT 0" rewrites to "max_word" instead of "-1" *)
   6.111 +
   6.112 +lemma "(-1 :: 32 word) = 0xFFFFFFFF" by simp
   6.113 +
   6.114 +lemma "(0b0010 :: 4 word) !! 1" by simp
   6.115 +lemma "\<not> (0b0010 :: 4 word) !! 0" by simp
   6.116 +lemma "\<not> (0b1000 :: 3 word) !! 4" by simp
   6.117 +lemma "\<not> (1 :: 3 word) !! 2" by simp
   6.118 +
   6.119 +lemma "(0b11000 :: 10 word) !! n = (n = 4 \<or> n = 3)"
   6.120 +  by (auto simp add: bin_nth_Bit0 bin_nth_Bit1)
   6.121 +
   6.122 +lemma "set_bit 55 7 True = (183::'a::len0 word)" by simp
   6.123 +lemma "set_bit 0b0010 7 True = (0b10000010::'a::len0 word)" by simp
   6.124 +lemma "set_bit 0b0010 1 False = (0::'a::len0 word)" by simp
   6.125 +lemma "set_bit 1 3 True = (0b1001::'a::len0 word)" by simp
   6.126 +lemma "set_bit 1 0 False = (0::'a::len0 word)" by simp
   6.127 +lemma "set_bit 0 3 True = (0b1000::'a::len0 word)" by simp
   6.128 +lemma "set_bit 0 3 False = (0::'a::len0 word)" by simp
   6.129 +
   6.130 +lemma "lsb (0b0101::'a::len word)" by simp
   6.131 +lemma "\<not> lsb (0b1000::'a::len word)" by simp
   6.132 +lemma "lsb (1::'a::len word)" by simp
   6.133 +lemma "\<not> lsb (0::'a::len word)" by simp
   6.134 +
   6.135 +lemma "\<not> msb (0b0101::4 word)" by simp
   6.136 +lemma   "msb (0b1000::4 word)" by simp
   6.137 +lemma "\<not> msb (1::4 word)" by simp
   6.138 +lemma "\<not> msb (0::4 word)" by simp
   6.139 +
   6.140 +lemma "word_cat (27::4 word) (27::8 word) = (2843::'a::len word)" by simp
   6.141 +lemma "word_cat (0b0011::4 word) (0b1111::6word) = (0b0011001111 :: 10 word)"
   6.142 +  by simp
   6.143 +
   6.144 +lemma "0b1011 << 2 = (0b101100::'a::len0 word)" by simp
   6.145 +lemma "0b1011 >> 2 = (0b10::8 word)" by simp
   6.146 +lemma "0b1011 >>> 2 = (0b10::8 word)" by simp
   6.147 +lemma "1 << 2 = (0b100::'a::len0 word)" apply simp? oops
   6.148 +
   6.149 +lemma "slice 3 (0b101111::6 word) = (0b101::3 word)" by simp
   6.150 +lemma "slice 3 (1::6 word) = (0::3 word)" apply simp? oops
   6.151 +
   6.152 +lemma "word_rotr 2 0b0110 = (0b1001::4 word)" by simp
   6.153 +lemma "word_rotl 1 0b1110 = (0b1101::4 word)" by simp
   6.154 +lemma "word_roti 2 0b1110 = (0b1011::4 word)" by simp
   6.155 +lemma "word_roti (- 2) 0b0110 = (0b1001::4 word)" by simp
   6.156 +lemma "word_rotr 2 0 = (0::4 word)" by simp
   6.157 +lemma "word_rotr 2 1 = (0b0100::4 word)" apply simp? oops
   6.158 +lemma "word_rotl 2 1 = (0b0100::4 word)" apply simp? oops
   6.159 +lemma "word_roti (- 2) 1 = (0b0100::4 word)" apply simp? oops
   6.160 +
   6.161 +lemma "(x AND 0xff00) OR (x AND 0x00ff) = (x::16 word)"
   6.162 +proof -
   6.163 +  have "(x AND 0xff00) OR (x AND 0x00ff) = x AND (0xff00 OR 0x00ff)"
   6.164 +    by (simp only: word_ao_dist2)
   6.165 +  also have "0xff00 OR 0x00ff = (-1::16 word)"
   6.166 +    by simp
   6.167 +  also have "x AND -1 = x"
   6.168 +    by simp
   6.169 +  finally show ?thesis .
   6.170 +qed
   6.171 +
   6.172 +text "alternative proof using bitwise expansion"
   6.173 +
   6.174 +lemma "(x AND 0xff00) OR (x AND 0x00ff) = (x::16 word)"
   6.175 +  by word_bitwise
   6.176 +
   6.177 +text "more proofs using bitwise expansion"
   6.178 +
   6.179 +lemma "(x AND NOT 3) >> 4 << 2 = ((x >> 2) AND NOT 3)"
   6.180 +  for x :: "10 word"
   6.181 +  by word_bitwise
   6.182 +
   6.183 +lemma "((x AND -8) >> 3) AND 7 = (x AND 56) >> 3"
   6.184 +  for x :: "12 word"
   6.185 +  by word_bitwise
   6.186 +
   6.187 +text "some problems require further reasoning after bit expansion"
   6.188 +
   6.189 +lemma "x \<le> 42 \<Longrightarrow> x \<le> 89"
   6.190 +  for x :: "8 word"
   6.191 +  apply word_bitwise
   6.192 +  apply blast
   6.193 +  done
   6.194 +
   6.195 +lemma "(x AND 1023) = 0 \<Longrightarrow> x \<le> -1024"
   6.196 +  for x :: word32
   6.197 +  apply word_bitwise
   6.198 +  apply clarsimp
   6.199 +  done
   6.200 +
   6.201 +text "operations like shifts by non-numerals will expose some internal list
   6.202 + representations but may still be easy to solve"
   6.203 +
   6.204 +lemma shiftr_overflow: "32 \<le> a \<Longrightarrow> b >> a = 0"
   6.205 +  for b :: word32
   6.206 +  apply word_bitwise
   6.207 +  apply simp
   6.208 +  done
   6.209 +
   6.210 +end