src/HOL/Numeral.thy
author berghofe
Tue, 30 May 2000 18:02:49 +0200
changeset 9001 93af64f54bf2
parent 6988 eed63543a3af
child 9035 371f023d3dbd
permissions -rw-r--r--
the is now defined using primrec, avoiding explicit use of arbitrary.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6905
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
     1
(*  Title:      HOL/Numeral.thy
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
     3
    Author:     Larry Paulson and Markus Wenzel
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
     4
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
     5
Generic numerals represented as twos-complement bitstrings.
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
     6
*)
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
     7
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
     8
theory Numeral = Datatype
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
     9
files "Tools/numeral_syntax.ML":;
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    10
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    11
datatype
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    12
  bin = Pls
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    13
      | Min
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    14
      | Bit bin bool	(infixl "BIT" 90);
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    15
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    16
axclass
6988
eed63543a3af renamed sort "numeral" to "number"
paulson
parents: 6905
diff changeset
    17
  number < "term";      (*for numeric types: nat, int, real, ...*)
6905
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    18
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    19
consts
6988
eed63543a3af renamed sort "numeral" to "number"
paulson
parents: 6905
diff changeset
    20
  number_of :: "bin => 'a::number";
6905
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    21
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    22
syntax
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    23
  "_Numeral" :: "xnum => 'a"	("_");
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    24
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    25
setup NumeralSyntax.setup;
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    26
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    27
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    28
end;