src/HOL/Lazy_Sequence.thy
changeset 38857 97775f3e8722
parent 36902 c6bae4456741
child 40051 b6acda4d1c29
     1.1 --- a/src/HOL/Lazy_Sequence.thy	Fri Aug 27 15:36:02 2010 +0200
     1.2 +++ b/src/HOL/Lazy_Sequence.thy	Fri Aug 27 19:34:23 2010 +0200
     1.3 @@ -39,10 +39,14 @@
     1.4    "size xq = (case yield xq of None => 0 | Some (x, xq') => size xq' + 1)"
     1.5  by (cases xq) auto
     1.6  
     1.7 -lemma [code]: "eq_class.eq xq yq = (case (yield xq, yield yq) of
     1.8 -  (None, None) => True | (Some (x, xq'), Some (y, yq')) => (HOL.eq x y) \<and> (eq_class.eq xq yq) | _ => False)"
     1.9 -apply (cases xq) apply (cases yq) apply (auto simp add: eq_class.eq_equals) 
    1.10 -apply (cases yq) apply (auto simp add: eq_class.eq_equals) done
    1.11 +lemma [code]: "HOL.equal xq yq = (case (yield xq, yield yq) of
    1.12 +  (None, None) => True | (Some (x, xq'), Some (y, yq')) => (HOL.equal x y) \<and> (HOL.equal xq yq) | _ => False)"
    1.13 +apply (cases xq) apply (cases yq) apply (auto simp add: equal_eq) 
    1.14 +apply (cases yq) apply (auto simp add: equal_eq) done
    1.15 +
    1.16 +lemma [code nbe]:
    1.17 +  "HOL.equal (x :: 'a lazy_sequence) x \<longleftrightarrow> True"
    1.18 +  by (fact equal_refl)
    1.19  
    1.20  lemma seq_case [code]:
    1.21    "lazy_sequence_case f g xq = (case (yield xq) of None => f | Some (x, xq') => g x xq')"