equal
deleted
inserted
replaced
1 (* Title: HOLCF/Coind.thy |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 Copyright 1993 Technische Universitaet Muenchen |
|
5 |
|
6 Example for co-induction on streams |
|
7 *) |
|
8 |
|
9 Coind = Stream2 + |
|
10 |
|
11 |
|
12 consts |
|
13 |
|
14 nats :: "dnat stream" |
|
15 from :: "dnat -> dnat stream" |
|
16 |
|
17 defs |
|
18 nats_def "nats == fix`(LAM h.scons`dzero`(smap`dsucc`h))" |
|
19 |
|
20 from_def "from == fix`(LAM h n.scons`n`(h`(dsucc`n)))" |
|
21 |
|
22 end |
|
23 |
|
24 (* |
|
25 smap`f`UU = UU |
|
26 x~=UU --> smap`f`(scons`x`xs) = scons`(f`x)`(smap`f`xs) |
|
27 |
|
28 nats = scons`dzero`(smap`dsucc`nats) |
|
29 |
|
30 from`n = scons`n`(from`(dsucc`n)) |
|
31 *) |
|
32 |
|
33 |
|