10213
|
1 |
(* Title: HOL/Wellfounded_Recursion.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Tobias Nipkow
|
|
4 |
Copyright 1992 University of Cambridge
|
|
5 |
|
|
6 |
Well-founded Recursion
|
|
7 |
*)
|
|
8 |
|
|
9 |
Wellfounded_Recursion = Transitive_Closure +
|
|
10 |
|
11328
|
11 |
consts
|
|
12 |
wfrec_rel :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => ('a * 'b) set"
|
|
13 |
|
|
14 |
inductive "wfrec_rel R F"
|
|
15 |
intrs
|
|
16 |
wfrecI "ALL z. (z, x) : R --> (z, g z) : wfrec_rel R F ==>
|
|
17 |
(x, F g x) : wfrec_rel R F"
|
|
18 |
|
10213
|
19 |
constdefs
|
|
20 |
wf :: "('a * 'a)set => bool"
|
|
21 |
"wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x. P(x)))"
|
|
22 |
|
|
23 |
acyclic :: "('a*'a)set => bool"
|
|
24 |
"acyclic r == !x. (x,x) ~: r^+"
|
|
25 |
|
|
26 |
cut :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b"
|
|
27 |
"cut f r x == (%y. if (y,x):r then f y else arbitrary)"
|
|
28 |
|
11328
|
29 |
adm_wf :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => bool"
|
|
30 |
"adm_wf R F == ALL f g x.
|
|
31 |
(ALL z. (z, x) : R --> f z = g z) --> F f x = F g x"
|
10213
|
32 |
|
11328
|
33 |
wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b"
|
|
34 |
"wfrec R F == %x. @y. (x, y) : wfrec_rel R (%f x. F (cut f R x) x)"
|
10213
|
35 |
|
11137
|
36 |
axclass
|
|
37 |
wellorder < linorder
|
|
38 |
wf "wf {(x,y::'a::ord). x<y}"
|
|
39 |
|
10213
|
40 |
end
|