src/HOL/WF.thy
author wenzelm
Thu May 18 11:43:57 2000 +0200 (2000-05-18)
changeset 8882 9df44a4f1bf7
parent 3947 eb707467f8c5
permissions -rw-r--r--
fewer consts declared as global;
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"
wenzelm@3842
    13
  "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x. P(x)))"
clasohm@1558
    14
nipkow@3413
    15
  acyclic :: "('a*'a)set => bool"
nipkow@3413
    16
  "acyclic r == !x. (x,x) ~: r^+"
nipkow@3413
    17
clasohm@1558
    18
  cut        :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b"
nipkow@3320
    19
  "cut f r x == (%y. if (y,x):r then f y else arbitrary)"
clasohm@923
    20
clasohm@1558
    21
  is_recfun  :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) =>'a=>('a=>'b) => bool"
clasohm@1558
    22
  "is_recfun r H a f == (f = cut (%x. H (cut f r x) x) r a)"
clasohm@923
    23
clasohm@1558
    24
  the_recfun :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) => 'a => 'a => 'b"
clasohm@1558
    25
  "the_recfun r H a  == (@f. is_recfun r H a f)"
clasohm@923
    26
clasohm@1558
    27
  wfrec      :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) => 'a => 'b"
clasohm@1558
    28
  "wfrec r H == (%x. H (cut (the_recfun (trancl r) (%f v. H (cut f r v) v) x)
clasohm@1558
    29
                            r x)  x)"
clasohm@923
    30
clasohm@923
    31
end