simplified session (again, see 39e29972cb96): WordExamples requires < 1s;
authorwenzelm
Sun Dec 03 19:09:42 2017 +0100 (10 months ago)
changeset 6712285b40f300fab
parent 67121 116968454d70
child 67123 3fe40ff1b921
simplified session (again, see 39e29972cb96): WordExamples requires < 1s;
src/HOL/ROOT
src/HOL/Word/Examples/WordExamples.thy
src/HOL/Word/Word.thy
src/HOL/Word/WordExamples.thy
     1.1 --- a/src/HOL/ROOT	Sun Dec 03 19:00:55 2017 +0100
     1.2 +++ b/src/HOL/ROOT	Sun Dec 03 19:09:42 2017 +0100
     1.3 @@ -786,11 +786,9 @@
     1.4      Word
     1.5      WordBitwise
     1.6      Bit_Comparison
     1.7 +    WordExamples
     1.8    document_files "root.bib" "root.tex"
     1.9  
    1.10 -session "HOL-Word-Examples" in "Word/Examples" = "HOL-Word" +
    1.11 -  theories WordExamples
    1.12 -
    1.13  session "HOL-Statespace" in Statespace = HOL +
    1.14    theories [skip_proofs = false]
    1.15      StateSpaceEx
     2.1 --- a/src/HOL/Word/Examples/WordExamples.thy	Sun Dec 03 19:00:55 2017 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,207 +0,0 @@
     2.4 -(*  Title:      HOL/Word/Examples/WordExamples.thy
     2.5 -    Authors:    Gerwin Klein and Thomas Sewell, NICTA
     2.6 -
     2.7 -Examples demonstrating and testing various word operations.
     2.8 -*)
     2.9 -
    2.10 -section "Examples of word operations"
    2.11 -
    2.12 -theory WordExamples
    2.13 -  imports "HOL-Word.Word" "HOL-Word.WordBitwise"
    2.14 -begin
    2.15 -
    2.16 -type_synonym word32 = "32 word"
    2.17 -type_synonym word8 = "8 word"
    2.18 -type_synonym byte = word8
    2.19 -
    2.20 -text "modulus"
    2.21 -
    2.22 -lemma "(27 :: 4 word) = -5" by simp
    2.23 -
    2.24 -lemma "(27 :: 4 word) = 11" by simp
    2.25 -
    2.26 -lemma "27 \<noteq> (11 :: 6 word)" by simp
    2.27 -
    2.28 -text "signed"
    2.29 -
    2.30 -lemma "(127 :: 6 word) = -1" by simp
    2.31 -
    2.32 -text "number ring simps"
    2.33 -
    2.34 -lemma
    2.35 -  "27 + 11 = (38::'a::len word)"
    2.36 -  "27 + 11 = (6::5 word)"
    2.37 -  "7 * 3 = (21::'a::len word)"
    2.38 -  "11 - 27 = (-16::'a::len word)"
    2.39 -  "- (- 11) = (11::'a::len word)"
    2.40 -  "-40 + 1 = (-39::'a::len word)"
    2.41 -  by simp_all
    2.42 -
    2.43 -lemma "word_pred 2 = 1" by simp
    2.44 -
    2.45 -lemma "word_succ (- 3) = -2" by simp
    2.46 -
    2.47 -lemma "23 < (27::8 word)" by simp
    2.48 -lemma "23 \<le> (27::8 word)" by simp
    2.49 -lemma "\<not> 23 < (27::2 word)" by simp
    2.50 -lemma "0 < (4::3 word)" by simp
    2.51 -lemma "1 < (4::3 word)" by simp
    2.52 -lemma "0 < (1::3 word)" by simp
    2.53 -
    2.54 -text "ring operations"
    2.55 -
    2.56 -lemma "a + 2 * b + c - b = (b + c) + (a :: 32 word)" by simp
    2.57 -
    2.58 -text "casting"
    2.59 -
    2.60 -lemma "uint (234567 :: 10 word) = 71" by simp
    2.61 -lemma "uint (-234567 :: 10 word) = 953" by simp
    2.62 -lemma "sint (234567 :: 10 word) = 71" by simp
    2.63 -lemma "sint (-234567 :: 10 word) = -71" by simp
    2.64 -lemma "uint (1 :: 10 word) = 1" by simp
    2.65 -
    2.66 -lemma "unat (-234567 :: 10 word) = 953" by simp
    2.67 -lemma "unat (1 :: 10 word) = 1" by simp
    2.68 -
    2.69 -lemma "ucast (0b1010 :: 4 word) = (0b10 :: 2 word)" by simp
    2.70 -lemma "ucast (0b1010 :: 4 word) = (0b1010 :: 10 word)" by simp
    2.71 -lemma "scast (0b1010 :: 4 word) = (0b111010 :: 6 word)" by simp
    2.72 -lemma "ucast (1 :: 4 word) = (1 :: 2 word)" by simp
    2.73 -
    2.74 -text "reducing goals to nat or int and arith:"
    2.75 -lemma "i < x \<Longrightarrow> i < i + 1" for i x :: "'a::len word"
    2.76 -  by unat_arith
    2.77 -lemma "i < x \<Longrightarrow> i < i + 1" for i x :: "'a::len word"
    2.78 -  by unat_arith
    2.79 -
    2.80 -text "bool lists"
    2.81 -
    2.82 -lemma "of_bl [True, False, True, True] = (0b1011::'a::len word)" by simp
    2.83 -
    2.84 -lemma "to_bl (0b110::4 word) = [False, True, True, False]" by simp
    2.85 -
    2.86 -text "this is not exactly fast, but bearable"
    2.87 -lemma "of_bl (replicate 32 True) = (0xFFFFFFFF::32 word)" by simp
    2.88 -
    2.89 -text "this works only for replicate n True"
    2.90 -lemma "of_bl (replicate 32 True) = (0xFFFFFFFF::32 word)"
    2.91 -  by (unfold mask_bl [symmetric]) (simp add: mask_def)
    2.92 -
    2.93 -
    2.94 -text "bit operations"
    2.95 -
    2.96 -lemma "0b110 AND 0b101 = (0b100 :: 32 word)" by simp
    2.97 -lemma "0b110 OR 0b011 = (0b111 :: 8 word)" by simp
    2.98 -lemma "0xF0 XOR 0xFF = (0x0F :: byte)" by simp
    2.99 -lemma "NOT (0xF0 :: 16 word) = 0xFF0F" by simp
   2.100 -lemma "0 AND 5 = (0 :: byte)" by simp
   2.101 -lemma "1 AND 1 = (1 :: byte)" by simp
   2.102 -lemma "1 AND 0 = (0 :: byte)" by simp
   2.103 -lemma "1 AND 5 = (1 :: byte)" by simp
   2.104 -lemma "1 OR 6 = (7 :: byte)" by simp
   2.105 -lemma "1 OR 1 = (1 :: byte)" by simp
   2.106 -lemma "1 XOR 7 = (6 :: byte)" by simp
   2.107 -lemma "1 XOR 1 = (0 :: byte)" by simp
   2.108 -lemma "NOT 1 = (254 :: byte)" by simp
   2.109 -lemma "NOT 0 = (255 :: byte)" apply simp oops
   2.110 -(* FIXME: "NOT 0" rewrites to "max_word" instead of "-1" *)
   2.111 -
   2.112 -lemma "(-1 :: 32 word) = 0xFFFFFFFF" by simp
   2.113 -
   2.114 -lemma "(0b0010 :: 4 word) !! 1" by simp
   2.115 -lemma "\<not> (0b0010 :: 4 word) !! 0" by simp
   2.116 -lemma "\<not> (0b1000 :: 3 word) !! 4" by simp
   2.117 -lemma "\<not> (1 :: 3 word) !! 2" by simp
   2.118 -
   2.119 -lemma "(0b11000 :: 10 word) !! n = (n = 4 \<or> n = 3)"
   2.120 -  by (auto simp add: bin_nth_Bit0 bin_nth_Bit1)
   2.121 -
   2.122 -lemma "set_bit 55 7 True = (183::'a::len0 word)" by simp
   2.123 -lemma "set_bit 0b0010 7 True = (0b10000010::'a::len0 word)" by simp
   2.124 -lemma "set_bit 0b0010 1 False = (0::'a::len0 word)" by simp
   2.125 -lemma "set_bit 1 3 True = (0b1001::'a::len0 word)" by simp
   2.126 -lemma "set_bit 1 0 False = (0::'a::len0 word)" by simp
   2.127 -lemma "set_bit 0 3 True = (0b1000::'a::len0 word)" by simp
   2.128 -lemma "set_bit 0 3 False = (0::'a::len0 word)" by simp
   2.129 -
   2.130 -lemma "lsb (0b0101::'a::len word)" by simp
   2.131 -lemma "\<not> lsb (0b1000::'a::len word)" by simp
   2.132 -lemma "lsb (1::'a::len word)" by simp
   2.133 -lemma "\<not> lsb (0::'a::len word)" by simp
   2.134 -
   2.135 -lemma "\<not> msb (0b0101::4 word)" by simp
   2.136 -lemma   "msb (0b1000::4 word)" by simp
   2.137 -lemma "\<not> msb (1::4 word)" by simp
   2.138 -lemma "\<not> msb (0::4 word)" by simp
   2.139 -
   2.140 -lemma "word_cat (27::4 word) (27::8 word) = (2843::'a::len word)" by simp
   2.141 -lemma "word_cat (0b0011::4 word) (0b1111::6word) = (0b0011001111 :: 10 word)"
   2.142 -  by simp
   2.143 -
   2.144 -lemma "0b1011 << 2 = (0b101100::'a::len0 word)" by simp
   2.145 -lemma "0b1011 >> 2 = (0b10::8 word)" by simp
   2.146 -lemma "0b1011 >>> 2 = (0b10::8 word)" by simp
   2.147 -lemma "1 << 2 = (0b100::'a::len0 word)" apply simp? oops
   2.148 -
   2.149 -lemma "slice 3 (0b101111::6 word) = (0b101::3 word)" by simp
   2.150 -lemma "slice 3 (1::6 word) = (0::3 word)" apply simp? oops
   2.151 -
   2.152 -lemma "word_rotr 2 0b0110 = (0b1001::4 word)" by simp
   2.153 -lemma "word_rotl 1 0b1110 = (0b1101::4 word)" by simp
   2.154 -lemma "word_roti 2 0b1110 = (0b1011::4 word)" by simp
   2.155 -lemma "word_roti (- 2) 0b0110 = (0b1001::4 word)" by simp
   2.156 -lemma "word_rotr 2 0 = (0::4 word)" by simp
   2.157 -lemma "word_rotr 2 1 = (0b0100::4 word)" apply simp? oops
   2.158 -lemma "word_rotl 2 1 = (0b0100::4 word)" apply simp? oops
   2.159 -lemma "word_roti (- 2) 1 = (0b0100::4 word)" apply simp? oops
   2.160 -
   2.161 -lemma "(x AND 0xff00) OR (x AND 0x00ff) = (x::16 word)"
   2.162 -proof -
   2.163 -  have "(x AND 0xff00) OR (x AND 0x00ff) = x AND (0xff00 OR 0x00ff)"
   2.164 -    by (simp only: word_ao_dist2)
   2.165 -  also have "0xff00 OR 0x00ff = (-1::16 word)"
   2.166 -    by simp
   2.167 -  also have "x AND -1 = x"
   2.168 -    by simp
   2.169 -  finally show ?thesis .
   2.170 -qed
   2.171 -
   2.172 -text "alternative proof using bitwise expansion"
   2.173 -
   2.174 -lemma "(x AND 0xff00) OR (x AND 0x00ff) = (x::16 word)"
   2.175 -  by word_bitwise
   2.176 -
   2.177 -text "more proofs using bitwise expansion"
   2.178 -
   2.179 -lemma "(x AND NOT 3) >> 4 << 2 = ((x >> 2) AND NOT 3)"
   2.180 -  for x :: "10 word"
   2.181 -  by word_bitwise
   2.182 -
   2.183 -lemma "((x AND -8) >> 3) AND 7 = (x AND 56) >> 3"
   2.184 -  for x :: "12 word"
   2.185 -  by word_bitwise
   2.186 -
   2.187 -text "some problems require further reasoning after bit expansion"
   2.188 -
   2.189 -lemma "x \<le> 42 \<Longrightarrow> x \<le> 89"
   2.190 -  for x :: "8 word"
   2.191 -  apply word_bitwise
   2.192 -  apply blast
   2.193 -  done
   2.194 -
   2.195 -lemma "(x AND 1023) = 0 \<Longrightarrow> x \<le> -1024"
   2.196 -  for x :: word32
   2.197 -  apply word_bitwise
   2.198 -  apply clarsimp
   2.199 -  done
   2.200 -
   2.201 -text "operations like shifts by non-numerals will expose some internal list
   2.202 - representations but may still be easy to solve"
   2.203 -
   2.204 -lemma shiftr_overflow: "32 \<le> a \<Longrightarrow> b >> a = 0"
   2.205 -  for b :: word32
   2.206 -  apply word_bitwise
   2.207 -  apply simp
   2.208 -  done
   2.209 -
   2.210 -end
     3.1 --- a/src/HOL/Word/Word.thy	Sun Dec 03 19:00:55 2017 +0100
     3.2 +++ b/src/HOL/Word/Word.thy	Sun Dec 03 19:09:42 2017 +0100
     3.3 @@ -14,7 +14,7 @@
     3.4    Word_Miscellaneous
     3.5  begin
     3.6  
     3.7 -text \<open>See \<^file>\<open>Examples/WordExamples.thy\<close> for examples.\<close>
     3.8 +text \<open>See \<^file>\<open>WordExamples.thy\<close> for examples.\<close>
     3.9  
    3.10  subsection \<open>Type definition\<close>
    3.11  
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Word/WordExamples.thy	Sun Dec 03 19:09:42 2017 +0100
     4.3 @@ -0,0 +1,207 @@
     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