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