author | huffman |
Wed, 03 Nov 2010 15:47:46 -0700 | |
changeset 40431 | 682d6c455670 |
parent 40430 | 483a4876e428 |
child 40771 | 1c6f7d4b110e |
permissions | -rw-r--r-- |
17293 | 1 |
(* Title: HOLCF/ex/Stream_adm.thy |
2 |
Author: David von Oheimb, TU Muenchen |
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
3 |
*) |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
4 |
|
17293 | 5 |
header {* Admissibility for streams *} |
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
6 |
|
17293 | 7 |
theory Stream_adm |
37110
7ffdbc24b27f
move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path
huffman
parents:
35174
diff
changeset
|
8 |
imports Stream Continuity |
17293 | 9 |
begin |
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
10 |
|
19763 | 11 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset
|
12 |
stream_monoP :: "(('a stream) set \<Rightarrow> ('a stream) set) \<Rightarrow> bool" where |
19763 | 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))" |
|
17293 | 15 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset
|
16 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset
|
17 |
stream_antiP :: "(('a stream) set \<Rightarrow> ('a stream) set) \<Rightarrow> bool" where |
19763 | 18 |
"stream_antiP F = (\<forall>P x. \<exists>Q i. |
17293 | 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> |
|
19763 | 21 |
(y \<in> F P) = (stream_take i\<cdot>y \<in> Q \<and> iterate i\<cdot>rt\<cdot>y \<in> P))))" |
17293 | 22 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset
|
23 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset
|
24 |
antitonP :: "'a set => bool" where |
19763 | 25 |
"antitonP P = (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> y\<in>P \<longrightarrow> x\<in>P)" |
17293 | 26 |
|
27 |
||
19759 | 28 |
(* ----------------------------------------------------------------------- *) |
29 |
||
30 |
section "admissibility" |
|
31 |
||
40430
483a4876e428
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman
parents:
37110
diff
changeset
|
32 |
lemma infinite_chain_adm_lemma: |
483a4876e428
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman
parents:
37110
diff
changeset
|
33 |
"\<lbrakk>Porder.chain Y; \<forall>i. P (Y i); |
483a4876e428
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman
parents:
37110
diff
changeset
|
34 |
\<And>Y. \<lbrakk>Porder.chain Y; \<forall>i. P (Y i); \<not> finite_chain Y\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)\<rbrakk> |
483a4876e428
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman
parents:
37110
diff
changeset
|
35 |
\<Longrightarrow> P (\<Squnion>i. Y i)" |
483a4876e428
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman
parents:
37110
diff
changeset
|
36 |
apply (case_tac "finite_chain Y") |
483a4876e428
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman
parents:
37110
diff
changeset
|
37 |
prefer 2 apply fast |
483a4876e428
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman
parents:
37110
diff
changeset
|
38 |
apply (unfold finite_chain_def) |
483a4876e428
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman
parents:
37110
diff
changeset
|
39 |
apply safe |
483a4876e428
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman
parents:
37110
diff
changeset
|
40 |
apply (erule lub_finch1 [THEN thelubI, THEN ssubst]) |
483a4876e428
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman
parents:
37110
diff
changeset
|
41 |
apply assumption |
483a4876e428
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman
parents:
37110
diff
changeset
|
42 |
apply (erule spec) |
483a4876e428
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman
parents:
37110
diff
changeset
|
43 |
done |
483a4876e428
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman
parents:
37110
diff
changeset
|
44 |
|
483a4876e428
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman
parents:
37110
diff
changeset
|
45 |
lemma increasing_chain_adm_lemma: |
483a4876e428
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman
parents:
37110
diff
changeset
|
46 |
"\<lbrakk>Porder.chain Y; \<forall>i. P (Y i); \<And>Y. \<lbrakk>Porder.chain Y; \<forall>i. P (Y i); |
483a4876e428
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman
parents:
37110
diff
changeset
|
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> |
483a4876e428
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman
parents:
37110
diff
changeset
|
48 |
\<Longrightarrow> P (\<Squnion>i. Y i)" |
483a4876e428
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman
parents:
37110
diff
changeset
|
49 |
apply (erule infinite_chain_adm_lemma) |
483a4876e428
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman
parents:
37110
diff
changeset
|
50 |
apply assumption |
483a4876e428
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman
parents:
37110
diff
changeset
|
51 |
apply (erule thin_rl) |
483a4876e428
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman
parents:
37110
diff
changeset
|
52 |
apply (unfold finite_chain_def) |
483a4876e428
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman
parents:
37110
diff
changeset
|
53 |
apply (unfold max_in_chain_def) |
483a4876e428
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman
parents:
37110
diff
changeset
|
54 |
apply (fast dest: le_imp_less_or_eq elim: chain_mono_less) |
483a4876e428
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman
parents:
37110
diff
changeset
|
55 |
done |
483a4876e428
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman
parents:
37110
diff
changeset
|
56 |
|
19759 | 57 |
lemma flatstream_adm_lemma: |
26451
f8a615f3bb31
avoid amiguity of Continuity.chain vs. Porder.chain;
wenzelm
parents:
26102
diff
changeset
|
58 |
assumes 1: "Porder.chain Y" |
19759 | 59 |
assumes 2: "!i. P (Y i)" |
26451
f8a615f3bb31
avoid amiguity of Continuity.chain vs. Porder.chain;
wenzelm
parents:
26102
diff
changeset
|
60 |
assumes 3: "(!!Y. [| Porder.chain Y; !i. P (Y i); !k. ? j. Fin k < #((Y j)::'a::flat stream)|] |
27413 | 61 |
==> P(LUB i. Y i))" |
62 |
shows "P(LUB i. Y i)" |
|
26838
7f7c6a9e083a
Instantiated rule increasing_chain_adm_lemma in proof of flatstream_adm_lemma
berghofe
parents:
26451
diff
changeset
|
63 |
apply (rule increasing_chain_adm_lemma [of _ P, OF 1 2]) |
19759 | 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) |
|
31084 | 77 |
apply (metis inat_ord_code(4) slen_infinite) |
19759 | 78 |
done |
79 |
||
80 |
(* should be without reference to stream length? *) |
|
26451
f8a615f3bb31
avoid amiguity of Continuity.chain vs. Porder.chain;
wenzelm
parents:
26102
diff
changeset
|
81 |
lemma flatstream_admI: "[|(!!Y. [| Porder.chain Y; !i. P (Y i); |
27413 | 82 |
!k. ? j. Fin k < #((Y j)::'a::flat stream)|] ==> P(LUB i. Y i))|]==> adm P" |
19759 | 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" |
|
27101
864d29f11c9d
slightly tuning of some proofs involving case distinction and induction on natural numbers and similar
haftmann
parents:
26838
diff
changeset
|
92 |
by (rule order_trans) auto |
19759 | 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 |
|
27101
864d29f11c9d
slightly tuning of some proofs involving case distinction and induction on natural numbers and similar
haftmann
parents:
26838
diff
changeset
|
107 |
apply ( erule order_trans) |
19759 | 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) |
|
27101
864d29f11c9d
slightly tuning of some proofs involving case distinction and induction on natural numbers and similar
haftmann
parents:
26838
diff
changeset
|
134 |
apply ( drule order_trans) |
19759 | 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) |
|
26102 | 158 |
apply (unfold linorder_not_less) |
19759 | 159 |
apply (drule (1) mp) |
40431 | 160 |
apply (erule all_dupE, drule mp, rule below_refl) |
19759 | 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: |
|
27413 | 213 |
"{\<Squnion>i. Y i |Y. Porder.chain Y & (\<forall>i. Y i \<in> P)} \<subseteq> P \<Longrightarrow> adm (\<lambda>x. x\<in>P)" |
19759 | 214 |
apply (unfold adm_def) |
215 |
apply (fast) |
|
216 |
done |
|
217 |
||
27413 | 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)" |
|
19759 | 220 |
apply (simp) |
221 |
apply (rule adm_set) |
|
222 |
apply (erule gfp_upperbound) |
|
223 |
done |
|
224 |
||
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
225 |
end |