1 (* Title: HOLCF/ex/Stream_adm.thy |
|
2 Author: David von Oheimb, TU Muenchen |
|
3 *) |
|
4 |
|
5 header {* Admissibility for streams *} |
|
6 |
|
7 theory Stream_adm |
|
8 imports Stream Continuity |
|
9 begin |
|
10 |
|
11 definition |
|
12 stream_monoP :: "(('a stream) set \<Rightarrow> ('a stream) set) \<Rightarrow> bool" where |
|
13 "stream_monoP F = (\<exists>Q i. \<forall>P s. Fin i \<le> #s \<longrightarrow> |
|
14 (s \<in> F P) = (stream_take i\<cdot>s \<in> Q \<and> iterate i\<cdot>rt\<cdot>s \<in> P))" |
|
15 |
|
16 definition |
|
17 stream_antiP :: "(('a stream) set \<Rightarrow> ('a stream) set) \<Rightarrow> bool" where |
|
18 "stream_antiP F = (\<forall>P x. \<exists>Q i. |
|
19 (#x < Fin i \<longrightarrow> (\<forall>y. x \<sqsubseteq> y \<longrightarrow> y \<in> F P \<longrightarrow> x \<in> F P)) \<and> |
|
20 (Fin i <= #x \<longrightarrow> (\<forall>y. x \<sqsubseteq> y \<longrightarrow> |
|
21 (y \<in> F P) = (stream_take i\<cdot>y \<in> Q \<and> iterate i\<cdot>rt\<cdot>y \<in> P))))" |
|
22 |
|
23 definition |
|
24 antitonP :: "'a set => bool" where |
|
25 "antitonP P = (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> y\<in>P \<longrightarrow> x\<in>P)" |
|
26 |
|
27 |
|
28 (* ----------------------------------------------------------------------- *) |
|
29 |
|
30 section "admissibility" |
|
31 |
|
32 lemma infinite_chain_adm_lemma: |
|
33 "\<lbrakk>Porder.chain Y; \<forall>i. P (Y i); |
|
34 \<And>Y. \<lbrakk>Porder.chain Y; \<forall>i. P (Y i); \<not> finite_chain Y\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)\<rbrakk> |
|
35 \<Longrightarrow> P (\<Squnion>i. Y i)" |
|
36 apply (case_tac "finite_chain Y") |
|
37 prefer 2 apply fast |
|
38 apply (unfold finite_chain_def) |
|
39 apply safe |
|
40 apply (erule lub_finch1 [THEN lub_eqI, THEN ssubst]) |
|
41 apply assumption |
|
42 apply (erule spec) |
|
43 done |
|
44 |
|
45 lemma increasing_chain_adm_lemma: |
|
46 "\<lbrakk>Porder.chain Y; \<forall>i. P (Y i); \<And>Y. \<lbrakk>Porder.chain Y; \<forall>i. P (Y i); |
|
47 \<forall>i. \<exists>j>i. Y i \<noteq> Y j \<and> Y i \<sqsubseteq> Y j\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)\<rbrakk> |
|
48 \<Longrightarrow> P (\<Squnion>i. Y i)" |
|
49 apply (erule infinite_chain_adm_lemma) |
|
50 apply assumption |
|
51 apply (erule thin_rl) |
|
52 apply (unfold finite_chain_def) |
|
53 apply (unfold max_in_chain_def) |
|
54 apply (fast dest: le_imp_less_or_eq elim: chain_mono_less) |
|
55 done |
|
56 |
|
57 lemma flatstream_adm_lemma: |
|
58 assumes 1: "Porder.chain Y" |
|
59 assumes 2: "!i. P (Y i)" |
|
60 assumes 3: "(!!Y. [| Porder.chain Y; !i. P (Y i); !k. ? j. Fin k < #((Y j)::'a::flat stream)|] |
|
61 ==> P(LUB i. Y i))" |
|
62 shows "P(LUB i. Y i)" |
|
63 apply (rule increasing_chain_adm_lemma [of _ P, OF 1 2]) |
|
64 apply (erule 3, assumption) |
|
65 apply (erule thin_rl) |
|
66 apply (rule allI) |
|
67 apply (case_tac "!j. stream_finite (Y j)") |
|
68 apply ( rule chain_incr) |
|
69 apply ( rule allI) |
|
70 apply ( drule spec) |
|
71 apply ( safe) |
|
72 apply ( rule exI) |
|
73 apply ( rule slen_strict_mono) |
|
74 apply ( erule spec) |
|
75 apply ( assumption) |
|
76 apply ( assumption) |
|
77 apply (metis inat_ord_code(4) slen_infinite) |
|
78 done |
|
79 |
|
80 (* should be without reference to stream length? *) |
|
81 lemma flatstream_admI: "[|(!!Y. [| Porder.chain Y; !i. P (Y i); |
|
82 !k. ? j. Fin k < #((Y j)::'a::flat stream)|] ==> P(LUB i. Y i))|]==> adm P" |
|
83 apply (unfold adm_def) |
|
84 apply (intro strip) |
|
85 apply (erule (1) flatstream_adm_lemma) |
|
86 apply (fast) |
|
87 done |
|
88 |
|
89 |
|
90 (* context (theory "Nat_InFinity");*) |
|
91 lemma ile_lemma: "Fin (i + j) <= x ==> Fin i <= x" |
|
92 by (rule order_trans) auto |
|
93 |
|
94 lemma stream_monoP2I: |
|
95 "!!X. stream_monoP F ==> !i. ? l. !x y. |
|
96 Fin l <= #x --> (x::'a::flat stream) << y --> x:down_iterate F i --> y:down_iterate F i" |
|
97 apply (unfold stream_monoP_def) |
|
98 apply (safe) |
|
99 apply (rule_tac x="i*ia" in exI) |
|
100 apply (induct_tac "ia") |
|
101 apply ( simp) |
|
102 apply (simp) |
|
103 apply (intro strip) |
|
104 apply (erule allE, erule all_dupE, drule mp, erule ile_lemma) |
|
105 apply (drule_tac P="%x. x" in subst, assumption) |
|
106 apply (erule allE, drule mp, rule ile_lemma) back |
|
107 apply ( erule order_trans) |
|
108 apply ( erule slen_mono) |
|
109 apply (erule ssubst) |
|
110 apply (safe) |
|
111 apply ( erule (2) ile_lemma [THEN slen_take_lemma3, THEN subst]) |
|
112 apply (erule allE) |
|
113 apply (drule mp) |
|
114 apply ( erule slen_rt_mult) |
|
115 apply (erule allE) |
|
116 apply (drule mp) |
|
117 apply (erule monofun_rt_mult) |
|
118 apply (drule (1) mp) |
|
119 apply (assumption) |
|
120 done |
|
121 |
|
122 lemma stream_monoP2_gfp_admI: "[| !i. ? l. !x y. |
|
123 Fin l <= #x --> (x::'a::flat stream) << y --> x:down_iterate F i --> y:down_iterate F i; |
|
124 down_cont F |] ==> adm (%x. x:gfp F)" |
|
125 apply (erule INTER_down_iterate_is_gfp [THEN ssubst]) (* cont *) |
|
126 apply (simp (no_asm)) |
|
127 apply (rule adm_lemmas) |
|
128 apply (rule flatstream_admI) |
|
129 apply (erule allE) |
|
130 apply (erule exE) |
|
131 apply (erule allE, erule exE) |
|
132 apply (erule allE, erule allE, drule mp) (* stream_monoP *) |
|
133 apply ( drule ileI1) |
|
134 apply ( drule order_trans) |
|
135 apply ( rule ile_iSuc) |
|
136 apply ( drule iSuc_ile_mono [THEN iffD1]) |
|
137 apply ( assumption) |
|
138 apply (drule mp) |
|
139 apply ( erule is_ub_thelub) |
|
140 apply (fast) |
|
141 done |
|
142 |
|
143 lemmas fstream_gfp_admI = stream_monoP2I [THEN stream_monoP2_gfp_admI] |
|
144 |
|
145 lemma stream_antiP2I: |
|
146 "!!X. [|stream_antiP (F::(('a::flat stream)set => ('a stream set)))|] |
|
147 ==> !i x y. x << y --> y:down_iterate F i --> x:down_iterate F i" |
|
148 apply (unfold stream_antiP_def) |
|
149 apply (rule allI) |
|
150 apply (induct_tac "i") |
|
151 apply ( simp) |
|
152 apply (simp) |
|
153 apply (intro strip) |
|
154 apply (erule allE, erule all_dupE, erule exE, erule exE) |
|
155 apply (erule conjE) |
|
156 apply (case_tac "#x < Fin i") |
|
157 apply ( fast) |
|
158 apply (unfold linorder_not_less) |
|
159 apply (drule (1) mp) |
|
160 apply (erule all_dupE, drule mp, rule below_refl) |
|
161 apply (erule ssubst) |
|
162 apply (erule allE, drule (1) mp) |
|
163 apply (drule_tac P="%x. x" in subst, assumption) |
|
164 apply (erule conjE, rule conjI) |
|
165 apply ( erule slen_take_lemma3 [THEN ssubst], assumption) |
|
166 apply ( assumption) |
|
167 apply (erule allE, erule allE, drule mp, erule monofun_rt_mult) |
|
168 apply (drule (1) mp) |
|
169 apply (assumption) |
|
170 done |
|
171 |
|
172 lemma stream_antiP2_non_gfp_admI: |
|
173 "!!X. [|!i x y. x << y --> y:down_iterate F i --> x:down_iterate F i; down_cont F |] |
|
174 ==> adm (%u. ~ u:gfp F)" |
|
175 apply (unfold adm_def) |
|
176 apply (simp add: INTER_down_iterate_is_gfp) |
|
177 apply (fast dest!: is_ub_thelub) |
|
178 done |
|
179 |
|
180 lemmas fstream_non_gfp_admI = stream_antiP2I [THEN stream_antiP2_non_gfp_admI] |
|
181 |
|
182 |
|
183 |
|
184 (**new approach for adm********************************************************) |
|
185 |
|
186 section "antitonP" |
|
187 |
|
188 lemma antitonPD: "[| antitonP P; y:P; x<<y |] ==> x:P" |
|
189 apply (unfold antitonP_def) |
|
190 apply auto |
|
191 done |
|
192 |
|
193 lemma antitonPI: "!x y. y:P --> x<<y --> x:P ==> antitonP P" |
|
194 apply (unfold antitonP_def) |
|
195 apply (fast) |
|
196 done |
|
197 |
|
198 lemma antitonP_adm_non_P: "antitonP P ==> adm (%u. u~:P)" |
|
199 apply (unfold adm_def) |
|
200 apply (auto dest: antitonPD elim: is_ub_thelub) |
|
201 done |
|
202 |
|
203 lemma def_gfp_adm_nonP: "P \<equiv> gfp F \<Longrightarrow> {y. \<exists>x::'a::pcpo. y \<sqsubseteq> x \<and> x \<in> P} \<subseteq> F {y. \<exists>x. y \<sqsubseteq> x \<and> x \<in> P} \<Longrightarrow> |
|
204 adm (\<lambda>u. u\<notin>P)" |
|
205 apply (simp) |
|
206 apply (rule antitonP_adm_non_P) |
|
207 apply (rule antitonPI) |
|
208 apply (drule gfp_upperbound) |
|
209 apply (fast) |
|
210 done |
|
211 |
|
212 lemma adm_set: |
|
213 "{\<Squnion>i. Y i |Y. Porder.chain Y & (\<forall>i. Y i \<in> P)} \<subseteq> P \<Longrightarrow> adm (\<lambda>x. x\<in>P)" |
|
214 apply (unfold adm_def) |
|
215 apply (fast) |
|
216 done |
|
217 |
|
218 lemma def_gfp_admI: "P \<equiv> gfp F \<Longrightarrow> {\<Squnion>i. Y i |Y. Porder.chain Y \<and> (\<forall>i. Y i \<in> P)} \<subseteq> |
|
219 F {\<Squnion>i. Y i |Y. Porder.chain Y \<and> (\<forall>i. Y i \<in> P)} \<Longrightarrow> adm (\<lambda>x. x\<in>P)" |
|
220 apply (simp) |
|
221 apply (rule adm_set) |
|
222 apply (erule gfp_upperbound) |
|
223 done |
|
224 |
|
225 end |
|