equal
deleted
inserted
replaced
13 Note that this is based on an untyped equality and so @{text "lam |
13 Note that this is based on an untyped equality and so @{text "lam |
14 x. b(x)"} is only hereditarily terminating if @{text "ALL x. b(x)"} |
14 x. b(x)"} is only hereditarily terminating if @{text "ALL x. b(x)"} |
15 is. Not so useful for functions! |
15 is. Not so useful for functions! |
16 *} |
16 *} |
17 |
17 |
18 consts |
18 definition HTTgen :: "i set => i set" where |
19 (*** Predicates ***) |
19 "HTTgen(R) == |
20 HTTgen :: "i set => i set" |
20 {t. t=true | t=false | (EX a b. t= <a, b> & a : R & b : R) | |
21 HTT :: "i set" |
21 (EX f. t = lam x. f(x) & (ALL x. f(x) : R))}" |
22 |
22 |
23 axioms |
23 definition HTT :: "i set" |
24 (*** Definitions of Hereditary Termination ***) |
24 where "HTT == gfp(HTTgen)" |
25 |
|
26 HTTgen_def: |
|
27 "HTTgen(R) == {t. t=true | t=false | (EX a b. t=<a,b> & a : R & b : R) | |
|
28 (EX f. t=lam x. f(x) & (ALL x. f(x) : R))}" |
|
29 HTT_def: "HTT == gfp(HTTgen)" |
|
30 |
25 |
31 |
26 |
32 subsection {* Hereditary Termination *} |
27 subsection {* Hereditary Termination *} |
33 |
28 |
34 lemma HTTgen_mono: "mono(%X. HTTgen(X))" |
29 lemma HTTgen_mono: "mono(%X. HTTgen(X))" |