src/CCL/Hered.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/CCL/Hered.thy	Thu Sep 16 12:20:38 1993 +0200
@@ -0,0 +1,30 @@
+(*  Title: 	CCL/hered.thy
+    ID:         $Id$
+    Author: 	Martin Coen
+    Copyright   1993  University of Cambridge
+
+Hereditary Termination - cf. Martin Lo\"f
+
+Note that this is based on an untyped equality and so lam x.b(x) is only 
+hereditarily terminating if ALL x.b(x) is.  Not so useful for functions!
+
+*)
+
+Hered = Type +
+
+consts
+      (*** Predicates ***)
+  HTTgen     ::       "i set => i set"
+  HTT        ::       "i set"
+
+
+rules
+
+  (*** Definitions of Hereditary Termination ***)
+
+  HTTgen_def 
+  "HTTgen(R) == {t. t=true | t=false | (EX a b.t=<a,b>      & a : R & b : R) | \
+\                                      (EX f.  t=lam x.f(x) & (ALL x.f(x) : R))}"
+  HTT_def       "HTT == gfp(HTTgen)"
+
+end