isabelle: src/ZF/epsilon.thy@a5a9c433f639 (annotated)

0 a5a9c433f639 Initial revision clasohm parents: diff changeset	1	(* Title: ZF/epsilon.thy
a5a9c433f639 Initial revision clasohm parents: diff changeset	2	ID: $Id$
a5a9c433f639 Initial revision clasohm parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
a5a9c433f639 Initial revision clasohm parents: diff changeset	4	Copyright 1993 University of Cambridge
a5a9c433f639 Initial revision clasohm parents: diff changeset	5
a5a9c433f639 Initial revision clasohm parents: diff changeset	6	Epsilon induction and recursion
a5a9c433f639 Initial revision clasohm parents: diff changeset	7	*)
a5a9c433f639 Initial revision clasohm parents: diff changeset	8
a5a9c433f639 Initial revision clasohm parents: diff changeset	9	Epsilon = Nat +
a5a9c433f639 Initial revision clasohm parents: diff changeset	10	consts
a5a9c433f639 Initial revision clasohm parents: diff changeset	11	eclose,rank :: "i=>i"
a5a9c433f639 Initial revision clasohm parents: diff changeset	12	transrec :: "[i, [i,i]=>i] =>i"
a5a9c433f639 Initial revision clasohm parents: diff changeset	13
a5a9c433f639 Initial revision clasohm parents: diff changeset	14	rules
a5a9c433f639 Initial revision clasohm parents: diff changeset	15	eclose_def "eclose(A) == UN n:nat. nat_rec(n, A, %m r. Union(r))"
a5a9c433f639 Initial revision clasohm parents: diff changeset	16	transrec_def "transrec(a,H) == wfrec(Memrel(eclose({a})), a, H)"
a5a9c433f639 Initial revision clasohm parents: diff changeset	17	rank_def "rank(a) == transrec(a, %x f. UN y:x. succ(f`y))"
a5a9c433f639 Initial revision clasohm parents: diff changeset	18	end

author	clasohm
	Thu, 16 Sep 1993 12:20:38 +0200
changeset 0	a5a9c433f639
child 124	858ab9a9b047
permissions	-rw-r--r--