examples for hex and bin numerals
authorkleing
Fri Oct 06 03:49:36 2006 +0200 (2006-10-06)
changeset 20866bc366b4b6ea4
parent 20865 2cfa020109c1
child 20867 e7b92a48e22b
examples for hex and bin numerals
src/HOL/IsaMakefile
src/HOL/ex/Hex_Bin_Examples.thy
src/HOL/ex/ROOT.ML
     1.1 --- a/src/HOL/IsaMakefile	Thu Oct 05 13:54:17 2006 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Oct 06 03:49:36 2006 +0200
     1.3 @@ -643,7 +643,7 @@
     1.4    ex/Abstract_NAT.thy ex/Antiquote.thy ex/BT.thy ex/BinEx.thy			\
     1.5    ex/Chinese.thy ex/Classical.thy ex/Classpackage.thy ex/CodeCollections.thy 	\
     1.6    ex/CodeEmbed.thy ex/CodeRandom.thy ex/CodeRevappl.thy			 	\
     1.7 -  ex/Codegenerator.thy ex/Commutative_RingEx.thy		               	\
     1.8 +  ex/Codegenerator.thy ex/Commutative_RingEx.thy ex/Hex_Bin_Examples.thy	\
     1.9    ex/Commutative_Ring_Complete.thy ex/Guess.thy ex/Hebrew.thy			\
    1.10    ex/Higher_Order_Logic.thy ex/Hilbert_Classical.thy ex/InSort.thy		\
    1.11    ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy			\
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/ex/Hex_Bin_Examples.thy	Fri Oct 06 03:49:36 2006 +0200
     2.3 @@ -0,0 +1,47 @@
     2.4 +(*  Title:      HOL/ex/Hex_Bin_Examples.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     Gerwin Klein, NICTA
     2.7 +*)
     2.8 +
     2.9 +header {* Examples for hexadecimal and binary numerals *}
    2.10 +
    2.11 +theory Hex_Bin_Examples imports Main 
    2.12 +begin
    2.13 +
    2.14 +
    2.15 +text "Hex and bin numerals can be used like normal decimal numerals in input"
    2.16 +lemma "0xFF = 255" by (rule refl)
    2.17 +lemma "0xF = 0b1111" by (rule refl)
    2.18 +
    2.19 +text {* 
    2.20 +  Just like decimal numeral they are polymorphic, for arithmetic 
    2.21 +  they need to be constrained
    2.22 +*}
    2.23 +lemma "0x0A + 0x10 = (0x1A :: nat)" by simp
    2.24 +
    2.25 +text "The number of leading zeros is irrelevant"
    2.26 +lemma "0b00010000 = 0x10" by (rule refl) 
    2.27 +
    2.28 +text "Unary minus works as for decimal numerals"
    2.29 +lemma "- 0x0A = - 10" by (rule refl)
    2.30 +
    2.31 +text {*
    2.32 +  Hex and bin numerals are printed as decimal: @{term "0b10"}
    2.33 +*}
    2.34 +term "0b10"
    2.35 +term "0x0A"
    2.36 +
    2.37 +text {* 
    2.38 +  The numerals 0 and 1 are syntactically different from the 
    2.39 +  constants 0 and 1. For the usual numeric types, their values 
    2.40 +  are the same, though.
    2.41 +*}
    2.42 +lemma "0x01 = 1" oops 
    2.43 +lemma "0x00 = 0" oops 
    2.44 +
    2.45 +lemma "0x01 = (1::nat)" by simp
    2.46 +lemma "0b0000 = (0::int)" by simp
    2.47 +
    2.48 +
    2.49 +end
    2.50 +
     3.1 --- a/src/HOL/ex/ROOT.ML	Thu Oct 05 13:54:17 2006 +0200
     3.2 +++ b/src/HOL/ex/ROOT.ML	Fri Oct 06 03:49:36 2006 +0200
     3.3 @@ -21,6 +21,7 @@
     3.4  time_use_thy "Records";
     3.5  time_use_thy "MonoidGroup";
     3.6  time_use_thy "BinEx";
     3.7 +time_use_thy "Hex_Bin_Examples";
     3.8  setmp proofs 2 time_use_thy "Hilbert_Classical";
     3.9  time_use_thy "Antiquote";
    3.10  time_use_thy "Multiquote";