author | clasohm |
Mon, 05 Feb 1996 14:44:09 +0100 | |
changeset 1474 | 3f7d67927fe2 |
parent 0 | a5a9c433f639 |
child 3837 | d7f033c74b38 |
permissions | -rw-r--r-- |
(* Title: CCL/Lazy/fix.thy ID: $Id$ Author: Martin Coen Copyright 1993 University of Cambridge Tentative attempt at including fixed point induction. Justified by Smith. *) Fix = Type + consts idgen :: "[i]=>i" INCL :: "[i=>o]=>o" rules idgen_def "idgen(f) == lam t.case(t,true,false,%x y.<f`x, f`y>,%u.lam x.f ` u(x))" INCL_def "INCL(%x.P(x)) == (ALL f.(ALL n:Nat.P(f^n`bot)) --> P(fix(f)))" po_INCL "INCL(%x.a(x) [= b(x))" INCL_subst "INCL(P) ==> INCL(%x.P((g::i=>i)(x)))" end