diff -r 95c6cf433c91 -r d2bc8a7e5fec src/HOL/Filter.thy
--- a/src/HOL/Filter.thy	Thu Feb 18 17:53:09 2016 +0100
+++ b/src/HOL/Filter.thy	Mon Feb 08 17:18:13 2016 +0100
@@ -479,6 +479,29 @@
     eventually P (INF b:B. F b) \<longleftrightarrow> (\<exists>b\<in>B. eventually P (F b))"
   by (subst eventually_Inf_base) auto
 
+lemma eventually_INF_mono:
+  assumes *: "\<forall>\<^sub>F x in \<Sqinter>i\<in>I. F i. P x"
+  assumes T1: "\<And>Q R P. (\<And>x. Q x \<and> R x \<longrightarrow> P x) \<Longrightarrow> (\<And>x. T Q x \<Longrightarrow> T R x \<Longrightarrow> T P x)"
+  assumes T2: "\<And>P. (\<And>x. P x) \<Longrightarrow> (\<And>x. T P x)"
+  assumes **: "\<And>i P. i \<in> I \<Longrightarrow> \<forall>\<^sub>F x in F i. P x \<Longrightarrow> \<forall>\<^sub>F x in F' i. T P x"
+  shows "\<forall>\<^sub>F x in \<Sqinter>i\<in>I. F' i. T P x"
+proof -
+  from * obtain X where "finite X" "X \<subseteq> I" "\<forall>\<^sub>F x in \<Sqinter>i\<in>X. F i. P x"
+    unfolding eventually_INF[of _ I] by auto
+  moreover then have "eventually (T P) (INFIMUM X F')"
+    apply (induction X arbitrary: P)
+    apply (auto simp: eventually_inf T2)
+    subgoal for x S P Q R
+      apply (intro exI[of _ "T Q"])
+      apply (auto intro!: **) []
+      apply (intro exI[of _ "T R"])
+      apply (auto intro: T1) []
+      done
+    done
+  ultimately show "\<forall>\<^sub>F x in \<Sqinter>i\<in>I. F' i. T P x"
+    by (subst eventually_INF) auto
+qed
+
 
 subsubsection \<open>Map function for filters\<close>
 
@@ -530,7 +553,6 @@
     by (subst (1 2) eventually_INF) auto
 qed
 
-
 subsubsection \<open>Standard filters\<close>
 
 definition principal :: "'a set \<Rightarrow> 'a filter" where
@@ -768,9 +790,116 @@
     by auto
 qed (auto simp: eventually_principal intro: eventually_True)
 
+lemma eventually_prod1:
+  assumes "B \<noteq> bot"
+  shows "(\<forall>\<^sub>F (x, y) in A \<times>\<^sub>F B. P x) \<longleftrightarrow> (\<forall>\<^sub>F x in A. P x)"
+  unfolding eventually_prod_filter
+proof safe
+  fix R Q assume "\<forall>\<^sub>F x in A. R x" "\<forall>\<^sub>F x in B. Q x" "\<forall>x y. R x \<longrightarrow> Q y \<longrightarrow> P x"
+  moreover with \<open>B \<noteq> bot\<close> obtain y where "Q y" by (auto dest: eventually_happens)
+  ultimately show "eventually P A"
+    by (force elim: eventually_mono)
+next
+  assume "eventually P A"
+  then show "\<exists>Pf Pg. eventually Pf A \<and> eventually Pg B \<and> (\<forall>x y. Pf x \<longrightarrow> Pg y \<longrightarrow> P x)"
+    by (intro exI[of _ P] exI[of _ "\<lambda>x. True"]) auto
+qed
+
+lemma eventually_prod2:
+  assumes "A \<noteq> bot"
+  shows "(\<forall>\<^sub>F (x, y) in A \<times>\<^sub>F B. P y) \<longleftrightarrow> (\<forall>\<^sub>F y in B. P y)"
+  unfolding eventually_prod_filter
+proof safe
+  fix R Q assume "\<forall>\<^sub>F x in A. R x" "\<forall>\<^sub>F x in B. Q x" "\<forall>x y. R x \<longrightarrow> Q y \<longrightarrow> P y"
+  moreover with \<open>A \<noteq> bot\<close> obtain x where "R x" by (auto dest: eventually_happens)
+  ultimately show "eventually P B"
+    by (force elim: eventually_mono)
+next
+  assume "eventually P B"
+  then show "\<exists>Pf Pg. eventually Pf A \<and> eventually Pg B \<and> (\<forall>x y. Pf x \<longrightarrow> Pg y \<longrightarrow> P y)"
+    by (intro exI[of _ P] exI[of _ "\<lambda>x. True"]) auto
+qed
+
+lemma INF_filter_bot_base:
+  fixes F :: "'a \<Rightarrow> 'b filter"
+  assumes *: "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> \<exists>k\<in>I. F k \<le> F i \<sqinter> F j"
+  shows "(INF i:I. F i) = bot \<longleftrightarrow> (\<exists>i\<in>I. F i = bot)"
+proof cases
+  assume "\<exists>i\<in>I. F i = bot"
+  moreover then have "(INF i:I. F i) \<le> bot"
+    by (auto intro: INF_lower2)
+  ultimately show ?thesis
+    by (auto simp: bot_unique)
+next
+  assume **: "\<not> (\<exists>i\<in>I. F i = bot)"
+  moreover have "(INF i:I. F i) \<noteq> bot"
+  proof cases
+    assume "I \<noteq> {}"
+    show ?thesis
+    proof (rule INF_filter_not_bot)
+      fix J assume "finite J" "J \<subseteq> I"
+      then have "\<exists>k\<in>I. F k \<le> (\<Sqinter>i\<in>J. F i)"
+      proof (induction J)
+        case empty then show ?case
+          using \<open>I \<noteq> {}\<close> by auto
+      next
+        case (insert i J)
+        moreover then obtain k where "k \<in> I" "F k \<le> (\<Sqinter>i\<in>J. F i)" by auto
+        moreover note *[of i k]
+        ultimately show ?case
+          by auto
+      qed
+      with ** show "(\<Sqinter>i\<in>J. F i) \<noteq> \<bottom>"
+        by (auto simp: bot_unique)
+    qed
+  qed (auto simp add: filter_eq_iff)
+  ultimately show ?thesis
+    by auto
+qed
+
+lemma Collect_empty_eq_bot: "Collect P = {} \<longleftrightarrow> P = \<bottom>"
+  by auto
+
+lemma prod_filter_eq_bot: "A \<times>\<^sub>F B = bot \<longleftrightarrow> A = bot \<or> B = bot"
+  unfolding prod_filter_def
+proof (subst INF_filter_bot_base; clarsimp simp: principal_eq_bot_iff Collect_empty_eq_bot bot_fun_def simp del: Collect_empty_eq)
+  fix A1 A2 B1 B2 assume "\<forall>\<^sub>F x in A. A1 x" "\<forall>\<^sub>F x in A. A2 x" "\<forall>\<^sub>F x in B. B1 x" "\<forall>\<^sub>F x in B. B2 x"
+  then show "\<exists>x. eventually x A \<and> (\<exists>y. eventually y B \<and> Collect x \<times> Collect y \<subseteq> Collect A1 \<times> Collect B1 \<and> Collect x \<times> Collect y \<subseteq> Collect A2 \<times> Collect B2)"
+    by (intro exI[of _ "\<lambda>x. A1 x \<and> A2 x"] exI[of _ "\<lambda>x. B1 x \<and> B2 x"] conjI)
+       (auto simp: eventually_conj_iff)
+next
+  show "(\<exists>x. eventually x A \<and> (\<exists>y. eventually y B \<and> (x = (\<lambda>x. False) \<or> y = (\<lambda>x. False)))) = (A = \<bottom> \<or> B = \<bottom>)"
+    by (auto simp: trivial_limit_def intro: eventually_True)
+qed
+
 lemma prod_filter_mono: "F \<le> F' \<Longrightarrow> G \<le> G' \<Longrightarrow> F \<times>\<^sub>F G \<le> F' \<times>\<^sub>F G'"
   by (auto simp: le_filter_def eventually_prod_filter)
 
+lemma prod_filter_mono_iff:
+  assumes nAB: "A \<noteq> bot" "B \<noteq> bot"
+  shows "A \<times>\<^sub>F B \<le> C \<times>\<^sub>F D \<longleftrightarrow> A \<le> C \<and> B \<le> D"
+proof safe
+  assume *: "A \<times>\<^sub>F B \<le> C \<times>\<^sub>F D"
+  moreover with assms have "A \<times>\<^sub>F B \<noteq> bot"
+    by (auto simp: bot_unique prod_filter_eq_bot)
+  ultimately have "C \<times>\<^sub>F D \<noteq> bot"
+    by (auto simp: bot_unique)
+  then have nCD: "C \<noteq> bot" "D \<noteq> bot"
+    by (auto simp: prod_filter_eq_bot)
+
+  show "A \<le> C"
+  proof (rule filter_leI)
+    fix P assume "eventually P C" with *[THEN filter_leD, of "\<lambda>(x, y). P x"] show "eventually P A"
+      using nAB nCD by (simp add: eventually_prod1 eventually_prod2)
+  qed
+
+  show "B \<le> D"
+  proof (rule filter_leI)
+    fix P assume "eventually P D" with *[THEN filter_leD, of "\<lambda>(x, y). P y"] show "eventually P B"
+      using nAB nCD by (simp add: eventually_prod1 eventually_prod2)
+  qed
+qed (intro prod_filter_mono)
+
 lemma eventually_prod_same: "eventually P (F \<times>\<^sub>F F) \<longleftrightarrow>
     (\<exists>Q. eventually Q F \<and> (\<forall>x y. Q x \<longrightarrow> Q y \<longrightarrow> P (x, y)))"
   unfolding eventually_prod_filter
@@ -791,6 +920,52 @@
   apply auto
   done
 
+lemma prod_filter_INF:
+  assumes "I \<noteq> {}" "J \<noteq> {}"
+  shows "(INF i:I. A i) \<times>\<^sub>F (INF j:J. B j) = (INF i:I. INF j:J. A i \<times>\<^sub>F B j)"
+proof (safe intro!: antisym INF_greatest)
+  from \<open>I \<noteq> {}\<close> obtain i where "i \<in> I" by auto
+  from \<open>J \<noteq> {}\<close> obtain j where "j \<in> J" by auto
+
+  show "(\<Sqinter>i\<in>I. \<Sqinter>j\<in>J. A i \<times>\<^sub>F B j) \<le> (\<Sqinter>i\<in>I. A i) \<times>\<^sub>F (\<Sqinter>j\<in>J. B j)"
+    unfolding prod_filter_def
+  proof (safe intro!: INF_greatest)
+    fix P Q assume P: "\<forall>\<^sub>F x in \<Sqinter>i\<in>I. A i. P x" and Q: "\<forall>\<^sub>F x in \<Sqinter>j\<in>J. B j. Q x"
+    let ?X = "(\<Sqinter>i\<in>I. \<Sqinter>j\<in>J. \<Sqinter>(P, Q)\<in>{(P, Q). (\<forall>\<^sub>F x in A i. P x) \<and> (\<forall>\<^sub>F x in B j. Q x)}. principal {(x, y). P x \<and> Q y})"
+    have "?X \<le> principal {x. P (fst x)} \<sqinter> principal {x. Q (snd x)}"
+    proof (intro inf_greatest)
+      have "?X \<le> (\<Sqinter>i\<in>I. \<Sqinter>P\<in>{P. eventually P (A i)}. principal {x. P (fst x)})"
+        by (auto intro!: INF_greatest INF_lower2[of j] INF_lower2 \<open>j\<in>J\<close> INF_lower2[of "(_, \<lambda>x. True)"])
+      also have "\<dots> \<le> principal {x. P (fst x)}"
+        unfolding le_principal
+      proof (rule eventually_INF_mono[OF P])
+        fix i P assume "i \<in> I" "eventually P (A i)"
+        then show "\<forall>\<^sub>F x in \<Sqinter>P\<in>{P. eventually P (A i)}. principal {x. P (fst x)}. x \<in> {x. P (fst x)}"
+          unfolding le_principal[symmetric] by (auto intro!: INF_lower)
+      qed auto
+      finally show "?X \<le> principal {x. P (fst x)}" .
+
+      have "?X \<le> (\<Sqinter>i\<in>J. \<Sqinter>P\<in>{P. eventually P (B i)}. principal {x. P (snd x)})"
+        by (auto intro!: INF_greatest INF_lower2[of i] INF_lower2 \<open>i\<in>I\<close> INF_lower2[of "(\<lambda>x. True, _)"])
+      also have "\<dots> \<le> principal {x. Q (snd x)}"
+        unfolding le_principal
+      proof (rule eventually_INF_mono[OF Q])
+        fix j Q assume "j \<in> J" "eventually Q (B j)"
+        then show "\<forall>\<^sub>F x in \<Sqinter>P\<in>{P. eventually P (B j)}. principal {x. P (snd x)}. x \<in> {x. Q (snd x)}"
+          unfolding le_principal[symmetric] by (auto intro!: INF_lower)
+      qed auto
+      finally show "?X \<le> principal {x. Q (snd x)}" .
+    qed
+    also have "\<dots> = principal {(x, y). P x \<and> Q y}"
+      by auto
+    finally show "?X \<le> principal {(x, y). P x \<and> Q y}" .
+  qed
+qed (intro prod_filter_mono INF_lower)
+
+lemma filtermap_Pair: "filtermap (\<lambda>x. (f x, g x)) F \<le> filtermap f F \<times>\<^sub>F filtermap g F"
+  by (simp add: le_filter_def eventually_filtermap eventually_prod_filter)
+     (auto elim: eventually_elim2)
+
 subsection \<open>Limits\<close>
 
 definition filterlim :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b filter \<Rightarrow> 'a filter \<Rightarrow> bool" where
@@ -800,7 +975,7 @@
   "_LIM" :: "pttrns \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> bool" ("(3LIM (_)/ (_)./ (_) :> (_))" [1000, 10, 0, 10] 10)
 
 translations
-  "LIM x F1. f :> F2"   == "CONST filterlim (%x. f) F2 F1"
+  "LIM x F1. f :> F2" == "CONST filterlim (\<lambda>x. f) F2 F1"
 
 lemma filterlim_iff:
   "(LIM x F1. f x :> F2) \<longleftrightarrow> (\<forall>P. eventually P F2 \<longrightarrow> eventually (\<lambda>x. P (f x)) F1)"
@@ -907,6 +1082,11 @@
     LIM x F. if P x then f x else g x :> G"
   unfolding filterlim_iff eventually_inf_principal by (auto simp: eventually_conj_iff)
 
+lemma filterlim_Pair:
+  "LIM x F. f x :> G \<Longrightarrow> LIM x F. g x :> H \<Longrightarrow> LIM x F. (f x, g x) :> G \<times>\<^sub>F H"
+  unfolding filterlim_def
+  by (rule order_trans[OF filtermap_Pair prod_filter_mono])
+
 subsection \<open>Limits to @{const at_top} and @{const at_bot}\<close>
 
 lemma filterlim_at_top: