src/HOL/WF.thy
author nipkow
Tue Apr 08 10:48:42 1997 +0200 (1997-04-08)
changeset 2919 953a47dc0519
parent 1558 9c6ebfab4e05
child 3320 3a5e4930fb77
permissions -rw-r--r--
Dep. on Provers/nat_transitive
clasohm@1475
     1
(*  Title:      HOL/wf.ML
clasohm@923
     2
    ID:         $Id$
clasohm@1475
     3
    Author:     Tobias Nipkow
clasohm@923
     4
    Copyright   1992  University of Cambridge
clasohm@923
     5
clasohm@923
     6
Well-founded Recursion
clasohm@923
     7
*)
clasohm@923
     8
clasohm@923
     9
WF = Trancl +
clasohm@1558
    10
clasohm@1558
    11
constdefs
clasohm@1558
    12
  wf         :: "('a * 'a)set => bool"
clasohm@1558
    13
  "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x.P(x)))"
clasohm@1558
    14
clasohm@1558
    15
  cut        :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b"
clasohm@1558
    16
  "cut f r x == (%y. if (y,x):r then f y else @z.True)"
clasohm@923
    17
clasohm@1558
    18
  is_recfun  :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) =>'a=>('a=>'b) => bool"
clasohm@1558
    19
  "is_recfun r H a f == (f = cut (%x. H (cut f r x) x) r a)"
clasohm@923
    20
clasohm@1558
    21
  the_recfun :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) => 'a => 'a => 'b"
clasohm@1558
    22
  "the_recfun r H a  == (@f. is_recfun r H a f)"
clasohm@923
    23
clasohm@1558
    24
  wfrec      :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) => 'a => 'b"
clasohm@1558
    25
  "wfrec r H == (%x. H (cut (the_recfun (trancl r) (%f v. H (cut f r v) v) x)
clasohm@1558
    26
                            r x)  x)"
clasohm@923
    27
clasohm@923
    28
end