isabelle: src/HOL/HOLCF/IOA/ABP/Impl_finite.thy@89da4dcd1fa8 (annotated)

42151 4da4fc77664b tuned headers; wenzelm parents: 41476 diff changeset	1	(* Title: HOL/HOLCF/IOA/ABP/Impl_finite.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
62002 f1599e98c4d0 isabelle update_cartouches -c -t; wenzelm parents: 61999 diff changeset	5	section \<open>The implementation\<close>
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_finite
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	8	imports Sender Receiver Abschannel_finite
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	9	begin
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 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_fin_state
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	13	= "'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	14	(* 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	15
25131 2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	16	definition
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	17	impl_fin_ioa :: "('m action, 'm impl_fin_state)ioa" where
61999 89291b5d0ede more symbols; wenzelm parents: 58880 diff changeset	18	"impl_fin_ioa = (sender_ioa \<parallel> receiver_ioa \<parallel> srch_fin_ioa \<parallel>
25131 2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	19	rsch_fin_ioa)"
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	20
25131 2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	21	definition
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	22	sen_fin :: "'m impl_fin_state => 'm sender_state" where
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	23	"sen_fin = fst"
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	24
25131 2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	25	definition
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	26	rec_fin :: "'m impl_fin_state => 'm receiver_state" where
62116 bc178c0fe1a1 misc tuning and modernization; wenzelm parents: 62002 diff changeset	27	"rec_fin = fst \<circ> snd"
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	28
25131 2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	29	definition
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	30	srch_fin :: "'m impl_fin_state => 'm packet list" where
62116 bc178c0fe1a1 misc tuning and modernization; wenzelm parents: 62002 diff changeset	31	"srch_fin = fst \<circ> snd \<circ> snd"
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	32
25131 2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	33	definition
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	34	rsch_fin :: "'m impl_fin_state => bool list" where
62116 bc178c0fe1a1 misc tuning and modernization; wenzelm parents: 62002 diff changeset	35	"rsch_fin = snd \<circ> snd \<circ> snd"
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	36
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	37	end

author	wenzelm
	Wed, 23 Jul 2025 14:53:21 +0200
changeset 82898	89da4dcd1fa8
parent 62116	bc178c0fe1a1
permissions	-rw-r--r--