# HG changeset patch
# User Andreas Lochbihler
# Date 1532074199 -7200
# Node ID 96aae7c44bb2159ae0748039dc60f1531f6a71fe
# Parent  4bee4828cfc318ad7c25487baa608e6bbe24e173
add lemmas about prod_filter

diff -r 4bee4828cfc3 -r 96aae7c44bb2 src/HOL/Filter.thy
--- a/src/HOL/Filter.thy	Fri Jul 20 09:05:34 2018 +0200
+++ b/src/HOL/Filter.thy	Fri Jul 20 10:09:59 2018 +0200
@@ -1104,6 +1104,34 @@
 lemma prod_filter_INF2: "J \<noteq> {} \<Longrightarrow> A \<times>\<^sub>F (\<Sqinter>i\<in>J. B i) = (\<Sqinter>i\<in>J. A \<times>\<^sub>F B i)"
   using prod_filter_INF[of "{A}" J "\<lambda>x. x" B] by simp
 
+lemma prod_filtermap1: "prod_filter (filtermap f F) G = filtermap (apfst f) (prod_filter F G)"
+  apply(clarsimp simp add: filter_eq_iff eventually_filtermap eventually_prod_filter; safe)
+  subgoal by auto
+  subgoal for P Q R by(rule exI[where x="\<lambda>y. \<exists>x. y = f x \<and> Q x"])(auto intro: eventually_mono)
+  done
+
+lemma prod_filtermap2: "prod_filter F (filtermap g G) = filtermap (apsnd g) (prod_filter F G)"
+  apply(clarsimp simp add: filter_eq_iff eventually_filtermap eventually_prod_filter; safe)
+  subgoal by auto
+  subgoal for P Q R  by(auto intro: exI[where x="\<lambda>y. \<exists>x. y = g x \<and> R x"] eventually_mono)
+  done
+
+lemma prod_filter_assoc:
+  "prod_filter (prod_filter F G) H = filtermap (\<lambda>(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="\<lambda>(a, b). T a \<and> S b"])
+  subgoal for P Q R S T by(auto 4 3 intro: exI[where x="\<lambda>(a, b). Q a \<and> 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="\<lambda>a. a = x"])
+
+lemma prod_filter_principal_singleton2: "prod_filter F (principal {x}) = filtermap (\<lambda>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="\<lambda>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 \<open>Limits\<close>
 
 definition filterlim :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b filter \<Rightarrow> 'a filter \<Rightarrow> bool" where
@@ -1699,6 +1727,50 @@
 
 end
 
+lemma prod_filter_parametric [transfer_rule]: includes lifting_syntax shows
+   "(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: "\<forall>\<^sub>F (x, y) in F. R x y" and G: "\<forall>\<^sub>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 \<times>\<^sub>F map_filter_on {(x, y). S x y} fst G)
+    (map_filter_on {(x, y). R x y} snd F \<times>\<^sub>F map_filter_on {(x, y). S x y} snd G)"
+    (is "rel_filter ?RS ?F ?G")
+  proof
+    let ?Z = "filtermap (\<lambda>((a, b), (a', b')). ((a, a'), (b, b'))) (prod_filter F G)"
+    show *: "\<forall>\<^sub>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="\<lambda>a. \<exists>b. P' (a, b) \<and> R a b"]; rule conjI)
+        subgoal by(fastforce elim: eventually_rev_mp eventually_mono)
+        subgoal
+          by(rule exI[where x="\<lambda>a. \<exists>b. P'' (a, b) \<and> 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="\<lambda>b. \<exists>a. P' (a, b) \<and> R a b"]; rule conjI)
+        subgoal by(fastforce elim: eventually_rev_mp eventually_mono)
+        subgoal
+          by(rule exI[where x="\<lambda>b. \<exists>a. P'' (a, b) \<and> S a b"])(fastforce elim: eventually_rev_mp eventually_mono)
+        done
+      subgoal by fastforce
+      done
+  qed
+qed
+
 text \<open>Code generation for filters\<close>
 
 definition abstract_filter :: "(unit \<Rightarrow> 'a filter) \<Rightarrow> 'a filter"