Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOLCF/IOA/ABP/Impl_finite.thy
author mueller
Wed, 30 Apr 1997 11:24:14 +0200
changeset 3072 a31419014be5
child 12218 6597093b77e7
permissions -rw-r--r--
Old ABP files now running under the IOA meta theory based on HOLCF;

(*  Title:      HOLCF/IOA/ABP/Impl.thy
    ID:         $Id$
    Author:     Olaf Mueller
    Copyright   1995  TU Muenchen

The implementation
*)

Impl_finite = Sender + Receiver +  Abschannel_finite +
  
types 

'm impl_fin_state 
= "'m sender_state * 'm receiver_state * 'm packet list * bool list"
(*  sender_state   *  receiver_state   *    srch_state  * rsch_state *)

constdefs

 impl_fin_ioa    :: ('m action, 'm impl_fin_state)ioa
 "impl_fin_ioa == (sender_ioa || receiver_ioa || srch_fin_ioa ||
                   rsch_fin_ioa)"

 sen_fin         :: 'm impl_fin_state => 'm sender_state
 "sen_fin == fst"

 rec_fin         :: 'm impl_fin_state => 'm receiver_state
 "rec_fin == fst o snd"

 srch_fin        :: 'm impl_fin_state => 'm packet list
 "srch_fin == fst o snd o snd"

 rsch_fin        :: 'm impl_fin_state => bool list
 "rsch_fin == snd o snd o snd"

end
isabelle