strengthen filter relator to canonical categorical definition with better properties
authorAndreas Lochbihler
Fri Feb 16 10:59:14 2018 +0100 (16 months ago)
changeset 676161d005f514417
parent 67614 560fbd6bc047
child 67617 9f9f64fe1705
strengthen filter relator to canonical categorical definition with better properties
NEWS
src/HOL/Filter.thy
     1.1 --- a/NEWS	Thu Feb 15 13:04:36 2018 +0100
     1.2 +++ b/NEWS	Fri Feb 16 10:59:14 2018 +0100
     1.3 @@ -210,6 +210,9 @@
     1.4  * Predicate pairwise_coprime abolished, use "pairwise coprime" instead.
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 +* The relator rel_filter on filters has been strengthened to its 
     1.8 +canonical categorical definition with better properties. INCOMPATIBILITY.
     1.9 +
    1.10  * HOL-Algebra: renamed (^) to [^]
    1.11  
    1.12  * Session HOL-Analysis: Moebius functions and the Riemann mapping
     2.1 --- a/src/HOL/Filter.thy	Thu Feb 15 13:04:36 2018 +0100
     2.2 +++ b/src/HOL/Filter.thy	Fri Feb 16 10:59:14 2018 +0100
     2.3 @@ -1368,65 +1368,267 @@
     2.4  
     2.5  subsection \<open>Setup @{typ "'a filter"} for lifting and transfer\<close>
     2.6  
     2.7 -context includes lifting_syntax
     2.8 -begin
     2.9 -
    2.10 -definition rel_filter :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> 'b filter \<Rightarrow> bool"
    2.11 -where "rel_filter R F G = ((R ===> (=)) ===> (=)) (Rep_filter F) (Rep_filter G)"
    2.12 -
    2.13 -lemma rel_filter_eventually:
    2.14 -  "rel_filter R F G \<longleftrightarrow>
    2.15 -  ((R ===> (=)) ===> (=)) (\<lambda>P. eventually P F) (\<lambda>P. eventually P G)"
    2.16 -by(simp add: rel_filter_def eventually_def)
    2.17 -
    2.18  lemma filtermap_id [simp, id_simps]: "filtermap id = id"
    2.19  by(simp add: fun_eq_iff id_def filtermap_ident)
    2.20  
    2.21  lemma filtermap_id' [simp]: "filtermap (\<lambda>x. x) = (\<lambda>F. F)"
    2.22  using filtermap_id unfolding id_def .
    2.23  
    2.24 -lemma Quotient_filter [quot_map]:
    2.25 -  assumes Q: "Quotient R Abs Rep T"
    2.26 -  shows "Quotient (rel_filter R) (filtermap Abs) (filtermap Rep) (rel_filter T)"
    2.27 -unfolding Quotient_alt_def
    2.28 -proof(intro conjI strip)
    2.29 -  from Q have *: "\<And>x y. T x y \<Longrightarrow> Abs x = y"
    2.30 -    unfolding Quotient_alt_def by blast
    2.31 +context includes lifting_syntax
    2.32 +begin
    2.33 +
    2.34 +definition map_filter_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a filter \<Rightarrow> 'b filter" where
    2.35 +  "map_filter_on X f F = Abs_filter (\<lambda>P. eventually (\<lambda>x. P (f x) \<and> x \<in> X) F)"
    2.36 +
    2.37 +lemma is_filter_map_filter_on:
    2.38 +  "is_filter (\<lambda>P. \<forall>\<^sub>F x in F. P (f x) \<and> x \<in> X) \<longleftrightarrow> eventually (\<lambda>x. x \<in> X) F"
    2.39 +proof(rule iffI; unfold_locales)
    2.40 +  show "\<forall>\<^sub>F x in F. True \<and> x \<in> X" if "eventually (\<lambda>x. x \<in> X) F" using that by simp
    2.41 +  show "\<forall>\<^sub>F x in F. (P (f x) \<and> Q (f x)) \<and> x \<in> X" if "\<forall>\<^sub>F x in F. P (f x) \<and> x \<in> X" "\<forall>\<^sub>F x in F. Q (f x) \<and> x \<in> X" for P Q
    2.42 +    using eventually_conj[OF that] by(auto simp add: conj_ac cong: conj_cong)
    2.43 +  show "\<forall>\<^sub>F x in F. Q (f x) \<and> x \<in> X" if "\<forall>x. P x \<longrightarrow> Q x" "\<forall>\<^sub>F x in F. P (f x) \<and> x \<in> X" for P Q
    2.44 +    using that(2) by(rule eventually_mono)(use that(1) in auto)
    2.45 +  show "eventually (\<lambda>x. x \<in> X) F" if "is_filter (\<lambda>P. \<forall>\<^sub>F x in F. P (f x) \<and> x \<in> X)"
    2.46 +    using is_filter.True[OF that] by simp
    2.47 +qed
    2.48 +
    2.49 +lemma eventually_map_filter_on: "eventually P (map_filter_on X f F) = (\<forall>\<^sub>F x in F. P (f x) \<and> x \<in> X)"
    2.50 +  if "eventually (\<lambda>x. x \<in> X) F"
    2.51 +  by(simp add: is_filter_map_filter_on map_filter_on_def eventually_Abs_filter that)
    2.52 +
    2.53 +lemma map_filter_on_UNIV: "map_filter_on UNIV = filtermap"
    2.54 +  by(simp add: map_filter_on_def filtermap_def fun_eq_iff)
    2.55 +
    2.56 +lemma map_filter_on_comp: "map_filter_on X f (map_filter_on Y g F) = map_filter_on Y (f \<circ> g) F"
    2.57 +  if "g ` Y \<subseteq> X" and "eventually (\<lambda>x. x \<in> Y) F"
    2.58 +  unfolding map_filter_on_def using that(1)
    2.59 +  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])
    2.60 +
    2.61 +inductive rel_filter :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> 'b filter \<Rightarrow> bool" for R F G where
    2.62 +  "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"
    2.63 +
    2.64 +lemma rel_filter_eq [relator_eq]: "rel_filter (=) = (=)"
    2.65 +proof(intro ext iffI)+
    2.66 +  show "F = G" if "rel_filter (=) F G" for F G using that
    2.67 +    by cases(clarsimp simp add: filter_eq_iff eventually_map_filter_on split_def cong: rev_conj_cong)
    2.68 +  show "rel_filter (=) F G" if "F = G" for F G unfolding \<open>F = G\<close>
    2.69 +  proof
    2.70 +    let ?Z = "map_filter_on UNIV (\<lambda>x. (x, x)) G"
    2.71 +    have [simp]: "range (\<lambda>x. (x, x)) \<subseteq> {(x, y). x = y}" by auto
    2.72 +    show "map_filter_on {(x, y). x = y} fst ?Z = G" and "map_filter_on {(x, y). x = y} snd ?Z = G"
    2.73 +      by(simp_all add: map_filter_on_comp)(simp_all add: map_filter_on_UNIV o_def)
    2.74 +    show "\<forall>\<^sub>F (x, y) in ?Z. x = y" by(simp add: eventually_map_filter_on)
    2.75 +  qed
    2.76 +qed
    2.77 +
    2.78 +lemma rel_filter_mono [relator_mono]: "rel_filter A \<le> rel_filter B" if le: "A \<le> B"
    2.79 +proof(clarify elim!: rel_filter.cases)
    2.80 +  show "rel_filter B (map_filter_on {(x, y). A x y} fst Z) (map_filter_on {(x, y). A x y} snd Z)"
    2.81 +    (is "rel_filter _ ?X ?Y") if "\<forall>\<^sub>F (x, y) in Z. A x y" for Z
    2.82 +  proof
    2.83 +    let ?Z = "map_filter_on {(x, y). A x y} id Z"
    2.84 +    show "\<forall>\<^sub>F (x, y) in ?Z. B x y" using le that
    2.85 +      by(simp add: eventually_map_filter_on le_fun_def split_def conj_commute cong: conj_cong)
    2.86 +    have [simp]: "{(x, y). A x y} \<subseteq> {(x, y). B x y}" using le by auto
    2.87 +    show "map_filter_on {(x, y). B x y} fst ?Z = ?X" "map_filter_on {(x, y). B x y} snd ?Z = ?Y"
    2.88 +      using le that by(simp_all add: le_fun_def map_filter_on_comp)
    2.89 +  qed
    2.90 +qed
    2.91 +
    2.92 +lemma rel_filter_conversep: "rel_filter A\<inverse>\<inverse> = (rel_filter A)\<inverse>\<inverse>"
    2.93 +proof(safe intro!: ext elim!: rel_filter.cases)
    2.94 +  show *: "rel_filter A (map_filter_on {(x, y). A\<inverse>\<inverse> x y} snd Z) (map_filter_on {(x, y). A\<inverse>\<inverse> x y} fst Z)"
    2.95 +    (is "rel_filter _ ?X ?Y") if "\<forall>\<^sub>F (x, y) in Z. A\<inverse>\<inverse> x y" for A Z
    2.96 +  proof
    2.97 +    let ?Z = "map_filter_on {(x, y). A y x} prod.swap Z"
    2.98 +    show "\<forall>\<^sub>F (x, y) in ?Z. A x y" using that by(simp add: eventually_map_filter_on)
    2.99 +    have [simp]: "prod.swap ` {(x, y). A y x} \<subseteq> {(x, y). A x y}" by auto
   2.100 +    show "map_filter_on {(x, y). A x y} fst ?Z = ?X" "map_filter_on {(x, y). A x y} snd ?Z = ?Y"
   2.101 +      using that by(simp_all add: map_filter_on_comp o_def)
   2.102 +  qed
   2.103 +  show "rel_filter A\<inverse>\<inverse> (map_filter_on {(x, y). A x y} snd Z) (map_filter_on {(x, y). A x y} fst Z)"
   2.104 +    if "\<forall>\<^sub>F (x, y) in Z. A x y" for Z using *[of "A\<inverse>\<inverse>" Z] that by simp
   2.105 +qed
   2.106 +
   2.107 +lemma rel_filter_distr [relator_distr]:
   2.108 +  "rel_filter A OO rel_filter B = rel_filter (A OO B)"
   2.109 +proof(safe intro!: ext elim!: rel_filter.cases)
   2.110 +  let ?AB = "{(x, y). (A OO B) x y}"
   2.111 +  show "(rel_filter A OO rel_filter B)
   2.112 +     (map_filter_on {(x, y). (A OO B) x y} fst Z) (map_filter_on {(x, y). (A OO B) x y} snd Z)"
   2.113 +    (is "(_ OO _) ?F ?H") if "\<forall>\<^sub>F (x, y) in Z. (A OO B) x y" for Z
   2.114 +  proof
   2.115 +    let ?G = "map_filter_on ?AB (\<lambda>(x, y). SOME z. A x z \<and> B z y) Z"
   2.116 +    show "rel_filter A ?F ?G"
   2.117 +    proof
   2.118 +      let ?Z = "map_filter_on ?AB (\<lambda>(x, y). (x, SOME z. A x z \<and> B z y)) Z"
   2.119 +      show "\<forall>\<^sub>F (x, y) in ?Z. A x y" using that
   2.120 +        by(auto simp add: eventually_map_filter_on split_def elim!: eventually_mono intro: someI2)
   2.121 +      have [simp]: "(\<lambda>p. (fst p, SOME z. A (fst p) z \<and> B z (snd p))) ` {p. (A OO B) (fst p) (snd p)} \<subseteq> {p. A (fst p) (snd p)}" by(auto intro: someI2)
   2.122 +      show "map_filter_on {(x, y). A x y} fst ?Z = ?F" "map_filter_on {(x, y). A x y} snd ?Z = ?G"
   2.123 +        using that by(simp_all add: map_filter_on_comp split_def o_def)
   2.124 +    qed
   2.125 +    show "rel_filter B ?G ?H"
   2.126 +    proof
   2.127 +      let ?Z = "map_filter_on ?AB (\<lambda>(x, y). (SOME z. A x z \<and> B z y, y)) Z"
   2.128 +      show "\<forall>\<^sub>F (x, y) in ?Z. B x y" using that
   2.129 +        by(auto simp add: eventually_map_filter_on split_def elim!: eventually_mono intro: someI2)
   2.130 +      have [simp]: "(\<lambda>p. (SOME z. A (fst p) z \<and> B z (snd p), snd p)) ` {p. (A OO B) (fst p) (snd p)} \<subseteq> {p. B (fst p) (snd p)}" by(auto intro: someI2)
   2.131 +      show "map_filter_on {(x, y). B x y} fst ?Z = ?G" "map_filter_on {(x, y). B x y} snd ?Z = ?H"
   2.132 +        using that by(simp_all add: map_filter_on_comp split_def o_def)
   2.133 +    qed
   2.134 +  qed
   2.135  
   2.136    fix F G
   2.137 -  assume "rel_filter T F G"
   2.138 -  thus "filtermap Abs F = G" unfolding filter_eq_iff
   2.139 -    by(auto simp add: eventually_filtermap rel_filter_eventually * rel_funI del: iffI elim!: rel_funD)
   2.140 -next
   2.141 -  from Q have *: "\<And>x. T (Rep x) x" unfolding Quotient_alt_def by blast
   2.142 +  assume F: "\<forall>\<^sub>F (x, y) in F. A x y" and G: "\<forall>\<^sub>F (x, y) in G. B x y"
   2.143 +    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")
   2.144 +  let ?X = "map_filter_on {(x, y). A x y} fst F"
   2.145 +    and ?Z = "(map_filter_on {(x, y). B x y} snd G)"
   2.146 +  have step: "\<exists>P'\<le>P. \<exists>Q' \<le> Q. eventually P' F \<and> eventually Q' G \<and> {y. \<exists>x. P' (x, y)} = {y. \<exists>z. Q' (y, z)}"
   2.147 +    if P: "eventually P F" and Q: "eventually Q G" for P Q
   2.148 +  proof -
   2.149 +    let ?P = "\<lambda>(x, y). P (x, y) \<and> A x y" and ?Q = "\<lambda>(y, z). Q (y, z) \<and> B y z"
   2.150 +    define P' where "P' \<equiv> \<lambda>(x, y). ?P (x, y) \<and> (\<exists>z. ?Q (y, z))"
   2.151 +    define Q' where "Q' \<equiv> \<lambda>(y, z). ?Q (y, z) \<and> (\<exists>x. ?P (x, y))"
   2.152 +    have "P' \<le> P" "Q' \<le> Q" "{y. \<exists>x. P' (x, y)} = {y. \<exists>z. Q' (y, z)}"
   2.153 +      by(auto simp add: P'_def Q'_def)
   2.154 +    moreover
   2.155 +    from P Q F G have P': "eventually ?P F" and Q': "eventually ?Q G" 
   2.156 +      by(simp_all add: eventually_conj_iff split_def)
   2.157 +    from P' F have "\<forall>\<^sub>F y in ?Y1. \<exists>x. P (x, y) \<and> A x y"
   2.158 +      by(auto simp add: eventually_map_filter_on elim!: eventually_mono)
   2.159 +    from this[folded eq] obtain Q'' where Q'': "eventually Q'' G"
   2.160 +      and Q''P: "{y. \<exists>z. Q'' (y, z)} \<subseteq> {y. \<exists>x. ?P (x, y)}"
   2.161 +      using G by(fastforce simp add: eventually_map_filter_on)
   2.162 +    have "eventually (inf Q'' ?Q) G" using Q'' Q' by(auto intro: eventually_conj simp add: inf_fun_def)
   2.163 +    then have "eventually Q' G" using Q''P  by(auto elim!: eventually_mono simp add: Q'_def)
   2.164 +    moreover
   2.165 +    from Q' G have "\<forall>\<^sub>F y in ?Y2. \<exists>z. Q (y, z) \<and> B y z"
   2.166 +      by(auto simp add: eventually_map_filter_on elim!: eventually_mono)
   2.167 +    from this[unfolded eq] obtain P'' where P'': "eventually P'' F"
   2.168 +      and P''Q: "{y. \<exists>x. P'' (x, y)} \<subseteq> {y. \<exists>z. ?Q (y, z)}"
   2.169 +      using F by(fastforce simp add: eventually_map_filter_on)
   2.170 +    have "eventually (inf P'' ?P) F" using P'' P' by(auto intro: eventually_conj simp add: inf_fun_def)
   2.171 +    then have "eventually P' F" using P''Q  by(auto elim!: eventually_mono simp add: P'_def)
   2.172 +    ultimately show ?thesis by blast
   2.173 +  qed
   2.174 +
   2.175 +  show "rel_filter (A OO B) ?X ?Z"
   2.176 +  proof
   2.177 +    let ?Y = "\<lambda>Y. \<exists>X Z. eventually X ?X \<and> eventually Z ?Z \<and> (\<lambda>(x, z). X x \<and> Z z \<and> (A OO B) x z) \<le> Y"
   2.178 +    have Y: "is_filter ?Y"
   2.179 +    proof
   2.180 +      show "?Y (\<lambda>_. True)" by(auto simp add: le_fun_def intro: eventually_True)
   2.181 +      show "?Y (\<lambda>x. P x \<and> Q x)" if "?Y P" "?Y Q" for P Q using that
   2.182 +        apply clarify
   2.183 +        apply(intro exI conjI; (elim eventually_rev_mp; fold imp_conjL; intro always_eventually allI; rule imp_refl)?)
   2.184 +        apply auto
   2.185 +        done
   2.186 +      show "?Y Q" if "?Y P" "\<forall>x. P x \<longrightarrow> Q x" for P Q using that by blast
   2.187 +    qed
   2.188 +    define Y where "Y = Abs_filter ?Y"
   2.189 +    have eventually_Y: "eventually P Y \<longleftrightarrow> ?Y P" for P
   2.190 +      using eventually_Abs_filter[OF Y, of P] by(simp add: Y_def)
   2.191 +    show YY: "\<forall>\<^sub>F (x, y) in Y. (A OO B) x y" using F G
   2.192 +      by(auto simp add: eventually_Y eventually_map_filter_on eventually_conj_iff intro!: eventually_True)
   2.193 +    have "?Y (\<lambda>(x, z). P x \<and> (A OO B) x z) \<longleftrightarrow> (\<forall>\<^sub>F (x, y) in F. P x \<and> A x y)" (is "?lhs = ?rhs") for P
   2.194 +    proof
   2.195 +      show ?lhs if ?rhs using G F that
   2.196 +        by(auto 4 3 intro: exI[where x="\<lambda>_. True"] simp add: eventually_map_filter_on split_def)
   2.197 +      assume ?lhs
   2.198 +      then obtain X Z where "\<forall>\<^sub>F (x, y) in F. X x \<and> A x y"
   2.199 +        and "\<forall>\<^sub>F (x, y) in G. Z y \<and> B x y"
   2.200 +        and "(\<lambda>(x, z). X x \<and> Z z \<and> (A OO B) x z) \<le> (\<lambda>(x, z). P x \<and> (A OO B) x z)"
   2.201 +        using F G by(auto simp add: eventually_map_filter_on split_def)
   2.202 +      from step[OF this(1, 2)] this(3)
   2.203 +      show ?rhs by(clarsimp elim!: eventually_rev_mp simp add: le_fun_def)(fastforce intro: always_eventually)
   2.204 +    qed
   2.205 +    then show "map_filter_on ?AB fst Y = ?X"
   2.206 +      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)
   2.207  
   2.208 -  fix F
   2.209 -  show "rel_filter T (filtermap Rep F) F"
   2.210 -    by(auto elim: rel_funD intro: * intro!: ext arg_cong[where f="\<lambda>P. eventually P F"] rel_funI
   2.211 -            del: iffI simp add: eventually_filtermap rel_filter_eventually)
   2.212 -qed(auto simp add: map_fun_def o_def eventually_filtermap filter_eq_iff fun_eq_iff rel_filter_eventually
   2.213 -         fun_quotient[OF fun_quotient[OF Q identity_quotient] identity_quotient, unfolded Quotient_alt_def])
   2.214 +    have "?Y (\<lambda>(x, z). P z \<and> (A OO B) x z) \<longleftrightarrow> (\<forall>\<^sub>F (x, y) in G. P y \<and> B x y)" (is "?lhs = ?rhs") for P
   2.215 +    proof
   2.216 +      show ?lhs if ?rhs using G F that
   2.217 +        by(auto 4 3 intro: exI[where x="\<lambda>_. True"] simp add: eventually_map_filter_on split_def)
   2.218 +      assume ?lhs
   2.219 +      then obtain X Z where "\<forall>\<^sub>F (x, y) in F. X x \<and> A x y"
   2.220 +        and "\<forall>\<^sub>F (x, y) in G. Z y \<and> B x y"
   2.221 +        and "(\<lambda>(x, z). X x \<and> Z z \<and> (A OO B) x z) \<le> (\<lambda>(x, z). P z \<and> (A OO B) x z)"
   2.222 +        using F G by(auto simp add: eventually_map_filter_on split_def)
   2.223 +      from step[OF this(1, 2)] this(3)
   2.224 +      show ?rhs by(clarsimp elim!: eventually_rev_mp simp add: le_fun_def)(fastforce intro: always_eventually)
   2.225 +    qed
   2.226 +    then show "map_filter_on ?AB snd Y = ?Z"
   2.227 +      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)
   2.228 +  qed
   2.229 +qed
   2.230 +
   2.231 +lemma filtermap_parametric: "((A ===> B) ===> rel_filter A ===> rel_filter B) filtermap filtermap"
   2.232 +proof(intro rel_funI; erule rel_filter.cases; hypsubst)
   2.233 +  fix f g Z
   2.234 +  assume fg: "(A ===> B) f g" and Z: "\<forall>\<^sub>F (x, y) in Z. A x y"
   2.235 +  have "rel_filter B (map_filter_on {(x, y). A x y} (f \<circ> fst) Z) (map_filter_on {(x, y). A x y} (g \<circ> snd) Z)"
   2.236 +    (is "rel_filter _ ?F ?G")
   2.237 +  proof
   2.238 +    let ?Z = "map_filter_on {(x, y). A x y} (map_prod f g) Z"
   2.239 +    show "\<forall>\<^sub>F (x, y) in ?Z. B x y" using fg Z
   2.240 +      by(auto simp add: eventually_map_filter_on split_def elim!: eventually_mono rel_funD)
   2.241 +    have [simp]: "map_prod f g ` {p. A (fst p) (snd p)} \<subseteq> {p. B (fst p) (snd p)}"
   2.242 +      using fg by(auto dest: rel_funD)
   2.243 +    show "map_filter_on {(x, y). B x y} fst ?Z = ?F" "map_filter_on {(x, y). B x y} snd ?Z = ?G"
   2.244 +      using Z by(auto simp add: map_filter_on_comp split_def)
   2.245 +  qed
   2.246 +  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))"
   2.247 +    using Z by(simp add: map_filter_on_UNIV[symmetric] map_filter_on_comp)
   2.248 +qed
   2.249 +
   2.250 +lemma rel_filter_Grp: "rel_filter (Grp UNIV f) = Grp UNIV (filtermap f)"
   2.251 +proof((intro antisym predicate2I; (elim GrpE; hypsubst)?), rule GrpI[OF _ UNIV_I])
   2.252 +  fix F G
   2.253 +  assume "rel_filter (Grp UNIV f) F G"
   2.254 +  hence "rel_filter (=) (filtermap f F) (filtermap id G)"
   2.255 +    by(rule filtermap_parametric[THEN rel_funD, THEN rel_funD, rotated])(simp add: Grp_def rel_fun_def)
   2.256 +  thus "filtermap f F = G" by(simp add: rel_filter_eq)
   2.257 +next
   2.258 +  fix F :: "'a filter"
   2.259 +  have "rel_filter (=) F F" by(simp add: rel_filter_eq)
   2.260 +  hence "rel_filter (Grp UNIV f) (filtermap id F) (filtermap f F)"
   2.261 +    by(rule filtermap_parametric[THEN rel_funD, THEN rel_funD, rotated])(simp add: Grp_def rel_fun_def)
   2.262 +  thus "rel_filter (Grp UNIV f) F (filtermap f F)" by simp
   2.263 +qed
   2.264 +
   2.265 +lemma Quotient_filter [quot_map]:
   2.266 +  "Quotient R Abs Rep T \<Longrightarrow> Quotient (rel_filter R) (filtermap Abs) (filtermap Rep) (rel_filter T)"
   2.267 +  unfolding Quotient_alt_def5 rel_filter_eq[symmetric] rel_filter_Grp[symmetric]
   2.268 +  by(simp add: rel_filter_distr[symmetric] rel_filter_conversep[symmetric] rel_filter_mono)
   2.269 +
   2.270 +lemma left_total_rel_filter [transfer_rule]: "left_total A \<Longrightarrow> left_total (rel_filter A)"
   2.271 +unfolding left_total_alt_def rel_filter_eq[symmetric] rel_filter_conversep[symmetric] rel_filter_distr
   2.272 +by(rule rel_filter_mono)
   2.273 +
   2.274 +lemma right_total_rel_filter [transfer_rule]: "right_total A \<Longrightarrow> right_total (rel_filter A)"
   2.275 +using left_total_rel_filter[of "A\<inverse>\<inverse>"] by(simp add: rel_filter_conversep)
   2.276 +
   2.277 +lemma bi_total_rel_filter [transfer_rule]: "bi_total A \<Longrightarrow> bi_total (rel_filter A)"
   2.278 +unfolding bi_total_alt_def by(simp add: left_total_rel_filter right_total_rel_filter)
   2.279 +
   2.280 +lemma left_unique_rel_filter [transfer_rule]: "left_unique A \<Longrightarrow> left_unique (rel_filter A)"
   2.281 +unfolding left_unique_alt_def rel_filter_eq[symmetric] rel_filter_conversep[symmetric] rel_filter_distr
   2.282 +by(rule rel_filter_mono)
   2.283 +
   2.284 +lemma right_unique_rel_filter [transfer_rule]:
   2.285 +  "right_unique A \<Longrightarrow> right_unique (rel_filter A)"
   2.286 +using left_unique_rel_filter[of "A\<inverse>\<inverse>"] by(simp add: rel_filter_conversep)
   2.287 +
   2.288 +lemma bi_unique_rel_filter [transfer_rule]: "bi_unique A \<Longrightarrow> bi_unique (rel_filter A)"
   2.289 +by(simp add: bi_unique_alt_def left_unique_rel_filter right_unique_rel_filter)
   2.290  
   2.291  lemma eventually_parametric [transfer_rule]:
   2.292    "((A ===> (=)) ===> rel_filter A ===> (=)) eventually eventually"
   2.293 -by(simp add: rel_fun_def rel_filter_eventually)
   2.294 -
   2.295 -lemma frequently_parametric [transfer_rule]:
   2.296 -  "((A ===> (=)) ===> rel_filter A ===> (=)) frequently frequently"
   2.297 -  unfolding frequently_def[abs_def] by transfer_prover
   2.298 -
   2.299 -lemma rel_filter_eq [relator_eq]: "rel_filter (=) = (=)"
   2.300 -by(auto simp add: rel_filter_eventually rel_fun_eq fun_eq_iff filter_eq_iff)
   2.301 +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)
   2.302  
   2.303 -lemma rel_filter_mono [relator_mono]:
   2.304 -  "A \<le> B \<Longrightarrow> rel_filter A \<le> rel_filter B"
   2.305 -unfolding rel_filter_eventually[abs_def]
   2.306 -by(rule le_funI)+(intro fun_mono fun_mono[THEN le_funD, THEN le_funD] order.refl)
   2.307 -
   2.308 -lemma rel_filter_conversep [simp]: "rel_filter A\<inverse>\<inverse> = (rel_filter A)\<inverse>\<inverse>"
   2.309 -apply (simp add: rel_filter_eventually fun_eq_iff rel_fun_def)
   2.310 -apply (safe; metis)
   2.311 -done
   2.312 +lemma frequently_parametric [transfer_rule]: "((A ===> (=)) ===> rel_filter A ===> (=)) frequently frequently"
   2.313 +  unfolding frequently_def[abs_def] by transfer_prover
   2.314  
   2.315  lemma is_filter_parametric_aux:
   2.316    assumes "is_filter F"
   2.317 @@ -1474,105 +1676,76 @@
   2.318  apply metis
   2.319  done
   2.320  
   2.321 -lemma left_total_rel_filter [transfer_rule]:
   2.322 -  assumes [transfer_rule]: "bi_total A" "bi_unique A"
   2.323 -  shows "left_total (rel_filter A)"
   2.324 -proof(rule left_totalI)
   2.325 -  fix F :: "'a filter"
   2.326 -  from bi_total_fun[OF bi_unique_fun[OF \<open>bi_total A\<close> bi_unique_eq] bi_total_eq]
   2.327 -  obtain G where [transfer_rule]: "((A ===> (=)) ===> (=)) (\<lambda>P. eventually P F) G"
   2.328 -    unfolding  bi_total_def by blast
   2.329 -  moreover have "is_filter (\<lambda>P. eventually P F) \<longleftrightarrow> is_filter G" by transfer_prover
   2.330 -  hence "is_filter G" by(simp add: eventually_def is_filter_Rep_filter)
   2.331 -  ultimately have "rel_filter A F (Abs_filter G)"
   2.332 -    by(simp add: rel_filter_eventually eventually_Abs_filter)
   2.333 -  thus "\<exists>G. rel_filter A F G" ..
   2.334 +lemma top_filter_parametric [transfer_rule]: "rel_filter A top top" if "bi_total A"
   2.335 +proof
   2.336 +  let ?Z = "principal {(x, y). A x y}"
   2.337 +  show "\<forall>\<^sub>F (x, y) in ?Z. A x y" by(simp add: eventually_principal)
   2.338 +  show "map_filter_on {(x, y). A x y} fst ?Z = top" "map_filter_on {(x, y). A x y} snd ?Z = top"
   2.339 +    using that by(auto simp add: filter_eq_iff eventually_map_filter_on eventually_principal bi_total_def)
   2.340 +qed
   2.341 +
   2.342 +lemma bot_filter_parametric [transfer_rule]: "rel_filter A bot bot"
   2.343 +proof
   2.344 +  show "\<forall>\<^sub>F (x, y) in bot. A x y" by simp
   2.345 +  show "map_filter_on {(x, y). A x y} fst bot = bot" "map_filter_on {(x, y). A x y} snd bot = bot"
   2.346 +    by(simp_all add: filter_eq_iff eventually_map_filter_on)
   2.347  qed
   2.348  
   2.349 -lemma right_total_rel_filter [transfer_rule]:
   2.350 -  "\<lbrakk> bi_total A; bi_unique A \<rbrakk> \<Longrightarrow> right_total (rel_filter A)"
   2.351 -using left_total_rel_filter[of "A\<inverse>\<inverse>"] by simp
   2.352 -
   2.353 -lemma bi_total_rel_filter [transfer_rule]:
   2.354 -  assumes "bi_total A" "bi_unique A"
   2.355 -  shows "bi_total (rel_filter A)"
   2.356 -unfolding bi_total_alt_def using assms
   2.357 -by(simp add: left_total_rel_filter right_total_rel_filter)
   2.358 +lemma principal_parametric [transfer_rule]: "(rel_set A ===> rel_filter A) principal principal"
   2.359 +proof(rule rel_funI rel_filter.intros)+
   2.360 +  fix S S'
   2.361 +  assume *: "rel_set A S S'"
   2.362 +  define SS' where "SS' = S \<times> S' \<inter> {(x, y). A x y}"
   2.363 +  have SS': "SS' \<subseteq> {(x, y). A x y}" and [simp]: "S = fst ` SS'" "S' = snd ` SS'"
   2.364 +    using * by(auto 4 3 dest: rel_setD1 rel_setD2 intro: rev_image_eqI simp add: SS'_def)
   2.365 +  let ?Z = "principal SS'"
   2.366 +  show "\<forall>\<^sub>F (x, y) in ?Z. A x y" using SS' by(auto simp add: eventually_principal)
   2.367 +  then show "map_filter_on {(x, y). A x y} fst ?Z = principal S"
   2.368 +    and "map_filter_on {(x, y). A x y} snd ?Z = principal S'"
   2.369 +    by(auto simp add: filter_eq_iff eventually_map_filter_on eventually_principal)
   2.370 +qed
   2.371  
   2.372 -lemma left_unique_rel_filter [transfer_rule]:
   2.373 -  assumes "left_unique A"
   2.374 -  shows "left_unique (rel_filter A)"
   2.375 -proof(rule left_uniqueI)
   2.376 -  fix F F' G
   2.377 -  assume [transfer_rule]: "rel_filter A F G" "rel_filter A F' G"
   2.378 -  show "F = F'"
   2.379 -    unfolding filter_eq_iff
   2.380 +lemma sup_filter_parametric [transfer_rule]:
   2.381 +  "(rel_filter A ===> rel_filter A ===> rel_filter A) sup sup"
   2.382 +proof(intro rel_funI; elim rel_filter.cases; hypsubst)
   2.383 +  show "rel_filter A
   2.384 +    (map_filter_on {(x, y). A x y} fst FG \<squnion> map_filter_on {(x, y). A x y} fst FG')
   2.385 +    (map_filter_on {(x, y). A x y} snd FG \<squnion> map_filter_on {(x, y). A x y} snd FG')"
   2.386 +    (is "rel_filter _ (sup ?F ?G) (sup ?F' ?G')")
   2.387 +    if "\<forall>\<^sub>F (x, y) in FG. A x y" "\<forall>\<^sub>F (x, y) in FG'. A x y" for FG FG'
   2.388    proof
   2.389 -    fix P :: "'a \<Rightarrow> bool"
   2.390 -    obtain P' where [transfer_rule]: "(A ===> (=)) P P'"
   2.391 -      using left_total_fun[OF assms left_total_eq] unfolding left_total_def by blast
   2.392 -    have "eventually P F = eventually P' G"
   2.393 -      and "eventually P F' = eventually P' G" by transfer_prover+
   2.394 -    thus "eventually P F = eventually P F'" by simp
   2.395 +    let ?Z = "sup FG FG'"
   2.396 +    show "\<forall>\<^sub>F (x, y) in ?Z. A x y" by(simp add: eventually_sup that)
   2.397 +    then show "map_filter_on {(x, y). A x y} fst ?Z = sup ?F ?G" 
   2.398 +      and "map_filter_on {(x, y). A x y} snd ?Z = sup ?F' ?G'"
   2.399 +      by(simp_all add: filter_eq_iff eventually_map_filter_on eventually_sup)
   2.400    qed
   2.401  qed
   2.402  
   2.403 -lemma right_unique_rel_filter [transfer_rule]:
   2.404 -  "right_unique A \<Longrightarrow> right_unique (rel_filter A)"
   2.405 -using left_unique_rel_filter[of "A\<inverse>\<inverse>"] by simp
   2.406 -
   2.407 -lemma bi_unique_rel_filter [transfer_rule]:
   2.408 -  "bi_unique A \<Longrightarrow> bi_unique (rel_filter A)"
   2.409 -by(simp add: bi_unique_alt_def left_unique_rel_filter right_unique_rel_filter)
   2.410 -
   2.411 -lemma top_filter_parametric [transfer_rule]:
   2.412 -  "bi_total A \<Longrightarrow> (rel_filter A) top top"
   2.413 -by(simp add: rel_filter_eventually All_transfer)
   2.414 -
   2.415 -lemma bot_filter_parametric [transfer_rule]: "(rel_filter A) bot bot"
   2.416 -by(simp add: rel_filter_eventually rel_fun_def)
   2.417 -
   2.418 -lemma sup_filter_parametric [transfer_rule]:
   2.419 -  "(rel_filter A ===> rel_filter A ===> rel_filter A) sup sup"
   2.420 -by(fastforce simp add: rel_filter_eventually[abs_def] eventually_sup dest: rel_funD)
   2.421 -
   2.422 -lemma Sup_filter_parametric [transfer_rule]:
   2.423 -  "(rel_set (rel_filter A) ===> rel_filter A) Sup Sup"
   2.424 -proof(rule rel_funI)
   2.425 -  fix S T
   2.426 -  assume [transfer_rule]: "rel_set (rel_filter A) S T"
   2.427 -  show "rel_filter A (Sup S) (Sup T)"
   2.428 -    by(simp add: rel_filter_eventually eventually_Sup) transfer_prover
   2.429 -qed
   2.430 -
   2.431 -lemma principal_parametric [transfer_rule]:
   2.432 -  "(rel_set A ===> rel_filter A) principal principal"
   2.433 +lemma Sup_filter_parametric [transfer_rule]: "(rel_set (rel_filter A) ===> rel_filter A) Sup Sup"
   2.434  proof(rule rel_funI)
   2.435    fix S S'
   2.436 -  assume [transfer_rule]: "rel_set A S S'"
   2.437 -  show "rel_filter A (principal S) (principal S')"
   2.438 -    by(simp add: rel_filter_eventually eventually_principal) transfer_prover
   2.439 -qed
   2.440 -  
   2.441 -lemma filtermap_parametric [transfer_rule]:
   2.442 -  "((A ===> B) ===> rel_filter A ===> rel_filter B) filtermap filtermap"
   2.443 -proof (intro rel_funI)
   2.444 -  fix f g F G assume [transfer_rule]: "(A ===> B) f g" "rel_filter A F G"
   2.445 -  show "rel_filter B (filtermap f F) (filtermap g G)"
   2.446 -    unfolding rel_filter_eventually eventually_filtermap by transfer_prover
   2.447 +  define SS' where "SS' = S \<times> S' \<inter> {(F, G). rel_filter A F G}"
   2.448 +  assume "rel_set (rel_filter A) S S'"
   2.449 +  then have SS': "SS' \<subseteq> {(F, G). rel_filter A F G}" and [simp]: "S = fst ` SS'" "S' = snd ` SS'"
   2.450 +    by(auto 4 3 dest: rel_setD1 rel_setD2 intro: rev_image_eqI simp add: SS'_def)
   2.451 +  from SS' obtain Z where Z: "\<And>F G. (F, G) \<in> SS' \<Longrightarrow>
   2.452 +    (\<forall>\<^sub>F (x, y) in Z F G. A x y) \<and>
   2.453 +    id F = map_filter_on {(x, y). A x y} fst (Z F G) \<and>
   2.454 +    id G = map_filter_on {(x, y). A x y} snd (Z F G)"
   2.455 +    unfolding rel_filter.simps by atomize_elim((rule choice allI)+; auto)
   2.456 +  have id: "eventually P F = eventually P (id F)" "eventually Q G = eventually Q (id G)"
   2.457 +    if "(F, G) \<in> SS'" for P Q F G by simp_all
   2.458 +  show "rel_filter A (Sup S) (Sup S')"
   2.459 +  proof
   2.460 +    let ?Z = "SUP (F, G):SS'. Z F G"
   2.461 +    show *: "\<forall>\<^sub>F (x, y) in ?Z. A x y" using Z by(auto simp add: eventually_Sup)
   2.462 +    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'"
   2.463 +      unfolding filter_eq_iff
   2.464 +      by(auto 4 4 simp add: id eventually_Sup eventually_map_filter_on *[simplified eventually_Sup] simp del: id_apply dest: Z)
   2.465 +  qed
   2.466  qed
   2.467  
   2.468 -(* TODO: Are those assumptions needed? *)
   2.469 -lemma filtercomap_parametric [transfer_rule]:
   2.470 -  assumes [transfer_rule]: "bi_unique B" "bi_total A"
   2.471 -  shows   "((A ===> B) ===> rel_filter B ===> rel_filter A) filtercomap filtercomap"
   2.472 -proof (intro rel_funI)
   2.473 -  fix f g F G assume [transfer_rule]: "(A ===> B) f g" "rel_filter B F G"
   2.474 -  show "rel_filter A (filtercomap f F) (filtercomap g G)"
   2.475 -    unfolding rel_filter_eventually eventually_filtercomap by transfer_prover
   2.476 -qed
   2.477 -    
   2.478 -
   2.479  context
   2.480    fixes A :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
   2.481    assumes [transfer_rule]: "bi_unique A"