src/CCL/Hered.thy
author clasohm
Mon Feb 05 14:44:09 1996 +0100 (1996-02-05)
changeset 1474 3f7d67927fe2
parent 1149 5750eba8820d
child 3837 d7f033c74b38
permissions -rw-r--r--
expanded tabs
clasohm@1474
     1
(*  Title:      CCL/hered.thy
clasohm@0
     2
    ID:         $Id$
clasohm@1474
     3
    Author:     Martin Coen
clasohm@0
     4
    Copyright   1993  University of Cambridge
clasohm@0
     5
clasohm@0
     6
Hereditary Termination - cf. Martin Lo\"f
clasohm@0
     7
clasohm@0
     8
Note that this is based on an untyped equality and so lam x.b(x) is only 
clasohm@0
     9
hereditarily terminating if ALL x.b(x) is.  Not so useful for functions!
clasohm@0
    10
clasohm@0
    11
*)
clasohm@0
    12
clasohm@0
    13
Hered = Type +
clasohm@0
    14
clasohm@0
    15
consts
clasohm@0
    16
      (*** Predicates ***)
clasohm@0
    17
  HTTgen     ::       "i set => i set"
clasohm@0
    18
  HTT        ::       "i set"
clasohm@0
    19
clasohm@0
    20
clasohm@0
    21
rules
clasohm@0
    22
clasohm@0
    23
  (*** Definitions of Hereditary Termination ***)
clasohm@0
    24
clasohm@0
    25
  HTTgen_def 
clasohm@1149
    26
  "HTTgen(R) == {t. t=true | t=false | (EX a b.t=<a,b>      & a : R & b : R) | 
clasohm@1149
    27
                                      (EX f.  t=lam x.f(x) & (ALL x.f(x) : R))}"
clasohm@0
    28
  HTT_def       "HTT == gfp(HTTgen)"
clasohm@0
    29
clasohm@0
    30
end