src/HOL/WF.thy
author wenzelm
Thu Mar 11 13:20:35 1999 +0100 (1999-03-11)
changeset 6349 f7750d816c21
parent 3947 eb707467f8c5
child 8882 9df44a4f1bf7
permissions -rw-r--r--
removed foo_build_completed -- now handled by session management (via usedir);
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
wenzelm@3947
    11
global
wenzelm@3947
    12
clasohm@1558
    13
constdefs
clasohm@1558
    14
  wf         :: "('a * 'a)set => bool"
wenzelm@3842
    15
  "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x. P(x)))"
clasohm@1558
    16
nipkow@3413
    17
  acyclic :: "('a*'a)set => bool"
nipkow@3413
    18
  "acyclic r == !x. (x,x) ~: r^+"
nipkow@3413
    19
clasohm@1558
    20
  cut        :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b"
nipkow@3320
    21
  "cut f r x == (%y. if (y,x):r then f y else arbitrary)"
clasohm@923
    22
clasohm@1558
    23
  is_recfun  :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) =>'a=>('a=>'b) => bool"
clasohm@1558
    24
  "is_recfun r H a f == (f = cut (%x. H (cut f r x) x) r a)"
clasohm@923
    25
clasohm@1558
    26
  the_recfun :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) => 'a => 'a => 'b"
clasohm@1558
    27
  "the_recfun r H a  == (@f. is_recfun r H a f)"
clasohm@923
    28
clasohm@1558
    29
  wfrec      :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) => 'a => 'b"
clasohm@1558
    30
  "wfrec r H == (%x. H (cut (the_recfun (trancl r) (%f v. H (cut f r v) v) x)
clasohm@1558
    31
                            r x)  x)"
clasohm@923
    32
wenzelm@3947
    33
local
wenzelm@3947
    34
clasohm@923
    35
end