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
