diff -r 000000000000 -r a5a9c433f639 src/CCL/Fix.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/CCL/Fix.thy Thu Sep 16 12:20:38 1993 +0200 @@ -0,0 +1,26 @@ +(* 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.,%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