author | nipkow |
Thu, 12 Oct 2000 18:38:23 +0200 | |
changeset 10212 | 33fe2d701ddd |
parent 8882 | 9df44a4f1bf7 |
permissions | -rw-r--r-- |
1475 | 1 |
(* Title: HOL/wf.ML |
923 | 2 |
ID: $Id$ |
1475 | 3 |
Author: Tobias Nipkow |
923 | 4 |
Copyright 1992 University of Cambridge |
5 |
||
6 |
Well-founded Recursion |
|
7 |
*) |
|
8 |
||
9 |
WF = Trancl + |
|
1558 | 10 |
|
11 |
constdefs |
|
12 |
wf :: "('a * 'a)set => bool" |
|
3842 | 13 |
"wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x. P(x)))" |
1558 | 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 | 18 |
cut :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b" |
3320 | 19 |
"cut f r x == (%y. if (y,x):r then f y else arbitrary)" |
923 | 20 |
|
1558 | 21 |
is_recfun :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) =>'a=>('a=>'b) => bool" |
22 |
"is_recfun r H a f == (f = cut (%x. H (cut f r x) x) r a)" |
|
923 | 23 |
|
1558 | 24 |
the_recfun :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) => 'a => 'a => 'b" |
25 |
"the_recfun r H a == (@f. is_recfun r H a f)" |
|
923 | 26 |
|
1558 | 27 |
wfrec :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) => 'a => 'b" |
28 |
"wfrec r H == (%x. H (cut (the_recfun (trancl r) (%f v. H (cut f r v) v) x) |
|
29 |
r x) x)" |
|
923 | 30 |
|
31 |
end |