src/HOL/Word/Examples/WordExamples.thy
author wenzelm
Sat Apr 23 13:00:19 2011 +0200 (2011-04-23)
changeset 42463 f270e3e18be5
parent 29640 741f26190c96
child 44762 8f9d09241a68
permissions -rw-r--r--
modernized specifications;
     1 (* 
     2   Author: Gerwin Klein, NICTA
     3 
     4   Examples demonstrating and testing various word operations.
     5 *)
     6 
     7 header "Examples of word operations"
     8 
     9 theory WordExamples
    10 imports Word
    11 begin
    12 
    13 type_synonym word32 = "32 word"
    14 type_synonym word8 = "8 word"
    15 type_synonym byte = word8
    16 
    17 -- "modulus"
    18 
    19 lemma "(27 :: 4 word) = -5" by simp
    20 
    21 lemma "(27 :: 4 word) = 11" by simp
    22 
    23 lemma "27 \<noteq> (11 :: 6 word)" by simp
    24 
    25 -- "signed"
    26 lemma "(127 :: 6 word) = -1" by simp
    27 
    28 -- "number ring simps"
    29 lemma 
    30   "27 + 11 = (38::'a::len word)"
    31   "27 + 11 = (6::5 word)"
    32   "7 * 3 = (21::'a::len word)"
    33   "11 - 27 = (-16::'a::len word)"
    34   "- -11 = (11::'a::len word)"
    35   "-40 + 1 = (-39::'a::len word)"
    36   by simp_all
    37 
    38 lemma "word_pred 2 = 1" by simp
    39 
    40 lemma "word_succ -3 = -2" by simp
    41   
    42 lemma "23 < (27::8 word)" by simp
    43 lemma "23 \<le> (27::8 word)" by simp
    44 lemma "\<not> 23 < (27::2 word)" by simp
    45 lemma "0 < (4::3 word)" by simp
    46 
    47 -- "ring operations"
    48 
    49 lemma "a + 2 * b + c - b = (b + c) + (a :: 32 word)" by simp
    50 
    51 -- "casting"
    52 
    53 lemma "uint (234567 :: 10 word) = 71" by simp
    54 lemma "uint (-234567 :: 10 word) = 953" by simp
    55 lemma "sint (234567 :: 10 word) = 71" by simp
    56 lemma "sint (-234567 :: 10 word) = -71" by simp
    57 
    58 lemma "unat (-234567 :: 10 word) = 953" by simp
    59 
    60 lemma "ucast (0b1010 :: 4 word) = (0b10 :: 2 word)" by simp
    61 lemma "ucast (0b1010 :: 4 word) = (0b1010 :: 10 word)" by simp
    62 lemma "scast (0b1010 :: 4 word) = (0b111010 :: 6 word)" by simp
    63 
    64 -- "reducing goals to nat or int and arith:"
    65 lemma "i < x ==> i < (i + 1 :: 'a :: len word)" by unat_arith
    66 lemma "i < x ==> i < (i + 1 :: 'a :: len word)" by uint_arith
    67 
    68 -- "bool lists"
    69 
    70 lemma "of_bl [True, False, True, True] = (0b1011::'a::len word)" by simp
    71 
    72 lemma "to_bl (0b110::4 word) = [False, True, True, False]" by simp
    73 
    74 -- "this is not exactly fast, but bearable"
    75 lemma "of_bl (replicate 32 True) = (0xFFFFFFFF::32 word)" by simp
    76 
    77 -- "this works only for replicate n True"
    78 lemma "of_bl (replicate 32 True) = (0xFFFFFFFF::32 word)"
    79   by (unfold mask_bl [symmetric]) (simp add: mask_def)
    80 
    81 
    82 -- "bit operations"
    83 
    84 lemma "0b110 AND 0b101 = (0b100 :: 32 word)" by simp
    85 
    86 lemma "0b110 OR 0b011 = (0b111 :: 8 word)" by simp
    87 
    88 lemma "0xF0 XOR 0xFF = (0x0F :: byte)" by simp
    89 
    90 lemma "NOT (0xF0 :: 16 word) = 0xFF0F" by simp
    91 
    92 lemma "(-1 :: 32 word) = 0xFFFFFFFF" by simp
    93 
    94 lemma "(0b0010 :: 4 word) !! 1" by simp
    95 lemma "\<not> (0b0010 :: 4 word) !! 0" by simp
    96 lemma "\<not> (0b1000 :: 3 word) !! 4" by simp
    97 
    98 lemma "(0b11000 :: 10 word) !! n = (n = 4 \<or> n = 3)" 
    99   by (auto simp add: bin_nth_Bit0 bin_nth_Bit1)
   100 
   101 lemma "set_bit 55 7 True = (183::'a::len0 word)" by simp
   102 lemma "set_bit 0b0010 7 True = (0b10000010::'a::len0 word)" by simp
   103 lemma "set_bit 0b0010 1 False = (0::'a::len0 word)" by simp
   104 
   105 lemma "lsb (0b0101::'a::len word)" by simp
   106 lemma "\<not> lsb (0b1000::'a::len word)" by simp
   107 
   108 lemma "\<not> msb (0b0101::4 word)" by simp
   109 lemma   "msb (0b1000::4 word)" by simp
   110 
   111 lemma "word_cat (27::4 word) (27::8 word) = (2843::'a::len word)" by simp
   112 lemma "word_cat (0b0011::4 word) (0b1111::6word) = (0b0011001111 :: 10 word)" 
   113   by simp
   114 
   115 lemma "0b1011 << 2 = (0b101100::'a::len0 word)" by simp
   116 lemma "0b1011 >> 2 = (0b10::8 word)" by simp
   117 lemma "0b1011 >>> 2 = (0b10::8 word)" by simp
   118 
   119 lemma "slice 3 (0b101111::6 word) = (0b101::3 word)" by simp
   120 
   121 lemma "word_rotr 2 0b0110 = (0b1001::4 word)" by simp
   122 lemma "word_rotl 1 0b1110 = (0b1101::4 word)" by simp
   123 lemma "word_roti 2 0b1110 = (0b1011::4 word)" by simp
   124 lemma "word_roti -2 0b0110 = (0b1001::4 word)" by simp
   125 
   126 lemma "(x AND 0xff00) OR (x AND 0x00ff) = (x::16 word)"
   127 proof -
   128   have "(x AND 0xff00) OR (x AND 0x00ff) = x AND (0xff00 OR 0x00ff)"
   129     by (simp only: word_ao_dist2)
   130   also have "0xff00 OR 0x00ff = (-1::16 word)"
   131     by simp
   132   also have "x AND -1 = x"
   133     by simp
   134   finally show ?thesis .
   135 qed
   136 
   137 end