author | schirmer |
Sun, 05 Jun 2005 13:49:51 +0200 | |
changeset 16272 | bcf05183df9e |
parent 15038 | eb2469e495cd |
child 17293 | ecf182ccc3ca |
permissions | -rw-r--r-- |
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
1 |
(* Title: HOLCF/FOCUS/Buffer.thy |
11355 | 2 |
ID: $Id$ |
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
3 |
Author: David von Oheimb, TU Muenchen |
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 | 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} |
|
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 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
19 |
Slides available from http://isabelle.in.tum.de/HOLCF/1-Buffer.ps.gz |
15038 | 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 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
23 |
Buffer = FOCUS + |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
24 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
25 |
types D |
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11355
diff
changeset
|
26 |
arities D :: type |
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
27 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
28 |
datatype |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
29 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
30 |
M = Md D | Mreq ("\\<bullet>") |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
31 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
32 |
datatype |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
33 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
34 |
State = Sd D | Snil ("\\<currency>") |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
35 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
36 |
types |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
37 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
38 |
SPF11 = "M fstream \\<rightarrow> D fstream" |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
39 |
SPEC11 = "SPF11 set" |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
40 |
SPSF11 = "State \\<Rightarrow> SPF11" |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
41 |
SPECS11 = "SPSF11 set" |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
42 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
43 |
consts |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
44 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
45 |
BufEq_F :: "SPEC11 \\<Rightarrow> SPEC11" |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
46 |
BufEq :: "SPEC11" |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
47 |
BufEq_alt :: "SPEC11" |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
48 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
49 |
BufAC_Asm_F :: " (M fstream set) \\<Rightarrow> (M fstream set)" |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
50 |
BufAC_Asm :: " (M fstream set)" |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
51 |
BufAC_Cmt_F :: "((M fstream * D fstream) set) \\<Rightarrow> \ |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
52 |
\ ((M fstream * D fstream) set)" |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
53 |
BufAC_Cmt :: "((M fstream * D fstream) set)" |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
54 |
BufAC :: "SPEC11" |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
55 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
56 |
BufSt_F :: "SPECS11 \\<Rightarrow> SPECS11" |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
57 |
BufSt_P :: "SPECS11" |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
58 |
BufSt :: "SPEC11" |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
59 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
60 |
defs |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
61 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
62 |
BufEq_F_def "BufEq_F B \\<equiv> {f. \\<forall>d. f\\<cdot>(Md d\\<leadsto><>) = <> \\<and> |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
63 |
(\\<forall>x. \\<exists>ff\\<in>B. f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>x) = d\\<leadsto>ff\\<cdot>x)}" |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
64 |
BufEq_def "BufEq \\<equiv> gfp BufEq_F" |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
65 |
BufEq_alt_def "BufEq_alt \\<equiv> gfp (\\<lambda>B. {f. \\<forall>d. f\\<cdot>(Md d\\<leadsto><> ) = <> \\<and> |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
66 |
(\\<exists>ff\\<in>B. (\\<forall>x. f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>x) = d\\<leadsto>ff\\<cdot>x))})" |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
67 |
BufAC_Asm_F_def "BufAC_Asm_F A \\<equiv> {s. s = <> \\<or> |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
68 |
(\\<exists>d x. s = Md d\\<leadsto>x \\<and> (x = <> \\<or> (ft\\<cdot>x = Def \\<bullet> \\<and> (rt\\<cdot>x)\\<in>A)))}" |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
69 |
BufAC_Asm_def "BufAC_Asm \\<equiv> gfp BufAC_Asm_F" |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
70 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
71 |
BufAC_Cmt_F_def "BufAC_Cmt_F C \\<equiv> {(s,t). \\<forall>d x. |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
72 |
(s = <> \\<longrightarrow> t = <> ) \\<and> |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
73 |
(s = Md d\\<leadsto><> \\<longrightarrow> t = <> ) \\<and> |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
74 |
(s = Md d\\<leadsto>\\<bullet>\\<leadsto>x \\<longrightarrow> (ft\\<cdot>t = Def d \\<and> (x,rt\\<cdot>t)\\<in>C))}" |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
75 |
BufAC_Cmt_def "BufAC_Cmt \\<equiv> gfp BufAC_Cmt_F" |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
76 |
BufAC_def "BufAC \\<equiv> {f. \\<forall>x. x\\<in>BufAC_Asm \\<longrightarrow> (x,f\\<cdot>x)\\<in>BufAC_Cmt}" |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
77 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
78 |
BufSt_F_def "BufSt_F H \\<equiv> {h. \\<forall>s . h s \\<cdot><> = <> \\<and> |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
79 |
(\\<forall>d x. h \\<currency> \\<cdot>(Md d\\<leadsto>x) = h (Sd d)\\<cdot>x \\<and> |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
80 |
(\\<exists>hh\\<in>H. h (Sd d)\\<cdot>(\\<bullet> \\<leadsto>x) = d\\<leadsto>(hh \\<currency>\\<cdot>x)))}" |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
81 |
BufSt_P_def "BufSt_P \\<equiv> gfp BufSt_F" |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
82 |
BufSt_def "BufSt \\<equiv> {f. \\<exists>h\\<in>BufSt_P. f = h \\<currency>}" |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
83 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
84 |
end |