|
0
|
1 |
(* Title: CCL/hered.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Martin Coen
|
|
|
4 |
Copyright 1993 University of Cambridge
|
|
|
5 |
|
|
|
6 |
Hereditary Termination - cf. Martin Lo\"f
|
|
|
7 |
|
|
|
8 |
Note that this is based on an untyped equality and so lam x.b(x) is only
|
|
|
9 |
hereditarily terminating if ALL x.b(x) is. Not so useful for functions!
|
|
|
10 |
|
|
|
11 |
*)
|
|
|
12 |
|
|
|
13 |
Hered = Type +
|
|
|
14 |
|
|
|
15 |
consts
|
|
|
16 |
(*** Predicates ***)
|
|
|
17 |
HTTgen :: "i set => i set"
|
|
|
18 |
HTT :: "i set"
|
|
|
19 |
|
|
|
20 |
|
|
|
21 |
rules
|
|
|
22 |
|
|
|
23 |
(*** Definitions of Hereditary Termination ***)
|
|
|
24 |
|
|
|
25 |
HTTgen_def
|
|
|
26 |
"HTTgen(R) == {t. t=true | t=false | (EX a b.t=<a,b> & a : R & b : R) | \
|
|
|
27 |
\ (EX f. t=lam x.f(x) & (ALL x.f(x) : R))}"
|
|
|
28 |
HTT_def "HTT == gfp(HTTgen)"
|
|
|
29 |
|
|
|
30 |
end
|