src/HOL/WF.thy
author berghofe
Tue, 30 May 2000 18:02:49 +0200
changeset 9001 93af64f54bf2
parent 8882 9df44a4f1bf7
permissions -rw-r--r--
the is now defined using primrec, avoiding explicit use of arbitrary.
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"
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3413
diff changeset
    13
  "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x. P(x)))"
1558
9c6ebfab4e05 added constdefs section
clasohm
parents: 1475
diff changeset
    14
3413
c1f63cc3a768 Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents: 3320
diff changeset
    15
  acyclic :: "('a*'a)set => bool"
c1f63cc3a768 Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents: 3320
diff changeset
    16
  "acyclic r == !x. (x,x) ~: r^+"
c1f63cc3a768 Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents: 3320
diff changeset
    17
1558
9c6ebfab4e05 added constdefs section
clasohm
parents: 1475
diff changeset
    18
  cut        :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b"
3320
3a5e4930fb77 Added `arbitrary'
nipkow
parents: 1558
diff changeset
    19
  "cut f r x == (%y. if (y,x):r then f y else arbitrary)"
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
  is_recfun  :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) =>'a=>('a=>'b) => bool"
9c6ebfab4e05 added constdefs section
clasohm
parents: 1475
diff changeset
    22
  "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
1558
9c6ebfab4e05 added constdefs section
clasohm
parents: 1475
diff changeset
    24
  the_recfun :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) => 'a => 'a => 'b"
9c6ebfab4e05 added constdefs section
clasohm
parents: 1475
diff changeset
    25
  "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
    26
1558
9c6ebfab4e05 added constdefs section
clasohm
parents: 1475
diff changeset
    27
  wfrec      :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) => 'a => 'b"
9c6ebfab4e05 added constdefs section
clasohm
parents: 1475
diff changeset
    28
  "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
    29
                            r x)  x)"
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    30
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    31
end