author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 42151  4da4fc77664b 
child 58305  57752a91eec4 
permissions  rwrr 
42151  1 
(* Title: HOL/HOLCF/FOCUS/Buffer.thy 
17293  2 
Author: David von Oheimb, TU Muenchen 
11350
4c55b020d6ee
added FOCUS including the OneElement Buffer by Manfred Broy
oheimb
parents:
diff
changeset

3 

4c55b020d6ee
added FOCUS including the OneElement Buffer by Manfred Broy
oheimb
parents:
diff
changeset

4 
Formalization of section 4 of 
4c55b020d6ee
added FOCUS including the OneElement 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 OneElement Buffer by Manfred Broy
oheimb
parents:
diff
changeset

16 
} 
4c55b020d6ee
added FOCUS including the OneElement Buffer by Manfred Broy
oheimb
parents:
diff
changeset

17 

17646  18 
Slides available from http://ddvo.net/talks/1Buffer.ps.gz 
15038  19 

11350
4c55b020d6ee
added FOCUS including the OneElement Buffer by Manfred Broy
oheimb
parents:
diff
changeset

20 
*) 
4c55b020d6ee
added FOCUS including the OneElement Buffer by Manfred Broy
oheimb
parents:
diff
changeset

21 

17293  22 
theory Buffer 
23 
imports FOCUS 

24 
begin 

11350
4c55b020d6ee
added FOCUS including the OneElement Buffer by Manfred Broy
oheimb
parents:
diff
changeset

25 

17293  26 
typedecl D 
11350
4c55b020d6ee
added FOCUS including the OneElement Buffer by Manfred Broy
oheimb
parents:
diff
changeset

27 

4c55b020d6ee
added FOCUS including the OneElement Buffer by Manfred Broy
oheimb
parents:
diff
changeset

28 
datatype 
4c55b020d6ee
added FOCUS including the OneElement Buffer by Manfred Broy
oheimb
parents:
diff
changeset

29 

17293  30 
M = Md D  Mreq ("\<bullet>") 
11350
4c55b020d6ee
added FOCUS including the OneElement Buffer by Manfred Broy
oheimb
parents:
diff
changeset

31 

4c55b020d6ee
added FOCUS including the OneElement Buffer by Manfred Broy
oheimb
parents:
diff
changeset

32 
datatype 
4c55b020d6ee
added FOCUS including the OneElement Buffer by Manfred Broy
oheimb
parents:
diff
changeset

33 

17293  34 
State = Sd D  Snil ("\<currency>") 
11350
4c55b020d6ee
added FOCUS including the OneElement Buffer by Manfred Broy
oheimb
parents:
diff
changeset

35 

41476  36 
type_synonym 
17293  37 
SPF11 = "M fstream \<rightarrow> D fstream" 
41476  38 

39 
type_synonym 

17293  40 
SPEC11 = "SPF11 set" 
41476  41 

42 
type_synonym 

17293  43 
SPSF11 = "State \<Rightarrow> SPF11" 
41476  44 

45 
type_synonym 

17293  46 
SPECS11 = "SPSF11 set" 
11350
4c55b020d6ee
added FOCUS including the OneElement Buffer by Manfred Broy
oheimb
parents:
diff
changeset

47 

19763  48 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset

49 
BufEq_F :: "SPEC11 \<Rightarrow> SPEC11" where 
19763  50 
"BufEq_F B = {f. \<forall>d. f\<cdot>(Md d\<leadsto><>) = <> \<and> 
51 
(\<forall>x. \<exists>ff\<in>B. f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>x) = d\<leadsto>ff\<cdot>x)}" 

52 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset

53 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset

54 
BufEq :: "SPEC11" where 
19763  55 
"BufEq = gfp BufEq_F" 
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 
BufEq_alt :: "SPEC11" where 
19763  59 
"BufEq_alt = gfp (\<lambda>B. {f. \<forall>d. f\<cdot>(Md d\<leadsto><> ) = <> \<and> 
60 
(\<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 OneElement Buffer by Manfred Broy
oheimb
parents:
diff
changeset

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_F :: " (M fstream set) \<Rightarrow> (M fstream set)" where 
19763  64 
"BufAC_Asm_F A = {s. s = <> \<or> 
65 
(\<exists>d x. s = Md d\<leadsto>x \<and> (x = <> \<or> (ft\<cdot>x = Def \<bullet> \<and> (rt\<cdot>x)\<in>A)))}" 

66 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset

67 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset

68 
BufAC_Asm :: " (M fstream set)" where 
19763  69 
"BufAC_Asm = gfp BufAC_Asm_F" 
70 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset

71 
definition 
17293  72 
BufAC_Cmt_F :: "((M fstream * D fstream) set) \<Rightarrow> 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset

73 
((M fstream * D fstream) set)" where 
19763  74 
"BufAC_Cmt_F C = {(s,t). \<forall>d x. 
17293  75 
(s = <> \<longrightarrow> t = <> ) \<and> 
76 
(s = Md d\<leadsto><> \<longrightarrow> t = <> ) \<and> 

77 
(s = Md d\<leadsto>\<bullet>\<leadsto>x \<longrightarrow> (ft\<cdot>t = Def d \<and> (x,rt\<cdot>t)\<in>C))}" 

19763  78 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset

79 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset

80 
BufAC_Cmt :: "((M fstream * D fstream) set)" where 
19763  81 
"BufAC_Cmt = gfp BufAC_Cmt_F" 
11350
4c55b020d6ee
added FOCUS including the OneElement Buffer by Manfred Broy
oheimb
parents:
diff
changeset

82 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset

83 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset

84 
BufAC :: "SPEC11" where 
19763  85 
"BufAC = {f. \<forall>x. x\<in>BufAC_Asm \<longrightarrow> (x,f\<cdot>x)\<in>BufAC_Cmt}" 
86 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset

87 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset

88 
BufSt_F :: "SPECS11 \<Rightarrow> SPECS11" where 
19763  89 
"BufSt_F H = {h. \<forall>s . h s \<cdot><> = <> \<and> 
17293  90 
(\<forall>d x. h \<currency> \<cdot>(Md d\<leadsto>x) = h (Sd d)\<cdot>x \<and> 
91 
(\<exists>hh\<in>H. h (Sd d)\<cdot>(\<bullet> \<leadsto>x) = d\<leadsto>(hh \<currency>\<cdot>x)))}" 

19763  92 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset

93 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset

94 
BufSt_P :: "SPECS11" where 
19763  95 
"BufSt_P = gfp BufSt_F" 
17293  96 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset

97 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset

98 
BufSt :: "SPEC11" where 
19763  99 
"BufSt = {f. \<exists>h\<in>BufSt_P. f = h \<currency>}" 
100 

11350
4c55b020d6ee
added FOCUS including the OneElement Buffer by Manfred Broy
oheimb
parents:
diff
changeset

101 

19759  102 
lemma set_cong: "!!X. A = B ==> (x:A) = (x:B)" 
103 
by (erule subst, rule refl) 

104 

105 

106 
(**** BufEq *******************************************************************) 

107 

108 
lemma mono_BufEq_F: "mono BufEq_F" 

109 
by (unfold mono_def BufEq_F_def, fast) 

110 

19763  111 
lemmas BufEq_fix = mono_BufEq_F [THEN BufEq_def [THEN eq_reflection, THEN def_gfp_unfold]] 
19759  112 

113 
lemma BufEq_unfold: "(f:BufEq) = (!d. f\<cdot>(Md d\<leadsto><>) = <> & 

114 
(!x. ? ff:BufEq. f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>x) = d\<leadsto>(ff\<cdot>x)))" 

115 
apply (subst BufEq_fix [THEN set_cong]) 

116 
apply (unfold BufEq_F_def) 

117 
apply (simp) 

118 
done 

119 

120 
lemma Buf_f_empty: "f:BufEq \<Longrightarrow> f\<cdot><> = <>" 

121 
by (drule BufEq_unfold [THEN iffD1], auto) 

122 

123 
lemma Buf_f_d: "f:BufEq \<Longrightarrow> f\<cdot>(Md d\<leadsto><>) = <>" 

124 
by (drule BufEq_unfold [THEN iffD1], auto) 

125 

126 
lemma Buf_f_d_req: 

127 
"f:BufEq \<Longrightarrow> \<exists>ff. ff:BufEq \<and> f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>x) = d\<leadsto>ff\<cdot>x" 

128 
by (drule BufEq_unfold [THEN iffD1], auto) 

129 

130 

131 
(**** BufAC_Asm ***************************************************************) 

132 

133 
lemma mono_BufAC_Asm_F: "mono BufAC_Asm_F" 

134 
by (unfold mono_def BufAC_Asm_F_def, fast) 

135 

19763  136 
lemmas BufAC_Asm_fix = 
137 
mono_BufAC_Asm_F [THEN BufAC_Asm_def [THEN eq_reflection, THEN def_gfp_unfold]] 

19759  138 

139 
lemma BufAC_Asm_unfold: "(s:BufAC_Asm) = (s = <>  (? d x. 

140 
s = Md d\<leadsto>x & (x = <>  (ft\<cdot>x = Def \<bullet> & (rt\<cdot>x):BufAC_Asm))))" 

141 
apply (subst BufAC_Asm_fix [THEN set_cong]) 

142 
apply (unfold BufAC_Asm_F_def) 

143 
apply (simp) 

144 
done 

145 

146 
lemma BufAC_Asm_empty: "<> :BufAC_Asm" 

147 
by (rule BufAC_Asm_unfold [THEN iffD2], auto) 

148 

149 
lemma BufAC_Asm_d: "Md d\<leadsto><>:BufAC_Asm" 

150 
by (rule BufAC_Asm_unfold [THEN iffD2], auto) 

151 
lemma BufAC_Asm_d_req: "x:BufAC_Asm ==> Md d\<leadsto>\<bullet>\<leadsto>x:BufAC_Asm" 

152 
by (rule BufAC_Asm_unfold [THEN iffD2], auto) 

153 
lemma BufAC_Asm_prefix2: "a\<leadsto>b\<leadsto>s:BufAC_Asm ==> s:BufAC_Asm" 

154 
by (drule BufAC_Asm_unfold [THEN iffD1], auto) 

155 

156 

157 
(**** BBufAC_Cmt **************************************************************) 

158 

159 
lemma mono_BufAC_Cmt_F: "mono BufAC_Cmt_F" 

160 
by (unfold mono_def BufAC_Cmt_F_def, fast) 

161 

19763  162 
lemmas BufAC_Cmt_fix = 
163 
mono_BufAC_Cmt_F [THEN BufAC_Cmt_def [THEN eq_reflection, THEN def_gfp_unfold]] 

19759  164 

165 
lemma BufAC_Cmt_unfold: "((s,t):BufAC_Cmt) = (!d x. 

166 
(s = <> > t = <>) & 

167 
(s = Md d\<leadsto><> > t = <>) & 

168 
(s = Md d\<leadsto>\<bullet>\<leadsto>x > ft\<cdot>t = Def d & (x, rt\<cdot>t):BufAC_Cmt))" 

169 
apply (subst BufAC_Cmt_fix [THEN set_cong]) 

170 
apply (unfold BufAC_Cmt_F_def) 

171 
apply (simp) 

172 
done 

173 

174 
lemma BufAC_Cmt_empty: "f:BufEq ==> (<>, f\<cdot><>):BufAC_Cmt" 

175 
by (rule BufAC_Cmt_unfold [THEN iffD2], auto simp add: Buf_f_empty) 

176 

177 
lemma BufAC_Cmt_d: "f:BufEq ==> (a\<leadsto>\<bottom>, f\<cdot>(a\<leadsto>\<bottom>)):BufAC_Cmt" 

178 
by (rule BufAC_Cmt_unfold [THEN iffD2], auto simp add: Buf_f_d) 

179 

180 
lemma BufAC_Cmt_d2: 

181 
"(Md d\<leadsto>\<bottom>, f\<cdot>(Md d\<leadsto>\<bottom>)):BufAC_Cmt ==> f\<cdot>(Md d\<leadsto>\<bottom>) = \<bottom>" 

182 
by (drule BufAC_Cmt_unfold [THEN iffD1], auto) 

183 

184 
lemma BufAC_Cmt_d3: 

185 
"(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" 

186 
by (drule BufAC_Cmt_unfold [THEN iffD1], auto) 

187 

188 
lemma BufAC_Cmt_d32: 

189 
"(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" 

190 
by (drule BufAC_Cmt_unfold [THEN iffD1], auto) 

191 

192 
(**** BufAC *******************************************************************) 

193 

194 
lemma BufAC_f_d: "f \<in> BufAC \<Longrightarrow> f\<cdot>(Md d\<leadsto>\<bottom>) = \<bottom>" 

195 
apply (unfold BufAC_def) 

196 
apply (fast intro: BufAC_Cmt_d2 BufAC_Asm_d) 

197 
done 

198 

199 
lemma ex_elim_lemma: "(? ff:B. (!x. f\<cdot>(a\<leadsto>b\<leadsto>x) = d\<leadsto>ff\<cdot>x)) = 

200 
((!x. ft\<cdot>(f\<cdot>(a\<leadsto>b\<leadsto>x)) = Def d) & (LAM x. rt\<cdot>(f\<cdot>(a\<leadsto>b\<leadsto>x))):B)" 

201 
(* this is an instance (though unification cannot handle this) of 

202 
lemma "(? ff:B. (!x. f\<cdot>x = d\<leadsto>ff\<cdot>x)) = \ 

203 
\((!x. ft\<cdot>(f\<cdot>x) = Def d) & (LAM x. rt\<cdot>(f\<cdot>x)):B)"*) 

204 
apply safe 

205 
apply ( rule_tac [2] P="(%x. x:B)" in ssubst) 

206 
prefer 3 

207 
apply ( assumption) 

40002
c5b5f7a3a3b1
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents:
35642
diff
changeset

208 
apply ( rule_tac [2] cfun_eqI) 
19759  209 
apply ( drule_tac [2] spec) 
210 
apply ( drule_tac [2] f="rt" in cfun_arg_cong) 

211 
prefer 2 

212 
apply ( simp) 

213 
prefer 2 

214 
apply ( simp) 

215 
apply (rule_tac bexI) 

216 
apply auto 

217 
apply (drule spec) 

218 
apply (erule exE) 

219 
apply (erule ssubst) 

220 
apply (simp) 

221 
done 

222 

223 
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" 

224 
apply (unfold BufAC_def) 

225 
apply (rule ex_elim_lemma [THEN iffD2]) 

226 
apply safe 

227 
apply (fast intro: BufAC_Cmt_d32 [THEN Def_maximal] 

228 
monofun_cfun_arg BufAC_Asm_empty [THEN BufAC_Asm_d_req]) 

229 
apply (auto intro: BufAC_Cmt_d3 BufAC_Asm_d_req) 

230 
done 

231 

232 

233 
(**** BufSt *******************************************************************) 

234 

235 
lemma mono_BufSt_F: "mono BufSt_F" 

236 
by (unfold mono_def BufSt_F_def, fast) 

237 

19763  238 
lemmas BufSt_P_fix = 
239 
mono_BufSt_F [THEN BufSt_P_def [THEN eq_reflection, THEN def_gfp_unfold]] 

19759  240 

241 
lemma BufSt_P_unfold: "(h:BufSt_P) = (!s. h s\<cdot><> = <> & 

242 
(!d x. h \<currency> \<cdot>(Md d\<leadsto>x) = h (Sd d)\<cdot>x & 

243 
(? hh:BufSt_P. h (Sd d)\<cdot>(\<bullet>\<leadsto>x) = d\<leadsto>(hh \<currency> \<cdot>x))))" 

244 
apply (subst BufSt_P_fix [THEN set_cong]) 

245 
apply (unfold BufSt_F_def) 

246 
apply (simp) 

247 
done 

248 

249 
lemma BufSt_P_empty: "h:BufSt_P ==> h s \<cdot> <> = <>" 

250 
by (drule BufSt_P_unfold [THEN iffD1], auto) 

251 
lemma BufSt_P_d: "h:BufSt_P ==> h \<currency> \<cdot>(Md d\<leadsto>x) = h (Sd d)\<cdot>x" 

252 
by (drule BufSt_P_unfold [THEN iffD1], auto) 

253 
lemma BufSt_P_d_req: "h:BufSt_P ==> \<exists>hh\<in>BufSt_P. 

254 
h (Sd d)\<cdot>(\<bullet> \<leadsto>x) = d\<leadsto>(hh \<currency> \<cdot>x)" 

255 
by (drule BufSt_P_unfold [THEN iffD1], auto) 

256 

257 

258 
(**** Buf_AC_imp_Eq ***********************************************************) 

259 

260 
lemma Buf_AC_imp_Eq: "BufAC \<subseteq> BufEq" 

261 
apply (unfold BufEq_def) 

262 
apply (rule gfp_upperbound) 

263 
apply (unfold BufEq_F_def) 

264 
apply safe 

265 
apply (erule BufAC_f_d) 

266 
apply (drule BufAC_f_d_req) 

267 
apply (fast) 

268 
done 

269 

270 

271 
(**** Buf_Eq_imp_AC by coinduction ********************************************) 

272 

273 
lemma BufAC_Asm_cong_lemma [rule_format]: "\<forall>s f ff. f\<in>BufEq \<longrightarrow> ff\<in>BufEq \<longrightarrow> 

274 
s\<in>BufAC_Asm \<longrightarrow> stream_take n\<cdot>(f\<cdot>s) = stream_take n\<cdot>(ff\<cdot>s)" 

275 
apply (induct_tac "n") 

276 
apply (simp) 

277 
apply (intro strip) 

278 
apply (drule BufAC_Asm_unfold [THEN iffD1]) 

279 
apply safe 

280 
apply (simp add: Buf_f_empty) 

281 
apply (simp add: Buf_f_d) 

282 
apply (drule ft_eq [THEN iffD1]) 

283 
apply (clarsimp) 

284 
apply (drule Buf_f_d_req)+ 

285 
apply safe 

286 
apply (erule ssubst)+ 

287 
apply (simp (no_asm)) 

288 
apply (fast) 

289 
done 

290 

291 
lemma BufAC_Asm_cong: "\<lbrakk>f \<in> BufEq; ff \<in> BufEq; s \<in> BufAC_Asm\<rbrakk> \<Longrightarrow> f\<cdot>s = ff\<cdot>s" 

35642
f478d5a9d238
generate separate qualified theorem name for each type's reach and take_lemma
huffman
parents:
32156
diff
changeset

292 
apply (rule stream.take_lemma) 
19759  293 
apply (erule (2) BufAC_Asm_cong_lemma) 
294 
done 

295 

296 
lemma Buf_Eq_imp_AC_lemma: "\<lbrakk>f \<in> BufEq; x \<in> BufAC_Asm\<rbrakk> \<Longrightarrow> (x, f\<cdot>x) \<in> BufAC_Cmt" 

297 
apply (unfold BufAC_Cmt_def) 

298 
apply (rotate_tac) 

299 
apply (erule weak_coinduct_image) 

300 
apply (unfold BufAC_Cmt_F_def) 

301 
apply safe 

302 
apply (erule Buf_f_empty) 

303 
apply (erule Buf_f_d) 

304 
apply (drule Buf_f_d_req) 

305 
apply (clarsimp) 

306 
apply (erule exI) 

307 
apply (drule BufAC_Asm_prefix2) 

308 
apply (frule Buf_f_d_req) 

309 
apply (clarsimp) 

310 
apply (erule ssubst) 

311 
apply (simp) 

312 
apply (drule (2) BufAC_Asm_cong) 

313 
apply (erule subst) 

314 
apply (erule imageI) 

315 
done 

316 
lemma Buf_Eq_imp_AC: "BufEq \<subseteq> BufAC" 

317 
apply (unfold BufAC_def) 

318 
apply (clarify) 

319 
apply (erule (1) Buf_Eq_imp_AC_lemma) 

320 
done 

321 

322 
(**** Buf_Eq_eq_AC ************************************************************) 

323 

324 
lemmas Buf_Eq_eq_AC = Buf_AC_imp_Eq [THEN Buf_Eq_imp_AC [THEN subset_antisym]] 

325 

326 

327 
(**** alternative (not strictly) stronger version of Buf_Eq *******************) 

328 

329 
lemma Buf_Eq_alt_imp_Eq: "BufEq_alt \<subseteq> BufEq" 

330 
apply (unfold BufEq_def BufEq_alt_def) 

331 
apply (rule gfp_mono) 

332 
apply (unfold BufEq_F_def) 

333 
apply (fast) 

334 
done 

335 

336 
(* direct proof of "BufEq \<subseteq> BufEq_alt" seems impossible *) 

337 

338 

339 
lemma Buf_AC_imp_Eq_alt: "BufAC <= BufEq_alt" 

340 
apply (unfold BufEq_alt_def) 

341 
apply (rule gfp_upperbound) 

342 
apply (fast elim: BufAC_f_d BufAC_f_d_req) 

343 
done 

344 

345 
lemmas Buf_Eq_imp_Eq_alt = subset_trans [OF Buf_Eq_imp_AC Buf_AC_imp_Eq_alt] 

346 

347 
lemmas Buf_Eq_alt_eq = subset_antisym [OF Buf_Eq_alt_imp_Eq Buf_Eq_imp_Eq_alt] 

348 

349 

350 
(**** Buf_Eq_eq_St ************************************************************) 

351 

352 
lemma Buf_St_imp_Eq: "BufSt <= BufEq" 

353 
apply (unfold BufSt_def BufEq_def) 

354 
apply (rule gfp_upperbound) 

355 
apply (unfold BufEq_F_def) 

356 
apply safe 

357 
apply ( simp add: BufSt_P_d BufSt_P_empty) 

358 
apply (simp add: BufSt_P_d) 

359 
apply (drule BufSt_P_d_req) 

360 
apply (force) 

361 
done 

362 

363 
lemma Buf_Eq_imp_St: "BufEq <= BufSt" 

364 
apply (unfold BufSt_def BufSt_P_def) 

365 
apply safe 

366 
apply (rename_tac f) 

367 
apply (rule_tac x="\<lambda>s. case s of Sd d => \<Lambda> x. f\<cdot>(Md d\<leadsto>x) \<currency> => f" in bexI) 

368 
apply ( simp) 

369 
apply (erule weak_coinduct_image) 

370 
apply (unfold BufSt_F_def) 

371 
apply (simp) 

372 
apply safe 

373 
apply ( rename_tac "s") 

374 
apply ( induct_tac "s") 

375 
apply ( simp add: Buf_f_d) 

376 
apply ( simp add: Buf_f_empty) 

377 
apply ( simp) 

378 
apply (simp) 

379 
apply (rename_tac f d x) 

380 
apply (drule_tac d="d" and x="x" in Buf_f_d_req) 

381 
apply auto 

382 
done 

383 

384 
lemmas Buf_Eq_eq_St = Buf_St_imp_Eq [THEN Buf_Eq_imp_St [THEN subset_antisym]] 

385 

11350
4c55b020d6ee
added FOCUS including the OneElement Buffer by Manfred Broy
oheimb
parents:
diff
changeset

386 
end 