|
1474
|
1 |
(* Title: CCL/Lazy/fix.thy
|
|
0
|
2 |
ID: $Id$
|
|
1474
|
3 |
Author: Martin Coen
|
|
0
|
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 |
|
|
1474
|
14 |
idgen :: "[i]=>i"
|
|
0
|
15 |
INCL :: "[i=>o]=>o"
|
|
|
16 |
|
|
|
17 |
rules
|
|
|
18 |
|
|
|
19 |
idgen_def
|
|
3837
|
20 |
"idgen(f) == lam t. case(t,true,false,%x y.<f`x, f`y>,%u. lam x. f ` u(x))"
|
|
0
|
21 |
|
|
3837
|
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)))"
|
|
0
|
25 |
|
|
|
26 |
end
|