src/HOL/ex/Hex_Bin_Examples.thy
 author wenzelm Tue Oct 06 17:47:28 2015 +0200 (2015-10-06) changeset 61343 5b5656a63bd6 parent 58889 5b7a9633cfa8 child 69597 ff784d5a5bfb permissions -rw-r--r--
isabelle update_cartouches;
 kleing@20866 ` 1` ```(* Title: HOL/ex/Hex_Bin_Examples.thy ``` kleing@20866 ` 2` ``` Author: Gerwin Klein, NICTA ``` kleing@20866 ` 3` ```*) ``` kleing@20866 ` 4` wenzelm@61343 ` 5` ```section \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` wenzelm@61343 ` 15` ```text \ ``` kleing@20866 ` 16` ``` Just like decimal numeral they are polymorphic, for arithmetic ``` kleing@20866 ` 17` ``` they need to be constrained ``` wenzelm@61343 ` 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` wenzelm@61343 ` 27` ```text \ ``` kleing@20866 ` 28` ``` Hex and bin numerals are printed as decimal: @{term "0b10"} ``` wenzelm@61343 ` 29` ```\ ``` kleing@20866 ` 30` ```term "0b10" ``` kleing@20866 ` 31` ```term "0x0A" ``` kleing@20866 ` 32` wenzelm@61343 ` 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. ``` wenzelm@61343 ` 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`