src/CCL/fix.thy
author oheimb
Fri Jun 02 20:38:28 2000 +0200 (2000-06-02)
changeset 9028 8a1ec8f05f14
parent 0 a5a9c433f639
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