src/HOL/ex/Hex_Bin_Examples.thy
 author haftmann Fri Oct 10 19:55:32 2014 +0200 (2014-10-10) changeset 58646 cd63a4b12a33 parent 41460 ea56b98aee83 child 58889 5b7a9633cfa8 permissions -rw-r--r--
specialized specification: avoid trivial instances
 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