author | paulson |
Wed, 07 May 1997 12:50:26 +0200 | |
changeset 3120 | c58423c20740 |
child 5977 | 9f0c8869cf71 |
permissions | -rw-r--r-- |
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 |