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
```
```     5     Copyright   2014, 2016
```
```     6
```
```     7 The filter function on lazy lists.
```
```     8 *)
```
```     9
```
```    10 section \<open>The Filter Function on Lazy Lists\<close>
```
```    11
```
```    12 theory LFilter
```
```    13 imports "HOL-Library.BNF_Corec"
```
```    14 begin
```
```    15
```
```    16 codatatype (lset: 'a) llist =
```
```    17   LNil
```
```    18 | LCons (lhd: 'a) (ltl: "'a llist")
```
```    19
```
```    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
```
```    39
```
```    40 lemma lfilter_LNil [simp]: "lfilter P LNil = LNil"
```
```    41   by(simp add: lfilter.code)
```
```    42
```
```    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)+
```
```    47 qed(simp add: lfilter.code)
```
```    48
```
```    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)
```
```    51
```
```    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
```
```    71
```
```    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)+
```
```    78
```
```    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
```
```    97
```
```    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)
```
```   100
```
```   101 end
```