src/HOL/ex/Hex_Bin_Examples.thy
changeset 20866 bc366b4b6ea4
child 41460 ea56b98aee83
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/ex/Hex_Bin_Examples.thy	Fri Oct 06 03:49:36 2006 +0200
     1.3 @@ -0,0 +1,47 @@
     1.4 +(*  Title:      HOL/ex/Hex_Bin_Examples.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Gerwin Klein, NICTA
     1.7 +*)
     1.8 +
     1.9 +header {* Examples for hexadecimal and binary numerals *}
    1.10 +
    1.11 +theory Hex_Bin_Examples imports Main 
    1.12 +begin
    1.13 +
    1.14 +
    1.15 +text "Hex and bin numerals can be used like normal decimal numerals in input"
    1.16 +lemma "0xFF = 255" by (rule refl)
    1.17 +lemma "0xF = 0b1111" by (rule refl)
    1.18 +
    1.19 +text {* 
    1.20 +  Just like decimal numeral they are polymorphic, for arithmetic 
    1.21 +  they need to be constrained
    1.22 +*}
    1.23 +lemma "0x0A + 0x10 = (0x1A :: nat)" by simp
    1.24 +
    1.25 +text "The number of leading zeros is irrelevant"
    1.26 +lemma "0b00010000 = 0x10" by (rule refl) 
    1.27 +
    1.28 +text "Unary minus works as for decimal numerals"
    1.29 +lemma "- 0x0A = - 10" by (rule refl)
    1.30 +
    1.31 +text {*
    1.32 +  Hex and bin numerals are printed as decimal: @{term "0b10"}
    1.33 +*}
    1.34 +term "0b10"
    1.35 +term "0x0A"
    1.36 +
    1.37 +text {* 
    1.38 +  The numerals 0 and 1 are syntactically different from the 
    1.39 +  constants 0 and 1. For the usual numeric types, their values 
    1.40 +  are the same, though.
    1.41 +*}
    1.42 +lemma "0x01 = 1" oops 
    1.43 +lemma "0x00 = 0" oops 
    1.44 +
    1.45 +lemma "0x01 = (1::nat)" by simp
    1.46 +lemma "0b0000 = (0::int)" by simp
    1.47 +
    1.48 +
    1.49 +end
    1.50 +