author  paulson 
Wed, 07 May 1997 12:50:26 +0200  
changeset 3120  c58423c20740 
child 5977  9f0c8869cf71 
permissions  rwrr 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

1 
(* Title: HOL/LList.thy 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

2 
ID: $Id$ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

4 
Copyright 1997 University of Cambridge 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

5 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

6 
The "filter" functional for coinductive lists 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

7 
defined by a combination of induction and coinduction 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

8 
*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

9 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

10 
LFilter = LList + Relation + 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

11 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

12 
consts 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

13 
findRel :: "('a => bool) => ('a llist * 'a llist)set" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

14 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

15 
inductive "findRel p" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

16 
intrs 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

17 
found "p x ==> (LCons x l, LCons x l) : findRel p" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

18 
seek "[ ~p x; (l,l') : findRel p ] ==> (LCons x l, l') : findRel p" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

19 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

20 
constdefs 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

21 
find :: ['a => bool, 'a llist] => 'a llist 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

22 
"find p l == @l'. (l,l'): findRel p  (l' = LNil & l ~: Domain(findRel p))" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

23 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

24 
lfilter :: ['a => bool, 'a llist] => 'a llist 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

25 
"lfilter p l == llist_corec l (%l. case find p l of 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

26 
LNil => Inl () 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

27 
 LCons y z => Inr(y,z))" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

28 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

29 
end 