isabelle: src/HOLCF/FOCUS/Buffer.thy@1fb24e545f88 (annotated)

11350 4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	1	(* Title: HOLCF/FOCUS/Buffer.thy
11355 778c369559d9 tuned wenzelm parents: 11350 diff changeset	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 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
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 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
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

author	huffman
	Thu, 31 Mar 2005 02:44:46 +0200
changeset 15638	1fb24e545f88
parent 15038	eb2469e495cd
child 17293	ecf182ccc3ca
permissions	-rw-r--r--