equal
deleted
inserted
replaced
7 header {*The "filter" functional for coinductive lists |
7 header {*The "filter" functional for coinductive lists |
8 --defined by a combination of induction and coinduction*} |
8 --defined by a combination of induction and coinduction*} |
9 |
9 |
10 theory LFilter imports LList begin |
10 theory LFilter imports LList begin |
11 |
11 |
12 consts |
12 inductive_set |
13 findRel :: "('a => bool) => ('a llist * 'a llist)set" |
13 findRel :: "('a => bool) => ('a llist * 'a llist)set" |
14 |
14 for p :: "'a => bool" |
15 inductive "findRel p" |
15 where |
16 intros |
|
17 found: "p x ==> (LCons x l, LCons x l) \<in> findRel p" |
16 found: "p x ==> (LCons x l, LCons x l) \<in> findRel p" |
18 seek: "[| ~p x; (l,l') \<in> findRel p |] ==> (LCons x l, l') \<in> findRel p" |
17 | seek: "[| ~p x; (l,l') \<in> findRel p |] ==> (LCons x l, l') \<in> findRel p" |
19 |
18 |
20 declare findRel.intros [intro] |
19 declare findRel.intros [intro] |
21 |
20 |
22 definition |
21 definition |
23 find :: "['a => bool, 'a llist] => 'a llist" where |
22 find :: "['a => bool, 'a llist] => 'a llist" where |