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`