isabelle: src/HOL/HOLCF/IOA/ABP/Env.thy@79f5e137779a (annotated)

42151 4da4fc77664b tuned headers; wenzelm parents: 41476 diff changeset	1	(* Title: HOL/HOLCF/IOA/ABP/Env.thy
40945 b8703f63bfb2 recoded latin1 as utf8; wenzelm parents: 40774 diff changeset	2	Author: Olaf Müller
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	3	*)
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	4
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	5	header {* The environment *}
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	6
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	7	theory Env
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	8	imports IOA Action
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	9	begin
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	10
41476 0fa9629aa399 types -> type_synonym huffman parents: 40945 diff changeset	11	type_synonym
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	12	'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	13
25131 2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	14	definition
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	15	env_asig :: "'m action signature" where
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	16	"env_asig == ({Next},
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	17	UN m. {S_msg(m)},
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	18	{})"
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	19
25131 2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	20	definition
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	21	env_trans :: "('m action, 'm env_state)transition set" where
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	22	"env_trans =
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	23	{tr. let s = fst(tr);
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	24	t = snd(snd(tr))
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	25	in case fst(snd(tr))
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	26	of
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	27	Next => t=True \|
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	28	S_msg(m) => s=True & t=False \|
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	29	R_msg(m) => False \|
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	30	S_pkt(pkt) => False \|
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	31	R_pkt(pkt) => False \|
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	32	S_ack(b) => False \|
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	33	R_ack(b) => False}"
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	34
25131 2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	35	definition
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	36	env_ioa :: "('m action, 'm env_state)ioa" where
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	37	"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	38
25131 2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	39	axiomatization
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	40	"next" :: "'m env_state => bool"
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	41
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	42	end

author	blanchet
	Tue, 06 Aug 2013 15:50:23 +0200
changeset 52869	79f5e137779a
parent 42151	4da4fc77664b
child 58880	0baae4311a9f
permissions	-rw-r--r--