isabelle: src/HOL/IOA/ABP/Impl.thy@b50b8c0eec01 (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
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	6	The implementation
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 = Sender + Receiver + Abschannel +
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_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
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	17
1570 fd1b9c721ac7 added constdefs section clasohm parents: 1376 diff changeset	18	constdefs
fd1b9c721ac7 added constdefs section clasohm parents: 1376 diff changeset	19
1376 92f83b9d17e1 removed quotes from consts and syntax sections clasohm parents: 1139 diff changeset	20	impl_ioa :: ('m action, 'm impl_state)ioa
1570 fd1b9c721ac7 added constdefs section clasohm parents: 1376 diff changeset	21	"impl_ioa == (sender_ioa \|\| receiver_ioa \|\| srch_ioa \|\| rsch_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 :: 'm impl_state => 'm sender_state
1570 fd1b9c721ac7 added constdefs section clasohm parents: 1376 diff changeset	24	"sen == 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 :: 'm impl_state => 'm receiver_state
fd1b9c721ac7 added constdefs section clasohm parents: 1376 diff changeset	27	"rec == fst o snd"
1050 0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	28
1570 fd1b9c721ac7 added constdefs section clasohm parents: 1376 diff changeset	29	srch :: 'm impl_state => 'm packet list
fd1b9c721ac7 added constdefs section clasohm parents: 1376 diff changeset	30	"srch == 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 :: 'm impl_state => bool list
fd1b9c721ac7 added constdefs section clasohm parents: 1376 diff changeset	33	"rsch == 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

author	paulson
	Fri, 03 Jan 1997 15:01:55 +0100
changeset 2469	b50b8c0eec01
parent 1570	fd1b9c721ac7
permissions	-rw-r--r--