equal
deleted
inserted
replaced
12 imports TreeFI Stream |
12 imports TreeFI Stream |
13 begin |
13 begin |
14 |
14 |
15 (* selectors for streams *) |
15 (* selectors for streams *) |
16 lemma shd_def': "shd as = fst (stream_dtor as)" |
16 lemma shd_def': "shd as = fst (stream_dtor as)" |
17 unfolding shd_def stream_case_def fst_def by (rule refl) |
17 apply (case_tac as) |
|
18 apply (auto simp add: shd_def) |
|
19 by (simp add: Stream_def stream.dtor_ctor) |
18 |
20 |
19 lemma stl_def': "stl as = snd (stream_dtor as)" |
21 lemma stl_def': "stl as = snd (stream_dtor as)" |
20 unfolding stl_def stream_case_def snd_def by (rule refl) |
22 apply (case_tac as) |
|
23 apply (auto simp add: stl_def) |
|
24 by (simp add: Stream_def stream.dtor_ctor) |
21 |
25 |
22 lemma unfold_pair_fun_shd[simp]: "shd (stream_dtor_unfold (f \<odot> g) t) = f t" |
26 lemma unfold_pair_fun_shd[simp]: "shd (stream_dtor_unfold (f \<odot> g) t) = f t" |
23 unfolding shd_def' pair_fun_def stream.dtor_unfold by simp |
27 unfolding shd_def' pair_fun_def stream.dtor_unfold by simp |
24 |
28 |
25 lemma unfold_pair_fun_stl[simp]: "stl (stream_dtor_unfold (f \<odot> g) t) = |
29 lemma unfold_pair_fun_stl[simp]: "stl (stream_dtor_unfold (f \<odot> g) t) = |