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

1050 0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	1	(* Title: HOL/IOA/ABP/Impl_finite.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 finite 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_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
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	17	consts
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	18
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	19	impl_fin_ioa :: "('m action, 'm impl_fin_state)ioa"
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	20	sen_fin :: "'m impl_fin_state => 'm sender_state"
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	21	rec_fin :: "'m impl_fin_state => 'm receiver_state"
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	22	srch_fin :: "'m impl_fin_state => 'm packet list"
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	23	rsch_fin :: "'m impl_fin_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_fin_def
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	28	"impl_fin_ioa == (sender_ioa \|\| receiver_ioa \|\| srch_fin_ioa \|\| rsch_fin_ioa)"
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	29	sen_fin_def "sen_fin == fst"
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	30	rec_fin_def "rec_fin == fst o snd"
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	31	srch_fin_def "srch_fin == fst o snd o snd"
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	32	rsch_fin_def "rsch_fin == snd o snd o snd"
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	33
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	34	end
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	35

author	lcp
	Tue, 25 Apr 1995 11:14:03 +0200
changeset 1072	0140ff702b23
parent 1050	0c36c6a52a1d
child 1139	993e475e70e2
permissions	-rw-r--r--