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