src/HOLCF/FOCUS/Buffer.thy
author haftmann
Mon, 26 Sep 2005 08:41:24 +0200
changeset 17646 c5a4fe81857e
parent 17293 ecf182ccc3ca
child 19759 2d0896653e7a
permissions -rw-r--r--
adjusted web link
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
17293
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15038
diff changeset
     1
(*  Title:      HOLCF/FOCUS/Buffer.thy
11355
wenzelm
parents: 11350
diff changeset
     2
    ID:         $Id$
17293
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15038
diff changeset
     3
    Author:     David von Oheimb, TU Muenchen
11350
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
     4
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
     5
Formalization of section 4 of
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
     6
15038
eb2469e495cd corrected bibtex entry
oheimb
parents: 14981
diff changeset
     7
@inproceedings {broy_mod94,
eb2469e495cd corrected bibtex entry
oheimb
parents: 14981
diff changeset
     8
    author = {Manfred Broy},
eb2469e495cd corrected bibtex entry
oheimb
parents: 14981
diff changeset
     9
    title = {{Specification and Refinement of a Buffer of Length One}},
eb2469e495cd corrected bibtex entry
oheimb
parents: 14981
diff changeset
    10
    booktitle = {Deductive Program Design},
eb2469e495cd corrected bibtex entry
oheimb
parents: 14981
diff changeset
    11
    year = {1994},
eb2469e495cd corrected bibtex entry
oheimb
parents: 14981
diff changeset
    12
    editor = {Manfred Broy},
eb2469e495cd corrected bibtex entry
oheimb
parents: 14981
diff changeset
    13
    volume = {152},
eb2469e495cd corrected bibtex entry
oheimb
parents: 14981
diff changeset
    14
    series = {ASI Series, Series F: Computer and System Sciences},
eb2469e495cd corrected bibtex entry
oheimb
parents: 14981
diff changeset
    15
    pages = {273 -- 304},
eb2469e495cd corrected bibtex entry
oheimb
parents: 14981
diff changeset
    16
    publisher = {Springer}
11350
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    17
}
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    18
17646
c5a4fe81857e adjusted web link
haftmann
parents: 17293
diff changeset
    19
Slides available from http://ddvo.net/talks/1-Buffer.ps.gz
15038
eb2469e495cd corrected bibtex entry
oheimb
parents: 14981
diff changeset
    20
11350
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    21
*)
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    22
17293
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15038
diff changeset
    23
theory Buffer
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15038
diff changeset
    24
imports FOCUS
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15038
diff changeset
    25
begin
11350
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    26
17293
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15038
diff changeset
    27
typedecl D
11350
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    28
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    29
datatype
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    30
17293
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15038
diff changeset
    31
  M     = Md D | Mreq ("\<bullet>")
11350
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    32
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    33
datatype
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    34
17293
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15038
diff changeset
    35
  State = Sd D | Snil ("\<currency>")
11350
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    36
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    37
types
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    38
17293
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15038
diff changeset
    39
  SPF11         = "M fstream \<rightarrow> D fstream"
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15038
diff changeset
    40
  SPEC11        = "SPF11 set"
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15038
diff changeset
    41
  SPSF11        = "State \<Rightarrow> SPF11"
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15038
diff changeset
    42
  SPECS11       = "SPSF11 set"
11350
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    43
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    44
consts
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    45
17293
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15038
diff changeset
    46
  BufEq_F       :: "SPEC11 \<Rightarrow> SPEC11"
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15038
diff changeset
    47
  BufEq         :: "SPEC11"
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15038
diff changeset
    48
  BufEq_alt     :: "SPEC11"
11350
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    49
17293
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15038
diff changeset
    50
  BufAC_Asm_F   :: " (M fstream set) \<Rightarrow> (M fstream set)"
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15038
diff changeset
    51
  BufAC_Asm     :: " (M fstream set)"
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15038
diff changeset
    52
  BufAC_Cmt_F   :: "((M fstream * D fstream) set) \<Rightarrow>
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15038
diff changeset
    53
                    ((M fstream * D fstream) set)"
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15038
diff changeset
    54
  BufAC_Cmt     :: "((M fstream * D fstream) set)"
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15038
diff changeset
    55
  BufAC         :: "SPEC11"
11350
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    56
17293
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15038
diff changeset
    57
  BufSt_F       :: "SPECS11 \<Rightarrow> SPECS11"
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15038
diff changeset
    58
  BufSt_P       :: "SPECS11"
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15038
diff changeset
    59
  BufSt         :: "SPEC11"
11350
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    60
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    61
defs
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    62
17293
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15038
diff changeset
    63
  BufEq_F_def:   "BufEq_F B \<equiv> {f. \<forall>d. f\<cdot>(Md d\<leadsto><>) = <> \<and>
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15038
diff changeset
    64
                                 (\<forall>x. \<exists>ff\<in>B. f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>x) = d\<leadsto>ff\<cdot>x)}"
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15038
diff changeset
    65
  BufEq_def:     "BufEq     \<equiv> gfp BufEq_F"
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15038
diff changeset
    66
  BufEq_alt_def: "BufEq_alt \<equiv> gfp (\<lambda>B. {f. \<forall>d. f\<cdot>(Md d\<leadsto><> ) = <> \<and>
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15038
diff changeset
    67
                                 (\<exists>ff\<in>B. (\<forall>x. f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>x) = d\<leadsto>ff\<cdot>x))})"
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15038
diff changeset
    68
  BufAC_Asm_F_def: "BufAC_Asm_F A \<equiv> {s. s = <> \<or>
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15038
diff changeset
    69
                  (\<exists>d x. s = Md d\<leadsto>x \<and> (x = <> \<or> (ft\<cdot>x = Def \<bullet> \<and> (rt\<cdot>x)\<in>A)))}"
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15038
diff changeset
    70
  BufAC_Asm_def: "BufAC_Asm \<equiv> gfp BufAC_Asm_F"
11350
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    71
17293
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15038
diff changeset
    72
  BufAC_Cmt_F_def: "BufAC_Cmt_F C \<equiv> {(s,t). \<forall>d x.
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15038
diff changeset
    73
                           (s = <>         \<longrightarrow>     t = <>                 ) \<and>
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15038
diff changeset
    74
                           (s = Md d\<leadsto><>   \<longrightarrow>     t = <>                 ) \<and>
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15038
diff changeset
    75
                           (s = Md d\<leadsto>\<bullet>\<leadsto>x \<longrightarrow> (ft\<cdot>t = Def d \<and> (x,rt\<cdot>t)\<in>C))}"
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15038
diff changeset
    76
  BufAC_Cmt_def: "BufAC_Cmt \<equiv> gfp BufAC_Cmt_F"
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15038
diff changeset
    77
  BufAC_def:     "BufAC \<equiv> {f. \<forall>x. x\<in>BufAC_Asm \<longrightarrow> (x,f\<cdot>x)\<in>BufAC_Cmt}"
11350
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    78
17293
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15038
diff changeset
    79
  BufSt_F_def:   "BufSt_F H \<equiv> {h. \<forall>s  . h s      \<cdot><>        = <>         \<and>
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15038
diff changeset
    80
                                 (\<forall>d x. h \<currency>     \<cdot>(Md d\<leadsto>x) = h (Sd d)\<cdot>x \<and>
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15038
diff changeset
    81
                                (\<exists>hh\<in>H. h (Sd d)\<cdot>(\<bullet>   \<leadsto>x) = d\<leadsto>(hh \<currency>\<cdot>x)))}"
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15038
diff changeset
    82
  BufSt_P_def:   "BufSt_P \<equiv> gfp BufSt_F"
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15038
diff changeset
    83
  BufSt_def:     "BufSt \<equiv> {f. \<exists>h\<in>BufSt_P. f = h \<currency>}"
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15038
diff changeset
    84
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15038
diff changeset
    85
ML {* use_legacy_bindings (the_context ()) *}
11350
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    86
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    87
end