src/HOL/IOA/ABP/Impl_finite.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
mueller@1139
     6
The implementation
nipkow@1050
     7
*)
nipkow@1050
     8
nipkow@1050
     9
Impl_finite = Sender + Receiver +  Abschannel_finite +
nipkow@1050
    10
  
nipkow@1050
    11
types 
nipkow@1050
    12
nipkow@1050
    13
'm impl_fin_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
clasohm@1570
    17
constdefs
nipkow@1050
    18
clasohm@1376
    19
 impl_fin_ioa    :: ('m action, 'm impl_fin_state)ioa
clasohm@1570
    20
 "impl_fin_ioa == (sender_ioa || receiver_ioa || srch_fin_ioa ||
clasohm@1570
    21
                   rsch_fin_ioa)"
clasohm@1570
    22
clasohm@1376
    23
 sen_fin         :: 'm impl_fin_state => 'm sender_state
clasohm@1570
    24
 "sen_fin == fst"
nipkow@1050
    25
clasohm@1570
    26
 rec_fin         :: 'm impl_fin_state => 'm receiver_state
clasohm@1570
    27
 "rec_fin == fst o snd"
clasohm@1570
    28
clasohm@1570
    29
 srch_fin        :: 'm impl_fin_state => 'm packet list
clasohm@1570
    30
 "srch_fin == fst o snd o snd"
clasohm@1570
    31
clasohm@1570
    32
 rsch_fin        :: 'm impl_fin_state => bool list
clasohm@1570
    33
 "rsch_fin == snd o snd o snd"
nipkow@1050
    34
nipkow@1050
    35
end
nipkow@1050
    36