src/HOL/WF.thy
author clasohm
Fri, 08 Mar 1996 13:11:09 +0100
changeset 1558 9c6ebfab4e05
parent 1475 7f5a4cd08209
child 3320 3a5e4930fb77
permissions -rw-r--r--
added constdefs section
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1475
7f5a4cd08209 expanded tabs; renamed subtype to typedef;
clasohm
parents: 1276
diff changeset
     1
(*  Title:      HOL/wf.ML
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1475
7f5a4cd08209 expanded tabs; renamed subtype to typedef;
clasohm
parents: 1276
diff changeset
     3
    Author:     Tobias Nipkow
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     4
    Copyright   1992  University of Cambridge
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     5
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     6
Well-founded Recursion
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     7
*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     8
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     9
WF = Trancl +
1558
9c6ebfab4e05 added constdefs section
clasohm
parents: 1475
diff changeset
    10
9c6ebfab4e05 added constdefs section
clasohm
parents: 1475
diff changeset
    11
constdefs
9c6ebfab4e05 added constdefs section
clasohm
parents: 1475
diff changeset
    12
  wf         :: "('a * 'a)set => bool"
9c6ebfab4e05 added constdefs section
clasohm
parents: 1475
diff changeset
    13
  "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x.P(x)))"
9c6ebfab4e05 added constdefs section
clasohm
parents: 1475
diff changeset
    14
9c6ebfab4e05 added constdefs section
clasohm
parents: 1475
diff changeset
    15
  cut        :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b"
9c6ebfab4e05 added constdefs section
clasohm
parents: 1475
diff changeset
    16
  "cut f r x == (%y. if (y,x):r then f y else @z.True)"
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    17
1558
9c6ebfab4e05 added constdefs section
clasohm
parents: 1475
diff changeset
    18
  is_recfun  :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) =>'a=>('a=>'b) => bool"
9c6ebfab4e05 added constdefs section
clasohm
parents: 1475
diff changeset
    19
  "is_recfun r H a f == (f = cut (%x. H (cut f r x) x) r a)"
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    20
1558
9c6ebfab4e05 added constdefs section
clasohm
parents: 1475
diff changeset
    21
  the_recfun :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) => 'a => 'a => 'b"
9c6ebfab4e05 added constdefs section
clasohm
parents: 1475
diff changeset
    22
  "the_recfun r H a  == (@f. is_recfun r H a f)"
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    23
1558
9c6ebfab4e05 added constdefs section
clasohm
parents: 1475
diff changeset
    24
  wfrec      :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) => 'a => 'b"
9c6ebfab4e05 added constdefs section
clasohm
parents: 1475
diff changeset
    25
  "wfrec r H == (%x. H (cut (the_recfun (trancl r) (%f v. H (cut f r v) v) x)
9c6ebfab4e05 added constdefs section
clasohm
parents: 1475
diff changeset
    26
                            r x)  x)"
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    27
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    28
end