equal
deleted
inserted
replaced
1 (* Title: HOLCF/stream2.ML |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 Copyright 1993 Technische Universitaet Muenchen |
|
5 |
|
6 Lemmas for theory Stream2.thy |
|
7 *) |
|
8 |
|
9 open Stream2; |
|
10 |
|
11 (* ------------------------------------------------------------------------- *) |
|
12 (* expand fixed point properties *) |
|
13 (* ------------------------------------------------------------------------- *) |
|
14 |
|
15 val smap_def2 = fix_prover2 Stream2.thy smap_def |
|
16 "smap = (LAM f s. stream_when`(LAM x l.scons`(f`x) `(smap`f`l)) `s)"; |
|
17 |
|
18 |
|
19 (* ------------------------------------------------------------------------- *) |
|
20 (* recursive properties *) |
|
21 (* ------------------------------------------------------------------------- *) |
|
22 |
|
23 |
|
24 qed_goal "smap1" Stream2.thy "smap`f`UU = UU" |
|
25 (fn prems => |
|
26 [ |
|
27 (rtac (smap_def2 RS ssubst) 1), |
|
28 (simp_tac (!simpset addsimps stream_when) 1) |
|
29 ]); |
|
30 |
|
31 qed_goal "smap2" Stream2.thy |
|
32 "x~=UU ==> smap`f`(scons`x`xs) = scons `(f`x) `(smap`f`xs)" |
|
33 (fn prems => |
|
34 [ |
|
35 (cut_facts_tac prems 1), |
|
36 (rtac trans 1), |
|
37 (rtac (smap_def2 RS ssubst) 1), |
|
38 (asm_simp_tac (!simpset addsimps stream_rews) 1), |
|
39 (rtac refl 1) |
|
40 ]); |
|
41 |
|
42 |
|
43 val stream2_rews = [smap1, smap2]; |
|