equal
deleted
inserted
replaced
|
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 |