isabelle: src/ZF/OrderType.thy@74e542a299f0 (annotated)

1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	1	(* Title: ZF/OrderType.thy
435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	2	ID: $Id$
1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	4	Copyright 1994 University of Cambridge
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	5
850 a744f9749885 Added constants Ord_alt, ++, ** lcp parents: 753 diff changeset	6	Order types and ordinal arithmetic.
435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	7
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	8	The order type of a well-ordering is the least ordinal isomorphic to it.
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	9	*)
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	10
2469 b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: 1478 diff changeset	11	OrderType = OrderArith + OrdQuant +
435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	12	consts
1401 0c439768f45c removed quotes from consts and syntax sections clasohm parents: 1033 diff changeset	13	ordermap :: [i,i]=>i
0c439768f45c removed quotes from consts and syntax sections clasohm parents: 1033 diff changeset	14	ordertype :: [i,i]=>i
435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	15
1401 0c439768f45c removed quotes from consts and syntax sections clasohm parents: 1033 diff changeset	16	Ord_alt :: i => o
850 a744f9749885 Added constants Ord_alt, ++, ** lcp parents: 753 diff changeset	17
1401 0c439768f45c removed quotes from consts and syntax sections clasohm parents: 1033 diff changeset	18	"**" :: [i,i]=>i (infixl 70)
0c439768f45c removed quotes from consts and syntax sections clasohm parents: 1033 diff changeset	19	"++" :: [i,i]=>i (infixl 65)
0c439768f45c removed quotes from consts and syntax sections clasohm parents: 1033 diff changeset	20	"--" :: [i,i]=>i (infixl 65)
850 a744f9749885 Added constants Ord_alt, ++, ** lcp parents: 753 diff changeset	21
a744f9749885 Added constants Ord_alt, ++, ** lcp parents: 753 diff changeset	22
753 ec86863e87c8 replaced "rules" by "defs" lcp parents: 467 diff changeset	23	defs
435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	24	ordermap_def
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	25	"ordermap(A,r) == lam x:A. wfrec[A](r, x, %x f. f `` pred(A,x,r))"
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	26
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	27	ordertype_def "ordertype(A,r) == ordermap(A,r)``A"
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	28
850 a744f9749885 Added constants Ord_alt, ++, ** lcp parents: 753 diff changeset	29	Ord_alt_def (alternative definition of ordinal numbers)
a744f9749885 Added constants Ord_alt, ++, ** lcp parents: 753 diff changeset	30	"Ord_alt(X) == well_ord(X, Memrel(X)) & (ALL u:X. u=pred(X, u, Memrel(X)))"
a744f9749885 Added constants Ord_alt, ++, ** lcp parents: 753 diff changeset	31
a744f9749885 Added constants Ord_alt, ++, ** lcp parents: 753 diff changeset	32	(ordinal multiplication)
a744f9749885 Added constants Ord_alt, ++, ** lcp parents: 753 diff changeset	33	omult_def "i ** j == ordertype(j*i, rmult(j,Memrel(j),i,Memrel(i)))"
a744f9749885 Added constants Ord_alt, ++, ** lcp parents: 753 diff changeset	34
a744f9749885 Added constants Ord_alt, ++, ** lcp parents: 753 diff changeset	35	(ordinal addition)
a744f9749885 Added constants Ord_alt, ++, ** lcp parents: 753 diff changeset	36	oadd_def "i ++ j == ordertype(i+j, radd(i,Memrel(i),j,Memrel(j)))"
a744f9749885 Added constants Ord_alt, ++, ** lcp parents: 753 diff changeset	37
1033 437728256de3 Defined ordinal difference, -- lcp parents: 850 diff changeset	38	(ordinal subtraction)
437728256de3 Defined ordinal difference, -- lcp parents: 850 diff changeset	39	odiff_def "i -- j == ordertype(i-j, Memrel(i))"
437728256de3 Defined ordinal difference, -- lcp parents: 850 diff changeset	40
9964 7966a2902266 tuned symbols; wenzelm parents: 9683 diff changeset	41	syntax (symbols)
7966a2902266 tuned symbols; wenzelm parents: 9683 diff changeset	42	"op **" :: [i,i] => i (infixl "\\<times>\\<times>" 70)
7966a2902266 tuned symbols; wenzelm parents: 9683 diff changeset	43
7966a2902266 tuned symbols; wenzelm parents: 9683 diff changeset	44	syntax (HTML output)
9683 f87c8c449018 added some xsymbols, and tidied paulson parents: 9654 diff changeset	45	"op **" :: [i,i] => i (infixl "\\<times>\\<times>" 70)
9654 9754ba005b64 X-symbols for ordinal, cardinal, integer arithmetic paulson parents: 2469 diff changeset	46
435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	47	end

author	wenzelm
	Mon, 04 Dec 2000 23:17:23 +0100
changeset 10581	74e542a299f0
parent 9964	7966a2902266
child 12114	a8e860c86252
permissions	-rw-r--r--