author Andreas Lochbihler Fri Feb 16 10:59:14 2018 +0100 (23 months ago ago) changeset 67615 1d005f514417 parent 67614 560fbd6bc047 child 67618 9f9f64fe1705
strengthen filter relator to canonical categorical definition with better properties
 NEWS file | annotate | diff | revisions src/HOL/Filter.thy file | annotate | diff | revisions
```     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.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.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.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.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.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.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.414 -
2.415 -lemma bot_filter_parametric [transfer_rule]: "(rel_filter A) bot bot"
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"
```