--- a/src/HOLCF/FOCUS/Buffer.thy Tue Sep 06 20:53:27 2005 +0200
+++ b/src/HOLCF/FOCUS/Buffer.thy Tue Sep 06 21:51:17 2005 +0200
@@ -1,6 +1,6 @@
-(* Title: HOLCF/FOCUS/Buffer.thy
+(* Title: HOLCF/FOCUS/Buffer.thy
ID: $Id$
- Author: David von Oheimb, TU Muenchen
+ Author: David von Oheimb, TU Muenchen
Formalization of section 4 of
@@ -20,65 +20,68 @@
*)
-Buffer = FOCUS +
+theory Buffer
+imports FOCUS
+begin
-types D
-arities D :: type
+typedecl D
datatype
- M = Md D | Mreq ("\\<bullet>")
+ M = Md D | Mreq ("\<bullet>")
datatype
- State = Sd D | Snil ("\\<currency>")
+ State = Sd D | Snil ("\<currency>")
types
- SPF11 = "M fstream \\<rightarrow> D fstream"
- SPEC11 = "SPF11 set"
- SPSF11 = "State \\<Rightarrow> SPF11"
- SPECS11 = "SPSF11 set"
+ SPF11 = "M fstream \<rightarrow> D fstream"
+ SPEC11 = "SPF11 set"
+ SPSF11 = "State \<Rightarrow> SPF11"
+ SPECS11 = "SPSF11 set"
consts
- BufEq_F :: "SPEC11 \\<Rightarrow> SPEC11"
- BufEq :: "SPEC11"
- BufEq_alt :: "SPEC11"
+ BufEq_F :: "SPEC11 \<Rightarrow> SPEC11"
+ BufEq :: "SPEC11"
+ BufEq_alt :: "SPEC11"
- BufAC_Asm_F :: " (M fstream set) \\<Rightarrow> (M fstream set)"
- BufAC_Asm :: " (M fstream set)"
- BufAC_Cmt_F :: "((M fstream * D fstream) set) \\<Rightarrow> \
-\ ((M fstream * D fstream) set)"
- BufAC_Cmt :: "((M fstream * D fstream) set)"
- BufAC :: "SPEC11"
+ BufAC_Asm_F :: " (M fstream set) \<Rightarrow> (M fstream set)"
+ BufAC_Asm :: " (M fstream set)"
+ BufAC_Cmt_F :: "((M fstream * D fstream) set) \<Rightarrow>
+ ((M fstream * D fstream) set)"
+ BufAC_Cmt :: "((M fstream * D fstream) set)"
+ BufAC :: "SPEC11"
- BufSt_F :: "SPECS11 \\<Rightarrow> SPECS11"
- BufSt_P :: "SPECS11"
- BufSt :: "SPEC11"
+ BufSt_F :: "SPECS11 \<Rightarrow> SPECS11"
+ BufSt_P :: "SPECS11"
+ BufSt :: "SPEC11"
defs
- BufEq_F_def "BufEq_F B \\<equiv> {f. \\<forall>d. f\\<cdot>(Md d\\<leadsto><>) = <> \\<and>
- (\\<forall>x. \\<exists>ff\\<in>B. f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>x) = d\\<leadsto>ff\\<cdot>x)}"
- BufEq_def "BufEq \\<equiv> gfp BufEq_F"
- BufEq_alt_def "BufEq_alt \\<equiv> gfp (\\<lambda>B. {f. \\<forall>d. f\\<cdot>(Md d\\<leadsto><> ) = <> \\<and>
- (\\<exists>ff\\<in>B. (\\<forall>x. f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>x) = d\\<leadsto>ff\\<cdot>x))})"
- BufAC_Asm_F_def "BufAC_Asm_F A \\<equiv> {s. s = <> \\<or>
- (\\<exists>d x. s = Md d\\<leadsto>x \\<and> (x = <> \\<or> (ft\\<cdot>x = Def \\<bullet> \\<and> (rt\\<cdot>x)\\<in>A)))}"
- BufAC_Asm_def "BufAC_Asm \\<equiv> gfp BufAC_Asm_F"
+ BufEq_F_def: "BufEq_F B \<equiv> {f. \<forall>d. f\<cdot>(Md d\<leadsto><>) = <> \<and>
+ (\<forall>x. \<exists>ff\<in>B. f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>x) = d\<leadsto>ff\<cdot>x)}"
+ BufEq_def: "BufEq \<equiv> gfp BufEq_F"
+ BufEq_alt_def: "BufEq_alt \<equiv> gfp (\<lambda>B. {f. \<forall>d. f\<cdot>(Md d\<leadsto><> ) = <> \<and>
+ (\<exists>ff\<in>B. (\<forall>x. f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>x) = d\<leadsto>ff\<cdot>x))})"
+ BufAC_Asm_F_def: "BufAC_Asm_F A \<equiv> {s. s = <> \<or>
+ (\<exists>d x. s = Md d\<leadsto>x \<and> (x = <> \<or> (ft\<cdot>x = Def \<bullet> \<and> (rt\<cdot>x)\<in>A)))}"
+ BufAC_Asm_def: "BufAC_Asm \<equiv> gfp BufAC_Asm_F"
- BufAC_Cmt_F_def "BufAC_Cmt_F C \\<equiv> {(s,t). \\<forall>d x.
- (s = <> \\<longrightarrow> t = <> ) \\<and>
- (s = Md d\\<leadsto><> \\<longrightarrow> t = <> ) \\<and>
- (s = Md d\\<leadsto>\\<bullet>\\<leadsto>x \\<longrightarrow> (ft\\<cdot>t = Def d \\<and> (x,rt\\<cdot>t)\\<in>C))}"
- BufAC_Cmt_def "BufAC_Cmt \\<equiv> gfp BufAC_Cmt_F"
- BufAC_def "BufAC \\<equiv> {f. \\<forall>x. x\\<in>BufAC_Asm \\<longrightarrow> (x,f\\<cdot>x)\\<in>BufAC_Cmt}"
+ BufAC_Cmt_F_def: "BufAC_Cmt_F C \<equiv> {(s,t). \<forall>d x.
+ (s = <> \<longrightarrow> t = <> ) \<and>
+ (s = Md d\<leadsto><> \<longrightarrow> t = <> ) \<and>
+ (s = Md d\<leadsto>\<bullet>\<leadsto>x \<longrightarrow> (ft\<cdot>t = Def d \<and> (x,rt\<cdot>t)\<in>C))}"
+ BufAC_Cmt_def: "BufAC_Cmt \<equiv> gfp BufAC_Cmt_F"
+ BufAC_def: "BufAC \<equiv> {f. \<forall>x. x\<in>BufAC_Asm \<longrightarrow> (x,f\<cdot>x)\<in>BufAC_Cmt}"
- BufSt_F_def "BufSt_F H \\<equiv> {h. \\<forall>s . h s \\<cdot><> = <> \\<and>
- (\\<forall>d x. h \\<currency> \\<cdot>(Md d\\<leadsto>x) = h (Sd d)\\<cdot>x \\<and>
- (\\<exists>hh\\<in>H. h (Sd d)\\<cdot>(\\<bullet> \\<leadsto>x) = d\\<leadsto>(hh \\<currency>\\<cdot>x)))}"
- BufSt_P_def "BufSt_P \\<equiv> gfp BufSt_F"
- BufSt_def "BufSt \\<equiv> {f. \\<exists>h\\<in>BufSt_P. f = h \\<currency>}"
+ BufSt_F_def: "BufSt_F H \<equiv> {h. \<forall>s . h s \<cdot><> = <> \<and>
+ (\<forall>d x. h \<currency> \<cdot>(Md d\<leadsto>x) = h (Sd d)\<cdot>x \<and>
+ (\<exists>hh\<in>H. h (Sd d)\<cdot>(\<bullet> \<leadsto>x) = d\<leadsto>(hh \<currency>\<cdot>x)))}"
+ BufSt_P_def: "BufSt_P \<equiv> gfp BufSt_F"
+ BufSt_def: "BufSt \<equiv> {f. \<exists>h\<in>BufSt_P. f = h \<currency>}"
+
+ML {* use_legacy_bindings (the_context ()) *}
end