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