- Installed specific code generator for equality enforcing that
arguments do not have function types, which would result in
an error message during compilation.
- Added test case generators for basic types.
(* Title: HOL/Numeral.thy
ID: $Id$
Author: Larry Paulson and Markus Wenzel
Generic numerals represented as twos-complement bit strings.
*)
theory Numeral = Datatype
files "Tools/numeral_syntax.ML":
(* The constructors Pls/Min are hidden in numeral_syntax.ML.
Only qualified access bin.Pls/Min is allowed.
Should also hide Bit, but that means one cannot use BIT anymore.
*)
datatype
bin = Pls
| Min
| Bit bin bool (infixl "BIT" 90)
axclass
number < type -- {* for numeric types: nat, int, real, \dots *}
consts
number_of :: "bin => 'a::number"
syntax
"_Numeral" :: "num_const => 'a" ("_")
Numeral0 :: 'a
Numeral1 :: 'a
translations
"Numeral0" == "number_of bin.Pls"
"Numeral1" == "number_of (bin.Pls BIT True)"
setup NumeralSyntax.setup
syntax (xsymbols)
"_square" :: "'a => 'a" ("(_\<twosuperior>)" [1000] 999)
syntax (HTML output)
"_square" :: "'a => 'a" ("(_\<twosuperior>)" [1000] 999)
syntax (output)
"_square" :: "'a => 'a" ("(_ ^/ 2)" [81] 80)
translations
"x\<twosuperior>" == "x^2"
"x\<twosuperior>" <= "x^(2::nat)"
lemma Let_number_of [simp]: "Let (number_of v) f == f (number_of v)"
-- {* Unfold all @{text let}s involving constants *}
by (simp add: Let_def)
lemma Let_0 [simp]: "Let 0 f == f 0"
by (simp add: Let_def)
lemma Let_1 [simp]: "Let 1 f == f 1"
by (simp add: Let_def)
end