src/HOL/Filter.thy
changeset 62101 26c0a70f78a3
parent 61955 e96292f32c3c
child 62102 877463945ce9
     1.1 --- a/src/HOL/Filter.thy	Fri Jan 08 16:37:56 2016 +0100
     1.2 +++ b/src/HOL/Filter.thy	Fri Jan 08 17:40:59 2016 +0100
     1.3 @@ -529,6 +529,8 @@
     1.4      unfolding le_filter_def eventually_filtermap
     1.5      by (subst (1 2) eventually_INF) auto
     1.6  qed
     1.7 +
     1.8 +
     1.9  subsubsection \<open>Standard filters\<close>
    1.10  
    1.11  definition principal :: "'a set \<Rightarrow> 'a filter" where
    1.12 @@ -743,6 +745,52 @@
    1.13      by (blast intro: finite_subset)
    1.14  qed
    1.15  
    1.16 +subsubsection \<open>Product of filters\<close>
    1.17 +
    1.18 +lemma filtermap_sequentually_ne_bot: "filtermap f sequentially \<noteq> bot"
    1.19 +  by (auto simp add: filter_eq_iff eventually_filtermap eventually_sequentially)
    1.20 +
    1.21 +definition prod_filter :: "'a filter \<Rightarrow> 'b filter \<Rightarrow> ('a \<times> 'b) filter" (infixr "\<times>\<^sub>F" 80) where
    1.22 +  "prod_filter F G =
    1.23 +    (INF (P, Q):{(P, Q). eventually P F \<and> eventually Q G}. principal {(x, y). P x \<and> Q y})"
    1.24 +
    1.25 +lemma eventually_prod_filter: "eventually P (F \<times>\<^sub>F G) \<longleftrightarrow>
    1.26 +  (\<exists>Pf Pg. eventually Pf F \<and> eventually Pg G \<and> (\<forall>x y. Pf x \<longrightarrow> Pg y \<longrightarrow> P (x, y)))"
    1.27 +  unfolding prod_filter_def
    1.28 +proof (subst eventually_INF_base, goal_cases)
    1.29 +  case 2
    1.30 +  moreover have "eventually Pf F \<Longrightarrow> eventually Qf F \<Longrightarrow> eventually Pg G \<Longrightarrow> eventually Qg G \<Longrightarrow>
    1.31 +    \<exists>P Q. eventually P F \<and> eventually Q G \<and>
    1.32 +      Collect P \<times> Collect Q \<subseteq> Collect Pf \<times> Collect Pg \<inter> Collect Qf \<times> Collect Qg" for Pf Pg Qf Qg
    1.33 +    by (intro conjI exI[of _ "inf Pf Qf"] exI[of _ "inf Pg Qg"])
    1.34 +       (auto simp: inf_fun_def eventually_conj)
    1.35 +  ultimately show ?case
    1.36 +    by auto
    1.37 +qed (auto simp: eventually_principal intro: eventually_True)
    1.38 +
    1.39 +lemma prod_filter_mono: "F \<le> F' \<Longrightarrow> G \<le> G' \<Longrightarrow> F \<times>\<^sub>F G \<le> F' \<times>\<^sub>F G'"
    1.40 +  by (auto simp: le_filter_def eventually_prod_filter)
    1.41 +
    1.42 +lemma eventually_prod_same: "eventually P (F \<times>\<^sub>F F) \<longleftrightarrow>
    1.43 +    (\<exists>Q. eventually Q F \<and> (\<forall>x y. Q x \<longrightarrow> Q y \<longrightarrow> P (x, y)))"
    1.44 +  unfolding eventually_prod_filter
    1.45 +  apply safe
    1.46 +  apply (rule_tac x="inf Pf Pg" in exI)
    1.47 +  apply (auto simp: inf_fun_def intro!: eventually_conj)
    1.48 +  done
    1.49 +
    1.50 +lemma eventually_prod_sequentially:
    1.51 +  "eventually P (sequentially \<times>\<^sub>F sequentially) \<longleftrightarrow> (\<exists>N. \<forall>m \<ge> N. \<forall>n \<ge> N. P (n, m))"
    1.52 +  unfolding eventually_prod_same eventually_sequentially by auto
    1.53 +
    1.54 +lemma principal_prod_principal: "principal A \<times>\<^sub>F principal B = principal (A \<times> B)"
    1.55 +  apply (simp add: filter_eq_iff eventually_prod_filter eventually_principal)
    1.56 +  apply safe
    1.57 +  apply blast
    1.58 +  apply (intro conjI exI[of _ "\<lambda>x. x \<in> A"] exI[of _ "\<lambda>x. x \<in> B"])
    1.59 +  apply auto
    1.60 +  done
    1.61 +
    1.62  subsection \<open>Limits\<close>
    1.63  
    1.64  definition filterlim :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b filter \<Rightarrow> 'a filter \<Rightarrow> bool" where