Old_HOL: Nat.thy@fd1be45b64bf (annotated)

145 a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 109 diff changeset	1	(* Title: HOL/Nat.thy
0 7949f97df77a Initial revision clasohm parents: diff changeset	2	ID: $Id$
145 a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 109 diff changeset	3	Author: Tobias Nipkow, Cambridge University Computer Laboratory
0 7949f97df77a Initial revision clasohm parents: diff changeset	4	Copyright 1991 University of Cambridge
7949f97df77a Initial revision clasohm parents: diff changeset	5
7949f97df77a Initial revision clasohm parents: diff changeset	6	Definition of types ind and nat.
7949f97df77a Initial revision clasohm parents: diff changeset	7
7949f97df77a Initial revision clasohm parents: diff changeset	8	Type nat is defined as a set Nat over type ind.
7949f97df77a Initial revision clasohm parents: diff changeset	9	*)
7949f97df77a Initial revision clasohm parents: diff changeset	10
7949f97df77a Initial revision clasohm parents: diff changeset	11	Nat = WF +
51 934a58983311 new type declaration syntax instead of numbers lcp parents: 0 diff changeset	12
934a58983311 new type declaration syntax instead of numbers lcp parents: 0 diff changeset	13	types
934a58983311 new type declaration syntax instead of numbers lcp parents: 0 diff changeset	14	ind
934a58983311 new type declaration syntax instead of numbers lcp parents: 0 diff changeset	15	nat
934a58983311 new type declaration syntax instead of numbers lcp parents: 0 diff changeset	16
934a58983311 new type declaration syntax instead of numbers lcp parents: 0 diff changeset	17	arities
145 a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 109 diff changeset	18	ind, nat :: term
a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 109 diff changeset	19
a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 109 diff changeset	20	instance
a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 109 diff changeset	21	nat :: ord
0 7949f97df77a Initial revision clasohm parents: diff changeset	22
7949f97df77a Initial revision clasohm parents: diff changeset	23	consts
145 a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 109 diff changeset	24	Zero_Rep :: "ind"
a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 109 diff changeset	25	Suc_Rep :: "ind => ind"
a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 109 diff changeset	26	Nat :: "ind set"
a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 109 diff changeset	27	Rep_Nat :: "nat => ind"
a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 109 diff changeset	28	Abs_Nat :: "ind => nat"
a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 109 diff changeset	29	Suc :: "nat => nat"
a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 109 diff changeset	30	nat_case :: "['a, nat=>'a, nat] =>'a"
a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 109 diff changeset	31	pred_nat :: "(nat * nat) set"
a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 109 diff changeset	32	nat_rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a"
a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 109 diff changeset	33	"0" :: "nat" ("0")
0 7949f97df77a Initial revision clasohm parents: diff changeset	34
109 c53c19fb22cb HOL/Nat: rotated arguments of nat_case; added translation for case macro lcp parents: 94 diff changeset	35	translations
c53c19fb22cb HOL/Nat: rotated arguments of nat_case; added translation for case macro lcp parents: 94 diff changeset	36	"case p of 0 => a \| Suc(y) => b" == "nat_case(a, %y.b, p)"
c53c19fb22cb HOL/Nat: rotated arguments of nat_case; added translation for case macro lcp parents: 94 diff changeset	37
0 7949f97df77a Initial revision clasohm parents: diff changeset	38	rules
7949f97df77a Initial revision clasohm parents: diff changeset	39	(the axiom of infinity in 2 parts)
145 a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 109 diff changeset	40	inj_Suc_Rep "inj(Suc_Rep)"
a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 109 diff changeset	41	Suc_Rep_not_Zero_Rep "~(Suc_Rep(x) = Zero_Rep)"
a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 109 diff changeset	42	Nat_def "Nat == lfp(%X. {Zero_Rep} Un (Suc_Rep``X))"
0 7949f97df77a Initial revision clasohm parents: diff changeset	43	(faking a type definition...)
145 a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 109 diff changeset	44	Rep_Nat "Rep_Nat(n): Nat"
a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 109 diff changeset	45	Rep_Nat_inverse "Abs_Nat(Rep_Nat(n)) = n"
a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 109 diff changeset	46	Abs_Nat_inverse "i: Nat ==> Rep_Nat(Abs_Nat(i)) = i"
0 7949f97df77a Initial revision clasohm parents: diff changeset	47	(defining the abstract constants)
145 a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 109 diff changeset	48	Zero_def "0 == Abs_Nat(Zero_Rep)"
a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 109 diff changeset	49	Suc_def "Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))"
0 7949f97df77a Initial revision clasohm parents: diff changeset	50	(nat operations and recursion)
145 a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 109 diff changeset	51	nat_case_def "nat_case(a,f,n) == @z. (n=0 --> z=a) \
109 c53c19fb22cb HOL/Nat: rotated arguments of nat_case; added translation for case macro lcp parents: 94 diff changeset	52	\ & (!x. n=Suc(x) --> z=f(x))"
145 a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 109 diff changeset	53	pred_nat_def "pred_nat == {p. ? n. p = <n, Suc(n)>}"
0 7949f97df77a Initial revision clasohm parents: diff changeset	54
7949f97df77a Initial revision clasohm parents: diff changeset	55	less_def "m<n == <m,n>:trancl(pred_nat)"
7949f97df77a Initial revision clasohm parents: diff changeset	56
90 5c7a69cef18b added parentheses made necessary by change of constrain's precedence clasohm parents: 51 diff changeset	57	le_def "m<=(n::nat) == ~(n<m)"
0 7949f97df77a Initial revision clasohm parents: diff changeset	58
145 a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 109 diff changeset	59	nat_rec_def "nat_rec(n,c,d) == wfrec(pred_nat, n, \
109 c53c19fb22cb HOL/Nat: rotated arguments of nat_case; added translation for case macro lcp parents: 94 diff changeset	60	\ nat_case(%g.c, %m g. d(m,g(m))))"
0 7949f97df77a Initial revision clasohm parents: diff changeset	61	end
145 a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 109 diff changeset	62

author	clasohm
	Wed, 02 Nov 1994 11:50:09 +0100
changeset 156	fd1be45b64bf
parent 145	a9f7ff3a464c
child 185	8325414a370a
permissions	-rw-r--r--