Theory Filter

(*  Title:      HOL/Filter.thy
    Author:     Brian Huffman
    Author:     Johannes Hölzl
*)

section ‹Filters on predicates›

theory Filter
imports Set_Interval Lifting_Set
begin

subsection ‹Filters›

text ‹
  This definition also allows non-proper filters.
›

locale is_filter =
  fixes F :: "('a  bool)  bool"
  assumes True: "F (λx. True)"
  assumes conj: "F (λx. P x)  F (λx. Q x)  F (λx. P x  Q x)"
  assumes mono: "x. P x  Q x  F (λx. P x)  F (λx. Q x)"

typedef 'a filter = "{F :: ('a  bool)  bool. is_filter F}"
proof
  show "(λx. True)  ?filter" by (auto intro: is_filter.intro)
qed

lemma is_filter_Rep_filter: "is_filter (Rep_filter F)"
  using Rep_filter [of F] by simp

lemma Abs_filter_inverse':
  assumes "is_filter F" shows "Rep_filter (Abs_filter F) = F"
  using assms by (simp add: Abs_filter_inverse)


subsubsection ‹Eventually›

definition eventually :: "('a  bool)  'a filter  bool"
  where "eventually P F  Rep_filter F P"

syntax
  "_eventually" :: "pttrn => 'a filter => bool => bool"  ("(3F _ in _./ _)" [0, 0, 10] 10)
translations
  "Fx in F. P" == "CONST eventually (λx. P) F"

lemma eventually_Abs_filter:
  assumes "is_filter F" shows "eventually P (Abs_filter F) = F P"
  unfolding eventually_def using assms by (simp add: Abs_filter_inverse)

lemma filter_eq_iff:
  shows "F = F'  (P. eventually P F = eventually P F')"
  unfolding Rep_filter_inject [symmetric] fun_eq_iff eventually_def ..

lemma eventually_True [simp]: "eventually (λx. True) F"
  unfolding eventually_def
  by (rule is_filter.True [OF is_filter_Rep_filter])

lemma always_eventually: "x. P x  eventually P F"
proof -
  assume "x. P x" hence "P = (λx. True)" by (simp add: ext)
  thus "eventually P F" by simp
qed

lemma eventuallyI: "(x. P x)  eventually P F"
  by (auto intro: always_eventually)

lemma filter_eqI: "(P. eventually P F  eventually P G)  F = G"
  by (auto simp: filter_eq_iff)

lemma eventually_mono:
  "eventually P F; x. P x  Q x  eventually Q F"
  unfolding eventually_def
  by (blast intro: is_filter.mono [OF is_filter_Rep_filter])

lemma eventually_conj:
  assumes P: "eventually (λx. P x) F"
  assumes Q: "eventually (λx. Q x) F"
  shows "eventually (λx. P x  Q x) F"
  using assms unfolding eventually_def
  by (rule is_filter.conj [OF is_filter_Rep_filter])

lemma eventually_mp:
  assumes "eventually (λx. P x  Q x) F"
  assumes "eventually (λx. P x) F"
  shows "eventually (λx. Q x) F"
proof -
  have "eventually (λx. (P x  Q x)  P x) F"
    using assms by (rule eventually_conj)
  then show ?thesis
    by (blast intro: eventually_mono)
qed

lemma eventually_rev_mp:
  assumes "eventually (λx. P x) F"
  assumes "eventually (λx. P x  Q x) F"
  shows "eventually (λx. Q x) F"
using assms(2) assms(1) by (rule eventually_mp)

lemma eventually_conj_iff:
  "eventually (λx. P x  Q x) F  eventually P F  eventually Q F"
  by (auto intro: eventually_conj elim: eventually_rev_mp)

lemma eventually_elim2:
  assumes "eventually (λi. P i) F"
  assumes "eventually (λi. Q i) F"
  assumes "i. P i  Q i  R i"
  shows "eventually (λi. R i) F"
  using assms by (auto elim!: eventually_rev_mp)

lemma eventually_cong:
  assumes "eventually P F" and "x. P x  Q x  R x"
  shows   "eventually Q F  eventually R F"
  using assms eventually_elim2 by blast

lemma eventually_ball_finite_distrib:
  "finite A  (eventually (λx. yA. P x y) net)  (yA. eventually (λx. P x y) net)"
  by (induction A rule: finite_induct) (auto simp: eventually_conj_iff)

lemma eventually_ball_finite:
  "finite A  yA. eventually (λx. P x y) net  eventually (λx. yA. P x y) net"
  by (auto simp: eventually_ball_finite_distrib)

lemma eventually_all_finite:
  fixes P :: "'a  'b::finite  bool"
  assumes "y. eventually (λx. P x y) net"
  shows "eventually (λx. y. P x y) net"
using eventually_ball_finite [of UNIV P] assms by simp

lemma eventually_ex: "(Fx in F. y. P x y)  (Y. Fx in F. P x (Y x))"
proof
  assume "Fx in F. y. P x y"
  then have "Fx in F. P x (SOME y. P x y)"
    by (auto intro: someI_ex eventually_mono)
  then show "Y. Fx in F. P x (Y x)"
    by auto
qed (auto intro: eventually_mono)

lemma not_eventually_impI: "eventually P F  ¬ eventually Q F  ¬ eventually (λx. P x  Q x) F"
  by (auto intro: eventually_mp)

lemma not_eventuallyD: "¬ eventually P F  x. ¬ P x"
  by (metis always_eventually)

lemma eventually_subst:
  assumes "eventually (λn. P n = Q n) F"
  shows "eventually P F = eventually Q F" (is "?L = ?R")
proof -
  from assms have "eventually (λx. P x  Q x) F"
      and "eventually (λx. Q x  P x) F"
    by (auto elim: eventually_mono)
  then show ?thesis by (auto elim: eventually_elim2)
qed

subsection ‹ Frequently as dual to eventually ›

definition frequently :: "('a  bool)  'a filter  bool"
  where "frequently P F  ¬ eventually (λx. ¬ P x) F"

syntax
  "_frequently" :: "pttrn  'a filter  bool  bool"  ("(3F _ in _./ _)" [0, 0, 10] 10)
translations
  "Fx in F. P" == "CONST frequently (λx. P) F"

lemma not_frequently_False [simp]: "¬ (Fx in F. False)"
  by (simp add: frequently_def)

lemma frequently_ex: "Fx in F. P x  x. P x"
  by (auto simp: frequently_def dest: not_eventuallyD)

lemma frequentlyE: assumes "frequently P F" obtains x where "P x"
  using frequently_ex[OF assms] by auto

lemma frequently_mp:
  assumes ev: "Fx in F. P x  Q x" and P: "Fx in F. P x" shows "Fx in F. Q x"
proof -
  from ev have "eventually (λx. ¬ Q x  ¬ P x) F"
    by (rule eventually_rev_mp) (auto intro!: always_eventually)
  from eventually_mp[OF this] P show ?thesis
    by (auto simp: frequently_def)
qed

lemma frequently_rev_mp:
  assumes "Fx in F. P x"
  assumes "Fx in F. P x  Q x"
  shows "Fx in F. Q x"
using assms(2) assms(1) by (rule frequently_mp)

lemma frequently_mono: "(x. P x  Q x)  frequently P F  frequently Q F"
  using frequently_mp[of P Q] by (simp add: always_eventually)

lemma frequently_elim1: "Fx in F. P x  (i. P i  Q i)  Fx in F. Q x"
  by (metis frequently_mono)

lemma frequently_disj_iff: "(Fx in F. P x  Q x)  (Fx in F. P x)  (Fx in F. Q x)"
  by (simp add: frequently_def eventually_conj_iff)

lemma frequently_disj: "Fx in F. P x  Fx in F. Q x  Fx in F. P x  Q x"
  by (simp add: frequently_disj_iff)

lemma frequently_bex_finite_distrib:
  assumes "finite A" shows "(Fx in F. yA. P x y)  (yA. Fx in F. P x y)"
  using assms by induction (auto simp: frequently_disj_iff)

lemma frequently_bex_finite: "finite A  Fx in F. yA. P x y  yA. Fx in F. P x y"
  by (simp add: frequently_bex_finite_distrib)

lemma frequently_all: "(Fx in F. y. P x y)  (Y. Fx in F. P x (Y x))"
  using eventually_ex[of "λx y. ¬ P x y" F] by (simp add: frequently_def)

lemma
  shows not_eventually: "¬ eventually P F  (Fx in F. ¬ P x)"
    and not_frequently: "¬ frequently P F  (Fx in F. ¬ P x)"
  by (auto simp: frequently_def)

lemma frequently_imp_iff:
  "(Fx in F. P x  Q x)  (eventually P F  frequently Q F)"
  unfolding imp_conv_disj frequently_disj_iff not_eventually[symmetric] ..

lemma frequently_eventually_conj:
  assumes "Fx in F. P x"
  assumes "Fx in F. Q x"
  shows "Fx in F. Q x  P x"
  using assms eventually_elim2 by (force simp add: frequently_def)

lemma frequently_cong:
  assumes ev: "eventually P F" and QR: "x. P x  Q x  R x"
  shows   "frequently Q F  frequently R F"
  unfolding frequently_def 
  using QR by (auto intro!: eventually_cong [OF ev])

lemma frequently_eventually_frequently:
  "frequently P F  eventually Q F  frequently (λx. P x  Q x) F"
  using frequently_cong [of Q F P "λx. P x  Q x"] by meson
  
lemma eventually_frequently_const_simps:
  "(Fx in F. P x  C)  (Fx in F. P x)  C"
  "(Fx in F. C  P x)  C  (Fx in F. P x)"
  "(Fx in F. P x  C)  (Fx in F. P x)  C"
  "(Fx in F. C  P x)  C  (Fx in F. P x)"
  "(Fx in F. P x  C)  ((Fx in F. P x)  C)"
  "(Fx in F. C  P x)  (C  (Fx in F. P x))"
  by (cases C; simp add: not_frequently)+

lemmas eventually_frequently_simps =
  eventually_frequently_const_simps
  not_eventually
  eventually_conj_iff
  eventually_ball_finite_distrib
  eventually_ex
  not_frequently
  frequently_disj_iff
  frequently_bex_finite_distrib
  frequently_all
  frequently_imp_iff

ML fun eventually_elim_tac facts =
    CONTEXT_SUBGOAL (fn (goal, i) => fn (ctxt, st) =>
      let
        val mp_facts = facts RL @{thms eventually_rev_mp}
        val rule =
          @{thm eventuallyI}
          |> fold (fn mp_fact => fn th => th RS mp_fact) mp_facts
          |> funpow (length facts) (fn th => @{thm impI} RS th)
        val cases_prop =
          Thm.prop_of (Rule_Cases.internalize_params (rule RS Goal.init (Thm.cterm_of ctxt goal)))
        val cases = Rule_Cases.make_common ctxt cases_prop [(("elim", []), [])]
      in CONTEXT_CASES cases (resolve_tac ctxt [rule] i) (ctxt, st) end)

method_setup eventually_elim = Scan.succeed (fn _ => CONTEXT_METHOD (fn facts => eventually_elim_tac facts 1)) "elimination of eventually quantifiers"

subsubsection ‹Finer-than relation›

text termF  F' means that filter termF is finer than
filter termF'.›

instantiation filter :: (type) complete_lattice
begin

definition le_filter_def:
  "F  F'  (P. eventually P F'  eventually P F)"

definition
  "(F :: 'a filter) < F'  F  F'  ¬ F'  F"

definition
  "top = Abs_filter (λP. x. P x)"

definition
  "bot = Abs_filter (λP. True)"

definition
  "sup F F' = Abs_filter (λP. eventually P F  eventually P F')"

definition
  "inf F F' = Abs_filter
      (λP. Q R. eventually Q F  eventually R F'  (x. Q x  R x  P x))"

definition
  "Sup S = Abs_filter (λP. FS. eventually P F)"

definition
  "Inf S = Sup {F::'a filter. F'S. F  F'}"

lemma eventually_top [simp]: "eventually P top  (x. P x)"
  unfolding top_filter_def
  by (rule eventually_Abs_filter, rule is_filter.intro, auto)

lemma eventually_bot [simp]: "eventually P bot"
  unfolding bot_filter_def
  by (subst eventually_Abs_filter, rule is_filter.intro, auto)

lemma eventually_sup:
  "eventually P (sup F F')  eventually P F  eventually P F'"
  unfolding sup_filter_def
  by (rule eventually_Abs_filter, rule is_filter.intro)
     (auto elim!: eventually_rev_mp)

lemma eventually_inf:
  "eventually P (inf F F') 
   (Q R. eventually Q F  eventually R F'  (x. Q x  R x  P x))"
  unfolding inf_filter_def
  apply (rule eventually_Abs_filter [OF is_filter.intro])
  apply (blast intro: eventually_True)
   apply (force elim!: eventually_conj)+
  done

lemma eventually_Sup:
  "eventually P (Sup S)  (FS. eventually P F)"
  unfolding Sup_filter_def
  apply (rule eventually_Abs_filter [OF is_filter.intro])
  apply (auto intro: eventually_conj elim!: eventually_rev_mp)
  done

instance proof
  fix F F' F'' :: "'a filter" and S :: "'a filter set"
  { show "F < F'  F  F'  ¬ F'  F"
    by (rule less_filter_def) }
  { show "F  F"
    unfolding le_filter_def by simp }
  { assume "F  F'" and "F'  F''" thus "F  F''"
    unfolding le_filter_def by simp }
  { assume "F  F'" and "F'  F" thus "F = F'"
    unfolding le_filter_def filter_eq_iff by fast }
  { show "inf F F'  F" and "inf F F'  F'"
    unfolding le_filter_def eventually_inf by (auto intro: eventually_True) }
  { assume "F  F'" and "F  F''" thus "F  inf F' F''"
    unfolding le_filter_def eventually_inf
    by (auto intro: eventually_mono [OF eventually_conj]) }
  { show "F  sup F F'" and "F'  sup F F'"
    unfolding le_filter_def eventually_sup by simp_all }
  { assume "F  F''" and "F'  F''" thus "sup F F'  F''"
    unfolding le_filter_def eventually_sup by simp }
  { assume "F''  S" thus "Inf S  F''"
    unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp }
  { assume "F'. F'  S  F  F'" thus "F  Inf S"
    unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp }
  { assume "F  S" thus "F  Sup S"
    unfolding le_filter_def eventually_Sup by simp }
  { assume "F. F  S  F  F'" thus "Sup S  F'"
    unfolding le_filter_def eventually_Sup by simp }
  { show "Inf {} = (top::'a filter)"
    by (auto simp: top_filter_def Inf_filter_def Sup_filter_def)
      (metis (full_types) top_filter_def always_eventually eventually_top) }
  { show "Sup {} = (bot::'a filter)"
    by (auto simp: bot_filter_def Sup_filter_def) }
qed

end

instance filter :: (type) distrib_lattice
proof
  fix F G H :: "'a filter"
  show "sup F (inf G H) = inf (sup F G) (sup F H)"
  proof (rule order.antisym)
    show "inf (sup F G) (sup F H)  sup F (inf G H)" 
      unfolding le_filter_def eventually_sup
    proof safe
      fix P assume 1: "eventually P F" and 2: "eventually P (inf G H)"
      from 2 obtain Q R 
        where QR: "eventually Q G" "eventually R H" "x. Q x  R x  P x"
        by (auto simp: eventually_inf)
      define Q' where "Q' = (λx. Q x  P x)"
      define R' where "R' = (λx. R x  P x)"
      from 1 have "eventually Q' F" 
        by (elim eventually_mono) (auto simp: Q'_def)
      moreover from 1 have "eventually R' F" 
        by (elim eventually_mono) (auto simp: R'_def)
      moreover from QR(1) have "eventually Q' G" 
        by (elim eventually_mono) (auto simp: Q'_def)
      moreover from QR(2) have "eventually R' H" 
        by (elim eventually_mono)(auto simp: R'_def)
      moreover from QR have "P x" if "Q' x" "R' x" for x 
        using that by (auto simp: Q'_def R'_def)
      ultimately show "eventually P (inf (sup F G) (sup F H))"
        by (auto simp: eventually_inf eventually_sup)
    qed
  qed (auto intro: inf.coboundedI1 inf.coboundedI2)
qed


lemma filter_leD:
  "F  F'  eventually P F'  eventually P F"
  unfolding le_filter_def by simp

lemma filter_leI:
  "(P. eventually P F'  eventually P F)  F  F'"
  unfolding le_filter_def by simp

lemma eventually_False:
  "eventually (λx. False) F  F = bot"
  unfolding filter_eq_iff by (auto elim: eventually_rev_mp)

lemma eventually_frequently: "F  bot  eventually P F  frequently P F"
  using eventually_conj[of P F "λx. ¬ P x"]
  by (auto simp add: frequently_def eventually_False)

lemma eventually_frequentlyE:
  assumes "eventually P F"
  assumes "eventually (λx. ¬ P x  Q x) F" "Fbot"
  shows "frequently Q F"
proof -
  have "eventually Q F"
    using eventually_conj[OF assms(1,2),simplified] by (auto elim:eventually_mono)
  then show ?thesis using eventually_frequently[OF Fbot] by auto
qed

lemma eventually_const_iff: "eventually (λx. P) F  P  F = bot"
  by (cases P) (auto simp: eventually_False)

lemma eventually_const[simp]: "F  bot  eventually (λx. P) F  P"
  by (simp add: eventually_const_iff)

lemma frequently_const_iff: "frequently (λx. P) F  P  F  bot"
  by (simp add: frequently_def eventually_const_iff)

lemma frequently_const[simp]: "F  bot  frequently (λx. P) F  P"
  by (simp add: frequently_const_iff)

lemma eventually_happens: "eventually P net  net = bot  (x. P x)"
  by (metis frequentlyE eventually_frequently)

lemma eventually_happens':
  assumes "F  bot" "eventually P F"
  shows   "x. P x"
  using assms eventually_frequently frequentlyE by blast

abbreviation (input) trivial_limit :: "'a filter  bool"
  where "trivial_limit F  F = bot"

lemma trivial_limit_def: "trivial_limit F  eventually (λx. False) F"
  by (rule eventually_False [symmetric])

lemma False_imp_not_eventually: "(x. ¬ P x )  ¬ trivial_limit net  ¬ eventually (λx. P x) net"
  by (simp add: eventually_False)

lemma trivial_limit_eventually: "trivial_limit net  eventually P net"
  by simp

lemma trivial_limit_eq: "trivial_limit net  (P. eventually P net)"
  by (simp add: filter_eq_iff)

lemma eventually_Inf: "eventually P (Inf B)  (XB. finite X  eventually P (Inf X))"
proof -
  let ?F = "λP. XB. finite X  eventually P (Inf X)"

  have eventually_F: "eventually P (Abs_filter ?F)  ?F P" for P
  proof (rule eventually_Abs_filter is_filter.intro)+
    show "?F (λx. True)"
      by (rule exI[of _ "{}"]) (simp add: le_fun_def)
  next
    fix P Q
    assume "?F P" "?F Q"
    then obtain X Y where
      "X  B" "finite X" "eventually P ( X)"
      "Y  B" "finite Y" "eventually Q ( Y)" by blast
    then show "?F (λx. P x  Q x)"
      by (intro exI[of _ "X  Y"]) (auto simp: Inf_union_distrib eventually_inf)
  next
    fix P Q
    assume "?F P"
    then obtain X where "X  B" "finite X" "eventually P ( X)"
      by blast
    moreover assume "x. P x  Q x"
    ultimately show "?F Q"
      by (intro exI[of _ X]) (auto elim: eventually_mono)
  qed

  have "Inf B = Abs_filter ?F"
  proof (intro antisym Inf_greatest)
    show "Inf B  Abs_filter ?F"
      by (auto simp: le_filter_def eventually_F dest: Inf_superset_mono)
  next
    fix F assume "F  B" then show "Abs_filter ?F  F"
      by (auto simp add: le_filter_def eventually_F intro!: exI[of _ "{F}"])
  qed
  then show ?thesis
    by (simp add: eventually_F)
qed

lemma eventually_INF: "eventually P (bB. F b)  (XB. finite X  eventually P (bX. F b))"
  unfolding eventually_Inf [of P "F`B"]
  by (metis finite_imageI image_mono finite_subset_image)

lemma Inf_filter_not_bot:
  fixes B :: "'a filter set"
  shows "(X. X  B  finite X  Inf X  bot)  Inf B  bot"
  unfolding trivial_limit_def eventually_Inf[of _ B]
    bot_bool_def [symmetric] bot_fun_def [symmetric] bot_unique by simp

lemma INF_filter_not_bot:
  fixes F :: "'i  'a filter"
  shows "(X. X  B  finite X  (bX. F b)  bot)  (bB. F b)  bot"
  unfolding trivial_limit_def eventually_INF [of _ _ B]
    bot_bool_def [symmetric] bot_fun_def [symmetric] bot_unique by simp

lemma eventually_Inf_base:
  assumes "B  {}" and base: "F G. F  B  G  B  xB. x  inf F G"
  shows "eventually P (Inf B)  (bB. eventually P b)"
proof (subst eventually_Inf, safe)
  fix X assume "finite X" "X  B"
  then have "bB. xX. b  x"
  proof induct
    case empty then show ?case
      using B  {} by auto
  next
    case (insert x X)
    then obtain b where "b  B" "x. x  X  b  x"
      by auto
    with insert x X  B base[of b x] show ?case
      by (auto intro: order_trans)
  qed
  then obtain b where "b  B" "b  Inf X"
    by (auto simp: le_Inf_iff)
  then show "eventually P (Inf X)  Bex B (eventually P)"
    by (intro bexI[of _ b]) (auto simp: le_filter_def)
qed (auto intro!: exI[of _ "{x}" for x])

lemma eventually_INF_base:
  "B  {}  (a b. a  B  b  B  xB. F x  inf (F a) (F b)) 
    eventually P (bB. F b)  (bB. eventually P (F b))"
  by (subst eventually_Inf_base) auto

lemma eventually_INF1: "i  I  eventually P (F i)  eventually P (iI. F i)"
  using filter_leD[OF INF_lower] .

lemma eventually_INF_finite:
  assumes "finite A"
  shows   "eventually P ( xA. F x) 
             (Q. (xA. eventually (Q x) (F x))  (y. (xA. Q x y)  P y))" 
  using assms
proof (induction arbitrary: P rule: finite_induct)
  case (insert a A P)
  from insert.hyps have [simp]: "x  a" if "x  A" for x
    using that by auto
  have "eventually P ( xinsert a A. F x) 
          (Q R S. eventually Q (F a)  (( (xA. eventually (S x) (F x)) 
            (y. (xA. S x y)  R y))  (x. Q x  R x  P x)))"
    unfolding ex_simps by (simp add: eventually_inf insert.IH)
  also have "  (Q. (xinsert a A. eventually (Q x) (F x)) 
                           (y. (xinsert a A. Q x y)  P y))"
  proof (safe, goal_cases)
    case (1 Q R S)
    thus ?case using 1 by (intro exI[of _ "S(a := Q)"]) auto
  next
    case (2 Q)
    show ?case
      by (rule exI[of _ "Q a"], rule exI[of _ "λy. xA. Q x y"],
          rule exI[of _ "Q(a := (λ_. True))"]) (use 2 in auto)
  qed
  finally show ?case .
qed auto

lemma eventually_le_le:
  fixes P :: "'a  ('b :: preorder)"
  assumes "eventually (λx. P x  Q x) F"
  assumes "eventually (λx. Q x  R  x) F"
  shows "eventually (λx. P x  R x) F"
using assms by eventually_elim (rule order_trans)

subsubsection ‹Map function for filters›

definition filtermap :: "('a  'b)  'a filter  'b filter"
  where "filtermap f F = Abs_filter (λP. eventually (λx. P (f x)) F)"

lemma eventually_filtermap:
  "eventually P (filtermap f F) = eventually (λx. P (f x)) F"
  unfolding filtermap_def
  apply (rule eventually_Abs_filter [OF is_filter.intro])
  apply (auto elim!: eventually_rev_mp)
  done

lemma eventually_comp_filtermap:
    "eventually (P  f) F  eventually P (filtermap f F)"
  unfolding comp_def using eventually_filtermap by auto

lemma filtermap_compose: "filtermap (f  g) F = filtermap f (filtermap g F)"
  unfolding filter_eq_iff by (simp add: eventually_filtermap)

lemma filtermap_ident: "filtermap (λx. x) F = F"
  by (simp add: filter_eq_iff eventually_filtermap)

lemma filtermap_filtermap:
  "filtermap f (filtermap g F) = filtermap (λx. f (g x)) F"
  by (simp add: filter_eq_iff eventually_filtermap)

lemma filtermap_mono: "F  F'  filtermap f F  filtermap f F'"
  unfolding le_filter_def eventually_filtermap by simp

lemma filtermap_bot [simp]: "filtermap f bot = bot"
  by (simp add: filter_eq_iff eventually_filtermap)

lemma filtermap_bot_iff: "filtermap f F = bot  F = bot"
  by (simp add: trivial_limit_def eventually_filtermap)

lemma filtermap_sup: "filtermap f (sup F1 F2) = sup (filtermap f F1) (filtermap f F2)"
  by (simp add: filter_eq_iff eventually_filtermap eventually_sup)

lemma filtermap_SUP: "filtermap f (bB. F b) = (bB. filtermap f (F b))"
  by (simp add: filter_eq_iff eventually_Sup eventually_filtermap)

lemma filtermap_inf: "filtermap f (inf F1 F2)  inf (filtermap f F1) (filtermap f F2)"
  by (intro inf_greatest filtermap_mono inf_sup_ord)

lemma filtermap_INF: "filtermap f (bB. F b)  (bB. filtermap f (F b))"
  by (rule INF_greatest, rule filtermap_mono, erule INF_lower)

lemma frequently_filtermap:
  "frequently P (filtermap f F) = frequently (λx. P (f x)) F"
  by (simp add: frequently_def eventually_filtermap)


subsubsection ‹Contravariant map function for filters›

definition filtercomap :: "('a  'b)  'b filter  'a filter" where
  "filtercomap f F = Abs_filter (λP. Q. eventually Q F  (x. Q (f x)  P x))"

lemma eventually_filtercomap:
  "eventually P (filtercomap f F)  (Q. eventually Q F  (x. Q (f x)  P x))"
  unfolding filtercomap_def
proof (intro eventually_Abs_filter, unfold_locales, goal_cases)
  case 1
  show ?case by (auto intro!: exI[of _ "λ_. True"])
next
  case (2 P Q)
  then obtain P' Q' where P'Q':
    "eventually P' F" "x. P' (f x)  P x"
    "eventually Q' F" "x. Q' (f x)  Q x"
    by (elim exE conjE)
  show ?case
    by (rule exI[of _ "λx. P' x  Q' x"]) (use P'Q' in auto intro!: eventually_conj)
next
  case (3 P Q)
  thus ?case by blast
qed

lemma filtercomap_ident: "filtercomap (λx. x) F = F"
  by (auto simp: filter_eq_iff eventually_filtercomap elim!: eventually_mono)

lemma filtercomap_filtercomap: "filtercomap f (filtercomap g F) = filtercomap (λx. g (f x)) F"
  unfolding filter_eq_iff by (auto simp: eventually_filtercomap)
  
lemma filtercomap_mono: "F  F'  filtercomap f F  filtercomap f F'"
  by (auto simp: eventually_filtercomap le_filter_def)

lemma filtercomap_bot [simp]: "filtercomap f bot = bot"
  by (auto simp: filter_eq_iff eventually_filtercomap)

lemma filtercomap_top [simp]: "filtercomap f top = top"
  by (auto simp: filter_eq_iff eventually_filtercomap)

lemma filtercomap_inf: "filtercomap f (inf F1 F2) = inf (filtercomap f F1) (filtercomap f F2)"
  unfolding filter_eq_iff
proof safe
  fix P
  assume "eventually P (filtercomap f (F1  F2))"
  then obtain Q R S where *:
    "eventually Q F1" "eventually R F2" "x. Q x  R x  S x" "x. S (f x)  P x"
    unfolding eventually_filtercomap eventually_inf by blast
  from * have "eventually (λx. Q (f x)) (filtercomap f F1)" 
              "eventually (λx. R (f x)) (filtercomap f F2)"
    by (auto simp: eventually_filtercomap)
  with * show "eventually P (filtercomap f F1  filtercomap f F2)"
    unfolding eventually_inf by blast
next
  fix P
  assume "eventually P (inf (filtercomap f F1) (filtercomap f F2))"
  then obtain Q Q' R R' where *:
    "eventually Q F1" "eventually R F2" "x. Q (f x)  Q' x" "x. R (f x)  R' x" 
    "x. Q' x  R' x  P x"
    unfolding eventually_filtercomap eventually_inf by blast
  from * have "eventually (λx. Q x  R x) (F1  F2)" by (auto simp: eventually_inf)
  with * show "eventually P (filtercomap f (F1  F2))"
    by (auto simp: eventually_filtercomap)
qed

lemma filtercomap_sup: "filtercomap f (sup F1 F2)  sup (filtercomap f F1) (filtercomap f F2)"
  by (intro sup_least filtercomap_mono inf_sup_ord)

lemma filtercomap_INF: "filtercomap f (bB. F b) = (bB. filtercomap f (F b))"
proof -
  have *: "filtercomap f (bB. F b) = (bB. filtercomap f (F b))" if "finite B" for B
    using that by induction (simp_all add: filtercomap_inf)
  show ?thesis unfolding filter_eq_iff
  proof
    fix P
    have "eventually P (bB. filtercomap f (F b))  
            (X. (X  B  finite X)  eventually P (bX. filtercomap f (F b)))"
      by (subst eventually_INF) blast
    also have "  (X. (X  B  finite X)  eventually P (filtercomap f (bX. F b)))"
      by (rule ex_cong) (simp add: *)
    also have "  eventually P (filtercomap f ((F ` B)))"
      unfolding eventually_filtercomap by (subst eventually_INF) blast
    finally show "eventually P (filtercomap f ((F ` B))) = 
                    eventually P (bB. filtercomap f (F b))" ..
  qed
qed

lemma filtercomap_SUP:
  "filtercomap f (bB. F b)  (bB. filtercomap f (F b))"
  by (intro SUP_least filtercomap_mono SUP_upper)

lemma filtermap_le_iff_le_filtercomap: "filtermap f F  G  F  filtercomap f G"
  unfolding le_filter_def eventually_filtermap eventually_filtercomap
  using eventually_mono by auto

lemma filtercomap_neq_bot:
  assumes "P. eventually P F  x. P (f x)"
  shows   "filtercomap f F  bot"
  using assms by (auto simp: trivial_limit_def eventually_filtercomap)

lemma filtercomap_neq_bot_surj:
  assumes "F  bot" and "surj f"
  shows   "filtercomap f F  bot"
proof (rule filtercomap_neq_bot)
  fix P assume *: "eventually P F"
  show "x. P (f x)"
  proof (rule ccontr)
    assume **: "¬(x. P (f x))"
    from * have "eventually (λ_. False) F"
    proof eventually_elim
      case (elim x)
      from surj f obtain y where "x = f y" by auto
      with elim and ** show False by auto
    qed
    with assms show False by (simp add: trivial_limit_def)
  qed
qed

lemma eventually_filtercomapI [intro]:
  assumes "eventually P F"
  shows   "eventually (λx. P (f x)) (filtercomap f F)"
  using assms by (auto simp: eventually_filtercomap)

lemma filtermap_filtercomap: "filtermap f (filtercomap f F)  F"
  by (auto simp: le_filter_def eventually_filtermap eventually_filtercomap)

lemma filtercomap_filtermap: "filtercomap f (filtermap f F)  F"
  unfolding le_filter_def eventually_filtermap eventually_filtercomap
  by (auto elim!: eventually_mono)


subsubsection ‹Standard filters›

definition principal :: "'a set  'a filter" where
  "principal S = Abs_filter (λP. xS. P x)"

lemma eventually_principal: "eventually P (principal S)  (xS. P x)"
  unfolding principal_def
  by (rule eventually_Abs_filter, rule is_filter.intro) auto

lemma eventually_inf_principal: "eventually P (inf F (principal s))  eventually (λx. x  s  P x) F"
  unfolding eventually_inf eventually_principal by (auto elim: eventually_mono)

lemma principal_UNIV[simp]: "principal UNIV = top"
  by (auto simp: filter_eq_iff eventually_principal)

lemma principal_empty[simp]: "principal {} = bot"
  by (auto simp: filter_eq_iff eventually_principal)

lemma principal_eq_bot_iff: "principal X = bot  X = {}"
  by (auto simp add: filter_eq_iff eventually_principal)

lemma principal_le_iff[iff]: "principal A  principal B  A  B"
  by (auto simp: le_filter_def eventually_principal)

lemma le_principal: "F  principal A  eventually (λx. x  A) F"
  unfolding le_filter_def eventually_principal
  by (force elim: eventually_mono)

lemma principal_inject[iff]: "principal A = principal B  A = B"
  unfolding eq_iff by simp

lemma sup_principal[simp]: "sup (principal A) (principal B) = principal (A  B)"
  unfolding filter_eq_iff eventually_sup eventually_principal by auto

lemma inf_principal[simp]: "inf (principal A) (principal B) = principal (A  B)"
  unfolding filter_eq_iff eventually_inf eventually_principal
  by (auto intro: exI[of _ "λx. x  A"] exI[of _ "λx. x  B"])

lemma SUP_principal[simp]: "(iI. principal (A i)) = principal (iI. A i)"
  unfolding filter_eq_iff eventually_Sup by (auto simp: eventually_principal)

lemma INF_principal_finite: "finite X  (xX. principal (f x)) = principal (xX. f x)"
  by (induct X rule: finite_induct) auto

lemma filtermap_principal[simp]: "filtermap f (principal A) = principal (f ` A)"
  unfolding filter_eq_iff eventually_filtermap eventually_principal by simp
    
lemma filtercomap_principal[simp]: "filtercomap f (principal A) = principal (f -` A)"
  unfolding filter_eq_iff eventually_filtercomap eventually_principal by fast

subsubsection ‹Order filters›

definition at_top :: "('a::order) filter"
  where "at_top = (k. principal {k ..})"

lemma at_top_sub: "at_top = (k{c::'a::linorder..}. principal {k ..})"
  by (auto intro!: INF_eq max.cobounded1 max.cobounded2 simp: at_top_def)

lemma eventually_at_top_linorder: "eventually P at_top  (N::'a::linorder. nN. P n)"
  unfolding at_top_def
  by (subst eventually_INF_base) (auto simp: eventually_principal intro: max.cobounded1 max.cobounded2)

lemma eventually_filtercomap_at_top_linorder: 
  "eventually P (filtercomap f at_top)  (N::'a::linorder. x. f x  N  P x)"
  by (auto simp: eventually_filtercomap eventually_at_top_linorder)

lemma eventually_at_top_linorderI:
  fixes c::"'a::linorder"
  assumes "x. c  x  P x"
  shows "eventually P at_top"
  using assms by (auto simp: eventually_at_top_linorder)

lemma eventually_ge_at_top [simp]:
  "eventually (λx. (c::_::linorder)  x) at_top"
  unfolding eventually_at_top_linorder by auto

lemma eventually_at_top_dense: "eventually P at_top  (N::'a::{no_top, linorder}. n>N. P n)"
proof -
  have "eventually P (k. principal {k <..})  (N::'a. n>N. P n)"
    by (subst eventually_INF_base) (auto simp: eventually_principal intro: max.cobounded1 max.cobounded2)
  also have "(k. principal {k::'a <..}) = at_top"
    unfolding at_top_def
    by (intro INF_eq) (auto intro: less_imp_le simp: Ici_subset_Ioi_iff gt_ex)
  finally show ?thesis .
qed
  
lemma eventually_filtercomap_at_top_dense: 
  "eventually P (filtercomap f at_top)  (N::'a::{no_top, linorder}. x. f x > N  P x)"
  by (auto simp: eventually_filtercomap eventually_at_top_dense)

lemma eventually_at_top_not_equal [simp]: "eventually (λx::'a::{no_top, linorder}. x  c) at_top"
  unfolding eventually_at_top_dense by auto

lemma eventually_gt_at_top [simp]: "eventually (λx. (c::_::{no_top, linorder}) < x) at_top"
  unfolding eventually_at_top_dense by auto

lemma eventually_all_ge_at_top:
  assumes "eventually P (at_top :: ('a :: linorder) filter)"
  shows   "eventually (λx. yx. P y) at_top"
proof -
  from assms obtain x where "y. y  x  P y" by (auto simp: eventually_at_top_linorder)
  hence "zy. P z" if "y  x" for y using that by simp
  thus ?thesis by (auto simp: eventually_at_top_linorder)
qed

definition at_bot :: "('a::order) filter"
  where "at_bot = (k. principal {.. k})"

lemma at_bot_sub: "at_bot = (k{.. c::'a::linorder}. principal {.. k})"
  by (auto intro!: INF_eq min.cobounded1 min.cobounded2 simp: at_bot_def)

lemma eventually_at_bot_linorder:
  fixes P :: "'a::linorder  bool" shows "eventually P at_bot  (N. nN. P n)"
  unfolding at_bot_def
  by (subst eventually_INF_base) (auto simp: eventually_principal intro: min.cobounded1 min.cobounded2)

lemma eventually_filtercomap_at_bot_linorder: 
  "eventually P (filtercomap f at_bot)  (N::'a::linorder. x. f x  N  P x)"
  by (auto simp: eventually_filtercomap eventually_at_bot_linorder)

lemma eventually_le_at_bot [simp]:
  "eventually (λx. x  (c::_::linorder)) at_bot"
  unfolding eventually_at_bot_linorder by auto

lemma eventually_at_bot_dense: "eventually P at_bot  (N::'a::{no_bot, linorder}. n<N. P n)"
proof -
  have "eventually P (k. principal {..< k})  (N::'a. n<N. P n)"
    by (subst eventually_INF_base) (auto simp: eventually_principal intro: min.cobounded1 min.cobounded2)
  also have "(k. principal {..< k::'a}) = at_bot"
    unfolding at_bot_def
    by (intro INF_eq) (auto intro: less_imp_le simp: Iic_subset_Iio_iff lt_ex)
  finally show ?thesis .
qed

lemma eventually_filtercomap_at_bot_dense: 
  "eventually P (filtercomap f at_bot)  (N::'a::{no_bot, linorder}. x. f x < N  P x)"
  by (auto simp: eventually_filtercomap eventually_at_bot_dense)

lemma eventually_at_bot_not_equal [simp]: "eventually (λx::'a::{no_bot, linorder}. x  c) at_bot"
  unfolding eventually_at_bot_dense by auto

lemma eventually_gt_at_bot [simp]:
  "eventually (λx. x < (c::_::unbounded_dense_linorder)) at_bot"
  unfolding eventually_at_bot_dense by auto

lemma trivial_limit_at_bot_linorder [simp]: "¬ trivial_limit (at_bot ::('a::linorder) filter)"
  unfolding trivial_limit_def
  by (metis eventually_at_bot_linorder order_refl)

lemma trivial_limit_at_top_linorder [simp]: "¬ trivial_limit (at_top ::('a::linorder) filter)"
  unfolding trivial_limit_def
  by (metis eventually_at_top_linorder order_refl)

subsection ‹Sequentially›

abbreviation sequentially :: "nat filter"
  where "sequentially  at_top"

lemma eventually_sequentially:
  "eventually P sequentially  (N. nN. P n)"
  by (rule eventually_at_top_linorder)

lemma sequentially_bot [simp, intro]: "sequentially  bot"
  unfolding filter_eq_iff eventually_sequentially by auto

lemmas trivial_limit_sequentially = sequentially_bot

lemma eventually_False_sequentially [simp]:
  "¬ eventually (λn. False) sequentially"
  by (simp add: eventually_False)

lemma le_sequentially:
  "F  sequentially  (N. eventually (λn. N  n) F)"
  by (simp add: at_top_def le_INF_iff le_principal)

lemma eventually_sequentiallyI [intro?]:
  assumes "x. c  x  P x"
  shows "eventually P sequentially"
using assms by (auto simp: eventually_sequentially)

lemma eventually_sequentially_Suc [simp]: "eventually (λi. P (Suc i)) sequentially  eventually P sequentially"
  unfolding eventually_sequentially by (metis Suc_le_D Suc_le_mono le_Suc_eq)

lemma eventually_sequentially_seg [simp]: "eventually (λn. P (n + k)) sequentially  eventually P sequentially"
  using eventually_sequentially_Suc[of "λn. P (n + k)" for k] by (induction k) auto

lemma filtermap_sequentually_ne_bot: "filtermap f sequentially  bot"
  by (simp add: filtermap_bot_iff)

subsection ‹Increasing finite subsets›

definition finite_subsets_at_top where
  "finite_subsets_at_top A = ( X{X. finite X  X  A}. principal {Y. finite Y  X  Y  Y  A})"

lemma eventually_finite_subsets_at_top:
  "eventually P (finite_subsets_at_top A) 
     (X. finite X  X  A  (Y. finite Y  X  Y  Y  A  P Y))"
  unfolding finite_subsets_at_top_def
proof (subst eventually_INF_base, goal_cases)
  show "{X. finite X  X  A}  {}" by auto
next
  case (2 B C)
  thus ?case by (intro bexI[of _ "B  C"]) auto
qed (simp_all add: eventually_principal)

lemma eventually_finite_subsets_at_top_weakI [intro]:
  assumes "X. finite X  X  A  P X"
  shows   "eventually P (finite_subsets_at_top A)"
proof -
  have "eventually (λX. finite X  X  A) (finite_subsets_at_top A)"
    by (auto simp: eventually_finite_subsets_at_top)
  thus ?thesis by eventually_elim (use assms in auto)
qed

lemma finite_subsets_at_top_neq_bot [simp]: "finite_subsets_at_top A  bot"
proof -
  have "¬eventually (λx. False) (finite_subsets_at_top A)"
    by (auto simp: eventually_finite_subsets_at_top)
  thus ?thesis by auto
qed

lemma filtermap_image_finite_subsets_at_top:
  assumes "inj_on f A"
  shows   "filtermap ((`) f) (finite_subsets_at_top A) = finite_subsets_at_top (f ` A)"
  unfolding filter_eq_iff eventually_filtermap
proof (safe, goal_cases)
  case (1 P)
  then obtain X where X: "finite X" "X  A" "Y. finite Y  X  Y  Y  A  P (f ` Y)"
    unfolding eventually_finite_subsets_at_top by force
  show ?case unfolding eventually_finite_subsets_at_top eventually_filtermap
  proof (rule exI[of _ "f ` X"], intro conjI allI impI, goal_cases)
    case (3 Y)
    with assms and X(1,2) have "P (f ` (f -` Y  A))" using X(1,2)
      by (intro X(3) finite_vimage_IntI) auto
    also have "f ` (f -` Y  A) = Y" using assms 3 by blast
    finally show ?case .
  qed (insert assms X(1,2), auto intro!: finite_vimage_IntI)
next
  case (2 P)
  then obtain X where X: "finite X" "X  f ` A" "Y. finite Y  X  Y  Y  f ` A  P Y"
    unfolding eventually_finite_subsets_at_top by force
  show ?case unfolding eventually_finite_subsets_at_top eventually_filtermap
  proof (rule exI[of _ "f -` X  A"], intro conjI allI impI, goal_cases)
    case (3 Y)
    with X(1,2) and assms show ?case by (intro X(3)) force+
  qed (insert assms X(1), auto intro!: finite_vimage_IntI)
qed

lemma eventually_finite_subsets_at_top_finite:
  assumes "finite A"
  shows   "eventually P (finite_subsets_at_top A)  P A"
  unfolding eventually_finite_subsets_at_top using assms by force

lemma finite_subsets_at_top_finite: "finite A  finite_subsets_at_top A = principal {A}"
  by (auto simp: filter_eq_iff eventually_finite_subsets_at_top_finite eventually_principal)


subsection ‹The cofinite filter›

definition "cofinite = Abs_filter (λP. finite {x. ¬ P x})"

abbreviation Inf_many :: "('a  bool)  bool"  (binder "" 10)
  where "Inf_many P  frequently P cofinite"

abbreviation Alm_all :: "('a  bool)  bool"  (binder "" 10)
  where "Alm_all P  eventually P cofinite"

notation (ASCII)
  Inf_many  (binder "INFM " 10) and
  Alm_all  (binder "MOST " 10)

lemma eventually_cofinite: "eventually P cofinite  finite {x. ¬ P x}"
  unfolding cofinite_def
proof (rule eventually_Abs_filter, rule is_filter.intro)
  fix P Q :: "'a  bool" assume "finite {x. ¬ P x}" "finite {x. ¬ Q x}"
  from finite_UnI[OF this] show "finite {x. ¬ (P x  Q x)}"
    by (rule rev_finite_subset) auto
next
  fix P Q :: "'a  bool" assume P: "finite {x. ¬ P x}" and *: "x. P x  Q x"
  from * show "finite {x. ¬ Q x}"
    by (intro finite_subset[OF _ P]) auto
qed simp

lemma frequently_cofinite: "frequently P cofinite  ¬ finite {x. P x}"
  by (simp add: frequently_def eventually_cofinite)

lemma cofinite_bot[simp]: "cofinite = (bot::'a filter)  finite (UNIV :: 'a set)"
  unfolding trivial_limit_def eventually_cofinite by simp

lemma cofinite_eq_sequentially: "cofinite = sequentially"
  unfolding filter_eq_iff eventually_sequentially eventually_cofinite
proof safe
  fix P :: "nat  bool" assume [simp]: "finite {x. ¬ P x}"
  show "N. nN. P n"
  proof cases
    assume "{x. ¬ P x}  {}" then show ?thesis
      by (intro exI[of _ "Suc (Max {x. ¬ P x})"]) (auto simp: Suc_le_eq)
  qed auto
next
  fix P :: "nat  bool" and N :: nat assume "nN. P n"
  then have "{x. ¬ P x}  {..< N}"
    by (auto simp: not_le)
  then show "finite {x. ¬ P x}"
    by (blast intro: finite_subset)
qed

subsubsection ‹Product of filters›

definition prod_filter :: "'a filter  'b filter  ('a × 'b) filter" (infixr "×F" 80) where
  "prod_filter F G =
    ((P, Q){(P, Q). eventually P F  eventually Q G}. principal {(x, y). P x  Q y})"

lemma eventually_prod_filter: "eventually P (F ×F G) 
  (Pf Pg. eventually Pf F  eventually Pg G  (x y. Pf x  Pg y  P (x, y)))"
  unfolding prod_filter_def
proof (subst eventually_INF_base, goal_cases)
  case 2
  moreover have "eventually Pf F  eventually Qf F  eventually Pg G  eventually Qg G 
    P Q. eventually P F  eventually Q G 
      Collect P × Collect Q  Collect Pf × Collect Pg  Collect Qf × Collect Qg" for Pf Pg Qf Qg
    by (intro conjI exI[of _ "inf Pf Qf"] exI[of _ "inf Pg Qg"])
       (auto simp: inf_fun_def eventually_conj)
  ultimately show ?case
    by auto
qed (auto simp: eventually_principal intro: eventually_True)

lemma eventually_prod1:
  assumes "B  bot"
  shows "(F (x, y) in A ×F B. P x)  (F x in A. P x)"
  unfolding eventually_prod_filter
proof safe
  fix R Q
  assume *: "F x in A. R x" "F x in B. Q x" "x y. R x  Q y  P x"
  with B  bot obtain y where "Q y" by (auto dest: eventually_happens)
  with * show "eventually P A"
    by (force elim: eventually_mono)
next
  assume "eventually P A"
  then show "Pf Pg. eventually Pf A  eventually Pg B  (x y. Pf x  Pg y  P x)"
    by (intro exI[of _ P] exI[of _ "λx. True"]) auto
qed

lemma eventually_prod2:
  assumes "A  bot"
  shows "(F (x, y) in A ×F B. P y)  (F y in B. P y)"
  unfolding eventually_prod_filter
proof safe
  fix R Q
  assume *: "F x in A. R x" "F x in B. Q x" "x y. R x  Q y  P y"
  with A  bot obtain x where "R x" by (auto dest: eventually_happens)
  with * show "eventually P B"
    by (force elim: eventually_mono)
next
  assume "eventually P B"
  then show "Pf Pg. eventually Pf A  eventually Pg B  (x y. Pf x  Pg y  P y)"
    by (intro exI[of _ P] exI[of _ "λx. True"]) auto
qed

lemma INF_filter_bot_base:
  fixes F :: "'a  'b filter"
  assumes *: "i j. i  I  j  I  kI. F k  F i  F j"
  shows "(iI. F i) = bot  (iI. F i = bot)"
proof (cases "iI. F i = bot")
  case True
  then have "(iI. F i)  bot"
    by (auto intro: INF_lower2)
  with True show ?thesis
    by (auto simp: bot_unique)
next
  case False
  moreover have "(iI. F i)  bot"
  proof (cases "I = {}")
    case True
    then show ?thesis
      by (auto simp add: filter_eq_iff)
  next
    case False': False
    show ?thesis
    proof (rule INF_filter_not_bot)
      fix J
      assume "finite J" "J  I"
      then have "kI. F k  (iJ. F i)"
      proof (induct J)
        case empty
        then show ?case
          using I  {} by auto
      next
        case (insert i J)
        then obtain k where "k  I" "F k  (iJ. F i)" by auto
        with insert *[of i k] show ?case
          by auto
      qed
      with False show "(iJ. F i)  "
        by (auto simp: bot_unique)
    qed
  qed
  ultimately show ?thesis
    by auto
qed

lemma Collect_empty_eq_bot: "Collect P = {}  P = "
  by auto

lemma prod_filter_eq_bot: "A ×F B = bot  A = bot  B = bot"
  unfolding trivial_limit_def
proof
  assume "F x in A ×F B. False"
  then obtain Pf Pg
    where Pf: "eventually (λx. Pf x) A" and Pg: "eventually (λy. Pg y) B"
    and *: "x y. Pf x  Pg y  False"
    unfolding eventually_prod_filter by fast
  from * have "(x. ¬ Pf x)  (y. ¬ Pg y)" by fast
  with Pf Pg show "(F x in A. False)  (F x in B. False)" by auto
next
  assume "(F x in A. False)  (F x in B. False)"
  then show "F x in A ×F B. False"
    unfolding eventually_prod_filter by (force intro: eventually_True)
qed

lemma prod_filter_mono: "F  F'  G  G'  F ×F G  F' ×F G'"
  by (auto simp: le_filter_def eventually_prod_filter)

lemma prod_filter_mono_iff:
  assumes nAB: "A  bot" "B  bot"
  shows "A ×F B  C ×F D  A  C  B  D"
proof safe
  assume *: "A ×F B  C ×F D"
  with assms have "A ×F B  bot"
    by (auto simp: bot_unique prod_filter_eq_bot)
  with * have "C ×F D  bot"
    by (auto simp: bot_unique)
  then have nCD: "C  bot" "D  bot"
    by (auto simp: prod_filter_eq_bot)

  show "A  C"
  proof (rule filter_leI)
    fix P assume "eventually P C" with *[THEN filter_leD, of "λ(x, y). P x"] show "eventually P A"
      using nAB nCD by (simp add: eventually_prod1 eventually_prod2)
  qed

  show "B  D"
  proof (rule filter_leI)
    fix P assume "eventually P D" with *[THEN filter_leD, of "λ(x, y). P y"] show "eventually P B"
      using nAB nCD by (simp add: eventually_prod1 eventually_prod2)
  qed
qed (intro prod_filter_mono)

lemma eventually_prod_same: "eventually P (F ×F F) 
    (Q. eventually Q F  (x y. Q x  Q y  P (x, y)))"
  unfolding eventually_prod_filter by (blast intro!: eventually_conj)

lemma eventually_prod_sequentially:
  "eventually P (sequentially ×F sequentially)  (N. m  N. n  N. P (n, m))"
  unfolding eventually_prod_same eventually_sequentially by auto

lemma principal_prod_principal: "principal A ×F principal B = principal (A × B)"
  unfolding filter_eq_iff eventually_prod_filter eventually_principal
  by (fast intro: exI[of _ "λx. x  A"] exI[of _ "λx. x  B"])

lemma le_prod_filterI:
  "filtermap fst F  A  filtermap snd F  B  F  A ×F B"
  unfolding le_filter_def eventually_filtermap eventually_prod_filter
  by (force elim: eventually_elim2)

lemma filtermap_fst_prod_filter: "filtermap fst (A ×F B)  A"
  unfolding le_filter_def eventually_filtermap eventually_prod_filter
  by (force intro: eventually_True)

lemma filtermap_snd_prod_filter: "filtermap snd (A ×F B)  B"
  unfolding le_filter_def eventually_filtermap eventually_prod_filter
  by (force intro: eventually_True)

lemma prod_filter_INF:
  assumes "I  {}" and "J  {}"
  shows "(iI. A i) ×F (jJ. B j) = (iI. jJ. A i ×F B j)"
proof (rule antisym)
  from I  {} obtain i where "i  I" by auto
  from J  {} obtain j where "j  J" by auto

  show "(iI. jJ. A i ×F B j)  (iI. A i) ×F (jJ. B j)"
    by (fast intro: le_prod_filterI INF_greatest INF_lower2
      order_trans[OF filtermap_INF] i  I j  J
      filtermap_fst_prod_filter filtermap_snd_prod_filter)
  show "(iI. A i) ×F (jJ. B j)  (iI. jJ. A i ×F B j)"
    by (intro INF_greatest prod_filter_mono INF_lower)
qed

lemma filtermap_Pair: "filtermap (λx. (f x, g x)) F  filtermap f F ×F filtermap g F"
  by (rule le_prod_filterI, simp_all add: filtermap_filtermap)

lemma eventually_prodI: "eventually P F  eventually Q G  eventually (λx. P (fst x)  Q (snd x)) (F ×F G)"
  unfolding eventually_prod_filter by auto

lemma prod_filter_INF1: "I  {}  (iI. A i) ×F B = (iI. A i ×F B)"
  using prod_filter_INF[of I "{B}" A "λx. x"] by simp

lemma prod_filter_INF2: "J  {}  A ×F (iJ. B i) = (iJ. A ×F B i)"
  using prod_filter_INF[of "{A}" J "λx. x" B] by simp

lemma prod_filtermap1: "prod_filter (filtermap f F) G = filtermap (apfst f) (prod_filter F G)"
  unfolding filter_eq_iff eventually_filtermap eventually_prod_filter
  apply safe
  subgoal by auto
  subgoal for P Q R by(rule exI[where x="λy. x. y = f x  Q x"])(auto intro: eventually_mono)
  done

lemma prod_filtermap2: "prod_filter F (filtermap g G) = filtermap (apsnd g) (prod_filter F G)"
  unfolding filter_eq_iff eventually_filtermap eventually_prod_filter
  apply safe
  subgoal by auto
  subgoal for P Q R  by(auto intro: exI[where x="λy. x. y = g x  R x"] eventually_mono)
  done

lemma prod_filter_assoc:
  "prod_filter (prod_filter F G) H = filtermap (λ(x, y, z). ((x, y), z)) (prod_filter F (prod_filter G H))"
  apply(clarsimp simp add: filter_eq_iff eventually_filtermap eventually_prod_filter; safe)
  subgoal for P Q R S T by(auto 4 4 intro: exI[where x="λ(a, b). T a  S b"])
  subgoal for P Q R S T by(auto 4 3 intro: exI[where x="λ(a, b). Q a  S b"])
  done

lemma prod_filter_principal_singleton: "prod_filter (principal {x}) F = filtermap (Pair x) F"
  by(fastforce simp add: filter_eq_iff eventually_prod_filter eventually_principal eventually_filtermap elim: eventually_mono intro: exI[where x="λa. a = x"])

lemma prod_filter_principal_singleton2: "prod_filter F (principal {x}) = filtermap (λa. (a, x)) F"
  by(fastforce simp add: filter_eq_iff eventually_prod_filter eventually_principal eventually_filtermap elim: eventually_mono intro: exI[where x="λa. a = x"])

lemma prod_filter_commute: "prod_filter F G = filtermap prod.swap (prod_filter G F)"
  by(auto simp add: filter_eq_iff eventually_prod_filter eventually_filtermap)

subsection ‹Limits›

definition filterlim :: "('a  'b)  'b filter  'a filter  bool" where
  "filterlim f F2 F1  filtermap f F1  F2"

syntax
  "_LIM" :: "pttrns  'a  'b  'a  bool" ("(3LIM (_)/ (_)./ (_) :> (_))" [1000, 10, 0, 10] 10)

translations
  "LIM x F1. f :> F2" == "CONST filterlim (λx. f) F2 F1"

lemma filterlim_filtercomapI: "filterlim f F G  filterlim (λx. f (g x)) F (filtercomap g G)"
  unfolding filterlim_def
  by (metis order_trans filtermap_filtercomap filtermap_filtermap filtermap_mono)

lemma filterlim_top [simp]: "filterlim f top F"
  by (simp add: filterlim_def)

lemma filterlim_iff:
  "(LIM x F1. f x :> F2)  (P. eventually P F2  eventually (λx. P (f x)) F1)"
  unfolding filterlim_def le_filter_def eventually_filtermap ..

lemma filterlim_compose:
  "filterlim g F3 F2  filterlim f F2 F1  filterlim (λx. g (f x)) F3 F1"
  unfolding filterlim_def filtermap_filtermap[symmetric] by (metis filtermap_mono order_trans)

lemma filterlim_mono:
  "filterlim f F2 F1  F2  F2'  F1'  F1  filterlim f F2' F1'"
  unfolding filterlim_def by (metis filtermap_mono order_trans)

lemma filterlim_ident: "LIM x F. x :> F"
  by (simp add: filterlim_def filtermap_ident)

lemma filterlim_cong:
  "F1 = F1'  F2 = F2'  eventually (λx. f x = g x) F2  filterlim f F1 F2 = filterlim g F1' F2'"
  by (auto simp: filterlim_def le_filter_def eventually_filtermap elim: eventually_elim2)

lemma filterlim_mono_eventually:
  assumes "filterlim f F G" and ord: "F  F'" "G'  G"
  assumes eq: "eventually (λx. f x = f' x) G'"
  shows "filterlim f' F' G'"
proof -
  have "filterlim f F' G'"
    by (simp add: filterlim_mono[OF _ ord] assms)
  then show ?thesis
    by (rule filterlim_cong[OF refl refl eq, THEN iffD1])
qed

lemma filtermap_mono_strong: "inj f  filtermap f F  filtermap f G  F  G"
  apply (safe intro!: filtermap_mono)
  apply (auto simp: le_filter_def eventually_filtermap)
  apply (erule_tac x="λx. P (inv f x)" in allE)
  apply auto
  done

lemma eventually_compose_filterlim:
  assumes "eventually P F" "filterlim f F G"
  shows "eventually (λx. P (f x)) G"
  using assms by (simp add: filterlim_iff)

lemma filtermap_eq_strong: "inj f  filtermap f F = filtermap f G  F = G"
  by (simp add: filtermap_mono_strong eq_iff)

lemma filtermap_fun_inverse:
  assumes g: "filterlim g F G"
  assumes f: "filterlim f G F"
  assumes ev: "eventually (λx. f (g x) = x) G"
  shows "filtermap f F = G"
proof (rule antisym)
  show "filtermap f F  G"
    using f unfolding filterlim_def .
  have "G = filtermap f (filtermap g G)"
    using ev by (auto elim: eventually_elim2 simp: filter_eq_iff eventually_filtermap)
  also have "  filtermap f F"
    using g by (intro filtermap_mono) (simp add: filterlim_def)
  finally show "G  filtermap f F" .
qed

lemma filterlim_principal:
  "(LIM x F. f x :> principal S)  (eventually (λx. f x  S) F)"
  unfolding filterlim_def eventually_filtermap le_principal ..

lemma filterlim_filtercomap [intro]: "filterlim f F (filtercomap f F)"
  unfolding filterlim_def by (rule filtermap_filtercomap)

lemma filterlim_inf:
  "(LIM x F1. f x :> inf F2 F3)  ((LIM x F1. f x :> F2)  (LIM x F1. f x :> F3))"
  unfolding filterlim_def by simp

lemma filterlim_INF:
  "(LIM x F. f x :> (bB. G b))  (bB. LIM x F. f x :> G b)"
  unfolding filterlim_def le_INF_iff ..

lemma filterlim_INF_INF:
  "(m. m  J  iI. filtermap f (F i)  G m)  LIM x (iI. F i). f x :> (jJ. G j)"
  unfolding filterlim_def by (rule order_trans[OF filtermap_INF INF_mono])

lemma filterlim_INF': "x  A  filterlim f F (G x)  filterlim f F ( xA. G x)"
  unfolding filterlim_def by (rule order.trans[OF filtermap_mono[OF INF_lower]])

lemma filterlim_filtercomap_iff: "filterlim f (filtercomap g G) F  filterlim (g  f) G F"
  by (simp add: filterlim_def filtermap_le_iff_le_filtercomap filtercomap_filtercomap o_def)

lemma filterlim_iff_le_filtercomap: "filterlim f F G  G  filtercomap f F"
  by (simp add: filterlim_def filtermap_le_iff_le_filtercomap)

lemma filterlim_base:
  "(m x. m  J  i m  I)  (m x. m  J  x  F (i m)  f x  G m) 
    LIM x (iI. principal (F i)). f x :> (jJ. principal (G j))"
  by (force intro!: filterlim_INF_INF simp: image_subset_iff)

lemma filterlim_base_iff:
  assumes "I  {}" and chain: "i j. i  I  j  I  F i  F j  F j  F i"
  shows "(LIM x (iI. principal (F i)). f x :> jJ. principal (G j)) 
    (jJ. iI. xF i. f x  G j)"
  unfolding filterlim_INF filterlim_principal
proof (subst eventually_INF_base)
  fix i j assume "i  I" "j  I"
  with chain[OF this] show "xI. principal (F x)  inf (principal (F i)) (principal (F j))"
    by auto
qed (auto simp: eventually_principal I  {})

lemma filterlim_filtermap: "filterlim f F1 (filtermap g F2) = filterlim (λx. f (g x)) F1 F2"
  unfolding filterlim_def filtermap_filtermap ..

lemma filterlim_sup:
  "filterlim f F F1  filterlim f F F2  filterlim f F (sup F1 F2)"
  unfolding filterlim_def filtermap_sup by auto

lemma filterlim_sequentially_Suc:
  "(LIM x sequentially. f (Suc x) :> F)  (LIM x sequentially. f x :> F)"
  unfolding filterlim_iff by (subst eventually_sequentially_Suc) simp

lemma filterlim_Suc: "filterlim Suc sequentially sequentially"
  by (simp add: filterlim_iff eventually_sequentially)

lemma filterlim_If:
  "LIM x inf F (principal {x. P x}). f x :> G 
    LIM x inf F (principal {x. ¬ P x}). g x :> G 
    LIM x F. if P x then f x else g x :> G"
  unfolding filterlim_iff eventually_inf_principal by (auto simp: eventually_conj_iff)

lemma filterlim_Pair:
  "LIM x F. f x :> G  LIM x F. g x :> H  LIM x F. (f x, g x) :> G ×F H"
  unfolding filterlim_def
  by (rule order_trans[OF filtermap_Pair prod_filter_mono])

subsection ‹Limits to constat_top and constat_bot

lemma filterlim_at_top:
  fixes f :: "'a  ('b::linorder)"
  shows "(LIM x F. f x :> at_top)  (Z. eventually (λx. Z  f x) F)"
  by (auto simp: filterlim_iff eventually_at_top_linorder elim!: eventually_mono)

lemma filterlim_at_top_mono:
  "LIM x F. f x :> at_top  eventually (λx. f x  (g x::'a::linorder)) F 
    LIM x F. g x :> at_top"
  by (auto simp: filterlim_at_top elim: eventually_elim2 intro: order_trans)

lemma filterlim_at_top_dense:
  fixes f :: "'a  ('b::unbounded_dense_linorder)"
  shows "(LIM x F. f x :> at_top)  (Z. eventually (λx. Z < f x) F)"
  by (metis eventually_mono[of _ F] eventually_gt_at_top order_less_imp_le
            filterlim_at_top[of f F] filterlim_iff[of f at_top F])

lemma filterlim_at_top_ge:
  fixes f :: "'a  ('b::linorder)" and c :: "'b"
  shows "(LIM x F. f x :> at_top)  (Zc. eventually (λx. Z  f x) F)"
  unfolding at_top_sub[of c] filterlim_INF by (auto simp add: filterlim_principal)

lemma filterlim_at_top_at_top:
  fixes f :: "'a::linorder  'b::linorder"
  assumes mono: "x y. Q x  Q y  x  y  f x  f y"
  assumes bij: "x. P x  f (g x) = x" "x. P x  Q (g x)"
  assumes Q: "eventually Q at_top"
  assumes P: "eventually P at_top"
  shows "filterlim f at_top at_top"
proof -
  from P obtain x where x: "y. x  y  P y"
    unfolding eventually_at_top_linorder by auto
  show ?thesis
  proof (intro filterlim_at_top_ge[THEN iffD2] allI impI)
    fix z assume "x  z"
    with x have "P z" by auto
    have "eventually (λx. g z  x) at_top"
      by (rule eventually_ge_at_top)
    with Q show "eventually (λx. z  f x) at_top"
      by eventually_elim (metis mono bij P z)
  qed
qed

lemma filterlim_at_top_gt:
  fixes f :: "'a  ('b::unbounded_dense_linorder)" and c :: "'b"
  shows "(LIM x F. f x :> at_top)  (Z>c. eventually (λx. Z  f x) F)"
  by (metis filterlim_at_top order_less_le_trans gt_ex filterlim_at_top_ge)

lemma filterlim_at_bot:
  fixes f :: "'a  ('b::linorder)"
  shows "(LIM x F. f x :> at_bot)  (Z. eventually (λx. f x  Z) F)"
  by (auto simp: filterlim_iff eventually_at_bot_linorder elim!: eventually_mono)

lemma filterlim_at_bot_dense:
  fixes f :: "'a  ('b::{dense_linorder, no_bot})"
  shows "(LIM x F. f x :> at_bot)  (Z. eventually (λx. f x < Z) F)"
proof (auto simp add: filterlim_at_bot[of f F])
  fix Z :: 'b
  from lt_ex [of Z] obtain Z' where 1: "Z' < Z" ..
  assume "Z. eventually (λx. f x  Z) F"
  hence "eventually (λx. f x  Z') F" by auto
  thus "eventually (λx. f x < Z) F"
    by (rule eventually_mono) (use 1 in auto)
  next
    fix Z :: 'b
    show "Z. eventually (λx. f x < Z) F  eventually (λx. f x  Z) F"
      by (drule spec [of _ Z], erule eventually_mono, auto simp add: less_imp_le)
qed

lemma filterlim_at_bot_le:
  fixes f :: "'a  ('b::linorder)" and c :: "'b"
  shows "(LIM x F. f x :> at_bot)  (Zc. eventually (λx. Z  f x) F)"
  unfolding filterlim_at_bot
proof safe
  fix Z assume *: "Zc. eventually (λx. Z  f x) F"
  with *[THEN spec, of "min Z c"] show "eventually (λx. Z  f x) F"
    by (auto elim!: eventually_mono)
qed simp

lemma filterlim_at_bot_lt:
  fixes f :: "'a  ('b::unbounded_dense_linorder)" and c :: "'b"
  shows "(LIM x F. f x :> at_bot)  (Z<c. eventually (λx. Z  f x) F)"
  by (metis filterlim_at_bot filterlim_at_bot_le lt_ex order_le_less_trans)

lemma filterlim_at_top_div_const_nat:
  assumes "c > 0"
  shows   "filterlim (λx::nat. x div c) at_top at_top"
  unfolding filterlim_at_top
proof
  fix C :: nat
  have *: "n div c  C" if "n  C * c" for n
    using assms that by (metis div_le_mono div_mult_self_is_m)
  have "eventually (λn. n  C * c) at_top"
    by (rule eventually_ge_at_top)
  thus "eventually (λn. n div c  C) at_top"
    by eventually_elim (use * in auto)
qed

lemma filterlim_finite_subsets_at_top:
  "filterlim f (finite_subsets_at_top A) F 
     (X. finite X  X  A  eventually (λy. finite (f y)  X  f y  f y  A) F)"
  (is "?lhs = ?rhs")
proof 
  assume ?lhs
  thus ?rhs
  proof (safe, goal_cases)
    case (1 X)
    hence *: "(F x in F. P (f x))" if "eventually P (finite_subsets_at_top A)" for P
      using that by (auto simp: filterlim_def le_filter_def eventually_filtermap)
    have "F Y in finite_subsets_at_top A. finite Y  X  Y  Y  A"
      using 1 unfolding eventually_finite_subsets_at_top by force
    thus ?case by (intro *) auto
  qed
next
  assume rhs: ?rhs
  show ?lhs unfolding filterlim_def le_filter_def eventually_finite_subsets_at_top
  proof (safe, goal_cases)
    case (1 P X)
    with rhs have "F y in F. finite (f y)  X  f y  f y  A" by auto
    thus "eventually P (filtermap f F)" unfolding eventually_filtermap
      by eventually_elim (insert 1, auto)
  qed
qed

lemma filterlim_atMost_at_top:
  "filterlim (λn. {..n}) (finite_subsets_at_top (UNIV :: nat set)) at_top"
  unfolding filterlim_finite_subsets_at_top
proof (safe, goal_cases)
  case (1 X)
  then obtain n where n: "X  {..n}" by (auto simp: finite_nat_set_iff_bounded_le)
  show ?case using eventually_ge_at_top[of n]
    by eventually_elim (insert n, auto)
qed

lemma filterlim_lessThan_at_top:
  "filterlim (λn. {..<n}) (finite_subsets_at_top (UNIV :: nat set)) at_top"
  unfolding filterlim_finite_subsets_at_top
proof (safe, goal_cases)
  case (1 X)
  then obtain n where n: "X  {..<n}" by (auto simp: finite_nat_set_iff_bounded)
  show ?case using eventually_ge_at_top[of n]
    by eventually_elim (insert n, auto)
qed

lemma filterlim_minus_const_nat_at_top:
  "filterlim (λn. n - c) sequentially sequentially"
  unfolding filterlim_at_top
proof
  fix a :: nat
  show "eventually (λn. n - c  a) at_top"
    using eventually_ge_at_top[of "a + c"] by eventually_elim auto
qed

lemma filterlim_add_const_nat_at_top:
  "filterlim (λn. n + c) sequentially sequentially"
  unfolding filterlim_at_top
proof
  fix a :: nat
  show "eventually (λn. n + c  a) at_top"
    using eventually_ge_at_top[of a] by eventually_elim auto
qed

subsection ‹Setup typ'a filter for lifting and transfer›

lemma filtermap_id [simp, id_simps]: "filtermap id = id"
by(simp add: fun_eq_iff id_def filtermap_ident)

lemma filtermap_id' [simp]: "filtermap (λx. x) = (λF. F)"
using filtermap_id unfolding id_def .

context includes lifting_syntax
begin

definition map_filter_on :: "'a set  ('a  'b)  'a filter  'b filter" where
  "map_filter_on X f F = Abs_filter (λP. eventually (λx. P (f x)  x  X) F)"

lemma is_filter_map_filter_on:
  "is_filter (λP. F x in F. P (f x)  x  X)  eventually (λx. x  X) F"
proof(rule iffI; unfold_locales)
  show "F x in F. True  x  X" if "eventually (λx. x  X) F" using that by simp
  show "F x in F. (P (f x)  Q (f x))  x  X" if "F x in F. P (f x)  x  X" "F x in F. Q (f x)  x  X" for P Q
    using eventually_conj[OF that] by(auto simp add: conj_ac cong: conj_cong)
  show "F x in F. Q (f x)  x  X" if "x. P x  Q x" "F x in F. P (f x)  x  X" for P Q
    using that(2) by(rule eventually_mono)(use that(1) in auto)
  show "eventually (λx. x  X) F" if "is_filter (λP. F x in F. P (f x)  x  X)"
    using is_filter.True[OF that] by simp
qed

lemma eventually_map_filter_on: "eventually P (map_filter_on X f F) = (F x in F. P (f x)  x  X)"
  if "eventually (λx. x  X) F"
  by(simp add: is_filter_map_filter_on map_filter_on_def eventually_Abs_filter that)

lemma map_filter_on_UNIV: "map_filter_on UNIV = filtermap"
  by(simp add: map_filter_on_def filtermap_def fun_eq_iff)

lemma map_filter_on_comp: "map_filter_on X f (map_filter_on Y g F) = map_filter_on Y (f  g) F"
  if "g ` Y  X" and "eventually (λx. x  Y) F"
  unfolding map_filter_on_def using that(1)
  by(auto simp add: eventually_Abs_filter that(2) is_filter_map_filter_on intro!: arg_cong[where f=Abs_filter] arg_cong2[where f=eventually])

inductive rel_filter :: "('a  'b  bool)  'a filter  'b filter  bool" for R F G where
  "rel_filter R F G" if "eventually (case_prod R) Z" "map_filter_on {(x, y). R x y} fst Z = F" "map_filter_on {(x, y). R x y} snd Z = G"

lemma rel_filter_eq [relator_eq]: "rel_filter (=) = (=)"
proof(intro ext iffI)+
  show "F = G" if "rel_filter (=) F G" for F G using that
    by cases(clarsimp simp add: filter_eq_iff eventually_map_filter_on split_def cong: rev_conj_cong)
  show "rel_filter (=) F G" if "F = G" for F G unfolding F = G
  proof
    let ?Z = "map_filter_on UNIV (λx. (x, x)) G"
    have [simp]: "range (λx. (x, x))  {(x, y). x = y}" by auto
    show "map_filter_on {(x, y). x = y} fst ?Z = G" and "map_filter_on {(x, y). x = y} snd ?Z = G"
      by(simp_all add: map_filter_on_comp)(simp_all add: map_filter_on_UNIV o_def)
    show "F (x, y) in ?Z. x = y" by(simp add: eventually_map_filter_on)
  qed
qed

lemma rel_filter_mono [relator_mono]: "rel_filter A  rel_filter B" if le: "A  B"
proof(clarify elim!: rel_filter.cases)
  show "rel_filter B (map_filter_on {(x, y). A x y} fst Z) (map_filter_on {(x, y). A x y} snd Z)"
    (is "rel_filter _ ?X ?Y") if "F (x, y) in Z. A x y" for Z
  proof
    let ?Z = "map_filter_on {(x, y). A x y} id Z"
    show "F (x, y) in ?Z. B x y" using le that
      by(simp add: eventually_map_filter_on le_fun_def split_def conj_commute cong: conj_cong)
    have [simp]: "{(x, y). A x y}  {(x, y). B x y}" using le by auto
    show "map_filter_on {(x, y). B x y} fst ?Z = ?X" "map_filter_on {(x, y). B x y} snd ?Z = ?Y"
      using le that by(simp_all add: le_fun_def map_filter_on_comp)
  qed
qed

lemma rel_filter_conversep: "rel_filter A¯¯ = (rel_filter A)¯¯"
proof(safe intro!: ext elim!: rel_filter.cases)
  show *: "rel_filter A (map_filter_on {(x, y). A¯¯ x y} snd Z) (map_filter_on {(x, y). A¯¯ x y} fst Z)"
    (is "rel_filter _ ?X ?Y") if "F (x, y) in Z. A¯¯ x y" for A Z
  proof
    let ?Z = "map_filter_on {(x, y). A y x} prod.swap Z"
    show "F (x, y) in ?Z. A x y" using that by(simp add: eventually_map_filter_on)
    have [simp]: "prod.swap ` {(x, y). A y x}  {(x, y). A x y}" by auto
    show "map_filter_on {(x, y). A x y} fst ?Z = ?X" "map_filter_on {(x, y). A x y} snd ?Z = ?Y"
      using that by(simp_all add: map_filter_on_comp o_def)
  qed
  show "rel_filter A¯¯ (map_filter_on {(x, y). A x y} snd Z) (map_filter_on {(x, y). A x y} fst Z)"
    if "F (x, y) in Z. A x y" for Z using *[of "A¯¯" Z] that by simp
qed

lemma rel_filter_distr [relator_distr]:
  "rel_filter A OO rel_filter B = rel_filter (A OO B)"
proof(safe intro!: ext elim!: rel_filter.cases)
  let ?AB = "{(x, y). (A OO B) x y}"
  show "(rel_filter A OO rel_filter B)
     (map_filter_on {(x, y). (A OO B) x y} fst Z) (map_filter_on {(x, y). (A OO B) x y} snd Z)"
    (is "(_ OO _) ?F ?H") if "F (x, y) in Z. (A OO B) x y" for Z
  proof
    let ?G = "map_filter_on ?AB (λ(x, y). SOME z. A x z  B z y) Z"
    show "rel_filter A ?F ?G"
    proof
      let ?Z = "map_filter_on ?AB (λ(x, y). (x, SOME z. A x z  B z y)) Z"
      show "F (x, y) in ?Z. A x y" using that
        by(auto simp add: eventually_map_filter_on split_def elim!: eventually_mono intro: someI2)
      have [simp]: "(λp. (fst p, SOME z. A (fst p) z  B z (snd p))) ` {p. (A OO B) (fst p) (snd p)}  {p. A (fst p) (snd p)}" by(auto intro: someI2)
      show "map_filter_on {(x, y). A x y} fst ?Z = ?F" "map_filter_on {(x, y). A x y} snd ?Z = ?G"
        using that by(simp_all add: map_filter_on_comp split_def o_def)
    qed
    show "rel_filter B ?G ?H"
    proof
      let ?Z = "map_filter_on ?AB (λ(x, y). (SOME z. A x z  B z y, y)) Z"
      show "F (x, y) in ?Z. B x y" using that
        by(auto simp add: eventually_map_filter_on split_def elim!: eventually_mono intro: someI2)
      have [simp]: "(λp. (SOME z. A (fst p) z  B z (snd p), snd p)) ` {p. (A OO B) (fst p) (snd p)}  {p. B (fst p) (snd p)}" by(auto intro: someI2)
      show "map_filter_on {(x, y). B x y} fst ?Z = ?G" "map_filter_on {(x, y). B x y} snd ?Z = ?H"
        using that by(simp_all add: map_filter_on_comp split_def o_def)
    qed
  qed

  fix F G
  assume F: "F (x, y) in F. A x y" and G: "F (x, y) in G. B x y"
    and eq: "map_filter_on {(x, y). B x y} fst G = map_filter_on {(x, y). A x y} snd F" (is "?Y2 = ?Y1")
  let ?X = "map_filter_on {(x, y). A x y} fst F"
    and ?Z = "(map_filter_on {(x, y). B x y} snd G)"
  have step: "P'P. Q'  Q. eventually P' F  eventually Q' G  {y. x. P' (x, y)} = {y. z. Q' (y, z)}"
    if P: "eventually P F" and Q: "eventually Q G" for P Q
  proof -
    let ?P = "λ(x, y). P (x, y)  A x y" and ?Q = "λ(y, z). Q (y, z)  B y z"
    define P' where "P'  λ(x, y). ?P (x, y)  (z. ?Q (y, z))"
    define Q' where "Q'  λ(y, z). ?Q (y, z)  (x. ?P (x, y))"
    have "P'  P" "Q'  Q" "{y. x. P' (x, y)} = {y. z. Q' (y, z)}"
      by(auto simp add: P'_def Q'_def)
    moreover
    from P Q F G have P': "eventually ?P F" and Q': "eventually ?Q G" 
      by(simp_all add: eventually_conj_iff split_def)
    from P' F have "F y in ?Y1. x. P (x, y)  A x y"
      by(auto simp add: eventually_map_filter_on elim!: eventually_mono)
    from this[folded eq] obtain Q'' where Q'': "eventually Q'' G"
      and Q''P: "{y. z. Q'' (y, z)}  {y. x. ?P (x, y)}"
      using G by(fastforce simp add: eventually_map_filter_on)
    have "eventually (inf Q'' ?Q) G" using Q'' Q' by(auto intro: eventually_conj simp add: inf_fun_def)
    then have "eventually Q' G" using Q''P  by(auto elim!: eventually_mono simp add: Q'_def)
    moreover
    from Q' G have "F y in ?Y2. z. Q (y, z)  B y z"
      by(auto simp add: eventually_map_filter_on elim!: eventually_mono)
    from this[unfolded eq] obtain P'' where P'': "eventually P'' F"
      and P''Q: "{y. x. P'' (x, y)}  {y. z. ?Q (y, z)}"
      using F by(fastforce simp add: eventually_map_filter_on)
    have "eventually (inf P'' ?P) F" using P'' P' by(auto intro: eventually_conj simp add: inf_fun_def)
    then have "eventually P' F" using P''Q  by(auto elim!: eventually_mono simp add: P'_def)
    ultimately show ?thesis by blast
  qed

  show "rel_filter (A OO B) ?X ?Z"
  proof
    let ?Y = "λY. X Z. eventually X ?X  eventually Z ?Z  (λ(x, z). X x  Z z  (A OO B) x z)  Y"
    have Y: "is_filter ?Y"
    proof
      show "?Y (λ_. True)" by(auto simp add: le_fun_def intro: eventually_True)
      show "?Y (λx. P x  Q x)" if "?Y P" "?Y Q" for P Q using that
        apply clarify
        apply(intro exI conjI; (elim eventually_rev_mp; fold imp_conjL; intro always_eventually allI; rule imp_refl)?)
        apply auto
        done
      show "?Y Q" if "?Y P" "x. P x  Q x" for P Q using that by blast
    qed
    define Y where "Y = Abs_filter ?Y"
    have eventually_Y: "eventually P Y  ?Y P" for P
      using eventually_Abs_filter[OF Y, of P] by(simp add: Y_def)
    show YY: "F (x, y) in Y. (A OO B) x y" using F G
      by(auto simp add: eventually_Y eventually_map_filter_on eventually_conj_iff intro!: eventually_True)
    have "?Y (λ(x, z). P x  (A OO B) x z)  (F (x, y) in F. P x  A x y)" (is "?lhs = ?rhs") for P
    proof
      show ?lhs if ?rhs using G F that
        by(auto 4 3 intro: exI[where x="λ_. True"] simp add: eventually_map_filter_on split_def)
      assume ?lhs
      then obtain X Z where "F (x, y) in F. X x  A x y"
        and "F (x, y) in G. Z y  B x y"
        and "(λ(x, z). X x  Z z  (A OO B) x z)  (λ(x, z). P x  (A OO B) x z)"
        using F G by(auto simp add: eventually_map_filter_on split_def)
      from step[OF this(1, 2)] this(3)
      show ?rhs by(clarsimp elim!: eventually_rev_mp simp add: le_fun_def)(fastforce intro: always_eventually)
    qed
    then show "map_filter_on ?AB fst Y = ?X"
      by(simp add: filter_eq_iff YY eventually_map_filter_on)(simp add: eventually_Y eventually_map_filter_on F G; simp add: split_def)

    have "?Y (λ(x, z). P z  (A OO B) x z)  (F (x, y) in G. P y  B x y)" (is "?lhs = ?rhs") for P
    proof
      show ?lhs if ?rhs using G F that
        by(auto 4 3 intro: exI[where x="λ_. True"] simp add: eventually_map_filter_on split_def)
      assume ?lhs
      then obtain X Z where "F (x, y) in F. X x  A x y"
        and "F (x, y) in G. Z y  B x y"
        and "(λ(x, z). X x  Z z  (A OO B) x z)  (λ(x, z). P z  (A OO B) x z)"
        using F G by(auto simp add: eventually_map_filter_on split_def)
      from step[OF this(1, 2)] this(3)
      show ?rhs by(clarsimp elim!: eventually_rev_mp simp add: le_fun_def)(fastforce intro: always_eventually)
    qed
    then show "map_filter_on ?AB snd Y = ?Z"
      by(simp add: filter_eq_iff YY eventually_map_filter_on)(simp add: eventually_Y eventually_map_filter_on F G; simp add: split_def)
  qed
qed

lemma filtermap_parametric: "((A ===> B) ===> rel_filter A ===> rel_filter B) filtermap filtermap"
proof(intro rel_funI; erule rel_filter.cases; hypsubst)
  fix f g Z
  assume fg: "(A ===> B) f g" and Z: "F (x, y) in Z. A x y"
  have "rel_filter B (map_filter_on {(x, y). A x y} (f  fst) Z) (map_filter_on {(x, y). A x y} (g  snd) Z)"
    (is "rel_filter _ ?F ?G")
  proof
    let ?Z = "map_filter_on {(x, y). A x y} (map_prod f g) Z"
    show "F (x, y) in ?Z. B x y" using fg Z
      by(auto simp add: eventually_map_filter_on split_def elim!: eventually_mono rel_funD)
    have [simp]: "map_prod f g ` {p. A (fst p) (snd p)}  {p. B (fst p) (snd p)}"
      using fg by(auto dest: rel_funD)
    show "map_filter_on {(x, y). B x y} fst ?Z = ?F" "map_filter_on {(x, y). B x y} snd ?Z = ?G"
      using Z by(auto simp add: map_filter_on_comp split_def)
  qed
  thus "rel_filter B (filtermap f (map_filter_on {(x, y). A x y} fst Z)) (filtermap g (map_filter_on {(x, y). A x y} snd Z))"
    using Z by(simp add: map_filter_on_UNIV[symmetric] map_filter_on_comp)
qed

lemma rel_filter_Grp: "rel_filter (Grp UNIV f) = Grp UNIV (filtermap f)"
proof((intro antisym predicate2I; (elim GrpE; hypsubst)?), rule GrpI[OF _ UNIV_I])
  fix F G
  assume "rel_filter (Grp UNIV f) F G"
  hence "rel_filter (=) (filtermap f F) (filtermap id G)"
    by(rule filtermap_parametric[THEN rel_funD, THEN rel_funD, rotated])(simp add: Grp_def rel_fun_def)
  thus "filtermap f F = G" by(simp add: rel_filter_eq)
next
  fix F :: "'a filter"
  have "rel_filter (=) F F" by(simp add: rel_filter_eq)
  hence "rel_filter (Grp UNIV f) (filtermap id F) (filtermap f F)"
    by(rule filtermap_parametric[THEN rel_funD, THEN rel_funD, rotated])(simp add: Grp_def rel_fun_def)
  thus "rel_filter (Grp UNIV f) F (filtermap f F)" by simp
qed

lemma Quotient_filter [quot_map]:
  "Quotient R Abs Rep T  Quotient (rel_filter R) (filtermap Abs) (filtermap Rep) (rel_filter T)"
  unfolding Quotient_alt_def5 rel_filter_eq[symmetric] rel_filter_Grp[symmetric]
  by(simp add: rel_filter_distr[symmetric] rel_filter_conversep[symmetric] rel_filter_mono)

lemma left_total_rel_filter [transfer_rule]: "left_total A  left_total (rel_filter A)"
unfolding left_total_alt_def rel_filter_eq[symmetric] rel_filter_conversep[symmetric] rel_filter_distr
by(rule rel_filter_mono)

lemma right_total_rel_filter [transfer_rule]: "right_total A  right_total (rel_filter A)"
using left_total_rel_filter[of "A¯¯"] by(simp add: rel_filter_conversep)

lemma bi_total_rel_filter [transfer_rule]: "bi_total A  bi_total (rel_filter A)"
unfolding bi_total_alt_def by(simp add: left_total_rel_filter right_total_rel_filter)

lemma left_unique_rel_filter [transfer_rule]: "left_unique A  left_unique (rel_filter A)"
unfolding left_unique_alt_def rel_filter_eq[symmetric] rel_filter_conversep[symmetric] rel_filter_distr
by(rule rel_filter_mono)

lemma right_unique_rel_filter [transfer_rule]:
  "right_unique A  right_unique (rel_filter A)"
using left_unique_rel_filter[of "A¯¯"] by(simp add: rel_filter_conversep)

lemma bi_unique_rel_filter [transfer_rule]: "bi_unique A  bi_unique (rel_filter A)"
by(simp add: bi_unique_alt_def left_unique_rel_filter right_unique_rel_filter)

lemma eventually_parametric [transfer_rule]:
  "((A ===> (=)) ===> rel_filter A ===> (=)) eventually eventually"
by(auto 4 4 intro!: rel_funI elim!: rel_filter.cases simp add: eventually_map_filter_on dest: rel_funD intro: always_eventually elim!: eventually_rev_mp)

lemma frequently_parametric [transfer_rule]: "((A ===> (=)) ===> rel_filter A ===> (=)) frequently frequently"
  unfolding frequently_def[abs_def] by transfer_prover

lemma is_filter_parametric [transfer_rule]:
  assumes [transfer_rule]: "bi_total A"
  assumes [transfer_rule]: "bi_unique A"
  shows "(((A ===> (=)) ===> (=)) ===> (=)) is_filter is_filter"
  unfolding is_filter_def by transfer_prover

lemma top_filter_parametric [transfer_rule]: "rel_filter A top top" if "bi_total A"
proof
  let ?Z = "principal {(x, y). A x y}"
  show "F (x, y) in ?Z. A x y" by(simp add: eventually_principal)
  show "map_filter_on {(x, y). A x y} fst ?Z = top" "map_filter_on {(x, y). A x y} snd ?Z = top"
    using that by(auto simp add: filter_eq_iff eventually_map_filter_on eventually_principal bi_total_def)
qed

lemma bot_filter_parametric [transfer_rule]: "rel_filter A bot bot"
proof
  show "F (x, y) in bot. A x y" by simp
  show "map_filter_on {(x, y). A x y} fst bot = bot" "map_filter_on {(x, y). A x y} snd bot = bot"
    by(simp_all add: filter_eq_iff eventually_map_filter_on)
qed

lemma principal_parametric [transfer_rule]: "(rel_set A ===> rel_filter A) principal principal"
proof(rule rel_funI rel_filter.intros)+
  fix S S'
  assume *: "rel_set A S S'"
  define SS' where "SS' = S × S'  {(x, y). A x y}"
  have SS': "SS'  {(x, y). A x y}" and [simp]: "S = fst ` SS'" "S' = snd ` SS'"
    using * by(auto 4 3 dest: rel_setD1 rel_setD2 intro: rev_image_eqI simp add: SS'_def)
  let ?Z = "principal SS'"
  show "F (x, y) in ?Z. A x y" using SS' by(auto simp add: eventually_principal)
  then show "map_filter_on {(x, y). A x y} fst ?Z = principal S"
    and "map_filter_on {(x, y). A x y} snd ?Z = principal S'"
    by(auto simp add: filter_eq_iff eventually_map_filter_on eventually_principal)
qed

lemma sup_filter_parametric [transfer_rule]:
  "(rel_filter A ===> rel_filter A ===> rel_filter A) sup sup"
proof(intro rel_funI; elim rel_filter.cases; hypsubst)
  show "rel_filter A
    (map_filter_on {(x, y). A x y} fst FG  map_filter_on {(x, y). A x y} fst FG')
    (map_filter_on {(x, y). A x y} snd FG  map_filter_on {(x, y). A x y} snd FG')"
    (is "rel_filter _ (sup ?F ?G) (sup ?F' ?G')")
    if "F (x, y) in FG. A x y" "F (x, y) in FG'. A x y" for FG FG'
  proof
    let ?Z = "sup FG FG'"
    show "F (x, y) in ?Z. A x y" by(simp add: eventually_sup that)
    then show "map_filter_on {(x, y). A x y} fst ?Z = sup ?F ?G" 
      and "map_filter_on {(x, y). A x y} snd ?Z = sup ?F' ?G'"
      by(simp_all add: filter_eq_iff eventually_map_filter_on eventually_sup)
  qed
qed

lemma Sup_filter_parametric [transfer_rule]: "(rel_set (rel_filter A) ===> rel_filter A) Sup Sup"
proof(rule rel_funI)
  fix S S'
  define SS' where "SS' = S × S'  {(F, G). rel_filter A F G}"
  assume "rel_set (rel_filter A) S S'"
  then have SS': "SS'  {(F, G). rel_filter A F G}" and [simp]: "S = fst ` SS'" "S' = snd ` SS'"
    by(auto 4 3 dest: rel_setD1 rel_setD2 intro: rev_image_eqI simp add: SS'_def)
  from SS' obtain Z where Z: "F G. (F, G)  SS' 
    (F (x, y) in Z F G. A x y) 
    id F = map_filter_on {(x, y). A x y} fst (Z F G) 
    id G = map_filter_on {(x, y). A x y} snd (Z F G)"
    unfolding rel_filter.simps by atomize_elim((rule choice allI)+; auto)
  have id: "eventually P F = eventually P (id F)" "eventually Q G = eventually Q (id G)"
    if "(F, G)  SS'" for P Q F G by simp_all
  show "rel_filter A (Sup S) (Sup S')"
  proof
    let ?Z = "(F, G)SS'. Z F G"
    show *: "F (x, y) in ?Z. A x y" using Z by(auto simp add: eventually_Sup)
    show "map_filter_on {(x, y). A x y} fst ?Z = Sup S" "map_filter_on {(x, y). A x y} snd ?Z = Sup S'"
      unfolding filter_eq_iff
      by(auto 4 4 simp add: id eventually_Sup eventually_map_filter_on *[simplified eventually_Sup] simp del: id_apply dest: Z)
  qed
qed

context
  fixes A :: "'a  'b  bool"
  assumes [transfer_rule]: "bi_unique A"
begin

lemma le_filter_parametric [transfer_rule]:
  "(rel_filter A ===> rel_filter A ===> (=)) (≤) (≤)"
unfolding le_filter_def[abs_def] by transfer_prover

lemma less_filter_parametric [transfer_rule]:
  "(rel_filter A ===> rel_filter A ===> (=)) (<) (<)"
unfolding less_filter_def[abs_def] by transfer_prover

context
  assumes [transfer_rule]: "bi_total A"
begin

lemma Inf_filter_parametric [transfer_rule]:
  "(rel_set (rel_filter A) ===> rel_filter A) Inf Inf"
unfolding Inf_filter_def[abs_def] by transfer_prover

lemma inf_filter_parametric [transfer_rule]:
  "(rel_filter A ===> rel_filter A ===> rel_filter A) inf inf"
proof(intro rel_funI)+
  fix F F' G G'
  assume [transfer_rule]: "rel_filter A F F'" "rel_filter A G G'"
  have "rel_filter A (Inf {F, G}) (Inf {F', G'})" by transfer_prover
  thus "rel_filter A (inf F G) (inf F' G')" by simp
qed

end

end

end

context
  includes lifting_syntax
begin

lemma prod_filter_parametric [transfer_rule]:
   "(rel_filter R ===> rel_filter S ===> rel_filter (rel_prod R S)) prod_filter prod_filter"
proof(intro rel_funI; elim rel_filter.cases; hypsubst)
  fix F G
  assume F: "F (x, y) in F. R x y" and G: "F (x, y) in G. S x y"
  show "rel_filter (rel_prod R S)
    (map_filter_on {(x, y). R x y} fst F ×F map_filter_on {(x, y). S x y} fst G)
    (map_filter_on {(x, y). R x y} snd F ×F map_filter_on {(x, y). S x y} snd G)"
    (is "rel_filter ?RS ?F ?G")
  proof
    let ?Z = "filtermap (λ((a, b), (a', b')). ((a, a'), (b, b'))) (prod_filter F G)"
    show *: "F (x, y) in ?Z. rel_prod R S x y" using F G
      by(auto simp add: eventually_filtermap split_beta eventually_prod_filter)
    show "map_filter_on {(x, y). ?RS x y} fst ?Z = ?F"
      using F G
      apply(clarsimp simp add: filter_eq_iff eventually_map_filter_on *)
      apply(simp add: eventually_filtermap split_beta eventually_prod_filter)
      apply(subst eventually_map_filter_on; simp)+
      apply(rule iffI; clarsimp)
      subgoal for P P' P''
        apply(rule exI[where x="λa. b. P' (a, b)  R a b"]; rule conjI)
        subgoal by(fastforce elim: eventually_rev_mp eventually_mono)
        subgoal
          by(rule exI[where x="λa. b. P'' (a, b)  S a b"])(fastforce elim: eventually_rev_mp eventually_mono)
        done
      subgoal by fastforce
      done
    show "map_filter_on {(x, y). ?RS x y} snd ?Z = ?G"
      using F G
      apply(clarsimp simp add: filter_eq_iff eventually_map_filter_on *)
      apply(simp add: eventually_filtermap split_beta eventually_prod_filter)
      apply(subst eventually_map_filter_on; simp)+
      apply(rule iffI; clarsimp)
      subgoal for P P' P''
        apply(rule exI[where x="λb. a. P' (a, b)  R a b"]; rule conjI)
        subgoal by(fastforce elim: eventually_rev_mp eventually_mono)
        subgoal
          by(rule exI[where x="λb. a. P'' (a, b)  S a b"])(fastforce elim: eventually_rev_mp eventually_mono)
        done
      subgoal by fastforce
      done
  qed
qed

end


text ‹Code generation for filters›

definition abstract_filter :: "(unit  'a filter)  'a filter"
  where [simp]: "abstract_filter f = f ()"

code_datatype principal abstract_filter

hide_const (open) abstract_filter

declare [[code drop: filterlim prod_filter filtermap eventually
  "inf :: _ filter  _" "sup :: _ filter  _" "less_eq :: _ filter  _"
  Abs_filter]]

declare filterlim_principal [code]
declare principal_prod_principal [code]
declare filtermap_principal [code]
declare filtercomap_principal [code]
declare eventually_principal [code]
declare inf_principal [code]
declare sup_principal [code]
declare principal_le_iff [code]

lemma Rep_filter_iff_eventually [simp, code]:
  "Rep_filter F P  eventually P F"
  by (simp add: eventually_def)

lemma bot_eq_principal_empty [code]:
  "bot = principal {}"
  by simp

lemma top_eq_principal_UNIV [code]:
  "top = principal UNIV"
  by simp

instantiation filter :: (equal) equal
begin

definition equal_filter :: "'a filter  'a filter  bool"
  where "equal_filter F F'  F = F'"

lemma equal_filter [code]:
  "HOL.equal (principal A) (principal B)  A = B"
  by (simp add: equal_filter_def)

instance
  by standard (simp add: equal_filter_def)

end

end