src/CCL/hered.thy
author paulson
Fri Feb 16 17:24:51 1996 +0100 (1996-02-16)
changeset 1511 09354d37a5ab
parent 0 a5a9c433f639
permissions -rw-r--r--
Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.
clasohm@0
     1
(*  Title: 	CCL/hered.thy
clasohm@0
     2
    ID:         $Id$
clasohm@0
     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@0
    26
  "HTTgen(R) == {t. t=true | t=false | (EX a b.t=<a,b>      & a : R & b : R) | \
clasohm@0
    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