src/CCL/Hered.thy
author clasohm
Thu, 16 Sep 1993 12:20:38 +0200
changeset 0 a5a9c433f639
child 1149 5750eba8820d
permissions -rw-r--r--
Initial revision
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	CCL/hered.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author: 	Martin Coen
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Hereditary Termination - cf. Martin Lo\"f
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
Note that this is based on an untyped equality and so lam x.b(x) is only 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
hereditarily terminating if ALL x.b(x) is.  Not so useful for functions!
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
Hered = Type +
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
consts
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
      (*** Predicates ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
  HTTgen     ::       "i set => i set"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
  HTT        ::       "i set"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
rules
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
  (*** Definitions of Hereditary Termination ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
  HTTgen_def 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
  "HTTgen(R) == {t. t=true | t=false | (EX a b.t=<a,b>      & a : R & b : R) | \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
\                                      (EX f.  t=lam x.f(x) & (ALL x.f(x) : R))}"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
  HTT_def       "HTT == gfp(HTTgen)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
end