isabelle: src/HOL/IOA/ABP/Impl_finite.thy@fd1b9c721ac7 (annotated)

1139 993e475e70e2 * empty log message * mueller parents: 1050 diff changeset	1	(* Title: HOL/IOA/example/Impl.thy
1050 0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	2	ID: $Id$
1139 993e475e70e2 * empty log message * mueller parents: 1050 diff changeset	3	Author: Tobias Nipkow & Konrad Slind
993e475e70e2 * empty log message * mueller parents: 1050 diff changeset	4	Copyright 1994 TU Muenchen
1050 0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	5
1139 993e475e70e2 * empty log message * mueller parents: 1050 diff changeset	6	The implementation
1050 0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	7	*)
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	8
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	9	Impl_finite = Sender + Receiver + Abschannel_finite +
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	10
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	11	types
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	12
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	13	'm impl_fin_state
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	14	= "'m sender_state * 'm receiver_state * 'm packet list * bool list"
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	15	(* sender_state * receiver_state * srch_state * rsch_state *)
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	16
1570 fd1b9c721ac7 added constdefs section clasohm parents: 1376 diff changeset	17	constdefs
1050 0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	18
1376 92f83b9d17e1 removed quotes from consts and syntax sections clasohm parents: 1139 diff changeset	19	impl_fin_ioa :: ('m action, 'm impl_fin_state)ioa
1570 fd1b9c721ac7 added constdefs section clasohm parents: 1376 diff changeset	20	"impl_fin_ioa == (sender_ioa \|\| receiver_ioa \|\| srch_fin_ioa \|\|
fd1b9c721ac7 added constdefs section clasohm parents: 1376 diff changeset	21	rsch_fin_ioa)"
fd1b9c721ac7 added constdefs section clasohm parents: 1376 diff changeset	22
1376 92f83b9d17e1 removed quotes from consts and syntax sections clasohm parents: 1139 diff changeset	23	sen_fin :: 'm impl_fin_state => 'm sender_state
1570 fd1b9c721ac7 added constdefs section clasohm parents: 1376 diff changeset	24	"sen_fin == fst"
1050 0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	25
1570 fd1b9c721ac7 added constdefs section clasohm parents: 1376 diff changeset	26	rec_fin :: 'm impl_fin_state => 'm receiver_state
fd1b9c721ac7 added constdefs section clasohm parents: 1376 diff changeset	27	"rec_fin == fst o snd"
fd1b9c721ac7 added constdefs section clasohm parents: 1376 diff changeset	28
fd1b9c721ac7 added constdefs section clasohm parents: 1376 diff changeset	29	srch_fin :: 'm impl_fin_state => 'm packet list
fd1b9c721ac7 added constdefs section clasohm parents: 1376 diff changeset	30	"srch_fin == fst o snd o snd"
fd1b9c721ac7 added constdefs section clasohm parents: 1376 diff changeset	31
fd1b9c721ac7 added constdefs section clasohm parents: 1376 diff changeset	32	rsch_fin :: 'm impl_fin_state => bool list
fd1b9c721ac7 added constdefs section clasohm parents: 1376 diff changeset	33	"rsch_fin == snd o snd o snd"
1050 0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	34
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	35	end
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	36

author	clasohm
	Mon, 11 Mar 1996 23:59:22 +0100
changeset 1570	fd1b9c721ac7
parent 1376	92f83b9d17e1
permissions	-rw-r--r--