isabelle: src/HOL/IOA/ABP/Impl.thy@bca91b4e1710 (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
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	18	consts
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	19	impl_ioa :: "('m action, 'm impl_state)ioa"
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	20	sen :: "'m impl_state => 'm sender_state"
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	21	rec :: "'m impl_state => 'm receiver_state"
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	22	srch :: "'m impl_state => 'm packet list"
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	23	rsch :: "'m impl_state => bool list"
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	24
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	25	defs
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	26
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	27	impl_def
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	28	"impl_ioa == (sender_ioa \|\| receiver_ioa \|\| srch_ioa \|\| rsch_ioa)"
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	29
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	30	sen_def "sen == fst"
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	31	rec_def "rec == fst o snd"
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	32	srch_def "srch == fst o snd o snd"
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	33	rsch_def "rsch == snd o snd o snd"
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	34
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	35	end

author	clasohm
	Wed, 04 Oct 1995 14:01:44 +0100
changeset 1267	bca91b4e1710
parent 1139	993e475e70e2
child 1376	92f83b9d17e1
permissions	-rw-r--r--