|
1 (* Title: HOLCF/FOCUS/Buffer.thy |
|
2 ID: $ $ |
|
3 Author: David von Oheimb, TU Muenchen |
|
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
5 |
|
6 Formalization of section 4 of |
|
7 |
|
8 @inproceedings{Broy95-SRBLO, |
|
9 author = {Manfred Broy}, |
|
10 title = {Specification and ReFinement of a Buffer of Length One}, |
|
11 booktitle = {Working Material of Marktoberdorf Summer School}, |
|
12 year = {1994}, |
|
13 publisher = {}, |
|
14 editor = {}, |
|
15 note = {\url{http://www4.in.tum.de/papers/broy_mod94.html}} |
|
16 } |
|
17 |
|
18 Slides available from http://isabelle.in.tum.de/HOLCF/1-Buffer.ps.gz |
|
19 *) |
|
20 |
|
21 Buffer = FOCUS + |
|
22 |
|
23 types D |
|
24 arities D::term |
|
25 |
|
26 datatype |
|
27 |
|
28 M = Md D | Mreq ("\\<bullet>") |
|
29 |
|
30 datatype |
|
31 |
|
32 State = Sd D | Snil ("\\<currency>") |
|
33 |
|
34 types |
|
35 |
|
36 SPF11 = "M fstream \\<rightarrow> D fstream" |
|
37 SPEC11 = "SPF11 set" |
|
38 SPSF11 = "State \\<Rightarrow> SPF11" |
|
39 SPECS11 = "SPSF11 set" |
|
40 |
|
41 consts |
|
42 |
|
43 BufEq_F :: "SPEC11 \\<Rightarrow> SPEC11" |
|
44 BufEq :: "SPEC11" |
|
45 BufEq_alt :: "SPEC11" |
|
46 |
|
47 BufAC_Asm_F :: " (M fstream set) \\<Rightarrow> (M fstream set)" |
|
48 BufAC_Asm :: " (M fstream set)" |
|
49 BufAC_Cmt_F :: "((M fstream * D fstream) set) \\<Rightarrow> \ |
|
50 \ ((M fstream * D fstream) set)" |
|
51 BufAC_Cmt :: "((M fstream * D fstream) set)" |
|
52 BufAC :: "SPEC11" |
|
53 |
|
54 BufSt_F :: "SPECS11 \\<Rightarrow> SPECS11" |
|
55 BufSt_P :: "SPECS11" |
|
56 BufSt :: "SPEC11" |
|
57 |
|
58 defs |
|
59 |
|
60 BufEq_F_def "BufEq_F B \\<equiv> {f. \\<forall>d. f\\<cdot>(Md d\\<leadsto><>) = <> \\<and> |
|
61 (\\<forall>x. \\<exists>ff\\<in>B. f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>x) = d\\<leadsto>ff\\<cdot>x)}" |
|
62 BufEq_def "BufEq \\<equiv> gfp BufEq_F" |
|
63 BufEq_alt_def "BufEq_alt \\<equiv> gfp (\\<lambda>B. {f. \\<forall>d. f\\<cdot>(Md d\\<leadsto><> ) = <> \\<and> |
|
64 (\\<exists>ff\\<in>B. (\\<forall>x. f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>x) = d\\<leadsto>ff\\<cdot>x))})" |
|
65 BufAC_Asm_F_def "BufAC_Asm_F A \\<equiv> {s. s = <> \\<or> |
|
66 (\\<exists>d x. s = Md d\\<leadsto>x \\<and> (x = <> \\<or> (ft\\<cdot>x = Def \\<bullet> \\<and> (rt\\<cdot>x)\\<in>A)))}" |
|
67 BufAC_Asm_def "BufAC_Asm \\<equiv> gfp BufAC_Asm_F" |
|
68 |
|
69 BufAC_Cmt_F_def "BufAC_Cmt_F C \\<equiv> {(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 BufAC_Cmt_def "BufAC_Cmt \\<equiv> gfp BufAC_Cmt_F" |
|
74 BufAC_def "BufAC \\<equiv> {f. \\<forall>x. x\\<in>BufAC_Asm \\<longrightarrow> (x,f\\<cdot>x)\\<in>BufAC_Cmt}" |
|
75 |
|
76 BufSt_F_def "BufSt_F H \\<equiv> {h. \\<forall>s . h s \\<cdot><> = <> \\<and> |
|
77 (\\<forall>d x. h \\<currency> \\<cdot>(Md d\\<leadsto>x) = h (Sd d)\\<cdot>x \\<and> |
|
78 (\\<exists>hh\\<in>H. h (Sd d)\\<cdot>(\\<bullet> \\<leadsto>x) = d\\<leadsto>(hh \\<currency>\\<cdot>x)))}" |
|
79 BufSt_P_def "BufSt_P \\<equiv> gfp BufSt_F" |
|
80 BufSt_def "BufSt \\<equiv> {f. \\<exists>h\\<in>BufSt_P. f = h \\<currency>}" |
|
81 |
|
82 end |