1474

1 
(* Title: CCL/hered.thy

0

2 
ID: $Id$

1474

3 
Author: Martin Coen

0

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

1149

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))}"

0

28 
HTT_def "HTT == gfp(HTTgen)"


29 


30 
end
