src/CCL/Fix.thy
author oheimb
Fri Jun 02 20:38:28 2000 +0200 (2000-06-02)
changeset 9028 8a1ec8f05f14
parent 3837 d7f033c74b38
child 17456 bcf7544875b2
permissions -rw-r--r--
added HOL/Prolog
     1 (*  Title:      CCL/Lazy/fix.thy
     2     ID:         $Id$
     3     Author:     Martin Coen
     4     Copyright   1993  University of Cambridge
     5 
     6 Tentative attempt at including fixed point induction.
     7 Justified by Smith.
     8 *)
     9 
    10 Fix = Type + 
    11 
    12 consts
    13 
    14   idgen      ::       "[i]=>i"
    15   INCL      :: "[i=>o]=>o"
    16 
    17 rules
    18 
    19   idgen_def
    20   "idgen(f) == lam t. case(t,true,false,%x y.<f`x, f`y>,%u. lam x. f ` u(x))"
    21 
    22   INCL_def   "INCL(%x. P(x)) == (ALL f.(ALL n:Nat. P(f^n`bot)) --> P(fix(f)))"
    23   po_INCL    "INCL(%x. a(x) [= b(x))"
    24   INCL_subst "INCL(P) ==> INCL(%x. P((g::i=>i)(x)))"
    25 
    26 end