# HG changeset patch
# User hoelzl
# Date 1454948293 -3600
# Node ID d2bc8a7e5fec870af53b44039378a2b96eecb508
# Parent  95c6cf433c9188e55f279d71bcb16b3b6f5bf325
move product topology to HOL-Complex_Main

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:
diff -r 95c6cf433c91 -r d2bc8a7e5fec src/HOL/Library/Product_Vector.thy
--- a/src/HOL/Library/Product_Vector.thy	Thu Feb 18 17:53:09 2016 +0100
+++ b/src/HOL/Library/Product_Vector.thy	Mon Feb 08 17:18:13 2016 +0100
@@ -40,239 +40,6 @@
 
 end
 
-subsection \<open>Product is a topological space\<close>
-
-instantiation prod :: (topological_space, topological_space) topological_space
-begin
-
-definition open_prod_def[code del]:
-  "open (S :: ('a \<times> 'b) set) \<longleftrightarrow>
-    (\<forall>x\<in>S. \<exists>A B. open A \<and> open B \<and> x \<in> A \<times> B \<and> A \<times> B \<subseteq> S)"
-
-lemma open_prod_elim:
-  assumes "open S" and "x \<in> S"
-  obtains A B where "open A" and "open B" and "x \<in> A \<times> B" and "A \<times> B \<subseteq> S"
-using assms unfolding open_prod_def by fast
-
-lemma open_prod_intro:
-  assumes "\<And>x. x \<in> S \<Longrightarrow> \<exists>A B. open A \<and> open B \<and> x \<in> A \<times> B \<and> A \<times> B \<subseteq> S"
-  shows "open S"
-using assms unfolding open_prod_def by fast
-
-instance
-proof
-  show "open (UNIV :: ('a \<times> 'b) set)"
-    unfolding open_prod_def by auto
-next
-  fix S T :: "('a \<times> 'b) set"
-  assume "open S" "open T"
-  show "open (S \<inter> T)"
-  proof (rule open_prod_intro)
-    fix x assume x: "x \<in> S \<inter> T"
-    from x have "x \<in> S" by simp
-    obtain Sa Sb where A: "open Sa" "open Sb" "x \<in> Sa \<times> Sb" "Sa \<times> Sb \<subseteq> S"
-      using \<open>open S\<close> and \<open>x \<in> S\<close> by (rule open_prod_elim)
-    from x have "x \<in> T" by simp
-    obtain Ta Tb where B: "open Ta" "open Tb" "x \<in> Ta \<times> Tb" "Ta \<times> Tb \<subseteq> T"
-      using \<open>open T\<close> and \<open>x \<in> T\<close> by (rule open_prod_elim)
-    let ?A = "Sa \<inter> Ta" and ?B = "Sb \<inter> Tb"
-    have "open ?A \<and> open ?B \<and> x \<in> ?A \<times> ?B \<and> ?A \<times> ?B \<subseteq> S \<inter> T"
-      using A B by (auto simp add: open_Int)
-    thus "\<exists>A B. open A \<and> open B \<and> x \<in> A \<times> B \<and> A \<times> B \<subseteq> S \<inter> T"
-      by fast
-  qed
-next
-  fix K :: "('a \<times> 'b) set set"
-  assume "\<forall>S\<in>K. open S" thus "open (\<Union>K)"
-    unfolding open_prod_def by fast
-qed
-
-end
-
-declare [[code abort: "open::('a::topological_space*'b::topological_space) set \<Rightarrow> bool"]]
-
-lemma open_Times: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<times> T)"
-unfolding open_prod_def by auto
-
-lemma fst_vimage_eq_Times: "fst -` S = S \<times> UNIV"
-by auto
-
-lemma snd_vimage_eq_Times: "snd -` S = UNIV \<times> S"
-by auto
-
-lemma open_vimage_fst: "open S \<Longrightarrow> open (fst -` S)"
-by (simp add: fst_vimage_eq_Times open_Times)
-
-lemma open_vimage_snd: "open S \<Longrightarrow> open (snd -` S)"
-by (simp add: snd_vimage_eq_Times open_Times)
-
-lemma closed_vimage_fst: "closed S \<Longrightarrow> closed (fst -` S)"
-unfolding closed_open vimage_Compl [symmetric]
-by (rule open_vimage_fst)
-
-lemma closed_vimage_snd: "closed S \<Longrightarrow> closed (snd -` S)"
-unfolding closed_open vimage_Compl [symmetric]
-by (rule open_vimage_snd)
-
-lemma closed_Times: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<times> T)"
-proof -
-  have "S \<times> T = (fst -` S) \<inter> (snd -` T)" by auto
-  thus "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<times> T)"
-    by (simp add: closed_vimage_fst closed_vimage_snd closed_Int)
-qed
-
-lemma subset_fst_imageI: "A \<times> B \<subseteq> S \<Longrightarrow> y \<in> B \<Longrightarrow> A \<subseteq> fst ` S"
-  unfolding image_def subset_eq by force
-
-lemma subset_snd_imageI: "A \<times> B \<subseteq> S \<Longrightarrow> x \<in> A \<Longrightarrow> B \<subseteq> snd ` S"
-  unfolding image_def subset_eq by force
-
-lemma open_image_fst: assumes "open S" shows "open (fst ` S)"
-proof (rule openI)
-  fix x assume "x \<in> fst ` S"
-  then obtain y where "(x, y) \<in> S" by auto
-  then obtain A B where "open A" "open B" "x \<in> A" "y \<in> B" "A \<times> B \<subseteq> S"
-    using \<open>open S\<close> unfolding open_prod_def by auto
-  from \<open>A \<times> B \<subseteq> S\<close> \<open>y \<in> B\<close> have "A \<subseteq> fst ` S" by (rule subset_fst_imageI)
-  with \<open>open A\<close> \<open>x \<in> A\<close> have "open A \<and> x \<in> A \<and> A \<subseteq> fst ` S" by simp
-  then show "\<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> fst ` S" by - (rule exI)
-qed
-
-lemma open_image_snd: assumes "open S" shows "open (snd ` S)"
-proof (rule openI)
-  fix y assume "y \<in> snd ` S"
-  then obtain x where "(x, y) \<in> S" by auto
-  then obtain A B where "open A" "open B" "x \<in> A" "y \<in> B" "A \<times> B \<subseteq> S"
-    using \<open>open S\<close> unfolding open_prod_def by auto
-  from \<open>A \<times> B \<subseteq> S\<close> \<open>x \<in> A\<close> have "B \<subseteq> snd ` S" by (rule subset_snd_imageI)
-  with \<open>open B\<close> \<open>y \<in> B\<close> have "open B \<and> y \<in> B \<and> B \<subseteq> snd ` S" by simp
-  then show "\<exists>T. open T \<and> y \<in> T \<and> T \<subseteq> snd ` S" by - (rule exI)
-qed
-
-subsubsection \<open>Continuity of operations\<close>
-
-lemma tendsto_fst [tendsto_intros]:
-  assumes "(f \<longlongrightarrow> a) F"
-  shows "((\<lambda>x. fst (f x)) \<longlongrightarrow> fst a) F"
-proof (rule topological_tendstoI)
-  fix S assume "open S" and "fst a \<in> S"
-  then have "open (fst -` S)" and "a \<in> fst -` S"
-    by (simp_all add: open_vimage_fst)
-  with assms have "eventually (\<lambda>x. f x \<in> fst -` S) F"
-    by (rule topological_tendstoD)
-  then show "eventually (\<lambda>x. fst (f x) \<in> S) F"
-    by simp
-qed
-
-lemma tendsto_snd [tendsto_intros]:
-  assumes "(f \<longlongrightarrow> a) F"
-  shows "((\<lambda>x. snd (f x)) \<longlongrightarrow> snd a) F"
-proof (rule topological_tendstoI)
-  fix S assume "open S" and "snd a \<in> S"
-  then have "open (snd -` S)" and "a \<in> snd -` S"
-    by (simp_all add: open_vimage_snd)
-  with assms have "eventually (\<lambda>x. f x \<in> snd -` S) F"
-    by (rule topological_tendstoD)
-  then show "eventually (\<lambda>x. snd (f x) \<in> S) F"
-    by simp
-qed
-
-lemma tendsto_Pair [tendsto_intros]:
-  assumes "(f \<longlongrightarrow> a) F" and "(g \<longlongrightarrow> b) F"
-  shows "((\<lambda>x. (f x, g x)) \<longlongrightarrow> (a, b)) F"
-proof (rule topological_tendstoI)
-  fix S assume "open S" and "(a, b) \<in> S"
-  then obtain A B where "open A" "open B" "a \<in> A" "b \<in> B" "A \<times> B \<subseteq> S"
-    unfolding open_prod_def by fast
-  have "eventually (\<lambda>x. f x \<in> A) F"
-    using \<open>(f \<longlongrightarrow> a) F\<close> \<open>open A\<close> \<open>a \<in> A\<close>
-    by (rule topological_tendstoD)
-  moreover
-  have "eventually (\<lambda>x. g x \<in> B) F"
-    using \<open>(g \<longlongrightarrow> b) F\<close> \<open>open B\<close> \<open>b \<in> B\<close>
-    by (rule topological_tendstoD)
-  ultimately
-  show "eventually (\<lambda>x. (f x, g x) \<in> S) F"
-    by (rule eventually_elim2)
-       (simp add: subsetD [OF \<open>A \<times> B \<subseteq> S\<close>])
-qed
-
-lemma continuous_fst[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. fst (f x))"
-  unfolding continuous_def by (rule tendsto_fst)
-
-lemma continuous_snd[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. snd (f x))"
-  unfolding continuous_def by (rule tendsto_snd)
-
-lemma continuous_Pair[continuous_intros]: "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. (f x, g x))"
-  unfolding continuous_def by (rule tendsto_Pair)
-
-lemma continuous_on_fst[continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. fst (f x))"
-  unfolding continuous_on_def by (auto intro: tendsto_fst)
-
-lemma continuous_on_snd[continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. snd (f x))"
-  unfolding continuous_on_def by (auto intro: tendsto_snd)
-
-lemma continuous_on_Pair[continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. (f x, g x))"
-  unfolding continuous_on_def by (auto intro: tendsto_Pair)
-
-lemma continuous_on_swap[continuous_intros]: "continuous_on A prod.swap"
-  by (simp add: prod.swap_def continuous_on_fst continuous_on_snd continuous_on_Pair continuous_on_id)
-
-lemma continuous_on_swap_args:
-  assumes "continuous_on (A\<times>B) (\<lambda>(x,y). d x y)" 
-    shows "continuous_on (B\<times>A) (\<lambda>(x,y). d y x)"
-proof -
-  have "(\<lambda>(x,y). d y x) = (\<lambda>(x,y). d x y) o prod.swap"
-    by force
-  then show ?thesis
-    apply (rule ssubst)
-    apply (rule continuous_on_compose)
-     apply (force intro: continuous_on_subset [OF continuous_on_swap])
-    apply (force intro: continuous_on_subset [OF assms])
-    done
-qed
-
-lemma isCont_fst [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. fst (f x)) a"
-  by (fact continuous_fst)
-
-lemma isCont_snd [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. snd (f x)) a"
-  by (fact continuous_snd)
-
-lemma isCont_Pair [simp]: "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. (f x, g x)) a"
-  by (fact continuous_Pair)
-
-subsubsection \<open>Separation axioms\<close>
-
-instance prod :: (t0_space, t0_space) t0_space
-proof
-  fix x y :: "'a \<times> 'b" assume "x \<noteq> y"
-  hence "fst x \<noteq> fst y \<or> snd x \<noteq> snd y"
-    by (simp add: prod_eq_iff)
-  thus "\<exists>U. open U \<and> (x \<in> U) \<noteq> (y \<in> U)"
-    by (fast dest: t0_space elim: open_vimage_fst open_vimage_snd)
-qed
-
-instance prod :: (t1_space, t1_space) t1_space
-proof
-  fix x y :: "'a \<times> 'b" assume "x \<noteq> y"
-  hence "fst x \<noteq> fst y \<or> snd x \<noteq> snd y"
-    by (simp add: prod_eq_iff)
-  thus "\<exists>U. open U \<and> x \<in> U \<and> y \<notin> U"
-    by (fast dest: t1_space elim: open_vimage_fst open_vimage_snd)
-qed
-
-instance prod :: (t2_space, t2_space) t2_space
-proof
-  fix x y :: "'a \<times> 'b" assume "x \<noteq> y"
-  hence "fst x \<noteq> fst y \<or> snd x \<noteq> snd y"
-    by (simp add: prod_eq_iff)
-  thus "\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}"
-    by (fast dest: hausdorff elim: open_vimage_fst open_vimage_snd)
-qed
-
-lemma isCont_swap[continuous_intros]: "isCont prod.swap a"
-  using continuous_on_eq_continuous_within continuous_on_swap by blast
-
 subsection \<open>Product is a metric space\<close>
 
 (* TODO: Product of uniform spaces and compatibility with metric_spaces! *)
diff -r 95c6cf433c91 -r d2bc8a7e5fec src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Thu Feb 18 17:53:09 2016 +0100
+++ b/src/HOL/Topological_Spaces.thy	Mon Feb 08 17:18:13 2016 +0100
@@ -2610,4 +2610,254 @@
   by (auto simp: filterlim_iff eventually_at_filter eventually_nhds_uniformity continuous_on_def
            elim: eventually_mono dest!: uniformly_continuous_onD[OF f])
 
+section \<open>Product Topology\<close>
+
+
+subsection \<open>Product is a topological space\<close>
+
+instantiation prod :: (topological_space, topological_space) topological_space
+begin
+
+definition open_prod_def[code del]:
+  "open (S :: ('a \<times> 'b) set) \<longleftrightarrow>
+    (\<forall>x\<in>S. \<exists>A B. open A \<and> open B \<and> x \<in> A \<times> B \<and> A \<times> B \<subseteq> S)"
+
+lemma open_prod_elim:
+  assumes "open S" and "x \<in> S"
+  obtains A B where "open A" and "open B" and "x \<in> A \<times> B" and "A \<times> B \<subseteq> S"
+using assms unfolding open_prod_def by fast
+
+lemma open_prod_intro:
+  assumes "\<And>x. x \<in> S \<Longrightarrow> \<exists>A B. open A \<and> open B \<and> x \<in> A \<times> B \<and> A \<times> B \<subseteq> S"
+  shows "open S"
+using assms unfolding open_prod_def by fast
+
+instance
+proof
+  show "open (UNIV :: ('a \<times> 'b) set)"
+    unfolding open_prod_def by auto
+next
+  fix S T :: "('a \<times> 'b) set"
+  assume "open S" "open T"
+  show "open (S \<inter> T)"
+  proof (rule open_prod_intro)
+    fix x assume x: "x \<in> S \<inter> T"
+    from x have "x \<in> S" by simp
+    obtain Sa Sb where A: "open Sa" "open Sb" "x \<in> Sa \<times> Sb" "Sa \<times> Sb \<subseteq> S"
+      using \<open>open S\<close> and \<open>x \<in> S\<close> by (rule open_prod_elim)
+    from x have "x \<in> T" by simp
+    obtain Ta Tb where B: "open Ta" "open Tb" "x \<in> Ta \<times> Tb" "Ta \<times> Tb \<subseteq> T"
+      using \<open>open T\<close> and \<open>x \<in> T\<close> by (rule open_prod_elim)
+    let ?A = "Sa \<inter> Ta" and ?B = "Sb \<inter> Tb"
+    have "open ?A \<and> open ?B \<and> x \<in> ?A \<times> ?B \<and> ?A \<times> ?B \<subseteq> S \<inter> T"
+      using A B by (auto simp add: open_Int)
+    thus "\<exists>A B. open A \<and> open B \<and> x \<in> A \<times> B \<and> A \<times> B \<subseteq> S \<inter> T"
+      by fast
+  qed
+next
+  fix K :: "('a \<times> 'b) set set"
+  assume "\<forall>S\<in>K. open S" thus "open (\<Union>K)"
+    unfolding open_prod_def by fast
+qed
+
 end
+
+declare [[code abort: "open::('a::topological_space*'b::topological_space) set \<Rightarrow> bool"]]
+
+lemma open_Times: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<times> T)"
+unfolding open_prod_def by auto
+
+lemma fst_vimage_eq_Times: "fst -` S = S \<times> UNIV"
+by auto
+
+lemma snd_vimage_eq_Times: "snd -` S = UNIV \<times> S"
+by auto
+
+lemma open_vimage_fst: "open S \<Longrightarrow> open (fst -` S)"
+by (simp add: fst_vimage_eq_Times open_Times)
+
+lemma open_vimage_snd: "open S \<Longrightarrow> open (snd -` S)"
+by (simp add: snd_vimage_eq_Times open_Times)
+
+lemma closed_vimage_fst: "closed S \<Longrightarrow> closed (fst -` S)"
+unfolding closed_open vimage_Compl [symmetric]
+by (rule open_vimage_fst)
+
+lemma closed_vimage_snd: "closed S \<Longrightarrow> closed (snd -` S)"
+unfolding closed_open vimage_Compl [symmetric]
+by (rule open_vimage_snd)
+
+lemma closed_Times: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<times> T)"
+proof -
+  have "S \<times> T = (fst -` S) \<inter> (snd -` T)" by auto
+  thus "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<times> T)"
+    by (simp add: closed_vimage_fst closed_vimage_snd closed_Int)
+qed
+
+lemma subset_fst_imageI: "A \<times> B \<subseteq> S \<Longrightarrow> y \<in> B \<Longrightarrow> A \<subseteq> fst ` S"
+  unfolding image_def subset_eq by force
+
+lemma subset_snd_imageI: "A \<times> B \<subseteq> S \<Longrightarrow> x \<in> A \<Longrightarrow> B \<subseteq> snd ` S"
+  unfolding image_def subset_eq by force
+
+lemma open_image_fst: assumes "open S" shows "open (fst ` S)"
+proof (rule openI)
+  fix x assume "x \<in> fst ` S"
+  then obtain y where "(x, y) \<in> S" by auto
+  then obtain A B where "open A" "open B" "x \<in> A" "y \<in> B" "A \<times> B \<subseteq> S"
+    using \<open>open S\<close> unfolding open_prod_def by auto
+  from \<open>A \<times> B \<subseteq> S\<close> \<open>y \<in> B\<close> have "A \<subseteq> fst ` S" by (rule subset_fst_imageI)
+  with \<open>open A\<close> \<open>x \<in> A\<close> have "open A \<and> x \<in> A \<and> A \<subseteq> fst ` S" by simp
+  then show "\<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> fst ` S" by - (rule exI)
+qed
+
+lemma open_image_snd: assumes "open S" shows "open (snd ` S)"
+proof (rule openI)
+  fix y assume "y \<in> snd ` S"
+  then obtain x where "(x, y) \<in> S" by auto
+  then obtain A B where "open A" "open B" "x \<in> A" "y \<in> B" "A \<times> B \<subseteq> S"
+    using \<open>open S\<close> unfolding open_prod_def by auto
+  from \<open>A \<times> B \<subseteq> S\<close> \<open>x \<in> A\<close> have "B \<subseteq> snd ` S" by (rule subset_snd_imageI)
+  with \<open>open B\<close> \<open>y \<in> B\<close> have "open B \<and> y \<in> B \<and> B \<subseteq> snd ` S" by simp
+  then show "\<exists>T. open T \<and> y \<in> T \<and> T \<subseteq> snd ` S" by - (rule exI)
+qed
+
+lemma nhds_prod: "nhds (a, b) = nhds a \<times>\<^sub>F nhds b"
+  unfolding nhds_def
+proof (subst prod_filter_INF, auto intro!: antisym INF_greatest simp: principal_prod_principal)
+  fix S T assume "open S" "a \<in> S" "open T" "b \<in> T"
+  then show "(INF x : {S. open S \<and> (a, b) \<in> S}. principal x) \<le> principal (S \<times> T)"
+    by (intro INF_lower) (auto intro!: open_Times)
+next
+  fix S' assume "open S'" "(a, b) \<in> S'"
+  then obtain S T where "open S" "a \<in> S" "open T" "b \<in> T" "S \<times> T \<subseteq> S'"
+    by (auto elim: open_prod_elim)
+  then show "(INF x : {S. open S \<and> a \<in> S}. INF y : {S. open S \<and> b \<in> S}. principal (x \<times> y)) \<le> principal S'"
+    by (auto intro!: INF_lower2)
+qed
+
+subsubsection \<open>Continuity of operations\<close>
+
+lemma tendsto_fst [tendsto_intros]:
+  assumes "(f \<longlongrightarrow> a) F"
+  shows "((\<lambda>x. fst (f x)) \<longlongrightarrow> fst a) F"
+proof (rule topological_tendstoI)
+  fix S assume "open S" and "fst a \<in> S"
+  then have "open (fst -` S)" and "a \<in> fst -` S"
+    by (simp_all add: open_vimage_fst)
+  with assms have "eventually (\<lambda>x. f x \<in> fst -` S) F"
+    by (rule topological_tendstoD)
+  then show "eventually (\<lambda>x. fst (f x) \<in> S) F"
+    by simp
+qed
+
+lemma tendsto_snd [tendsto_intros]:
+  assumes "(f \<longlongrightarrow> a) F"
+  shows "((\<lambda>x. snd (f x)) \<longlongrightarrow> snd a) F"
+proof (rule topological_tendstoI)
+  fix S assume "open S" and "snd a \<in> S"
+  then have "open (snd -` S)" and "a \<in> snd -` S"
+    by (simp_all add: open_vimage_snd)
+  with assms have "eventually (\<lambda>x. f x \<in> snd -` S) F"
+    by (rule topological_tendstoD)
+  then show "eventually (\<lambda>x. snd (f x) \<in> S) F"
+    by simp
+qed
+
+lemma tendsto_Pair [tendsto_intros]:
+  assumes "(f \<longlongrightarrow> a) F" and "(g \<longlongrightarrow> b) F"
+  shows "((\<lambda>x. (f x, g x)) \<longlongrightarrow> (a, b)) F"
+proof (rule topological_tendstoI)
+  fix S assume "open S" and "(a, b) \<in> S"
+  then obtain A B where "open A" "open B" "a \<in> A" "b \<in> B" "A \<times> B \<subseteq> S"
+    unfolding open_prod_def by fast
+  have "eventually (\<lambda>x. f x \<in> A) F"
+    using \<open>(f \<longlongrightarrow> a) F\<close> \<open>open A\<close> \<open>a \<in> A\<close>
+    by (rule topological_tendstoD)
+  moreover
+  have "eventually (\<lambda>x. g x \<in> B) F"
+    using \<open>(g \<longlongrightarrow> b) F\<close> \<open>open B\<close> \<open>b \<in> B\<close>
+    by (rule topological_tendstoD)
+  ultimately
+  show "eventually (\<lambda>x. (f x, g x) \<in> S) F"
+    by (rule eventually_elim2)
+       (simp add: subsetD [OF \<open>A \<times> B \<subseteq> S\<close>])
+qed
+
+lemma continuous_fst[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. fst (f x))"
+  unfolding continuous_def by (rule tendsto_fst)
+
+lemma continuous_snd[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. snd (f x))"
+  unfolding continuous_def by (rule tendsto_snd)
+
+lemma continuous_Pair[continuous_intros]: "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. (f x, g x))"
+  unfolding continuous_def by (rule tendsto_Pair)
+
+lemma continuous_on_fst[continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. fst (f x))"
+  unfolding continuous_on_def by (auto intro: tendsto_fst)
+
+lemma continuous_on_snd[continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. snd (f x))"
+  unfolding continuous_on_def by (auto intro: tendsto_snd)
+
+lemma continuous_on_Pair[continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. (f x, g x))"
+  unfolding continuous_on_def by (auto intro: tendsto_Pair)
+
+lemma continuous_on_swap[continuous_intros]: "continuous_on A prod.swap"
+  by (simp add: prod.swap_def continuous_on_fst continuous_on_snd continuous_on_Pair continuous_on_id)
+
+lemma continuous_on_swap_args:
+  assumes "continuous_on (A\<times>B) (\<lambda>(x,y). d x y)"
+    shows "continuous_on (B\<times>A) (\<lambda>(x,y). d y x)"
+proof -
+  have "(\<lambda>(x,y). d y x) = (\<lambda>(x,y). d x y) o prod.swap"
+    by force
+  then show ?thesis
+    apply (rule ssubst)
+    apply (rule continuous_on_compose)
+     apply (force intro: continuous_on_subset [OF continuous_on_swap])
+    apply (force intro: continuous_on_subset [OF assms])
+    done
+qed
+
+lemma isCont_fst [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. fst (f x)) a"
+  by (fact continuous_fst)
+
+lemma isCont_snd [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. snd (f x)) a"
+  by (fact continuous_snd)
+
+lemma isCont_Pair [simp]: "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. (f x, g x)) a"
+  by (fact continuous_Pair)
+
+subsubsection \<open>Separation axioms\<close>
+
+instance prod :: (t0_space, t0_space) t0_space
+proof
+  fix x y :: "'a \<times> 'b" assume "x \<noteq> y"
+  hence "fst x \<noteq> fst y \<or> snd x \<noteq> snd y"
+    by (simp add: prod_eq_iff)
+  thus "\<exists>U. open U \<and> (x \<in> U) \<noteq> (y \<in> U)"
+    by (fast dest: t0_space elim: open_vimage_fst open_vimage_snd)
+qed
+
+instance prod :: (t1_space, t1_space) t1_space
+proof
+  fix x y :: "'a \<times> 'b" assume "x \<noteq> y"
+  hence "fst x \<noteq> fst y \<or> snd x \<noteq> snd y"
+    by (simp add: prod_eq_iff)
+  thus "\<exists>U. open U \<and> x \<in> U \<and> y \<notin> U"
+    by (fast dest: t1_space elim: open_vimage_fst open_vimage_snd)
+qed
+
+instance prod :: (t2_space, t2_space) t2_space
+proof
+  fix x y :: "'a \<times> 'b" assume "x \<noteq> y"
+  hence "fst x \<noteq> fst y \<or> snd x \<noteq> snd y"
+    by (simp add: prod_eq_iff)
+  thus "\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}"
+    by (fast dest: hausdorff elim: open_vimage_fst open_vimage_snd)
+qed
+
+lemma isCont_swap[continuous_intros]: "isCont prod.swap a"
+  using continuous_on_eq_continuous_within continuous_on_swap by blast
+
+end