isabelle: src/HOL/Numeral.thy@70f9158b6695 (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
13490 44bdc150211b Added Mi and Max on sets, hid Min and Pls on numerals. nipkow parents: 12738 diff changeset	11	(* The constructors Pls/Min are hidden in numeral_syntax.ML.
44bdc150211b Added Mi and Max on sets, hid Min and Pls on numerals. nipkow parents: 12738 diff changeset	12	Only qualified access bin.Pls/Min is allowed.
44bdc150211b Added Mi and Max on sets, hid Min and Pls on numerals. nipkow parents: 12738 diff changeset	13	Should also hide Bit, but that means one cannot use BIT anymore.
44bdc150211b Added Mi and Max on sets, hid Min and Pls on numerals. nipkow parents: 12738 diff changeset	14	*)
44bdc150211b Added Mi and Max on sets, hid Min and Pls on numerals. nipkow parents: 12738 diff changeset	15
6905 9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML; wenzelm parents: diff changeset	16	datatype
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML; wenzelm parents: diff changeset	17	bin = Pls
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML; wenzelm parents: diff changeset	18	\| Min
9358 973672495414 added syntax for proper / improper selector functions; wenzelm parents: 9035 diff changeset	19	\| Bit bin bool (infixl "BIT" 90)
6905 9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML; wenzelm parents: diff changeset	20
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML; wenzelm parents: diff changeset	21	axclass
12338 de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type"); wenzelm parents: 12098 diff changeset	22	number < type -- {* for numeric types: nat, int, real, \dots *}
6905 9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML; wenzelm parents: diff changeset	23
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML; wenzelm parents: diff changeset	24	consts
9035 371f023d3dbd removed explicit terminator (";"); wenzelm parents: 6988 diff changeset	25	number_of :: "bin => 'a::number"
6905 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	syntax
12098 784fe681ba26 use num_const of Pure; wenzelm parents: 11868 diff changeset	28	"_Numeral" :: "num_const => 'a" ("_")
11699 c7df55158574 "num" syntax; wenzelm parents: 11488 diff changeset	29	Numeral0 :: 'a
c7df55158574 "num" syntax; wenzelm parents: 11488 diff changeset	30	Numeral1 :: 'a
c7df55158574 "num" syntax; wenzelm parents: 11488 diff changeset	31
c7df55158574 "num" syntax; wenzelm parents: 11488 diff changeset	32	translations
13490 44bdc150211b Added Mi and Max on sets, hid Min and Pls on numerals. nipkow parents: 12738 diff changeset	33	"Numeral0" == "number_of bin.Pls"
44bdc150211b Added Mi and Max on sets, hid Min and Pls on numerals. nipkow parents: 12738 diff changeset	34	"Numeral1" == "number_of (bin.Pls BIT True)"
11488 4ff900551340 constify numeral tokens in order to allow translations; wenzelm parents: 9410 diff changeset	35
6905 9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML; wenzelm parents: diff changeset	36
9035 371f023d3dbd removed explicit terminator (";"); wenzelm parents: 6988 diff changeset	37	setup NumeralSyntax.setup
6905 9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML; wenzelm parents: diff changeset	38
12738 9d80e3746eb0 symbolic syntax for x^2 (faills back on plain infix "^"); wenzelm parents: 12338 diff changeset	39	syntax (xsymbols)
9d80e3746eb0 symbolic syntax for x^2 (faills back on plain infix "^"); wenzelm parents: 12338 diff changeset	40	"_square" :: "'a => 'a" ("(_\<twosuperior>)" [1000] 999)
9d80e3746eb0 symbolic syntax for x^2 (faills back on plain infix "^"); wenzelm parents: 12338 diff changeset	41	syntax (HTML output)
9d80e3746eb0 symbolic syntax for x^2 (faills back on plain infix "^"); wenzelm parents: 12338 diff changeset	42	"_square" :: "'a => 'a" ("(_\<twosuperior>)" [1000] 999)
9d80e3746eb0 symbolic syntax for x^2 (faills back on plain infix "^"); wenzelm parents: 12338 diff changeset	43	syntax (output)
9d80e3746eb0 symbolic syntax for x^2 (faills back on plain infix "^"); wenzelm parents: 12338 diff changeset	44	"_square" :: "'a => 'a" ("(_ ^/ 2)" [81] 80)
9d80e3746eb0 symbolic syntax for x^2 (faills back on plain infix "^"); wenzelm parents: 12338 diff changeset	45	translations
9d80e3746eb0 symbolic syntax for x^2 (faills back on plain infix "^"); wenzelm parents: 12338 diff changeset	46	"x\<twosuperior>" == "x^2"
9d80e3746eb0 symbolic syntax for x^2 (faills back on plain infix "^"); wenzelm parents: 12338 diff changeset	47	"x\<twosuperior>" <= "x^(2::nat)"
11699 c7df55158574 "num" syntax; wenzelm parents: 11488 diff changeset	48
12738 9d80e3746eb0 symbolic syntax for x^2 (faills back on plain infix "^"); wenzelm parents: 12338 diff changeset	49
11699 c7df55158574 "num" syntax; wenzelm parents: 11488 diff changeset	50	lemma Let_number_of [simp]: "Let (number_of v) f == f (number_of v)"
12738 9d80e3746eb0 symbolic syntax for x^2 (faills back on plain infix "^"); wenzelm parents: 12338 diff changeset	51	-- {* Unfold all @{text let}s involving constants *}
11699 c7df55158574 "num" syntax; wenzelm parents: 11488 diff changeset	52	by (simp add: Let_def)
c7df55158574 "num" syntax; wenzelm parents: 11488 diff changeset	53
11868 56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite paulson parents: 11704 diff changeset	54	lemma Let_0 [simp]: "Let 0 f == f 0"
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite paulson parents: 11704 diff changeset	55	by (simp add: Let_def)
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite paulson parents: 11704 diff changeset	56
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite paulson parents: 11704 diff changeset	57	lemma Let_1 [simp]: "Let 1 f == f 1"
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite paulson parents: 11704 diff changeset	58	by (simp add: Let_def)
11699 c7df55158574 "num" syntax; wenzelm parents: 11488 diff changeset	59
9035 371f023d3dbd removed explicit terminator (";"); wenzelm parents: 6988 diff changeset	60	end

author	paulson
	Mon, 05 May 2003 18:34:16 +0200
changeset 13960	70f9158b6695
parent 13490	44bdc150211b
child 14288	d149e3cbdb39
permissions	-rw-r--r--