isabelle: src/HOL/HOLCF/IOA/ABP/Impl.thy@ecab67f5a5c2 (annotated)

42151 4da4fc77664b tuned headers; wenzelm parents: 41476 diff changeset	1	(* Title: HOL/HOLCF/IOA/ABP/Impl.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 implementation *}
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	6
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	7	theory Impl
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	8	imports Sender Receiver Abschannel
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 impl_state = "'m sender_state * 'm receiver_state * 'm packet list * bool list"
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	13	(* sender_state * receiver_state * srch_state * rsch_state *)
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	14
25131 2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	15	definition
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	16	impl_ioa :: "('m action, 'm impl_state)ioa" where
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	17	"impl_ioa = (sender_ioa \|\| receiver_ioa \|\| srch_ioa \|\| rsch_ioa)"
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	18
25131 2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	19	definition
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	20	sen :: "'m impl_state => 'm sender_state" where
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	21	"sen = fst"
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	22
25131 2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	23	definition
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	24	rec :: "'m impl_state => 'm receiver_state" where
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	25	"rec = fst o snd"
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	26
25131 2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	27	definition
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	28	srch :: "'m impl_state => 'm packet list" where
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	29	"srch = fst o snd o snd"
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	30
25131 2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	31	definition
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	32	rsch :: "'m impl_state => bool list" where
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	33	"rsch = snd o snd o snd"
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	34
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	35	end

author	blanchet
	Wed, 04 Jan 2012 12:09:53 +0100
changeset 46115	ecab67f5a5c2
parent 42151	4da4fc77664b
child 58880	0baae4311a9f
permissions	-rw-r--r--