src/HOL/Lazy_Sequence.thy
changeset 56846 9df717fef2bb
parent 56643 41d3596d8a64
child 58152 6fe60a9a5bad
     1.1 --- a/src/HOL/Lazy_Sequence.thy	Sun May 04 16:17:53 2014 +0200
     1.2 +++ b/src/HOL/Lazy_Sequence.thy	Sun May 04 18:14:58 2014 +0200
     1.3 @@ -27,13 +27,10 @@
     1.4    "xq = yq \<longleftrightarrow> list_of_lazy_sequence xq = list_of_lazy_sequence yq"
     1.5    by (auto intro: lazy_sequence_eqI)
     1.6  
     1.7 -lemma lazy_sequence_size_eq:
     1.8 -  "lazy_sequence_size f xq = Suc (size_list f (list_of_lazy_sequence xq))"
     1.9 -  by (cases xq) simp
    1.10 -
    1.11  lemma size_lazy_sequence_eq [code]:
    1.12 +  "size_lazy_sequence f xq = Suc (size_list f (list_of_lazy_sequence xq))"
    1.13    "size (xq :: 'a lazy_sequence) = 0"
    1.14 -  by (cases xq) simp
    1.15 +  by (cases xq, simp)+
    1.16  
    1.17  lemma case_lazy_sequence [simp]:
    1.18    "case_lazy_sequence f xq = f (list_of_lazy_sequence xq)"
    1.19 @@ -75,11 +72,11 @@
    1.20    case_list g (\<lambda>x. curry h x \<circ> lazy_sequence_of_list) (list_of_lazy_sequence xq)"
    1.21    by (cases "list_of_lazy_sequence xq") (simp_all add: yield_def)
    1.22  
    1.23 -lemma lazy_sequence_size_code [code]:
    1.24 -  "lazy_sequence_size s xq = (case yield xq of
    1.25 +lemma size_lazy_sequence_code [code]:
    1.26 +  "size_lazy_sequence s xq = (case yield xq of
    1.27      None \<Rightarrow> 1
    1.28 -  | Some (x, xq') \<Rightarrow> Suc (s x + lazy_sequence_size s xq'))"
    1.29 -  by (cases "list_of_lazy_sequence xq") (simp_all add: lazy_sequence_size_eq)
    1.30 +  | Some (x, xq') \<Rightarrow> Suc (s x + size_lazy_sequence s xq'))"
    1.31 +  by (cases "list_of_lazy_sequence xq") (simp_all add: size_lazy_sequence_eq)
    1.32  
    1.33  lemma equal_lazy_sequence_code [code]:
    1.34    "HOL.equal xq yq = (case (yield xq, yield yq) of