Theory LFilter

(*  Title:      HOL/Corec_Examples/LFilter.thy
    Author:     Andreas Lochbihler, ETH Zuerich
    Author:     Dmitriy Traytel, ETH Zuerich
    Author:     Andrei Popescu, TU Muenchen
    Copyright   2014, 2016

The filter function on lazy lists.
*)

section ‹The Filter Function on Lazy Lists›

theory LFilter
imports "HOL-Library.BNF_Corec"
begin

codatatype (lset: 'a) llist =
  LNil
| LCons (lhd: 'a) (ltl: "'a llist")

corecursive lfilter where
  "lfilter P xs = (if ∀x ∈ lset xs. ¬ P x then
    LNil
    else if P (lhd xs) then
      LCons (lhd xs) (lfilter P (ltl xs))
    else
      lfilter P (ltl xs))"
proof (relation "measure (λ(P, xs). LEAST n. P (lhd ((ltl ^^ n) xs)))", rule wf_measure, clarsimp)
  fix P xs x
  assume "x ∈ lset xs" "P x" "¬ P (lhd xs)"
  from this(1,2) obtain a where "P (lhd ((ltl ^^ a) xs))"
    by (atomize_elim, induct x xs rule: llist.set_induct)
       (auto simp: funpow_Suc_right simp del: funpow.simps(2) intro: exI[of _ 0] exI[of _ "Suc i" for i])
  with ‹¬ P (lhd xs)›
    have "(LEAST n. P (lhd ((ltl ^^ n) xs))) = Suc (LEAST n. P (lhd ((ltl ^^ Suc n) xs)))"
    by (intro Least_Suc) auto
  then show "(LEAST n. P (lhd ((ltl ^^ n) (ltl xs)))) < (LEAST n. P (lhd ((ltl ^^ n) xs)))"
    by (simp add: funpow_swap1[of ltl])
qed

lemma lfilter_LNil [simp]: "lfilter P LNil = LNil"
  by(simp add: lfilter.code)

lemma lnull_lfilter [simp]: "lfilter P xs = LNil ⟷ (∀x ∈ lset xs. ¬ P x)"
proof(rule iffI ballI)+
  show "¬ P x" if "x ∈ lset xs" "lfilter P xs = LNil" for x using that
    by(induction rule: llist.set_induct)(subst (asm) lfilter.code; auto split: if_split_asm; fail)+
qed(simp add: lfilter.code)

lemma lfilter_LCons [simp]: "lfilter P (LCons x xs) = (if P x then LCons x (lfilter P xs) else lfilter P xs)"
  by(subst lfilter.code)(auto intro: sym)

lemma llist_in_lfilter [simp]: "lset (lfilter P xs) = lset xs ∩ {x. P x}"
proof(intro set_eqI iffI)
  show "x ∈ lset xs ∩ {x. P x}" if "x ∈ lset (lfilter P xs)" for x using that
  proof(induction ys≡"lfilter P xs" arbitrary: xs rule: llist.set_induct)
    case (LCons1 x xs ys)
    from this show ?case
      apply(induction arg≡"(P, ys)" arbitrary: ys rule: lfilter.inner_induct)
      subgoal by(subst (asm) (2) lfilter.code)(auto split: if_split_asm elim: llist.set_cases)
      done
  next
    case (LCons2 xs y x ys)
    from LCons2(3) LCons2(1) show ?case
      apply(induction arg≡"(P, ys)" arbitrary: ys rule: lfilter.inner_induct)
      subgoal using LCons2(2) by(subst (asm) (2) lfilter.code)(auto split: if_split_asm elim: llist.set_cases)
      done
  qed
  show "x ∈ lset (lfilter P xs)" if "x ∈ lset xs ∩ {x. P x}" for x
    using that[THEN IntD1] that[THEN IntD2] by(induction) auto
qed

lemma lfilter_unique_weak:
  "(⋀xs. f xs = (if ∀x ∈ lset xs. ¬ P x then LNil
    else if P (lhd xs) then LCons (lhd xs) (f (ltl xs))
    else lfilter P (ltl xs)))
   ⟹ f = lfilter P"
  by(corec_unique)(rule ext lfilter.code)+

lemma lfilter_unique:
  assumes "⋀xs. f xs = (if ∀x∈lset xs. ¬ P x then LNil
    else if P (lhd xs) then LCons (lhd xs) (f (ltl xs))
    else f (ltl xs))"
  shows "f = lfilter P"
― ‹It seems as if we cannot use @{thm lfilter_unique_weak} for showing this as the induction and the coinduction must be nested›
proof(rule ext)
  show "f xs = lfilter P xs" for xs
  proof(coinduction arbitrary: xs)
    case (Eq_llist xs)
    show ?case
      apply(induction arg≡"(P, xs)" arbitrary: xs rule: lfilter.inner_induct)
      apply(subst (1 2 3 4) assms)
      apply(subst (1 2 3 4) lfilter.code)
      apply auto
      done
  qed
qed

lemma lfilter_lfilter: "lfilter P ∘ lfilter Q = lfilter (λx. P x ∧ Q x)"
  by(rule lfilter_unique)(auto elim: llist.set_cases)

end