isabelle: src/HOLCF/IOA/ABP/Impl_finite.thy@c2544c7b0611 (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: 3072 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 implementation *}
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	7
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	8	theory Impl_finite
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	9	imports Sender Receiver Abschannel_finite
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	10	begin
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	11
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	12	types
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	13	'm impl_fin_state
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	14	= "'m sender_state * 'm receiver_state * 'm packet list * bool list"
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	15	(* sender_state * receiver_state * srch_state * rsch_state *)
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	16
25131 2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	17	definition
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	18	impl_fin_ioa :: "('m action, 'm impl_fin_state)ioa" where
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	19	"impl_fin_ioa = (sender_ioa \|\| receiver_ioa \|\| srch_fin_ioa \|\|
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	20	rsch_fin_ioa)"
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	21
25131 2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	22	definition
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	23	sen_fin :: "'m impl_fin_state => 'm sender_state" where
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	24	"sen_fin = fst"
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	25
25131 2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	26	definition
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	27	rec_fin :: "'m impl_fin_state => 'm receiver_state" where
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	28	"rec_fin = fst o snd"
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	29
25131 2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	30	definition
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	31	srch_fin :: "'m impl_fin_state => 'm packet list" where
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	32	"srch_fin = fst o snd o snd"
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	33
25131 2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	34	definition
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	35	rsch_fin :: "'m impl_fin_state => bool list" where
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	36	"rsch_fin = snd o snd o snd"
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	end

author	haftmann
	Thu, 10 Sep 2009 15:23:08 +0200
changeset 32556	c2544c7b0611
parent 25131	2c8caac48ade
child 35174	e15040ae75d7
permissions	-rw-r--r--