# HG changeset patch
# User kleing
# Date 1160099376 -7200
# Node ID bc366b4b6ea42c430788fce334d6378727db027f
# Parent  2cfa020109c1958d900b7e0d9656be24b3d1bd44
examples for hex and bin numerals

diff -r 2cfa020109c1 -r bc366b4b6ea4 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Oct 05 13:54:17 2006 +0200
+++ b/src/HOL/IsaMakefile	Fri Oct 06 03:49:36 2006 +0200
@@ -643,7 +643,7 @@
   ex/Abstract_NAT.thy ex/Antiquote.thy ex/BT.thy ex/BinEx.thy			\
   ex/Chinese.thy ex/Classical.thy ex/Classpackage.thy ex/CodeCollections.thy 	\
   ex/CodeEmbed.thy ex/CodeRandom.thy ex/CodeRevappl.thy			 	\
-  ex/Codegenerator.thy ex/Commutative_RingEx.thy		               	\
+  ex/Codegenerator.thy ex/Commutative_RingEx.thy ex/Hex_Bin_Examples.thy	\
   ex/Commutative_Ring_Complete.thy ex/Guess.thy ex/Hebrew.thy			\
   ex/Higher_Order_Logic.thy ex/Hilbert_Classical.thy ex/InSort.thy		\
   ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy			\
diff -r 2cfa020109c1 -r bc366b4b6ea4 src/HOL/ex/Hex_Bin_Examples.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Hex_Bin_Examples.thy	Fri Oct 06 03:49:36 2006 +0200
@@ -0,0 +1,47 @@
+(*  Title:      HOL/ex/Hex_Bin_Examples.thy
+    ID:         $Id$
+    Author:     Gerwin Klein, NICTA
+*)
+
+header {* Examples for hexadecimal and binary numerals *}
+
+theory Hex_Bin_Examples imports Main 
+begin
+
+
+text "Hex and bin numerals can be used like normal decimal numerals in input"
+lemma "0xFF = 255" by (rule refl)
+lemma "0xF = 0b1111" by (rule refl)
+
+text {* 
+  Just like decimal numeral they are polymorphic, for arithmetic 
+  they need to be constrained
+*}
+lemma "0x0A + 0x10 = (0x1A :: nat)" by simp
+
+text "The number of leading zeros is irrelevant"
+lemma "0b00010000 = 0x10" by (rule refl) 
+
+text "Unary minus works as for decimal numerals"
+lemma "- 0x0A = - 10" by (rule refl)
+
+text {*
+  Hex and bin numerals are printed as decimal: @{term "0b10"}
+*}
+term "0b10"
+term "0x0A"
+
+text {* 
+  The numerals 0 and 1 are syntactically different from the 
+  constants 0 and 1. For the usual numeric types, their values 
+  are the same, though.
+*}
+lemma "0x01 = 1" oops 
+lemma "0x00 = 0" oops 
+
+lemma "0x01 = (1::nat)" by simp
+lemma "0b0000 = (0::int)" by simp
+
+
+end
+
diff -r 2cfa020109c1 -r bc366b4b6ea4 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Thu Oct 05 13:54:17 2006 +0200
+++ b/src/HOL/ex/ROOT.ML	Fri Oct 06 03:49:36 2006 +0200
@@ -21,6 +21,7 @@
 time_use_thy "Records";
 time_use_thy "MonoidGroup";
 time_use_thy "BinEx";
+time_use_thy "Hex_Bin_Examples";
 setmp proofs 2 time_use_thy "Hilbert_Classical";
 time_use_thy "Antiquote";
 time_use_thy "Multiquote";