src/HOL/Induct/LFilter.thy
author wenzelm
Thu, 26 Jun 1997 11:14:46 +0200
changeset 3462 3472fa00b1d4
parent 3120 c58423c20740
child 5977 9f0c8869cf71
permissions -rw-r--r--
rearrange pages of ps file to be printed as booklet (duplex);

(*  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