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