isabelle: src/ZF/Rel.thy@53022e5f73ff (annotated)

1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	1	(* Title: ZF/Rel.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
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	6	Relations in Zermelo-Fraenkel Set Theory
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
13168 afcbca3498b0 converted domrange to Isar and merged with equalities paulson parents: 2469 diff changeset	9	Rel = equalities +
435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	10	consts
1401 0c439768f45c removed quotes from consts and syntax sections clasohm parents: 1155 diff changeset	11	refl,irrefl,equiv :: [i,i]=>o
0c439768f45c removed quotes from consts and syntax sections clasohm parents: 1155 diff changeset	12	sym,asym,antisym,trans :: i=>o
1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	13	trans_on :: [i,i]=>o ("trans[_]'(_')")
435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	14
753 ec86863e87c8 replaced "rules" by "defs" lcp parents: 435 diff changeset	15	defs
435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	16	refl_def "refl(A,r) == (ALL x: A. <x,x> : r)"
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	17
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	18	irrefl_def "irrefl(A,r) == ALL x: A. <x,x> ~: r"
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	19
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	20	sym_def "sym(r) == ALL x y. <x,y>: r --> <y,x>: r"
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	21
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	22	asym_def "asym(r) == ALL x y. <x,y>:r --> ~ <y,x>:r"
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	23
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	24	antisym_def "antisym(r) == ALL x y.<x,y>:r --> <y,x>:r --> x=y"
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	25
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	26	trans_def "trans(r) == ALL x y z. <x,y>: r --> <y,z>: r --> <x,z>: r"
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	27
1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	28	trans_on_def "trans[A](r) == ALL x:A. ALL y:A. ALL z:A.
1155 928a16e02f9f removed \...\ inside strings clasohm parents: 753 diff changeset	29	<x,y>: r --> <y,z>: r --> <x,z>: r"
435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	30
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	31	equiv_def "equiv(A,r) == r <= A*A & refl(A,r) & sym(r) & trans(r)"
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	32
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	33	end

author	wenzelm
	Wed, 05 Jun 2002 12:24:14 +0200
changeset 13202	53022e5f73ff
parent 13168	afcbca3498b0
child 13220	62c899c77151
permissions	-rw-r--r--