author | wenzelm |
Thu, 23 Jul 2009 18:44:09 +0200 | |
changeset 32149 | ef59550a55d3 |
parent 30609 | 983e8b6e4e69 |
child 32156 | 910443ff0839 |
permissions | -rw-r--r-- |
17293 | 1 |
(* Title: HOLCF/FOCUS/Buffer.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 |
Formalization of section 4 of |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
5 |
|
15038 | 6 |
@inproceedings {broy_mod94, |
7 |
author = {Manfred Broy}, |
|
8 |
title = {{Specification and Refinement of a Buffer of Length One}}, |
|
9 |
booktitle = {Deductive Program Design}, |
|
10 |
year = {1994}, |
|
11 |
editor = {Manfred Broy}, |
|
12 |
volume = {152}, |
|
13 |
series = {ASI Series, Series F: Computer and System Sciences}, |
|
14 |
pages = {273 -- 304}, |
|
15 |
publisher = {Springer} |
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
16 |
} |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
17 |
|
17646 | 18 |
Slides available from http://ddvo.net/talks/1-Buffer.ps.gz |
15038 | 19 |
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
20 |
*) |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
21 |
|
17293 | 22 |
theory Buffer |
23 |
imports FOCUS |
|
24 |
begin |
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
25 |
|
17293 | 26 |
typedecl D |
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
27 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
28 |
datatype |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
29 |
|
17293 | 30 |
M = Md D | Mreq ("\<bullet>") |
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
31 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
32 |
datatype |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
33 |
|
17293 | 34 |
State = Sd D | Snil ("\<currency>") |
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
35 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
36 |
types |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
37 |
|
17293 | 38 |
SPF11 = "M fstream \<rightarrow> D fstream" |
39 |
SPEC11 = "SPF11 set" |
|
40 |
SPSF11 = "State \<Rightarrow> SPF11" |
|
41 |
SPECS11 = "SPSF11 set" |
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
42 |
|
19763 | 43 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset
|
44 |
BufEq_F :: "SPEC11 \<Rightarrow> SPEC11" where |
19763 | 45 |
"BufEq_F B = {f. \<forall>d. f\<cdot>(Md d\<leadsto><>) = <> \<and> |
46 |
(\<forall>x. \<exists>ff\<in>B. f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>x) = d\<leadsto>ff\<cdot>x)}" |
|
47 |
||
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset
|
48 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset
|
49 |
BufEq :: "SPEC11" where |
19763 | 50 |
"BufEq = gfp BufEq_F" |
51 |
||
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset
|
52 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset
|
53 |
BufEq_alt :: "SPEC11" where |
19763 | 54 |
"BufEq_alt = gfp (\<lambda>B. {f. \<forall>d. f\<cdot>(Md d\<leadsto><> ) = <> \<and> |
55 |
(\<exists>ff\<in>B. (\<forall>x. f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>x) = d\<leadsto>ff\<cdot>x))})" |
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
56 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset
|
57 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset
|
58 |
BufAC_Asm_F :: " (M fstream set) \<Rightarrow> (M fstream set)" where |
19763 | 59 |
"BufAC_Asm_F A = {s. s = <> \<or> |
60 |
(\<exists>d x. s = Md d\<leadsto>x \<and> (x = <> \<or> (ft\<cdot>x = Def \<bullet> \<and> (rt\<cdot>x)\<in>A)))}" |
|
61 |
||
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset
|
62 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset
|
63 |
BufAC_Asm :: " (M fstream set)" where |
19763 | 64 |
"BufAC_Asm = gfp BufAC_Asm_F" |
65 |
||
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset
|
66 |
definition |
17293 | 67 |
BufAC_Cmt_F :: "((M fstream * D fstream) set) \<Rightarrow> |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset
|
68 |
((M fstream * D fstream) set)" where |
19763 | 69 |
"BufAC_Cmt_F C = {(s,t). \<forall>d x. |
17293 | 70 |
(s = <> \<longrightarrow> t = <> ) \<and> |
71 |
(s = Md d\<leadsto><> \<longrightarrow> t = <> ) \<and> |
|
72 |
(s = Md d\<leadsto>\<bullet>\<leadsto>x \<longrightarrow> (ft\<cdot>t = Def d \<and> (x,rt\<cdot>t)\<in>C))}" |
|
19763 | 73 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset
|
74 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset
|
75 |
BufAC_Cmt :: "((M fstream * D fstream) set)" where |
19763 | 76 |
"BufAC_Cmt = gfp BufAC_Cmt_F" |
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
77 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset
|
78 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset
|
79 |
BufAC :: "SPEC11" where |
19763 | 80 |
"BufAC = {f. \<forall>x. x\<in>BufAC_Asm \<longrightarrow> (x,f\<cdot>x)\<in>BufAC_Cmt}" |
81 |
||
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset
|
82 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset
|
83 |
BufSt_F :: "SPECS11 \<Rightarrow> SPECS11" where |
19763 | 84 |
"BufSt_F H = {h. \<forall>s . h s \<cdot><> = <> \<and> |
17293 | 85 |
(\<forall>d x. h \<currency> \<cdot>(Md d\<leadsto>x) = h (Sd d)\<cdot>x \<and> |
86 |
(\<exists>hh\<in>H. h (Sd d)\<cdot>(\<bullet> \<leadsto>x) = d\<leadsto>(hh \<currency>\<cdot>x)))}" |
|
19763 | 87 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset
|
88 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset
|
89 |
BufSt_P :: "SPECS11" where |
19763 | 90 |
"BufSt_P = gfp BufSt_F" |
17293 | 91 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset
|
92 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset
|
93 |
BufSt :: "SPEC11" where |
19763 | 94 |
"BufSt = {f. \<exists>h\<in>BufSt_P. f = h \<currency>}" |
95 |
||
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
96 |
|
19759 | 97 |
lemma set_cong: "!!X. A = B ==> (x:A) = (x:B)" |
98 |
by (erule subst, rule refl) |
|
99 |
||
100 |
ML {* |
|
30609
983e8b6e4e69
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
wenzelm
parents:
28952
diff
changeset
|
101 |
fun B_prover s tac eqs = |
983e8b6e4e69
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
wenzelm
parents:
28952
diff
changeset
|
102 |
let val thy = the_context () in |
983e8b6e4e69
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
wenzelm
parents:
28952
diff
changeset
|
103 |
prove_goal thy s (fn prems => [cut_facts_tac prems 1, |
32149
ef59550a55d3
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
wenzelm
parents:
30609
diff
changeset
|
104 |
tac 1, auto_tac (global_claset_of thy, global_simpset_of thy addsimps eqs)]) |
30609
983e8b6e4e69
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
wenzelm
parents:
28952
diff
changeset
|
105 |
end; |
19759 | 106 |
|
107 |
fun prove_forw s thm = B_prover s (dtac (thm RS iffD1)) []; |
|
108 |
fun prove_backw s thm eqs = B_prover s (rtac (thm RS iffD2)) eqs; |
|
109 |
*} |
|
110 |
||
111 |
(**** BufEq *******************************************************************) |
|
112 |
||
113 |
lemma mono_BufEq_F: "mono BufEq_F" |
|
114 |
by (unfold mono_def BufEq_F_def, fast) |
|
115 |
||
19763 | 116 |
lemmas BufEq_fix = mono_BufEq_F [THEN BufEq_def [THEN eq_reflection, THEN def_gfp_unfold]] |
19759 | 117 |
|
118 |
lemma BufEq_unfold: "(f:BufEq) = (!d. f\<cdot>(Md d\<leadsto><>) = <> & |
|
119 |
(!x. ? ff:BufEq. f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>x) = d\<leadsto>(ff\<cdot>x)))" |
|
120 |
apply (subst BufEq_fix [THEN set_cong]) |
|
121 |
apply (unfold BufEq_F_def) |
|
122 |
apply (simp) |
|
123 |
done |
|
124 |
||
125 |
lemma Buf_f_empty: "f:BufEq \<Longrightarrow> f\<cdot><> = <>" |
|
126 |
by (drule BufEq_unfold [THEN iffD1], auto) |
|
127 |
||
128 |
lemma Buf_f_d: "f:BufEq \<Longrightarrow> f\<cdot>(Md d\<leadsto><>) = <>" |
|
129 |
by (drule BufEq_unfold [THEN iffD1], auto) |
|
130 |
||
131 |
lemma Buf_f_d_req: |
|
132 |
"f:BufEq \<Longrightarrow> \<exists>ff. ff:BufEq \<and> f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>x) = d\<leadsto>ff\<cdot>x" |
|
133 |
by (drule BufEq_unfold [THEN iffD1], auto) |
|
134 |
||
135 |
||
136 |
(**** BufAC_Asm ***************************************************************) |
|
137 |
||
138 |
lemma mono_BufAC_Asm_F: "mono BufAC_Asm_F" |
|
139 |
by (unfold mono_def BufAC_Asm_F_def, fast) |
|
140 |
||
19763 | 141 |
lemmas BufAC_Asm_fix = |
142 |
mono_BufAC_Asm_F [THEN BufAC_Asm_def [THEN eq_reflection, THEN def_gfp_unfold]] |
|
19759 | 143 |
|
144 |
lemma BufAC_Asm_unfold: "(s:BufAC_Asm) = (s = <> | (? d x. |
|
145 |
s = Md d\<leadsto>x & (x = <> | (ft\<cdot>x = Def \<bullet> & (rt\<cdot>x):BufAC_Asm))))" |
|
146 |
apply (subst BufAC_Asm_fix [THEN set_cong]) |
|
147 |
apply (unfold BufAC_Asm_F_def) |
|
148 |
apply (simp) |
|
149 |
done |
|
150 |
||
151 |
lemma BufAC_Asm_empty: "<> :BufAC_Asm" |
|
152 |
by (rule BufAC_Asm_unfold [THEN iffD2], auto) |
|
153 |
||
154 |
lemma BufAC_Asm_d: "Md d\<leadsto><>:BufAC_Asm" |
|
155 |
by (rule BufAC_Asm_unfold [THEN iffD2], auto) |
|
156 |
lemma BufAC_Asm_d_req: "x:BufAC_Asm ==> Md d\<leadsto>\<bullet>\<leadsto>x:BufAC_Asm" |
|
157 |
by (rule BufAC_Asm_unfold [THEN iffD2], auto) |
|
158 |
lemma BufAC_Asm_prefix2: "a\<leadsto>b\<leadsto>s:BufAC_Asm ==> s:BufAC_Asm" |
|
159 |
by (drule BufAC_Asm_unfold [THEN iffD1], auto) |
|
160 |
||
161 |
||
162 |
(**** BBufAC_Cmt **************************************************************) |
|
163 |
||
164 |
lemma mono_BufAC_Cmt_F: "mono BufAC_Cmt_F" |
|
165 |
by (unfold mono_def BufAC_Cmt_F_def, fast) |
|
166 |
||
19763 | 167 |
lemmas BufAC_Cmt_fix = |
168 |
mono_BufAC_Cmt_F [THEN BufAC_Cmt_def [THEN eq_reflection, THEN def_gfp_unfold]] |
|
19759 | 169 |
|
170 |
lemma BufAC_Cmt_unfold: "((s,t):BufAC_Cmt) = (!d x. |
|
171 |
(s = <> --> t = <>) & |
|
172 |
(s = Md d\<leadsto><> --> t = <>) & |
|
173 |
(s = Md d\<leadsto>\<bullet>\<leadsto>x --> ft\<cdot>t = Def d & (x, rt\<cdot>t):BufAC_Cmt))" |
|
174 |
apply (subst BufAC_Cmt_fix [THEN set_cong]) |
|
175 |
apply (unfold BufAC_Cmt_F_def) |
|
176 |
apply (simp) |
|
177 |
done |
|
178 |
||
179 |
lemma BufAC_Cmt_empty: "f:BufEq ==> (<>, f\<cdot><>):BufAC_Cmt" |
|
180 |
by (rule BufAC_Cmt_unfold [THEN iffD2], auto simp add: Buf_f_empty) |
|
181 |
||
182 |
lemma BufAC_Cmt_d: "f:BufEq ==> (a\<leadsto>\<bottom>, f\<cdot>(a\<leadsto>\<bottom>)):BufAC_Cmt" |
|
183 |
by (rule BufAC_Cmt_unfold [THEN iffD2], auto simp add: Buf_f_d) |
|
184 |
||
185 |
lemma BufAC_Cmt_d2: |
|
186 |
"(Md d\<leadsto>\<bottom>, f\<cdot>(Md d\<leadsto>\<bottom>)):BufAC_Cmt ==> f\<cdot>(Md d\<leadsto>\<bottom>) = \<bottom>" |
|
187 |
by (drule BufAC_Cmt_unfold [THEN iffD1], auto) |
|
188 |
||
189 |
lemma BufAC_Cmt_d3: |
|
190 |
"(Md d\<leadsto>\<bullet>\<leadsto>x, f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>x)):BufAC_Cmt ==> (x, rt\<cdot>(f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>x))):BufAC_Cmt" |
|
191 |
by (drule BufAC_Cmt_unfold [THEN iffD1], auto) |
|
192 |
||
193 |
lemma BufAC_Cmt_d32: |
|
194 |
"(Md d\<leadsto>\<bullet>\<leadsto>x, f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>x)):BufAC_Cmt ==> ft\<cdot>(f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>x)) = Def d" |
|
195 |
by (drule BufAC_Cmt_unfold [THEN iffD1], auto) |
|
196 |
||
197 |
(**** BufAC *******************************************************************) |
|
198 |
||
199 |
lemma BufAC_f_d: "f \<in> BufAC \<Longrightarrow> f\<cdot>(Md d\<leadsto>\<bottom>) = \<bottom>" |
|
200 |
apply (unfold BufAC_def) |
|
201 |
apply (fast intro: BufAC_Cmt_d2 BufAC_Asm_d) |
|
202 |
done |
|
203 |
||
204 |
lemma ex_elim_lemma: "(? ff:B. (!x. f\<cdot>(a\<leadsto>b\<leadsto>x) = d\<leadsto>ff\<cdot>x)) = |
|
205 |
((!x. ft\<cdot>(f\<cdot>(a\<leadsto>b\<leadsto>x)) = Def d) & (LAM x. rt\<cdot>(f\<cdot>(a\<leadsto>b\<leadsto>x))):B)" |
|
206 |
(* this is an instance (though unification cannot handle this) of |
|
207 |
lemma "(? ff:B. (!x. f\<cdot>x = d\<leadsto>ff\<cdot>x)) = \ |
|
208 |
\((!x. ft\<cdot>(f\<cdot>x) = Def d) & (LAM x. rt\<cdot>(f\<cdot>x)):B)"*) |
|
209 |
apply safe |
|
210 |
apply ( rule_tac [2] P="(%x. x:B)" in ssubst) |
|
211 |
prefer 3 |
|
212 |
apply ( assumption) |
|
213 |
apply ( rule_tac [2] ext_cfun) |
|
214 |
apply ( drule_tac [2] spec) |
|
215 |
apply ( drule_tac [2] f="rt" in cfun_arg_cong) |
|
216 |
prefer 2 |
|
217 |
apply ( simp) |
|
218 |
prefer 2 |
|
219 |
apply ( simp) |
|
220 |
apply (rule_tac bexI) |
|
221 |
apply auto |
|
222 |
apply (drule spec) |
|
223 |
apply (erule exE) |
|
224 |
apply (erule ssubst) |
|
225 |
apply (simp) |
|
226 |
done |
|
227 |
||
228 |
lemma BufAC_f_d_req: "f\<in>BufAC \<Longrightarrow> \<exists>ff\<in>BufAC. \<forall>x. f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>x) = d\<leadsto>ff\<cdot>x" |
|
229 |
apply (unfold BufAC_def) |
|
230 |
apply (rule ex_elim_lemma [THEN iffD2]) |
|
231 |
apply safe |
|
232 |
apply (fast intro: BufAC_Cmt_d32 [THEN Def_maximal] |
|
233 |
monofun_cfun_arg BufAC_Asm_empty [THEN BufAC_Asm_d_req]) |
|
234 |
apply (auto intro: BufAC_Cmt_d3 BufAC_Asm_d_req) |
|
235 |
done |
|
236 |
||
237 |
||
238 |
(**** BufSt *******************************************************************) |
|
239 |
||
240 |
lemma mono_BufSt_F: "mono BufSt_F" |
|
241 |
by (unfold mono_def BufSt_F_def, fast) |
|
242 |
||
19763 | 243 |
lemmas BufSt_P_fix = |
244 |
mono_BufSt_F [THEN BufSt_P_def [THEN eq_reflection, THEN def_gfp_unfold]] |
|
19759 | 245 |
|
246 |
lemma BufSt_P_unfold: "(h:BufSt_P) = (!s. h s\<cdot><> = <> & |
|
247 |
(!d x. h \<currency> \<cdot>(Md d\<leadsto>x) = h (Sd d)\<cdot>x & |
|
248 |
(? hh:BufSt_P. h (Sd d)\<cdot>(\<bullet>\<leadsto>x) = d\<leadsto>(hh \<currency> \<cdot>x))))" |
|
249 |
apply (subst BufSt_P_fix [THEN set_cong]) |
|
250 |
apply (unfold BufSt_F_def) |
|
251 |
apply (simp) |
|
252 |
done |
|
253 |
||
254 |
lemma BufSt_P_empty: "h:BufSt_P ==> h s \<cdot> <> = <>" |
|
255 |
by (drule BufSt_P_unfold [THEN iffD1], auto) |
|
256 |
lemma BufSt_P_d: "h:BufSt_P ==> h \<currency> \<cdot>(Md d\<leadsto>x) = h (Sd d)\<cdot>x" |
|
257 |
by (drule BufSt_P_unfold [THEN iffD1], auto) |
|
258 |
lemma BufSt_P_d_req: "h:BufSt_P ==> \<exists>hh\<in>BufSt_P. |
|
259 |
h (Sd d)\<cdot>(\<bullet> \<leadsto>x) = d\<leadsto>(hh \<currency> \<cdot>x)" |
|
260 |
by (drule BufSt_P_unfold [THEN iffD1], auto) |
|
261 |
||
262 |
||
263 |
(**** Buf_AC_imp_Eq ***********************************************************) |
|
264 |
||
265 |
lemma Buf_AC_imp_Eq: "BufAC \<subseteq> BufEq" |
|
266 |
apply (unfold BufEq_def) |
|
267 |
apply (rule gfp_upperbound) |
|
268 |
apply (unfold BufEq_F_def) |
|
269 |
apply safe |
|
270 |
apply (erule BufAC_f_d) |
|
271 |
apply (drule BufAC_f_d_req) |
|
272 |
apply (fast) |
|
273 |
done |
|
274 |
||
275 |
||
276 |
(**** Buf_Eq_imp_AC by coinduction ********************************************) |
|
277 |
||
278 |
lemma BufAC_Asm_cong_lemma [rule_format]: "\<forall>s f ff. f\<in>BufEq \<longrightarrow> ff\<in>BufEq \<longrightarrow> |
|
279 |
s\<in>BufAC_Asm \<longrightarrow> stream_take n\<cdot>(f\<cdot>s) = stream_take n\<cdot>(ff\<cdot>s)" |
|
280 |
apply (induct_tac "n") |
|
281 |
apply (simp) |
|
282 |
apply (intro strip) |
|
283 |
apply (drule BufAC_Asm_unfold [THEN iffD1]) |
|
284 |
apply safe |
|
285 |
apply (simp add: Buf_f_empty) |
|
286 |
apply (simp add: Buf_f_d) |
|
287 |
apply (drule ft_eq [THEN iffD1]) |
|
288 |
apply (clarsimp) |
|
289 |
apply (drule Buf_f_d_req)+ |
|
290 |
apply safe |
|
291 |
apply (erule ssubst)+ |
|
292 |
apply (simp (no_asm)) |
|
293 |
apply (fast) |
|
294 |
done |
|
295 |
||
296 |
lemma BufAC_Asm_cong: "\<lbrakk>f \<in> BufEq; ff \<in> BufEq; s \<in> BufAC_Asm\<rbrakk> \<Longrightarrow> f\<cdot>s = ff\<cdot>s" |
|
297 |
apply (rule stream.take_lemmas) |
|
298 |
apply (erule (2) BufAC_Asm_cong_lemma) |
|
299 |
done |
|
300 |
||
301 |
lemma Buf_Eq_imp_AC_lemma: "\<lbrakk>f \<in> BufEq; x \<in> BufAC_Asm\<rbrakk> \<Longrightarrow> (x, f\<cdot>x) \<in> BufAC_Cmt" |
|
302 |
apply (unfold BufAC_Cmt_def) |
|
303 |
apply (rotate_tac) |
|
304 |
apply (erule weak_coinduct_image) |
|
305 |
apply (unfold BufAC_Cmt_F_def) |
|
306 |
apply safe |
|
307 |
apply (erule Buf_f_empty) |
|
308 |
apply (erule Buf_f_d) |
|
309 |
apply (drule Buf_f_d_req) |
|
310 |
apply (clarsimp) |
|
311 |
apply (erule exI) |
|
312 |
apply (drule BufAC_Asm_prefix2) |
|
313 |
apply (frule Buf_f_d_req) |
|
314 |
apply (clarsimp) |
|
315 |
apply (erule ssubst) |
|
316 |
apply (simp) |
|
317 |
apply (drule (2) BufAC_Asm_cong) |
|
318 |
apply (erule subst) |
|
319 |
apply (erule imageI) |
|
320 |
done |
|
321 |
lemma Buf_Eq_imp_AC: "BufEq \<subseteq> BufAC" |
|
322 |
apply (unfold BufAC_def) |
|
323 |
apply (clarify) |
|
324 |
apply (erule (1) Buf_Eq_imp_AC_lemma) |
|
325 |
done |
|
326 |
||
327 |
(**** Buf_Eq_eq_AC ************************************************************) |
|
328 |
||
329 |
lemmas Buf_Eq_eq_AC = Buf_AC_imp_Eq [THEN Buf_Eq_imp_AC [THEN subset_antisym]] |
|
330 |
||
331 |
||
332 |
(**** alternative (not strictly) stronger version of Buf_Eq *******************) |
|
333 |
||
334 |
lemma Buf_Eq_alt_imp_Eq: "BufEq_alt \<subseteq> BufEq" |
|
335 |
apply (unfold BufEq_def BufEq_alt_def) |
|
336 |
apply (rule gfp_mono) |
|
337 |
apply (unfold BufEq_F_def) |
|
338 |
apply (fast) |
|
339 |
done |
|
340 |
||
341 |
(* direct proof of "BufEq \<subseteq> BufEq_alt" seems impossible *) |
|
342 |
||
343 |
||
344 |
lemma Buf_AC_imp_Eq_alt: "BufAC <= BufEq_alt" |
|
345 |
apply (unfold BufEq_alt_def) |
|
346 |
apply (rule gfp_upperbound) |
|
347 |
apply (fast elim: BufAC_f_d BufAC_f_d_req) |
|
348 |
done |
|
349 |
||
350 |
lemmas Buf_Eq_imp_Eq_alt = subset_trans [OF Buf_Eq_imp_AC Buf_AC_imp_Eq_alt] |
|
351 |
||
352 |
lemmas Buf_Eq_alt_eq = subset_antisym [OF Buf_Eq_alt_imp_Eq Buf_Eq_imp_Eq_alt] |
|
353 |
||
354 |
||
355 |
(**** Buf_Eq_eq_St ************************************************************) |
|
356 |
||
357 |
lemma Buf_St_imp_Eq: "BufSt <= BufEq" |
|
358 |
apply (unfold BufSt_def BufEq_def) |
|
359 |
apply (rule gfp_upperbound) |
|
360 |
apply (unfold BufEq_F_def) |
|
361 |
apply safe |
|
362 |
apply ( simp add: BufSt_P_d BufSt_P_empty) |
|
363 |
apply (simp add: BufSt_P_d) |
|
364 |
apply (drule BufSt_P_d_req) |
|
365 |
apply (force) |
|
366 |
done |
|
367 |
||
368 |
lemma Buf_Eq_imp_St: "BufEq <= BufSt" |
|
369 |
apply (unfold BufSt_def BufSt_P_def) |
|
370 |
apply safe |
|
371 |
apply (rename_tac f) |
|
372 |
apply (rule_tac x="\<lambda>s. case s of Sd d => \<Lambda> x. f\<cdot>(Md d\<leadsto>x)| \<currency> => f" in bexI) |
|
373 |
apply ( simp) |
|
374 |
apply (erule weak_coinduct_image) |
|
375 |
apply (unfold BufSt_F_def) |
|
376 |
apply (simp) |
|
377 |
apply safe |
|
378 |
apply ( rename_tac "s") |
|
379 |
apply ( induct_tac "s") |
|
380 |
apply ( simp add: Buf_f_d) |
|
381 |
apply ( simp add: Buf_f_empty) |
|
382 |
apply ( simp) |
|
383 |
apply (simp) |
|
384 |
apply (rename_tac f d x) |
|
385 |
apply (drule_tac d="d" and x="x" in Buf_f_d_req) |
|
386 |
apply auto |
|
387 |
done |
|
388 |
||
389 |
lemmas Buf_Eq_eq_St = Buf_St_imp_Eq [THEN Buf_Eq_imp_St [THEN subset_antisym]] |
|
390 |
||
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
391 |
end |