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:
hoelzl@60036: "(\x. P x \ Q x) \ eventually P F \ eventually Q F"
hoelzl@60036: unfolding eventually_def
hoelzl@60036: by (rule is_filter.mono [OF is_filter_Rep_filter])
hoelzl@60036:
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"
hoelzl@60036: proof (rule eventually_mono)
hoelzl@60036: show "\x. (P x \ Q x) \ P x \ Q x" by simp
hoelzl@60036: show "eventually (\x. (P x \ Q x) \ P x) F"
hoelzl@60036: using assms by (rule eventually_conj)
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_elim1:
hoelzl@60036: assumes "eventually (\i. P i) F"
hoelzl@60036: assumes "\i. P i \ Q i"
hoelzl@60036: shows "eventually (\i. Q i) F"
hoelzl@60036: using assms by (auto 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)"
hoelzl@60040: by (auto intro: someI_ex eventually_elim1)
hoelzl@60040: then show "\Y. \\<^sub>Fx in F. P x (Y x)"
hoelzl@60040: by auto
hoelzl@60040: qed (auto intro: eventually_elim1)
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"
hoelzl@60036: by (auto elim: eventually_elim1)
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"
hoelzl@60040: 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:
hoelzl@60040: 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' \