summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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

4 Examples demonstrating and testing various word operations.

5 *)

7 header "Examples of word operations"

9 theory WordExamples

10 imports Word

11 begin

13 type_synonym word32 = "32 word"

14 type_synonym word8 = "8 word"

15 type_synonym byte = word8

17 -- "modulus"

19 lemma "(27 :: 4 word) = -5" by simp

21 lemma "(27 :: 4 word) = 11" by simp

23 lemma "27 \<noteq> (11 :: 6 word)" by simp

25 -- "signed"

26 lemma "(127 :: 6 word) = -1" by simp

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

38 lemma "word_pred 2 = 1" by simp

40 lemma "word_succ -3 = -2" by simp

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

47 -- "ring operations"

49 lemma "a + 2 * b + c - b = (b + c) + (a :: 32 word)" by simp

51 -- "casting"

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

58 lemma "unat (-234567 :: 10 word) = 953" by simp

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

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

68 -- "bool lists"

70 lemma "of_bl [True, False, True, True] = (0b1011::'a::len word)" by simp

72 lemma "to_bl (0b110::4 word) = [False, True, True, False]" by simp

74 -- "this is not exactly fast, but bearable"

75 lemma "of_bl (replicate 32 True) = (0xFFFFFFFF::32 word)" by simp

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)

82 -- "bit operations"

84 lemma "0b110 AND 0b101 = (0b100 :: 32 word)" by simp

86 lemma "0b110 OR 0b011 = (0b111 :: 8 word)" by simp

88 lemma "0xF0 XOR 0xFF = (0x0F :: byte)" by simp

90 lemma "NOT (0xF0 :: 16 word) = 0xFF0F" by simp

92 lemma "(-1 :: 32 word) = 0xFFFFFFFF" by simp

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

98 lemma "(0b11000 :: 10 word) !! n = (n = 4 \<or> n = 3)"

99 by (auto simp add: bin_nth_Bit0 bin_nth_Bit1)

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

105 lemma "lsb (0b0101::'a::len word)" by simp

106 lemma "\<not> lsb (0b1000::'a::len word)" by simp

108 lemma "\<not> msb (0b0101::4 word)" by simp

109 lemma "msb (0b1000::4 word)" by simp

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

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

119 lemma "slice 3 (0b101111::6 word) = (0b101::3 word)" by simp

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

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

137 end