src/HOL/Filter.thy
changeset 61806 d2e62ae01cd8
parent 61531 ab2e862263e7
child 61810 3c5040d5694a
     1.1 --- a/src/HOL/Filter.thy	Mon Dec 07 10:38:04 2015 +0100
     1.2 +++ b/src/HOL/Filter.thy	Mon Dec 07 16:44:26 2015 +0000
     1.3 @@ -71,6 +71,11 @@
     1.4    unfolding eventually_def
     1.5    by (rule is_filter.mono [OF is_filter_Rep_filter])
     1.6  
     1.7 +lemma eventually_mono':
     1.8 +  "\<lbrakk>eventually P F; \<And>x. P x \<Longrightarrow> Q x\<rbrakk> \<Longrightarrow> eventually Q F"
     1.9 +  unfolding eventually_def
    1.10 +  by (blast intro: is_filter.mono [OF is_filter_Rep_filter])
    1.11 +
    1.12  lemma eventually_conj:
    1.13    assumes P: "eventually (\<lambda>x. P x) F"
    1.14    assumes Q: "eventually (\<lambda>x. Q x) F"
    1.15 @@ -82,10 +87,11 @@
    1.16    assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
    1.17    assumes "eventually (\<lambda>x. P x) F"
    1.18    shows "eventually (\<lambda>x. Q x) F"
    1.19 -proof (rule eventually_mono)
    1.20 -  show "\<forall>x. (P x \<longrightarrow> Q x) \<and> P x \<longrightarrow> Q x" by simp
    1.21 -  show "eventually (\<lambda>x. (P x \<longrightarrow> Q x) \<and> P x) F"
    1.22 +proof -
    1.23 +  have "eventually (\<lambda>x. (P x \<longrightarrow> Q x) \<and> P x) F"
    1.24      using assms by (rule eventually_conj)
    1.25 +  then show ?thesis
    1.26 +    by (blast intro: eventually_mono')
    1.27  qed
    1.28  
    1.29  lemma eventually_rev_mp:
    1.30 @@ -172,7 +178,7 @@
    1.31  
    1.32  lemma frequently_mp:
    1.33    assumes ev: "\<forall>\<^sub>Fx in F. P x \<longrightarrow> Q x" and P: "\<exists>\<^sub>Fx in F. P x" shows "\<exists>\<^sub>Fx in F. Q x"
    1.34 -proof - 
    1.35 +proof -
    1.36    from ev have "eventually (\<lambda>x. \<not> Q x \<longrightarrow> \<not> P x) F"
    1.37      by (rule eventually_rev_mp) (auto intro!: always_eventually)
    1.38    from eventually_mp[OF this] P show ?thesis
    1.39 @@ -225,7 +231,7 @@
    1.40    "(\<forall>\<^sub>Fx in F. C \<longrightarrow> P x) \<longleftrightarrow> (C \<longrightarrow> (\<forall>\<^sub>Fx in F. P x))"
    1.41    by (cases C; simp add: not_frequently)+
    1.42  
    1.43 -lemmas eventually_frequently_simps = 
    1.44 +lemmas eventually_frequently_simps =
    1.45    eventually_frequently_const_simps
    1.46    not_eventually
    1.47    eventually_conj_iff
    1.48 @@ -340,7 +346,7 @@
    1.49      unfolding le_filter_def eventually_inf by (auto intro: eventually_True) }
    1.50    { assume "F \<le> F'" and "F \<le> F''" thus "F \<le> inf F' F''"
    1.51      unfolding le_filter_def eventually_inf
    1.52 -    by (auto elim!: eventually_mono intro: eventually_conj) }
    1.53 +    by (auto intro: eventually_mono' [OF eventually_conj]) }
    1.54    { show "F \<le> sup F F'" and "F' \<le> sup F F'"
    1.55      unfolding le_filter_def eventually_sup by simp_all }
    1.56    { assume "F \<le> F''" and "F' \<le> F''" thus "sup F F' \<le> F''"
    1.57 @@ -404,10 +410,13 @@
    1.58  lemma trivial_limit_def: "trivial_limit F \<longleftrightarrow> eventually (\<lambda>x. False) F"
    1.59    by (rule eventually_False [symmetric])
    1.60  
    1.61 +lemma False_imp_not_eventually: "(\<forall>x. \<not> P x ) \<Longrightarrow> \<not> trivial_limit net \<Longrightarrow> \<not> eventually (\<lambda>x. P x) net"
    1.62 +  by (simp add: eventually_False)
    1.63 +
    1.64  lemma eventually_Inf: "eventually P (Inf B) \<longleftrightarrow> (\<exists>X\<subseteq>B. finite X \<and> eventually P (Inf X))"
    1.65  proof -
    1.66    let ?F = "\<lambda>P. \<exists>X\<subseteq>B. finite X \<and> eventually P (Inf X)"
    1.67 -  
    1.68 +
    1.69    { fix P have "eventually P (Abs_filter ?F) \<longleftrightarrow> ?F P"
    1.70      proof (rule eventually_Abs_filter is_filter.intro)+
    1.71        show "?F (\<lambda>x. True)"
    1.72 @@ -605,7 +614,7 @@
    1.73    have "eventually P (INF k. principal {k <..}) \<longleftrightarrow> (\<exists>N::'a. \<forall>n>N. P n)"
    1.74      by (subst eventually_INF_base) (auto simp: eventually_principal intro: max.cobounded1 max.cobounded2)
    1.75    also have "(INF k. principal {k::'a <..}) = at_top"
    1.76 -    unfolding at_top_def 
    1.77 +    unfolding at_top_def
    1.78      by (intro INF_eq) (auto intro: less_imp_le simp: Ici_subset_Ioi_iff gt_ex)
    1.79    finally show ?thesis .
    1.80  qed
    1.81 @@ -645,7 +654,7 @@
    1.82    have "eventually P (INF k. principal {..< k}) \<longleftrightarrow> (\<exists>N::'a. \<forall>n<N. P n)"
    1.83      by (subst eventually_INF_base) (auto simp: eventually_principal intro: min.cobounded1 min.cobounded2)
    1.84    also have "(INF k. principal {..< k::'a}) = at_bot"
    1.85 -    unfolding at_bot_def 
    1.86 +    unfolding at_bot_def
    1.87      by (intro INF_eq) (auto intro: less_imp_le simp: Iic_subset_Iio_iff lt_ex)
    1.88    finally show ?thesis .
    1.89  qed
    1.90 @@ -828,11 +837,11 @@
    1.91    unfolding filterlim_def by (rule order_trans[OF filtermap_INF INF_mono])
    1.92  
    1.93  lemma filterlim_base:
    1.94 -  "(\<And>m x. m \<in> J \<Longrightarrow> i m \<in> I) \<Longrightarrow> (\<And>m x. m \<in> J \<Longrightarrow> x \<in> F (i m) \<Longrightarrow> f x \<in> G m) \<Longrightarrow> 
    1.95 +  "(\<And>m x. m \<in> J \<Longrightarrow> i m \<in> I) \<Longrightarrow> (\<And>m x. m \<in> J \<Longrightarrow> x \<in> F (i m) \<Longrightarrow> f x \<in> G m) \<Longrightarrow>
    1.96      LIM x (INF i:I. principal (F i)). f x :> (INF j:J. principal (G j))"
    1.97    by (force intro!: filterlim_INF_INF simp: image_subset_iff)
    1.98  
    1.99 -lemma filterlim_base_iff: 
   1.100 +lemma filterlim_base_iff:
   1.101    assumes "I \<noteq> {}" and chain: "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> F i \<subseteq> F j \<or> F j \<subseteq> F i"
   1.102    shows "(LIM x (INF i:I. principal (F i)). f x :> INF j:J. principal (G j)) \<longleftrightarrow>
   1.103      (\<forall>j\<in>J. \<exists>i\<in>I. \<forall>x\<in>F i. f x \<in> G j)"
   1.104 @@ -912,7 +921,7 @@
   1.105    shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z>c. eventually (\<lambda>x. Z \<le> f x) F)"
   1.106    by (metis filterlim_at_top order_less_le_trans gt_ex filterlim_at_top_ge)
   1.107  
   1.108 -lemma filterlim_at_bot: 
   1.109 +lemma filterlim_at_bot:
   1.110    fixes f :: "'a \<Rightarrow> ('b::linorder)"
   1.111    shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. f x \<le> Z) F)"
   1.112    by (auto simp: filterlim_iff eventually_at_bot_linorder elim!: eventually_elim1)
   1.113 @@ -926,12 +935,12 @@
   1.114    assume "\<forall>Z. eventually (\<lambda>x. f x \<le> Z) F"
   1.115    hence "eventually (\<lambda>x. f x \<le> Z') F" by auto
   1.116    thus "eventually (\<lambda>x. f x < Z) F"
   1.117 -    apply (rule eventually_mono[rotated])
   1.118 +    apply (rule eventually_mono')
   1.119      using 1 by auto
   1.120 -  next 
   1.121 -    fix Z :: 'b 
   1.122 +  next
   1.123 +    fix Z :: 'b
   1.124      show "\<forall>Z. eventually (\<lambda>x. f x < Z) F \<Longrightarrow> eventually (\<lambda>x. f x \<le> Z) F"
   1.125 -      by (drule spec [of _ Z], erule eventually_mono[rotated], auto simp add: less_imp_le)
   1.126 +      by (drule spec [of _ Z], erule eventually_mono', auto simp add: less_imp_le)
   1.127  qed
   1.128  
   1.129  lemma filterlim_at_bot_le:
   1.130 @@ -958,7 +967,7 @@
   1.131  where "rel_filter R F G = ((R ===> op =) ===> op =) (Rep_filter F) (Rep_filter G)"
   1.132  
   1.133  lemma rel_filter_eventually:
   1.134 -  "rel_filter R F G \<longleftrightarrow> 
   1.135 +  "rel_filter R F G \<longleftrightarrow>
   1.136    ((R ===> op =) ===> op =) (\<lambda>P. eventually P F) (\<lambda>P. eventually P G)"
   1.137  by(simp add: rel_filter_def eventually_def)
   1.138  
   1.139 @@ -984,7 +993,7 @@
   1.140    from Q have *: "\<And>x. T (Rep x) x" unfolding Quotient_alt_def by blast
   1.141  
   1.142    fix F
   1.143 -  show "rel_filter T (filtermap Rep F) F" 
   1.144 +  show "rel_filter T (filtermap Rep F) F"
   1.145      by(auto elim: rel_funD intro: * intro!: ext arg_cong[where f="\<lambda>P. eventually P F"] rel_funI
   1.146              del: iffI simp add: eventually_filtermap rel_filter_eventually)
   1.147  qed(auto simp add: map_fun_def o_def eventually_filtermap filter_eq_iff fun_eq_iff rel_filter_eventually
   1.148 @@ -1063,7 +1072,7 @@
   1.149  proof(rule left_totalI)
   1.150    fix F :: "'a filter"
   1.151    from bi_total_fun[OF bi_unique_fun[OF \<open>bi_total A\<close> bi_unique_eq] bi_total_eq]
   1.152 -  obtain G where [transfer_rule]: "((A ===> op =) ===> op =) (\<lambda>P. eventually P F) G" 
   1.153 +  obtain G where [transfer_rule]: "((A ===> op =) ===> op =) (\<lambda>P. eventually P F) G"
   1.154      unfolding  bi_total_def by blast
   1.155    moreover have "is_filter (\<lambda>P. eventually P F) \<longleftrightarrow> is_filter G" by transfer_prover
   1.156    hence "is_filter G" by(simp add: eventually_def is_filter_Rep_filter)
   1.157 @@ -1094,7 +1103,7 @@
   1.158      fix P :: "'a \<Rightarrow> bool"
   1.159      obtain P' where [transfer_rule]: "(A ===> op =) P P'"
   1.160        using left_total_fun[OF assms left_total_eq] unfolding left_total_def by blast
   1.161 -    have "eventually P F = eventually P' G" 
   1.162 +    have "eventually P F = eventually P' G"
   1.163        and "eventually P F' = eventually P' G" by transfer_prover+
   1.164      thus "eventually P F = eventually P F'" by simp
   1.165    qed
   1.166 @@ -1139,7 +1148,7 @@
   1.167  
   1.168  context
   1.169    fixes A :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
   1.170 -  assumes [transfer_rule]: "bi_unique A" 
   1.171 +  assumes [transfer_rule]: "bi_unique A"
   1.172  begin
   1.173  
   1.174  lemma le_filter_parametric [transfer_rule]:
   1.175 @@ -1173,4 +1182,4 @@
   1.176  
   1.177  end
   1.178  
   1.179 -end
   1.180 \ No newline at end of file
   1.181 +end