src/HOL/WF.thy
author clasohm
Mon Feb 05 21:27:16 1996 +0100 (1996-02-05)
changeset 1475 7f5a4cd08209
parent 1276 42ccfd3e1fb4
child 1558 9c6ebfab4e05
permissions -rw-r--r--
expanded tabs; renamed subtype to typedef;
incorporated Konrad's changes
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@923
    10
consts
clasohm@1475
    11
 wf         :: "('a * 'a)set => bool"
clasohm@1475
    12
 cut        :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b"
clasohm@1475
    13
 is_recfun  :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) =>'a=>('a=>'b) => bool"
clasohm@1475
    14
 the_recfun :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) => 'a => 'a => 'b"
clasohm@1475
    15
 wfrec      :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) => 'a => 'b"
clasohm@923
    16
clasohm@923
    17
defs
clasohm@972
    18
  wf_def  "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x.P(x)))"
clasohm@923
    19
  
clasohm@1475
    20
  cut_def        "cut f r x == (%y. if (y,x):r then f y else @z.True)"
clasohm@923
    21
clasohm@1475
    22
  is_recfun_def  "is_recfun r H a f == (f = cut (%x. H (cut f r x) x) r a)"
clasohm@923
    23
clasohm@1475
    24
  the_recfun_def "the_recfun r H a  == (@f. is_recfun r H a f)"
clasohm@923
    25
clasohm@1475
    26
  wfrec_def
clasohm@1475
    27
    "wfrec r H == (%x. H (cut (the_recfun (trancl r) (%f v. H (cut f r v) v) x)
clasohm@1475
    28
                              r x)  x)"
clasohm@923
    29
end