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