src/HOLCF/Eventual.thy
 author haftmann Fri Jun 19 21:08:07 2009 +0200 (2009-06-19) changeset 31726 ffd2dc631d88 parent 27408 22a515a55bf5 child 35771 2b75230f272f permissions -rw-r--r--
merged
```     1 theory Eventual
```
```     2 imports Infinite_Set
```
```     3 begin
```
```     4
```
```     5 subsection {* Lemmas about MOST *}
```
```     6
```
```     7 lemma MOST_INFM:
```
```     8   assumes inf: "infinite (UNIV::'a set)"
```
```     9   shows "MOST x::'a. P x \<Longrightarrow> INFM x::'a. P x"
```
```    10   unfolding Alm_all_def Inf_many_def
```
```    11   apply (auto simp add: Collect_neg_eq)
```
```    12   apply (drule (1) finite_UnI)
```
```    13   apply (simp add: Compl_partition2 inf)
```
```    14   done
```
```    15
```
```    16 lemma MOST_comp: "\<lbrakk>inj f; MOST x. P x\<rbrakk> \<Longrightarrow> MOST x. P (f x)"
```
```    17 unfolding MOST_iff_finiteNeg
```
```    18 by (drule (1) finite_vimageI, simp)
```
```    19
```
```    20 lemma INFM_comp: "\<lbrakk>inj f; INFM x. P (f x)\<rbrakk> \<Longrightarrow> INFM x. P x"
```
```    21 unfolding Inf_many_def
```
```    22 by (clarify, drule (1) finite_vimageI, simp)
```
```    23
```
```    24 lemma MOST_SucI: "MOST n. P n \<Longrightarrow> MOST n. P (Suc n)"
```
```    25 by (rule MOST_comp [OF inj_Suc])
```
```    26
```
```    27 lemma MOST_SucD: "MOST n. P (Suc n) \<Longrightarrow> MOST n. P n"
```
```    28 unfolding MOST_nat
```
```    29 apply (clarify, rule_tac x="Suc m" in exI, clarify)
```
```    30 apply (erule Suc_lessE, simp)
```
```    31 done
```
```    32
```
```    33 lemma MOST_Suc_iff: "(MOST n. P (Suc n)) \<longleftrightarrow> (MOST n. P n)"
```
```    34 by (rule iffI [OF MOST_SucD MOST_SucI])
```
```    35
```
```    36 lemma INFM_finite_Bex_distrib:
```
```    37   "finite A \<Longrightarrow> (INFM y. \<exists>x\<in>A. P x y) \<longleftrightarrow> (\<exists>x\<in>A. INFM y. P x y)"
```
```    38 by (induct set: finite, simp, simp add: INFM_disj_distrib)
```
```    39
```
```    40 lemma MOST_finite_Ball_distrib:
```
```    41   "finite A \<Longrightarrow> (MOST y. \<forall>x\<in>A. P x y) \<longleftrightarrow> (\<forall>x\<in>A. MOST y. P x y)"
```
```    42 by (induct set: finite, simp, simp add: MOST_conj_distrib)
```
```    43
```
```    44 lemma MOST_ge_nat: "MOST n::nat. m \<le> n"
```
```    45 unfolding MOST_nat_le by fast
```
```    46
```
```    47 subsection {* Eventually constant sequences *}
```
```    48
```
```    49 definition
```
```    50   eventually_constant :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool"
```
```    51 where
```
```    52   "eventually_constant S = (\<exists>x. MOST i. S i = x)"
```
```    53
```
```    54 lemma eventually_constant_MOST_MOST:
```
```    55   "eventually_constant S \<longleftrightarrow> (MOST m. MOST n. S n = S m)"
```
```    56 unfolding eventually_constant_def MOST_nat
```
```    57 apply safe
```
```    58 apply (rule_tac x=m in exI, clarify)
```
```    59 apply (rule_tac x=m in exI, clarify)
```
```    60 apply simp
```
```    61 apply fast
```
```    62 done
```
```    63
```
```    64 lemma eventually_constantI: "MOST i. S i = x \<Longrightarrow> eventually_constant S"
```
```    65 unfolding eventually_constant_def by fast
```
```    66
```
```    67 lemma eventually_constant_comp:
```
```    68   "eventually_constant (\<lambda>i. S i) \<Longrightarrow> eventually_constant (\<lambda>i. f (S i))"
```
```    69 unfolding eventually_constant_def
```
```    70 apply (erule exE, rule_tac x="f x" in exI)
```
```    71 apply (erule MOST_mono, simp)
```
```    72 done
```
```    73
```
```    74 lemma eventually_constant_Suc_iff:
```
```    75   "eventually_constant (\<lambda>i. S (Suc i)) \<longleftrightarrow> eventually_constant (\<lambda>i. S i)"
```
```    76 unfolding eventually_constant_def
```
```    77 by (subst MOST_Suc_iff, rule refl)
```
```    78
```
```    79 lemma eventually_constant_SucD:
```
```    80   "eventually_constant (\<lambda>i. S (Suc i)) \<Longrightarrow> eventually_constant (\<lambda>i. S i)"
```
```    81 by (rule eventually_constant_Suc_iff [THEN iffD1])
```
```    82
```
```    83 subsection {* Limits of eventually constant sequences *}
```
```    84
```
```    85 definition
```
```    86   eventual :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a" where
```
```    87   "eventual S = (THE x. MOST i. S i = x)"
```
```    88
```
```    89 lemma eventual_eqI: "MOST i. S i = x \<Longrightarrow> eventual S = x"
```
```    90 unfolding eventual_def
```
```    91 apply (rule the_equality, assumption)
```
```    92 apply (rename_tac y)
```
```    93 apply (subgoal_tac "MOST i::nat. y = x", simp)
```
```    94 apply (erule MOST_rev_mp)
```
```    95 apply (erule MOST_rev_mp)
```
```    96 apply simp
```
```    97 done
```
```    98
```
```    99 lemma MOST_eq_eventual:
```
```   100   "eventually_constant S \<Longrightarrow> MOST i. S i = eventual S"
```
```   101 unfolding eventually_constant_def
```
```   102 by (erule exE, simp add: eventual_eqI)
```
```   103
```
```   104 lemma eventual_mem_range:
```
```   105   "eventually_constant S \<Longrightarrow> eventual S \<in> range S"
```
```   106 apply (drule MOST_eq_eventual)
```
```   107 apply (simp only: MOST_nat_le, clarify)
```
```   108 apply (drule spec, drule mp, rule order_refl)
```
```   109 apply (erule range_eqI [OF sym])
```
```   110 done
```
```   111
```
```   112 lemma eventually_constant_MOST_iff:
```
```   113   assumes S: "eventually_constant S"
```
```   114   shows "(MOST n. P (S n)) \<longleftrightarrow> P (eventual S)"
```
```   115 apply (subgoal_tac "(MOST n. P (S n)) \<longleftrightarrow> (MOST n::nat. P (eventual S))")
```
```   116 apply simp
```
```   117 apply (rule iffI)
```
```   118 apply (rule MOST_rev_mp [OF MOST_eq_eventual [OF S]])
```
```   119 apply (erule MOST_mono, force)
```
```   120 apply (rule MOST_rev_mp [OF MOST_eq_eventual [OF S]])
```
```   121 apply (erule MOST_mono, simp)
```
```   122 done
```
```   123
```
```   124 lemma MOST_eventual:
```
```   125   "\<lbrakk>eventually_constant S; MOST n. P (S n)\<rbrakk> \<Longrightarrow> P (eventual S)"
```
```   126 proof -
```
```   127   assume "eventually_constant S"
```
```   128   hence "MOST n. S n = eventual S"
```
```   129     by (rule MOST_eq_eventual)
```
```   130   moreover assume "MOST n. P (S n)"
```
```   131   ultimately have "MOST n. S n = eventual S \<and> P (S n)"
```
```   132     by (rule MOST_conj_distrib [THEN iffD2, OF conjI])
```
```   133   hence "MOST n::nat. P (eventual S)"
```
```   134     by (rule MOST_mono) auto
```
```   135   thus ?thesis by simp
```
```   136 qed
```
```   137
```
```   138 lemma eventually_constant_MOST_Suc_eq:
```
```   139   "eventually_constant S \<Longrightarrow> MOST n. S (Suc n) = S n"
```
```   140 apply (drule MOST_eq_eventual)
```
```   141 apply (frule MOST_Suc_iff [THEN iffD2])
```
```   142 apply (erule MOST_rev_mp)
```
```   143 apply (erule MOST_rev_mp)
```
```   144 apply simp
```
```   145 done
```
```   146
```
```   147 lemma eventual_comp:
```
```   148   "eventually_constant S \<Longrightarrow> eventual (\<lambda>i. f (S i)) = f (eventual (\<lambda>i. S i))"
```
```   149 apply (rule eventual_eqI)
```
```   150 apply (rule MOST_mono)
```
```   151 apply (erule MOST_eq_eventual)
```
```   152 apply simp
```
```   153 done
```
```   154
```
```   155 end
```