src/HOL/ex/Hex_Bin_Examples.thy
author kleing
Fri Oct 06 03:49:36 2006 +0200 (2006-10-06)
changeset 20866 bc366b4b6ea4
child 41460 ea56b98aee83
permissions -rw-r--r--
examples for hex and bin numerals
     1 (*  Title:      HOL/ex/Hex_Bin_Examples.thy
     2     ID:         $Id$
     3     Author:     Gerwin Klein, NICTA
     4 *)
     5 
     6 header {* Examples for hexadecimal and binary numerals *}
     7 
     8 theory Hex_Bin_Examples imports Main 
     9 begin
    10 
    11 
    12 text "Hex and bin numerals can be used like normal decimal numerals in input"
    13 lemma "0xFF = 255" by (rule refl)
    14 lemma "0xF = 0b1111" by (rule refl)
    15 
    16 text {* 
    17   Just like decimal numeral they are polymorphic, for arithmetic 
    18   they need to be constrained
    19 *}
    20 lemma "0x0A + 0x10 = (0x1A :: nat)" by simp
    21 
    22 text "The number of leading zeros is irrelevant"
    23 lemma "0b00010000 = 0x10" by (rule refl) 
    24 
    25 text "Unary minus works as for decimal numerals"
    26 lemma "- 0x0A = - 10" by (rule refl)
    27 
    28 text {*
    29   Hex and bin numerals are printed as decimal: @{term "0b10"}
    30 *}
    31 term "0b10"
    32 term "0x0A"
    33 
    34 text {* 
    35   The numerals 0 and 1 are syntactically different from the 
    36   constants 0 and 1. For the usual numeric types, their values 
    37   are the same, though.
    38 *}
    39 lemma "0x01 = 1" oops 
    40 lemma "0x00 = 0" oops 
    41 
    42 lemma "0x01 = (1::nat)" by simp
    43 lemma "0b0000 = (0::int)" by simp
    44 
    45 
    46 end
    47