author  wenzelm 
Sun, 27 Nov 2011 23:06:59 +0100  
changeset 45653  63ed1be524eb 
parent 43924  1165fe965da8 
child 49521  06cb12198b92 
permissions  rwrr 
42151  1 
(* Title: HOL/HOLCF/FOCUS/Buffer_adm.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 

17293  5 
header {* Oneelement buffer, proof of Buf_Eq_imp_AC by induction + admissibility *} 
11350
4c55b020d6ee
added FOCUS including the OneElement Buffer by Manfred Broy
oheimb
parents:
diff
changeset

6 

17293  7 
theory Buffer_adm 
8 
imports Buffer Stream_adm 

9 
begin 

10 

43924  11 
declare enat_0 [simp] 
19759  12 

13 
lemma BufAC_Asm_d2: "a\<leadsto>s:BufAC_Asm ==> ? d. a=Md d" 

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

15 

16 
lemma BufAC_Asm_d3: 

17 
"a\<leadsto>b\<leadsto>s:BufAC_Asm ==> ? d. a=Md d & b=\<bullet> & s:BufAC_Asm" 

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

19 

20 
lemma BufAC_Asm_F_def3: 

21 
"(s:BufAC_Asm_F A) = (s=<>  

22 
(? d. ft\<cdot>s=Def(Md d)) & (rt\<cdot>s=<>  ft\<cdot>(rt\<cdot>s)=Def \<bullet> & rt\<cdot>(rt\<cdot>s):A))" 

23 
by (unfold BufAC_Asm_F_def, auto) 

24 

25 
lemma cont_BufAC_Asm_F: "down_cont BufAC_Asm_F" 

26 
by (auto simp add: down_cont_def BufAC_Asm_F_def3) 

27 

28 
lemma BufAC_Cmt_F_def3: 

29 
"((s,t):BufAC_Cmt_F C) = (!d x. 

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

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

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

33 
apply (unfold BufAC_Cmt_F_def) 

34 
apply (subgoal_tac "!d x. (s = Md d\<leadsto>\<bullet>\<leadsto>x > (? y. t = d\<leadsto>y & (x,y):C)) = 

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

36 
apply (simp) 

37 
apply (auto intro: surjectiv_scons [symmetric]) 

38 
done 

39 

40 
lemma cont_BufAC_Cmt_F: "down_cont BufAC_Cmt_F" 

41 
by (auto simp add: down_cont_def BufAC_Cmt_F_def3) 

42 

43 

44 
(**** adm_BufAC_Asm ***********************************************************) 

45 

46 
lemma BufAC_Asm_F_stream_monoP: "stream_monoP BufAC_Asm_F" 

47 
apply (unfold BufAC_Asm_F_def stream_monoP_def) 

48 
apply (rule_tac x="{x. (? d. x = Md d\<leadsto>\<bullet>\<leadsto><>)}" in exI) 

49 
apply (rule_tac x="Suc (Suc 0)" in exI) 

50 
apply (clarsimp) 

51 
done 

52 

53 
lemma adm_BufAC_Asm: "adm (%x. x:BufAC_Asm)" 

54 
apply (unfold BufAC_Asm_def) 

55 
apply (rule cont_BufAC_Asm_F [THEN BufAC_Asm_F_stream_monoP [THEN fstream_gfp_admI]]) 

56 
done 

57 

58 

59 
(**** adm_non_BufAC_Asm *******************************************************) 

60 

61 
lemma BufAC_Asm_F_stream_antiP: "stream_antiP BufAC_Asm_F" 

62 
apply (unfold stream_antiP_def BufAC_Asm_F_def) 

63 
apply (intro strip) 

64 
apply (rule_tac x="{x. (? d. x = Md d\<leadsto>\<bullet>\<leadsto><>)}" in exI) 

65 
apply (rule_tac x="Suc (Suc 0)" in exI) 

66 
apply (rule conjI) 

67 
prefer 2 

68 
apply ( intro strip) 

69 
apply ( drule slen_mono) 

27101
864d29f11c9d
slightly tuning of some proofs involving case distinction and induction on natural numbers and similar
haftmann
parents:
26304
diff
changeset

70 
apply ( drule (1) order_trans) 
19759  71 
apply (force)+ 
72 
done 

73 

74 
lemma adm_non_BufAC_Asm: "adm (%u. u~:BufAC_Asm)" 

75 
apply (unfold BufAC_Asm_def) 

76 
apply (rule cont_BufAC_Asm_F [THEN BufAC_Asm_F_stream_antiP [THEN fstream_non_gfp_admI]]) 

77 
done 

78 

79 
(**** adm_BufAC ***************************************************************) 

80 

81 
(*adm_non_BufAC_Asm*) 

82 
lemma BufAC_Asm_cong [rule_format]: "!f ff. f:BufEq > ff:BufEq > s:BufAC_Asm > f\<cdot>s = ff\<cdot>s" 

83 
apply (rule fstream_ind2) 

84 
apply (simp add: adm_non_BufAC_Asm) 

85 
apply (force dest: Buf_f_empty) 

86 
apply (force dest!: BufAC_Asm_d2 

87 
dest: Buf_f_d elim: ssubst) 

88 
apply (safe dest!: BufAC_Asm_d3) 

89 
apply (drule Buf_f_d_req)+ 

90 
apply (fast elim: ssubst) 

91 
done 

92 

93 
(*adm_non_BufAC_Asm,BufAC_Asm_cong*) 

94 
lemma BufAC_Cmt_d_req: 

95 
"!!X. [f:BufEq; s:BufAC_Asm; (s, f\<cdot>s):BufAC_Cmt] ==> (a\<leadsto>b\<leadsto>s, f\<cdot>(a\<leadsto>b\<leadsto>s)):BufAC_Cmt" 

96 
apply (rule BufAC_Cmt_unfold [THEN iffD2]) 

97 
apply (intro strip) 

98 
apply (frule Buf_f_d_req) 

99 
apply (auto elim: BufAC_Asm_cong [THEN subst]) 

100 
done 

101 

102 
(*adm_BufAC_Asm*) 

103 
lemma BufAC_Asm_antiton: "antitonP BufAC_Asm" 

104 
apply (rule antitonPI) 

105 
apply (rule allI) 

106 
apply (rule fstream_ind2) 

107 
apply ( rule adm_lemmas)+ 

108 
apply ( rule cont_id) 

109 
apply ( rule adm_BufAC_Asm) 

110 
apply ( safe) 

111 
apply ( rule BufAC_Asm_empty) 

112 
apply ( force dest!: fstream_prefix 

113 
dest: BufAC_Asm_d2 intro: BufAC_Asm_d) 

114 
apply ( force dest!: fstream_prefix 

115 
dest: BufAC_Asm_d3 intro!: BufAC_Asm_d_req) 

116 
done 

117 

118 
(*adm_BufAC_Asm,BufAC_Asm_antiton,adm_non_BufAC_Asm,BufAC_Asm_cong*) 

43924  119 
lemma BufAC_Cmt_2stream_monoP: "f:BufEq ==> ? l. !i x s. s:BufAC_Asm > x << s > enat (l i) < #x > 
19759  120 
(x,f\<cdot>x):down_iterate BufAC_Cmt_F i > 
121 
(s,f\<cdot>s):down_iterate BufAC_Cmt_F i" 

122 
apply (rule_tac x="%i. 2*i" in exI) 

123 
apply (rule allI) 

124 
apply (induct_tac "i") 

125 
apply ( simp) 

126 
apply (simp add: add_commute) 

127 
apply (intro strip) 

128 
apply (subst BufAC_Cmt_F_def3) 

129 
apply (drule_tac P="%x. x" in BufAC_Cmt_F_def3 [THEN subst]) 

130 
apply safe 

131 
apply ( erule Buf_f_empty) 

132 
apply ( erule Buf_f_d) 

133 
apply ( drule Buf_f_d_req) 

134 
apply ( safe, erule ssubst, simp) 

135 
apply clarsimp 

136 
apply (rename_tac i d xa ya t) 

137 
(* 

138 
1. \<And>i d xa ya t. 

139 
\<lbrakk>f \<in> BufEq; 

140 
\<forall>x s. s \<in> BufAC_Asm \<longrightarrow> 

141 
x \<sqsubseteq> s \<longrightarrow> 

43924  142 
enat (2 * i) < #x \<longrightarrow> 
19759  143 
(x, f\<cdot>x) \<in> down_iterate BufAC_Cmt_F i \<longrightarrow> 
144 
(s, f\<cdot>s) \<in> down_iterate BufAC_Cmt_F i; 

43924  145 
Md d\<leadsto>\<bullet>\<leadsto>xa \<in> BufAC_Asm; enat (2 * i) < #ya; f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>ya) = d\<leadsto>t; 
19759  146 
(ya, t) \<in> down_iterate BufAC_Cmt_F i; ya \<sqsubseteq> xa\<rbrakk> 
147 
\<Longrightarrow> (xa, rt\<cdot>(f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>xa))) \<in> down_iterate BufAC_Cmt_F i 

148 
*) 

149 
apply (rotate_tac 2) 

150 
apply (drule BufAC_Asm_prefix2) 

151 
apply (frule Buf_f_d_req, erule exE, erule conjE, rotate_tac 1, erule ssubst) 

152 
apply (frule Buf_f_d_req, erule exE, erule conjE) 

153 
apply ( subgoal_tac "f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>ya) = d\<leadsto>ffa\<cdot>ya") 

154 
prefer 2 

155 
apply ( assumption) 

156 
apply ( rotate_tac 1) 

157 
apply ( simp) 

158 
apply (erule subst) 

159 
(* 

160 
1. \<And>i d xa ya t ff ffa. 

43924  161 
\<lbrakk>f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>ya) = d\<leadsto>ffa\<cdot>ya; enat (2 * i) < #ya; 
19759  162 
(ya, ffa\<cdot>ya) \<in> down_iterate BufAC_Cmt_F i; ya \<sqsubseteq> xa; f \<in> BufEq; 
163 
\<forall>x s. s \<in> BufAC_Asm \<longrightarrow> 

164 
x \<sqsubseteq> s \<longrightarrow> 

43924  165 
enat (2 * i) < #x \<longrightarrow> 
19759  166 
(x, f\<cdot>x) \<in> down_iterate BufAC_Cmt_F i \<longrightarrow> 
167 
(s, f\<cdot>s) \<in> down_iterate BufAC_Cmt_F i; 

168 
xa \<in> BufAC_Asm; ff \<in> BufEq; ffa \<in> BufEq\<rbrakk> 

169 
\<Longrightarrow> (xa, ff\<cdot>xa) \<in> down_iterate BufAC_Cmt_F i 

170 
*) 

171 
apply (drule spec, drule spec, drule (1) mp) 

172 
apply (drule (1) mp) 

173 
apply (drule (1) mp) 

174 
apply (erule impE) 

175 
apply ( subst BufAC_Asm_cong, assumption) 

176 
prefer 3 apply assumption 

177 
apply assumption 

178 
apply ( erule (1) BufAC_Asm_antiton [THEN antitonPD]) 

179 
apply (subst BufAC_Asm_cong, assumption) 

180 
prefer 3 apply assumption 

181 
apply assumption 

182 
apply assumption 

183 
done 

184 

185 
lemma BufAC_Cmt_iterate_all: "(x\<in>BufAC_Cmt) = (\<forall>n. x\<in>down_iterate BufAC_Cmt_F n)" 

186 
apply (unfold BufAC_Cmt_def) 

187 
apply (subst cont_BufAC_Cmt_F [THEN INTER_down_iterate_is_gfp]) 

188 
apply (fast) 

189 
done 

190 

191 
(*adm_BufAC_Asm,BufAC_Asm_antiton,adm_non_BufAC_Asm,BufAC_Asm_cong, 

192 
BufAC_Cmt_2stream_monoP*) 

193 
lemma adm_BufAC: "f:BufEq ==> adm (%s. s:BufAC_Asm > (s, f\<cdot>s):BufAC_Cmt)" 

194 
apply (rule flatstream_admI) 

195 
apply (subst BufAC_Cmt_iterate_all) 

196 
apply (drule BufAC_Cmt_2stream_monoP) 

197 
apply safe 

198 
apply (drule spec, erule exE) 

199 
apply (drule spec, erule impE) 

200 
apply (erule BufAC_Asm_antiton [THEN antitonPD]) 

201 
apply (erule is_ub_thelub) 

202 
apply (tactic "smp_tac 3 1") 

203 
apply (drule is_ub_thelub) 

204 
apply (drule (1) mp) 

205 
apply (drule (1) mp) 

206 
apply (erule mp) 

207 
apply (drule BufAC_Cmt_iterate_all [THEN iffD1]) 

208 
apply (erule spec) 

209 
done 

210 

211 

212 

213 
(**** Buf_Eq_imp_AC by induction **********************************************) 

214 

215 
(*adm_BufAC_Asm,BufAC_Asm_antiton,adm_non_BufAC_Asm,BufAC_Asm_cong, 

216 
BufAC_Cmt_2stream_monoP,adm_BufAC,BufAC_Cmt_d_req*) 

217 
lemma Buf_Eq_imp_AC: "BufEq <= BufAC" 

218 
apply (unfold BufAC_def) 

219 
apply (rule subsetI) 

220 
apply (simp) 

221 
apply (rule allI) 

222 
apply (rule fstream_ind2) 

223 
back 

224 
apply ( erule adm_BufAC) 

225 
apply ( safe) 

226 
apply ( erule BufAC_Cmt_empty) 

227 
apply ( erule BufAC_Cmt_d) 

228 
apply ( drule BufAC_Asm_prefix2) 

229 
apply ( simp) 

230 
apply (fast intro: BufAC_Cmt_d_req BufAC_Asm_prefix2) 

231 
done 

232 

233 
(**** new approach for admissibility, reduces itself to absurdity *************) 

234 

26304  235 
lemma adm_BufAC_Asm': "adm (\<lambda>x. x\<in>BufAC_Asm)" 
19759  236 
apply (rule def_gfp_admI) 
19763  237 
apply (rule BufAC_Asm_def [THEN eq_reflection]) 
19759  238 
apply (safe) 
239 
apply (unfold BufAC_Asm_F_def) 

240 
apply (safe) 

241 
apply (erule contrapos_np) 

242 
apply (drule fstream_exhaust_eq [THEN iffD1]) 

243 
apply (clarsimp) 

244 
apply (drule (1) fstream_lub_lemma) 

245 
apply (clarify) 

246 
apply (erule_tac x="j" in all_dupE) 

247 
apply (simp) 

248 
apply (drule BufAC_Asm_d2) 

249 
apply (clarify) 

250 
apply (simp) 

251 
apply (rule disjCI) 

252 
apply (erule contrapos_np) 

253 
apply (drule fstream_exhaust_eq [THEN iffD1]) 

254 
apply (clarsimp) 

255 
apply (drule (1) fstream_lub_lemma) 

256 
apply (clarsimp) 

45653  257 
apply (simp only: ex_simps [symmetric] all_simps [symmetric]) 
19759  258 
apply (rule_tac x="Xa" in exI) 
259 
apply (rule allI) 

260 
apply (rotate_tac 1) 

261 
apply (erule_tac x="i" in allE) 

262 
apply (clarsimp) 

263 
apply (erule_tac x="jb" in allE) 

264 
apply (clarsimp) 

265 
apply (erule_tac x="jc" in allE) 

266 
apply (clarsimp dest!: BufAC_Asm_d3) 

267 
done 

268 

269 
lemma adm_non_BufAC_Asm': "adm (\<lambda>u. u \<notin> BufAC_Asm)" (* uses antitonP *) 

270 
apply (rule def_gfp_adm_nonP) 

19763  271 
apply (rule BufAC_Asm_def [THEN eq_reflection]) 
19759  272 
apply (unfold BufAC_Asm_F_def) 
273 
apply (safe) 

274 
apply (erule contrapos_np) 

275 
apply (drule fstream_exhaust_eq [THEN iffD1]) 

276 
apply (clarsimp) 

277 
apply (frule fstream_prefix) 

278 
apply (clarsimp) 

279 
apply (frule BufAC_Asm_d2) 

280 
apply (clarsimp) 

281 
apply (rotate_tac 1) 

282 
apply (erule contrapos_pp) 

283 
apply (drule fstream_exhaust_eq [THEN iffD1]) 

284 
apply (clarsimp) 

285 
apply (frule fstream_prefix) 

286 
apply (clarsimp) 

287 
apply (frule BufAC_Asm_d3) 

288 
apply (force) 

289 
done 

290 

291 
lemma adm_BufAC': "f \<in> BufEq \<Longrightarrow> adm (\<lambda>u. u \<in> BufAC_Asm \<longrightarrow> (u, f\<cdot>u) \<in> BufAC_Cmt)" 

292 
apply (rule triv_admI) 

293 
apply (clarify) 

294 
apply (erule (1) Buf_Eq_imp_AC_lemma) 

295 
(* this is what we originally aimed to show, using admissibilty :( *) 

296 
done 

297 

17293  298 
end 
299 

300 