isabelle: src/HOL/IOA/ABP/Impl.thy@0140ff702b23 (annotated)

1050 0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	1	(* Title: HOL/IOA/ABP/Impl.thy
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	2	ID: $Id$
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	3	Author: Tobias Nipkow & Olaf Mueller
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	4	Copyright 1995 TU Muenchen
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	lcp
	Tue, 25 Apr 1995 11:14:03 +0200
changeset 1072	0140ff702b23
parent 1050	0c36c6a52a1d
child 1139	993e475e70e2
permissions	-rw-r--r--