hoelzl@60036: (* Title: HOL/Filter.thy hoelzl@60036: Author: Brian Huffman hoelzl@60036: Author: Johannes Hölzl hoelzl@60036: *) hoelzl@60036: wenzelm@60758: section \Filters on predicates\ hoelzl@60036: hoelzl@60036: theory Filter hoelzl@60036: imports Set_Interval Lifting_Set hoelzl@60036: begin hoelzl@60036: wenzelm@60758: subsection \Filters\ hoelzl@60036: wenzelm@60758: text \ hoelzl@60036: This definition also allows non-proper filters. wenzelm@60758: \ hoelzl@60036: hoelzl@60036: locale is_filter = hoelzl@60036: fixes F :: "('a \ bool) \ bool" hoelzl@60036: assumes True: "F (\x. True)" hoelzl@60036: assumes conj: "F (\x. P x) \ F (\x. Q x) \ F (\x. P x \ Q x)" hoelzl@60036: assumes mono: "\x. P x \ Q x \ F (\x. P x) \ F (\x. Q x)" hoelzl@60036: hoelzl@60036: typedef 'a filter = "{F :: ('a \ bool) \ bool. is_filter F}" hoelzl@60036: proof hoelzl@60036: show "(\x. True) \ ?filter" by (auto intro: is_filter.intro) hoelzl@60036: qed hoelzl@60036: hoelzl@60036: lemma is_filter_Rep_filter: "is_filter (Rep_filter F)" hoelzl@60036: using Rep_filter [of F] by simp hoelzl@60036: hoelzl@60036: lemma Abs_filter_inverse': hoelzl@60036: assumes "is_filter F" shows "Rep_filter (Abs_filter F) = F" hoelzl@60036: using assms by (simp add: Abs_filter_inverse) hoelzl@60036: hoelzl@60036: wenzelm@60758: subsubsection \Eventually\ hoelzl@60036: hoelzl@60036: definition eventually :: "('a \ bool) \ 'a filter \ bool" hoelzl@60036: where "eventually P F \ Rep_filter F P" hoelzl@60036: hoelzl@60037: syntax (xsymbols) hoelzl@60038: "_eventually" :: "pttrn => 'a filter => bool => bool" ("(3\\<^sub>F _ in _./ _)" [0, 0, 10] 10) hoelzl@60037: hoelzl@60037: translations hoelzl@60038: "\\<^sub>Fx in F. P" == "CONST eventually (\x. P) F" hoelzl@60037: hoelzl@60036: lemma eventually_Abs_filter: hoelzl@60036: assumes "is_filter F" shows "eventually P (Abs_filter F) = F P" hoelzl@60036: unfolding eventually_def using assms by (simp add: Abs_filter_inverse) hoelzl@60036: hoelzl@60036: lemma filter_eq_iff: hoelzl@60036: shows "F = F' \ (\P. eventually P F = eventually P F')" hoelzl@60036: unfolding Rep_filter_inject [symmetric] fun_eq_iff eventually_def .. hoelzl@60036: hoelzl@60036: lemma eventually_True [simp]: "eventually (\x. True) F" hoelzl@60036: unfolding eventually_def hoelzl@60036: by (rule is_filter.True [OF is_filter_Rep_filter]) hoelzl@60036: hoelzl@60036: lemma always_eventually: "\x. P x \ eventually P F" hoelzl@60036: proof - hoelzl@60036: assume "\x. P x" hence "P = (\x. True)" by (simp add: ext) hoelzl@60036: thus "eventually P F" by simp hoelzl@60036: qed hoelzl@60036: hoelzl@60040: lemma eventuallyI: "(\x. P x) \ eventually P F" hoelzl@60040: by (auto intro: always_eventually) hoelzl@60040: hoelzl@60036: lemma eventually_mono: lp15@61806: "\eventually P F; \x. P x \ Q x\ \ eventually Q F" lp15@61806: unfolding eventually_def lp15@61806: by (blast intro: is_filter.mono [OF is_filter_Rep_filter]) lp15@61806: hoelzl@60036: lemma eventually_conj: hoelzl@60036: assumes P: "eventually (\x. P x) F" hoelzl@60036: assumes Q: "eventually (\x. Q x) F" hoelzl@60036: shows "eventually (\x. P x \ Q x) F" hoelzl@60036: using assms unfolding eventually_def hoelzl@60036: by (rule is_filter.conj [OF is_filter_Rep_filter]) hoelzl@60036: hoelzl@60036: lemma eventually_mp: hoelzl@60036: assumes "eventually (\x. P x \ Q x) F" hoelzl@60036: assumes "eventually (\x. P x) F" hoelzl@60036: shows "eventually (\x. Q x) F" lp15@61806: proof - lp15@61806: have "eventually (\x. (P x \ Q x) \ P x) F" hoelzl@60036: using assms by (rule eventually_conj) lp15@61806: then show ?thesis lp15@61810: by (blast intro: eventually_mono) hoelzl@60036: qed hoelzl@60036: hoelzl@60036: lemma eventually_rev_mp: hoelzl@60036: assumes "eventually (\x. P x) F" hoelzl@60036: assumes "eventually (\x. P x \ Q x) F" hoelzl@60036: shows "eventually (\x. Q x) F" hoelzl@60036: using assms(2) assms(1) by (rule eventually_mp) hoelzl@60036: hoelzl@60036: lemma eventually_conj_iff: hoelzl@60036: "eventually (\x. P x \ Q x) F \ eventually P F \ eventually Q F" hoelzl@60036: by (auto intro: eventually_conj elim: eventually_rev_mp) hoelzl@60036: hoelzl@60036: lemma eventually_elim2: hoelzl@60036: assumes "eventually (\i. P i) F" hoelzl@60036: assumes "eventually (\i. Q i) F" hoelzl@60036: assumes "\i. P i \ Q i \ R i" hoelzl@60036: shows "eventually (\i. R i) F" hoelzl@60036: using assms by (auto elim!: eventually_rev_mp) hoelzl@60036: hoelzl@60040: lemma eventually_ball_finite_distrib: hoelzl@60040: "finite A \ (eventually (\x. \y\A. P x y) net) \ (\y\A. eventually (\x. P x y) net)" hoelzl@60040: by (induction A rule: finite_induct) (auto simp: eventually_conj_iff) hoelzl@60040: hoelzl@60040: lemma eventually_ball_finite: hoelzl@60040: "finite A \ \y\A. eventually (\x. P x y) net \ eventually (\x. \y\A. P x y) net" hoelzl@60040: by (auto simp: eventually_ball_finite_distrib) hoelzl@60040: hoelzl@60040: lemma eventually_all_finite: hoelzl@60040: fixes P :: "'a \ 'b::finite \ bool" hoelzl@60040: assumes "\y. eventually (\x. P x y) net" hoelzl@60040: shows "eventually (\x. \y. P x y) net" hoelzl@60040: using eventually_ball_finite [of UNIV P] assms by simp hoelzl@60040: hoelzl@60040: lemma eventually_ex: "(\\<^sub>Fx in F. \y. P x y) \ (\Y. \\<^sub>Fx in F. P x (Y x))" hoelzl@60040: proof hoelzl@60040: assume "\\<^sub>Fx in F. \y. P x y" hoelzl@60040: then have "\\<^sub>Fx in F. P x (SOME y. P x y)" lp15@61810: by (auto intro: someI_ex eventually_mono) hoelzl@60040: then show "\Y. \\<^sub>Fx in F. P x (Y x)" hoelzl@60040: by auto lp15@61810: qed (auto intro: eventually_mono) hoelzl@60040: hoelzl@60036: lemma not_eventually_impI: "eventually P F \ \ eventually Q F \ \ eventually (\x. P x \ Q x) F" hoelzl@60036: by (auto intro: eventually_mp) hoelzl@60036: hoelzl@60036: lemma not_eventuallyD: "\ eventually P F \ \x. \ P x" hoelzl@60036: by (metis always_eventually) hoelzl@60036: hoelzl@60036: lemma eventually_subst: hoelzl@60036: assumes "eventually (\n. P n = Q n) F" hoelzl@60036: shows "eventually P F = eventually Q F" (is "?L = ?R") hoelzl@60036: proof - hoelzl@60036: from assms have "eventually (\x. P x \ Q x) F" hoelzl@60036: and "eventually (\x. Q x \ P x) F" lp15@61810: by (auto elim: eventually_mono) hoelzl@60036: then show ?thesis by (auto elim: eventually_elim2) hoelzl@60036: qed hoelzl@60036: hoelzl@60040: subsection \ Frequently as dual to eventually \ hoelzl@60040: hoelzl@60040: definition frequently :: "('a \ bool) \ 'a filter \ bool" hoelzl@60040: where "frequently P F \ \ eventually (\x. \ P x) F" hoelzl@60040: hoelzl@60040: syntax (xsymbols) hoelzl@60040: "_frequently" :: "pttrn \ 'a filter \ bool \ bool" ("(3\\<^sub>F _ in _./ _)" [0, 0, 10] 10) hoelzl@60040: hoelzl@60040: translations hoelzl@60040: "\\<^sub>Fx in F. P" == "CONST frequently (\x. P) F" hoelzl@60040: hoelzl@60040: lemma not_frequently_False [simp]: "\ (\\<^sub>Fx in F. False)" hoelzl@60040: by (simp add: frequently_def) hoelzl@60040: hoelzl@60040: lemma frequently_ex: "\\<^sub>Fx in F. P x \ \x. P x" hoelzl@60040: by (auto simp: frequently_def dest: not_eventuallyD) hoelzl@60040: hoelzl@60040: lemma frequentlyE: assumes "frequently P F" obtains x where "P x" hoelzl@60040: using frequently_ex[OF assms] by auto hoelzl@60040: hoelzl@60040: lemma frequently_mp: hoelzl@60040: assumes ev: "\\<^sub>Fx in F. P x \ Q x" and P: "\\<^sub>Fx in F. P x" shows "\\<^sub>Fx in F. Q x" lp15@61806: proof - hoelzl@60040: from ev have "eventually (\x. \ Q x \ \ P x) F" hoelzl@60040: by (rule eventually_rev_mp) (auto intro!: always_eventually) hoelzl@60040: from eventually_mp[OF this] P show ?thesis hoelzl@60040: by (auto simp: frequently_def) hoelzl@60040: qed hoelzl@60040: hoelzl@60040: lemma frequently_rev_mp: hoelzl@60040: assumes "\\<^sub>Fx in F. P x" hoelzl@60040: assumes "\\<^sub>Fx in F. P x \ Q x" hoelzl@60040: shows "\\<^sub>Fx in F. Q x" hoelzl@60040: using assms(2) assms(1) by (rule frequently_mp) hoelzl@60040: hoelzl@60040: lemma frequently_mono: "(\x. P x \ Q x) \ frequently P F \ frequently Q F" hoelzl@60040: using frequently_mp[of P Q] by (simp add: always_eventually) hoelzl@60040: hoelzl@60040: lemma frequently_elim1: "\\<^sub>Fx in F. P x \ (\i. P i \ Q i) \ \\<^sub>Fx in F. Q x" hoelzl@60040: by (metis frequently_mono) hoelzl@60040: hoelzl@60040: lemma frequently_disj_iff: "(\\<^sub>Fx in F. P x \ Q x) \ (\\<^sub>Fx in F. P x) \ (\\<^sub>Fx in F. Q x)" hoelzl@60040: by (simp add: frequently_def eventually_conj_iff) hoelzl@60040: hoelzl@60040: lemma frequently_disj: "\\<^sub>Fx in F. P x \ \\<^sub>Fx in F. Q x \ \\<^sub>Fx in F. P x \ Q x" hoelzl@60040: by (simp add: frequently_disj_iff) hoelzl@60040: hoelzl@60040: lemma frequently_bex_finite_distrib: hoelzl@60040: assumes "finite A" shows "(\\<^sub>Fx in F. \y\A. P x y) \ (\y\A. \\<^sub>Fx in F. P x y)" hoelzl@60040: using assms by induction (auto simp: frequently_disj_iff) hoelzl@60040: hoelzl@60040: lemma frequently_bex_finite: "finite A \ \\<^sub>Fx in F. \y\A. P x y \ \y\A. \\<^sub>Fx in F. P x y" hoelzl@60040: by (simp add: frequently_bex_finite_distrib) hoelzl@60040: hoelzl@60040: lemma frequently_all: "(\\<^sub>Fx in F. \y. P x y) \ (\Y. \\<^sub>Fx in F. P x (Y x))" hoelzl@60040: using eventually_ex[of "\x y. \ P x y" F] by (simp add: frequently_def) hoelzl@60040: hoelzl@60040: lemma hoelzl@60040: shows not_eventually: "\ eventually P F \ (\\<^sub>Fx in F. \ P x)" hoelzl@60040: and not_frequently: "\ frequently P F \ (\\<^sub>Fx in F. \ P x)" hoelzl@60040: by (auto simp: frequently_def) hoelzl@60040: hoelzl@60040: lemma frequently_imp_iff: hoelzl@60040: "(\\<^sub>Fx in F. P x \ Q x) \ (eventually P F \ frequently Q F)" hoelzl@60040: unfolding imp_conv_disj frequently_disj_iff not_eventually[symmetric] .. hoelzl@60040: hoelzl@60040: lemma eventually_frequently_const_simps: hoelzl@60040: "(\\<^sub>Fx in F. P x \ C) \ (\\<^sub>Fx in F. P x) \ C" hoelzl@60040: "(\\<^sub>Fx in F. C \ P x) \ C \ (\\<^sub>Fx in F. P x)" hoelzl@60040: "(\\<^sub>Fx in F. P x \ C) \ (\\<^sub>Fx in F. P x) \ C" hoelzl@60040: "(\\<^sub>Fx in F. C \ P x) \ C \ (\\<^sub>Fx in F. P x)" hoelzl@60040: "(\\<^sub>Fx in F. P x \ C) \ ((\\<^sub>Fx in F. P x) \ C)" hoelzl@60040: "(\\<^sub>Fx in F. C \ P x) \ (C \ (\\<^sub>Fx in F. P x))" hoelzl@60040: by (cases C; simp add: not_frequently)+ hoelzl@60040: lp15@61806: lemmas eventually_frequently_simps = hoelzl@60040: eventually_frequently_const_simps hoelzl@60040: not_eventually hoelzl@60040: eventually_conj_iff hoelzl@60040: eventually_ball_finite_distrib hoelzl@60040: eventually_ex hoelzl@60040: not_frequently hoelzl@60040: frequently_disj_iff hoelzl@60040: frequently_bex_finite_distrib hoelzl@60040: frequently_all hoelzl@60040: frequently_imp_iff hoelzl@60040: wenzelm@60758: ML \ hoelzl@60036: fun eventually_elim_tac ctxt facts = SUBGOAL_CASES (fn (goal, i) => hoelzl@60036: let hoelzl@60036: val mp_thms = facts RL @{thms eventually_rev_mp} hoelzl@60036: val raw_elim_thm = hoelzl@60036: (@{thm allI} RS @{thm always_eventually}) hoelzl@60036: |> fold (fn thm1 => fn thm2 => thm2 RS thm1) mp_thms hoelzl@60036: |> fold (fn _ => fn thm => @{thm impI} RS thm) facts wenzelm@60589: val cases_prop = wenzelm@60589: Thm.prop_of wenzelm@60589: (Rule_Cases.internalize_params (raw_elim_thm RS Goal.init (Thm.cterm_of ctxt goal))) hoelzl@60036: val cases = Rule_Cases.make_common ctxt cases_prop [(("elim", []), [])] hoelzl@60036: in wenzelm@60752: CASES cases (resolve_tac ctxt [raw_elim_thm] i) hoelzl@60036: end) wenzelm@60758: \ hoelzl@60036: wenzelm@60758: method_setup eventually_elim = \ hoelzl@60036: Scan.succeed (fn ctxt => METHOD_CASES (HEADGOAL o eventually_elim_tac ctxt)) wenzelm@60758: \ "elimination of eventually quantifiers" hoelzl@60036: wenzelm@60758: subsubsection \Finer-than relation\ hoelzl@60036: wenzelm@60758: text \@{term "F \ F'"} means that filter @{term F} is finer than wenzelm@60758: filter @{term F'}.\ hoelzl@60036: hoelzl@60036: instantiation filter :: (type) complete_lattice hoelzl@60036: begin hoelzl@60036: hoelzl@60036: definition le_filter_def: hoelzl@60036: "F \ F' \ (\P. eventually P F' \ eventually P F)" hoelzl@60036: hoelzl@60036: definition hoelzl@60036: "(F :: 'a filter) < F' \ F \ F' \ \ F' \ F" hoelzl@60036: hoelzl@60036: definition hoelzl@60036: "top = Abs_filter (\P. \x. P x)" hoelzl@60036: hoelzl@60036: definition hoelzl@60036: "bot = Abs_filter (\P. True)" hoelzl@60036: hoelzl@60036: definition hoelzl@60036: "sup F F' = Abs_filter (\P. eventually P F \ eventually P F')" hoelzl@60036: hoelzl@60036: definition hoelzl@60036: "inf F F' = Abs_filter hoelzl@60036: (\P. \Q R. eventually Q F \ eventually R F' \ (\x. Q x \ R x \ P x))" hoelzl@60036: hoelzl@60036: definition hoelzl@60036: "Sup S = Abs_filter (\P. \F\S. eventually P F)" hoelzl@60036: hoelzl@60036: definition hoelzl@60036: "Inf S = Sup {F::'a filter. \F'\S. F \ F'}" hoelzl@60036: hoelzl@60036: lemma eventually_top [simp]: "eventually P top \ (\x. P x)" hoelzl@60036: unfolding top_filter_def hoelzl@60036: by (rule eventually_Abs_filter, rule is_filter.intro, auto) hoelzl@60036: hoelzl@60036: lemma eventually_bot [simp]: "eventually P bot" hoelzl@60036: unfolding bot_filter_def hoelzl@60036: by (subst eventually_Abs_filter, rule is_filter.intro, auto) hoelzl@60036: hoelzl@60036: lemma eventually_sup: hoelzl@60036: "eventually P (sup F F') \ eventually P F \ eventually P F'" hoelzl@60036: unfolding sup_filter_def hoelzl@60036: by (rule eventually_Abs_filter, rule is_filter.intro) hoelzl@60036: (auto elim!: eventually_rev_mp) hoelzl@60036: hoelzl@60036: lemma eventually_inf: hoelzl@60036: "eventually P (inf F F') \ hoelzl@60036: (\Q R. eventually Q F \ eventually R F' \ (\x. Q x \ R x \ P x))" hoelzl@60036: unfolding inf_filter_def hoelzl@60036: apply (rule eventually_Abs_filter, rule is_filter.intro) hoelzl@60036: apply (fast intro: eventually_True) hoelzl@60036: apply clarify hoelzl@60036: apply (intro exI conjI) hoelzl@60036: apply (erule (1) eventually_conj) hoelzl@60036: apply (erule (1) eventually_conj) hoelzl@60036: apply simp hoelzl@60036: apply auto hoelzl@60036: done hoelzl@60036: hoelzl@60036: lemma eventually_Sup: hoelzl@60036: "eventually P (Sup S) \ (\F\S. eventually P F)" hoelzl@60036: unfolding Sup_filter_def hoelzl@60036: apply (rule eventually_Abs_filter, rule is_filter.intro) hoelzl@60036: apply (auto intro: eventually_conj elim!: eventually_rev_mp) hoelzl@60036: done hoelzl@60036: hoelzl@60036: instance proof hoelzl@60036: fix F F' F'' :: "'a filter" and S :: "'a filter set" hoelzl@60036: { show "F < F' \ F \ F' \ \ F' \ F" hoelzl@60036: by (rule less_filter_def) } hoelzl@60036: { show "F \ F" hoelzl@60036: unfolding le_filter_def by simp } hoelzl@60036: { assume "F \ F'" and "F' \ F''" thus "F \ F''" hoelzl@60036: unfolding le_filter_def by simp } hoelzl@60036: { assume "F \ F'" and "F' \ F" thus "F = F'" hoelzl@60036: unfolding le_filter_def filter_eq_iff by fast } hoelzl@60036: { show "inf F F' \ F" and "inf F F' \ F'" hoelzl@60036: unfolding le_filter_def eventually_inf by (auto intro: eventually_True) } hoelzl@60036: { assume "F \ F'" and "F \ F''" thus "F \ inf F' F''" hoelzl@60036: unfolding le_filter_def eventually_inf lp15@61810: by (auto intro: eventually_mono [OF eventually_conj]) } hoelzl@60036: { show "F \ sup F F'" and "F' \ sup F F'" hoelzl@60036: unfolding le_filter_def eventually_sup by simp_all } hoelzl@60036: { assume "F \ F''" and "F' \ F''" thus "sup F F' \ F''" hoelzl@60036: unfolding le_filter_def eventually_sup by simp } hoelzl@60036: { assume "F'' \ S" thus "Inf S \ F''" hoelzl@60036: unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp } hoelzl@60036: { assume "\F'. F' \ S \ F \ F'" thus "F \ Inf S" hoelzl@60036: unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp } hoelzl@60036: { assume "F \ S" thus "F \ Sup S" hoelzl@60036: unfolding le_filter_def eventually_Sup by simp } hoelzl@60036: { assume "\F. F \ S \ F \ F'" thus "Sup S \ F'" hoelzl@60036: unfolding le_filter_def eventually_Sup by simp } hoelzl@60036: { show "Inf {} = (top::'a filter)" hoelzl@60036: by (auto simp: top_filter_def Inf_filter_def Sup_filter_def) hoelzl@60036: (metis (full_types) top_filter_def always_eventually eventually_top) } hoelzl@60036: { show "Sup {} = (bot::'a filter)" hoelzl@60036: by (auto simp: bot_filter_def Sup_filter_def) } hoelzl@60036: qed hoelzl@60036: hoelzl@60036: end hoelzl@60036: hoelzl@60036: lemma filter_leD: hoelzl@60036: "F \ F' \ eventually P F' \ eventually P F" hoelzl@60036: unfolding le_filter_def by simp hoelzl@60036: hoelzl@60036: lemma filter_leI: hoelzl@60036: "(\P. eventually P F' \ eventually P F) \ F \ F'" hoelzl@60036: unfolding le_filter_def by simp hoelzl@60036: hoelzl@60036: lemma eventually_False: hoelzl@60036: "eventually (\x. False) F \ F = bot" hoelzl@60036: unfolding filter_eq_iff by (auto elim: eventually_rev_mp) hoelzl@60036: hoelzl@60040: lemma eventually_frequently: "F \ bot \ eventually P F \ frequently P F" hoelzl@60040: using eventually_conj[of P F "\x. \ P x"] hoelzl@60040: by (auto simp add: frequently_def eventually_False) hoelzl@60040: hoelzl@60040: lemma eventually_const_iff: "eventually (\x. P) F \ P \ F = bot" hoelzl@60040: by (cases P) (auto simp: eventually_False) hoelzl@60040: hoelzl@60040: lemma eventually_const[simp]: "F \ bot \ eventually (\x. P) F \ P" hoelzl@60040: by (simp add: eventually_const_iff) hoelzl@60040: hoelzl@60040: lemma frequently_const_iff: "frequently (\x. P) F \ P \ F \ bot" hoelzl@60040: by (simp add: frequently_def eventually_const_iff) hoelzl@60040: hoelzl@60040: lemma frequently_const[simp]: "F \ bot \ frequently (\x. P) F \ P" hoelzl@60040: by (simp add: frequently_const_iff) hoelzl@60040: hoelzl@61245: lemma eventually_happens: "eventually P net \ net = bot \ (\x. P x)" hoelzl@61245: by (metis frequentlyE eventually_frequently) hoelzl@61245: eberlm@61531: lemma eventually_happens': eberlm@61531: assumes "F \ bot" "eventually P F" eberlm@61531: shows "\x. P x" eberlm@61531: using assms eventually_frequently frequentlyE by blast eberlm@61531: hoelzl@60036: abbreviation (input) trivial_limit :: "'a filter \ bool" hoelzl@60036: where "trivial_limit F \ F = bot" hoelzl@60036: hoelzl@60036: lemma trivial_limit_def: "trivial_limit F \ eventually (\x. False) F" hoelzl@60036: by (rule eventually_False [symmetric]) hoelzl@60036: lp15@61806: lemma False_imp_not_eventually: "(\x. \ P x ) \ \ trivial_limit net \ \ eventually (\x. P x) net" lp15@61806: by (simp add: eventually_False) lp15@61806: hoelzl@60036: lemma eventually_Inf: "eventually P (Inf B) \ (\X\B. finite X \ eventually P (Inf X))" hoelzl@60036: proof - hoelzl@60036: let ?F = "\P. \X\B. finite X \ eventually P (Inf X)" lp15@61806: hoelzl@60036: { fix P have "eventually P (Abs_filter ?F) \ ?F P" hoelzl@60036: proof (rule eventually_Abs_filter is_filter.intro)+ hoelzl@60036: show "?F (\x. True)" hoelzl@60036: by (rule exI[of _ "{}"]) (simp add: le_fun_def) hoelzl@60036: next hoelzl@60036: fix P Q hoelzl@60036: assume "?F P" then guess X .. hoelzl@60036: moreover hoelzl@60036: assume "?F Q" then guess Y .. hoelzl@60036: ultimately show "?F (\x. P x \ Q x)" hoelzl@60036: by (intro exI[of _ "X \ Y"]) hoelzl@60036: (auto simp: Inf_union_distrib eventually_inf) hoelzl@60036: next hoelzl@60036: fix P Q hoelzl@60036: assume "?F P" then guess X .. hoelzl@60036: moreover assume "\x. P x \ Q x" hoelzl@60036: ultimately show "?F Q" lp15@61810: by (intro exI[of _ X]) (auto elim: eventually_mono) hoelzl@60036: qed } hoelzl@60036: note eventually_F = this hoelzl@60036: hoelzl@60036: have "Inf B = Abs_filter ?F" hoelzl@60036: proof (intro antisym Inf_greatest) hoelzl@60036: show "Inf B \ Abs_filter ?F" hoelzl@60036: by (auto simp: le_filter_def eventually_F dest: Inf_superset_mono) hoelzl@60036: next hoelzl@60036: fix F assume "F \ B" then show "Abs_filter ?F \ F" hoelzl@60036: by (auto simp add: le_filter_def eventually_F intro!: exI[of _ "{F}"]) hoelzl@60036: qed hoelzl@60036: then show ?thesis hoelzl@60036: by (simp add: eventually_F) hoelzl@60036: qed hoelzl@60036: hoelzl@60036: lemma eventually_INF: "eventually P (INF b:B. F b) \ (\X\B. finite X \ eventually P (INF b:X. F b))" hoelzl@60036: unfolding INF_def[of B] eventually_Inf[of P "F`B"] hoelzl@60036: by (metis Inf_image_eq finite_imageI image_mono finite_subset_image) hoelzl@60036: hoelzl@60036: lemma Inf_filter_not_bot: hoelzl@60036: fixes B :: "'a filter set" hoelzl@60036: shows "(\X. X \ B \ finite X \ Inf X \ bot) \ Inf B \ bot" hoelzl@60036: unfolding trivial_limit_def eventually_Inf[of _ B] hoelzl@60036: bot_bool_def [symmetric] bot_fun_def [symmetric] bot_unique by simp hoelzl@60036: hoelzl@60036: lemma INF_filter_not_bot: hoelzl@60036: fixes F :: "'i \ 'a filter" hoelzl@60036: shows "(\X. X \ B \ finite X \ (INF b:X. F b) \ bot) \ (INF b:B. F b) \ bot" hoelzl@60036: unfolding trivial_limit_def eventually_INF[of _ B] hoelzl@60036: bot_bool_def [symmetric] bot_fun_def [symmetric] bot_unique by simp hoelzl@60036: hoelzl@60036: lemma eventually_Inf_base: hoelzl@60036: assumes "B \ {}" and base: "\F G. F \ B \ G \ B \ \x\B. x \ inf F G" hoelzl@60036: shows "eventually P (Inf B) \ (\b\B. eventually P b)" hoelzl@60036: proof (subst eventually_Inf, safe) hoelzl@60036: fix X assume "finite X" "X \ B" hoelzl@60036: then have "\b\B. \x\X. b \ x" hoelzl@60036: proof induct hoelzl@60036: case empty then show ?case wenzelm@60758: using \B \ {}\ by auto hoelzl@60036: next hoelzl@60036: case (insert x X) hoelzl@60036: then obtain b where "b \ B" "\x. x \ X \ b \ x" hoelzl@60036: by auto wenzelm@60758: with \insert x X \ B\ base[of b x] show ?case hoelzl@60036: by (auto intro: order_trans) hoelzl@60036: qed hoelzl@60036: then obtain b where "b \ B" "b \ Inf X" hoelzl@60036: by (auto simp: le_Inf_iff) hoelzl@60036: then show "eventually P (Inf X) \ Bex B (eventually P)" hoelzl@60036: by (intro bexI[of _ b]) (auto simp: le_filter_def) hoelzl@60036: qed (auto intro!: exI[of _ "{x}" for x]) hoelzl@60036: hoelzl@60036: lemma eventually_INF_base: hoelzl@60036: "B \ {} \ (\a b. a \ B \ b \ B \ \x\B. F x \ inf (F a) (F b)) \ hoelzl@60036: eventually P (INF b:B. F b) \ (\b\B. eventually P (F b))" hoelzl@60036: unfolding INF_def by (subst eventually_Inf_base) auto hoelzl@60036: hoelzl@60036: wenzelm@60758: subsubsection \Map function for filters\ hoelzl@60036: hoelzl@60036: definition filtermap :: "('a \ 'b) \ 'a filter \ 'b filter" hoelzl@60036: where "filtermap f F = Abs_filter (\P. eventually (\x. P (f x)) F)" hoelzl@60036: hoelzl@60036: lemma eventually_filtermap: hoelzl@60036: "eventually P (filtermap f F) = eventually (\x. P (f x)) F" hoelzl@60036: unfolding filtermap_def hoelzl@60036: apply (rule eventually_Abs_filter) hoelzl@60036: apply (rule is_filter.intro) hoelzl@60036: apply (auto elim!: eventually_rev_mp) hoelzl@60036: done hoelzl@60036: hoelzl@60036: lemma filtermap_ident: "filtermap (\x. x) F = F" hoelzl@60036: by (simp add: filter_eq_iff eventually_filtermap) hoelzl@60036: hoelzl@60036: lemma filtermap_filtermap: hoelzl@60036: "filtermap f (filtermap g F) = filtermap (\x. f (g x)) F" hoelzl@60036: by (simp add: filter_eq_iff eventually_filtermap) hoelzl@60036: hoelzl@60036: lemma filtermap_mono: "F \ F' \ filtermap f F \ filtermap f F'" hoelzl@60036: unfolding le_filter_def eventually_filtermap by simp hoelzl@60036: hoelzl@60036: lemma filtermap_bot [simp]: "filtermap f bot = bot" hoelzl@60036: by (simp add: filter_eq_iff eventually_filtermap) hoelzl@60036: hoelzl@60036: lemma filtermap_sup: "filtermap f (sup F1 F2) = sup (filtermap f F1) (filtermap f F2)" hoelzl@60036: by (auto simp: filter_eq_iff eventually_filtermap eventually_sup) hoelzl@60036: hoelzl@60036: lemma filtermap_inf: "filtermap f (inf F1 F2) \ inf (filtermap f F1) (filtermap f F2)" hoelzl@60036: by (auto simp: le_filter_def eventually_filtermap eventually_inf) hoelzl@60036: hoelzl@60036: lemma filtermap_INF: "filtermap f (INF b:B. F b) \ (INF b:B. filtermap f (F b))" hoelzl@60036: proof - hoelzl@60036: { fix X :: "'c set" assume "finite X" hoelzl@60036: then have "filtermap f (INFIMUM X F) \ (INF b:X. filtermap f (F b))" hoelzl@60036: proof induct hoelzl@60036: case (insert x X) hoelzl@60036: have "filtermap f (INF a:insert x X. F a) \ inf (filtermap f (F x)) (filtermap f (INF a:X. F a))" hoelzl@60036: by (rule order_trans[OF _ filtermap_inf]) simp hoelzl@60036: also have "\ \ inf (filtermap f (F x)) (INF a:X. filtermap f (F a))" hoelzl@60036: by (intro inf_mono insert order_refl) hoelzl@60036: finally show ?case hoelzl@60036: by simp hoelzl@60036: qed simp } hoelzl@60036: then show ?thesis hoelzl@60036: unfolding le_filter_def eventually_filtermap hoelzl@60036: by (subst (1 2) eventually_INF) auto hoelzl@60036: qed wenzelm@60758: subsubsection \Standard filters\ hoelzl@60036: hoelzl@60036: definition principal :: "'a set \ 'a filter" where hoelzl@60036: "principal S = Abs_filter (\P. \x\S. P x)" hoelzl@60036: hoelzl@60036: lemma eventually_principal: "eventually P (principal S) \ (\x\S. P x)" hoelzl@60036: unfolding principal_def hoelzl@60036: by (rule eventually_Abs_filter, rule is_filter.intro) auto hoelzl@60036: hoelzl@60036: lemma eventually_inf_principal: "eventually P (inf F (principal s)) \ eventually (\x. x \ s \ P x) F" lp15@61810: unfolding eventually_inf eventually_principal by (auto elim: eventually_mono) hoelzl@60036: hoelzl@60036: lemma principal_UNIV[simp]: "principal UNIV = top" hoelzl@60036: by (auto simp: filter_eq_iff eventually_principal) hoelzl@60036: hoelzl@60036: lemma principal_empty[simp]: "principal {} = bot" hoelzl@60036: by (auto simp: filter_eq_iff eventually_principal) hoelzl@60036: hoelzl@60036: lemma principal_eq_bot_iff: "principal X = bot \ X = {}" hoelzl@60036: by (auto simp add: filter_eq_iff eventually_principal) hoelzl@60036: hoelzl@60036: lemma principal_le_iff[iff]: "principal A \ principal B \ A \ B" hoelzl@60036: by (auto simp: le_filter_def eventually_principal) hoelzl@60036: hoelzl@60036: lemma le_principal: "F \ principal A \ eventually (\x. x \ A) F" hoelzl@60036: unfolding le_filter_def eventually_principal hoelzl@60036: apply safe hoelzl@60036: apply (erule_tac x="\x. x \ A" in allE) lp15@61810: apply (auto elim: eventually_mono) hoelzl@60036: done hoelzl@60036: hoelzl@60036: lemma principal_inject[iff]: "principal A = principal B \ A = B" hoelzl@60036: unfolding eq_iff by simp hoelzl@60036: hoelzl@60036: lemma sup_principal[simp]: "sup (principal A) (principal B) = principal (A \ B)" hoelzl@60036: unfolding filter_eq_iff eventually_sup eventually_principal by auto hoelzl@60036: hoelzl@60036: lemma inf_principal[simp]: "inf (principal A) (principal B) = principal (A \ B)" hoelzl@60036: unfolding filter_eq_iff eventually_inf eventually_principal hoelzl@60036: by (auto intro: exI[of _ "\x. x \ A"] exI[of _ "\x. x \ B"]) hoelzl@60036: hoelzl@60036: lemma SUP_principal[simp]: "(SUP i : I. principal (A i)) = principal (\i\I. A i)" hoelzl@60036: unfolding filter_eq_iff eventually_Sup SUP_def by (auto simp: eventually_principal) hoelzl@60036: hoelzl@60036: lemma INF_principal_finite: "finite X \ (INF x:X. principal (f x)) = principal (\x\X. f x)" hoelzl@60036: by (induct X rule: finite_induct) auto hoelzl@60036: hoelzl@60036: lemma filtermap_principal[simp]: "filtermap f (principal A) = principal (f ` A)" hoelzl@60036: unfolding filter_eq_iff eventually_filtermap eventually_principal by simp hoelzl@60036: wenzelm@60758: subsubsection \Order filters\ hoelzl@60036: hoelzl@60036: definition at_top :: "('a::order) filter" hoelzl@60036: where "at_top = (INF k. principal {k ..})" hoelzl@60036: hoelzl@60036: lemma at_top_sub: "at_top = (INF k:{c::'a::linorder..}. principal {k ..})" hoelzl@60036: by (auto intro!: INF_eq max.cobounded1 max.cobounded2 simp: at_top_def) hoelzl@60036: hoelzl@60036: lemma eventually_at_top_linorder: "eventually P at_top \ (\N::'a::linorder. \n\N. P n)" hoelzl@60036: unfolding at_top_def hoelzl@60036: by (subst eventually_INF_base) (auto simp: eventually_principal intro: max.cobounded1 max.cobounded2) hoelzl@60036: hoelzl@60036: lemma eventually_ge_at_top: hoelzl@60036: "eventually (\x. (c::_::linorder) \ x) at_top" hoelzl@60036: unfolding eventually_at_top_linorder by auto hoelzl@60036: hoelzl@60036: lemma eventually_at_top_dense: "eventually P at_top \ (\N::'a::{no_top, linorder}. \n>N. P n)" hoelzl@60036: proof - hoelzl@60036: have "eventually P (INF k. principal {k <..}) \ (\N::'a. \n>N. P n)" hoelzl@60036: by (subst eventually_INF_base) (auto simp: eventually_principal intro: max.cobounded1 max.cobounded2) hoelzl@60036: also have "(INF k. principal {k::'a <..}) = at_top" lp15@61806: unfolding at_top_def hoelzl@60036: by (intro INF_eq) (auto intro: less_imp_le simp: Ici_subset_Ioi_iff gt_ex) hoelzl@60036: finally show ?thesis . hoelzl@60036: qed hoelzl@60036: hoelzl@60721: lemma eventually_at_top_not_equal: "eventually (\x::'a::{no_top, linorder}. x \ c) at_top" hoelzl@60721: unfolding eventually_at_top_dense by auto hoelzl@60721: hoelzl@60721: lemma eventually_gt_at_top: "eventually (\x. (c::_::{no_top, linorder}) < x) at_top" hoelzl@60036: unfolding eventually_at_top_dense by auto hoelzl@60036: eberlm@61531: lemma eventually_all_ge_at_top: eberlm@61531: assumes "eventually P (at_top :: ('a :: linorder) filter)" eberlm@61531: shows "eventually (\x. \y\x. P y) at_top" eberlm@61531: proof - eberlm@61531: from assms obtain x where "\y. y \ x \ P y" by (auto simp: eventually_at_top_linorder) eberlm@61531: hence "\z\y. P z" if "y \ x" for y using that by simp eberlm@61531: thus ?thesis by (auto simp: eventually_at_top_linorder) eberlm@61531: qed eberlm@61531: hoelzl@60036: definition at_bot :: "('a::order) filter" hoelzl@60036: where "at_bot = (INF k. principal {.. k})" hoelzl@60036: hoelzl@60036: lemma at_bot_sub: "at_bot = (INF k:{.. c::'a::linorder}. principal {.. k})" hoelzl@60036: by (auto intro!: INF_eq min.cobounded1 min.cobounded2 simp: at_bot_def) hoelzl@60036: hoelzl@60036: lemma eventually_at_bot_linorder: hoelzl@60036: fixes P :: "'a::linorder \ bool" shows "eventually P at_bot \ (\N. \n\N. P n)" hoelzl@60036: unfolding at_bot_def hoelzl@60036: by (subst eventually_INF_base) (auto simp: eventually_principal intro: min.cobounded1 min.cobounded2) hoelzl@60036: hoelzl@60036: lemma eventually_le_at_bot: hoelzl@60036: "eventually (\x. x \ (c::_::linorder)) at_bot" hoelzl@60036: unfolding eventually_at_bot_linorder by auto hoelzl@60036: hoelzl@60036: lemma eventually_at_bot_dense: "eventually P at_bot \ (\N::'a::{no_bot, linorder}. \n (\N::'a. \nx::'a::{no_bot, linorder}. x \ c) at_bot" hoelzl@60721: unfolding eventually_at_bot_dense by auto hoelzl@60721: hoelzl@60036: lemma eventually_gt_at_bot: hoelzl@60036: "eventually (\x. x < (c::_::unbounded_dense_linorder)) at_bot" hoelzl@60036: unfolding eventually_at_bot_dense by auto hoelzl@60036: hoelzl@60036: lemma trivial_limit_at_bot_linorder: "\ trivial_limit (at_bot ::('a::linorder) filter)" hoelzl@60036: unfolding trivial_limit_def hoelzl@60036: by (metis eventually_at_bot_linorder order_refl) hoelzl@60036: hoelzl@60036: lemma trivial_limit_at_top_linorder: "\ trivial_limit (at_top ::('a::linorder) filter)" hoelzl@60036: unfolding trivial_limit_def hoelzl@60036: by (metis eventually_at_top_linorder order_refl) hoelzl@60036: wenzelm@60758: subsection \Sequentially\ hoelzl@60036: hoelzl@60036: abbreviation sequentially :: "nat filter" hoelzl@60036: where "sequentially \ at_top" hoelzl@60036: hoelzl@60036: lemma eventually_sequentially: hoelzl@60036: "eventually P sequentially \ (\N. \n\N. P n)" hoelzl@60036: by (rule eventually_at_top_linorder) hoelzl@60036: hoelzl@60036: lemma sequentially_bot [simp, intro]: "sequentially \ bot" hoelzl@60036: unfolding filter_eq_iff eventually_sequentially by auto hoelzl@60036: hoelzl@60036: lemmas trivial_limit_sequentially = sequentially_bot hoelzl@60036: hoelzl@60036: lemma eventually_False_sequentially [simp]: hoelzl@60036: "\ eventually (\n. False) sequentially" hoelzl@60036: by (simp add: eventually_False) hoelzl@60036: hoelzl@60036: lemma le_sequentially: hoelzl@60036: "F \ sequentially \ (\N. eventually (\n. N \ n) F)" hoelzl@60036: by (simp add: at_top_def le_INF_iff le_principal) hoelzl@60036: lp15@60974: lemma eventually_sequentiallyI [intro?]: hoelzl@60036: assumes "\x. c \ x \ P x" hoelzl@60036: shows "eventually P sequentially" hoelzl@60036: using assms by (auto simp: eventually_sequentially) hoelzl@60036: hoelzl@60040: lemma eventually_sequentially_Suc: "eventually (\i. P (Suc i)) sequentially \ eventually P sequentially" hoelzl@60040: unfolding eventually_sequentially by (metis Suc_le_D Suc_le_mono le_Suc_eq) hoelzl@60040: hoelzl@60040: lemma eventually_sequentially_seg: "eventually (\n. P (n + k)) sequentially \ eventually P sequentially" hoelzl@60040: using eventually_sequentially_Suc[of "\n. P (n + k)" for k] by (induction k) auto hoelzl@60036: hoelzl@60039: subsection \ The cofinite filter \ hoelzl@60039: hoelzl@60039: definition "cofinite = Abs_filter (\P. finite {x. \ P x})" hoelzl@60039: hoelzl@60040: abbreviation Inf_many :: "('a \ bool) \ bool" (binder "INFM " 10) where hoelzl@60040: "Inf_many P \ frequently P cofinite" hoelzl@60040: hoelzl@60040: abbreviation Alm_all :: "('a \ bool) \ bool" (binder "MOST " 10) where hoelzl@60040: "Alm_all P \ eventually P cofinite" hoelzl@60040: hoelzl@60040: notation (xsymbols) hoelzl@60040: Inf_many (binder "\\<^sub>\" 10) and hoelzl@60040: Alm_all (binder "\\<^sub>\" 10) hoelzl@60040: hoelzl@60039: lemma eventually_cofinite: "eventually P cofinite \ finite {x. \ P x}" hoelzl@60039: unfolding cofinite_def hoelzl@60039: proof (rule eventually_Abs_filter, rule is_filter.intro) hoelzl@60039: fix P Q :: "'a \ bool" assume "finite {x. \ P x}" "finite {x. \ Q x}" hoelzl@60039: from finite_UnI[OF this] show "finite {x. \ (P x \ Q x)}" hoelzl@60039: by (rule rev_finite_subset) auto hoelzl@60039: next hoelzl@60039: fix P Q :: "'a \ bool" assume P: "finite {x. \ P x}" and *: "\x. P x \ Q x" hoelzl@60039: from * show "finite {x. \ Q x}" hoelzl@60039: by (intro finite_subset[OF _ P]) auto hoelzl@60039: qed simp hoelzl@60039: hoelzl@60040: lemma frequently_cofinite: "frequently P cofinite \ \ finite {x. P x}" hoelzl@60040: by (simp add: frequently_def eventually_cofinite) hoelzl@60040: hoelzl@60039: lemma cofinite_bot[simp]: "cofinite = (bot::'a filter) \ finite (UNIV :: 'a set)" hoelzl@60039: unfolding trivial_limit_def eventually_cofinite by simp hoelzl@60039: hoelzl@60039: lemma cofinite_eq_sequentially: "cofinite = sequentially" hoelzl@60039: unfolding filter_eq_iff eventually_sequentially eventually_cofinite hoelzl@60039: proof safe hoelzl@60039: fix P :: "nat \ bool" assume [simp]: "finite {x. \ P x}" hoelzl@60039: show "\N. \n\N. P n" hoelzl@60039: proof cases hoelzl@60039: assume "{x. \ P x} \ {}" then show ?thesis hoelzl@60039: by (intro exI[of _ "Suc (Max {x. \ P x})"]) (auto simp: Suc_le_eq) hoelzl@60039: qed auto hoelzl@60039: next hoelzl@60039: fix P :: "nat \ bool" and N :: nat assume "\n\N. P n" hoelzl@60039: then have "{x. \ P x} \ {..< N}" hoelzl@60039: by (auto simp: not_le) hoelzl@60039: then show "finite {x. \ P x}" hoelzl@60039: by (blast intro: finite_subset) hoelzl@60039: qed hoelzl@60036: wenzelm@60758: subsection \Limits\ hoelzl@60036: hoelzl@60036: definition filterlim :: "('a \ 'b) \ 'b filter \ 'a filter \ bool" where hoelzl@60036: "filterlim f F2 F1 \ filtermap f F1 \ F2" hoelzl@60036: hoelzl@60036: syntax hoelzl@60036: "_LIM" :: "pttrns \ 'a \ 'b \ 'a \ bool" ("(3LIM (_)/ (_)./ (_) :> (_))" [1000, 10, 0, 10] 10) hoelzl@60036: hoelzl@60036: translations hoelzl@60036: "LIM x F1. f :> F2" == "CONST filterlim (%x. f) F2 F1" hoelzl@60036: hoelzl@60036: lemma filterlim_iff: hoelzl@60036: "(LIM x F1. f x :> F2) \ (\P. eventually P F2 \ eventually (\x. P (f x)) F1)" hoelzl@60036: unfolding filterlim_def le_filter_def eventually_filtermap .. hoelzl@60036: hoelzl@60036: lemma filterlim_compose: hoelzl@60036: "filterlim g F3 F2 \ filterlim f F2 F1 \ filterlim (\x. g (f x)) F3 F1" hoelzl@60036: unfolding filterlim_def filtermap_filtermap[symmetric] by (metis filtermap_mono order_trans) hoelzl@60036: hoelzl@60036: lemma filterlim_mono: hoelzl@60036: "filterlim f F2 F1 \ F2 \ F2' \ F1' \ F1 \ filterlim f F2' F1'" hoelzl@60036: unfolding filterlim_def by (metis filtermap_mono order_trans) hoelzl@60036: hoelzl@60036: lemma filterlim_ident: "LIM x F. x :> F" hoelzl@60036: by (simp add: filterlim_def filtermap_ident) hoelzl@60036: hoelzl@60036: lemma filterlim_cong: hoelzl@60036: "F1 = F1' \ F2 = F2' \ eventually (\x. f x = g x) F2 \ filterlim f F1 F2 = filterlim g F1' F2'" hoelzl@60036: by (auto simp: filterlim_def le_filter_def eventually_filtermap elim: eventually_elim2) hoelzl@60036: hoelzl@60036: lemma filterlim_mono_eventually: hoelzl@60036: assumes "filterlim f F G" and ord: "F \ F'" "G' \ G" hoelzl@60036: assumes eq: "eventually (\x. f x = f' x) G'" hoelzl@60036: shows "filterlim f' F' G'" hoelzl@60036: apply (rule filterlim_cong[OF refl refl eq, THEN iffD1]) hoelzl@60036: apply (rule filterlim_mono[OF _ ord]) hoelzl@60036: apply fact hoelzl@60036: done hoelzl@60036: hoelzl@60036: lemma filtermap_mono_strong: "inj f \ filtermap f F \ filtermap f G \ F \ G" hoelzl@60036: apply (auto intro!: filtermap_mono) [] hoelzl@60036: apply (auto simp: le_filter_def eventually_filtermap) hoelzl@60036: apply (erule_tac x="\x. P (inv f x)" in allE) hoelzl@60036: apply auto hoelzl@60036: done hoelzl@60036: hoelzl@60036: lemma filtermap_eq_strong: "inj f \ filtermap f F = filtermap f G \ F = G" hoelzl@60036: by (simp add: filtermap_mono_strong eq_iff) hoelzl@60036: hoelzl@60721: lemma filtermap_fun_inverse: hoelzl@60721: assumes g: "filterlim g F G" hoelzl@60721: assumes f: "filterlim f G F" hoelzl@60721: assumes ev: "eventually (\x. f (g x) = x) G" hoelzl@60721: shows "filtermap f F = G" hoelzl@60721: proof (rule antisym) hoelzl@60721: show "filtermap f F \ G" hoelzl@60721: using f unfolding filterlim_def . hoelzl@60721: have "G = filtermap f (filtermap g G)" hoelzl@60721: using ev by (auto elim: eventually_elim2 simp: filter_eq_iff eventually_filtermap) hoelzl@60721: also have "\ \ filtermap f F" hoelzl@60721: using g by (intro filtermap_mono) (simp add: filterlim_def) hoelzl@60721: finally show "G \ filtermap f F" . hoelzl@60721: qed hoelzl@60721: hoelzl@60036: lemma filterlim_principal: hoelzl@60036: "(LIM x F. f x :> principal S) \ (eventually (\x. f x \ S) F)" hoelzl@60036: unfolding filterlim_def eventually_filtermap le_principal .. hoelzl@60036: hoelzl@60036: lemma filterlim_inf: hoelzl@60036: "(LIM x F1. f x :> inf F2 F3) \ ((LIM x F1. f x :> F2) \ (LIM x F1. f x :> F3))" hoelzl@60036: unfolding filterlim_def by simp hoelzl@60036: hoelzl@60036: lemma filterlim_INF: hoelzl@60036: "(LIM x F. f x :> (INF b:B. G b)) \ (\b\B. LIM x F. f x :> G b)" hoelzl@60036: unfolding filterlim_def le_INF_iff .. hoelzl@60036: hoelzl@60036: lemma filterlim_INF_INF: hoelzl@60036: "(\m. m \ J \ \i\I. filtermap f (F i) \ G m) \ LIM x (INF i:I. F i). f x :> (INF j:J. G j)" hoelzl@60036: unfolding filterlim_def by (rule order_trans[OF filtermap_INF INF_mono]) hoelzl@60036: hoelzl@60036: lemma filterlim_base: lp15@61806: "(\m x. m \ J \ i m \ I) \ (\m x. m \ J \ x \ F (i m) \ f x \ G m) \ hoelzl@60036: LIM x (INF i:I. principal (F i)). f x :> (INF j:J. principal (G j))" hoelzl@60036: by (force intro!: filterlim_INF_INF simp: image_subset_iff) hoelzl@60036: lp15@61806: lemma filterlim_base_iff: hoelzl@60036: assumes "I \ {}" and chain: "\i j. i \ I \ j \ I \ F i \ F j \ F j \ F i" hoelzl@60036: shows "(LIM x (INF i:I. principal (F i)). f x :> INF j:J. principal (G j)) \ hoelzl@60036: (\j\J. \i\I. \x\F i. f x \ G j)" hoelzl@60036: unfolding filterlim_INF filterlim_principal hoelzl@60036: proof (subst eventually_INF_base) hoelzl@60036: fix i j assume "i \ I" "j \ I" hoelzl@60036: with chain[OF this] show "\x\I. principal (F x) \ inf (principal (F i)) (principal (F j))" hoelzl@60036: by auto wenzelm@60758: qed (auto simp: eventually_principal \I \ {}\) hoelzl@60036: hoelzl@60036: lemma filterlim_filtermap: "filterlim f F1 (filtermap g F2) = filterlim (\x. f (g x)) F1 F2" hoelzl@60036: unfolding filterlim_def filtermap_filtermap .. hoelzl@60036: hoelzl@60036: lemma filterlim_sup: hoelzl@60036: "filterlim f F F1 \ filterlim f F F2 \ filterlim f F (sup F1 F2)" hoelzl@60036: unfolding filterlim_def filtermap_sup by auto hoelzl@60036: hoelzl@60036: lemma filterlim_sequentially_Suc: hoelzl@60036: "(LIM x sequentially. f (Suc x) :> F) \ (LIM x sequentially. f x :> F)" hoelzl@60036: unfolding filterlim_iff by (subst eventually_sequentially_Suc) simp hoelzl@60036: hoelzl@60036: lemma filterlim_Suc: "filterlim Suc sequentially sequentially" hoelzl@60036: by (simp add: filterlim_iff eventually_sequentially) (metis le_Suc_eq) hoelzl@60036: hoelzl@60182: lemma filterlim_If: hoelzl@60182: "LIM x inf F (principal {x. P x}). f x :> G \ hoelzl@60182: LIM x inf F (principal {x. \ P x}). g x :> G \ hoelzl@60182: LIM x F. if P x then f x else g x :> G" hoelzl@60182: unfolding filterlim_iff eventually_inf_principal by (auto simp: eventually_conj_iff) hoelzl@60036: wenzelm@60758: subsection \Limits to @{const at_top} and @{const at_bot}\ hoelzl@60036: hoelzl@60036: lemma filterlim_at_top: hoelzl@60036: fixes f :: "'a \ ('b::linorder)" hoelzl@60036: shows "(LIM x F. f x :> at_top) \ (\Z. eventually (\x. Z \ f x) F)" lp15@61810: by (auto simp: filterlim_iff eventually_at_top_linorder elim!: eventually_mono) hoelzl@60036: hoelzl@60036: lemma filterlim_at_top_mono: hoelzl@60036: "LIM x F. f x :> at_top \ eventually (\x. f x \ (g x::'a::linorder)) F \ hoelzl@60036: LIM x F. g x :> at_top" hoelzl@60036: by (auto simp: filterlim_at_top elim: eventually_elim2 intro: order_trans) hoelzl@60036: hoelzl@60036: lemma filterlim_at_top_dense: hoelzl@60036: fixes f :: "'a \ ('b::unbounded_dense_linorder)" hoelzl@60036: shows "(LIM x F. f x :> at_top) \ (\Z. eventually (\x. Z < f x) F)" lp15@61810: by (metis eventually_mono[of _ F] eventually_gt_at_top order_less_imp_le hoelzl@60036: filterlim_at_top[of f F] filterlim_iff[of f at_top F]) hoelzl@60036: hoelzl@60036: lemma filterlim_at_top_ge: hoelzl@60036: fixes f :: "'a \ ('b::linorder)" and c :: "'b" hoelzl@60036: shows "(LIM x F. f x :> at_top) \ (\Z\c. eventually (\x. Z \ f x) F)" hoelzl@60036: unfolding at_top_sub[of c] filterlim_INF by (auto simp add: filterlim_principal) hoelzl@60036: hoelzl@60036: lemma filterlim_at_top_at_top: hoelzl@60036: fixes f :: "'a::linorder \ 'b::linorder" hoelzl@60036: assumes mono: "\x y. Q x \ Q y \ x \ y \ f x \ f y" hoelzl@60036: assumes bij: "\x. P x \ f (g x) = x" "\x. P x \ Q (g x)" hoelzl@60036: assumes Q: "eventually Q at_top" hoelzl@60036: assumes P: "eventually P at_top" hoelzl@60036: shows "filterlim f at_top at_top" hoelzl@60036: proof - hoelzl@60036: from P obtain x where x: "\y. x \ y \ P y" hoelzl@60036: unfolding eventually_at_top_linorder by auto hoelzl@60036: show ?thesis hoelzl@60036: proof (intro filterlim_at_top_ge[THEN iffD2] allI impI) hoelzl@60036: fix z assume "x \ z" hoelzl@60036: with x have "P z" by auto hoelzl@60036: have "eventually (\x. g z \ x) at_top" hoelzl@60036: by (rule eventually_ge_at_top) hoelzl@60036: with Q show "eventually (\x. z \ f x) at_top" wenzelm@60758: by eventually_elim (metis mono bij \P z\) hoelzl@60036: qed hoelzl@60036: qed hoelzl@60036: hoelzl@60036: lemma filterlim_at_top_gt: hoelzl@60036: fixes f :: "'a \ ('b::unbounded_dense_linorder)" and c :: "'b" hoelzl@60036: shows "(LIM x F. f x :> at_top) \ (\Z>c. eventually (\x. Z \ f x) F)" hoelzl@60036: by (metis filterlim_at_top order_less_le_trans gt_ex filterlim_at_top_ge) hoelzl@60036: lp15@61806: lemma filterlim_at_bot: hoelzl@60036: fixes f :: "'a \ ('b::linorder)" hoelzl@60036: shows "(LIM x F. f x :> at_bot) \ (\Z. eventually (\x. f x \ Z) F)" lp15@61810: by (auto simp: filterlim_iff eventually_at_bot_linorder elim!: eventually_mono) hoelzl@60036: hoelzl@60036: lemma filterlim_at_bot_dense: hoelzl@60036: fixes f :: "'a \ ('b::{dense_linorder, no_bot})" hoelzl@60036: shows "(LIM x F. f x :> at_bot) \ (\Z. eventually (\x. f x < Z) F)" hoelzl@60036: proof (auto simp add: filterlim_at_bot[of f F]) hoelzl@60036: fix Z :: 'b hoelzl@60036: from lt_ex [of Z] obtain Z' where 1: "Z' < Z" .. hoelzl@60036: assume "\Z. eventually (\x. f x \ Z) F" hoelzl@60036: hence "eventually (\x. f x \ Z') F" by auto hoelzl@60036: thus "eventually (\x. f x < Z) F" lp15@61810: apply (rule eventually_mono) hoelzl@60036: using 1 by auto lp15@61806: next lp15@61806: fix Z :: 'b hoelzl@60036: show "\Z. eventually (\x. f x < Z) F \ eventually (\x. f x \ Z) F" lp15@61810: by (drule spec [of _ Z], erule eventually_mono, auto simp add: less_imp_le) hoelzl@60036: qed hoelzl@60036: hoelzl@60036: lemma filterlim_at_bot_le: hoelzl@60036: fixes f :: "'a \ ('b::linorder)" and c :: "'b" hoelzl@60036: shows "(LIM x F. f x :> at_bot) \ (\Z\c. eventually (\x. Z \ f x) F)" hoelzl@60036: unfolding filterlim_at_bot hoelzl@60036: proof safe hoelzl@60036: fix Z assume *: "\Z\c. eventually (\x. Z \ f x) F" hoelzl@60036: with *[THEN spec, of "min Z c"] show "eventually (\x. Z \ f x) F" lp15@61810: by (auto elim!: eventually_mono) hoelzl@60036: qed simp hoelzl@60036: hoelzl@60036: lemma filterlim_at_bot_lt: hoelzl@60036: fixes f :: "'a \ ('b::unbounded_dense_linorder)" and c :: "'b" hoelzl@60036: shows "(LIM x F. f x :> at_bot) \ (\Zx. Z \ f x) F)" hoelzl@60036: by (metis filterlim_at_bot filterlim_at_bot_le lt_ex order_le_less_trans) hoelzl@60036: hoelzl@60036: wenzelm@60758: subsection \Setup @{typ "'a filter"} for lifting and transfer\ hoelzl@60036: hoelzl@60036: context begin interpretation lifting_syntax . hoelzl@60036: hoelzl@60036: definition rel_filter :: "('a \ 'b \ bool) \ 'a filter \ 'b filter \ bool" hoelzl@60036: where "rel_filter R F G = ((R ===> op =) ===> op =) (Rep_filter F) (Rep_filter G)" hoelzl@60036: hoelzl@60036: lemma rel_filter_eventually: lp15@61806: "rel_filter R F G \ hoelzl@60036: ((R ===> op =) ===> op =) (\P. eventually P F) (\P. eventually P G)" hoelzl@60036: by(simp add: rel_filter_def eventually_def) hoelzl@60036: hoelzl@60036: lemma filtermap_id [simp, id_simps]: "filtermap id = id" hoelzl@60036: by(simp add: fun_eq_iff id_def filtermap_ident) hoelzl@60036: hoelzl@60036: lemma filtermap_id' [simp]: "filtermap (\x. x) = (\F. F)" hoelzl@60036: using filtermap_id unfolding id_def . hoelzl@60036: hoelzl@60036: lemma Quotient_filter [quot_map]: hoelzl@60036: assumes Q: "Quotient R Abs Rep T" hoelzl@60036: shows "Quotient (rel_filter R) (filtermap Abs) (filtermap Rep) (rel_filter T)" hoelzl@60036: unfolding Quotient_alt_def hoelzl@60036: proof(intro conjI strip) hoelzl@60036: from Q have *: "\x y. T x y \ Abs x = y" hoelzl@60036: unfolding Quotient_alt_def by blast hoelzl@60036: hoelzl@60036: fix F G hoelzl@60036: assume "rel_filter T F G" hoelzl@60036: thus "filtermap Abs F = G" unfolding filter_eq_iff hoelzl@60036: by(auto simp add: eventually_filtermap rel_filter_eventually * rel_funI del: iffI elim!: rel_funD) hoelzl@60036: next hoelzl@60036: from Q have *: "\x. T (Rep x) x" unfolding Quotient_alt_def by blast hoelzl@60036: hoelzl@60036: fix F lp15@61806: show "rel_filter T (filtermap Rep F) F" hoelzl@60036: by(auto elim: rel_funD intro: * intro!: ext arg_cong[where f="\P. eventually P F"] rel_funI hoelzl@60036: del: iffI simp add: eventually_filtermap rel_filter_eventually) hoelzl@60036: qed(auto simp add: map_fun_def o_def eventually_filtermap filter_eq_iff fun_eq_iff rel_filter_eventually hoelzl@60036: fun_quotient[OF fun_quotient[OF Q identity_quotient] identity_quotient, unfolded Quotient_alt_def]) hoelzl@60036: hoelzl@60036: lemma eventually_parametric [transfer_rule]: hoelzl@60036: "((A ===> op =) ===> rel_filter A ===> op =) eventually eventually" hoelzl@60036: by(simp add: rel_fun_def rel_filter_eventually) hoelzl@60036: hoelzl@60038: lemma frequently_parametric [transfer_rule]: hoelzl@60038: "((A ===> op =) ===> rel_filter A ===> op =) frequently frequently" hoelzl@60038: unfolding frequently_def[abs_def] by transfer_prover hoelzl@60038: hoelzl@60036: lemma rel_filter_eq [relator_eq]: "rel_filter op = = op =" hoelzl@60036: by(auto simp add: rel_filter_eventually rel_fun_eq fun_eq_iff filter_eq_iff) hoelzl@60036: hoelzl@60036: lemma rel_filter_mono [relator_mono]: hoelzl@60036: "A \ B \ rel_filter A \ rel_filter B" hoelzl@60036: unfolding rel_filter_eventually[abs_def] hoelzl@60036: by(rule le_funI)+(intro fun_mono fun_mono[THEN le_funD, THEN le_funD] order.refl) hoelzl@60036: hoelzl@60036: lemma rel_filter_conversep [simp]: "rel_filter A\\ = (rel_filter A)\\" lp15@61233: apply (simp add: rel_filter_eventually fun_eq_iff rel_fun_def) lp15@61233: apply (safe; metis) lp15@61233: done hoelzl@60036: hoelzl@60036: lemma is_filter_parametric_aux: hoelzl@60036: assumes "is_filter F" hoelzl@60036: assumes [transfer_rule]: "bi_total A" "bi_unique A" hoelzl@60036: and [transfer_rule]: "((A ===> op =) ===> op =) F G" hoelzl@60036: shows "is_filter G" hoelzl@60036: proof - hoelzl@60036: interpret is_filter F by fact hoelzl@60036: show ?thesis hoelzl@60036: proof hoelzl@60036: have "F (\_. True) = G (\x. True)" by transfer_prover hoelzl@60036: thus "G (\x. True)" by(simp add: True) hoelzl@60036: next hoelzl@60036: fix P' Q' hoelzl@60036: assume "G P'" "G Q'" hoelzl@60036: moreover wenzelm@60758: from bi_total_fun[OF \bi_unique A\ bi_total_eq, unfolded bi_total_def] hoelzl@60036: obtain P Q where [transfer_rule]: "(A ===> op =) P P'" "(A ===> op =) Q Q'" by blast hoelzl@60036: have "F P = G P'" "F Q = G Q'" by transfer_prover+ hoelzl@60036: ultimately have "F (\x. P x \ Q x)" by(simp add: conj) hoelzl@60036: moreover have "F (\x. P x \ Q x) = G (\x. P' x \ Q' x)" by transfer_prover hoelzl@60036: ultimately show "G (\x. P' x \ Q' x)" by simp hoelzl@60036: next hoelzl@60036: fix P' Q' hoelzl@60036: assume "\x. P' x \ Q' x" "G P'" hoelzl@60036: moreover wenzelm@60758: from bi_total_fun[OF \bi_unique A\ bi_total_eq, unfolded bi_total_def] hoelzl@60036: obtain P Q where [transfer_rule]: "(A ===> op =) P P'" "(A ===> op =) Q Q'" by blast hoelzl@60036: have "F P = G P'" by transfer_prover hoelzl@60036: moreover have "(\x. P x \ Q x) \ (\x. P' x \ Q' x)" by transfer_prover hoelzl@60036: ultimately have "F Q" by(simp add: mono) hoelzl@60036: moreover have "F Q = G Q'" by transfer_prover hoelzl@60036: ultimately show "G Q'" by simp hoelzl@60036: qed hoelzl@60036: qed hoelzl@60036: hoelzl@60036: lemma is_filter_parametric [transfer_rule]: hoelzl@60036: "\ bi_total A; bi_unique A \ hoelzl@60036: \ (((A ===> op =) ===> op =) ===> op =) is_filter is_filter" hoelzl@60036: apply(rule rel_funI) hoelzl@60036: apply(rule iffI) hoelzl@60036: apply(erule (3) is_filter_parametric_aux) hoelzl@60036: apply(erule is_filter_parametric_aux[where A="conversep A"]) lp15@61233: apply (simp_all add: rel_fun_def) lp15@61233: apply metis hoelzl@60036: done hoelzl@60036: hoelzl@60036: lemma left_total_rel_filter [transfer_rule]: hoelzl@60036: assumes [transfer_rule]: "bi_total A" "bi_unique A" hoelzl@60036: shows "left_total (rel_filter A)" hoelzl@60036: proof(rule left_totalI) hoelzl@60036: fix F :: "'a filter" wenzelm@60758: from bi_total_fun[OF bi_unique_fun[OF \bi_total A\ bi_unique_eq] bi_total_eq] lp15@61806: obtain G where [transfer_rule]: "((A ===> op =) ===> op =) (\P. eventually P F) G" hoelzl@60036: unfolding bi_total_def by blast hoelzl@60036: moreover have "is_filter (\P. eventually P F) \ is_filter G" by transfer_prover hoelzl@60036: hence "is_filter G" by(simp add: eventually_def is_filter_Rep_filter) hoelzl@60036: ultimately have "rel_filter A F (Abs_filter G)" hoelzl@60036: by(simp add: rel_filter_eventually eventually_Abs_filter) hoelzl@60036: thus "\G. rel_filter A F G" .. hoelzl@60036: qed hoelzl@60036: hoelzl@60036: lemma right_total_rel_filter [transfer_rule]: hoelzl@60036: "\ bi_total A; bi_unique A \ \ right_total (rel_filter A)" hoelzl@60036: using left_total_rel_filter[of "A\\"] by simp hoelzl@60036: hoelzl@60036: lemma bi_total_rel_filter [transfer_rule]: hoelzl@60036: assumes "bi_total A" "bi_unique A" hoelzl@60036: shows "bi_total (rel_filter A)" hoelzl@60036: unfolding bi_total_alt_def using assms hoelzl@60036: by(simp add: left_total_rel_filter right_total_rel_filter) hoelzl@60036: hoelzl@60036: lemma left_unique_rel_filter [transfer_rule]: hoelzl@60036: assumes "left_unique A" hoelzl@60036: shows "left_unique (rel_filter A)" hoelzl@60036: proof(rule left_uniqueI) hoelzl@60036: fix F F' G hoelzl@60036: assume [transfer_rule]: "rel_filter A F G" "rel_filter A F' G" hoelzl@60036: show "F = F'" hoelzl@60036: unfolding filter_eq_iff hoelzl@60036: proof hoelzl@60036: fix P :: "'a \ bool" hoelzl@60036: obtain P' where [transfer_rule]: "(A ===> op =) P P'" hoelzl@60036: using left_total_fun[OF assms left_total_eq] unfolding left_total_def by blast lp15@61806: have "eventually P F = eventually P' G" hoelzl@60036: and "eventually P F' = eventually P' G" by transfer_prover+ hoelzl@60036: thus "eventually P F = eventually P F'" by simp hoelzl@60036: qed hoelzl@60036: qed hoelzl@60036: hoelzl@60036: lemma right_unique_rel_filter [transfer_rule]: hoelzl@60036: "right_unique A \ right_unique (rel_filter A)" hoelzl@60036: using left_unique_rel_filter[of "A\\"] by simp hoelzl@60036: hoelzl@60036: lemma bi_unique_rel_filter [transfer_rule]: hoelzl@60036: "bi_unique A \ bi_unique (rel_filter A)" hoelzl@60036: by(simp add: bi_unique_alt_def left_unique_rel_filter right_unique_rel_filter) hoelzl@60036: hoelzl@60036: lemma top_filter_parametric [transfer_rule]: hoelzl@60036: "bi_total A \ (rel_filter A) top top" hoelzl@60036: by(simp add: rel_filter_eventually All_transfer) hoelzl@60036: hoelzl@60036: lemma bot_filter_parametric [transfer_rule]: "(rel_filter A) bot bot" hoelzl@60036: by(simp add: rel_filter_eventually rel_fun_def) hoelzl@60036: hoelzl@60036: lemma sup_filter_parametric [transfer_rule]: hoelzl@60036: "(rel_filter A ===> rel_filter A ===> rel_filter A) sup sup" hoelzl@60036: by(fastforce simp add: rel_filter_eventually[abs_def] eventually_sup dest: rel_funD) hoelzl@60036: hoelzl@60036: lemma Sup_filter_parametric [transfer_rule]: hoelzl@60036: "(rel_set (rel_filter A) ===> rel_filter A) Sup Sup" hoelzl@60036: proof(rule rel_funI) hoelzl@60036: fix S T hoelzl@60036: assume [transfer_rule]: "rel_set (rel_filter A) S T" hoelzl@60036: show "rel_filter A (Sup S) (Sup T)" hoelzl@60036: by(simp add: rel_filter_eventually eventually_Sup) transfer_prover hoelzl@60036: qed hoelzl@60036: hoelzl@60036: lemma principal_parametric [transfer_rule]: hoelzl@60036: "(rel_set A ===> rel_filter A) principal principal" hoelzl@60036: proof(rule rel_funI) hoelzl@60036: fix S S' hoelzl@60036: assume [transfer_rule]: "rel_set A S S'" hoelzl@60036: show "rel_filter A (principal S) (principal S')" hoelzl@60036: by(simp add: rel_filter_eventually eventually_principal) transfer_prover hoelzl@60036: qed hoelzl@60036: hoelzl@60036: context hoelzl@60036: fixes A :: "'a \ 'b \ bool" lp15@61806: assumes [transfer_rule]: "bi_unique A" hoelzl@60036: begin hoelzl@60036: hoelzl@60036: lemma le_filter_parametric [transfer_rule]: hoelzl@60036: "(rel_filter A ===> rel_filter A ===> op =) op \ op \" hoelzl@60036: unfolding le_filter_def[abs_def] by transfer_prover hoelzl@60036: hoelzl@60036: lemma less_filter_parametric [transfer_rule]: hoelzl@60036: "(rel_filter A ===> rel_filter A ===> op =) op < op <" hoelzl@60036: unfolding less_filter_def[abs_def] by transfer_prover hoelzl@60036: hoelzl@60036: context hoelzl@60036: assumes [transfer_rule]: "bi_total A" hoelzl@60036: begin hoelzl@60036: hoelzl@60036: lemma Inf_filter_parametric [transfer_rule]: hoelzl@60036: "(rel_set (rel_filter A) ===> rel_filter A) Inf Inf" hoelzl@60036: unfolding Inf_filter_def[abs_def] by transfer_prover hoelzl@60036: hoelzl@60036: lemma inf_filter_parametric [transfer_rule]: hoelzl@60036: "(rel_filter A ===> rel_filter A ===> rel_filter A) inf inf" hoelzl@60036: proof(intro rel_funI)+ hoelzl@60036: fix F F' G G' hoelzl@60036: assume [transfer_rule]: "rel_filter A F F'" "rel_filter A G G'" hoelzl@60036: have "rel_filter A (Inf {F, G}) (Inf {F', G'})" by transfer_prover hoelzl@60036: thus "rel_filter A (inf F G) (inf F' G')" by simp hoelzl@60036: qed hoelzl@60036: hoelzl@60036: end hoelzl@60036: hoelzl@60036: end hoelzl@60036: hoelzl@60036: end hoelzl@60036: lp15@61806: end