src/HOL/Corec_Examples/LFilter.thy
 author wenzelm Tue Sep 26 20:54:40 2017 +0200 (23 months ago) changeset 66695 91500c024c7f parent 66453 cc19f7ca2ed6 permissions -rw-r--r--
tuned;
1 (*  Title:      HOL/Corec_Examples/LFilter.thy
2     Author:     Andreas Lochbihler, ETH Zuerich
3     Author:     Dmitriy Traytel, ETH Zuerich
4     Author:     Andrei Popescu, TU Muenchen
7 The filter function on lazy lists.
8 *)
10 section \<open>The Filter Function on Lazy Lists\<close>
12 theory LFilter
13 imports "HOL-Library.BNF_Corec"
14 begin
16 codatatype (lset: 'a) llist =
17   LNil
18 | LCons (lhd: 'a) (ltl: "'a llist")
20 corecursive lfilter where
21   "lfilter P xs = (if \<forall>x \<in> lset xs. \<not> P x then
22     LNil
23     else if P (lhd xs) then
24       LCons (lhd xs) (lfilter P (ltl xs))
25     else
26       lfilter P (ltl xs))"
27 proof (relation "measure (\<lambda>(P, xs). LEAST n. P (lhd ((ltl ^^ n) xs)))", rule wf_measure, clarsimp)
28   fix P xs x
29   assume "x \<in> lset xs" "P x" "\<not> P (lhd xs)"
30   from this(1,2) obtain a where "P (lhd ((ltl ^^ a) xs))"
31     by (atomize_elim, induct x xs rule: llist.set_induct)
32        (auto simp: funpow_Suc_right simp del: funpow.simps(2) intro: exI[of _ 0] exI[of _ "Suc i" for i])
33   with \<open>\<not> P (lhd xs)\<close>
34     have "(LEAST n. P (lhd ((ltl ^^ n) xs))) = Suc (LEAST n. P (lhd ((ltl ^^ Suc n) xs)))"
35     by (intro Least_Suc) auto
36   then show "(LEAST n. P (lhd ((ltl ^^ n) (ltl xs)))) < (LEAST n. P (lhd ((ltl ^^ n) xs)))"
37     by (simp add: funpow_swap1[of ltl])
38 qed
40 lemma lfilter_LNil [simp]: "lfilter P LNil = LNil"
43 lemma lnull_lfilter [simp]: "lfilter P xs = LNil \<longleftrightarrow> (\<forall>x \<in> lset xs. \<not> P x)"
44 proof(rule iffI ballI)+
45   show "\<not> P x" if "x \<in> lset xs" "lfilter P xs = LNil" for x using that
46     by(induction rule: llist.set_induct)(subst (asm) lfilter.code; auto split: if_split_asm; fail)+
49 lemma lfilter_LCons [simp]: "lfilter P (LCons x xs) = (if P x then LCons x (lfilter P xs) else lfilter P xs)"
50   by(subst lfilter.code)(auto intro: sym)
52 lemma llist_in_lfilter [simp]: "lset (lfilter P xs) = lset xs \<inter> {x. P x}"
53 proof(intro set_eqI iffI)
54   show "x \<in> lset xs \<inter> {x. P x}" if "x \<in> lset (lfilter P xs)" for x using that
55   proof(induction ys\<equiv>"lfilter P xs" arbitrary: xs rule: llist.set_induct)
56     case (LCons1 x xs ys)
57     from this show ?case
58       apply(induction arg\<equiv>"(P, ys)" arbitrary: ys rule: lfilter.inner_induct)
59       subgoal by(subst (asm) (2) lfilter.code)(auto split: if_split_asm elim: llist.set_cases)
60       done
61   next
62     case (LCons2 xs y x ys)
63     from LCons2(3) LCons2(1) show ?case
64       apply(induction arg\<equiv>"(P, ys)" arbitrary: ys rule: lfilter.inner_induct)
65       subgoal using LCons2(2) by(subst (asm) (2) lfilter.code)(auto split: if_split_asm elim: llist.set_cases)
66       done
67   qed
68   show "x \<in> lset (lfilter P xs)" if "x \<in> lset xs \<inter> {x. P x}" for x
69     using that[THEN IntD1] that[THEN IntD2] by(induction) auto
70 qed
72 lemma lfilter_unique_weak:
73   "(\<And>xs. f xs = (if \<forall>x \<in> lset xs. \<not> P x then LNil
74     else if P (lhd xs) then LCons (lhd xs) (f (ltl xs))
75     else lfilter P (ltl xs)))
76    \<Longrightarrow> f = lfilter P"
77   by(corec_unique)(rule ext lfilter.code)+
79 lemma lfilter_unique:
80   assumes "\<And>xs. f xs = (if \<forall>x\<in>lset xs. \<not> P x then LNil
81     else if P (lhd xs) then LCons (lhd xs) (f (ltl xs))
82     else f (ltl xs))"
83   shows "f = lfilter P"
84 \<comment> \<open>It seems as if we cannot use @{thm lfilter_unique_weak} for showing this as the induction and the coinduction must be nested\<close>
85 proof(rule ext)
86   show "f xs = lfilter P xs" for xs
87   proof(coinduction arbitrary: xs)
88     case (Eq_llist xs)
89     show ?case
90       apply(induction arg\<equiv>"(P, xs)" arbitrary: xs rule: lfilter.inner_induct)
91       apply(subst (1 2 3 4) assms)
92       apply(subst (1 2 3 4) lfilter.code)
93       apply auto
94       done
95   qed
96 qed
98 lemma lfilter_lfilter: "lfilter P \<circ> lfilter Q = lfilter (\<lambda>x. P x \<and> Q x)"
99   by(rule lfilter_unique)(auto elim: llist.set_cases)
101 end