# HG changeset patch
# User Lars Hupel <lars.hupel@mytum.de>
# Date 1518788480 -3600
# Node ID 37ba3d234fbfd9ce15a6af9d7b9f733ddd7d0e26
# Parent  3107dcea3493f5d6f0ca489ec939386c4f00dc2e# Parent  9f9f64fe170582c5cb02004c9ff6d5c83c6264ab
merged

diff -r 3107dcea3493 -r 37ba3d234fbf NEWS
--- a/NEWS	Fri Feb 16 11:03:17 2018 +0100
+++ b/NEWS	Fri Feb 16 14:41:20 2018 +0100
@@ -210,6 +210,9 @@
 * Predicate pairwise_coprime abolished, use "pairwise coprime" instead.
 INCOMPATIBILITY.
 
+* The relator rel_filter on filters has been strengthened to its 
+canonical categorical definition with better properties. INCOMPATIBILITY.
+
 * HOL-Algebra: renamed (^) to [^]
 
 * Session HOL-Analysis: Moebius functions and the Riemann mapping
diff -r 3107dcea3493 -r 37ba3d234fbf src/HOL/Filter.thy
--- a/src/HOL/Filter.thy	Fri Feb 16 11:03:17 2018 +0100
+++ b/src/HOL/Filter.thy	Fri Feb 16 14:41:20 2018 +0100
@@ -1368,65 +1368,267 @@
 
 subsection \<open>Setup @{typ "'a filter"} for lifting and transfer\<close>
 
-context includes lifting_syntax
-begin
-
-definition rel_filter :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> 'b filter \<Rightarrow> bool"
-where "rel_filter R F G = ((R ===> (=)) ===> (=)) (Rep_filter F) (Rep_filter G)"
-
-lemma rel_filter_eventually:
-  "rel_filter R F G \<longleftrightarrow>
-  ((R ===> (=)) ===> (=)) (\<lambda>P. eventually P F) (\<lambda>P. eventually P G)"
-by(simp add: rel_filter_def eventually_def)
-
 lemma filtermap_id [simp, id_simps]: "filtermap id = id"
 by(simp add: fun_eq_iff id_def filtermap_ident)
 
 lemma filtermap_id' [simp]: "filtermap (\<lambda>x. x) = (\<lambda>F. F)"
 using filtermap_id unfolding id_def .
 
-lemma Quotient_filter [quot_map]:
-  assumes Q: "Quotient R Abs Rep T"
-  shows "Quotient (rel_filter R) (filtermap Abs) (filtermap Rep) (rel_filter T)"
-unfolding Quotient_alt_def
-proof(intro conjI strip)
-  from Q have *: "\<And>x y. T x y \<Longrightarrow> Abs x = y"
-    unfolding Quotient_alt_def by blast
+context includes lifting_syntax
+begin
+
+definition map_filter_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a filter \<Rightarrow> 'b filter" where
+  "map_filter_on X f F = Abs_filter (\<lambda>P. eventually (\<lambda>x. P (f x) \<and> x \<in> X) F)"
+
+lemma is_filter_map_filter_on:
+  "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"
+proof(rule iffI; unfold_locales)
+  show "\<forall>\<^sub>F x in F. True \<and> x \<in> X" if "eventually (\<lambda>x. x \<in> X) F" using that by simp
+  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
+    using eventually_conj[OF that] by(auto simp add: conj_ac cong: conj_cong)
+  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
+    using that(2) by(rule eventually_mono)(use that(1) in auto)
+  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)"
+    using is_filter.True[OF that] by simp
+qed
+
+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)"
+  if "eventually (\<lambda>x. x \<in> 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 \<circ> g) F"
+  if "g ` Y \<subseteq> X" and "eventually (\<lambda>x. x \<in> 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 \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> 'b filter \<Rightarrow> 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 \<open>F = G\<close>
+  proof
+    let ?Z = "map_filter_on UNIV (\<lambda>x. (x, x)) G"
+    have [simp]: "range (\<lambda>x. (x, x)) \<subseteq> {(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 "\<forall>\<^sub>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 \<le> rel_filter B" if le: "A \<le> 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 "\<forall>\<^sub>F (x, y) in Z. A x y" for Z
+  proof
+    let ?Z = "map_filter_on {(x, y). A x y} id Z"
+    show "\<forall>\<^sub>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} \<subseteq> {(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\<inverse>\<inverse> = (rel_filter A)\<inverse>\<inverse>"
+proof(safe intro!: ext elim!: rel_filter.cases)
+  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)"
+    (is "rel_filter _ ?X ?Y") if "\<forall>\<^sub>F (x, y) in Z. A\<inverse>\<inverse> x y" for A Z
+  proof
+    let ?Z = "map_filter_on {(x, y). A y x} prod.swap Z"
+    show "\<forall>\<^sub>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} \<subseteq> {(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\<inverse>\<inverse> (map_filter_on {(x, y). A x y} snd Z) (map_filter_on {(x, y). A x y} fst Z)"
+    if "\<forall>\<^sub>F (x, y) in Z. A x y" for Z using *[of "A\<inverse>\<inverse>" 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 "\<forall>\<^sub>F (x, y) in Z. (A OO B) x y" for Z
+  proof
+    let ?G = "map_filter_on ?AB (\<lambda>(x, y). SOME z. A x z \<and> B z y) Z"
+    show "rel_filter A ?F ?G"
+    proof
+      let ?Z = "map_filter_on ?AB (\<lambda>(x, y). (x, SOME z. A x z \<and> B z y)) Z"
+      show "\<forall>\<^sub>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]: "(\<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)
+      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 (\<lambda>(x, y). (SOME z. A x z \<and> B z y, y)) Z"
+      show "\<forall>\<^sub>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]: "(\<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)
+      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 "rel_filter T F G"
-  thus "filtermap Abs F = G" unfolding filter_eq_iff
-    by(auto simp add: eventually_filtermap rel_filter_eventually * rel_funI del: iffI elim!: rel_funD)
-next
-  from Q have *: "\<And>x. T (Rep x) x" unfolding Quotient_alt_def by blast
+  assume F: "\<forall>\<^sub>F (x, y) in F. A x y" and G: "\<forall>\<^sub>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: "\<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)}"
+    if P: "eventually P F" and Q: "eventually Q G" for P Q
+  proof -
+    let ?P = "\<lambda>(x, y). P (x, y) \<and> A x y" and ?Q = "\<lambda>(y, z). Q (y, z) \<and> B y z"
+    define P' where "P' \<equiv> \<lambda>(x, y). ?P (x, y) \<and> (\<exists>z. ?Q (y, z))"
+    define Q' where "Q' \<equiv> \<lambda>(y, z). ?Q (y, z) \<and> (\<exists>x. ?P (x, y))"
+    have "P' \<le> P" "Q' \<le> Q" "{y. \<exists>x. P' (x, y)} = {y. \<exists>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 "\<forall>\<^sub>F y in ?Y1. \<exists>x. P (x, y) \<and> 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. \<exists>z. Q'' (y, z)} \<subseteq> {y. \<exists>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 "\<forall>\<^sub>F y in ?Y2. \<exists>z. Q (y, z) \<and> 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. \<exists>x. P'' (x, y)} \<subseteq> {y. \<exists>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 = "\<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"
+    have Y: "is_filter ?Y"
+    proof
+      show "?Y (\<lambda>_. True)" by(auto simp add: le_fun_def intro: eventually_True)
+      show "?Y (\<lambda>x. P x \<and> 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" "\<forall>x. P x \<longrightarrow> Q x" for P Q using that by blast
+    qed
+    define Y where "Y = Abs_filter ?Y"
+    have eventually_Y: "eventually P Y \<longleftrightarrow> ?Y P" for P
+      using eventually_Abs_filter[OF Y, of P] by(simp add: Y_def)
+    show YY: "\<forall>\<^sub>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 (\<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
+    proof
+      show ?lhs if ?rhs using G F that
+        by(auto 4 3 intro: exI[where x="\<lambda>_. True"] simp add: eventually_map_filter_on split_def)
+      assume ?lhs
+      then obtain X Z where "\<forall>\<^sub>F (x, y) in F. X x \<and> A x y"
+        and "\<forall>\<^sub>F (x, y) in G. Z y \<and> B x y"
+        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)"
+        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)
 
-  fix F
-  show "rel_filter T (filtermap Rep F) F"
-    by(auto elim: rel_funD intro: * intro!: ext arg_cong[where f="\<lambda>P. eventually P F"] rel_funI
-            del: iffI simp add: eventually_filtermap rel_filter_eventually)
-qed(auto simp add: map_fun_def o_def eventually_filtermap filter_eq_iff fun_eq_iff rel_filter_eventually
-         fun_quotient[OF fun_quotient[OF Q identity_quotient] identity_quotient, unfolded Quotient_alt_def])
+    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
+    proof
+      show ?lhs if ?rhs using G F that
+        by(auto 4 3 intro: exI[where x="\<lambda>_. True"] simp add: eventually_map_filter_on split_def)
+      assume ?lhs
+      then obtain X Z where "\<forall>\<^sub>F (x, y) in F. X x \<and> A x y"
+        and "\<forall>\<^sub>F (x, y) in G. Z y \<and> B x y"
+        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)"
+        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: "\<forall>\<^sub>F (x, y) in Z. A x y"
+  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)"
+    (is "rel_filter _ ?F ?G")
+  proof
+    let ?Z = "map_filter_on {(x, y). A x y} (map_prod f g) Z"
+    show "\<forall>\<^sub>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)} \<subseteq> {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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> right_total (rel_filter A)"
+using left_total_rel_filter[of "A\<inverse>\<inverse>"] by(simp add: rel_filter_conversep)
+
+lemma bi_total_rel_filter [transfer_rule]: "bi_total A \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> right_unique (rel_filter A)"
+using left_unique_rel_filter[of "A\<inverse>\<inverse>"] by(simp add: rel_filter_conversep)
+
+lemma bi_unique_rel_filter [transfer_rule]: "bi_unique A \<Longrightarrow> 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(simp add: rel_fun_def rel_filter_eventually)
-
-lemma frequently_parametric [transfer_rule]:
-  "((A ===> (=)) ===> rel_filter A ===> (=)) frequently frequently"
-  unfolding frequently_def[abs_def] by transfer_prover
-
-lemma rel_filter_eq [relator_eq]: "rel_filter (=) = (=)"
-by(auto simp add: rel_filter_eventually rel_fun_eq fun_eq_iff filter_eq_iff)
+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 rel_filter_mono [relator_mono]:
-  "A \<le> B \<Longrightarrow> rel_filter A \<le> rel_filter B"
-unfolding rel_filter_eventually[abs_def]
-by(rule le_funI)+(intro fun_mono fun_mono[THEN le_funD, THEN le_funD] order.refl)
-
-lemma rel_filter_conversep [simp]: "rel_filter A\<inverse>\<inverse> = (rel_filter A)\<inverse>\<inverse>"
-apply (simp add: rel_filter_eventually fun_eq_iff rel_fun_def)
-apply (safe; metis)
-done
+lemma frequently_parametric [transfer_rule]: "((A ===> (=)) ===> rel_filter A ===> (=)) frequently frequently"
+  unfolding frequently_def[abs_def] by transfer_prover
 
 lemma is_filter_parametric_aux:
   assumes "is_filter F"
@@ -1474,105 +1676,76 @@
 apply metis
 done
 
-lemma left_total_rel_filter [transfer_rule]:
-  assumes [transfer_rule]: "bi_total A" "bi_unique A"
-  shows "left_total (rel_filter A)"
-proof(rule left_totalI)
-  fix F :: "'a filter"
-  from bi_total_fun[OF bi_unique_fun[OF \<open>bi_total A\<close> bi_unique_eq] bi_total_eq]
-  obtain G where [transfer_rule]: "((A ===> (=)) ===> (=)) (\<lambda>P. eventually P F) G"
-    unfolding  bi_total_def by blast
-  moreover have "is_filter (\<lambda>P. eventually P F) \<longleftrightarrow> is_filter G" by transfer_prover
-  hence "is_filter G" by(simp add: eventually_def is_filter_Rep_filter)
-  ultimately have "rel_filter A F (Abs_filter G)"
-    by(simp add: rel_filter_eventually eventually_Abs_filter)
-  thus "\<exists>G. rel_filter A F G" ..
+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 "\<forall>\<^sub>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 "\<forall>\<^sub>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 right_total_rel_filter [transfer_rule]:
-  "\<lbrakk> bi_total A; bi_unique A \<rbrakk> \<Longrightarrow> right_total (rel_filter A)"
-using left_total_rel_filter[of "A\<inverse>\<inverse>"] by simp
-
-lemma bi_total_rel_filter [transfer_rule]:
-  assumes "bi_total A" "bi_unique A"
-  shows "bi_total (rel_filter A)"
-unfolding bi_total_alt_def using assms
-by(simp add: left_total_rel_filter right_total_rel_filter)
+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 \<times> S' \<inter> {(x, y). A x y}"
+  have SS': "SS' \<subseteq> {(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 "\<forall>\<^sub>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 left_unique_rel_filter [transfer_rule]:
-  assumes "left_unique A"
-  shows "left_unique (rel_filter A)"
-proof(rule left_uniqueI)
-  fix F F' G
-  assume [transfer_rule]: "rel_filter A F G" "rel_filter A F' G"
-  show "F = F'"
-    unfolding filter_eq_iff
+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 \<squnion> map_filter_on {(x, y). A x y} fst FG')
+    (map_filter_on {(x, y). A x y} snd FG \<squnion> map_filter_on {(x, y). A x y} snd FG')"
+    (is "rel_filter _ (sup ?F ?G) (sup ?F' ?G')")
+    if "\<forall>\<^sub>F (x, y) in FG. A x y" "\<forall>\<^sub>F (x, y) in FG'. A x y" for FG FG'
   proof
-    fix P :: "'a \<Rightarrow> bool"
-    obtain P' where [transfer_rule]: "(A ===> (=)) P P'"
-      using left_total_fun[OF assms left_total_eq] unfolding left_total_def by blast
-    have "eventually P F = eventually P' G"
-      and "eventually P F' = eventually P' G" by transfer_prover+
-    thus "eventually P F = eventually P F'" by simp
+    let ?Z = "sup FG FG'"
+    show "\<forall>\<^sub>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 right_unique_rel_filter [transfer_rule]:
-  "right_unique A \<Longrightarrow> right_unique (rel_filter A)"
-using left_unique_rel_filter[of "A\<inverse>\<inverse>"] by simp
-
-lemma bi_unique_rel_filter [transfer_rule]:
-  "bi_unique A \<Longrightarrow> bi_unique (rel_filter A)"
-by(simp add: bi_unique_alt_def left_unique_rel_filter right_unique_rel_filter)
-
-lemma top_filter_parametric [transfer_rule]:
-  "bi_total A \<Longrightarrow> (rel_filter A) top top"
-by(simp add: rel_filter_eventually All_transfer)
-
-lemma bot_filter_parametric [transfer_rule]: "(rel_filter A) bot bot"
-by(simp add: rel_filter_eventually rel_fun_def)
-
-lemma sup_filter_parametric [transfer_rule]:
-  "(rel_filter A ===> rel_filter A ===> rel_filter A) sup sup"
-by(fastforce simp add: rel_filter_eventually[abs_def] eventually_sup dest: rel_funD)
-
-lemma Sup_filter_parametric [transfer_rule]:
-  "(rel_set (rel_filter A) ===> rel_filter A) Sup Sup"
-proof(rule rel_funI)
-  fix S T
-  assume [transfer_rule]: "rel_set (rel_filter A) S T"
-  show "rel_filter A (Sup S) (Sup T)"
-    by(simp add: rel_filter_eventually eventually_Sup) transfer_prover
-qed
-
-lemma principal_parametric [transfer_rule]:
-  "(rel_set A ===> rel_filter A) principal principal"
+lemma Sup_filter_parametric [transfer_rule]: "(rel_set (rel_filter A) ===> rel_filter A) Sup Sup"
 proof(rule rel_funI)
   fix S S'
-  assume [transfer_rule]: "rel_set A S S'"
-  show "rel_filter A (principal S) (principal S')"
-    by(simp add: rel_filter_eventually eventually_principal) transfer_prover
-qed
-  
-lemma filtermap_parametric [transfer_rule]:
-  "((A ===> B) ===> rel_filter A ===> rel_filter B) filtermap filtermap"
-proof (intro rel_funI)
-  fix f g F G assume [transfer_rule]: "(A ===> B) f g" "rel_filter A F G"
-  show "rel_filter B (filtermap f F) (filtermap g G)"
-    unfolding rel_filter_eventually eventually_filtermap by transfer_prover
+  define SS' where "SS' = S \<times> S' \<inter> {(F, G). rel_filter A F G}"
+  assume "rel_set (rel_filter A) S S'"
+  then have SS': "SS' \<subseteq> {(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: "\<And>F G. (F, G) \<in> SS' \<Longrightarrow>
+    (\<forall>\<^sub>F (x, y) in Z F G. A x y) \<and>
+    id F = map_filter_on {(x, y). A x y} fst (Z F G) \<and>
+    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) \<in> SS'" for P Q F G by simp_all
+  show "rel_filter A (Sup S) (Sup S')"
+  proof
+    let ?Z = "SUP (F, G):SS'. Z F G"
+    show *: "\<forall>\<^sub>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
 
-(* TODO: Are those assumptions needed? *)
-lemma filtercomap_parametric [transfer_rule]:
-  assumes [transfer_rule]: "bi_unique B" "bi_total A"
-  shows   "((A ===> B) ===> rel_filter B ===> rel_filter A) filtercomap filtercomap"
-proof (intro rel_funI)
-  fix f g F G assume [transfer_rule]: "(A ===> B) f g" "rel_filter B F G"
-  show "rel_filter A (filtercomap f F) (filtercomap g G)"
-    unfolding rel_filter_eventually eventually_filtercomap by transfer_prover
-qed
-    
-
 context
   fixes A :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
   assumes [transfer_rule]: "bi_unique A"