src/HOL/Induct/LFilter.thy
author paulson
Thu, 26 Nov 1998 17:40:10 +0100
changeset 5977 9f0c8869cf71
parent 3120 c58423c20740
child 9101 b643f4d7b9e9
permissions -rw-r--r--
tidied up list definitions, using type 'a option instead of unit + 'a, also using real typedefs instead of faking them with extra rules

(*  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 => None
                                          | LCons y z => Some(y,z))"

end