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