src/HOL/ex/Hex_Bin_Examples.thy
author hoelzl
Thu Jan 31 11:31:27 2013 +0100 (2013-01-31)
changeset 50999 3de230ed0547
parent 41460 ea56b98aee83
child 58889 5b7a9633cfa8
permissions -rw-r--r--
introduce order topology
     1 (*  Title:      HOL/ex/Hex_Bin_Examples.thy
     2     Author:     Gerwin Klein, NICTA
     3 *)
     4 
     5 header {* Examples for hexadecimal and binary numerals *}
     6 
     7 theory Hex_Bin_Examples imports Main 
     8 begin
     9 
    10 
    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)
    14 
    15 text {* 
    16   Just like decimal numeral they are polymorphic, for arithmetic 
    17   they need to be constrained
    18 *}
    19 lemma "0x0A + 0x10 = (0x1A :: nat)" by simp
    20 
    21 text "The number of leading zeros is irrelevant"
    22 lemma "0b00010000 = 0x10" by (rule refl) 
    23 
    24 text "Unary minus works as for decimal numerals"
    25 lemma "- 0x0A = - 10" by (rule refl)
    26 
    27 text {*
    28   Hex and bin numerals are printed as decimal: @{term "0b10"}
    29 *}
    30 term "0b10"
    31 term "0x0A"
    32 
    33 text {* 
    34   The numerals 0 and 1 are syntactically different from the 
    35   constants 0 and 1. For the usual numeric types, their values 
    36   are the same, though.
    37 *}
    38 lemma "0x01 = 1" oops 
    39 lemma "0x00 = 0" oops 
    40 
    41 lemma "0x01 = (1::nat)" by simp
    42 lemma "0b0000 = (0::int)" by simp
    43 
    44 
    45 end
    46