src/HOL/Lazy_Sequence.thy
changeset 58334 7553a1bcecb7
parent 58310 91ea607a34d8
child 58350 919149921e46
     1.1 --- a/src/HOL/Lazy_Sequence.thy	Sat Sep 13 18:08:45 2014 +0200
     1.2 +++ b/src/HOL/Lazy_Sequence.thy	Sun Sep 14 22:59:30 2014 +0200
     1.3 @@ -1,4 +1,3 @@
     1.4 -
     1.5  (* Author: Lukas Bulwahn, TU Muenchen *)
     1.6  
     1.7  header {* Lazy sequences *}
     1.8 @@ -9,7 +8,7 @@
     1.9  
    1.10  subsection {* Type of lazy sequences *}
    1.11  
    1.12 -datatype (dead 'a) lazy_sequence = lazy_sequence_of_list "'a list"
    1.13 +datatype (plugins only: code) (dead 'a) lazy_sequence = lazy_sequence_of_list "'a list"
    1.14  
    1.15  primrec list_of_lazy_sequence :: "'a lazy_sequence \<Rightarrow> 'a list"
    1.16  where
    1.17 @@ -27,11 +26,6 @@
    1.18    "xq = yq \<longleftrightarrow> list_of_lazy_sequence xq = list_of_lazy_sequence yq"
    1.19    by (auto intro: lazy_sequence_eqI)
    1.20  
    1.21 -lemma size_lazy_sequence_eq [code]:
    1.22 -  "size_lazy_sequence f xq = Suc (size_list f (list_of_lazy_sequence xq))"
    1.23 -  "size xq = Suc (length (list_of_lazy_sequence xq))"
    1.24 -  by (cases xq, simp)+
    1.25 -
    1.26  lemma case_lazy_sequence [simp]:
    1.27    "case_lazy_sequence f xq = f (list_of_lazy_sequence xq)"
    1.28    by (cases xq) auto
    1.29 @@ -72,12 +66,6 @@
    1.30    case_list g (\<lambda>x. curry h x \<circ> lazy_sequence_of_list) (list_of_lazy_sequence xq)"
    1.31    by (cases "list_of_lazy_sequence xq") (simp_all add: yield_def)
    1.32  
    1.33 -lemma size_lazy_sequence_code [code]:
    1.34 -  "size_lazy_sequence s xq = (case yield xq of
    1.35 -    None \<Rightarrow> 1
    1.36 -  | Some (x, xq') \<Rightarrow> Suc (s x + size_lazy_sequence s xq'))"
    1.37 -  by (cases "list_of_lazy_sequence xq") (simp_all add: size_lazy_sequence_eq)
    1.38 -
    1.39  lemma equal_lazy_sequence_code [code]:
    1.40    "HOL.equal xq yq = (case (yield xq, yield yq) of
    1.41      (None, None) \<Rightarrow> True