summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | hoelzl |

Sun, 12 Apr 2015 11:33:44 +0200 | |

changeset 60038 | ca431cbce2a3 |

parent 60037 | 071a99649dde |

child 60039 | d55937a8f97e |

add frequently as dual for eventually

--- a/src/HOL/Filter.thy Sun Apr 12 11:33:30 2015 +0200 +++ b/src/HOL/Filter.thy Sun Apr 12 11:33:44 2015 +0200 @@ -39,14 +39,11 @@ definition eventually :: "('a \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> bool" where "eventually P F \<longleftrightarrow> Rep_filter F P" -syntax - "_eventually" :: "pttrn => 'a filter => bool => bool" ("(3ALL _ in _./ _)" [0, 0, 10] 10) - syntax (xsymbols) - "_eventually" :: "pttrn => 'a filter => bool => bool" ("(3\<forall>_ in _./ _)" [0, 0, 10] 10) + "_eventually" :: "pttrn => 'a filter => bool => bool" ("(3\<forall>\<^sub>F _ in _./ _)" [0, 0, 10] 10) translations - "\<forall>x in F. P" == "CONST eventually (%x. P) F" + "\<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" @@ -157,6 +154,53 @@ Scan.succeed (fn ctxt => METHOD_CASES (HEADGOAL o eventually_elim_tac ctxt)) *} "elimination of eventually quantifiers" +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> frequently (\<lambda>x. False) F" + by (simp add: frequently_def) + +lemma frequently_ex: "frequently P F \<Longrightarrow> \<exists>x. P x" + by (auto simp: frequently_def dest: not_eventuallyD) + +lemma frequently_mp: + assumes ev: "eventually (\<lambda>x. P x \<longrightarrow> Q x) F" and P: "frequently (\<lambda>x. P x) F" + shows "frequently (\<lambda>x. Q x) F" +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 "frequently (\<lambda>x. P x) F" + assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) F" + shows "frequently (\<lambda>x. Q x) F" +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_disj_iff: + "frequently (\<lambda>x. P x \<or> Q x) F \<longleftrightarrow> frequently (\<lambda>x. P x) F \<or> frequently (\<lambda>x. Q x) F" + by (simp add: frequently_def eventually_conj_iff) + +lemma frequently_disj: + "frequently (\<lambda>x. P x) F \<Longrightarrow> frequently (\<lambda>x. Q x) F \<Longrightarrow> frequently (\<lambda>x. P x \<or> Q x) F" + by (simp add: frequently_disj_iff) + +lemma frequently_Bex_finite: + assumes "finite A" shows "frequently (\<lambda>x. \<exists>y\<in>A. P x y) net \<longleftrightarrow> (\<exists>y\<in>A. frequently (\<lambda>x. P x y) net)" + using assms by induction (auto simp: frequently_disj_iff) subsubsection {* Finer-than relation *} @@ -800,6 +844,10 @@ "((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)