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