isabelle: src/HOL/TLA/Buffer/DBuffer.thy@b3e7da94b51f (annotated)

3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	1	(*
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	2	File: DBuffer.thy
17309 c43ed29bd197 converted to Isar theory format; wenzelm parents: 6255 diff changeset	3	ID: $Id$
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	4	Author: Stephan Merz
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	5	Copyright: 1997 University of Munich
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	6
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	7	Theory Name: DBuffer
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	8	Logic Image: TLA
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	9	*)
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	10
17309 c43ed29bd197 converted to Isar theory format; wenzelm parents: 6255 diff changeset	11	header {* Two FIFO buffers in a row, with interleaving assumption *}
c43ed29bd197 converted to Isar theory format; wenzelm parents: 6255 diff changeset	12
c43ed29bd197 converted to Isar theory format; wenzelm parents: 6255 diff changeset	13	theory DBuffer
c43ed29bd197 converted to Isar theory format; wenzelm parents: 6255 diff changeset	14	imports Buffer
c43ed29bd197 converted to Isar theory format; wenzelm parents: 6255 diff changeset	15	begin
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	16
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	17	consts
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	18	(* implementation variables *)
17309 c43ed29bd197 converted to Isar theory format; wenzelm parents: 6255 diff changeset	19	inp :: "nat stfun"
c43ed29bd197 converted to Isar theory format; wenzelm parents: 6255 diff changeset	20	mid :: "nat stfun"
c43ed29bd197 converted to Isar theory format; wenzelm parents: 6255 diff changeset	21	out :: "nat stfun"
c43ed29bd197 converted to Isar theory format; wenzelm parents: 6255 diff changeset	22	q1 :: "nat list stfun"
c43ed29bd197 converted to Isar theory format; wenzelm parents: 6255 diff changeset	23	q2 :: "nat list stfun"
c43ed29bd197 converted to Isar theory format; wenzelm parents: 6255 diff changeset	24	qc :: "nat list stfun"
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	25
17309 c43ed29bd197 converted to Isar theory format; wenzelm parents: 6255 diff changeset	26	DBInit :: stpred
c43ed29bd197 converted to Isar theory format; wenzelm parents: 6255 diff changeset	27	DBEnq :: action
c43ed29bd197 converted to Isar theory format; wenzelm parents: 6255 diff changeset	28	DBDeq :: action
c43ed29bd197 converted to Isar theory format; wenzelm parents: 6255 diff changeset	29	DBPass :: action
c43ed29bd197 converted to Isar theory format; wenzelm parents: 6255 diff changeset	30	DBNext :: action
c43ed29bd197 converted to Isar theory format; wenzelm parents: 6255 diff changeset	31	DBuffer :: temporal
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	32
17309 c43ed29bd197 converted to Isar theory format; wenzelm parents: 6255 diff changeset	33	axioms
c43ed29bd197 converted to Isar theory format; wenzelm parents: 6255 diff changeset	34	DB_base: "basevars (inp,mid,out,q1,q2)"
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	35
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	36	(* the concatenation of the two buffers *)
17309 c43ed29bd197 converted to Isar theory format; wenzelm parents: 6255 diff changeset	37	qc_def: "PRED qc == PRED (q2 @ q1)"
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	38
17309 c43ed29bd197 converted to Isar theory format; wenzelm parents: 6255 diff changeset	39	DBInit_def: "DBInit == PRED (BInit inp q1 mid & BInit mid q2 out)"
c43ed29bd197 converted to Isar theory format; wenzelm parents: 6255 diff changeset	40	DBEnq_def: "DBEnq == ACT Enq inp q1 mid & unchanged (q2,out)"
c43ed29bd197 converted to Isar theory format; wenzelm parents: 6255 diff changeset	41	DBDeq_def: "DBDeq == ACT Deq mid q2 out & unchanged (inp,q1)"
c43ed29bd197 converted to Isar theory format; wenzelm parents: 6255 diff changeset	42	DBPass_def: "DBPass == ACT Deq inp q1 mid
6255 db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	43	& (q2$ = $q2 @ [ mid$ ])
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	44	& (out$ = $out)"
17309 c43ed29bd197 converted to Isar theory format; wenzelm parents: 6255 diff changeset	45	DBNext_def: "DBNext == ACT (DBEnq \| DBDeq \| DBPass)"
c43ed29bd197 converted to Isar theory format; wenzelm parents: 6255 diff changeset	46	DBuffer_def: "DBuffer == TEMP Init DBInit
6255 db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	47	& [][DBNext]_(inp,mid,out,q1,q2)
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	48	& WF(DBDeq)_(inp,mid,out,q1,q2)
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	49	& WF(DBPass)_(inp,mid,out,q1,q2)"
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	50
17309 c43ed29bd197 converted to Isar theory format; wenzelm parents: 6255 diff changeset	51	ML {* use_legacy_bindings (the_context ()) *}
c43ed29bd197 converted to Isar theory format; wenzelm parents: 6255 diff changeset	52
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	53	end

author	urbanc
	Tue, 13 Dec 2005 18:11:21 +0100
changeset 18396	b3e7da94b51f
parent 17309	c43ed29bd197
child 21624	6f79647cf536
permissions	-rw-r--r--