src/HOL/IOA/ABP/Impl.thy
author nipkow
Tue Apr 08 10:48:42 1997 +0200 (1997-04-08)
changeset 2919 953a47dc0519
parent 1570 fd1b9c721ac7
permissions -rw-r--r--
Dep. on Provers/nat_transitive
mueller@1139
     1
(*  Title:      HOL/IOA/example/Impl.thy
nipkow@1050
     2
    ID:         $Id$
mueller@1139
     3
    Author:     Tobias Nipkow & Konrad Slind
mueller@1139
     4
    Copyright   1994  TU Muenchen
nipkow@1050
     5
nipkow@1050
     6
The implementation
nipkow@1050
     7
*)
nipkow@1050
     8
nipkow@1050
     9
Impl = Sender + Receiver +  Abschannel +
nipkow@1050
    10
nipkow@1050
    11
types 
nipkow@1050
    12
nipkow@1050
    13
'm impl_state 
nipkow@1050
    14
= "'m sender_state * 'm receiver_state * 'm packet list * bool list"
nipkow@1050
    15
(*  sender_state   *  receiver_state   *    srch_state  * rsch_state *)
nipkow@1050
    16
nipkow@1050
    17
clasohm@1570
    18
constdefs
clasohm@1570
    19
clasohm@1376
    20
 impl_ioa    :: ('m action, 'm impl_state)ioa
clasohm@1570
    21
 "impl_ioa == (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)"
clasohm@1570
    22
clasohm@1376
    23
 sen         :: 'm impl_state => 'm sender_state
clasohm@1570
    24
 "sen == fst"
nipkow@1050
    25
clasohm@1570
    26
 rec         :: 'm impl_state => 'm receiver_state
clasohm@1570
    27
 "rec == fst o snd"
nipkow@1050
    28
clasohm@1570
    29
 srch        :: 'm impl_state => 'm packet list
clasohm@1570
    30
 "srch == fst o snd o snd"
clasohm@1570
    31
clasohm@1570
    32
 rsch        :: 'm impl_state => bool list
clasohm@1570
    33
 "rsch == snd o snd o snd"
nipkow@1050
    34
nipkow@1050
    35
end