add frequently as dual for eventually
authorhoelzl
Sun Apr 12 11:33:44 2015 +0200 (2015-04-12)
changeset 60038ca431cbce2a3
parent 60037 071a99649dde
child 60039 d55937a8f97e
add frequently as dual for eventually
src/HOL/Filter.thy
     1.1 --- a/src/HOL/Filter.thy	Sun Apr 12 11:33:30 2015 +0200
     1.2 +++ b/src/HOL/Filter.thy	Sun Apr 12 11:33:44 2015 +0200
     1.3 @@ -39,14 +39,11 @@
     1.4  definition eventually :: "('a \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> bool"
     1.5    where "eventually P F \<longleftrightarrow> Rep_filter F P"
     1.6  
     1.7 -syntax
     1.8 -  "_eventually"  :: "pttrn => 'a filter => bool => bool"      ("(3ALL _ in _./ _)" [0, 0, 10] 10)
     1.9 -
    1.10  syntax (xsymbols)
    1.11 -  "_eventually"  :: "pttrn => 'a filter => bool => bool"      ("(3\<forall>_ in _./ _)" [0, 0, 10] 10)
    1.12 +  "_eventually"  :: "pttrn => 'a filter => bool => bool"      ("(3\<forall>\<^sub>F _ in _./ _)" [0, 0, 10] 10)
    1.13  
    1.14  translations
    1.15 -  "\<forall>x in F. P" == "CONST eventually (%x. P) F"
    1.16 +  "\<forall>\<^sub>Fx in F. P" == "CONST eventually (\<lambda>x. P) F"
    1.17  
    1.18  lemma eventually_Abs_filter:
    1.19    assumes "is_filter F" shows "eventually P (Abs_filter F) = F P"
    1.20 @@ -157,6 +154,53 @@
    1.21    Scan.succeed (fn ctxt => METHOD_CASES (HEADGOAL o eventually_elim_tac ctxt))
    1.22  *} "elimination of eventually quantifiers"
    1.23  
    1.24 +subsection \<open> Frequently as dual to eventually \<close>
    1.25 +
    1.26 +definition frequently :: "('a \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> bool"
    1.27 +  where "frequently P F \<longleftrightarrow> \<not> eventually (\<lambda>x. \<not> P x) F"
    1.28 +
    1.29 +syntax (xsymbols)
    1.30 +  "_frequently"  :: "pttrn \<Rightarrow> 'a filter \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<exists>\<^sub>F _ in _./ _)" [0, 0, 10] 10)
    1.31 +
    1.32 +translations
    1.33 +  "\<exists>\<^sub>Fx in F. P" == "CONST frequently (\<lambda>x. P) F"
    1.34 +
    1.35 +lemma not_frequently_False [simp]: "\<not> frequently (\<lambda>x. False) F"
    1.36 +  by (simp add: frequently_def)
    1.37 +
    1.38 +lemma frequently_ex: "frequently P F \<Longrightarrow> \<exists>x. P x"
    1.39 +  by (auto simp: frequently_def dest: not_eventuallyD)
    1.40 +
    1.41 +lemma frequently_mp:
    1.42 +  assumes ev: "eventually (\<lambda>x. P x \<longrightarrow> Q x) F" and P: "frequently (\<lambda>x. P x) F"
    1.43 +  shows "frequently (\<lambda>x. Q x) F"
    1.44 +proof - 
    1.45 +  from ev have "eventually (\<lambda>x. \<not> Q x \<longrightarrow> \<not> P x) F"
    1.46 +    by (rule eventually_rev_mp) (auto intro!: always_eventually)
    1.47 +  from eventually_mp[OF this] P show ?thesis
    1.48 +    by (auto simp: frequently_def)
    1.49 +qed
    1.50 +
    1.51 +lemma frequently_rev_mp:
    1.52 +  assumes "frequently (\<lambda>x. P x) F"
    1.53 +  assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
    1.54 +  shows "frequently (\<lambda>x. Q x) F"
    1.55 +using assms(2) assms(1) by (rule frequently_mp)
    1.56 +
    1.57 +lemma frequently_mono: "(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> frequently P F \<Longrightarrow> frequently Q F"
    1.58 +  using frequently_mp[of P Q] by (simp add: always_eventually)
    1.59 +
    1.60 +lemma frequently_disj_iff:
    1.61 +  "frequently (\<lambda>x. P x \<or> Q x) F \<longleftrightarrow> frequently (\<lambda>x. P x) F \<or> frequently (\<lambda>x. Q x) F"
    1.62 +  by (simp add: frequently_def eventually_conj_iff)
    1.63 +
    1.64 +lemma frequently_disj:
    1.65 +  "frequently (\<lambda>x. P x) F \<Longrightarrow> frequently (\<lambda>x. Q x) F \<Longrightarrow> frequently (\<lambda>x. P x \<or> Q x) F"
    1.66 +  by (simp add: frequently_disj_iff)
    1.67 +
    1.68 +lemma frequently_Bex_finite:
    1.69 +  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)"
    1.70 +  using assms by induction (auto simp: frequently_disj_iff)
    1.71  
    1.72  subsubsection {* Finer-than relation *}
    1.73  
    1.74 @@ -800,6 +844,10 @@
    1.75    "((A ===> op =) ===> rel_filter A ===> op =) eventually eventually"
    1.76  by(simp add: rel_fun_def rel_filter_eventually)
    1.77  
    1.78 +lemma frequently_parametric [transfer_rule]:
    1.79 +  "((A ===> op =) ===> rel_filter A ===> op =) frequently frequently"
    1.80 +  unfolding frequently_def[abs_def] by transfer_prover
    1.81 +
    1.82  lemma rel_filter_eq [relator_eq]: "rel_filter op = = op ="
    1.83  by(auto simp add: rel_filter_eventually rel_fun_eq fun_eq_iff filter_eq_iff)
    1.84