src/CCL/Fix.thy
changeset 0 a5a9c433f639
child 1474 3f7d67927fe2
equal deleted inserted replaced
-1:000000000000 0:a5a9c433f639
       
     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