isabelle: src/HOL/Numeral.thy@b5b15bbca582 (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
12338 de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type"); wenzelm parents: 12098 diff changeset	17	number < type -- {* for numeric types: nat, int, real, \dots *}
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
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML; wenzelm parents: diff changeset	22	syntax
12098 784fe681ba26 use num_const of Pure; wenzelm parents: 11868 diff changeset	23	"_Numeral" :: "num_const => 'a" ("_")
11699 c7df55158574 "num" syntax; wenzelm parents: 11488 diff changeset	24	Numeral0 :: 'a
c7df55158574 "num" syntax; wenzelm parents: 11488 diff changeset	25	Numeral1 :: 'a
c7df55158574 "num" syntax; wenzelm parents: 11488 diff changeset	26
c7df55158574 "num" syntax; wenzelm parents: 11488 diff changeset	27	translations
c7df55158574 "num" syntax; wenzelm parents: 11488 diff changeset	28	"Numeral0" == "number_of Pls"
c7df55158574 "num" syntax; wenzelm parents: 11488 diff changeset	29	"Numeral1" == "number_of (Pls BIT True)"
11488 4ff900551340 constify numeral tokens in order to allow translations; wenzelm parents: 9410 diff changeset	30
6905 9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML; wenzelm parents: diff changeset	31
9035 371f023d3dbd removed explicit terminator (";"); wenzelm parents: 6988 diff changeset	32	setup NumeralSyntax.setup
6905 9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML; wenzelm parents: diff changeset	33
12738 9d80e3746eb0 symbolic syntax for x^2 (faills back on plain infix "^"); wenzelm parents: 12338 diff changeset	34	syntax (xsymbols)
9d80e3746eb0 symbolic syntax for x^2 (faills back on plain infix "^"); wenzelm parents: 12338 diff changeset	35	"_square" :: "'a => 'a" ("(_\<twosuperior>)" [1000] 999)
9d80e3746eb0 symbolic syntax for x^2 (faills back on plain infix "^"); wenzelm parents: 12338 diff changeset	36	syntax (HTML output)
9d80e3746eb0 symbolic syntax for x^2 (faills back on plain infix "^"); wenzelm parents: 12338 diff changeset	37	"_square" :: "'a => 'a" ("(_\<twosuperior>)" [1000] 999)
9d80e3746eb0 symbolic syntax for x^2 (faills back on plain infix "^"); wenzelm parents: 12338 diff changeset	38	syntax (output)
9d80e3746eb0 symbolic syntax for x^2 (faills back on plain infix "^"); wenzelm parents: 12338 diff changeset	39	"_square" :: "'a => 'a" ("(_ ^/ 2)" [81] 80)
9d80e3746eb0 symbolic syntax for x^2 (faills back on plain infix "^"); wenzelm parents: 12338 diff changeset	40	translations
9d80e3746eb0 symbolic syntax for x^2 (faills back on plain infix "^"); wenzelm parents: 12338 diff changeset	41	"x\<twosuperior>" == "x^2"
9d80e3746eb0 symbolic syntax for x^2 (faills back on plain infix "^"); wenzelm parents: 12338 diff changeset	42	"x\<twosuperior>" <= "x^(2::nat)"
11699 c7df55158574 "num" syntax; wenzelm parents: 11488 diff changeset	43
12738 9d80e3746eb0 symbolic syntax for x^2 (faills back on plain infix "^"); wenzelm parents: 12338 diff changeset	44
11699 c7df55158574 "num" syntax; wenzelm parents: 11488 diff changeset	45	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	46	-- {* Unfold all @{text let}s involving constants *}
11699 c7df55158574 "num" syntax; wenzelm parents: 11488 diff changeset	47	by (simp add: Let_def)
c7df55158574 "num" syntax; wenzelm parents: 11488 diff changeset	48
11868 56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite paulson parents: 11704 diff changeset	49	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	50	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	51
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite paulson parents: 11704 diff changeset	52	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	53	by (simp add: Let_def)
11699 c7df55158574 "num" syntax; wenzelm parents: 11488 diff changeset	54
9035 371f023d3dbd removed explicit terminator (";"); wenzelm parents: 6988 diff changeset	55	end

author	wenzelm
	Thu, 24 Jan 2002 16:37:49 +0100
changeset 12844	b5b15bbca582
parent 12738	9d80e3746eb0
child 13490	44bdc150211b
permissions	-rw-r--r--