equal
deleted
inserted
replaced
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 |
|