src/CCL/Fix.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/Fix.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 {* Tentative attempt at including fixed point induction; justified by Smith *}
wenzelm@17456
     8
wenzelm@17456
     9
theory Fix
wenzelm@17456
    10
imports Type
wenzelm@17456
    11
begin
clasohm@0
    12
clasohm@0
    13
consts
clasohm@1474
    14
  idgen      ::       "[i]=>i"
clasohm@0
    15
  INCL      :: "[i=>o]=>o"
clasohm@0
    16
wenzelm@17456
    17
axioms
wenzelm@17456
    18
  idgen_def:
wenzelm@3837
    19
  "idgen(f) == lam t. case(t,true,false,%x y.<f`x, f`y>,%u. lam x. f ` u(x))"
clasohm@0
    20
wenzelm@17456
    21
  INCL_def:   "INCL(%x. P(x)) == (ALL f.(ALL n:Nat. P(f^n`bot)) --> P(fix(f)))"
wenzelm@17456
    22
  po_INCL:    "INCL(%x. a(x) [= b(x))"
wenzelm@17456
    23
  INCL_subst: "INCL(P) ==> INCL(%x. P((g::i=>i)(x)))"
wenzelm@17456
    24
wenzelm@17456
    25
ML {* use_legacy_bindings (the_context ()) *}
clasohm@0
    26
clasohm@0
    27
end