equal
deleted
inserted
replaced
7 imports Predicate |
7 imports Predicate |
8 begin |
8 begin |
9 |
9 |
10 subsection {* Type of lazy sequences *} |
10 subsection {* Type of lazy sequences *} |
11 |
11 |
12 datatype 'a lazy_sequence = lazy_sequence_of_list "'a list" |
12 datatype_new (dead 'a) lazy_sequence = lazy_sequence_of_list "'a list" |
13 |
13 |
14 primrec list_of_lazy_sequence :: "'a lazy_sequence \<Rightarrow> 'a list" |
14 primrec list_of_lazy_sequence :: "'a lazy_sequence \<Rightarrow> 'a list" |
15 where |
15 where |
16 "list_of_lazy_sequence (lazy_sequence_of_list xs) = xs" |
16 "list_of_lazy_sequence (lazy_sequence_of_list xs) = xs" |
17 |
17 |
27 "xq = yq \<longleftrightarrow> list_of_lazy_sequence xq = list_of_lazy_sequence yq" |
27 "xq = yq \<longleftrightarrow> list_of_lazy_sequence xq = list_of_lazy_sequence yq" |
28 by (auto intro: lazy_sequence_eqI) |
28 by (auto intro: lazy_sequence_eqI) |
29 |
29 |
30 lemma size_lazy_sequence_eq [code]: |
30 lemma size_lazy_sequence_eq [code]: |
31 "size_lazy_sequence f xq = Suc (size_list f (list_of_lazy_sequence xq))" |
31 "size_lazy_sequence f xq = Suc (size_list f (list_of_lazy_sequence xq))" |
32 "size (xq :: 'a lazy_sequence) = 0" |
32 "size xq = Suc (length (list_of_lazy_sequence xq))" |
33 by (cases xq, simp)+ |
33 by (cases xq, simp)+ |
34 |
34 |
35 lemma case_lazy_sequence [simp]: |
35 lemma case_lazy_sequence [simp]: |
36 "case_lazy_sequence f xq = f (list_of_lazy_sequence xq)" |
36 "case_lazy_sequence f xq = f (list_of_lazy_sequence xq)" |
37 by (cases xq) auto |
37 by (cases xq) auto |