--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Filter.thy Mon Apr 13 00:59:17 2015 +0200
@@ -0,0 +1,1133 @@
+(* Title: HOL/Filter.thy
+ Author: Brian Huffman
+ Author: Johannes Hölzl
+*)
+
+section {* Filters on predicates *}
+
+theory Filter
+imports Set_Interval Lifting_Set
+begin
+
+subsection {* Filters *}
+
+text {*
+ This definition also allows non-proper filters.
+*}
+
+locale is_filter =
+ fixes F :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
+ assumes True: "F (\<lambda>x. True)"
+ assumes conj: "F (\<lambda>x. P x) \<Longrightarrow> F (\<lambda>x. Q x) \<Longrightarrow> F (\<lambda>x. P x \<and> Q x)"
+ assumes mono: "\<forall>x. P x \<longrightarrow> Q x \<Longrightarrow> F (\<lambda>x. P x) \<Longrightarrow> F (\<lambda>x. Q x)"
+
+typedef 'a filter = "{F :: ('a \<Rightarrow> bool) \<Rightarrow> bool. is_filter F}"
+proof
+ show "(\<lambda>x. True) \<in> ?filter" by (auto intro: is_filter.intro)
+qed
+
+lemma is_filter_Rep_filter: "is_filter (Rep_filter F)"
+ using Rep_filter [of F] by simp
+
+lemma Abs_filter_inverse':
+ assumes "is_filter F" shows "Rep_filter (Abs_filter F) = F"
+ using assms by (simp add: Abs_filter_inverse)
+
+
+subsubsection {* Eventually *}
+
+definition eventually :: "('a \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> bool"
+ where "eventually P F \<longleftrightarrow> Rep_filter F P"
+
+syntax (xsymbols)
+ "_eventually" :: "pttrn => 'a filter => bool => bool" ("(3\<forall>\<^sub>F _ in _./ _)" [0, 0, 10] 10)
+
+translations
+ "\<forall>\<^sub>Fx in F. P" == "CONST eventually (\<lambda>x. P) F"
+
+lemma eventually_Abs_filter:
+ assumes "is_filter F" shows "eventually P (Abs_filter F) = F P"
+ unfolding eventually_def using assms by (simp add: Abs_filter_inverse)
+
+lemma filter_eq_iff:
+ shows "F = F' \<longleftrightarrow> (\<forall>P. eventually P F = eventually P F')"
+ unfolding Rep_filter_inject [symmetric] fun_eq_iff eventually_def ..
+
+lemma eventually_True [simp]: "eventually (\<lambda>x. True) F"
+ unfolding eventually_def
+ by (rule is_filter.True [OF is_filter_Rep_filter])
+
+lemma always_eventually: "\<forall>x. P x \<Longrightarrow> eventually P F"
+proof -
+ assume "\<forall>x. P x" hence "P = (\<lambda>x. True)" by (simp add: ext)
+ thus "eventually P F" by simp
+qed
+
+lemma eventuallyI: "(\<And>x. P x) \<Longrightarrow> eventually P F"
+ by (auto intro: always_eventually)
+
+lemma eventually_mono:
+ "(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually P F \<Longrightarrow> eventually Q F"
+ unfolding eventually_def
+ by (rule is_filter.mono [OF is_filter_Rep_filter])
+
+lemma eventually_conj:
+ assumes P: "eventually (\<lambda>x. P x) F"
+ assumes Q: "eventually (\<lambda>x. Q x) F"
+ shows "eventually (\<lambda>x. P x \<and> Q x) F"
+ using assms unfolding eventually_def
+ by (rule is_filter.conj [OF is_filter_Rep_filter])
+
+lemma eventually_mp:
+ assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
+ assumes "eventually (\<lambda>x. P x) F"
+ shows "eventually (\<lambda>x. Q x) F"
+proof (rule eventually_mono)
+ show "\<forall>x. (P x \<longrightarrow> Q x) \<and> P x \<longrightarrow> Q x" by simp
+ show "eventually (\<lambda>x. (P x \<longrightarrow> Q x) \<and> P x) F"
+ using assms by (rule eventually_conj)
+qed
+
+lemma eventually_rev_mp:
+ assumes "eventually (\<lambda>x. P x) F"
+ assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
+ shows "eventually (\<lambda>x. Q x) F"
+using assms(2) assms(1) by (rule eventually_mp)
+
+lemma eventually_conj_iff:
+ "eventually (\<lambda>x. P x \<and> Q x) F \<longleftrightarrow> eventually P F \<and> eventually Q F"
+ by (auto intro: eventually_conj elim: eventually_rev_mp)
+
+lemma eventually_elim1:
+ assumes "eventually (\<lambda>i. P i) F"
+ assumes "\<And>i. P i \<Longrightarrow> Q i"
+ shows "eventually (\<lambda>i. Q i) F"
+ using assms by (auto elim!: eventually_rev_mp)
+
+lemma eventually_elim2:
+ assumes "eventually (\<lambda>i. P i) F"
+ assumes "eventually (\<lambda>i. Q i) F"
+ assumes "\<And>i. P i \<Longrightarrow> Q i \<Longrightarrow> R i"
+ shows "eventually (\<lambda>i. R i) F"
+ using assms by (auto elim!: eventually_rev_mp)
+
+lemma eventually_ball_finite_distrib:
+ "finite A \<Longrightarrow> (eventually (\<lambda>x. \<forall>y\<in>A. P x y) net) \<longleftrightarrow> (\<forall>y\<in>A. eventually (\<lambda>x. P x y) net)"
+ by (induction A rule: finite_induct) (auto simp: eventually_conj_iff)
+
+lemma eventually_ball_finite:
+ "finite A \<Longrightarrow> \<forall>y\<in>A. eventually (\<lambda>x. P x y) net \<Longrightarrow> eventually (\<lambda>x. \<forall>y\<in>A. P x y) net"
+ by (auto simp: eventually_ball_finite_distrib)
+
+lemma eventually_all_finite:
+ fixes P :: "'a \<Rightarrow> 'b::finite \<Rightarrow> bool"
+ assumes "\<And>y. eventually (\<lambda>x. P x y) net"
+ shows "eventually (\<lambda>x. \<forall>y. P x y) net"
+using eventually_ball_finite [of UNIV P] assms by simp
+
+lemma eventually_ex: "(\<forall>\<^sub>Fx in F. \<exists>y. P x y) \<longleftrightarrow> (\<exists>Y. \<forall>\<^sub>Fx in F. P x (Y x))"
+proof
+ assume "\<forall>\<^sub>Fx in F. \<exists>y. P x y"
+ then have "\<forall>\<^sub>Fx in F. P x (SOME y. P x y)"
+ by (auto intro: someI_ex eventually_elim1)
+ then show "\<exists>Y. \<forall>\<^sub>Fx in F. P x (Y x)"
+ by auto
+qed (auto intro: eventually_elim1)
+
+lemma not_eventually_impI: "eventually P F \<Longrightarrow> \<not> eventually Q F \<Longrightarrow> \<not> eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
+ by (auto intro: eventually_mp)
+
+lemma not_eventuallyD: "\<not> eventually P F \<Longrightarrow> \<exists>x. \<not> P x"
+ by (metis always_eventually)
+
+lemma eventually_subst:
+ assumes "eventually (\<lambda>n. P n = Q n) F"
+ shows "eventually P F = eventually Q F" (is "?L = ?R")
+proof -
+ from assms have "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
+ and "eventually (\<lambda>x. Q x \<longrightarrow> P x) F"
+ by (auto elim: eventually_elim1)
+ then show ?thesis by (auto elim: eventually_elim2)
+qed
+
+subsection \<open> Frequently as dual to eventually \<close>
+
+definition frequently :: "('a \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> bool"
+ where "frequently P F \<longleftrightarrow> \<not> eventually (\<lambda>x. \<not> P x) F"
+
+syntax (xsymbols)
+ "_frequently" :: "pttrn \<Rightarrow> 'a filter \<Rightarrow> bool \<Rightarrow> bool" ("(3\<exists>\<^sub>F _ in _./ _)" [0, 0, 10] 10)
+
+translations
+ "\<exists>\<^sub>Fx in F. P" == "CONST frequently (\<lambda>x. P) F"
+
+lemma not_frequently_False [simp]: "\<not> (\<exists>\<^sub>Fx in F. False)"
+ by (simp add: frequently_def)
+
+lemma frequently_ex: "\<exists>\<^sub>Fx in F. P x \<Longrightarrow> \<exists>x. P x"
+ by (auto simp: frequently_def dest: not_eventuallyD)
+
+lemma frequentlyE: assumes "frequently P F" obtains x where "P x"
+ using frequently_ex[OF assms] by auto
+
+lemma frequently_mp:
+ 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"
+proof -
+ from ev have "eventually (\<lambda>x. \<not> Q x \<longrightarrow> \<not> P x) F"
+ by (rule eventually_rev_mp) (auto intro!: always_eventually)
+ from eventually_mp[OF this] P show ?thesis
+ by (auto simp: frequently_def)
+qed
+
+lemma frequently_rev_mp:
+ assumes "\<exists>\<^sub>Fx in F. P x"
+ assumes "\<forall>\<^sub>Fx in F. P x \<longrightarrow> Q x"
+ shows "\<exists>\<^sub>Fx in F. Q x"
+using assms(2) assms(1) by (rule frequently_mp)
+
+lemma frequently_mono: "(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> frequently P F \<Longrightarrow> frequently Q F"
+ using frequently_mp[of P Q] by (simp add: always_eventually)
+
+lemma frequently_elim1: "\<exists>\<^sub>Fx in F. P x \<Longrightarrow> (\<And>i. P i \<Longrightarrow> Q i) \<Longrightarrow> \<exists>\<^sub>Fx in F. Q x"
+ by (metis frequently_mono)
+
+lemma frequently_disj_iff: "(\<exists>\<^sub>Fx in F. P x \<or> Q x) \<longleftrightarrow> (\<exists>\<^sub>Fx in F. P x) \<or> (\<exists>\<^sub>Fx in F. Q x)"
+ by (simp add: frequently_def eventually_conj_iff)
+
+lemma frequently_disj: "\<exists>\<^sub>Fx in F. P x \<Longrightarrow> \<exists>\<^sub>Fx in F. Q x \<Longrightarrow> \<exists>\<^sub>Fx in F. P x \<or> Q x"
+ by (simp add: frequently_disj_iff)
+
+lemma frequently_bex_finite_distrib:
+ assumes "finite A" shows "(\<exists>\<^sub>Fx in F. \<exists>y\<in>A. P x y) \<longleftrightarrow> (\<exists>y\<in>A. \<exists>\<^sub>Fx in F. P x y)"
+ using assms by induction (auto simp: frequently_disj_iff)
+
+lemma frequently_bex_finite: "finite A \<Longrightarrow> \<exists>\<^sub>Fx in F. \<exists>y\<in>A. P x y \<Longrightarrow> \<exists>y\<in>A. \<exists>\<^sub>Fx in F. P x y"
+ by (simp add: frequently_bex_finite_distrib)
+
+lemma frequently_all: "(\<exists>\<^sub>Fx in F. \<forall>y. P x y) \<longleftrightarrow> (\<forall>Y. \<exists>\<^sub>Fx in F. P x (Y x))"
+ using eventually_ex[of "\<lambda>x y. \<not> P x y" F] by (simp add: frequently_def)
+
+lemma
+ shows not_eventually: "\<not> eventually P F \<longleftrightarrow> (\<exists>\<^sub>Fx in F. \<not> P x)"
+ and not_frequently: "\<not> frequently P F \<longleftrightarrow> (\<forall>\<^sub>Fx in F. \<not> P x)"
+ by (auto simp: frequently_def)
+
+lemma frequently_imp_iff:
+ "(\<exists>\<^sub>Fx in F. P x \<longrightarrow> Q x) \<longleftrightarrow> (eventually P F \<longrightarrow> frequently Q F)"
+ unfolding imp_conv_disj frequently_disj_iff not_eventually[symmetric] ..
+
+lemma eventually_frequently_const_simps:
+ "(\<exists>\<^sub>Fx in F. P x \<and> C) \<longleftrightarrow> (\<exists>\<^sub>Fx in F. P x) \<and> C"
+ "(\<exists>\<^sub>Fx in F. C \<and> P x) \<longleftrightarrow> C \<and> (\<exists>\<^sub>Fx in F. P x)"
+ "(\<forall>\<^sub>Fx in F. P x \<or> C) \<longleftrightarrow> (\<forall>\<^sub>Fx in F. P x) \<or> C"
+ "(\<forall>\<^sub>Fx in F. C \<or> P x) \<longleftrightarrow> C \<or> (\<forall>\<^sub>Fx in F. P x)"
+ "(\<forall>\<^sub>Fx in F. P x \<longrightarrow> C) \<longleftrightarrow> ((\<exists>\<^sub>Fx in F. P x) \<longrightarrow> C)"
+ "(\<forall>\<^sub>Fx in F. C \<longrightarrow> P x) \<longleftrightarrow> (C \<longrightarrow> (\<forall>\<^sub>Fx in F. P x))"
+ by (cases C; simp add: not_frequently)+
+
+lemmas eventually_frequently_simps =
+ eventually_frequently_const_simps
+ not_eventually
+ eventually_conj_iff
+ eventually_ball_finite_distrib
+ eventually_ex
+ not_frequently
+ frequently_disj_iff
+ frequently_bex_finite_distrib
+ frequently_all
+ frequently_imp_iff
+
+ML {*
+ fun eventually_elim_tac ctxt facts = SUBGOAL_CASES (fn (goal, i) =>
+ let
+ val mp_thms = facts RL @{thms eventually_rev_mp}
+ val raw_elim_thm =
+ (@{thm allI} RS @{thm always_eventually})
+ |> fold (fn thm1 => fn thm2 => thm2 RS thm1) mp_thms
+ |> fold (fn _ => fn thm => @{thm impI} RS thm) facts
+ val cases_prop = Thm.prop_of (raw_elim_thm RS Goal.init (Thm.cterm_of ctxt goal))
+ val cases = Rule_Cases.make_common ctxt cases_prop [(("elim", []), [])]
+ in
+ CASES cases (rtac raw_elim_thm i)
+ end)
+*}
+
+method_setup eventually_elim = {*
+ Scan.succeed (fn ctxt => METHOD_CASES (HEADGOAL o eventually_elim_tac ctxt))
+*} "elimination of eventually quantifiers"
+
+subsubsection {* Finer-than relation *}
+
+text {* @{term "F \<le> F'"} means that filter @{term F} is finer than
+filter @{term F'}. *}
+
+instantiation filter :: (type) complete_lattice
+begin
+
+definition le_filter_def:
+ "F \<le> F' \<longleftrightarrow> (\<forall>P. eventually P F' \<longrightarrow> eventually P F)"
+
+definition
+ "(F :: 'a filter) < F' \<longleftrightarrow> F \<le> F' \<and> \<not> F' \<le> F"
+
+definition
+ "top = Abs_filter (\<lambda>P. \<forall>x. P x)"
+
+definition
+ "bot = Abs_filter (\<lambda>P. True)"
+
+definition
+ "sup F F' = Abs_filter (\<lambda>P. eventually P F \<and> eventually P F')"
+
+definition
+ "inf F F' = Abs_filter
+ (\<lambda>P. \<exists>Q R. eventually Q F \<and> eventually R F' \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x))"
+
+definition
+ "Sup S = Abs_filter (\<lambda>P. \<forall>F\<in>S. eventually P F)"
+
+definition
+ "Inf S = Sup {F::'a filter. \<forall>F'\<in>S. F \<le> F'}"
+
+lemma eventually_top [simp]: "eventually P top \<longleftrightarrow> (\<forall>x. P x)"
+ unfolding top_filter_def
+ by (rule eventually_Abs_filter, rule is_filter.intro, auto)
+
+lemma eventually_bot [simp]: "eventually P bot"
+ unfolding bot_filter_def
+ by (subst eventually_Abs_filter, rule is_filter.intro, auto)
+
+lemma eventually_sup:
+ "eventually P (sup F F') \<longleftrightarrow> eventually P F \<and> eventually P F'"
+ unfolding sup_filter_def
+ by (rule eventually_Abs_filter, rule is_filter.intro)
+ (auto elim!: eventually_rev_mp)
+
+lemma eventually_inf:
+ "eventually P (inf F F') \<longleftrightarrow>
+ (\<exists>Q R. eventually Q F \<and> eventually R F' \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x))"
+ unfolding inf_filter_def
+ apply (rule eventually_Abs_filter, rule is_filter.intro)
+ apply (fast intro: eventually_True)
+ apply clarify
+ apply (intro exI conjI)
+ apply (erule (1) eventually_conj)
+ apply (erule (1) eventually_conj)
+ apply simp
+ apply auto
+ done
+
+lemma eventually_Sup:
+ "eventually P (Sup S) \<longleftrightarrow> (\<forall>F\<in>S. eventually P F)"
+ unfolding Sup_filter_def
+ apply (rule eventually_Abs_filter, rule is_filter.intro)
+ apply (auto intro: eventually_conj elim!: eventually_rev_mp)
+ done
+
+instance proof
+ fix F F' F'' :: "'a filter" and S :: "'a filter set"
+ { show "F < F' \<longleftrightarrow> F \<le> F' \<and> \<not> F' \<le> F"
+ by (rule less_filter_def) }
+ { show "F \<le> F"
+ unfolding le_filter_def by simp }
+ { assume "F \<le> F'" and "F' \<le> F''" thus "F \<le> F''"
+ unfolding le_filter_def by simp }
+ { assume "F \<le> F'" and "F' \<le> F" thus "F = F'"
+ unfolding le_filter_def filter_eq_iff by fast }
+ { show "inf F F' \<le> F" and "inf F F' \<le> F'"
+ unfolding le_filter_def eventually_inf by (auto intro: eventually_True) }
+ { assume "F \<le> F'" and "F \<le> F''" thus "F \<le> inf F' F''"
+ unfolding le_filter_def eventually_inf
+ by (auto elim!: eventually_mono intro: eventually_conj) }
+ { show "F \<le> sup F F'" and "F' \<le> sup F F'"
+ unfolding le_filter_def eventually_sup by simp_all }
+ { assume "F \<le> F''" and "F' \<le> F''" thus "sup F F' \<le> F''"
+ unfolding le_filter_def eventually_sup by simp }
+ { assume "F'' \<in> S" thus "Inf S \<le> F''"
+ unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp }
+ { assume "\<And>F'. F' \<in> S \<Longrightarrow> F \<le> F'" thus "F \<le> Inf S"
+ unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp }
+ { assume "F \<in> S" thus "F \<le> Sup S"
+ unfolding le_filter_def eventually_Sup by simp }
+ { assume "\<And>F. F \<in> S \<Longrightarrow> F \<le> F'" thus "Sup S \<le> F'"
+ unfolding le_filter_def eventually_Sup by simp }
+ { show "Inf {} = (top::'a filter)"
+ by (auto simp: top_filter_def Inf_filter_def Sup_filter_def)
+ (metis (full_types) top_filter_def always_eventually eventually_top) }
+ { show "Sup {} = (bot::'a filter)"
+ by (auto simp: bot_filter_def Sup_filter_def) }
+qed
+
+end
+
+lemma filter_leD:
+ "F \<le> F' \<Longrightarrow> eventually P F' \<Longrightarrow> eventually P F"
+ unfolding le_filter_def by simp
+
+lemma filter_leI:
+ "(\<And>P. eventually P F' \<Longrightarrow> eventually P F) \<Longrightarrow> F \<le> F'"
+ unfolding le_filter_def by simp
+
+lemma eventually_False:
+ "eventually (\<lambda>x. False) F \<longleftrightarrow> F = bot"
+ unfolding filter_eq_iff by (auto elim: eventually_rev_mp)
+
+lemma eventually_frequently: "F \<noteq> bot \<Longrightarrow> eventually P F \<Longrightarrow> frequently P F"
+ using eventually_conj[of P F "\<lambda>x. \<not> P x"]
+ by (auto simp add: frequently_def eventually_False)
+
+lemma eventually_const_iff: "eventually (\<lambda>x. P) F \<longleftrightarrow> P \<or> F = bot"
+ by (cases P) (auto simp: eventually_False)
+
+lemma eventually_const[simp]: "F \<noteq> bot \<Longrightarrow> eventually (\<lambda>x. P) F \<longleftrightarrow> P"
+ by (simp add: eventually_const_iff)
+
+lemma frequently_const_iff: "frequently (\<lambda>x. P) F \<longleftrightarrow> P \<and> F \<noteq> bot"
+ by (simp add: frequently_def eventually_const_iff)
+
+lemma frequently_const[simp]: "F \<noteq> bot \<Longrightarrow> frequently (\<lambda>x. P) F \<longleftrightarrow> P"
+ by (simp add: frequently_const_iff)
+
+abbreviation (input) trivial_limit :: "'a filter \<Rightarrow> bool"
+ where "trivial_limit F \<equiv> F = bot"
+
+lemma trivial_limit_def: "trivial_limit F \<longleftrightarrow> eventually (\<lambda>x. False) F"
+ by (rule eventually_False [symmetric])
+
+lemma eventually_Inf: "eventually P (Inf B) \<longleftrightarrow> (\<exists>X\<subseteq>B. finite X \<and> eventually P (Inf X))"
+proof -
+ let ?F = "\<lambda>P. \<exists>X\<subseteq>B. finite X \<and> eventually P (Inf X)"
+
+ { fix P have "eventually P (Abs_filter ?F) \<longleftrightarrow> ?F P"
+ proof (rule eventually_Abs_filter is_filter.intro)+
+ show "?F (\<lambda>x. True)"
+ by (rule exI[of _ "{}"]) (simp add: le_fun_def)
+ next
+ fix P Q
+ assume "?F P" then guess X ..
+ moreover
+ assume "?F Q" then guess Y ..
+ ultimately show "?F (\<lambda>x. P x \<and> Q x)"
+ by (intro exI[of _ "X \<union> Y"])
+ (auto simp: Inf_union_distrib eventually_inf)
+ next
+ fix P Q
+ assume "?F P" then guess X ..
+ moreover assume "\<forall>x. P x \<longrightarrow> Q x"
+ ultimately show "?F Q"
+ by (intro exI[of _ X]) (auto elim: eventually_elim1)
+ qed }
+ note eventually_F = this
+
+ have "Inf B = Abs_filter ?F"
+ proof (intro antisym Inf_greatest)
+ show "Inf B \<le> Abs_filter ?F"
+ by (auto simp: le_filter_def eventually_F dest: Inf_superset_mono)
+ next
+ fix F assume "F \<in> B" then show "Abs_filter ?F \<le> F"
+ by (auto simp add: le_filter_def eventually_F intro!: exI[of _ "{F}"])
+ qed
+ then show ?thesis
+ by (simp add: eventually_F)
+qed
+
+lemma eventually_INF: "eventually P (INF b:B. F b) \<longleftrightarrow> (\<exists>X\<subseteq>B. finite X \<and> eventually P (INF b:X. F b))"
+ unfolding INF_def[of B] eventually_Inf[of P "F`B"]
+ by (metis Inf_image_eq finite_imageI image_mono finite_subset_image)
+
+lemma Inf_filter_not_bot:
+ fixes B :: "'a filter set"
+ shows "(\<And>X. X \<subseteq> B \<Longrightarrow> finite X \<Longrightarrow> Inf X \<noteq> bot) \<Longrightarrow> Inf B \<noteq> bot"
+ unfolding trivial_limit_def eventually_Inf[of _ B]
+ bot_bool_def [symmetric] bot_fun_def [symmetric] bot_unique by simp
+
+lemma INF_filter_not_bot:
+ fixes F :: "'i \<Rightarrow> 'a filter"
+ shows "(\<And>X. X \<subseteq> B \<Longrightarrow> finite X \<Longrightarrow> (INF b:X. F b) \<noteq> bot) \<Longrightarrow> (INF b:B. F b) \<noteq> bot"
+ unfolding trivial_limit_def eventually_INF[of _ B]
+ bot_bool_def [symmetric] bot_fun_def [symmetric] bot_unique by simp
+
+lemma eventually_Inf_base:
+ assumes "B \<noteq> {}" and base: "\<And>F G. F \<in> B \<Longrightarrow> G \<in> B \<Longrightarrow> \<exists>x\<in>B. x \<le> inf F G"
+ shows "eventually P (Inf B) \<longleftrightarrow> (\<exists>b\<in>B. eventually P b)"
+proof (subst eventually_Inf, safe)
+ fix X assume "finite X" "X \<subseteq> B"
+ then have "\<exists>b\<in>B. \<forall>x\<in>X. b \<le> x"
+ proof induct
+ case empty then show ?case
+ using `B \<noteq> {}` by auto
+ next
+ case (insert x X)
+ then obtain b where "b \<in> B" "\<And>x. x \<in> X \<Longrightarrow> b \<le> x"
+ by auto
+ with `insert x X \<subseteq> B` base[of b x] show ?case
+ by (auto intro: order_trans)
+ qed
+ then obtain b where "b \<in> B" "b \<le> Inf X"
+ by (auto simp: le_Inf_iff)
+ then show "eventually P (Inf X) \<Longrightarrow> Bex B (eventually P)"
+ by (intro bexI[of _ b]) (auto simp: le_filter_def)
+qed (auto intro!: exI[of _ "{x}" for x])
+
+lemma eventually_INF_base:
+ "B \<noteq> {} \<Longrightarrow> (\<And>a b. a \<in> B \<Longrightarrow> b \<in> B \<Longrightarrow> \<exists>x\<in>B. F x \<le> inf (F a) (F b)) \<Longrightarrow>
+ eventually P (INF b:B. F b) \<longleftrightarrow> (\<exists>b\<in>B. eventually P (F b))"
+ unfolding INF_def by (subst eventually_Inf_base) auto
+
+
+subsubsection {* Map function for filters *}
+
+definition filtermap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a filter \<Rightarrow> 'b filter"
+ where "filtermap f F = Abs_filter (\<lambda>P. eventually (\<lambda>x. P (f x)) F)"
+
+lemma eventually_filtermap:
+ "eventually P (filtermap f F) = eventually (\<lambda>x. P (f x)) F"
+ unfolding filtermap_def
+ apply (rule eventually_Abs_filter)
+ apply (rule is_filter.intro)
+ apply (auto elim!: eventually_rev_mp)
+ done
+
+lemma filtermap_ident: "filtermap (\<lambda>x. x) F = F"
+ by (simp add: filter_eq_iff eventually_filtermap)
+
+lemma filtermap_filtermap:
+ "filtermap f (filtermap g F) = filtermap (\<lambda>x. f (g x)) F"
+ by (simp add: filter_eq_iff eventually_filtermap)
+
+lemma filtermap_mono: "F \<le> F' \<Longrightarrow> filtermap f F \<le> filtermap f F'"
+ unfolding le_filter_def eventually_filtermap by simp
+
+lemma filtermap_bot [simp]: "filtermap f bot = bot"
+ by (simp add: filter_eq_iff eventually_filtermap)
+
+lemma filtermap_sup: "filtermap f (sup F1 F2) = sup (filtermap f F1) (filtermap f F2)"
+ by (auto simp: filter_eq_iff eventually_filtermap eventually_sup)
+
+lemma filtermap_inf: "filtermap f (inf F1 F2) \<le> inf (filtermap f F1) (filtermap f F2)"
+ by (auto simp: le_filter_def eventually_filtermap eventually_inf)
+
+lemma filtermap_INF: "filtermap f (INF b:B. F b) \<le> (INF b:B. filtermap f (F b))"
+proof -
+ { fix X :: "'c set" assume "finite X"
+ then have "filtermap f (INFIMUM X F) \<le> (INF b:X. filtermap f (F b))"
+ proof induct
+ case (insert x X)
+ have "filtermap f (INF a:insert x X. F a) \<le> inf (filtermap f (F x)) (filtermap f (INF a:X. F a))"
+ by (rule order_trans[OF _ filtermap_inf]) simp
+ also have "\<dots> \<le> inf (filtermap f (F x)) (INF a:X. filtermap f (F a))"
+ by (intro inf_mono insert order_refl)
+ finally show ?case
+ by simp
+ qed simp }
+ then show ?thesis
+ unfolding le_filter_def eventually_filtermap
+ by (subst (1 2) eventually_INF) auto
+qed
+subsubsection {* Standard filters *}
+
+definition principal :: "'a set \<Rightarrow> 'a filter" where
+ "principal S = Abs_filter (\<lambda>P. \<forall>x\<in>S. P x)"
+
+lemma eventually_principal: "eventually P (principal S) \<longleftrightarrow> (\<forall>x\<in>S. P x)"
+ unfolding principal_def
+ by (rule eventually_Abs_filter, rule is_filter.intro) auto
+
+lemma eventually_inf_principal: "eventually P (inf F (principal s)) \<longleftrightarrow> eventually (\<lambda>x. x \<in> s \<longrightarrow> P x) F"
+ unfolding eventually_inf eventually_principal by (auto elim: eventually_elim1)
+
+lemma principal_UNIV[simp]: "principal UNIV = top"
+ by (auto simp: filter_eq_iff eventually_principal)
+
+lemma principal_empty[simp]: "principal {} = bot"
+ by (auto simp: filter_eq_iff eventually_principal)
+
+lemma principal_eq_bot_iff: "principal X = bot \<longleftrightarrow> X = {}"
+ by (auto simp add: filter_eq_iff eventually_principal)
+
+lemma principal_le_iff[iff]: "principal A \<le> principal B \<longleftrightarrow> A \<subseteq> B"
+ by (auto simp: le_filter_def eventually_principal)
+
+lemma le_principal: "F \<le> principal A \<longleftrightarrow> eventually (\<lambda>x. x \<in> A) F"
+ unfolding le_filter_def eventually_principal
+ apply safe
+ apply (erule_tac x="\<lambda>x. x \<in> A" in allE)
+ apply (auto elim: eventually_elim1)
+ done
+
+lemma principal_inject[iff]: "principal A = principal B \<longleftrightarrow> A = B"
+ unfolding eq_iff by simp
+
+lemma sup_principal[simp]: "sup (principal A) (principal B) = principal (A \<union> B)"
+ unfolding filter_eq_iff eventually_sup eventually_principal by auto
+
+lemma inf_principal[simp]: "inf (principal A) (principal B) = principal (A \<inter> B)"
+ unfolding filter_eq_iff eventually_inf eventually_principal
+ by (auto intro: exI[of _ "\<lambda>x. x \<in> A"] exI[of _ "\<lambda>x. x \<in> B"])
+
+lemma SUP_principal[simp]: "(SUP i : I. principal (A i)) = principal (\<Union>i\<in>I. A i)"
+ unfolding filter_eq_iff eventually_Sup SUP_def by (auto simp: eventually_principal)
+
+lemma INF_principal_finite: "finite X \<Longrightarrow> (INF x:X. principal (f x)) = principal (\<Inter>x\<in>X. f x)"
+ by (induct X rule: finite_induct) auto
+
+lemma filtermap_principal[simp]: "filtermap f (principal A) = principal (f ` A)"
+ unfolding filter_eq_iff eventually_filtermap eventually_principal by simp
+
+subsubsection {* Order filters *}
+
+definition at_top :: "('a::order) filter"
+ where "at_top = (INF k. principal {k ..})"
+
+lemma at_top_sub: "at_top = (INF k:{c::'a::linorder..}. principal {k ..})"
+ by (auto intro!: INF_eq max.cobounded1 max.cobounded2 simp: at_top_def)
+
+lemma eventually_at_top_linorder: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::linorder. \<forall>n\<ge>N. P n)"
+ unfolding at_top_def
+ by (subst eventually_INF_base) (auto simp: eventually_principal intro: max.cobounded1 max.cobounded2)
+
+lemma eventually_ge_at_top:
+ "eventually (\<lambda>x. (c::_::linorder) \<le> x) at_top"
+ unfolding eventually_at_top_linorder by auto
+
+lemma eventually_at_top_dense: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::{no_top, linorder}. \<forall>n>N. P n)"
+proof -
+ have "eventually P (INF k. principal {k <..}) \<longleftrightarrow> (\<exists>N::'a. \<forall>n>N. P n)"
+ by (subst eventually_INF_base) (auto simp: eventually_principal intro: max.cobounded1 max.cobounded2)
+ also have "(INF k. principal {k::'a <..}) = at_top"
+ unfolding at_top_def
+ by (intro INF_eq) (auto intro: less_imp_le simp: Ici_subset_Ioi_iff gt_ex)
+ finally show ?thesis .
+qed
+
+lemma eventually_gt_at_top:
+ "eventually (\<lambda>x. (c::_::unbounded_dense_linorder) < x) at_top"
+ unfolding eventually_at_top_dense by auto
+
+definition at_bot :: "('a::order) filter"
+ where "at_bot = (INF k. principal {.. k})"
+
+lemma at_bot_sub: "at_bot = (INF k:{.. c::'a::linorder}. principal {.. k})"
+ by (auto intro!: INF_eq min.cobounded1 min.cobounded2 simp: at_bot_def)
+
+lemma eventually_at_bot_linorder:
+ fixes P :: "'a::linorder \<Rightarrow> bool" shows "eventually P at_bot \<longleftrightarrow> (\<exists>N. \<forall>n\<le>N. P n)"
+ unfolding at_bot_def
+ by (subst eventually_INF_base) (auto simp: eventually_principal intro: min.cobounded1 min.cobounded2)
+
+lemma eventually_le_at_bot:
+ "eventually (\<lambda>x. x \<le> (c::_::linorder)) at_bot"
+ unfolding eventually_at_bot_linorder by auto
+
+lemma eventually_at_bot_dense: "eventually P at_bot \<longleftrightarrow> (\<exists>N::'a::{no_bot, linorder}. \<forall>n<N. P n)"
+proof -
+ have "eventually P (INF k. principal {..< k}) \<longleftrightarrow> (\<exists>N::'a. \<forall>n<N. P n)"
+ by (subst eventually_INF_base) (auto simp: eventually_principal intro: min.cobounded1 min.cobounded2)
+ also have "(INF k. principal {..< k::'a}) = at_bot"
+ unfolding at_bot_def
+ by (intro INF_eq) (auto intro: less_imp_le simp: Iic_subset_Iio_iff lt_ex)
+ finally show ?thesis .
+qed
+
+lemma eventually_gt_at_bot:
+ "eventually (\<lambda>x. x < (c::_::unbounded_dense_linorder)) at_bot"
+ unfolding eventually_at_bot_dense by auto
+
+lemma trivial_limit_at_bot_linorder: "\<not> trivial_limit (at_bot ::('a::linorder) filter)"
+ unfolding trivial_limit_def
+ by (metis eventually_at_bot_linorder order_refl)
+
+lemma trivial_limit_at_top_linorder: "\<not> trivial_limit (at_top ::('a::linorder) filter)"
+ unfolding trivial_limit_def
+ by (metis eventually_at_top_linorder order_refl)
+
+subsection {* Sequentially *}
+
+abbreviation sequentially :: "nat filter"
+ where "sequentially \<equiv> at_top"
+
+lemma eventually_sequentially:
+ "eventually P sequentially \<longleftrightarrow> (\<exists>N. \<forall>n\<ge>N. P n)"
+ by (rule eventually_at_top_linorder)
+
+lemma sequentially_bot [simp, intro]: "sequentially \<noteq> bot"
+ unfolding filter_eq_iff eventually_sequentially by auto
+
+lemmas trivial_limit_sequentially = sequentially_bot
+
+lemma eventually_False_sequentially [simp]:
+ "\<not> eventually (\<lambda>n. False) sequentially"
+ by (simp add: eventually_False)
+
+lemma le_sequentially:
+ "F \<le> sequentially \<longleftrightarrow> (\<forall>N. eventually (\<lambda>n. N \<le> n) F)"
+ by (simp add: at_top_def le_INF_iff le_principal)
+
+lemma eventually_sequentiallyI:
+ assumes "\<And>x. c \<le> x \<Longrightarrow> P x"
+ shows "eventually P sequentially"
+using assms by (auto simp: eventually_sequentially)
+
+lemma eventually_sequentially_Suc: "eventually (\<lambda>i. P (Suc i)) sequentially \<longleftrightarrow> eventually P sequentially"
+ unfolding eventually_sequentially by (metis Suc_le_D Suc_le_mono le_Suc_eq)
+
+lemma eventually_sequentially_seg: "eventually (\<lambda>n. P (n + k)) sequentially \<longleftrightarrow> eventually P sequentially"
+ using eventually_sequentially_Suc[of "\<lambda>n. P (n + k)" for k] by (induction k) auto
+
+subsection \<open> The cofinite filter \<close>
+
+definition "cofinite = Abs_filter (\<lambda>P. finite {x. \<not> P x})"
+
+abbreviation Inf_many :: "('a \<Rightarrow> bool) \<Rightarrow> bool" (binder "INFM " 10) where
+ "Inf_many P \<equiv> frequently P cofinite"
+
+abbreviation Alm_all :: "('a \<Rightarrow> bool) \<Rightarrow> bool" (binder "MOST " 10) where
+ "Alm_all P \<equiv> eventually P cofinite"
+
+notation (xsymbols)
+ Inf_many (binder "\<exists>\<^sub>\<infinity>" 10) and
+ Alm_all (binder "\<forall>\<^sub>\<infinity>" 10)
+
+notation (HTML output)
+ Inf_many (binder "\<exists>\<^sub>\<infinity>" 10) and
+ Alm_all (binder "\<forall>\<^sub>\<infinity>" 10)
+
+lemma eventually_cofinite: "eventually P cofinite \<longleftrightarrow> finite {x. \<not> P x}"
+ unfolding cofinite_def
+proof (rule eventually_Abs_filter, rule is_filter.intro)
+ fix P Q :: "'a \<Rightarrow> bool" assume "finite {x. \<not> P x}" "finite {x. \<not> Q x}"
+ from finite_UnI[OF this] show "finite {x. \<not> (P x \<and> Q x)}"
+ by (rule rev_finite_subset) auto
+next
+ fix P Q :: "'a \<Rightarrow> bool" assume P: "finite {x. \<not> P x}" and *: "\<forall>x. P x \<longrightarrow> Q x"
+ from * show "finite {x. \<not> Q x}"
+ by (intro finite_subset[OF _ P]) auto
+qed simp
+
+lemma frequently_cofinite: "frequently P cofinite \<longleftrightarrow> \<not> finite {x. P x}"
+ by (simp add: frequently_def eventually_cofinite)
+
+lemma cofinite_bot[simp]: "cofinite = (bot::'a filter) \<longleftrightarrow> finite (UNIV :: 'a set)"
+ unfolding trivial_limit_def eventually_cofinite by simp
+
+lemma cofinite_eq_sequentially: "cofinite = sequentially"
+ unfolding filter_eq_iff eventually_sequentially eventually_cofinite
+proof safe
+ fix P :: "nat \<Rightarrow> bool" assume [simp]: "finite {x. \<not> P x}"
+ show "\<exists>N. \<forall>n\<ge>N. P n"
+ proof cases
+ assume "{x. \<not> P x} \<noteq> {}" then show ?thesis
+ by (intro exI[of _ "Suc (Max {x. \<not> P x})"]) (auto simp: Suc_le_eq)
+ qed auto
+next
+ fix P :: "nat \<Rightarrow> bool" and N :: nat assume "\<forall>n\<ge>N. P n"
+ then have "{x. \<not> P x} \<subseteq> {..< N}"
+ by (auto simp: not_le)
+ then show "finite {x. \<not> P x}"
+ by (blast intro: finite_subset)
+qed
+
+subsection {* Limits *}
+
+definition filterlim :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b filter \<Rightarrow> 'a filter \<Rightarrow> bool" where
+ "filterlim f F2 F1 \<longleftrightarrow> filtermap f F1 \<le> F2"
+
+syntax
+ "_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"
+
+lemma filterlim_iff:
+ "(LIM x F1. f x :> F2) \<longleftrightarrow> (\<forall>P. eventually P F2 \<longrightarrow> eventually (\<lambda>x. P (f x)) F1)"
+ unfolding filterlim_def le_filter_def eventually_filtermap ..
+
+lemma filterlim_compose:
+ "filterlim g F3 F2 \<Longrightarrow> filterlim f F2 F1 \<Longrightarrow> filterlim (\<lambda>x. g (f x)) F3 F1"
+ unfolding filterlim_def filtermap_filtermap[symmetric] by (metis filtermap_mono order_trans)
+
+lemma filterlim_mono:
+ "filterlim f F2 F1 \<Longrightarrow> F2 \<le> F2' \<Longrightarrow> F1' \<le> F1 \<Longrightarrow> filterlim f F2' F1'"
+ unfolding filterlim_def by (metis filtermap_mono order_trans)
+
+lemma filterlim_ident: "LIM x F. x :> F"
+ by (simp add: filterlim_def filtermap_ident)
+
+lemma filterlim_cong:
+ "F1 = F1' \<Longrightarrow> F2 = F2' \<Longrightarrow> eventually (\<lambda>x. f x = g x) F2 \<Longrightarrow> filterlim f F1 F2 = filterlim g F1' F2'"
+ by (auto simp: filterlim_def le_filter_def eventually_filtermap elim: eventually_elim2)
+
+lemma filterlim_mono_eventually:
+ assumes "filterlim f F G" and ord: "F \<le> F'" "G' \<le> G"
+ assumes eq: "eventually (\<lambda>x. f x = f' x) G'"
+ shows "filterlim f' F' G'"
+ apply (rule filterlim_cong[OF refl refl eq, THEN iffD1])
+ apply (rule filterlim_mono[OF _ ord])
+ apply fact
+ done
+
+lemma filtermap_mono_strong: "inj f \<Longrightarrow> filtermap f F \<le> filtermap f G \<longleftrightarrow> F \<le> G"
+ apply (auto intro!: filtermap_mono) []
+ apply (auto simp: le_filter_def eventually_filtermap)
+ apply (erule_tac x="\<lambda>x. P (inv f x)" in allE)
+ apply auto
+ done
+
+lemma filtermap_eq_strong: "inj f \<Longrightarrow> filtermap f F = filtermap f G \<longleftrightarrow> F = G"
+ by (simp add: filtermap_mono_strong eq_iff)
+
+lemma filterlim_principal:
+ "(LIM x F. f x :> principal S) \<longleftrightarrow> (eventually (\<lambda>x. f x \<in> S) F)"
+ unfolding filterlim_def eventually_filtermap le_principal ..
+
+lemma filterlim_inf:
+ "(LIM x F1. f x :> inf F2 F3) \<longleftrightarrow> ((LIM x F1. f x :> F2) \<and> (LIM x F1. f x :> F3))"
+ unfolding filterlim_def by simp
+
+lemma filterlim_INF:
+ "(LIM x F. f x :> (INF b:B. G b)) \<longleftrightarrow> (\<forall>b\<in>B. LIM x F. f x :> G b)"
+ unfolding filterlim_def le_INF_iff ..
+
+lemma filterlim_INF_INF:
+ "(\<And>m. m \<in> J \<Longrightarrow> \<exists>i\<in>I. filtermap f (F i) \<le> G m) \<Longrightarrow> LIM x (INF i:I. F i). f x :> (INF j:J. G j)"
+ unfolding filterlim_def by (rule order_trans[OF filtermap_INF INF_mono])
+
+lemma filterlim_base:
+ "(\<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>
+ LIM x (INF i:I. principal (F i)). f x :> (INF j:J. principal (G j))"
+ by (force intro!: filterlim_INF_INF simp: image_subset_iff)
+
+lemma filterlim_base_iff:
+ 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"
+ shows "(LIM x (INF i:I. principal (F i)). f x :> INF j:J. principal (G j)) \<longleftrightarrow>
+ (\<forall>j\<in>J. \<exists>i\<in>I. \<forall>x\<in>F i. f x \<in> G j)"
+ unfolding filterlim_INF filterlim_principal
+proof (subst eventually_INF_base)
+ fix i j assume "i \<in> I" "j \<in> I"
+ with chain[OF this] show "\<exists>x\<in>I. principal (F x) \<le> inf (principal (F i)) (principal (F j))"
+ by auto
+qed (auto simp: eventually_principal `I \<noteq> {}`)
+
+lemma filterlim_filtermap: "filterlim f F1 (filtermap g F2) = filterlim (\<lambda>x. f (g x)) F1 F2"
+ unfolding filterlim_def filtermap_filtermap ..
+
+lemma filterlim_sup:
+ "filterlim f F F1 \<Longrightarrow> filterlim f F F2 \<Longrightarrow> filterlim f F (sup F1 F2)"
+ unfolding filterlim_def filtermap_sup by auto
+
+lemma filterlim_sequentially_Suc:
+ "(LIM x sequentially. f (Suc x) :> F) \<longleftrightarrow> (LIM x sequentially. f x :> F)"
+ unfolding filterlim_iff by (subst eventually_sequentially_Suc) simp
+
+lemma filterlim_Suc: "filterlim Suc sequentially sequentially"
+ by (simp add: filterlim_iff eventually_sequentially) (metis le_Suc_eq)
+
+
+subsection {* Limits to @{const at_top} and @{const at_bot} *}
+
+lemma filterlim_at_top:
+ fixes f :: "'a \<Rightarrow> ('b::linorder)"
+ shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. Z \<le> f x) F)"
+ by (auto simp: filterlim_iff eventually_at_top_linorder elim!: eventually_elim1)
+
+lemma filterlim_at_top_mono:
+ "LIM x F. f x :> at_top \<Longrightarrow> eventually (\<lambda>x. f x \<le> (g x::'a::linorder)) F \<Longrightarrow>
+ LIM x F. g x :> at_top"
+ by (auto simp: filterlim_at_top elim: eventually_elim2 intro: order_trans)
+
+lemma filterlim_at_top_dense:
+ fixes f :: "'a \<Rightarrow> ('b::unbounded_dense_linorder)"
+ shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. Z < f x) F)"
+ by (metis eventually_elim1[of _ F] eventually_gt_at_top order_less_imp_le
+ filterlim_at_top[of f F] filterlim_iff[of f at_top F])
+
+lemma filterlim_at_top_ge:
+ fixes f :: "'a \<Rightarrow> ('b::linorder)" and c :: "'b"
+ shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z\<ge>c. eventually (\<lambda>x. Z \<le> f x) F)"
+ unfolding at_top_sub[of c] filterlim_INF by (auto simp add: filterlim_principal)
+
+lemma filterlim_at_top_at_top:
+ fixes f :: "'a::linorder \<Rightarrow> 'b::linorder"
+ assumes mono: "\<And>x y. Q x \<Longrightarrow> Q y \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
+ assumes bij: "\<And>x. P x \<Longrightarrow> f (g x) = x" "\<And>x. P x \<Longrightarrow> Q (g x)"
+ assumes Q: "eventually Q at_top"
+ assumes P: "eventually P at_top"
+ shows "filterlim f at_top at_top"
+proof -
+ from P obtain x where x: "\<And>y. x \<le> y \<Longrightarrow> P y"
+ unfolding eventually_at_top_linorder by auto
+ show ?thesis
+ proof (intro filterlim_at_top_ge[THEN iffD2] allI impI)
+ fix z assume "x \<le> z"
+ with x have "P z" by auto
+ have "eventually (\<lambda>x. g z \<le> x) at_top"
+ by (rule eventually_ge_at_top)
+ with Q show "eventually (\<lambda>x. z \<le> f x) at_top"
+ by eventually_elim (metis mono bij `P z`)
+ qed
+qed
+
+lemma filterlim_at_top_gt:
+ fixes f :: "'a \<Rightarrow> ('b::unbounded_dense_linorder)" and c :: "'b"
+ shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z>c. eventually (\<lambda>x. Z \<le> f x) F)"
+ by (metis filterlim_at_top order_less_le_trans gt_ex filterlim_at_top_ge)
+
+lemma filterlim_at_bot:
+ fixes f :: "'a \<Rightarrow> ('b::linorder)"
+ shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. f x \<le> Z) F)"
+ by (auto simp: filterlim_iff eventually_at_bot_linorder elim!: eventually_elim1)
+
+lemma filterlim_at_bot_dense:
+ fixes f :: "'a \<Rightarrow> ('b::{dense_linorder, no_bot})"
+ shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. f x < Z) F)"
+proof (auto simp add: filterlim_at_bot[of f F])
+ fix Z :: 'b
+ from lt_ex [of Z] obtain Z' where 1: "Z' < Z" ..
+ assume "\<forall>Z. eventually (\<lambda>x. f x \<le> Z) F"
+ hence "eventually (\<lambda>x. f x \<le> Z') F" by auto
+ thus "eventually (\<lambda>x. f x < Z) F"
+ apply (rule eventually_mono[rotated])
+ using 1 by auto
+ next
+ fix Z :: 'b
+ show "\<forall>Z. eventually (\<lambda>x. f x < Z) F \<Longrightarrow> eventually (\<lambda>x. f x \<le> Z) F"
+ by (drule spec [of _ Z], erule eventually_mono[rotated], auto simp add: less_imp_le)
+qed
+
+lemma filterlim_at_bot_le:
+ fixes f :: "'a \<Rightarrow> ('b::linorder)" and c :: "'b"
+ shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z\<le>c. eventually (\<lambda>x. Z \<ge> f x) F)"
+ unfolding filterlim_at_bot
+proof safe
+ fix Z assume *: "\<forall>Z\<le>c. eventually (\<lambda>x. Z \<ge> f x) F"
+ with *[THEN spec, of "min Z c"] show "eventually (\<lambda>x. Z \<ge> f x) F"
+ by (auto elim!: eventually_elim1)
+qed simp
+
+lemma filterlim_at_bot_lt:
+ fixes f :: "'a \<Rightarrow> ('b::unbounded_dense_linorder)" and c :: "'b"
+ shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z<c. eventually (\<lambda>x. Z \<ge> f x) F)"
+ by (metis filterlim_at_bot filterlim_at_bot_le lt_ex order_le_less_trans)
+
+
+subsection {* Setup @{typ "'a filter"} for lifting and transfer *}
+
+context begin interpretation lifting_syntax .
+
+definition rel_filter :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> 'b filter \<Rightarrow> bool"
+where "rel_filter R F G = ((R ===> op =) ===> op =) (Rep_filter F) (Rep_filter G)"
+
+lemma rel_filter_eventually:
+ "rel_filter R F G \<longleftrightarrow>
+ ((R ===> op =) ===> op =) (\<lambda>P. eventually P F) (\<lambda>P. eventually P G)"
+by(simp add: rel_filter_def eventually_def)
+
+lemma filtermap_id [simp, id_simps]: "filtermap id = id"
+by(simp add: fun_eq_iff id_def filtermap_ident)
+
+lemma filtermap_id' [simp]: "filtermap (\<lambda>x. x) = (\<lambda>F. F)"
+using filtermap_id unfolding id_def .
+
+lemma Quotient_filter [quot_map]:
+ assumes Q: "Quotient R Abs Rep T"
+ shows "Quotient (rel_filter R) (filtermap Abs) (filtermap Rep) (rel_filter T)"
+unfolding Quotient_alt_def
+proof(intro conjI strip)
+ from Q have *: "\<And>x y. T x y \<Longrightarrow> Abs x = y"
+ unfolding Quotient_alt_def by blast
+
+ fix F G
+ assume "rel_filter T F G"
+ thus "filtermap Abs F = G" unfolding filter_eq_iff
+ by(auto simp add: eventually_filtermap rel_filter_eventually * rel_funI del: iffI elim!: rel_funD)
+next
+ from Q have *: "\<And>x. T (Rep x) x" unfolding Quotient_alt_def by blast
+
+ fix F
+ show "rel_filter T (filtermap Rep F) F"
+ by(auto elim: rel_funD intro: * intro!: ext arg_cong[where f="\<lambda>P. eventually P F"] rel_funI
+ del: iffI simp add: eventually_filtermap rel_filter_eventually)
+qed(auto simp add: map_fun_def o_def eventually_filtermap filter_eq_iff fun_eq_iff rel_filter_eventually
+ fun_quotient[OF fun_quotient[OF Q identity_quotient] identity_quotient, unfolded Quotient_alt_def])
+
+lemma eventually_parametric [transfer_rule]:
+ "((A ===> op =) ===> rel_filter A ===> op =) eventually eventually"
+by(simp add: rel_fun_def rel_filter_eventually)
+
+lemma frequently_parametric [transfer_rule]:
+ "((A ===> op =) ===> rel_filter A ===> op =) frequently frequently"
+ unfolding frequently_def[abs_def] by transfer_prover
+
+lemma rel_filter_eq [relator_eq]: "rel_filter op = = op ="
+by(auto simp add: rel_filter_eventually rel_fun_eq fun_eq_iff filter_eq_iff)
+
+lemma rel_filter_mono [relator_mono]:
+ "A \<le> B \<Longrightarrow> rel_filter A \<le> rel_filter B"
+unfolding rel_filter_eventually[abs_def]
+by(rule le_funI)+(intro fun_mono fun_mono[THEN le_funD, THEN le_funD] order.refl)
+
+lemma rel_filter_conversep [simp]: "rel_filter A\<inverse>\<inverse> = (rel_filter A)\<inverse>\<inverse>"
+by(auto simp add: rel_filter_eventually fun_eq_iff rel_fun_def)
+
+lemma is_filter_parametric_aux:
+ assumes "is_filter F"
+ assumes [transfer_rule]: "bi_total A" "bi_unique A"
+ and [transfer_rule]: "((A ===> op =) ===> op =) F G"
+ shows "is_filter G"
+proof -
+ interpret is_filter F by fact
+ show ?thesis
+ proof
+ have "F (\<lambda>_. True) = G (\<lambda>x. True)" by transfer_prover
+ thus "G (\<lambda>x. True)" by(simp add: True)
+ next
+ fix P' Q'
+ assume "G P'" "G Q'"
+ moreover
+ from bi_total_fun[OF `bi_unique A` bi_total_eq, unfolded bi_total_def]
+ obtain P Q where [transfer_rule]: "(A ===> op =) P P'" "(A ===> op =) Q Q'" by blast
+ have "F P = G P'" "F Q = G Q'" by transfer_prover+
+ ultimately have "F (\<lambda>x. P x \<and> Q x)" by(simp add: conj)
+ moreover have "F (\<lambda>x. P x \<and> Q x) = G (\<lambda>x. P' x \<and> Q' x)" by transfer_prover
+ ultimately show "G (\<lambda>x. P' x \<and> Q' x)" by simp
+ next
+ fix P' Q'
+ assume "\<forall>x. P' x \<longrightarrow> Q' x" "G P'"
+ moreover
+ from bi_total_fun[OF `bi_unique A` bi_total_eq, unfolded bi_total_def]
+ obtain P Q where [transfer_rule]: "(A ===> op =) P P'" "(A ===> op =) Q Q'" by blast
+ have "F P = G P'" by transfer_prover
+ moreover have "(\<forall>x. P x \<longrightarrow> Q x) \<longleftrightarrow> (\<forall>x. P' x \<longrightarrow> Q' x)" by transfer_prover
+ ultimately have "F Q" by(simp add: mono)
+ moreover have "F Q = G Q'" by transfer_prover
+ ultimately show "G Q'" by simp
+ qed
+qed
+
+lemma is_filter_parametric [transfer_rule]:
+ "\<lbrakk> bi_total A; bi_unique A \<rbrakk>
+ \<Longrightarrow> (((A ===> op =) ===> op =) ===> op =) is_filter is_filter"
+apply(rule rel_funI)
+apply(rule iffI)
+ apply(erule (3) is_filter_parametric_aux)
+apply(erule is_filter_parametric_aux[where A="conversep A"])
+apply(auto simp add: rel_fun_def)
+done
+
+lemma left_total_rel_filter [transfer_rule]:
+ assumes [transfer_rule]: "bi_total A" "bi_unique A"
+ shows "left_total (rel_filter A)"
+proof(rule left_totalI)
+ fix F :: "'a filter"
+ from bi_total_fun[OF bi_unique_fun[OF `bi_total A` bi_unique_eq] bi_total_eq]
+ obtain G where [transfer_rule]: "((A ===> op =) ===> op =) (\<lambda>P. eventually P F) G"
+ unfolding bi_total_def by blast
+ moreover have "is_filter (\<lambda>P. eventually P F) \<longleftrightarrow> is_filter G" by transfer_prover
+ hence "is_filter G" by(simp add: eventually_def is_filter_Rep_filter)
+ ultimately have "rel_filter A F (Abs_filter G)"
+ by(simp add: rel_filter_eventually eventually_Abs_filter)
+ thus "\<exists>G. rel_filter A F G" ..
+qed
+
+lemma right_total_rel_filter [transfer_rule]:
+ "\<lbrakk> bi_total A; bi_unique A \<rbrakk> \<Longrightarrow> right_total (rel_filter A)"
+using left_total_rel_filter[of "A\<inverse>\<inverse>"] by simp
+
+lemma bi_total_rel_filter [transfer_rule]:
+ assumes "bi_total A" "bi_unique A"
+ shows "bi_total (rel_filter A)"
+unfolding bi_total_alt_def using assms
+by(simp add: left_total_rel_filter right_total_rel_filter)
+
+lemma left_unique_rel_filter [transfer_rule]:
+ assumes "left_unique A"
+ shows "left_unique (rel_filter A)"
+proof(rule left_uniqueI)
+ fix F F' G
+ assume [transfer_rule]: "rel_filter A F G" "rel_filter A F' G"
+ show "F = F'"
+ unfolding filter_eq_iff
+ proof
+ fix P :: "'a \<Rightarrow> bool"
+ obtain P' where [transfer_rule]: "(A ===> op =) P P'"
+ using left_total_fun[OF assms left_total_eq] unfolding left_total_def by blast
+ have "eventually P F = eventually P' G"
+ and "eventually P F' = eventually P' G" by transfer_prover+
+ thus "eventually P F = eventually P F'" by simp
+ qed
+qed
+
+lemma right_unique_rel_filter [transfer_rule]:
+ "right_unique A \<Longrightarrow> right_unique (rel_filter A)"
+using left_unique_rel_filter[of "A\<inverse>\<inverse>"] by simp
+
+lemma bi_unique_rel_filter [transfer_rule]:
+ "bi_unique A \<Longrightarrow> bi_unique (rel_filter A)"
+by(simp add: bi_unique_alt_def left_unique_rel_filter right_unique_rel_filter)
+
+lemma top_filter_parametric [transfer_rule]:
+ "bi_total A \<Longrightarrow> (rel_filter A) top top"
+by(simp add: rel_filter_eventually All_transfer)
+
+lemma bot_filter_parametric [transfer_rule]: "(rel_filter A) bot bot"
+by(simp add: rel_filter_eventually rel_fun_def)
+
+lemma sup_filter_parametric [transfer_rule]:
+ "(rel_filter A ===> rel_filter A ===> rel_filter A) sup sup"
+by(fastforce simp add: rel_filter_eventually[abs_def] eventually_sup dest: rel_funD)
+
+lemma Sup_filter_parametric [transfer_rule]:
+ "(rel_set (rel_filter A) ===> rel_filter A) Sup Sup"
+proof(rule rel_funI)
+ fix S T
+ assume [transfer_rule]: "rel_set (rel_filter A) S T"
+ show "rel_filter A (Sup S) (Sup T)"
+ by(simp add: rel_filter_eventually eventually_Sup) transfer_prover
+qed
+
+lemma principal_parametric [transfer_rule]:
+ "(rel_set A ===> rel_filter A) principal principal"
+proof(rule rel_funI)
+ fix S S'
+ assume [transfer_rule]: "rel_set A S S'"
+ show "rel_filter A (principal S) (principal S')"
+ by(simp add: rel_filter_eventually eventually_principal) transfer_prover
+qed
+
+context
+ fixes A :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
+ assumes [transfer_rule]: "bi_unique A"
+begin
+
+lemma le_filter_parametric [transfer_rule]:
+ "(rel_filter A ===> rel_filter A ===> op =) op \<le> op \<le>"
+unfolding le_filter_def[abs_def] by transfer_prover
+
+lemma less_filter_parametric [transfer_rule]:
+ "(rel_filter A ===> rel_filter A ===> op =) op < op <"
+unfolding less_filter_def[abs_def] by transfer_prover
+
+context
+ assumes [transfer_rule]: "bi_total A"
+begin
+
+lemma Inf_filter_parametric [transfer_rule]:
+ "(rel_set (rel_filter A) ===> rel_filter A) Inf Inf"
+unfolding Inf_filter_def[abs_def] by transfer_prover
+
+lemma inf_filter_parametric [transfer_rule]:
+ "(rel_filter A ===> rel_filter A ===> rel_filter A) inf inf"
+proof(intro rel_funI)+
+ fix F F' G G'
+ assume [transfer_rule]: "rel_filter A F F'" "rel_filter A G G'"
+ have "rel_filter A (Inf {F, G}) (Inf {F', G'})" by transfer_prover
+ thus "rel_filter A (inf F G) (inf F' G')" by simp
+qed
+
+end
+
+end
+
+end
+
+end
\ No newline at end of file
--- a/src/HOL/HOLCF/Library/Defl_Bifinite.thy Sun Apr 12 20:05:35 2015 +0200
+++ b/src/HOL/HOLCF/Library/Defl_Bifinite.thy Mon Apr 13 00:59:17 2015 +0200
@@ -12,38 +12,6 @@
default_sort type
-lemma MOST_INFM:
- assumes inf: "infinite (UNIV::'a set)"
- shows "MOST x::'a. P x \<Longrightarrow> INFM x::'a. P x"
- unfolding Alm_all_def Inf_many_def
- apply (auto simp add: Collect_neg_eq)
- apply (drule (1) finite_UnI)
- apply (simp add: Compl_partition2 inf)
- done
-
-lemma MOST_SucI: "MOST n. P n \<Longrightarrow> MOST n. P (Suc n)"
-by (rule MOST_inj [OF _ inj_Suc])
-
-lemma MOST_SucD: "MOST n. P (Suc n) \<Longrightarrow> MOST n. P n"
-unfolding MOST_nat
-apply (clarify, rule_tac x="Suc m" in exI, clarify)
-apply (erule Suc_lessE, simp)
-done
-
-lemma MOST_Suc_iff: "(MOST n. P (Suc n)) \<longleftrightarrow> (MOST n. P n)"
-by (rule iffI [OF MOST_SucD MOST_SucI])
-
-lemma INFM_finite_Bex_distrib:
- "finite A \<Longrightarrow> (INFM y. \<exists>x\<in>A. P x y) \<longleftrightarrow> (\<exists>x\<in>A. INFM y. P x y)"
-by (induct set: finite, simp, simp add: INFM_disj_distrib)
-
-lemma MOST_finite_Ball_distrib:
- "finite A \<Longrightarrow> (MOST y. \<forall>x\<in>A. P x y) \<longleftrightarrow> (\<forall>x\<in>A. MOST y. P x y)"
-by (induct set: finite, simp, simp add: MOST_conj_distrib)
-
-lemma MOST_ge_nat: "MOST n::nat. m \<le> n"
-unfolding MOST_nat_le by fast
-
subsection {* Eventually constant sequences *}
definition
--- a/src/HOL/HOLCF/Plain_HOLCF.thy Sun Apr 12 20:05:35 2015 +0200
+++ b/src/HOL/HOLCF/Plain_HOLCF.thy Mon Apr 13 00:59:17 2015 +0200
@@ -12,4 +12,6 @@
Basic HOLCF concepts and types; does not include definition packages.
*}
+hide_const (open) Filter.principal
+
end
--- a/src/HOL/Library/Infinite_Set.thy Sun Apr 12 20:05:35 2015 +0200
+++ b/src/HOL/Library/Infinite_Set.thy Mon Apr 13 00:59:17 2015 +0200
@@ -67,36 +67,22 @@
infinite.
*}
-lemma finite_nat_bounded: assumes S: "finite (S::nat set)" shows "\<exists>k. S \<subseteq> {..<k}"
-proof cases
- assume "S \<noteq> {}" with Max_less_iff[OF S this] show ?thesis
- by auto
-qed simp
+lemma infinite_nat_iff_unbounded_le: "infinite (S::nat set) \<longleftrightarrow> (\<forall>m. \<exists>n\<ge>m. n \<in> S)"
+ using frequently_cofinite[of "\<lambda>x. x \<in> S"]
+ by (simp add: cofinite_eq_sequentially frequently_def eventually_sequentially)
+
+lemma infinite_nat_iff_unbounded: "infinite (S::nat set) \<longleftrightarrow> (\<forall>m. \<exists>n>m. n \<in> S)"
+ using frequently_cofinite[of "\<lambda>x. x \<in> S"]
+ by (simp add: cofinite_eq_sequentially frequently_def eventually_at_top_dense)
lemma finite_nat_iff_bounded: "finite (S::nat set) \<longleftrightarrow> (\<exists>k. S \<subseteq> {..<k})"
- by (auto intro: finite_nat_bounded dest: finite_subset)
+ using infinite_nat_iff_unbounded_le[of S] by (simp add: subset_eq) (metis not_le)
-lemma finite_nat_iff_bounded_le:
- "finite (S::nat set) \<longleftrightarrow> (\<exists>k. S \<subseteq> {..k})" (is "?lhs \<longleftrightarrow> ?rhs")
-proof
- assume ?lhs
- then obtain k where "S \<subseteq> {..<k}"
- by (blast dest: finite_nat_bounded)
- then have "S \<subseteq> {..k}" by auto
- then show ?rhs ..
-next
- assume ?rhs
- then obtain k where "S \<subseteq> {..k}" ..
- then show "finite S"
- by (rule finite_subset) simp
-qed
+lemma finite_nat_iff_bounded_le: "finite (S::nat set) \<longleftrightarrow> (\<exists>k. S \<subseteq> {.. k})"
+ using infinite_nat_iff_unbounded[of S] by (simp add: subset_eq) (metis not_le)
-lemma infinite_nat_iff_unbounded: "infinite (S::nat set) \<longleftrightarrow> (\<forall>m. \<exists>n. m < n \<and> n \<in> S)"
- unfolding finite_nat_iff_bounded_le by (auto simp: subset_eq not_le)
-
-lemma infinite_nat_iff_unbounded_le:
- "infinite (S::nat set) \<longleftrightarrow> (\<forall>m. \<exists>n. m \<le> n \<and> n \<in> S)"
- unfolding finite_nat_iff_bounded by (auto simp: subset_eq not_less)
+lemma finite_nat_bounded: "finite (S::nat set) \<Longrightarrow> \<exists>k. S \<subseteq> {..<k}"
+ by (simp add: finite_nat_iff_bounded)
text {*
For a set of natural numbers to be infinite, it is enough to know
@@ -104,25 +90,9 @@
number that is an element of the set.
*}
-lemma unbounded_k_infinite:
- assumes k: "\<forall>m. k < m \<longrightarrow> (\<exists>n. m < n \<and> n \<in> S)"
- shows "infinite (S::nat set)"
-proof -
- {
- fix m have "\<exists>n. m < n \<and> n \<in> S"
- proof (cases "k < m")
- case True
- with k show ?thesis by blast
- next
- case False
- from k obtain n where "Suc k < n \<and> n \<in> S" by auto
- with False have "m < n \<and> n \<in> S" by auto
- then show ?thesis ..
- qed
- }
- then show ?thesis
- by (auto simp add: infinite_nat_iff_unbounded)
-qed
+lemma unbounded_k_infinite: "\<forall>m>k. \<exists>n>m. n \<in> S \<Longrightarrow> infinite (S::nat set)"
+ by (metis (full_types) infinite_nat_iff_unbounded_le le_imp_less_Suc not_less
+ not_less_iff_gr_or_eq sup.bounded_iff)
lemma nat_not_finite: "finite (UNIV::nat set) \<Longrightarrow> R"
by simp
@@ -178,181 +148,106 @@
we introduce corresponding binders and their proof rules.
*}
-definition Inf_many :: "('a \<Rightarrow> bool) \<Rightarrow> bool" (binder "INFM " 10)
- where "Inf_many P \<longleftrightarrow> infinite {x. P x}"
-
-definition Alm_all :: "('a \<Rightarrow> bool) \<Rightarrow> bool" (binder "MOST " 10)
- where "Alm_all P \<longleftrightarrow> \<not> (INFM x. \<not> P x)"
-
-notation (xsymbols)
- Inf_many (binder "\<exists>\<^sub>\<infinity>" 10) and
- Alm_all (binder "\<forall>\<^sub>\<infinity>" 10)
-
-notation (HTML output)
- Inf_many (binder "\<exists>\<^sub>\<infinity>" 10) and
- Alm_all (binder "\<forall>\<^sub>\<infinity>" 10)
-
-lemma INFM_iff_infinite: "(INFM x. P x) \<longleftrightarrow> infinite {x. P x}"
- unfolding Inf_many_def ..
-
-lemma MOST_iff_cofinite: "(MOST x. P x) \<longleftrightarrow> finite {x. \<not> P x}"
- unfolding Alm_all_def Inf_many_def by simp
-
-(* legacy name *)
-lemmas MOST_iff_finiteNeg = MOST_iff_cofinite
-
-lemma not_INFM [simp]: "\<not> (INFM x. P x) \<longleftrightarrow> (MOST x. \<not> P x)"
- unfolding Alm_all_def not_not ..
-
-lemma not_MOST [simp]: "\<not> (MOST x. P x) \<longleftrightarrow> (INFM x. \<not> P x)"
- unfolding Alm_all_def not_not ..
+(* The following two lemmas are available as filter-rules, but not in the simp-set *)
+lemma not_INFM [simp]: "\<not> (INFM x. P x) \<longleftrightarrow> (MOST x. \<not> P x)" by (fact not_frequently)
+lemma not_MOST [simp]: "\<not> (MOST x. P x) \<longleftrightarrow> (INFM x. \<not> P x)" by (fact not_eventually)
lemma INFM_const [simp]: "(INFM x::'a. P) \<longleftrightarrow> P \<and> infinite (UNIV::'a set)"
- unfolding Inf_many_def by simp
+ by (simp add: frequently_const_iff)
lemma MOST_const [simp]: "(MOST x::'a. P) \<longleftrightarrow> P \<or> finite (UNIV::'a set)"
- unfolding Alm_all_def by simp
-
-lemma INFM_EX: "(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)"
- apply (erule contrapos_pp)
- apply simp
- done
-
-lemma ALL_MOST: "\<forall>x. P x \<Longrightarrow> \<forall>\<^sub>\<infinity>x. P x"
- by simp
-
-lemma INFM_E:
- assumes "INFM x. P x"
- obtains x where "P x"
- using INFM_EX [OF assms] by (rule exE)
-
-lemma MOST_I:
- assumes "\<And>x. P x"
- shows "MOST x. P x"
- using assms by simp
+ by (simp add: eventually_const_iff)
-lemma INFM_mono:
- assumes inf: "\<exists>\<^sub>\<infinity>x. P x" and q: "\<And>x. P x \<Longrightarrow> Q x"
- shows "\<exists>\<^sub>\<infinity>x. Q x"
-proof -
- from inf have "infinite {x. P x}" unfolding Inf_many_def .
- moreover from q have "{x. P x} \<subseteq> {x. Q x}" by auto
- ultimately show ?thesis
- using Inf_many_def infinite_super by blast
-qed
-
-lemma MOST_mono: "\<forall>\<^sub>\<infinity>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> \<forall>\<^sub>\<infinity>x. Q x"
- unfolding Alm_all_def by (blast intro: INFM_mono)
-
-lemma INFM_disj_distrib:
- "(\<exists>\<^sub>\<infinity>x. P x \<or> Q x) \<longleftrightarrow> (\<exists>\<^sub>\<infinity>x. P x) \<or> (\<exists>\<^sub>\<infinity>x. Q x)"
- unfolding Inf_many_def by (simp add: Collect_disj_eq)
-
-lemma INFM_imp_distrib:
- "(INFM x. P x \<longrightarrow> Q x) \<longleftrightarrow> ((MOST x. P x) \<longrightarrow> (INFM x. Q x))"
- by (simp only: imp_conv_disj INFM_disj_distrib not_MOST)
+lemma INFM_imp_distrib: "(INFM x. P x \<longrightarrow> Q x) \<longleftrightarrow> ((MOST x. P x) \<longrightarrow> (INFM x. Q x))"
+ by (simp only: imp_conv_disj frequently_disj_iff not_eventually)
-lemma MOST_conj_distrib:
- "(\<forall>\<^sub>\<infinity>x. P x \<and> Q x) \<longleftrightarrow> (\<forall>\<^sub>\<infinity>x. P x) \<and> (\<forall>\<^sub>\<infinity>x. Q x)"
- unfolding Alm_all_def by (simp add: INFM_disj_distrib del: disj_not1)
-
-lemma MOST_conjI:
- "MOST x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> MOST x. P x \<and> Q x"
- by (simp add: MOST_conj_distrib)
-
-lemma INFM_conjI:
- "INFM x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> INFM x. P x \<and> Q x"
- unfolding MOST_iff_cofinite INFM_iff_infinite
- apply (drule (1) Diff_infinite_finite)
- apply (simp add: Collect_conj_eq Collect_neg_eq)
- done
+lemma MOST_imp_iff: "MOST x. P x \<Longrightarrow> (MOST x. P x \<longrightarrow> Q x) \<longleftrightarrow> (MOST x. Q x)"
+ by (auto intro: eventually_rev_mp eventually_elim1)
-lemma MOST_rev_mp:
- assumes "\<forall>\<^sub>\<infinity>x. P x" and "\<forall>\<^sub>\<infinity>x. P x \<longrightarrow> Q x"
- shows "\<forall>\<^sub>\<infinity>x. Q x"
-proof -
- have "\<forall>\<^sub>\<infinity>x. P x \<and> (P x \<longrightarrow> Q x)"
- using assms by (rule MOST_conjI)
- thus ?thesis by (rule MOST_mono) simp
-qed
-
-lemma MOST_imp_iff:
- assumes "MOST x. P x"
- shows "(MOST x. P x \<longrightarrow> Q x) \<longleftrightarrow> (MOST x. Q x)"
-proof
- assume "MOST x. P x \<longrightarrow> Q x"
- with assms show "MOST x. Q x" by (rule MOST_rev_mp)
-next
- assume "MOST x. Q x"
- then show "MOST x. P x \<longrightarrow> Q x" by (rule MOST_mono) simp
-qed
-
-lemma INFM_MOST_simps [simp]:
- "\<And>P Q. (INFM x. P x \<and> Q) \<longleftrightarrow> (INFM x. P x) \<and> Q"
- "\<And>P Q. (INFM x. P \<and> Q x) \<longleftrightarrow> P \<and> (INFM x. Q x)"
- "\<And>P Q. (MOST x. P x \<or> Q) \<longleftrightarrow> (MOST x. P x) \<or> Q"
- "\<And>P Q. (MOST x. P \<or> Q x) \<longleftrightarrow> P \<or> (MOST x. Q x)"
- "\<And>P Q. (MOST x. P x \<longrightarrow> Q) \<longleftrightarrow> ((INFM x. P x) \<longrightarrow> Q)"
- "\<And>P Q. (MOST x. P \<longrightarrow> Q x) \<longleftrightarrow> (P \<longrightarrow> (MOST x. Q x))"
- unfolding Alm_all_def Inf_many_def
- by (simp_all add: Collect_conj_eq)
+lemma INFM_conjI: "INFM x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> INFM x. P x \<and> Q x"
+ by (rule frequently_rev_mp[of P]) (auto elim: eventually_elim1)
text {* Properties of quantifiers with injective functions. *}
lemma INFM_inj: "INFM x. P (f x) \<Longrightarrow> inj f \<Longrightarrow> INFM x. P x"
- unfolding INFM_iff_infinite
- apply clarify
- apply (drule (1) finite_vimageI)
- apply simp
- done
+ using finite_vimageI[of "{x. P x}" f] by (auto simp: frequently_cofinite)
lemma MOST_inj: "MOST x. P x \<Longrightarrow> inj f \<Longrightarrow> MOST x. P (f x)"
- unfolding MOST_iff_cofinite
- apply (drule (1) finite_vimageI)
- apply simp
- done
+ using finite_vimageI[of "{x. \<not> P x}" f] by (auto simp: eventually_cofinite)
text {* Properties of quantifiers with singletons. *}
lemma not_INFM_eq [simp]:
"\<not> (INFM x. x = a)"
"\<not> (INFM x. a = x)"
- unfolding INFM_iff_infinite by simp_all
+ unfolding frequently_cofinite by simp_all
lemma MOST_neq [simp]:
"MOST x. x \<noteq> a"
"MOST x. a \<noteq> x"
- unfolding MOST_iff_cofinite by simp_all
+ unfolding eventually_cofinite by simp_all
lemma INFM_neq [simp]:
"(INFM x::'a. x \<noteq> a) \<longleftrightarrow> infinite (UNIV::'a set)"
"(INFM x::'a. a \<noteq> x) \<longleftrightarrow> infinite (UNIV::'a set)"
- unfolding INFM_iff_infinite by simp_all
+ unfolding frequently_cofinite by simp_all
lemma MOST_eq [simp]:
"(MOST x::'a. x = a) \<longleftrightarrow> finite (UNIV::'a set)"
"(MOST x::'a. a = x) \<longleftrightarrow> finite (UNIV::'a set)"
- unfolding MOST_iff_cofinite by simp_all
+ unfolding eventually_cofinite by simp_all
lemma MOST_eq_imp:
"MOST x. x = a \<longrightarrow> P x"
"MOST x. a = x \<longrightarrow> P x"
- unfolding MOST_iff_cofinite by simp_all
+ unfolding eventually_cofinite by simp_all
text {* Properties of quantifiers over the naturals. *}
-lemma INFM_nat: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<forall>m. \<exists>n. m < n \<and> P n)"
- by (simp add: Inf_many_def infinite_nat_iff_unbounded)
+lemma MOST_nat: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<exists>m. \<forall>n>m. P n)"
+ by (auto simp add: eventually_cofinite finite_nat_iff_bounded_le subset_eq not_le[symmetric])
+
+lemma MOST_nat_le: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<exists>m. \<forall>n\<ge>m. P n)"
+ by (auto simp add: eventually_cofinite finite_nat_iff_bounded subset_eq not_le[symmetric])
+
+lemma INFM_nat: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<forall>m. \<exists>n>m. P n)"
+ by (simp add: frequently_cofinite infinite_nat_iff_unbounded)
-lemma INFM_nat_le: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<forall>m. \<exists>n. m \<le> n \<and> P n)"
- by (simp add: Inf_many_def infinite_nat_iff_unbounded_le)
+lemma INFM_nat_le: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<forall>m. \<exists>n\<ge>m. P n)"
+ by (simp add: frequently_cofinite infinite_nat_iff_unbounded_le)
+
+lemma MOST_INFM: "infinite (UNIV::'a set) \<Longrightarrow> MOST x::'a. P x \<Longrightarrow> INFM x::'a. P x"
+ by (simp add: eventually_frequently)
+
+lemma MOST_Suc_iff: "(MOST n. P (Suc n)) \<longleftrightarrow> (MOST n. P n)"
+ by (simp add: cofinite_eq_sequentially eventually_sequentially_Suc)
-lemma MOST_nat: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<exists>m. \<forall>n. m < n \<longrightarrow> P n)"
- by (simp add: Alm_all_def INFM_nat)
+lemma
+ shows MOST_SucI: "MOST n. P n \<Longrightarrow> MOST n. P (Suc n)"
+ and MOST_SucD: "MOST n. P (Suc n) \<Longrightarrow> MOST n. P n"
+ by (simp_all add: MOST_Suc_iff)
+
+lemma MOST_ge_nat: "MOST n::nat. m \<le> n"
+ by (simp add: cofinite_eq_sequentially eventually_ge_at_top)
-lemma MOST_nat_le: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<exists>m. \<forall>n. m \<le> n \<longrightarrow> P n)"
- by (simp add: Alm_all_def INFM_nat_le)
-
+(* legacy names *)
+lemma Inf_many_def: "Inf_many P \<longleftrightarrow> infinite {x. P x}" by (fact frequently_cofinite)
+lemma Alm_all_def: "Alm_all P \<longleftrightarrow> \<not> (INFM x. \<not> P x)" by simp
+lemma INFM_iff_infinite: "(INFM x. P x) \<longleftrightarrow> infinite {x. P x}" by (fact frequently_cofinite)
+lemma MOST_iff_cofinite: "(MOST x. P x) \<longleftrightarrow> finite {x. \<not> P x}" by (fact eventually_cofinite)
+lemma INFM_EX: "(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)" by (fact frequently_ex)
+lemma ALL_MOST: "\<forall>x. P x \<Longrightarrow> \<forall>\<^sub>\<infinity>x. P x" by (fact always_eventually)
+lemma INFM_mono: "\<exists>\<^sub>\<infinity>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> \<exists>\<^sub>\<infinity>x. Q x" by (fact frequently_elim1)
+lemma MOST_mono: "\<forall>\<^sub>\<infinity>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> \<forall>\<^sub>\<infinity>x. Q x" by (fact eventually_elim1)
+lemma INFM_disj_distrib: "(\<exists>\<^sub>\<infinity>x. P x \<or> Q x) \<longleftrightarrow> (\<exists>\<^sub>\<infinity>x. P x) \<or> (\<exists>\<^sub>\<infinity>x. Q x)" by (fact frequently_disj_iff)
+lemma MOST_rev_mp: "\<forall>\<^sub>\<infinity>x. P x \<Longrightarrow> \<forall>\<^sub>\<infinity>x. P x \<longrightarrow> Q x \<Longrightarrow> \<forall>\<^sub>\<infinity>x. Q x" by (fact eventually_rev_mp)
+lemma MOST_conj_distrib: "(\<forall>\<^sub>\<infinity>x. P x \<and> Q x) \<longleftrightarrow> (\<forall>\<^sub>\<infinity>x. P x) \<and> (\<forall>\<^sub>\<infinity>x. Q x)" by (fact eventually_conj_iff)
+lemma MOST_conjI: "MOST x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> MOST x. P x \<and> Q x" by (fact eventually_conj)
+lemma INFM_finite_Bex_distrib: "finite A \<Longrightarrow> (INFM y. \<exists>x\<in>A. P x y) \<longleftrightarrow> (\<exists>x\<in>A. INFM y. P x y)" by (fact frequently_bex_finite_distrib)
+lemma MOST_finite_Ball_distrib: "finite A \<Longrightarrow> (MOST y. \<forall>x\<in>A. P x y) \<longleftrightarrow> (\<forall>x\<in>A. MOST y. P x y)" by (fact eventually_ball_finite_distrib)
+lemma INFM_E: "INFM x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> thesis) \<Longrightarrow> thesis" by (fact frequentlyE)
+lemma MOST_I: "(\<And>x. P x) \<Longrightarrow> MOST x. P x" by (rule eventuallyI)
+lemmas MOST_iff_finiteNeg = MOST_iff_cofinite
subsection "Enumeration of an Infinite Set"
@@ -360,6 +255,11 @@
The set's element type must be wellordered (e.g. the natural numbers).
*}
+text \<open>
+ Could be generalized to
+ @{term "enumerate' S n = (SOME t. t \<in> s \<and> finite {s\<in>S. s < t} \<and> card {s\<in>S. s < t} = n)"}.
+\<close>
+
primrec (in wellorder) enumerate :: "'a set \<Rightarrow> nat \<Rightarrow> 'a"
where
enumerate_0: "enumerate S 0 = (LEAST n. n \<in> S)"
@@ -368,7 +268,7 @@
lemma enumerate_Suc': "enumerate S (Suc n) = enumerate (S - {enumerate S 0}) n"
by simp
-lemma enumerate_in_set: "infinite S \<Longrightarrow> enumerate S n : S"
+lemma enumerate_in_set: "infinite S \<Longrightarrow> enumerate S n \<in> S"
apply (induct n arbitrary: S)
apply (fastforce intro: LeastI dest!: infinite_imp_nonempty)
apply simp
@@ -382,13 +282,13 @@
apply (rule order_le_neq_trans)
apply (simp add: enumerate_0 Least_le enumerate_in_set)
apply (simp only: enumerate_Suc')
- apply (subgoal_tac "enumerate (S - {enumerate S 0}) 0 : S - {enumerate S 0}")
+ apply (subgoal_tac "enumerate (S - {enumerate S 0}) 0 \<in> S - {enumerate S 0}")
apply (blast intro: sym)
apply (simp add: enumerate_in_set del: Diff_iff)
apply (simp add: enumerate_Suc')
done
-lemma enumerate_mono: "m<n \<Longrightarrow> infinite S \<Longrightarrow> enumerate S m < enumerate S n"
+lemma enumerate_mono: "m < n \<Longrightarrow> infinite S \<Longrightarrow> enumerate S m < enumerate S n"
apply (erule less_Suc_induct)
apply (auto intro: enumerate_step)
done
--- a/src/HOL/Library/Polynomial.thy Sun Apr 12 20:05:35 2015 +0200
+++ b/src/HOL/Library/Polynomial.thy Mon Apr 13 00:59:17 2015 +0200
@@ -50,9 +50,6 @@
"tl (x ## xs) = xs"
by (simp add: cCons_def)
-lemma MOST_SucD: "(\<forall>\<^sub>\<infinity> n. P (Suc n)) \<Longrightarrow> (\<forall>\<^sub>\<infinity> n. P n)"
- by (auto simp: MOST_nat) (metis Suc_lessE)
-
subsection {* Definition of type @{text poly} *}
typedef 'a poly = "{f :: nat \<Rightarrow> 'a::zero. \<forall>\<^sub>\<infinity> n. f n = 0}"
@@ -501,9 +498,9 @@
lift_definition plus_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
is "\<lambda>p q n. coeff p n + coeff q n"
-proof (rule MOST_rev_mp[OF MOST_coeff_eq_0 MOST_rev_mp[OF MOST_coeff_eq_0]])
- fix q p :: "'a poly" show "\<forall>\<^sub>\<infinity>n. coeff p n = 0 \<longrightarrow> coeff q n = 0 \<longrightarrow> coeff p n + coeff q n = 0"
- by simp
+proof -
+ fix q p :: "'a poly" show "\<forall>\<^sub>\<infinity>n. coeff p n + coeff q n = 0"
+ using MOST_coeff_eq_0[of p] MOST_coeff_eq_0[of q] by eventually_elim simp
qed
lemma coeff_add [simp]:
@@ -527,9 +524,9 @@
lift_definition minus_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
is "\<lambda>p q n. coeff p n - coeff q n"
-proof (rule MOST_rev_mp[OF MOST_coeff_eq_0 MOST_rev_mp[OF MOST_coeff_eq_0]])
- fix q p :: "'a poly" show "\<forall>\<^sub>\<infinity>n. coeff p n = 0 \<longrightarrow> coeff q n = 0 \<longrightarrow> coeff p n - coeff q n = 0"
- by simp
+proof -
+ fix q p :: "'a poly" show "\<forall>\<^sub>\<infinity>n. coeff p n - coeff q n = 0"
+ using MOST_coeff_eq_0[of p] MOST_coeff_eq_0[of q] by eventually_elim simp
qed
lemma coeff_diff [simp]:
@@ -551,9 +548,9 @@
lift_definition uminus_poly :: "'a poly \<Rightarrow> 'a poly"
is "\<lambda>p n. - coeff p n"
-proof (rule MOST_rev_mp[OF MOST_coeff_eq_0])
- fix p :: "'a poly" show "\<forall>\<^sub>\<infinity>n. coeff p n = 0 \<longrightarrow> - coeff p n = 0"
- by simp
+proof -
+ fix p :: "'a poly" show "\<forall>\<^sub>\<infinity>n. - coeff p n = 0"
+ using MOST_coeff_eq_0 by simp
qed
lemma coeff_minus [simp]: "coeff (- p) n = - coeff p n"
@@ -707,11 +704,9 @@
lift_definition smult :: "'a::comm_semiring_0 \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
is "\<lambda>a p n. a * coeff p n"
-proof (intro MOST_nat[THEN iffD2] exI allI impI)
- fix a :: 'a and p :: "'a poly" and i
- assume "degree p < i"
- then show "a * coeff p i = 0"
- by (simp add: coeff_eq_0)
+proof -
+ fix a :: 'a and p :: "'a poly" show "\<forall>\<^sub>\<infinity> i. a * coeff p i = 0"
+ using MOST_coeff_eq_0[of p] by eventually_elim simp
qed
lemma coeff_smult [simp]:
--- a/src/HOL/Main.thy Sun Apr 12 20:05:35 2015 +0200
+++ b/src/HOL/Main.thy Mon Apr 13 00:59:17 2015 +0200
@@ -1,7 +1,7 @@
section {* Main HOL *}
theory Main
-imports Predicate_Compile Quickcheck_Narrowing Extraction Coinduction Nitpick BNF_Greatest_Fixpoint
+imports Predicate_Compile Quickcheck_Narrowing Extraction Coinduction Nitpick BNF_Greatest_Fixpoint Filter
begin
text {*
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Sun Apr 12 20:05:35 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Apr 13 00:59:17 2015 +0200
@@ -3331,10 +3331,8 @@
have "(\<forall>B \<subseteq> Z. finite B \<longrightarrow> U \<inter> \<Inter>B \<noteq> {})"
proof (intro allI impI)
fix B assume "finite B" "B \<subseteq> Z"
- with `finite B` ev_Z have "eventually (\<lambda>x. \<forall>b\<in>B. x \<in> b) F"
- by (auto intro!: eventually_Ball_finite)
- with F(2) have "eventually (\<lambda>x. x \<in> U \<inter> (\<Inter>B)) F"
- by eventually_elim auto
+ with `finite B` ev_Z F(2) have "eventually (\<lambda>x. x \<in> U \<inter> (\<Inter>B)) F"
+ by (auto simp: eventually_ball_finite_distrib eventually_conj_iff)
with F show "U \<inter> \<Inter>B \<noteq> {}"
by (intro notI) (simp add: eventually_False)
qed
@@ -7506,7 +7504,7 @@
then have cont: "continuous_on ?D (\<lambda>x. dist ((g \<circ> fst) x) (snd x))"
unfolding continuous_on_eq_continuous_within
by (intro continuous_dist ballI continuous_within_compose)
- (auto intro!: continuous_fst continuous_snd continuous_within_id simp: image_image)
+ (auto intro!: continuous_fst continuous_snd continuous_within_id simp: image_image)
obtain a where "a \<in> s" and le: "\<And>x. x \<in> s \<Longrightarrow> dist (g a) a \<le> dist (g x) x"
using continuous_attains_inf[OF D cont] by auto
--- a/src/HOL/NSA/Filter.thy Sun Apr 12 20:05:35 2015 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,413 +0,0 @@
-(* Title: HOL/NSA/Filter.thy
- Author: Jacques D. Fleuriot, University of Cambridge
- Author: Lawrence C Paulson
- Author: Brian Huffman
-*)
-
-section {* Filters and Ultrafilters *}
-
-theory Filter
-imports "~~/src/HOL/Library/Infinite_Set"
-begin
-
-subsection {* Definitions and basic properties *}
-
-subsubsection {* Filters *}
-
-locale filter =
- fixes F :: "'a set set"
- assumes UNIV [iff]: "UNIV \<in> F"
- assumes empty [iff]: "{} \<notin> F"
- assumes Int: "\<lbrakk>u \<in> F; v \<in> F\<rbrakk> \<Longrightarrow> u \<inter> v \<in> F"
- assumes subset: "\<lbrakk>u \<in> F; u \<subseteq> v\<rbrakk> \<Longrightarrow> v \<in> F"
-begin
-
-lemma memD: "A \<in> F \<Longrightarrow> - A \<notin> F"
-proof
- assume "A \<in> F" and "- A \<in> F"
- hence "A \<inter> (- A) \<in> F" by (rule Int)
- thus "False" by simp
-qed
-
-lemma not_memI: "- A \<in> F \<Longrightarrow> A \<notin> F"
-by (drule memD, simp)
-
-lemma Int_iff: "(x \<inter> y \<in> F) = (x \<in> F \<and> y \<in> F)"
-by (auto elim: subset intro: Int)
-
-end
-
-subsubsection {* Ultrafilters *}
-
-locale ultrafilter = filter +
- assumes ultra: "A \<in> F \<or> - A \<in> F"
-begin
-
-lemma memI: "- A \<notin> F \<Longrightarrow> A \<in> F"
-using ultra [of A] by simp
-
-lemma not_memD: "A \<notin> F \<Longrightarrow> - A \<in> F"
-by (rule memI, simp)
-
-lemma not_mem_iff: "(A \<notin> F) = (- A \<in> F)"
-by (rule iffI [OF not_memD not_memI])
-
-lemma Compl_iff: "(- A \<in> F) = (A \<notin> F)"
-by (rule iffI [OF not_memI not_memD])
-
-lemma Un_iff: "(x \<union> y \<in> F) = (x \<in> F \<or> y \<in> F)"
- apply (rule iffI)
- apply (erule contrapos_pp)
- apply (simp add: Int_iff not_mem_iff)
- apply (auto elim: subset)
-done
-
-end
-
-subsubsection {* Free Ultrafilters *}
-
-locale freeultrafilter = ultrafilter +
- assumes infinite: "A \<in> F \<Longrightarrow> infinite A"
-begin
-
-lemma finite: "finite A \<Longrightarrow> A \<notin> F"
-by (erule contrapos_pn, erule infinite)
-
-lemma singleton: "{x} \<notin> F"
-by (rule finite, simp)
-
-lemma insert_iff [simp]: "(insert x A \<in> F) = (A \<in> F)"
-apply (subst insert_is_Un)
-apply (subst Un_iff)
-apply (simp add: singleton)
-done
-
-lemma filter: "filter F" ..
-
-lemma ultrafilter: "ultrafilter F" ..
-
-end
-
-subsection {* Collect properties *}
-
-lemma (in filter) Collect_ex:
- "({n. \<exists>x. P n x} \<in> F) = (\<exists>X. {n. P n (X n)} \<in> F)"
-proof
- assume "{n. \<exists>x. P n x} \<in> F"
- hence "{n. P n (SOME x. P n x)} \<in> F"
- by (auto elim: someI subset)
- thus "\<exists>X. {n. P n (X n)} \<in> F" by fast
-next
- show "\<exists>X. {n. P n (X n)} \<in> F \<Longrightarrow> {n. \<exists>x. P n x} \<in> F"
- by (auto elim: subset)
-qed
-
-lemma (in filter) Collect_conj:
- "({n. P n \<and> Q n} \<in> F) = ({n. P n} \<in> F \<and> {n. Q n} \<in> F)"
-by (subst Collect_conj_eq, rule Int_iff)
-
-lemma (in ultrafilter) Collect_not:
- "({n. \<not> P n} \<in> F) = ({n. P n} \<notin> F)"
-by (subst Collect_neg_eq, rule Compl_iff)
-
-lemma (in ultrafilter) Collect_disj:
- "({n. P n \<or> Q n} \<in> F) = ({n. P n} \<in> F \<or> {n. Q n} \<in> F)"
-by (subst Collect_disj_eq, rule Un_iff)
-
-lemma (in ultrafilter) Collect_all:
- "({n. \<forall>x. P n x} \<in> F) = (\<forall>X. {n. P n (X n)} \<in> F)"
-apply (rule Not_eq_iff [THEN iffD1])
-apply (simp add: Collect_not [symmetric])
-apply (rule Collect_ex)
-done
-
-subsection {* Maximal filter = Ultrafilter *}
-
-text {*
- A filter F is an ultrafilter iff it is a maximal filter,
- i.e. whenever G is a filter and @{term "F \<subseteq> G"} then @{term "F = G"}
-*}
-text {*
- Lemmas that shows existence of an extension to what was assumed to
- be a maximal filter. Will be used to derive contradiction in proof of
- property of ultrafilter.
-*}
-
-lemma extend_lemma1: "UNIV \<in> F \<Longrightarrow> A \<in> {X. \<exists>f\<in>F. A \<inter> f \<subseteq> X}"
-by blast
-
-lemma extend_lemma2: "F \<subseteq> {X. \<exists>f\<in>F. A \<inter> f \<subseteq> X}"
-by blast
-
-lemma (in filter) extend_filter:
-assumes A: "- A \<notin> F"
-shows "filter {X. \<exists>f\<in>F. A \<inter> f \<subseteq> X}" (is "filter ?X")
-proof (rule filter.intro)
- show "UNIV \<in> ?X" by blast
-next
- show "{} \<notin> ?X"
- proof (clarify)
- fix f assume f: "f \<in> F" and Af: "A \<inter> f \<subseteq> {}"
- from Af have fA: "f \<subseteq> - A" by blast
- from f fA have "- A \<in> F" by (rule subset)
- with A show "False" by simp
- qed
-next
- fix u and v
- assume u: "u \<in> ?X" and v: "v \<in> ?X"
- from u obtain f where f: "f \<in> F" and Af: "A \<inter> f \<subseteq> u" by blast
- from v obtain g where g: "g \<in> F" and Ag: "A \<inter> g \<subseteq> v" by blast
- from f g have fg: "f \<inter> g \<in> F" by (rule Int)
- from Af Ag have Afg: "A \<inter> (f \<inter> g) \<subseteq> u \<inter> v" by blast
- from fg Afg show "u \<inter> v \<in> ?X" by blast
-next
- fix u and v
- assume uv: "u \<subseteq> v" and u: "u \<in> ?X"
- from u obtain f where f: "f \<in> F" and Afu: "A \<inter> f \<subseteq> u" by blast
- from Afu uv have Afv: "A \<inter> f \<subseteq> v" by blast
- from f Afv have "\<exists>f\<in>F. A \<inter> f \<subseteq> v" by blast
- thus "v \<in> ?X" by simp
-qed
-
-lemma (in filter) max_filter_ultrafilter:
-assumes max: "\<And>G. \<lbrakk>filter G; F \<subseteq> G\<rbrakk> \<Longrightarrow> F = G"
-shows "ultrafilter_axioms F"
-proof (rule ultrafilter_axioms.intro)
- fix A show "A \<in> F \<or> - A \<in> F"
- proof (rule disjCI)
- let ?X = "{X. \<exists>f\<in>F. A \<inter> f \<subseteq> X}"
- assume AF: "- A \<notin> F"
- from AF have X: "filter ?X" by (rule extend_filter)
- from UNIV have AX: "A \<in> ?X" by (rule extend_lemma1)
- have FX: "F \<subseteq> ?X" by (rule extend_lemma2)
- from X FX have "F = ?X" by (rule max)
- with AX show "A \<in> F" by simp
- qed
-qed
-
-lemma (in ultrafilter) max_filter:
-assumes G: "filter G" and sub: "F \<subseteq> G" shows "F = G"
-proof
- show "F \<subseteq> G" using sub .
- show "G \<subseteq> F"
- proof
- fix A assume A: "A \<in> G"
- from G A have "- A \<notin> G" by (rule filter.memD)
- with sub have B: "- A \<notin> F" by blast
- thus "A \<in> F" by (rule memI)
- qed
-qed
-
-subsection {* Ultrafilter Theorem *}
-
-text "A local context makes proof of ultrafilter Theorem more modular"
-context
- fixes frechet :: "'a set set"
- and superfrechet :: "'a set set set"
-
- assumes infinite_UNIV: "infinite (UNIV :: 'a set)"
-
- defines frechet_def: "frechet \<equiv> {A. finite (- A)}"
- and superfrechet_def: "superfrechet \<equiv> {G. filter G \<and> frechet \<subseteq> G}"
-begin
-
-lemma superfrechetI:
- "\<lbrakk>filter G; frechet \<subseteq> G\<rbrakk> \<Longrightarrow> G \<in> superfrechet"
-by (simp add: superfrechet_def)
-
-lemma superfrechetD1:
- "G \<in> superfrechet \<Longrightarrow> filter G"
-by (simp add: superfrechet_def)
-
-lemma superfrechetD2:
- "G \<in> superfrechet \<Longrightarrow> frechet \<subseteq> G"
-by (simp add: superfrechet_def)
-
-text {* A few properties of free filters *}
-
-lemma filter_cofinite:
-assumes inf: "infinite (UNIV :: 'a set)"
-shows "filter {A:: 'a set. finite (- A)}" (is "filter ?F")
-proof (rule filter.intro)
- show "UNIV \<in> ?F" by simp
-next
- show "{} \<notin> ?F" using inf by simp
-next
- fix u v assume "u \<in> ?F" and "v \<in> ?F"
- thus "u \<inter> v \<in> ?F" by simp
-next
- fix u v assume uv: "u \<subseteq> v" and u: "u \<in> ?F"
- from uv have vu: "- v \<subseteq> - u" by simp
- from u show "v \<in> ?F"
- by (simp add: finite_subset [OF vu])
-qed
-
-text {*
- We prove: 1. Existence of maximal filter i.e. ultrafilter;
- 2. Freeness property i.e ultrafilter is free.
- Use a locale to prove various lemmas and then
- export main result: The ultrafilter Theorem
-*}
-
-lemma filter_frechet: "filter frechet"
-by (unfold frechet_def, rule filter_cofinite [OF infinite_UNIV])
-
-lemma frechet_in_superfrechet: "frechet \<in> superfrechet"
-by (rule superfrechetI [OF filter_frechet subset_refl])
-
-lemma lemma_mem_chain_filter:
- "\<lbrakk>c \<in> chains superfrechet; x \<in> c\<rbrakk> \<Longrightarrow> filter x"
-by (unfold chains_def superfrechet_def, blast)
-
-
-subsubsection {* Unions of chains of superfrechets *}
-
-text "In this section we prove that superfrechet is closed
-with respect to unions of non-empty chains. We must show
- 1) Union of a chain is a filter,
- 2) Union of a chain contains frechet.
-
-Number 2 is trivial, but 1 requires us to prove all the filter rules."
-
-lemma Union_chain_UNIV:
- "\<lbrakk>c \<in> chains superfrechet; c \<noteq> {}\<rbrakk> \<Longrightarrow> UNIV \<in> \<Union>c"
-proof -
- assume 1: "c \<in> chains superfrechet" and 2: "c \<noteq> {}"
- from 2 obtain x where 3: "x \<in> c" by blast
- from 1 3 have "filter x" by (rule lemma_mem_chain_filter)
- hence "UNIV \<in> x" by (rule filter.UNIV)
- with 3 show "UNIV \<in> \<Union>c" by blast
-qed
-
-lemma Union_chain_empty:
- "c \<in> chains superfrechet \<Longrightarrow> {} \<notin> \<Union>c"
-proof
- assume 1: "c \<in> chains superfrechet" and 2: "{} \<in> \<Union>c"
- from 2 obtain x where 3: "x \<in> c" and 4: "{} \<in> x" ..
- from 1 3 have "filter x" by (rule lemma_mem_chain_filter)
- hence "{} \<notin> x" by (rule filter.empty)
- with 4 show "False" by simp
-qed
-
-lemma Union_chain_Int:
- "\<lbrakk>c \<in> chains superfrechet; u \<in> \<Union>c; v \<in> \<Union>c\<rbrakk> \<Longrightarrow> u \<inter> v \<in> \<Union>c"
-proof -
- assume c: "c \<in> chains superfrechet"
- assume "u \<in> \<Union>c"
- then obtain x where ux: "u \<in> x" and xc: "x \<in> c" ..
- assume "v \<in> \<Union>c"
- then obtain y where vy: "v \<in> y" and yc: "y \<in> c" ..
- from c xc yc have "x \<subseteq> y \<or> y \<subseteq> x" using c unfolding chains_def chain_subset_def by auto
- with xc yc have xyc: "x \<union> y \<in> c"
- by (auto simp add: Un_absorb1 Un_absorb2)
- with c have fxy: "filter (x \<union> y)" by (rule lemma_mem_chain_filter)
- from ux have uxy: "u \<in> x \<union> y" by simp
- from vy have vxy: "v \<in> x \<union> y" by simp
- from fxy uxy vxy have "u \<inter> v \<in> x \<union> y" by (rule filter.Int)
- with xyc show "u \<inter> v \<in> \<Union>c" ..
-qed
-
-lemma Union_chain_subset:
- "\<lbrakk>c \<in> chains superfrechet; u \<in> \<Union>c; u \<subseteq> v\<rbrakk> \<Longrightarrow> v \<in> \<Union>c"
-proof -
- assume c: "c \<in> chains superfrechet"
- and u: "u \<in> \<Union>c" and uv: "u \<subseteq> v"
- from u obtain x where ux: "u \<in> x" and xc: "x \<in> c" ..
- from c xc have fx: "filter x" by (rule lemma_mem_chain_filter)
- from fx ux uv have vx: "v \<in> x" by (rule filter.subset)
- with xc show "v \<in> \<Union>c" ..
-qed
-
-lemma Union_chain_filter:
-assumes chain: "c \<in> chains superfrechet" and nonempty: "c \<noteq> {}"
-shows "filter (\<Union>c)"
-proof (rule filter.intro)
- show "UNIV \<in> \<Union>c" using chain nonempty by (rule Union_chain_UNIV)
-next
- show "{} \<notin> \<Union>c" using chain by (rule Union_chain_empty)
-next
- fix u v assume "u \<in> \<Union>c" and "v \<in> \<Union>c"
- with chain show "u \<inter> v \<in> \<Union>c" by (rule Union_chain_Int)
-next
- fix u v assume "u \<in> \<Union>c" and "u \<subseteq> v"
- with chain show "v \<in> \<Union>c" by (rule Union_chain_subset)
-qed
-
-lemma lemma_mem_chain_frechet_subset:
- "\<lbrakk>c \<in> chains superfrechet; x \<in> c\<rbrakk> \<Longrightarrow> frechet \<subseteq> x"
-by (unfold superfrechet_def chains_def, blast)
-
-lemma Union_chain_superfrechet:
- "\<lbrakk>c \<noteq> {}; c \<in> chains superfrechet\<rbrakk> \<Longrightarrow> \<Union>c \<in> superfrechet"
-proof (rule superfrechetI)
- assume 1: "c \<in> chains superfrechet" and 2: "c \<noteq> {}"
- thus "filter (\<Union>c)" by (rule Union_chain_filter)
- from 2 obtain x where 3: "x \<in> c" by blast
- from 1 3 have "frechet \<subseteq> x" by (rule lemma_mem_chain_frechet_subset)
- also from 3 have "x \<subseteq> \<Union>c" by blast
- finally show "frechet \<subseteq> \<Union>c" .
-qed
-
-subsubsection {* Existence of free ultrafilter *}
-
-lemma max_cofinite_filter_Ex:
- "\<exists>U\<in>superfrechet. \<forall>G\<in>superfrechet. U \<subseteq> G \<longrightarrow> G = U"
-proof (rule Zorn_Lemma2, safe)
- fix c assume c: "c \<in> chains superfrechet"
- show "\<exists>U\<in>superfrechet. \<forall>G\<in>c. G \<subseteq> U" (is "?U")
- proof (cases)
- assume "c = {}"
- with frechet_in_superfrechet show "?U" by blast
- next
- assume A: "c \<noteq> {}"
- from A c have "\<Union>c \<in> superfrechet"
- by (rule Union_chain_superfrechet)
- thus "?U" by blast
- qed
-qed
-
-lemma mem_superfrechet_all_infinite:
- "\<lbrakk>U \<in> superfrechet; A \<in> U\<rbrakk> \<Longrightarrow> infinite A"
-proof
- assume U: "U \<in> superfrechet" and A: "A \<in> U" and fin: "finite A"
- from U have fil: "filter U" and fre: "frechet \<subseteq> U"
- by (simp_all add: superfrechet_def)
- from fin have "- A \<in> frechet" by (simp add: frechet_def)
- with fre have cA: "- A \<in> U" by (rule subsetD)
- from fil A cA have "A \<inter> - A \<in> U" by (rule filter.Int)
- with fil show "False" by (simp add: filter.empty)
-qed
-
-text {* There exists a free ultrafilter on any infinite set *}
-
-lemma freeultrafilter_Ex:
- "\<exists>U::'a set set. freeultrafilter U"
-proof -
- from max_cofinite_filter_Ex obtain U
- where U: "U \<in> superfrechet"
- and max [rule_format]: "\<forall>G\<in>superfrechet. U \<subseteq> G \<longrightarrow> G = U" ..
- from U have fil: "filter U" by (rule superfrechetD1)
- from U have fre: "frechet \<subseteq> U" by (rule superfrechetD2)
- have ultra: "ultrafilter_axioms U"
- proof (rule filter.max_filter_ultrafilter [OF fil])
- fix G assume G: "filter G" and UG: "U \<subseteq> G"
- from fre UG have "frechet \<subseteq> G" by simp
- with G have "G \<in> superfrechet" by (rule superfrechetI)
- from this UG show "U = G" by (rule max[symmetric])
- qed
- have free: "freeultrafilter_axioms U"
- proof (rule freeultrafilter_axioms.intro)
- fix A assume "A \<in> U"
- with U show "infinite A" by (rule mem_superfrechet_all_infinite)
- qed
- from fil ultra free have "freeultrafilter U"
- by (rule freeultrafilter.intro [OF ultrafilter.intro])
- (* FIXME: unfold_locales should use chained facts *)
- then show ?thesis ..
-qed
-
-end
-
-hide_const (open) filter
-
-end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NSA/Free_Ultrafilter.thy Mon Apr 13 00:59:17 2015 +0200
@@ -0,0 +1,200 @@
+(* Title: HOL/NSA/Free_Ultrafilter.thy
+ Author: Jacques D. Fleuriot, University of Cambridge
+ Author: Lawrence C Paulson
+ Author: Brian Huffman
+*)
+
+section {* Filters and Ultrafilters *}
+
+theory Free_Ultrafilter
+imports "~~/src/HOL/Library/Infinite_Set"
+begin
+
+subsection {* Definitions and basic properties *}
+
+subsubsection {* Ultrafilters *}
+
+locale ultrafilter =
+ fixes F :: "'a filter"
+ assumes proper: "F \<noteq> bot"
+ assumes ultra: "eventually P F \<or> eventually (\<lambda>x. \<not> P x) F"
+begin
+
+lemma eventually_imp_frequently: "frequently P F \<Longrightarrow> eventually P F"
+ using ultra[of P] by (simp add: frequently_def)
+
+lemma frequently_eq_eventually: "frequently P F = eventually P F"
+ using eventually_imp_frequently eventually_frequently[OF proper] ..
+
+lemma eventually_disj_iff: "eventually (\<lambda>x. P x \<or> Q x) F \<longleftrightarrow> eventually P F \<or> eventually Q F"
+ unfolding frequently_eq_eventually[symmetric] frequently_disj_iff ..
+
+lemma eventually_all_iff: "eventually (\<lambda>x. \<forall>y. P x y) F = (\<forall>Y. eventually (\<lambda>x. P x (Y x)) F)"
+ using frequently_all[of P F] by (simp add: frequently_eq_eventually)
+
+lemma eventually_imp_iff: "eventually (\<lambda>x. P x \<longrightarrow> Q x) F \<longleftrightarrow> (eventually P F \<longrightarrow> eventually Q F)"
+ using frequently_imp_iff[of P Q F] by (simp add: frequently_eq_eventually)
+
+lemma eventually_iff_iff: "eventually (\<lambda>x. P x \<longleftrightarrow> Q x) F \<longleftrightarrow> (eventually P F \<longleftrightarrow> eventually Q F)"
+ unfolding iff_conv_conj_imp eventually_conj_iff eventually_imp_iff by simp
+
+lemma eventually_not_iff: "eventually (\<lambda>x. \<not> P x) F \<longleftrightarrow> \<not> eventually P F"
+ unfolding not_eventually frequently_eq_eventually ..
+
+end
+
+subsection {* Maximal filter = Ultrafilter *}
+
+text {*
+ A filter F is an ultrafilter iff it is a maximal filter,
+ i.e. whenever G is a filter and @{term "F \<subseteq> G"} then @{term "F = G"}
+*}
+text {*
+ Lemmas that shows existence of an extension to what was assumed to
+ be a maximal filter. Will be used to derive contradiction in proof of
+ property of ultrafilter.
+*}
+
+lemma extend_filter:
+ "frequently P F \<Longrightarrow> inf F (principal {x. P x}) \<noteq> bot"
+ unfolding trivial_limit_def eventually_inf_principal by (simp add: not_eventually)
+
+lemma max_filter_ultrafilter:
+ assumes proper: "F \<noteq> bot"
+ assumes max: "\<And>G. G \<noteq> bot \<Longrightarrow> G \<le> F \<Longrightarrow> F = G"
+ shows "ultrafilter F"
+proof
+ fix P show "eventually P F \<or> (\<forall>\<^sub>Fx in F. \<not> P x)"
+ proof (rule disjCI)
+ assume "\<not> (\<forall>\<^sub>Fx in F. \<not> P x)"
+ then have "inf F (principal {x. P x}) \<noteq> bot"
+ by (simp add: not_eventually extend_filter)
+ then have F: "F = inf F (principal {x. P x})"
+ by (rule max) simp
+ show "eventually P F"
+ by (subst F) (simp add: eventually_inf_principal)
+ qed
+qed fact
+
+lemma le_filter_frequently: "F \<le> G \<longleftrightarrow> (\<forall>P. frequently P F \<longrightarrow> frequently P G)"
+ unfolding frequently_def le_filter_def
+ apply auto
+ apply (erule_tac x="\<lambda>x. \<not> P x" in allE)
+ apply auto
+ done
+
+lemma (in ultrafilter) max_filter:
+ assumes G: "G \<noteq> bot" and sub: "G \<le> F" shows "F = G"
+proof (rule antisym)
+ show "F \<le> G"
+ using sub
+ by (auto simp: le_filter_frequently[of F] frequently_eq_eventually le_filter_def[of G]
+ intro!: eventually_frequently G proper)
+qed fact
+
+subsection {* Ultrafilter Theorem *}
+
+text "A local context makes proof of ultrafilter Theorem more modular"
+
+lemma ex_max_ultrafilter:
+ fixes F :: "'a filter"
+ assumes F: "F \<noteq> bot"
+ shows "\<exists>U\<le>F. ultrafilter U"
+proof -
+ let ?X = "{G. G \<noteq> bot \<and> G \<le> F}"
+ let ?R = "{(b, a). a \<noteq> bot \<and> a \<le> b \<and> b \<le> F}"
+
+ have bot_notin_R: "\<And>c. c \<in> Chains ?R \<Longrightarrow> bot \<notin> c"
+ by (auto simp: Chains_def)
+
+ have [simp]: "Field ?R = ?X"
+ by (auto simp: Field_def bot_unique)
+
+ have "\<exists>m\<in>Field ?R. \<forall>a\<in>Field ?R. (m, a) \<in> ?R \<longrightarrow> a = m"
+ proof (rule Zorns_po_lemma)
+ show "Partial_order ?R"
+ unfolding partial_order_on_def preorder_on_def
+ by (auto simp: antisym_def refl_on_def trans_def Field_def bot_unique)
+ show "\<forall>C\<in>Chains ?R. \<exists>u\<in>Field ?R. \<forall>a\<in>C. (a, u) \<in> ?R"
+ proof (safe intro!: bexI del: notI)
+ fix c x assume c: "c \<in> Chains ?R"
+
+ { assume "c \<noteq> {}"
+ with c have "Inf c = bot \<longleftrightarrow> (\<exists>x\<in>c. x = bot)"
+ unfolding trivial_limit_def by (intro eventually_Inf_base) (auto simp: Chains_def)
+ with c have 1: "Inf c \<noteq> bot"
+ by (simp add: bot_notin_R)
+ from `c \<noteq> {}` obtain x where "x \<in> c" by auto
+ with c have 2: "Inf c \<le> F"
+ by (auto intro!: Inf_lower2[of x] simp: Chains_def)
+ note 1 2 }
+ note Inf_c = this
+ then have [simp]: "inf F (Inf c) = (if c = {} then F else Inf c)"
+ using c by (auto simp add: inf_absorb2)
+
+ show "inf F (Inf c) \<noteq> bot"
+ using c by (simp add: F Inf_c)
+
+ show "inf F (Inf c) \<in> Field ?R"
+ using c by (simp add: Chains_def Inf_c F)
+
+ assume x: "x \<in> c"
+ with c show "inf F (Inf c) \<le> x" "x \<le> F"
+ by (auto intro: Inf_lower simp: Chains_def)
+ qed
+ qed
+ then guess U ..
+ then show ?thesis
+ by (intro exI[of _ U] conjI max_filter_ultrafilter) auto
+qed
+
+subsubsection {* Free Ultrafilters *}
+
+text {* There exists a free ultrafilter on any infinite set *}
+
+locale freeultrafilter = ultrafilter +
+ assumes infinite: "eventually P F \<Longrightarrow> infinite {x. P x}"
+begin
+
+lemma finite: "finite {x. P x} \<Longrightarrow> \<not> eventually P F"
+ by (erule contrapos_pn, erule infinite)
+
+lemma finite': "finite {x. \<not> P x} \<Longrightarrow> eventually P F"
+ by (drule finite) (simp add: not_eventually frequently_eq_eventually)
+
+lemma le_cofinite: "F \<le> cofinite"
+ by (intro filter_leI)
+ (auto simp add: eventually_cofinite not_eventually frequently_eq_eventually dest!: finite)
+
+lemma singleton: "\<not> eventually (\<lambda>x. x = a) F"
+by (rule finite, simp)
+
+lemma singleton': "\<not> eventually (op = a) F"
+by (rule finite, simp)
+
+lemma ultrafilter: "ultrafilter F" ..
+
+end
+
+lemma freeultrafilter_Ex:
+ assumes [simp]: "infinite (UNIV :: 'a set)"
+ shows "\<exists>U::'a filter. freeultrafilter U"
+proof -
+ from ex_max_ultrafilter[of "cofinite :: 'a filter"]
+ obtain U :: "'a filter" where "U \<le> cofinite" "ultrafilter U"
+ by auto
+ interpret ultrafilter U by fact
+ have "freeultrafilter U"
+ proof
+ fix P assume "eventually P U"
+ with proper have "frequently P U"
+ by (rule eventually_frequently)
+ then have "frequently P cofinite"
+ using `U \<le> cofinite` by (simp add: le_filter_frequently)
+ then show "infinite {x. P x}"
+ by (simp add: frequently_cofinite)
+ qed
+ then show ?thesis ..
+qed
+
+end
--- a/src/HOL/NSA/HyperDef.thy Sun Apr 12 20:05:35 2015 +0200
+++ b/src/HOL/NSA/HyperDef.thy Mon Apr 13 00:59:17 2015 +0200
@@ -178,7 +178,7 @@
by (cases x, simp add: star_n_def)
lemma Rep_star_star_n_iff [simp]:
- "(X \<in> Rep_star (star_n Y)) = ({n. Y n = X n} \<in> \<U>)"
+ "(X \<in> Rep_star (star_n Y)) = (eventually (\<lambda>n. Y n = X n) \<U>)"
by (simp add: star_n_def)
lemma Rep_star_star_n: "X \<in> Rep_star (star_n X)"
@@ -207,12 +207,11 @@
by (simp only: star_inverse_def starfun_star_n)
lemma star_n_le:
- "star_n X \<le> star_n Y =
- ({n. X n \<le> Y n} \<in> FreeUltrafilterNat)"
+ "star_n X \<le> star_n Y = (eventually (\<lambda>n. X n \<le> Y n) FreeUltrafilterNat)"
by (simp only: star_le_def starP2_star_n)
lemma star_n_less:
- "star_n X < star_n Y = ({n. X n < Y n} \<in> FreeUltrafilterNat)"
+ "star_n X < star_n Y = (eventually (\<lambda>n. X n < Y n) FreeUltrafilterNat)"
by (simp only: star_less_def starP2_star_n)
lemma star_n_zero_num: "0 = star_n (%n. 0)"
@@ -273,7 +272,7 @@
by (insert not_ex_hypreal_of_real_eq_epsilon, auto)
lemma hypreal_epsilon_not_zero: "epsilon \<noteq> 0"
-by (simp add: epsilon_def star_zero_def star_of_def star_n_eq_iff
+by (simp add: epsilon_def star_zero_def star_of_def star_n_eq_iff FreeUltrafilterNat.proper
del: star_of_zero)
lemma hypreal_epsilon_inverse_omega: "epsilon = inverse(omega)"
--- a/src/HOL/NSA/HyperNat.thy Sun Apr 12 20:05:35 2015 +0200
+++ b/src/HOL/NSA/HyperNat.thy Mon Apr 13 00:59:17 2015 +0200
@@ -274,10 +274,10 @@
hypnat_omega_def: "whn = star_n (%n::nat. n)"
lemma hypnat_of_nat_neq_whn: "hypnat_of_nat n \<noteq> whn"
-by (simp add: hypnat_omega_def star_of_def star_n_eq_iff)
+by (simp add: FreeUltrafilterNat.singleton' hypnat_omega_def star_of_def star_n_eq_iff)
lemma whn_neq_hypnat_of_nat: "whn \<noteq> hypnat_of_nat n"
-by (simp add: hypnat_omega_def star_of_def star_n_eq_iff)
+by (simp add: FreeUltrafilterNat.singleton hypnat_omega_def star_of_def star_n_eq_iff)
lemma whn_not_Nats [simp]: "whn \<notin> Nats"
by (simp add: Nats_def image_def whn_neq_hypnat_of_nat)
@@ -285,15 +285,9 @@
lemma HNatInfinite_whn [simp]: "whn \<in> HNatInfinite"
by (simp add: HNatInfinite_def)
-lemma lemma_unbounded_set [simp]: "{n::nat. m < n} \<in> FreeUltrafilterNat"
-apply (insert finite_atMost [of m])
-apply (drule FreeUltrafilterNat.finite)
-apply (drule FreeUltrafilterNat.not_memD)
-apply (simp add: Collect_neg_eq [symmetric] linorder_not_le atMost_def)
-done
-
-lemma Compl_Collect_le: "- {n::nat. N \<le> n} = {n. n < N}"
-by (simp add: Collect_neg_eq [symmetric] linorder_not_le)
+lemma lemma_unbounded_set [simp]: "eventually (\<lambda>n::nat. m < n) \<U>"
+ by (rule filter_leD[OF FreeUltrafilterNat.le_cofinite])
+ (auto simp add: cofinite_eq_sequentially eventually_at_top_dense)
lemma hypnat_of_nat_eq:
"hypnat_of_nat m = star_n (%n::nat. m)"
@@ -327,14 +321,14 @@
(*??delete? similar reasoning in hypnat_omega_gt_SHNat above*)
lemma HNatInfinite_FreeUltrafilterNat_lemma:
- assumes "\<forall>N::nat. {n. f n \<noteq> N} \<in> FreeUltrafilterNat"
- shows "{n. N < f n} \<in> FreeUltrafilterNat"
+ assumes "\<forall>N::nat. eventually (\<lambda>n. f n \<noteq> N) \<U>"
+ shows "eventually (\<lambda>n. N < f n) \<U>"
apply (induct N)
using assms
apply (drule_tac x = 0 in spec, simp)
using assms
apply (drule_tac x = "Suc N" in spec)
-apply (elim ultra, auto)
+apply (auto elim: eventually_elim2)
done
lemma HNatInfinite_iff: "HNatInfinite = {N. \<forall>n \<in> Nats. n < N}"
@@ -347,18 +341,18 @@
Free Ultrafilter*}
lemma HNatInfinite_FreeUltrafilterNat:
- "star_n X \<in> HNatInfinite ==> \<forall>u. {n. u < X n}: FreeUltrafilterNat"
+ "star_n X \<in> HNatInfinite ==> \<forall>u. eventually (\<lambda>n. u < X n) FreeUltrafilterNat"
apply (auto simp add: HNatInfinite_iff SHNat_eq)
apply (drule_tac x="star_of u" in spec, simp)
apply (simp add: star_of_def star_less_def starP2_star_n)
done
lemma FreeUltrafilterNat_HNatInfinite:
- "\<forall>u. {n. u < X n}: FreeUltrafilterNat ==> star_n X \<in> HNatInfinite"
+ "\<forall>u. eventually (\<lambda>n. u < X n) FreeUltrafilterNat ==> star_n X \<in> HNatInfinite"
by (auto simp add: star_less_def starP2_star_n HNatInfinite_iff SHNat_eq hypnat_of_nat_eq)
lemma HNatInfinite_FreeUltrafilterNat_iff:
- "(star_n X \<in> HNatInfinite) = (\<forall>u. {n. u < X n}: FreeUltrafilterNat)"
+ "(star_n X \<in> HNatInfinite) = (\<forall>u. eventually (\<lambda>n. u < X n) FreeUltrafilterNat)"
by (rule iffI [OF HNatInfinite_FreeUltrafilterNat
FreeUltrafilterNat_HNatInfinite])
--- a/src/HOL/NSA/NSA.thy Sun Apr 12 20:05:35 2015 +0200
+++ b/src/HOL/NSA/NSA.thy Mon Apr 13 00:59:17 2015 +0200
@@ -1915,7 +1915,7 @@
lemma HFinite_FreeUltrafilterNat:
"star_n X \<in> HFinite
- ==> \<exists>u. {n. norm (X n) < u} \<in> FreeUltrafilterNat"
+ ==> \<exists>u. eventually (\<lambda>n. norm (X n) < u) FreeUltrafilterNat"
apply (auto simp add: HFinite_def SReal_def)
apply (rule_tac x=r in exI)
apply (simp add: hnorm_def star_of_def starfun_star_n)
@@ -1923,7 +1923,7 @@
done
lemma FreeUltrafilterNat_HFinite:
- "\<exists>u. {n. norm (X n) < u} \<in> FreeUltrafilterNat
+ "\<exists>u. eventually (\<lambda>n. norm (X n) < u) FreeUltrafilterNat
==> star_n X \<in> HFinite"
apply (auto simp add: HFinite_def mem_Rep_star_iff)
apply (rule_tac x="star_of u" in bexI)
@@ -1933,7 +1933,7 @@
done
lemma HFinite_FreeUltrafilterNat_iff:
- "(star_n X \<in> HFinite) = (\<exists>u. {n. norm (X n) < u} \<in> FreeUltrafilterNat)"
+ "(star_n X \<in> HFinite) = (\<exists>u. eventually (\<lambda>n. norm (X n) < u) FreeUltrafilterNat)"
by (blast intro!: HFinite_FreeUltrafilterNat FreeUltrafilterNat_HFinite)
subsubsection {* @{term HInfinite} *}
@@ -1957,20 +1957,19 @@
ultrafilter for Infinite numbers!
-------------------------------------*)
lemma FreeUltrafilterNat_const_Finite:
- "{n. norm (X n) = u} \<in> FreeUltrafilterNat ==> star_n X \<in> HFinite"
+ "eventually (\<lambda>n. norm (X n) = u) FreeUltrafilterNat ==> star_n X \<in> HFinite"
apply (rule FreeUltrafilterNat_HFinite)
apply (rule_tac x = "u + 1" in exI)
-apply (erule ultra, simp)
+apply (auto elim: eventually_elim1)
done
lemma HInfinite_FreeUltrafilterNat:
- "star_n X \<in> HInfinite ==> \<forall>u. {n. u < norm (X n)} \<in> FreeUltrafilterNat"
+ "star_n X \<in> HInfinite ==> \<forall>u. eventually (\<lambda>n. u < norm (X n)) FreeUltrafilterNat"
apply (drule HInfinite_HFinite_iff [THEN iffD1])
apply (simp add: HFinite_FreeUltrafilterNat_iff)
apply (rule allI, drule_tac x="u + 1" in spec)
-apply (drule FreeUltrafilterNat.not_memD)
-apply (simp add: Collect_neg_eq [symmetric] linorder_not_less)
-apply (erule ultra, simp)
+apply (simp add: FreeUltrafilterNat.eventually_not_iff[symmetric])
+apply (auto elim: eventually_elim1)
done
lemma lemma_Int_HI:
@@ -1981,17 +1980,20 @@
by (auto intro: order_less_asym)
lemma FreeUltrafilterNat_HInfinite:
- "\<forall>u. {n. u < norm (X n)} \<in> FreeUltrafilterNat ==> star_n X \<in> HInfinite"
+ "\<forall>u. eventually (\<lambda>n. u < norm (X n)) FreeUltrafilterNat ==> star_n X \<in> HInfinite"
apply (rule HInfinite_HFinite_iff [THEN iffD2])
apply (safe, drule HFinite_FreeUltrafilterNat, safe)
apply (drule_tac x = u in spec)
-apply (drule (1) FreeUltrafilterNat.Int)
-apply (simp add: Collect_conj_eq [symmetric])
-apply (subgoal_tac "\<forall>n. \<not> (norm (X n) < u \<and> u < norm (X n))", auto)
-done
+proof -
+ fix u assume "\<forall>\<^sub>Fn in \<U>. norm (X n) < u" "\<forall>\<^sub>Fn in \<U>. u < norm (X n)"
+ then have "\<forall>\<^sub>F x in \<U>. False"
+ by eventually_elim auto
+ then show False
+ by (simp add: eventually_False FreeUltrafilterNat.proper)
+qed
lemma HInfinite_FreeUltrafilterNat_iff:
- "(star_n X \<in> HInfinite) = (\<forall>u. {n. u < norm (X n)} \<in> FreeUltrafilterNat)"
+ "(star_n X \<in> HInfinite) = (\<forall>u. eventually (\<lambda>n. u < norm (X n)) FreeUltrafilterNat)"
by (blast intro!: HInfinite_FreeUltrafilterNat FreeUltrafilterNat_HInfinite)
subsubsection {* @{term Infinitesimal} *}
@@ -2000,21 +2002,21 @@
by (unfold SReal_def, auto)
lemma Infinitesimal_FreeUltrafilterNat:
- "star_n X \<in> Infinitesimal ==> \<forall>u>0. {n. norm (X n) < u} \<in> \<U>"
+ "star_n X \<in> Infinitesimal ==> \<forall>u>0. eventually (\<lambda>n. norm (X n) < u) \<U>"
apply (simp add: Infinitesimal_def ball_SReal_eq)
apply (simp add: hnorm_def starfun_star_n star_of_def)
apply (simp add: star_less_def starP2_star_n)
done
lemma FreeUltrafilterNat_Infinitesimal:
- "\<forall>u>0. {n. norm (X n) < u} \<in> \<U> ==> star_n X \<in> Infinitesimal"
+ "\<forall>u>0. eventually (\<lambda>n. norm (X n) < u) \<U> ==> star_n X \<in> Infinitesimal"
apply (simp add: Infinitesimal_def ball_SReal_eq)
apply (simp add: hnorm_def starfun_star_n star_of_def)
apply (simp add: star_less_def starP2_star_n)
done
lemma Infinitesimal_FreeUltrafilterNat_iff:
- "(star_n X \<in> Infinitesimal) = (\<forall>u>0. {n. norm (X n) < u} \<in> \<U>)"
+ "(star_n X \<in> Infinitesimal) = (\<forall>u>0. eventually (\<lambda>n. norm (X n) < u) \<U>)"
by (blast intro!: Infinitesimal_FreeUltrafilterNat FreeUltrafilterNat_Infinitesimal)
(*------------------------------------------------------------------------
@@ -2087,14 +2089,13 @@
done
lemma rabs_real_of_nat_le_real_FreeUltrafilterNat:
- "{n. abs(real n) \<le> u} \<notin> FreeUltrafilterNat"
+ "\<not> eventually (\<lambda>n. abs(real n) \<le> u) FreeUltrafilterNat"
by (blast intro!: FreeUltrafilterNat.finite finite_rabs_real_of_nat_le_real)
-lemma FreeUltrafilterNat_nat_gt_real: "{n. u < real n} \<in> FreeUltrafilterNat"
-apply (rule ccontr, drule FreeUltrafilterNat.not_memD)
-apply (subgoal_tac "- {n::nat. u < real n} = {n. real n \<le> u}")
-prefer 2 apply force
-apply (simp add: finite_real_of_nat_le_real [THEN FreeUltrafilterNat.finite])
+lemma FreeUltrafilterNat_nat_gt_real: "eventually (\<lambda>n. u < real n) FreeUltrafilterNat"
+apply (rule FreeUltrafilterNat.finite')
+apply (subgoal_tac "{n::nat. \<not> u < real n} = {n. real n \<le> u}")
+apply (auto simp add: finite_real_of_nat_le_real)
done
(*--------------------------------------------------------------
@@ -2108,10 +2109,8 @@
text{*@{term omega} is a member of @{term HInfinite}*}
-lemma FreeUltrafilterNat_omega: "{n. u < real n} \<in> FreeUltrafilterNat"
-apply (cut_tac u = u in rabs_real_of_nat_le_real_FreeUltrafilterNat)
-apply (auto dest: FreeUltrafilterNat.not_memD simp add: Compl_real_le_eq)
-done
+lemma FreeUltrafilterNat_omega: "eventually (\<lambda>n. u < real n) FreeUltrafilterNat"
+ by (fact FreeUltrafilterNat_nat_gt_real)
theorem HInfinite_omega [simp]: "omega \<in> HInfinite"
apply (simp add: omega_def)
@@ -2165,7 +2164,7 @@
by (auto simp add: lemma_real_le_Un_eq2 lemma_finite_epsilon_set finite_inverse_real_of_posnat_gt_real)
lemma inverse_real_of_posnat_ge_real_FreeUltrafilterNat:
- "0 < u ==> {n. u \<le> inverse(real(Suc n))} \<notin> FreeUltrafilterNat"
+ "0 < u ==> \<not> eventually (\<lambda>n. u \<le> inverse(real(Suc n))) FreeUltrafilterNat"
by (blast intro!: FreeUltrafilterNat.finite finite_inverse_real_of_posnat_ge_real)
(*--------------------------------------------------------------
@@ -2179,9 +2178,9 @@
lemma FreeUltrafilterNat_inverse_real_of_posnat:
- "0 < u ==>
- {n. inverse(real(Suc n)) < u} \<in> FreeUltrafilterNat"
-by (metis Compl_le_inverse_eq FreeUltrafilterNat.ultra inverse_real_of_posnat_ge_real_FreeUltrafilterNat)
+ "0 < u ==> eventually (\<lambda>n. inverse(real(Suc n)) < u) FreeUltrafilterNat"
+by (drule inverse_real_of_posnat_ge_real_FreeUltrafilterNat)
+ (simp add: FreeUltrafilterNat.eventually_not_iff not_le[symmetric])
text{* Example of an hypersequence (i.e. an extended standard sequence)
whose term with an hypernatural suffix is an infinitesimal i.e.
@@ -2208,8 +2207,8 @@
"\<forall>n. norm(X n - x) < inverse(real(Suc n))
==> star_n X - star_of x \<in> Infinitesimal"
unfolding star_n_diff star_of_def Infinitesimal_FreeUltrafilterNat_iff star_n_inverse
-by (auto dest: FreeUltrafilterNat_inverse_real_of_posnat FreeUltrafilterNat.Int
- intro: order_less_trans FreeUltrafilterNat.subset)
+by (auto dest!: FreeUltrafilterNat_inverse_real_of_posnat
+ intro: order_less_trans elim!: eventually_elim1)
lemma real_seq_to_hypreal_approx:
"\<forall>n. norm(X n - x) < inverse(real(Suc n))
@@ -2225,7 +2224,7 @@
"\<forall>n. norm(X n - Y n) < inverse(real(Suc n))
==> star_n X - star_n Y \<in> Infinitesimal"
unfolding Infinitesimal_FreeUltrafilterNat_iff star_n_diff
-by (auto dest: FreeUltrafilterNat_inverse_real_of_posnat
- intro: order_less_trans FreeUltrafilterNat.subset)
+by (auto dest!: FreeUltrafilterNat_inverse_real_of_posnat
+ intro: order_less_trans elim!: eventually_elim1)
end
--- a/src/HOL/NSA/Star.thy Sun Apr 12 20:05:35 2015 +0200
+++ b/src/HOL/NSA/Star.thy Mon Apr 13 00:59:17 2015 +0200
@@ -22,8 +22,8 @@
definition
(* nonstandard extension of function *)
is_starext :: "['a star => 'a star, 'a => 'a] => bool" where
- "is_starext F f = (\<forall>x y. \<exists>X \<in> Rep_star(x). \<exists>Y \<in> Rep_star(y).
- ((y = (F x)) = ({n. Y n = f(X n)} : FreeUltrafilterNat)))"
+ "is_starext F f =
+ (\<forall>x y. \<exists>X \<in> Rep_star(x). \<exists>Y \<in> Rep_star(y). ((y = (F x)) = (eventually (\<lambda>n. Y n = f(X n)) \<U>)))"
definition
(* internal functions *)
@@ -71,7 +71,7 @@
lemma STAR_real_seq_to_hypreal:
"\<forall>n. (X n) \<notin> M ==> star_n X \<notin> *s* M"
apply (unfold starset_def star_of_def)
-apply (simp add: Iset_star_n)
+apply (simp add: Iset_star_n FreeUltrafilterNat.proper)
done
lemma STAR_singleton: "*s* {x} = {star_of x}"
@@ -304,9 +304,7 @@
In this theory since @{text hypreal_hrabs} proved here. Maybe
move both theorems??*}
lemma Infinitesimal_FreeUltrafilterNat_iff2:
- "(star_n X \<in> Infinitesimal) =
- (\<forall>m. {n. norm(X n) < inverse(real(Suc m))}
- \<in> FreeUltrafilterNat)"
+ "(star_n X \<in> Infinitesimal) = (\<forall>m. eventually (\<lambda>n. norm(X n) < inverse(real(Suc m))) \<U>)"
by (simp add: Infinitesimal_hypreal_of_nat_iff star_of_def
hnorm_def star_of_nat_def starfun_star_n
star_n_inverse star_n_less real_of_nat_def)
@@ -318,11 +316,11 @@
HNatInfinite_FreeUltrafilterNat_iff
Infinitesimal_FreeUltrafilterNat_iff2)
apply (drule_tac x="Suc m" in spec)
-apply (erule ultra, simp)
+apply (auto elim!: eventually_elim1)
done
lemma approx_FreeUltrafilterNat_iff: "star_n X @= star_n Y =
- (\<forall>r>0. {n. norm (X n - Y n) < r} : FreeUltrafilterNat)"
+ (\<forall>r>0. eventually (\<lambda>n. norm (X n - Y n) < r) \<U>)"
apply (subst approx_minus_iff)
apply (rule mem_infmal_iff [THEN subst])
apply (simp add: star_n_diff)
@@ -330,8 +328,7 @@
done
lemma approx_FreeUltrafilterNat_iff2: "star_n X @= star_n Y =
- (\<forall>m. {n. norm (X n - Y n) <
- inverse(real(Suc m))} : FreeUltrafilterNat)"
+ (\<forall>m. eventually (\<lambda>n. norm (X n - Y n) < inverse(real(Suc m))) \<U>)"
apply (subst approx_minus_iff)
apply (rule mem_infmal_iff [THEN subst])
apply (simp add: star_n_diff)
@@ -342,7 +339,7 @@
apply (rule inj_onI)
apply (rule ext, rule ccontr)
apply (drule_tac x = "star_n (%n. xa)" in fun_cong)
-apply (auto simp add: starfun star_n_eq_iff)
+apply (auto simp add: starfun star_n_eq_iff FreeUltrafilterNat.proper)
done
end
--- a/src/HOL/NSA/StarDef.thy Sun Apr 12 20:05:35 2015 +0200
+++ b/src/HOL/NSA/StarDef.thy Mon Apr 13 00:59:17 2015 +0200
@@ -5,13 +5,13 @@
section {* Construction of Star Types Using Ultrafilters *}
theory StarDef
-imports Filter
+imports Free_Ultrafilter
begin
subsection {* A Free Ultrafilter over the Naturals *}
definition
- FreeUltrafilterNat :: "nat set set" ("\<U>") where
+ FreeUltrafilterNat :: "nat filter" ("\<U>") where
"\<U> = (SOME U. freeultrafilter U)"
lemma freeultrafilter_FreeUltrafilterNat: "freeultrafilter \<U>"
@@ -24,19 +24,11 @@
interpretation FreeUltrafilterNat: freeultrafilter FreeUltrafilterNat
by (rule freeultrafilter_FreeUltrafilterNat)
-text {* This rule takes the place of the old ultra tactic *}
-
-lemma ultra:
- "\<lbrakk>{n. P n} \<in> \<U>; {n. P n \<longrightarrow> Q n} \<in> \<U>\<rbrakk> \<Longrightarrow> {n. Q n} \<in> \<U>"
-by (simp add: Collect_imp_eq
- FreeUltrafilterNat.Un_iff FreeUltrafilterNat.Compl_iff)
-
-
subsection {* Definition of @{text star} type constructor *}
definition
starrel :: "((nat \<Rightarrow> 'a) \<times> (nat \<Rightarrow> 'a)) set" where
- "starrel = {(X,Y). {n. X n = Y n} \<in> \<U>}"
+ "starrel = {(X,Y). eventually (\<lambda>n. X n = Y n) \<U>}"
definition "star = (UNIV :: (nat \<Rightarrow> 'a) set) // starrel"
@@ -59,14 +51,14 @@
text {* Proving that @{term starrel} is an equivalence relation *}
-lemma starrel_iff [iff]: "((X,Y) \<in> starrel) = ({n. X n = Y n} \<in> \<U>)"
+lemma starrel_iff [iff]: "((X,Y) \<in> starrel) = (eventually (\<lambda>n. X n = Y n) \<U>)"
by (simp add: starrel_def)
lemma equiv_starrel: "equiv UNIV starrel"
proof (rule equivI)
show "refl starrel" by (simp add: refl_on_def)
show "sym starrel" by (simp add: sym_def eq_commute)
- show "trans starrel" by (auto intro: transI elim!: ultra)
+ show "trans starrel" by (intro transI) (auto elim: eventually_elim2)
qed
lemmas equiv_starrel_iff =
@@ -75,7 +67,7 @@
lemma starrel_in_star: "starrel``{x} \<in> star"
by (simp add: star_def quotientI)
-lemma star_n_eq_iff: "(star_n X = star_n Y) = ({n. X n = Y n} \<in> \<U>)"
+lemma star_n_eq_iff: "(star_n X = star_n Y) = (eventually (\<lambda>n. X n = Y n) \<U>)"
by (simp add: star_n_def Abs_star_inject starrel_in_star equiv_starrel_iff)
@@ -83,8 +75,8 @@
text {* This introduction rule starts each transfer proof. *}
lemma transfer_start:
- "P \<equiv> {n. Q} \<in> \<U> \<Longrightarrow> Trueprop P \<equiv> Trueprop Q"
-by (subgoal_tac "P \<equiv> Q", simp, simp add: atomize_eq)
+ "P \<equiv> eventually (\<lambda>n. Q) \<U> \<Longrightarrow> Trueprop P \<equiv> Trueprop Q"
+ by (simp add: FreeUltrafilterNat.proper)
text {*Initialize transfer tactic.*}
ML_file "transfer.ML"
@@ -98,66 +90,66 @@
text {* Transfer introduction rules. *}
lemma transfer_ex [transfer_intro]:
- "\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
- \<Longrightarrow> \<exists>x::'a star. p x \<equiv> {n. \<exists>x. P n x} \<in> \<U>"
-by (simp only: ex_star_eq FreeUltrafilterNat.Collect_ex)
+ "\<lbrakk>\<And>X. p (star_n X) \<equiv> eventually (\<lambda>n. P n (X n)) \<U>\<rbrakk>
+ \<Longrightarrow> \<exists>x::'a star. p x \<equiv> eventually (\<lambda>n. \<exists>x. P n x) \<U>"
+by (simp only: ex_star_eq eventually_ex)
lemma transfer_all [transfer_intro]:
- "\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
- \<Longrightarrow> \<forall>x::'a star. p x \<equiv> {n. \<forall>x. P n x} \<in> \<U>"
-by (simp only: all_star_eq FreeUltrafilterNat.Collect_all)
+ "\<lbrakk>\<And>X. p (star_n X) \<equiv> eventually (\<lambda>n. P n (X n)) \<U>\<rbrakk>
+ \<Longrightarrow> \<forall>x::'a star. p x \<equiv> eventually (\<lambda>n. \<forall>x. P n x) \<U>"
+by (simp only: all_star_eq FreeUltrafilterNat.eventually_all_iff)
lemma transfer_not [transfer_intro]:
- "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>\<rbrakk> \<Longrightarrow> \<not> p \<equiv> {n. \<not> P n} \<in> \<U>"
-by (simp only: FreeUltrafilterNat.Collect_not)
+ "\<lbrakk>p \<equiv> eventually P \<U>\<rbrakk> \<Longrightarrow> \<not> p \<equiv> eventually (\<lambda>n. \<not> P n) \<U>"
+by (simp only: FreeUltrafilterNat.eventually_not_iff)
lemma transfer_conj [transfer_intro]:
- "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
- \<Longrightarrow> p \<and> q \<equiv> {n. P n \<and> Q n} \<in> \<U>"
-by (simp only: FreeUltrafilterNat.Collect_conj)
+ "\<lbrakk>p \<equiv> eventually P \<U>; q \<equiv> eventually Q \<U>\<rbrakk>
+ \<Longrightarrow> p \<and> q \<equiv> eventually (\<lambda>n. P n \<and> Q n) \<U>"
+by (simp only: eventually_conj_iff)
lemma transfer_disj [transfer_intro]:
- "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
- \<Longrightarrow> p \<or> q \<equiv> {n. P n \<or> Q n} \<in> \<U>"
-by (simp only: FreeUltrafilterNat.Collect_disj)
+ "\<lbrakk>p \<equiv> eventually P \<U>; q \<equiv> eventually Q \<U>\<rbrakk>
+ \<Longrightarrow> p \<or> q \<equiv> eventually (\<lambda>n. P n \<or> Q n) \<U>"
+by (simp only: FreeUltrafilterNat.eventually_disj_iff)
lemma transfer_imp [transfer_intro]:
- "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
- \<Longrightarrow> p \<longrightarrow> q \<equiv> {n. P n \<longrightarrow> Q n} \<in> \<U>"
-by (simp only: imp_conv_disj transfer_disj transfer_not)
+ "\<lbrakk>p \<equiv> eventually P \<U>; q \<equiv> eventually Q \<U>\<rbrakk>
+ \<Longrightarrow> p \<longrightarrow> q \<equiv> eventually (\<lambda>n. P n \<longrightarrow> Q n) \<U>"
+by (simp only: FreeUltrafilterNat.eventually_imp_iff)
lemma transfer_iff [transfer_intro]:
- "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
- \<Longrightarrow> p = q \<equiv> {n. P n = Q n} \<in> \<U>"
-by (simp only: iff_conv_conj_imp transfer_conj transfer_imp)
+ "\<lbrakk>p \<equiv> eventually P \<U>; q \<equiv> eventually Q \<U>\<rbrakk>
+ \<Longrightarrow> p = q \<equiv> eventually (\<lambda>n. P n = Q n) \<U>"
+by (simp only: FreeUltrafilterNat.eventually_iff_iff)
lemma transfer_if_bool [transfer_intro]:
- "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; x \<equiv> {n. X n} \<in> \<U>; y \<equiv> {n. Y n} \<in> \<U>\<rbrakk>
- \<Longrightarrow> (if p then x else y) \<equiv> {n. if P n then X n else Y n} \<in> \<U>"
+ "\<lbrakk>p \<equiv> eventually P \<U>; x \<equiv> eventually X \<U>; y \<equiv> eventually Y \<U>\<rbrakk>
+ \<Longrightarrow> (if p then x else y) \<equiv> eventually (\<lambda>n. if P n then X n else Y n) \<U>"
by (simp only: if_bool_eq_conj transfer_conj transfer_imp transfer_not)
lemma transfer_eq [transfer_intro]:
- "\<lbrakk>x \<equiv> star_n X; y \<equiv> star_n Y\<rbrakk> \<Longrightarrow> x = y \<equiv> {n. X n = Y n} \<in> \<U>"
+ "\<lbrakk>x \<equiv> star_n X; y \<equiv> star_n Y\<rbrakk> \<Longrightarrow> x = y \<equiv> eventually (\<lambda>n. X n = Y n) \<U>"
by (simp only: star_n_eq_iff)
lemma transfer_if [transfer_intro]:
- "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; x \<equiv> star_n X; y \<equiv> star_n Y\<rbrakk>
+ "\<lbrakk>p \<equiv> eventually (\<lambda>n. P n) \<U>; x \<equiv> star_n X; y \<equiv> star_n Y\<rbrakk>
\<Longrightarrow> (if p then x else y) \<equiv> star_n (\<lambda>n. if P n then X n else Y n)"
apply (rule eq_reflection)
-apply (auto simp add: star_n_eq_iff transfer_not elim!: ultra)
+apply (auto simp add: star_n_eq_iff transfer_not elim!: eventually_elim1)
done
lemma transfer_fun_eq [transfer_intro]:
"\<lbrakk>\<And>X. f (star_n X) = g (star_n X)
- \<equiv> {n. F n (X n) = G n (X n)} \<in> \<U>\<rbrakk>
- \<Longrightarrow> f = g \<equiv> {n. F n = G n} \<in> \<U>"
+ \<equiv> eventually (\<lambda>n. F n (X n) = G n (X n)) \<U>\<rbrakk>
+ \<Longrightarrow> f = g \<equiv> eventually (\<lambda>n. F n = G n) \<U>"
by (simp only: fun_eq_iff transfer_all)
lemma transfer_star_n [transfer_intro]: "star_n X \<equiv> star_n (\<lambda>n. X n)"
by (rule reflexive)
-lemma transfer_bool [transfer_intro]: "p \<equiv> {n. p} \<in> \<U>"
-by (simp add: atomize_eq)
+lemma transfer_bool [transfer_intro]: "p \<equiv> eventually (\<lambda>n. p) \<U>"
+by (simp add: FreeUltrafilterNat.proper)
subsection {* Standard elements *}
@@ -191,7 +183,7 @@
lemma Ifun_congruent2:
"congruent2 starrel starrel (\<lambda>F X. starrel``{\<lambda>n. F n (X n)})"
-by (auto simp add: congruent2_def equiv_starrel_iff elim!: ultra)
+by (auto simp add: congruent2_def equiv_starrel_iff elim!: eventually_rev_mp)
lemma Ifun_star_n: "star_n F \<star> star_n X = star_n (\<lambda>n. F n (X n))"
by (simp add: Ifun_def star_n_def Abs_star_inverse starrel_in_star
@@ -298,7 +290,7 @@
definition unstar :: "bool star \<Rightarrow> bool" where
"unstar b \<longleftrightarrow> b = star_of True"
-lemma unstar_star_n: "unstar (star_n P) = ({n. P n} \<in> \<U>)"
+lemma unstar_star_n: "unstar (star_n P) = (eventually P \<U>)"
by (simp add: unstar_def star_of_def star_n_eq_iff)
lemma unstar_star_of [simp]: "unstar (star_of p) = p"
@@ -308,7 +300,7 @@
setup {* Transfer_Principle.add_const @{const_name unstar} *}
lemma transfer_unstar [transfer_intro]:
- "p \<equiv> star_n P \<Longrightarrow> unstar p \<equiv> {n. P n} \<in> \<U>"
+ "p \<equiv> star_n P \<Longrightarrow> unstar p \<equiv> eventually P \<U>"
by (simp only: unstar_star_n)
definition
@@ -322,11 +314,11 @@
declare starP_def [transfer_unfold]
declare starP2_def [transfer_unfold]
-lemma starP_star_n: "( *p* P) (star_n X) = ({n. P (X n)} \<in> \<U>)"
+lemma starP_star_n: "( *p* P) (star_n X) = (eventually (\<lambda>n. P (X n)) \<U>)"
by (simp only: starP_def star_of_def Ifun_star_n unstar_star_n)
lemma starP2_star_n:
- "( *p2* P) (star_n X) (star_n Y) = ({n. P (X n) (Y n)} \<in> \<U>)"
+ "( *p2* P) (star_n X) (star_n Y) = (eventually (\<lambda>n. P (X n) (Y n)) \<U>)"
by (simp only: starP2_def star_of_def Ifun_star_n unstar_star_n)
lemma starP_star_of [simp]: "( *p* P) (star_of x) = P x"
@@ -343,7 +335,7 @@
"Iset A = {x. ( *p2* op \<in>) x A}"
lemma Iset_star_n:
- "(star_n X \<in> Iset (star_n A)) = ({n. X n \<in> A n} \<in> \<U>)"
+ "(star_n X \<in> Iset (star_n A)) = (eventually (\<lambda>n. X n \<in> A n) \<U>)"
by (simp add: Iset_def starP2_star_n)
text {* Transfer tactic should remove occurrences of @{term Iset} *}
@@ -351,27 +343,27 @@
lemma transfer_mem [transfer_intro]:
"\<lbrakk>x \<equiv> star_n X; a \<equiv> Iset (star_n A)\<rbrakk>
- \<Longrightarrow> x \<in> a \<equiv> {n. X n \<in> A n} \<in> \<U>"
+ \<Longrightarrow> x \<in> a \<equiv> eventually (\<lambda>n. X n \<in> A n) \<U>"
by (simp only: Iset_star_n)
lemma transfer_Collect [transfer_intro]:
- "\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
+ "\<lbrakk>\<And>X. p (star_n X) \<equiv> eventually (\<lambda>n. P n (X n)) \<U>\<rbrakk>
\<Longrightarrow> Collect p \<equiv> Iset (star_n (\<lambda>n. Collect (P n)))"
by (simp add: atomize_eq set_eq_iff all_star_eq Iset_star_n)
lemma transfer_set_eq [transfer_intro]:
"\<lbrakk>a \<equiv> Iset (star_n A); b \<equiv> Iset (star_n B)\<rbrakk>
- \<Longrightarrow> a = b \<equiv> {n. A n = B n} \<in> \<U>"
+ \<Longrightarrow> a = b \<equiv> eventually (\<lambda>n. A n = B n) \<U>"
by (simp only: set_eq_iff transfer_all transfer_iff transfer_mem)
lemma transfer_ball [transfer_intro]:
- "\<lbrakk>a \<equiv> Iset (star_n A); \<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
- \<Longrightarrow> \<forall>x\<in>a. p x \<equiv> {n. \<forall>x\<in>A n. P n x} \<in> \<U>"
+ "\<lbrakk>a \<equiv> Iset (star_n A); \<And>X. p (star_n X) \<equiv> eventually (\<lambda>n. P n (X n)) \<U>\<rbrakk>
+ \<Longrightarrow> \<forall>x\<in>a. p x \<equiv> eventually (\<lambda>n. \<forall>x\<in>A n. P n x) \<U>"
by (simp only: Ball_def transfer_all transfer_imp transfer_mem)
lemma transfer_bex [transfer_intro]:
- "\<lbrakk>a \<equiv> Iset (star_n A); \<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
- \<Longrightarrow> \<exists>x\<in>a. p x \<equiv> {n. \<exists>x\<in>A n. P n x} \<in> \<U>"
+ "\<lbrakk>a \<equiv> Iset (star_n A); \<And>X. p (star_n X) \<equiv> eventually (\<lambda>n. P n (X n)) \<U>\<rbrakk>
+ \<Longrightarrow> \<exists>x\<in>a. p x \<equiv> eventually (\<lambda>n. \<exists>x\<in>A n. P n x) \<U>"
by (simp only: Bex_def transfer_ex transfer_conj transfer_mem)
lemma transfer_Iset [transfer_intro]:
--- a/src/HOL/Topological_Spaces.thy Sun Apr 12 20:05:35 2015 +0200
+++ b/src/HOL/Topological_Spaces.thy Mon Apr 13 00:59:17 2015 +0200
@@ -322,557 +322,6 @@
by auto
qed
-subsection {* Filters *}
-
-text {*
- This definition also allows non-proper filters.
-*}
-
-locale is_filter =
- fixes F :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
- assumes True: "F (\<lambda>x. True)"
- assumes conj: "F (\<lambda>x. P x) \<Longrightarrow> F (\<lambda>x. Q x) \<Longrightarrow> F (\<lambda>x. P x \<and> Q x)"
- assumes mono: "\<forall>x. P x \<longrightarrow> Q x \<Longrightarrow> F (\<lambda>x. P x) \<Longrightarrow> F (\<lambda>x. Q x)"
-
-typedef 'a filter = "{F :: ('a \<Rightarrow> bool) \<Rightarrow> bool. is_filter F}"
-proof
- show "(\<lambda>x. True) \<in> ?filter" by (auto intro: is_filter.intro)
-qed
-
-lemma is_filter_Rep_filter: "is_filter (Rep_filter F)"
- using Rep_filter [of F] by simp
-
-lemma Abs_filter_inverse':
- assumes "is_filter F" shows "Rep_filter (Abs_filter F) = F"
- using assms by (simp add: Abs_filter_inverse)
-
-
-subsubsection {* Eventually *}
-
-definition eventually :: "('a \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> bool"
- where "eventually P F \<longleftrightarrow> Rep_filter F P"
-
-lemma eventually_Abs_filter:
- assumes "is_filter F" shows "eventually P (Abs_filter F) = F P"
- unfolding eventually_def using assms by (simp add: Abs_filter_inverse)
-
-lemma filter_eq_iff:
- shows "F = F' \<longleftrightarrow> (\<forall>P. eventually P F = eventually P F')"
- unfolding Rep_filter_inject [symmetric] fun_eq_iff eventually_def ..
-
-lemma eventually_True [simp]: "eventually (\<lambda>x. True) F"
- unfolding eventually_def
- by (rule is_filter.True [OF is_filter_Rep_filter])
-
-lemma always_eventually: "\<forall>x. P x \<Longrightarrow> eventually P F"
-proof -
- assume "\<forall>x. P x" hence "P = (\<lambda>x. True)" by (simp add: ext)
- thus "eventually P F" by simp
-qed
-
-lemma eventually_mono:
- "(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually P F \<Longrightarrow> eventually Q F"
- unfolding eventually_def
- by (rule is_filter.mono [OF is_filter_Rep_filter])
-
-lemma eventually_conj:
- assumes P: "eventually (\<lambda>x. P x) F"
- assumes Q: "eventually (\<lambda>x. Q x) F"
- shows "eventually (\<lambda>x. P x \<and> Q x) F"
- using assms unfolding eventually_def
- by (rule is_filter.conj [OF is_filter_Rep_filter])
-
-lemma eventually_Ball_finite:
- assumes "finite A" and "\<forall>y\<in>A. eventually (\<lambda>x. P x y) net"
- shows "eventually (\<lambda>x. \<forall>y\<in>A. P x y) net"
-using assms by (induct set: finite, simp, simp add: eventually_conj)
-
-lemma eventually_all_finite:
- fixes P :: "'a \<Rightarrow> 'b::finite \<Rightarrow> bool"
- assumes "\<And>y. eventually (\<lambda>x. P x y) net"
- shows "eventually (\<lambda>x. \<forall>y. P x y) net"
-using eventually_Ball_finite [of UNIV P] assms by simp
-
-lemma eventually_mp:
- assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
- assumes "eventually (\<lambda>x. P x) F"
- shows "eventually (\<lambda>x. Q x) F"
-proof (rule eventually_mono)
- show "\<forall>x. (P x \<longrightarrow> Q x) \<and> P x \<longrightarrow> Q x" by simp
- show "eventually (\<lambda>x. (P x \<longrightarrow> Q x) \<and> P x) F"
- using assms by (rule eventually_conj)
-qed
-
-lemma eventually_rev_mp:
- assumes "eventually (\<lambda>x. P x) F"
- assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
- shows "eventually (\<lambda>x. Q x) F"
-using assms(2) assms(1) by (rule eventually_mp)
-
-lemma eventually_conj_iff:
- "eventually (\<lambda>x. P x \<and> Q x) F \<longleftrightarrow> eventually P F \<and> eventually Q F"
- by (auto intro: eventually_conj elim: eventually_rev_mp)
-
-lemma eventually_elim1:
- assumes "eventually (\<lambda>i. P i) F"
- assumes "\<And>i. P i \<Longrightarrow> Q i"
- shows "eventually (\<lambda>i. Q i) F"
- using assms by (auto elim!: eventually_rev_mp)
-
-lemma eventually_elim2:
- assumes "eventually (\<lambda>i. P i) F"
- assumes "eventually (\<lambda>i. Q i) F"
- assumes "\<And>i. P i \<Longrightarrow> Q i \<Longrightarrow> R i"
- shows "eventually (\<lambda>i. R i) F"
- using assms by (auto elim!: eventually_rev_mp)
-
-lemma not_eventually_impI: "eventually P F \<Longrightarrow> \<not> eventually Q F \<Longrightarrow> \<not> eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
- by (auto intro: eventually_mp)
-
-lemma not_eventuallyD: "\<not> eventually P F \<Longrightarrow> \<exists>x. \<not> P x"
- by (metis always_eventually)
-
-lemma eventually_subst:
- assumes "eventually (\<lambda>n. P n = Q n) F"
- shows "eventually P F = eventually Q F" (is "?L = ?R")
-proof -
- from assms have "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
- and "eventually (\<lambda>x. Q x \<longrightarrow> P x) F"
- by (auto elim: eventually_elim1)
- then show ?thesis by (auto elim: eventually_elim2)
-qed
-
-ML {*
- fun eventually_elim_tac ctxt facts = SUBGOAL_CASES (fn (goal, i) =>
- let
- val mp_thms = facts RL @{thms eventually_rev_mp}
- val raw_elim_thm =
- (@{thm allI} RS @{thm always_eventually})
- |> fold (fn thm1 => fn thm2 => thm2 RS thm1) mp_thms
- |> fold (fn _ => fn thm => @{thm impI} RS thm) facts
- val cases_prop = Thm.prop_of (raw_elim_thm RS Goal.init (Thm.cterm_of ctxt goal))
- val cases = Rule_Cases.make_common ctxt cases_prop [(("elim", []), [])]
- in
- CASES cases (rtac raw_elim_thm i)
- end)
-*}
-
-method_setup eventually_elim = {*
- Scan.succeed (fn ctxt => METHOD_CASES (HEADGOAL o eventually_elim_tac ctxt))
-*} "elimination of eventually quantifiers"
-
-
-subsubsection {* Finer-than relation *}
-
-text {* @{term "F \<le> F'"} means that filter @{term F} is finer than
-filter @{term F'}. *}
-
-instantiation filter :: (type) complete_lattice
-begin
-
-definition le_filter_def:
- "F \<le> F' \<longleftrightarrow> (\<forall>P. eventually P F' \<longrightarrow> eventually P F)"
-
-definition
- "(F :: 'a filter) < F' \<longleftrightarrow> F \<le> F' \<and> \<not> F' \<le> F"
-
-definition
- "top = Abs_filter (\<lambda>P. \<forall>x. P x)"
-
-definition
- "bot = Abs_filter (\<lambda>P. True)"
-
-definition
- "sup F F' = Abs_filter (\<lambda>P. eventually P F \<and> eventually P F')"
-
-definition
- "inf F F' = Abs_filter
- (\<lambda>P. \<exists>Q R. eventually Q F \<and> eventually R F' \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x))"
-
-definition
- "Sup S = Abs_filter (\<lambda>P. \<forall>F\<in>S. eventually P F)"
-
-definition
- "Inf S = Sup {F::'a filter. \<forall>F'\<in>S. F \<le> F'}"
-
-lemma eventually_top [simp]: "eventually P top \<longleftrightarrow> (\<forall>x. P x)"
- unfolding top_filter_def
- by (rule eventually_Abs_filter, rule is_filter.intro, auto)
-
-lemma eventually_bot [simp]: "eventually P bot"
- unfolding bot_filter_def
- by (subst eventually_Abs_filter, rule is_filter.intro, auto)
-
-lemma eventually_sup:
- "eventually P (sup F F') \<longleftrightarrow> eventually P F \<and> eventually P F'"
- unfolding sup_filter_def
- by (rule eventually_Abs_filter, rule is_filter.intro)
- (auto elim!: eventually_rev_mp)
-
-lemma eventually_inf:
- "eventually P (inf F F') \<longleftrightarrow>
- (\<exists>Q R. eventually Q F \<and> eventually R F' \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x))"
- unfolding inf_filter_def
- apply (rule eventually_Abs_filter, rule is_filter.intro)
- apply (fast intro: eventually_True)
- apply clarify
- apply (intro exI conjI)
- apply (erule (1) eventually_conj)
- apply (erule (1) eventually_conj)
- apply simp
- apply auto
- done
-
-lemma eventually_Sup:
- "eventually P (Sup S) \<longleftrightarrow> (\<forall>F\<in>S. eventually P F)"
- unfolding Sup_filter_def
- apply (rule eventually_Abs_filter, rule is_filter.intro)
- apply (auto intro: eventually_conj elim!: eventually_rev_mp)
- done
-
-instance proof
- fix F F' F'' :: "'a filter" and S :: "'a filter set"
- { show "F < F' \<longleftrightarrow> F \<le> F' \<and> \<not> F' \<le> F"
- by (rule less_filter_def) }
- { show "F \<le> F"
- unfolding le_filter_def by simp }
- { assume "F \<le> F'" and "F' \<le> F''" thus "F \<le> F''"
- unfolding le_filter_def by simp }
- { assume "F \<le> F'" and "F' \<le> F" thus "F = F'"
- unfolding le_filter_def filter_eq_iff by fast }
- { show "inf F F' \<le> F" and "inf F F' \<le> F'"
- unfolding le_filter_def eventually_inf by (auto intro: eventually_True) }
- { assume "F \<le> F'" and "F \<le> F''" thus "F \<le> inf F' F''"
- unfolding le_filter_def eventually_inf
- by (auto elim!: eventually_mono intro: eventually_conj) }
- { show "F \<le> sup F F'" and "F' \<le> sup F F'"
- unfolding le_filter_def eventually_sup by simp_all }
- { assume "F \<le> F''" and "F' \<le> F''" thus "sup F F' \<le> F''"
- unfolding le_filter_def eventually_sup by simp }
- { assume "F'' \<in> S" thus "Inf S \<le> F''"
- unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp }
- { assume "\<And>F'. F' \<in> S \<Longrightarrow> F \<le> F'" thus "F \<le> Inf S"
- unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp }
- { assume "F \<in> S" thus "F \<le> Sup S"
- unfolding le_filter_def eventually_Sup by simp }
- { assume "\<And>F. F \<in> S \<Longrightarrow> F \<le> F'" thus "Sup S \<le> F'"
- unfolding le_filter_def eventually_Sup by simp }
- { show "Inf {} = (top::'a filter)"
- by (auto simp: top_filter_def Inf_filter_def Sup_filter_def)
- (metis (full_types) top_filter_def always_eventually eventually_top) }
- { show "Sup {} = (bot::'a filter)"
- by (auto simp: bot_filter_def Sup_filter_def) }
-qed
-
-end
-
-lemma filter_leD:
- "F \<le> F' \<Longrightarrow> eventually P F' \<Longrightarrow> eventually P F"
- unfolding le_filter_def by simp
-
-lemma filter_leI:
- "(\<And>P. eventually P F' \<Longrightarrow> eventually P F) \<Longrightarrow> F \<le> F'"
- unfolding le_filter_def by simp
-
-lemma eventually_False:
- "eventually (\<lambda>x. False) F \<longleftrightarrow> F = bot"
- unfolding filter_eq_iff by (auto elim: eventually_rev_mp)
-
-abbreviation (input) trivial_limit :: "'a filter \<Rightarrow> bool"
- where "trivial_limit F \<equiv> F = bot"
-
-lemma trivial_limit_def: "trivial_limit F \<longleftrightarrow> eventually (\<lambda>x. False) F"
- by (rule eventually_False [symmetric])
-
-lemma eventually_const: "\<not> trivial_limit net \<Longrightarrow> eventually (\<lambda>x. P) net \<longleftrightarrow> P"
- by (cases P) (simp_all add: eventually_False)
-
-lemma eventually_Inf: "eventually P (Inf B) \<longleftrightarrow> (\<exists>X\<subseteq>B. finite X \<and> eventually P (Inf X))"
-proof -
- let ?F = "\<lambda>P. \<exists>X\<subseteq>B. finite X \<and> eventually P (Inf X)"
-
- { fix P have "eventually P (Abs_filter ?F) \<longleftrightarrow> ?F P"
- proof (rule eventually_Abs_filter is_filter.intro)+
- show "?F (\<lambda>x. True)"
- by (rule exI[of _ "{}"]) (simp add: le_fun_def)
- next
- fix P Q
- assume "?F P" then guess X ..
- moreover
- assume "?F Q" then guess Y ..
- ultimately show "?F (\<lambda>x. P x \<and> Q x)"
- by (intro exI[of _ "X \<union> Y"])
- (auto simp: Inf_union_distrib eventually_inf)
- next
- fix P Q
- assume "?F P" then guess X ..
- moreover assume "\<forall>x. P x \<longrightarrow> Q x"
- ultimately show "?F Q"
- by (intro exI[of _ X]) (auto elim: eventually_elim1)
- qed }
- note eventually_F = this
-
- have "Inf B = Abs_filter ?F"
- proof (intro antisym Inf_greatest)
- show "Inf B \<le> Abs_filter ?F"
- by (auto simp: le_filter_def eventually_F dest: Inf_superset_mono)
- next
- fix F assume "F \<in> B" then show "Abs_filter ?F \<le> F"
- by (auto simp add: le_filter_def eventually_F intro!: exI[of _ "{F}"])
- qed
- then show ?thesis
- by (simp add: eventually_F)
-qed
-
-lemma eventually_INF: "eventually P (INF b:B. F b) \<longleftrightarrow> (\<exists>X\<subseteq>B. finite X \<and> eventually P (INF b:X. F b))"
- unfolding INF_def[of B] eventually_Inf[of P "F`B"]
- by (metis Inf_image_eq finite_imageI image_mono finite_subset_image)
-
-lemma Inf_filter_not_bot:
- fixes B :: "'a filter set"
- shows "(\<And>X. X \<subseteq> B \<Longrightarrow> finite X \<Longrightarrow> Inf X \<noteq> bot) \<Longrightarrow> Inf B \<noteq> bot"
- unfolding trivial_limit_def eventually_Inf[of _ B]
- bot_bool_def [symmetric] bot_fun_def [symmetric] bot_unique by simp
-
-lemma INF_filter_not_bot:
- fixes F :: "'i \<Rightarrow> 'a filter"
- shows "(\<And>X. X \<subseteq> B \<Longrightarrow> finite X \<Longrightarrow> (INF b:X. F b) \<noteq> bot) \<Longrightarrow> (INF b:B. F b) \<noteq> bot"
- unfolding trivial_limit_def eventually_INF[of _ B]
- bot_bool_def [symmetric] bot_fun_def [symmetric] bot_unique by simp
-
-lemma eventually_Inf_base:
- assumes "B \<noteq> {}" and base: "\<And>F G. F \<in> B \<Longrightarrow> G \<in> B \<Longrightarrow> \<exists>x\<in>B. x \<le> inf F G"
- shows "eventually P (Inf B) \<longleftrightarrow> (\<exists>b\<in>B. eventually P b)"
-proof (subst eventually_Inf, safe)
- fix X assume "finite X" "X \<subseteq> B"
- then have "\<exists>b\<in>B. \<forall>x\<in>X. b \<le> x"
- proof induct
- case empty then show ?case
- using `B \<noteq> {}` by auto
- next
- case (insert x X)
- then obtain b where "b \<in> B" "\<And>x. x \<in> X \<Longrightarrow> b \<le> x"
- by auto
- with `insert x X \<subseteq> B` base[of b x] show ?case
- by (auto intro: order_trans)
- qed
- then obtain b where "b \<in> B" "b \<le> Inf X"
- by (auto simp: le_Inf_iff)
- then show "eventually P (Inf X) \<Longrightarrow> Bex B (eventually P)"
- by (intro bexI[of _ b]) (auto simp: le_filter_def)
-qed (auto intro!: exI[of _ "{x}" for x])
-
-lemma eventually_INF_base:
- "B \<noteq> {} \<Longrightarrow> (\<And>a b. a \<in> B \<Longrightarrow> b \<in> B \<Longrightarrow> \<exists>x\<in>B. F x \<le> inf (F a) (F b)) \<Longrightarrow>
- eventually P (INF b:B. F b) \<longleftrightarrow> (\<exists>b\<in>B. eventually P (F b))"
- unfolding INF_def by (subst eventually_Inf_base) auto
-
-
-subsubsection {* Map function for filters *}
-
-definition filtermap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a filter \<Rightarrow> 'b filter"
- where "filtermap f F = Abs_filter (\<lambda>P. eventually (\<lambda>x. P (f x)) F)"
-
-lemma eventually_filtermap:
- "eventually P (filtermap f F) = eventually (\<lambda>x. P (f x)) F"
- unfolding filtermap_def
- apply (rule eventually_Abs_filter)
- apply (rule is_filter.intro)
- apply (auto elim!: eventually_rev_mp)
- done
-
-lemma filtermap_ident: "filtermap (\<lambda>x. x) F = F"
- by (simp add: filter_eq_iff eventually_filtermap)
-
-lemma filtermap_filtermap:
- "filtermap f (filtermap g F) = filtermap (\<lambda>x. f (g x)) F"
- by (simp add: filter_eq_iff eventually_filtermap)
-
-lemma filtermap_mono: "F \<le> F' \<Longrightarrow> filtermap f F \<le> filtermap f F'"
- unfolding le_filter_def eventually_filtermap by simp
-
-lemma filtermap_bot [simp]: "filtermap f bot = bot"
- by (simp add: filter_eq_iff eventually_filtermap)
-
-lemma filtermap_sup: "filtermap f (sup F1 F2) = sup (filtermap f F1) (filtermap f F2)"
- by (auto simp: filter_eq_iff eventually_filtermap eventually_sup)
-
-lemma filtermap_inf: "filtermap f (inf F1 F2) \<le> inf (filtermap f F1) (filtermap f F2)"
- by (auto simp: le_filter_def eventually_filtermap eventually_inf)
-
-lemma filtermap_INF: "filtermap f (INF b:B. F b) \<le> (INF b:B. filtermap f (F b))"
-proof -
- { fix X :: "'c set" assume "finite X"
- then have "filtermap f (INFIMUM X F) \<le> (INF b:X. filtermap f (F b))"
- proof induct
- case (insert x X)
- have "filtermap f (INF a:insert x X. F a) \<le> inf (filtermap f (F x)) (filtermap f (INF a:X. F a))"
- by (rule order_trans[OF _ filtermap_inf]) simp
- also have "\<dots> \<le> inf (filtermap f (F x)) (INF a:X. filtermap f (F a))"
- by (intro inf_mono insert order_refl)
- finally show ?case
- by simp
- qed simp }
- then show ?thesis
- unfolding le_filter_def eventually_filtermap
- by (subst (1 2) eventually_INF) auto
-qed
-subsubsection {* Standard filters *}
-
-definition principal :: "'a set \<Rightarrow> 'a filter" where
- "principal S = Abs_filter (\<lambda>P. \<forall>x\<in>S. P x)"
-
-lemma eventually_principal: "eventually P (principal S) \<longleftrightarrow> (\<forall>x\<in>S. P x)"
- unfolding principal_def
- by (rule eventually_Abs_filter, rule is_filter.intro) auto
-
-lemma eventually_inf_principal: "eventually P (inf F (principal s)) \<longleftrightarrow> eventually (\<lambda>x. x \<in> s \<longrightarrow> P x) F"
- unfolding eventually_inf eventually_principal by (auto elim: eventually_elim1)
-
-lemma principal_UNIV[simp]: "principal UNIV = top"
- by (auto simp: filter_eq_iff eventually_principal)
-
-lemma principal_empty[simp]: "principal {} = bot"
- by (auto simp: filter_eq_iff eventually_principal)
-
-lemma principal_eq_bot_iff: "principal X = bot \<longleftrightarrow> X = {}"
- by (auto simp add: filter_eq_iff eventually_principal)
-
-lemma principal_le_iff[iff]: "principal A \<le> principal B \<longleftrightarrow> A \<subseteq> B"
- by (auto simp: le_filter_def eventually_principal)
-
-lemma le_principal: "F \<le> principal A \<longleftrightarrow> eventually (\<lambda>x. x \<in> A) F"
- unfolding le_filter_def eventually_principal
- apply safe
- apply (erule_tac x="\<lambda>x. x \<in> A" in allE)
- apply (auto elim: eventually_elim1)
- done
-
-lemma principal_inject[iff]: "principal A = principal B \<longleftrightarrow> A = B"
- unfolding eq_iff by simp
-
-lemma sup_principal[simp]: "sup (principal A) (principal B) = principal (A \<union> B)"
- unfolding filter_eq_iff eventually_sup eventually_principal by auto
-
-lemma inf_principal[simp]: "inf (principal A) (principal B) = principal (A \<inter> B)"
- unfolding filter_eq_iff eventually_inf eventually_principal
- by (auto intro: exI[of _ "\<lambda>x. x \<in> A"] exI[of _ "\<lambda>x. x \<in> B"])
-
-lemma SUP_principal[simp]: "(SUP i : I. principal (A i)) = principal (\<Union>i\<in>I. A i)"
- unfolding filter_eq_iff eventually_Sup SUP_def by (auto simp: eventually_principal)
-
-lemma INF_principal_finite: "finite X \<Longrightarrow> (INF x:X. principal (f x)) = principal (\<Inter>x\<in>X. f x)"
- by (induct X rule: finite_induct) auto
-
-lemma filtermap_principal[simp]: "filtermap f (principal A) = principal (f ` A)"
- unfolding filter_eq_iff eventually_filtermap eventually_principal by simp
-
-subsubsection {* Order filters *}
-
-definition at_top :: "('a::order) filter"
- where "at_top = (INF k. principal {k ..})"
-
-lemma at_top_sub: "at_top = (INF k:{c::'a::linorder..}. principal {k ..})"
- by (auto intro!: INF_eq max.cobounded1 max.cobounded2 simp: at_top_def)
-
-lemma eventually_at_top_linorder: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::linorder. \<forall>n\<ge>N. P n)"
- unfolding at_top_def
- by (subst eventually_INF_base) (auto simp: eventually_principal intro: max.cobounded1 max.cobounded2)
-
-lemma eventually_ge_at_top:
- "eventually (\<lambda>x. (c::_::linorder) \<le> x) at_top"
- unfolding eventually_at_top_linorder by auto
-
-lemma eventually_at_top_dense: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::{no_top, linorder}. \<forall>n>N. P n)"
-proof -
- have "eventually P (INF k. principal {k <..}) \<longleftrightarrow> (\<exists>N::'a. \<forall>n>N. P n)"
- by (subst eventually_INF_base) (auto simp: eventually_principal intro: max.cobounded1 max.cobounded2)
- also have "(INF k. principal {k::'a <..}) = at_top"
- unfolding at_top_def
- by (intro INF_eq) (auto intro: less_imp_le simp: Ici_subset_Ioi_iff gt_ex)
- finally show ?thesis .
-qed
-
-lemma eventually_gt_at_top:
- "eventually (\<lambda>x. (c::_::unbounded_dense_linorder) < x) at_top"
- unfolding eventually_at_top_dense by auto
-
-definition at_bot :: "('a::order) filter"
- where "at_bot = (INF k. principal {.. k})"
-
-lemma at_bot_sub: "at_bot = (INF k:{.. c::'a::linorder}. principal {.. k})"
- by (auto intro!: INF_eq min.cobounded1 min.cobounded2 simp: at_bot_def)
-
-lemma eventually_at_bot_linorder:
- fixes P :: "'a::linorder \<Rightarrow> bool" shows "eventually P at_bot \<longleftrightarrow> (\<exists>N. \<forall>n\<le>N. P n)"
- unfolding at_bot_def
- by (subst eventually_INF_base) (auto simp: eventually_principal intro: min.cobounded1 min.cobounded2)
-
-lemma eventually_le_at_bot:
- "eventually (\<lambda>x. x \<le> (c::_::linorder)) at_bot"
- unfolding eventually_at_bot_linorder by auto
-
-lemma eventually_at_bot_dense: "eventually P at_bot \<longleftrightarrow> (\<exists>N::'a::{no_bot, linorder}. \<forall>n<N. P n)"
-proof -
- have "eventually P (INF k. principal {..< k}) \<longleftrightarrow> (\<exists>N::'a. \<forall>n<N. P n)"
- by (subst eventually_INF_base) (auto simp: eventually_principal intro: min.cobounded1 min.cobounded2)
- also have "(INF k. principal {..< k::'a}) = at_bot"
- unfolding at_bot_def
- by (intro INF_eq) (auto intro: less_imp_le simp: Iic_subset_Iio_iff lt_ex)
- finally show ?thesis .
-qed
-
-lemma eventually_gt_at_bot:
- "eventually (\<lambda>x. x < (c::_::unbounded_dense_linorder)) at_bot"
- unfolding eventually_at_bot_dense by auto
-
-lemma trivial_limit_at_bot_linorder: "\<not> trivial_limit (at_bot ::('a::linorder) filter)"
- unfolding trivial_limit_def
- by (metis eventually_at_bot_linorder order_refl)
-
-lemma trivial_limit_at_top_linorder: "\<not> trivial_limit (at_top ::('a::linorder) filter)"
- unfolding trivial_limit_def
- by (metis eventually_at_top_linorder order_refl)
-
-subsection {* Sequentially *}
-
-abbreviation sequentially :: "nat filter"
- where "sequentially \<equiv> at_top"
-
-lemma eventually_sequentially:
- "eventually P sequentially \<longleftrightarrow> (\<exists>N. \<forall>n\<ge>N. P n)"
- by (rule eventually_at_top_linorder)
-
-lemma sequentially_bot [simp, intro]: "sequentially \<noteq> bot"
- unfolding filter_eq_iff eventually_sequentially by auto
-
-lemmas trivial_limit_sequentially = sequentially_bot
-
-lemma eventually_False_sequentially [simp]:
- "\<not> eventually (\<lambda>n. False) sequentially"
- by (simp add: eventually_False)
-
-lemma le_sequentially:
- "F \<le> sequentially \<longleftrightarrow> (\<forall>N. eventually (\<lambda>n. N \<le> n) F)"
- by (simp add: at_top_def le_INF_iff le_principal)
-
-lemma eventually_sequentiallyI:
- assumes "\<And>x. c \<le> x \<Longrightarrow> P x"
- shows "eventually P sequentially"
-using assms by (auto simp: eventually_sequentially)
-
-lemma eventually_sequentially_seg:
- "eventually (\<lambda>n. P (n + k)) sequentially \<longleftrightarrow> eventually P sequentially"
- unfolding eventually_sequentially
- apply safe
- apply (rule_tac x="N + k" in exI)
- apply rule
- apply (erule_tac x="n - k" in allE)
- apply auto []
- apply (rule_tac x=N in exI)
- apply auto []
- done
-
subsubsection {* Topological filters *}
definition (in topological_space) nhds :: "'a \<Rightarrow> 'a filter"
@@ -1005,104 +454,6 @@
"eventually P (at (x::'a::linorder_topology)) \<longleftrightarrow> eventually P (at_left x) \<and> eventually P (at_right x)"
by (subst at_eq_sup_left_right) (simp add: eventually_sup)
-subsection {* Limits *}
-
-definition filterlim :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b filter \<Rightarrow> 'a filter \<Rightarrow> bool" where
- "filterlim f F2 F1 \<longleftrightarrow> filtermap f F1 \<le> F2"
-
-syntax
- "_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"
-
-lemma filterlim_iff:
- "(LIM x F1. f x :> F2) \<longleftrightarrow> (\<forall>P. eventually P F2 \<longrightarrow> eventually (\<lambda>x. P (f x)) F1)"
- unfolding filterlim_def le_filter_def eventually_filtermap ..
-
-lemma filterlim_compose:
- "filterlim g F3 F2 \<Longrightarrow> filterlim f F2 F1 \<Longrightarrow> filterlim (\<lambda>x. g (f x)) F3 F1"
- unfolding filterlim_def filtermap_filtermap[symmetric] by (metis filtermap_mono order_trans)
-
-lemma filterlim_mono:
- "filterlim f F2 F1 \<Longrightarrow> F2 \<le> F2' \<Longrightarrow> F1' \<le> F1 \<Longrightarrow> filterlim f F2' F1'"
- unfolding filterlim_def by (metis filtermap_mono order_trans)
-
-lemma filterlim_ident: "LIM x F. x :> F"
- by (simp add: filterlim_def filtermap_ident)
-
-lemma filterlim_cong:
- "F1 = F1' \<Longrightarrow> F2 = F2' \<Longrightarrow> eventually (\<lambda>x. f x = g x) F2 \<Longrightarrow> filterlim f F1 F2 = filterlim g F1' F2'"
- by (auto simp: filterlim_def le_filter_def eventually_filtermap elim: eventually_elim2)
-
-lemma filterlim_mono_eventually:
- assumes "filterlim f F G" and ord: "F \<le> F'" "G' \<le> G"
- assumes eq: "eventually (\<lambda>x. f x = f' x) G'"
- shows "filterlim f' F' G'"
- apply (rule filterlim_cong[OF refl refl eq, THEN iffD1])
- apply (rule filterlim_mono[OF _ ord])
- apply fact
- done
-
-lemma filtermap_mono_strong: "inj f \<Longrightarrow> filtermap f F \<le> filtermap f G \<longleftrightarrow> F \<le> G"
- apply (auto intro!: filtermap_mono) []
- apply (auto simp: le_filter_def eventually_filtermap)
- apply (erule_tac x="\<lambda>x. P (inv f x)" in allE)
- apply auto
- done
-
-lemma filtermap_eq_strong: "inj f \<Longrightarrow> filtermap f F = filtermap f G \<longleftrightarrow> F = G"
- by (simp add: filtermap_mono_strong eq_iff)
-
-lemma filterlim_principal:
- "(LIM x F. f x :> principal S) \<longleftrightarrow> (eventually (\<lambda>x. f x \<in> S) F)"
- unfolding filterlim_def eventually_filtermap le_principal ..
-
-lemma filterlim_inf:
- "(LIM x F1. f x :> inf F2 F3) \<longleftrightarrow> ((LIM x F1. f x :> F2) \<and> (LIM x F1. f x :> F3))"
- unfolding filterlim_def by simp
-
-lemma filterlim_INF:
- "(LIM x F. f x :> (INF b:B. G b)) \<longleftrightarrow> (\<forall>b\<in>B. LIM x F. f x :> G b)"
- unfolding filterlim_def le_INF_iff ..
-
-lemma filterlim_INF_INF:
- "(\<And>m. m \<in> J \<Longrightarrow> \<exists>i\<in>I. filtermap f (F i) \<le> G m) \<Longrightarrow> LIM x (INF i:I. F i). f x :> (INF j:J. G j)"
- unfolding filterlim_def by (rule order_trans[OF filtermap_INF INF_mono])
-
-lemma filterlim_base:
- "(\<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>
- LIM x (INF i:I. principal (F i)). f x :> (INF j:J. principal (G j))"
- by (force intro!: filterlim_INF_INF simp: image_subset_iff)
-
-lemma filterlim_base_iff:
- 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"
- shows "(LIM x (INF i:I. principal (F i)). f x :> INF j:J. principal (G j)) \<longleftrightarrow>
- (\<forall>j\<in>J. \<exists>i\<in>I. \<forall>x\<in>F i. f x \<in> G j)"
- unfolding filterlim_INF filterlim_principal
-proof (subst eventually_INF_base)
- fix i j assume "i \<in> I" "j \<in> I"
- with chain[OF this] show "\<exists>x\<in>I. principal (F x) \<le> inf (principal (F i)) (principal (F j))"
- by auto
-qed (auto simp: eventually_principal `I \<noteq> {}`)
-
-lemma filterlim_filtermap: "filterlim f F1 (filtermap g F2) = filterlim (\<lambda>x. f (g x)) F1 F2"
- unfolding filterlim_def filtermap_filtermap ..
-
-lemma filterlim_sup:
- "filterlim f F F1 \<Longrightarrow> filterlim f F F2 \<Longrightarrow> filterlim f F (sup F1 F2)"
- unfolding filterlim_def filtermap_sup by auto
-
-lemma eventually_sequentially_Suc: "eventually (\<lambda>i. P (Suc i)) sequentially \<longleftrightarrow> eventually P sequentially"
- unfolding eventually_sequentially by (metis Suc_le_D Suc_le_mono le_Suc_eq)
-
-lemma filterlim_sequentially_Suc:
- "(LIM x sequentially. f (Suc x) :> F) \<longleftrightarrow> (LIM x sequentially. f x :> F)"
- unfolding filterlim_iff by (subst eventually_sequentially_Suc) simp
-
-lemma filterlim_Suc: "filterlim Suc sequentially sequentially"
- by (simp add: filterlim_iff eventually_sequentially) (metis le_Suc_eq)
-
subsubsection {* Tendsto *}
abbreviation (in topological_space)
@@ -1296,92 +647,6 @@
lemma Lim_ident_at: "\<not> trivial_limit (at x within s) \<Longrightarrow> Lim (at x within s) (\<lambda>x. x) = x"
by (rule tendsto_Lim[OF _ tendsto_ident_at]) auto
-subsection {* Limits to @{const at_top} and @{const at_bot} *}
-
-lemma filterlim_at_top:
- fixes f :: "'a \<Rightarrow> ('b::linorder)"
- shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. Z \<le> f x) F)"
- by (auto simp: filterlim_iff eventually_at_top_linorder elim!: eventually_elim1)
-
-lemma filterlim_at_top_mono:
- "LIM x F. f x :> at_top \<Longrightarrow> eventually (\<lambda>x. f x \<le> (g x::'a::linorder)) F \<Longrightarrow>
- LIM x F. g x :> at_top"
- by (auto simp: filterlim_at_top elim: eventually_elim2 intro: order_trans)
-
-lemma filterlim_at_top_dense:
- fixes f :: "'a \<Rightarrow> ('b::unbounded_dense_linorder)"
- shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. Z < f x) F)"
- by (metis eventually_elim1[of _ F] eventually_gt_at_top order_less_imp_le
- filterlim_at_top[of f F] filterlim_iff[of f at_top F])
-
-lemma filterlim_at_top_ge:
- fixes f :: "'a \<Rightarrow> ('b::linorder)" and c :: "'b"
- shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z\<ge>c. eventually (\<lambda>x. Z \<le> f x) F)"
- unfolding at_top_sub[of c] filterlim_INF by (auto simp add: filterlim_principal)
-
-lemma filterlim_at_top_at_top:
- fixes f :: "'a::linorder \<Rightarrow> 'b::linorder"
- assumes mono: "\<And>x y. Q x \<Longrightarrow> Q y \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
- assumes bij: "\<And>x. P x \<Longrightarrow> f (g x) = x" "\<And>x. P x \<Longrightarrow> Q (g x)"
- assumes Q: "eventually Q at_top"
- assumes P: "eventually P at_top"
- shows "filterlim f at_top at_top"
-proof -
- from P obtain x where x: "\<And>y. x \<le> y \<Longrightarrow> P y"
- unfolding eventually_at_top_linorder by auto
- show ?thesis
- proof (intro filterlim_at_top_ge[THEN iffD2] allI impI)
- fix z assume "x \<le> z"
- with x have "P z" by auto
- have "eventually (\<lambda>x. g z \<le> x) at_top"
- by (rule eventually_ge_at_top)
- with Q show "eventually (\<lambda>x. z \<le> f x) at_top"
- by eventually_elim (metis mono bij `P z`)
- qed
-qed
-
-lemma filterlim_at_top_gt:
- fixes f :: "'a \<Rightarrow> ('b::unbounded_dense_linorder)" and c :: "'b"
- shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z>c. eventually (\<lambda>x. Z \<le> f x) F)"
- by (metis filterlim_at_top order_less_le_trans gt_ex filterlim_at_top_ge)
-
-lemma filterlim_at_bot:
- fixes f :: "'a \<Rightarrow> ('b::linorder)"
- shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. f x \<le> Z) F)"
- by (auto simp: filterlim_iff eventually_at_bot_linorder elim!: eventually_elim1)
-
-lemma filterlim_at_bot_dense:
- fixes f :: "'a \<Rightarrow> ('b::{dense_linorder, no_bot})"
- shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. f x < Z) F)"
-proof (auto simp add: filterlim_at_bot[of f F])
- fix Z :: 'b
- from lt_ex [of Z] obtain Z' where 1: "Z' < Z" ..
- assume "\<forall>Z. eventually (\<lambda>x. f x \<le> Z) F"
- hence "eventually (\<lambda>x. f x \<le> Z') F" by auto
- thus "eventually (\<lambda>x. f x < Z) F"
- apply (rule eventually_mono[rotated])
- using 1 by auto
- next
- fix Z :: 'b
- show "\<forall>Z. eventually (\<lambda>x. f x < Z) F \<Longrightarrow> eventually (\<lambda>x. f x \<le> Z) F"
- by (drule spec [of _ Z], erule eventually_mono[rotated], auto simp add: less_imp_le)
-qed
-
-lemma filterlim_at_bot_le:
- fixes f :: "'a \<Rightarrow> ('b::linorder)" and c :: "'b"
- shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z\<le>c. eventually (\<lambda>x. Z \<ge> f x) F)"
- unfolding filterlim_at_bot
-proof safe
- fix Z assume *: "\<forall>Z\<le>c. eventually (\<lambda>x. Z \<ge> f x) F"
- with *[THEN spec, of "min Z c"] show "eventually (\<lambda>x. Z \<ge> f x) F"
- by (auto elim!: eventually_elim1)
-qed simp
-
-lemma filterlim_at_bot_lt:
- fixes f :: "'a \<Rightarrow> ('b::unbounded_dense_linorder)" and c :: "'b"
- shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z<c. eventually (\<lambda>x. Z \<ge> f x) F)"
- by (metis filterlim_at_bot filterlim_at_bot_le lt_ex order_le_less_trans)
-
lemma filterlim_at_bot_at_right:
fixes f :: "'a::linorder_topology \<Rightarrow> 'b::linorder"
assumes mono: "\<And>x y. Q x \<Longrightarrow> Q y \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
@@ -2371,7 +1636,7 @@
by (rule compactE)
from `D \<subseteq> ?C` have "\<forall>x\<in>D. eventually (\<lambda>y. y \<notin> x) (nhds y)" by auto
with `finite D` have "eventually (\<lambda>y. y \<notin> \<Union>D) (nhds y)"
- by (simp add: eventually_Ball_finite)
+ by (simp add: eventually_ball_finite)
with `s \<subseteq> \<Union>D` have "eventually (\<lambda>y. y \<notin> s) (nhds y)"
by (auto elim!: eventually_mono [rotated])
thus "\<exists>t. open t \<and> y \<in> t \<and> t \<subseteq> - s"
@@ -2936,220 +2201,4 @@
qed
qed (intro cSUP_least `antimono f`[THEN antimonoD] cInf_lower S)
-subsection {* Setup @{typ "'a filter"} for lifting and transfer *}
-
-context begin interpretation lifting_syntax .
-
-definition rel_filter :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> 'b filter \<Rightarrow> bool"
-where "rel_filter R F G = ((R ===> op =) ===> op =) (Rep_filter F) (Rep_filter G)"
-
-lemma rel_filter_eventually:
- "rel_filter R F G \<longleftrightarrow>
- ((R ===> op =) ===> op =) (\<lambda>P. eventually P F) (\<lambda>P. eventually P G)"
-by(simp add: rel_filter_def eventually_def)
-
-lemma filtermap_id [simp, id_simps]: "filtermap id = id"
-by(simp add: fun_eq_iff id_def filtermap_ident)
-
-lemma filtermap_id' [simp]: "filtermap (\<lambda>x. x) = (\<lambda>F. F)"
-using filtermap_id unfolding id_def .
-
-lemma Quotient_filter [quot_map]:
- assumes Q: "Quotient R Abs Rep T"
- shows "Quotient (rel_filter R) (filtermap Abs) (filtermap Rep) (rel_filter T)"
-unfolding Quotient_alt_def
-proof(intro conjI strip)
- from Q have *: "\<And>x y. T x y \<Longrightarrow> Abs x = y"
- unfolding Quotient_alt_def by blast
-
- fix F G
- assume "rel_filter T F G"
- thus "filtermap Abs F = G" unfolding filter_eq_iff
- by(auto simp add: eventually_filtermap rel_filter_eventually * rel_funI del: iffI elim!: rel_funD)
-next
- from Q have *: "\<And>x. T (Rep x) x" unfolding Quotient_alt_def by blast
-
- fix F
- show "rel_filter T (filtermap Rep F) F"
- by(auto elim: rel_funD intro: * intro!: ext arg_cong[where f="\<lambda>P. eventually P F"] rel_funI
- del: iffI simp add: eventually_filtermap rel_filter_eventually)
-qed(auto simp add: map_fun_def o_def eventually_filtermap filter_eq_iff fun_eq_iff rel_filter_eventually
- fun_quotient[OF fun_quotient[OF Q identity_quotient] identity_quotient, unfolded Quotient_alt_def])
-
-lemma eventually_parametric [transfer_rule]:
- "((A ===> op =) ===> rel_filter A ===> op =) eventually eventually"
-by(simp add: rel_fun_def rel_filter_eventually)
-
-lemma rel_filter_eq [relator_eq]: "rel_filter op = = op ="
-by(auto simp add: rel_filter_eventually rel_fun_eq fun_eq_iff filter_eq_iff)
-
-lemma rel_filter_mono [relator_mono]:
- "A \<le> B \<Longrightarrow> rel_filter A \<le> rel_filter B"
-unfolding rel_filter_eventually[abs_def]
-by(rule le_funI)+(intro fun_mono fun_mono[THEN le_funD, THEN le_funD] order.refl)
-
-lemma rel_filter_conversep [simp]: "rel_filter A\<inverse>\<inverse> = (rel_filter A)\<inverse>\<inverse>"
-by(auto simp add: rel_filter_eventually fun_eq_iff rel_fun_def)
-
-lemma is_filter_parametric_aux:
- assumes "is_filter F"
- assumes [transfer_rule]: "bi_total A" "bi_unique A"
- and [transfer_rule]: "((A ===> op =) ===> op =) F G"
- shows "is_filter G"
-proof -
- interpret is_filter F by fact
- show ?thesis
- proof
- have "F (\<lambda>_. True) = G (\<lambda>x. True)" by transfer_prover
- thus "G (\<lambda>x. True)" by(simp add: True)
- next
- fix P' Q'
- assume "G P'" "G Q'"
- moreover
- from bi_total_fun[OF `bi_unique A` bi_total_eq, unfolded bi_total_def]
- obtain P Q where [transfer_rule]: "(A ===> op =) P P'" "(A ===> op =) Q Q'" by blast
- have "F P = G P'" "F Q = G Q'" by transfer_prover+
- ultimately have "F (\<lambda>x. P x \<and> Q x)" by(simp add: conj)
- moreover have "F (\<lambda>x. P x \<and> Q x) = G (\<lambda>x. P' x \<and> Q' x)" by transfer_prover
- ultimately show "G (\<lambda>x. P' x \<and> Q' x)" by simp
- next
- fix P' Q'
- assume "\<forall>x. P' x \<longrightarrow> Q' x" "G P'"
- moreover
- from bi_total_fun[OF `bi_unique A` bi_total_eq, unfolded bi_total_def]
- obtain P Q where [transfer_rule]: "(A ===> op =) P P'" "(A ===> op =) Q Q'" by blast
- have "F P = G P'" by transfer_prover
- moreover have "(\<forall>x. P x \<longrightarrow> Q x) \<longleftrightarrow> (\<forall>x. P' x \<longrightarrow> Q' x)" by transfer_prover
- ultimately have "F Q" by(simp add: mono)
- moreover have "F Q = G Q'" by transfer_prover
- ultimately show "G Q'" by simp
- qed
-qed
-
-lemma is_filter_parametric [transfer_rule]:
- "\<lbrakk> bi_total A; bi_unique A \<rbrakk>
- \<Longrightarrow> (((A ===> op =) ===> op =) ===> op =) is_filter is_filter"
-apply(rule rel_funI)
-apply(rule iffI)
- apply(erule (3) is_filter_parametric_aux)
-apply(erule is_filter_parametric_aux[where A="conversep A"])
-apply(auto simp add: rel_fun_def)
-done
-
-lemma left_total_rel_filter [transfer_rule]:
- assumes [transfer_rule]: "bi_total A" "bi_unique A"
- shows "left_total (rel_filter A)"
-proof(rule left_totalI)
- fix F :: "'a filter"
- from bi_total_fun[OF bi_unique_fun[OF `bi_total A` bi_unique_eq] bi_total_eq]
- obtain G where [transfer_rule]: "((A ===> op =) ===> op =) (\<lambda>P. eventually P F) G"
- unfolding bi_total_def by blast
- moreover have "is_filter (\<lambda>P. eventually P F) \<longleftrightarrow> is_filter G" by transfer_prover
- hence "is_filter G" by(simp add: eventually_def is_filter_Rep_filter)
- ultimately have "rel_filter A F (Abs_filter G)"
- by(simp add: rel_filter_eventually eventually_Abs_filter)
- thus "\<exists>G. rel_filter A F G" ..
-qed
-
-lemma right_total_rel_filter [transfer_rule]:
- "\<lbrakk> bi_total A; bi_unique A \<rbrakk> \<Longrightarrow> right_total (rel_filter A)"
-using left_total_rel_filter[of "A\<inverse>\<inverse>"] by simp
-
-lemma bi_total_rel_filter [transfer_rule]:
- assumes "bi_total A" "bi_unique A"
- shows "bi_total (rel_filter A)"
-unfolding bi_total_alt_def using assms
-by(simp add: left_total_rel_filter right_total_rel_filter)
-
-lemma left_unique_rel_filter [transfer_rule]:
- assumes "left_unique A"
- shows "left_unique (rel_filter A)"
-proof(rule left_uniqueI)
- fix F F' G
- assume [transfer_rule]: "rel_filter A F G" "rel_filter A F' G"
- show "F = F'"
- unfolding filter_eq_iff
- proof
- fix P :: "'a \<Rightarrow> bool"
- obtain P' where [transfer_rule]: "(A ===> op =) P P'"
- using left_total_fun[OF assms left_total_eq] unfolding left_total_def by blast
- have "eventually P F = eventually P' G"
- and "eventually P F' = eventually P' G" by transfer_prover+
- thus "eventually P F = eventually P F'" by simp
- qed
-qed
-
-lemma right_unique_rel_filter [transfer_rule]:
- "right_unique A \<Longrightarrow> right_unique (rel_filter A)"
-using left_unique_rel_filter[of "A\<inverse>\<inverse>"] by simp
-
-lemma bi_unique_rel_filter [transfer_rule]:
- "bi_unique A \<Longrightarrow> bi_unique (rel_filter A)"
-by(simp add: bi_unique_alt_def left_unique_rel_filter right_unique_rel_filter)
-
-lemma top_filter_parametric [transfer_rule]:
- "bi_total A \<Longrightarrow> (rel_filter A) top top"
-by(simp add: rel_filter_eventually All_transfer)
-
-lemma bot_filter_parametric [transfer_rule]: "(rel_filter A) bot bot"
-by(simp add: rel_filter_eventually rel_fun_def)
-
-lemma sup_filter_parametric [transfer_rule]:
- "(rel_filter A ===> rel_filter A ===> rel_filter A) sup sup"
-by(fastforce simp add: rel_filter_eventually[abs_def] eventually_sup dest: rel_funD)
-
-lemma Sup_filter_parametric [transfer_rule]:
- "(rel_set (rel_filter A) ===> rel_filter A) Sup Sup"
-proof(rule rel_funI)
- fix S T
- assume [transfer_rule]: "rel_set (rel_filter A) S T"
- show "rel_filter A (Sup S) (Sup T)"
- by(simp add: rel_filter_eventually eventually_Sup) transfer_prover
-qed
-
-lemma principal_parametric [transfer_rule]:
- "(rel_set A ===> rel_filter A) principal principal"
-proof(rule rel_funI)
- fix S S'
- assume [transfer_rule]: "rel_set A S S'"
- show "rel_filter A (principal S) (principal S')"
- by(simp add: rel_filter_eventually eventually_principal) transfer_prover
-qed
-
-context
- fixes A :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
- assumes [transfer_rule]: "bi_unique A"
-begin
-
-lemma le_filter_parametric [transfer_rule]:
- "(rel_filter A ===> rel_filter A ===> op =) op \<le> op \<le>"
-unfolding le_filter_def[abs_def] by transfer_prover
-
-lemma less_filter_parametric [transfer_rule]:
- "(rel_filter A ===> rel_filter A ===> op =) op < op <"
-unfolding less_filter_def[abs_def] by transfer_prover
-
-context
- assumes [transfer_rule]: "bi_total A"
-begin
-
-lemma Inf_filter_parametric [transfer_rule]:
- "(rel_set (rel_filter A) ===> rel_filter A) Inf Inf"
-unfolding Inf_filter_def[abs_def] by transfer_prover
-
-lemma inf_filter_parametric [transfer_rule]:
- "(rel_filter A ===> rel_filter A ===> rel_filter A) inf inf"
-proof(intro rel_funI)+
- fix F F' G G'
- assume [transfer_rule]: "rel_filter A F F'" "rel_filter A G G'"
- have "rel_filter A (Inf {F, G}) (Inf {F', G'})" by transfer_prover
- thus "rel_filter A (inf F G) (inf F' G')" by simp
-qed
-
end
-
-end
-
-end
-
-end
--- a/src/HOL/Transcendental.thy Sun Apr 12 20:05:35 2015 +0200
+++ b/src/HOL/Transcendental.thy Mon Apr 13 00:59:17 2015 +0200
@@ -2321,7 +2321,7 @@
shows "\<lbrakk>(f ---> a) F; (g ---> b) F; a \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x powr g x) ---> a powr b) F"
apply (simp add: powr_def)
apply (simp add: tendsto_def)
- apply (simp add: Topological_Spaces.eventually_conj_iff )
+ apply (simp add: eventually_conj_iff )
apply safe
apply (case_tac "0 \<in> S")
apply (auto simp: )
@@ -5201,7 +5201,7 @@
then have wnz: "\<And>w. w \<noteq> 0 \<Longrightarrow> (\<Sum>i\<le>n. c (Suc i) * w^i) = 0"
using Suc by auto
then have "(\<lambda>h. \<Sum>i\<le>n. c (Suc i) * h^i) -- 0 --> 0"
- by (simp cong: LIM_cong) --{*the case @{term"w=0"} by continuity}*}
+ by (simp cong: LIM_cong) --{*the case @{term"w=0"} by continuity*}
then have "(\<Sum>i\<le>n. c (Suc i) * 0^i) = 0"
using isCont_polynom [of 0 "\<lambda>i. c (Suc i)" n] LIM_unique
by (force simp add: Limits.isCont_iff)