|
0
|
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
|