isabelle: src/HOLCF/IOA/ABP/Impl.thy@0b2ff9541727 (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
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	9	imports Sender Receiver Abschannel
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
17244 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_state = "'m sender_state * 'm receiver_state * 'm packet list * bool list"
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	14	(* 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	15
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	16	constdefs
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	17
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	18	impl_ioa :: "('m action, 'm impl_state)ioa"
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	19	"impl_ioa == (sender_ioa \|\| receiver_ioa \|\| srch_ioa \|\| rsch_ioa)"
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	20
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	21	sen :: "'m impl_state => 'm sender_state"
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	22	"sen == fst"
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	23
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	24	rec :: "'m impl_state => 'm receiver_state"
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	25	"rec == fst o snd"
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	26
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	27	srch :: "'m impl_state => 'm packet list"
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	28	"srch == fst o snd o snd"
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	29
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	30	rsch :: "'m impl_state => bool list"
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	31	"rsch == snd o snd o snd"
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	32
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	33	ML {* use_legacy_bindings (the_context ()) *}
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	34
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	35	end

author	wenzelm
	Sat, 03 Sep 2005 16:50:22 +0200
changeset 17244	0b2ff9541727
parent 14981	e73f8140af78
child 19738	1ac610922636
permissions	-rw-r--r--