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