author | wenzelm |
Tue, 06 Sep 2005 21:51:17 +0200 | |
changeset 17293 | ecf182ccc3ca |
parent 15038 | eb2469e495cd |
child 17646 | c5a4fe81857e |
permissions | -rw-r--r-- |
17293 | 1 |
(* Title: HOLCF/FOCUS/Buffer.thy |
11355 | 2 |
ID: $Id$ |
17293 | 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 | 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 |
|
17293 | 23 |
theory Buffer |
24 |
imports FOCUS |
|
25 |
begin |
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
26 |
|
17293 | 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 | 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 | 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 | 39 |
SPF11 = "M fstream \<rightarrow> D fstream" |
40 |
SPEC11 = "SPF11 set" |
|
41 |
SPSF11 = "State \<Rightarrow> SPF11" |
|
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 | 46 |
BufEq_F :: "SPEC11 \<Rightarrow> SPEC11" |
47 |
BufEq :: "SPEC11" |
|
48 |
BufEq_alt :: "SPEC11" |
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
49 |
|
17293 | 50 |
BufAC_Asm_F :: " (M fstream set) \<Rightarrow> (M fstream set)" |
51 |
BufAC_Asm :: " (M fstream set)" |
|
52 |
BufAC_Cmt_F :: "((M fstream * D fstream) set) \<Rightarrow> |
|
53 |
((M fstream * D fstream) set)" |
|
54 |
BufAC_Cmt :: "((M fstream * D fstream) set)" |
|
55 |
BufAC :: "SPEC11" |
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
56 |
|
17293 | 57 |
BufSt_F :: "SPECS11 \<Rightarrow> SPECS11" |
58 |
BufSt_P :: "SPECS11" |
|
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 | 63 |
BufEq_F_def: "BufEq_F B \<equiv> {f. \<forall>d. f\<cdot>(Md d\<leadsto><>) = <> \<and> |
64 |
(\<forall>x. \<exists>ff\<in>B. f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>x) = d\<leadsto>ff\<cdot>x)}" |
|
65 |
BufEq_def: "BufEq \<equiv> gfp BufEq_F" |
|
66 |
BufEq_alt_def: "BufEq_alt \<equiv> gfp (\<lambda>B. {f. \<forall>d. f\<cdot>(Md d\<leadsto><> ) = <> \<and> |
|
67 |
(\<exists>ff\<in>B. (\<forall>x. f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>x) = d\<leadsto>ff\<cdot>x))})" |
|
68 |
BufAC_Asm_F_def: "BufAC_Asm_F A \<equiv> {s. s = <> \<or> |
|
69 |
(\<exists>d x. s = Md d\<leadsto>x \<and> (x = <> \<or> (ft\<cdot>x = Def \<bullet> \<and> (rt\<cdot>x)\<in>A)))}" |
|
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 | 72 |
BufAC_Cmt_F_def: "BufAC_Cmt_F C \<equiv> {(s,t). \<forall>d x. |
73 |
(s = <> \<longrightarrow> t = <> ) \<and> |
|
74 |
(s = Md d\<leadsto><> \<longrightarrow> t = <> ) \<and> |
|
75 |
(s = Md d\<leadsto>\<bullet>\<leadsto>x \<longrightarrow> (ft\<cdot>t = Def d \<and> (x,rt\<cdot>t)\<in>C))}" |
|
76 |
BufAC_Cmt_def: "BufAC_Cmt \<equiv> gfp BufAC_Cmt_F" |
|
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 | 79 |
BufSt_F_def: "BufSt_F H \<equiv> {h. \<forall>s . h s \<cdot><> = <> \<and> |
80 |
(\<forall>d x. h \<currency> \<cdot>(Md d\<leadsto>x) = h (Sd d)\<cdot>x \<and> |
|
81 |
(\<exists>hh\<in>H. h (Sd d)\<cdot>(\<bullet> \<leadsto>x) = d\<leadsto>(hh \<currency>\<cdot>x)))}" |
|
82 |
BufSt_P_def: "BufSt_P \<equiv> gfp BufSt_F" |
|
83 |
BufSt_def: "BufSt \<equiv> {f. \<exists>h\<in>BufSt_P. f = h \<currency>}" |
|
84 |
||
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 |