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