src/HOL/ex/Hex_Bin_Examples.thy
 author hoelzl Thu Jan 31 11:31:27 2013 +0100 (2013-01-31) changeset 50999 3de230ed0547 parent 41460 ea56b98aee83 child 58889 5b7a9633cfa8 permissions -rw-r--r--
introduce order topology
 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`