src/HOL/ex/LFilter.thy

+(*  Title:      HOL/LList.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1997  University of Cambridge
+
+The "filter" functional for coinductive lists
+  --defined by a combination of induction and coinduction
+*)
+
+LFilter = LList + Relation +
+
+consts
+  findRel	:: "('a => bool) => ('a llist * 'a llist)set"
+
+inductive "findRel p"
+  intrs
+    found  "p x ==> (LCons x l, LCons x l) : findRel p"
+    seek   "[| ~p x;  (l,l') : findRel p |] ==> (LCons x l, l') : findRel p"
+
+constdefs
+  find		:: ['a => bool, 'a llist] => 'a llist
+    "find p l == @l'. (l,l'): findRel p | (l' = LNil & l ~: Domain(findRel p))"
+
+  lfilter	:: ['a => bool, 'a llist] => 'a llist
+    "lfilter p l == llist_corec l (%l. case find p l of
+                                            LNil => Inl ()
+                                          | LCons y z => Inr(y,z))"
+
+end