src/CCL/Hered.thy
author wenzelm
Sat Sep 17 17:35:26 2005 +0200 (2005-09-17)
changeset 17456 bcf7544875b2
parent 3837 d7f033c74b38
child 20140 98acc6d0fab6
permissions -rw-r--r--
converted to Isar theory format;
wenzelm@17456
     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
wenzelm@17456
     7
header {* Hereditary Termination -- cf. Martin Lo\"f *}
wenzelm@17456
     8
wenzelm@17456
     9
theory Hered
wenzelm@17456
    10
imports Type
wenzelm@17456
    11
uses "coinduction.ML"
wenzelm@17456
    12
begin
wenzelm@17456
    13
wenzelm@17456
    14
text {*
wenzelm@17456
    15
  Note that this is based on an untyped equality and so @{text "lam
wenzelm@17456
    16
  x. b(x)"} is only hereditarily terminating if @{text "ALL x. b(x)"}
wenzelm@17456
    17
  is.  Not so useful for functions!
wenzelm@17456
    18
*}
clasohm@0
    19
clasohm@0
    20
consts
clasohm@0
    21
      (*** Predicates ***)
clasohm@0
    22
  HTTgen     ::       "i set => i set"
clasohm@0
    23
  HTT        ::       "i set"
clasohm@0
    24
wenzelm@17456
    25
axioms
clasohm@0
    26
  (*** Definitions of Hereditary Termination ***)
clasohm@0
    27
wenzelm@17456
    28
  HTTgen_def:
wenzelm@17456
    29
  "HTTgen(R) == {t. t=true | t=false | (EX a b. t=<a,b>      & a : R & b : R) |
wenzelm@3837
    30
                                      (EX f.  t=lam x. f(x) & (ALL x. f(x) : R))}"
wenzelm@17456
    31
  HTT_def:       "HTT == gfp(HTTgen)"
wenzelm@17456
    32
wenzelm@17456
    33
ML {* use_legacy_bindings (the_context ()) *}
clasohm@0
    34
clasohm@0
    35
end