isabelle: src/HOL/Numeral.thy@85b3735a51e1 (annotated)

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
9410 612ee826a409 removed selector syntax -- improper tuples are broken beyond repair :-( wenzelm parents: 9358 diff changeset	5	Generic numerals represented as twos-complement bit strings.
6905 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
9035 371f023d3dbd removed explicit terminator (";"); wenzelm parents: 6988 diff changeset	9	files "Tools/numeral_syntax.ML":
6905 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
9358 973672495414 added syntax for proper / improper selector functions; wenzelm parents: 9035 diff changeset	14	\| Bit bin bool (infixl "BIT" 90)
6905 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
9035 371f023d3dbd removed explicit terminator (";"); wenzelm parents: 6988 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
9035 371f023d3dbd removed explicit terminator (";"); wenzelm parents: 6988 diff changeset	20	number_of :: "bin => 'a::number"
6905 9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML; wenzelm parents: diff changeset	21
11488 4ff900551340 constify numeral tokens in order to allow translations; wenzelm parents: 9410 diff changeset	22	nonterminals
4ff900551340 constify numeral tokens in order to allow translations; wenzelm parents: 9410 diff changeset	23	numeral
4ff900551340 constify numeral tokens in order to allow translations; wenzelm parents: 9410 diff changeset	24
6905 9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML; wenzelm parents: diff changeset	25	syntax
11699 c7df55158574 "num" syntax; wenzelm parents: 11488 diff changeset	26	"_constify" :: "num => numeral" ("_")
11704 3c50a2cd6f00 * sane numerals (stage 2): plain "num" syntax (removed "#"); wenzelm parents: 11699 diff changeset	27	"_Numeral" :: "numeral => 'a" ("_")
11699 c7df55158574 "num" syntax; wenzelm parents: 11488 diff changeset	28	Numeral0 :: 'a
c7df55158574 "num" syntax; wenzelm parents: 11488 diff changeset	29	Numeral1 :: 'a
c7df55158574 "num" syntax; wenzelm parents: 11488 diff changeset	30
c7df55158574 "num" syntax; wenzelm parents: 11488 diff changeset	31	translations
c7df55158574 "num" syntax; wenzelm parents: 11488 diff changeset	32	"Numeral0" == "number_of Pls"
c7df55158574 "num" syntax; wenzelm parents: 11488 diff changeset	33	"Numeral1" == "number_of (Pls BIT True)"
11488 4ff900551340 constify numeral tokens in order to allow translations; wenzelm parents: 9410 diff changeset	34
6905 9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML; wenzelm parents: diff changeset	35
9035 371f023d3dbd removed explicit terminator (";"); wenzelm parents: 6988 diff changeset	36	setup NumeralSyntax.setup
6905 9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML; wenzelm parents: diff changeset	37
11699 c7df55158574 "num" syntax; wenzelm parents: 11488 diff changeset	38
c7df55158574 "num" syntax; wenzelm parents: 11488 diff changeset	39	(Unfold all "let"s involving constants)
c7df55158574 "num" syntax; wenzelm parents: 11488 diff changeset	40	lemma Let_number_of [simp]: "Let (number_of v) f == f (number_of v)"
c7df55158574 "num" syntax; wenzelm parents: 11488 diff changeset	41	by (simp add: Let_def)
c7df55158574 "num" syntax; wenzelm parents: 11488 diff changeset	42
c7df55158574 "num" syntax; wenzelm parents: 11488 diff changeset	43	(*The condition "True" is a hack to prevent looping.
c7df55158574 "num" syntax; wenzelm parents: 11488 diff changeset	44	Conditional rewrite rules are tried after unconditional ones, so a rule
c7df55158574 "num" syntax; wenzelm parents: 11488 diff changeset	45	like eq_nat_number_of will be tried first to eliminate #mm=#nn. *)
c7df55158574 "num" syntax; wenzelm parents: 11488 diff changeset	46	lemma number_of_reorient [simp]: "True ==> (number_of w = x) = (x = number_of w)"
c7df55158574 "num" syntax; wenzelm parents: 11488 diff changeset	47	by auto
c7df55158574 "num" syntax; wenzelm parents: 11488 diff changeset	48
9035 371f023d3dbd removed explicit terminator (";"); wenzelm parents: 6988 diff changeset	49	end

author	kleing
	Mon, 15 Oct 2001 21:04:32 +0200
changeset 11787	85b3735a51e1
parent 11704	3c50a2cd6f00
child 11868	56db9f3a6b3e
permissions	-rw-r--r--