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
5    Copyright   2014, 2016
6
7The filter function on lazy lists.
8*)
9
10section \<open>The Filter Function on Lazy Lists\<close>
11
12theory LFilter
13imports "HOL-Library.BNF_Corec"
14begin
15
16codatatype (lset: 'a) llist =
17  LNil
18| LCons (lhd: 'a) (ltl: "'a llist")
19
20corecursive 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))"
27proof (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])
38qed
39
40lemma lfilter_LNil [simp]: "lfilter P LNil = LNil"
41  by(simp add: lfilter.code)
42
43lemma lnull_lfilter [simp]: "lfilter P xs = LNil \<longleftrightarrow> (\<forall>x \<in> lset xs. \<not> P x)"
44proof(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)+
47qed(simp add: lfilter.code)
48
49lemma 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)
51
52lemma llist_in_lfilter [simp]: "lset (lfilter P xs) = lset xs \<inter> {x. P x}"
53proof(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
70qed
71
72lemma 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)+
78
79lemma 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>
85proof(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
96qed
97
98lemma 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)
100
101end
102