src/ZF/WF.thy
 author clasohm Sat Dec 09 13:36:11 1995 +0100 (1995-12-09 ago) changeset 1401 0c439768f45c parent 1155 928a16e02f9f child 1478 2b8c2a7547ab permissions -rw-r--r--
removed quotes from consts and syntax sections
 clasohm@0 1 (* Title: ZF/wf.thy clasohm@0 2 ID: \$Id\$ clasohm@0 3 Author: Tobias Nipkow and Lawrence C Paulson lcp@435 4 Copyright 1994 University of Cambridge clasohm@0 5 clasohm@0 6 Well-founded Recursion clasohm@0 7 *) clasohm@0 8 lcp@435 9 WF = Trancl + "mono" + "equalities" + clasohm@0 10 consts clasohm@1401 11 wf :: i=>o clasohm@1401 12 wf_on :: [i,i]=>o ("wf[_]'(_')") lcp@435 13 clasohm@1401 14 wftrec,wfrec :: [i, i, [i,i]=>i] =>i clasohm@1401 15 wfrec_on :: [i, i, i, [i,i]=>i] =>i ("wfrec[_]'(_,_,_')") clasohm@1401 16 is_recfun :: [i, i, [i,i]=>i, i] =>o clasohm@1401 17 the_recfun :: [i, i, [i,i]=>i] =>i clasohm@0 18 lcp@930 19 defs clasohm@0 20 (*r is a well-founded relation*) clasohm@0 21 wf_def "wf(r) == ALL Z. Z=0 | (EX x:Z. ALL y. :r --> ~ y:Z)" clasohm@0 22 lcp@435 23 (*r is well-founded relation over A*) lcp@435 24 wf_on_def "wf_on(A,r) == wf(r Int A*A)" lcp@435 25 clasohm@1155 26 is_recfun_def "is_recfun(r,a,H,f) == clasohm@1155 27 (f = (lam x: r-``{a}. H(x, restrict(f, r-``{x}))))" clasohm@0 28 clasohm@0 29 the_recfun_def "the_recfun(r,a,H) == (THE f.is_recfun(r,a,H,f))" clasohm@0 30 clasohm@0 31 wftrec_def "wftrec(r,a,H) == H(a, the_recfun(r,a,H))" clasohm@0 32 clasohm@0 33 (*public version. Does not require r to be transitive*) clasohm@0 34 wfrec_def "wfrec(r,a,H) == wftrec(r^+, a, %x f. H(x, restrict(f,r-``{x})))" clasohm@0 35 lcp@435 36 wfrec_on_def "wfrec[A](r,a,H) == wfrec(r Int A*A, a, H)" lcp@435 37 clasohm@0 38 end