1 (* Title: HOL/ex/Hex_Bin_Examples.thy
2 Author: Gerwin Klein, NICTA
5 section {* Examples for hexadecimal and binary numerals *}
7 theory Hex_Bin_Examples imports Main
11 text "Hex and bin numerals can be used like normal decimal numerals in input"
12 lemma "0xFF = 255" by (rule refl)
13 lemma "0xF = 0b1111" by (rule refl)
16 Just like decimal numeral they are polymorphic, for arithmetic
17 they need to be constrained
19 lemma "0x0A + 0x10 = (0x1A :: nat)" by simp
21 text "The number of leading zeros is irrelevant"
22 lemma "0b00010000 = 0x10" by (rule refl)
24 text "Unary minus works as for decimal numerals"
25 lemma "- 0x0A = - 10" by (rule refl)
28 Hex and bin numerals are printed as decimal: @{term "0b10"}
34 The numerals 0 and 1 are syntactically different from the
35 constants 0 and 1. For the usual numeric types, their values
41 lemma "0x01 = (1::nat)" by simp
42 lemma "0b0000 = (0::int)" by simp