src/HOL/ex/Hex_Bin_Examples.thy
author wenzelm
Tue Oct 06 17:47:28 2015 +0200 (2015-10-06)
changeset 61343 5b5656a63bd6
parent 58889 5b7a9633cfa8
child 69597 ff784d5a5bfb
permissions -rw-r--r--
isabelle update_cartouches;
kleing@20866
     1
(*  Title:      HOL/ex/Hex_Bin_Examples.thy
kleing@20866
     2
    Author:     Gerwin Klein, NICTA
kleing@20866
     3
*)
kleing@20866
     4
wenzelm@61343
     5
section \<open>Examples for hexadecimal and binary numerals\<close>
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
wenzelm@61343
    15
text \<open>
kleing@20866
    16
  Just like decimal numeral they are polymorphic, for arithmetic 
kleing@20866
    17
  they need to be constrained
wenzelm@61343
    18
\<close>
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
wenzelm@61343
    27
text \<open>
kleing@20866
    28
  Hex and bin numerals are printed as decimal: @{term "0b10"}
wenzelm@61343
    29
\<close>
kleing@20866
    30
term "0b10"
kleing@20866
    31
term "0x0A"
kleing@20866
    32
wenzelm@61343
    33
text \<open>
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.
wenzelm@61343
    37
\<close>
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