isabelle: src/HOLCF/IOA/ABP/Env.thy@8fc3d7237e03 (annotated)

3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	1	(* Title: HOLCF/IOA/ABP/Impl.thy
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	2	ID: $Id$
12218 6597093b77e7 GPLed; wenzelm parents: 6468 diff changeset	3	Author: Olaf M�ller
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	4	*)
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	5
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	6	header {* The environment *}
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	7
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	8	theory Env
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	9	imports IOA Action
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	10	begin
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	11
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	12	types
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	13	'm env_state = bool -- {* give next bit to system *}
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	14
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	15	constdefs
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	16	env_asig :: "'m action signature"
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	17	"env_asig == ({Next},
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	18	UN m. {S_msg(m)},
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	19	{})"
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	20
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	21	env_trans :: "('m action, 'm env_state)transition set"
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	22	"env_trans ==
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	23	{tr. let s = fst(tr);
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	24	t = snd(snd(tr))
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	25	in case fst(snd(tr))
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	26	of
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	27	Next => t=True \|
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	28	S_msg(m) => s=True & t=False \|
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	29	R_msg(m) => False \|
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	30	S_pkt(pkt) => False \|
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	31	R_pkt(pkt) => False \|
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	32	S_ack(b) => False \|
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	33	R_ack(b) => False}"
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	34
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	35	env_ioa :: "('m action, 'm env_state)ioa"
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	36	"env_ioa == (env_asig, {True}, env_trans,{},{})"
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	37
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	38	consts
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	39	"next" :: "'m env_state => bool"
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	40
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	41	end

author	haftmann
	Tue, 20 Mar 2007 15:52:39 +0100
changeset 22482	8fc3d7237e03
parent 19738	1ac610922636
child 25131	2c8caac48ade
permissions	-rw-r--r--