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