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