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