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