Theory Hex_Bin_Examples

(*  Title:      HOL/ex/Hex_Bin_Examples.thy
    Author:     Gerwin Klein, NICTA
*)

section ‹Examples for hexadecimal and binary numerals›

theory Hex_Bin_Examples imports Main 
begin


text "Hex and bin numerals can be used like normal decimal numerals in input"
lemma "0xFF = 255" by (rule refl)
lemma "0xF = 0b1111" by (rule refl)

text ‹
  Just like decimal numeral they are polymorphic, for arithmetic 
  they need to be constrained
›
lemma "0x0A + 0x10 = (0x1A :: nat)" by simp

text "The number of leading zeros is irrelevant"
lemma "0b00010000 = 0x10" by (rule refl) 

text "Unary minus works as for decimal numerals"
lemma "- 0x0A = - 10" by (rule refl)

text ‹
  Hex and bin numerals are printed as decimal: \<^term>‹0b10›
›
term "0b10"
term "0x0A"

text ‹
  The numerals 0 and 1 are syntactically different from the 
  constants 0 and 1. For the usual numeric types, their values 
  are the same, though.
›
lemma "0x01 = 1" oops 
lemma "0x00 = 0" oops 

lemma "0x01 = (1::nat)" by simp
lemma "0b0000 = (0::int)" by simp


end