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