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