--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/LFilter.thy Wed May 07 12:50:26 1997 +0200
@@ -0,0 +1,29 @@
+(* 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