src/HOLCF/IOA/ABP/Abschannel.thy
author wenzelm
Sat Sep 03 16:50:22 2005 +0200 (2005-09-03)
changeset 17244 0b2ff9541727
parent 14981 e73f8140af78
child 19738 1ac610922636
permissions -rw-r--r--
converted to Isar theory format;
mueller@3072
     1
(*  Title:      HOLCF/IOA/ABP/Abschannel.thy
mueller@3072
     2
    ID:         $Id$
wenzelm@12218
     3
    Author:     Olaf Müller
mueller@3072
     4
*)
mueller@3072
     5
wenzelm@17244
     6
header {* The transmission channel *}
mueller@3072
     7
wenzelm@17244
     8
theory Abschannel
wenzelm@17244
     9
imports IOA Action Lemmas
wenzelm@17244
    10
begin
mueller@3072
    11
wenzelm@17244
    12
datatype 'a abs_action = S 'a | R 'a
mueller@3072
    13
mueller@3072
    14
mueller@3072
    15
consts
wenzelm@17244
    16
mueller@6468
    17
ch_asig  :: "'a abs_action signature"
wenzelm@17244
    18
ch_trans :: "('a abs_action, 'a list)transition set"
wenzelm@17244
    19
ch_ioa   :: "('a abs_action, 'a list)ioa"
mueller@3072
    20
wenzelm@17244
    21
rsch_actions  :: "'m action => bool abs_action option"
mueller@3072
    22
srch_actions  :: "'m action =>(bool * 'm) abs_action option"
mueller@3072
    23
wenzelm@17244
    24
srch_asig  :: "'m action signature"
mueller@6468
    25
rsch_asig  :: "'m action signature"
mueller@3072
    26
wenzelm@17244
    27
srch_trans :: "('m action, 'm packet list)transition set"
wenzelm@17244
    28
rsch_trans :: "('m action, bool list)transition set"
wenzelm@17244
    29
wenzelm@17244
    30
srch_ioa   :: "('m action, 'm packet list)ioa"
wenzelm@17244
    31
rsch_ioa   :: "('m action, bool list)ioa"
mueller@3072
    32
mueller@3072
    33
mueller@3072
    34
defs
mueller@3072
    35
wenzelm@17244
    36
srch_asig_def: "srch_asig == asig_of(srch_ioa)"
wenzelm@17244
    37
rsch_asig_def: "rsch_asig == asig_of(rsch_ioa)"
mueller@3072
    38
wenzelm@17244
    39
srch_trans_def: "srch_trans == trans_of(srch_ioa)"
wenzelm@17244
    40
rsch_trans_def: "rsch_trans == trans_of(rsch_ioa)"
mueller@3072
    41
wenzelm@17244
    42
srch_ioa_def: "srch_ioa == rename ch_ioa srch_actions"
wenzelm@17244
    43
rsch_ioa_def: "rsch_ioa == rename ch_ioa rsch_actions"
mueller@3072
    44
wenzelm@17244
    45
mueller@3072
    46
(**********************************************************
mueller@3072
    47
       G e n e r i c   C h a n n e l
mueller@3072
    48
 *********************************************************)
wenzelm@17244
    49
wenzelm@17244
    50
ch_asig_def: "ch_asig == (UN b. {S(b)}, UN b. {R(b)}, {})"
mueller@3072
    51
wenzelm@17244
    52
ch_trans_def: "ch_trans ==
wenzelm@17244
    53
 {tr. let s = fst(tr);
wenzelm@17244
    54
          t = snd(snd(tr))
wenzelm@17244
    55
      in
wenzelm@17244
    56
      case fst(snd(tr))
wenzelm@17244
    57
        of S(b) => ((t = s) | (t = s @ [b]))  |
wenzelm@17244
    58
           R(b) => s ~= [] &
wenzelm@17244
    59
                    b = hd(s) &
mueller@3072
    60
                    ((t = s) | (t = tl(s)))    }"
wenzelm@17244
    61
wenzelm@17244
    62
ch_ioa_def: "ch_ioa == (ch_asig, {[]}, ch_trans,{},{})"
mueller@3072
    63
mueller@3072
    64
(**********************************************************
wenzelm@17244
    65
  C o n c r e t e  C h a n n e l s  b y   R e n a m i n g
mueller@3072
    66
 *********************************************************)
wenzelm@17244
    67
wenzelm@17244
    68
rsch_actions_def: "rsch_actions (akt) ==
wenzelm@17244
    69
            case akt of
wenzelm@17244
    70
           Next    =>  None |
wenzelm@17244
    71
           S_msg(m) => None |
wenzelm@17244
    72
            R_msg(m) => None |
wenzelm@17244
    73
           S_pkt(packet) => None |
wenzelm@17244
    74
            R_pkt(packet) => None |
wenzelm@17244
    75
            S_ack(b) => Some(S(b)) |
mueller@3072
    76
            R_ack(b) => Some(R(b))"
mueller@3072
    77
wenzelm@17244
    78
srch_actions_def: "srch_actions (akt) ==
wenzelm@17244
    79
            case akt of
wenzelm@17244
    80
            Next    =>  None |
wenzelm@17244
    81
           S_msg(m) => None |
wenzelm@17244
    82
            R_msg(m) => None |
wenzelm@17244
    83
           S_pkt(p) => Some(S(p)) |
wenzelm@17244
    84
            R_pkt(p) => Some(R(p)) |
wenzelm@17244
    85
            S_ack(b) => None |
mueller@3072
    86
            R_ack(b) => None"
mueller@3072
    87
wenzelm@17244
    88
ML {* use_legacy_bindings (the_context ()) *}
mueller@3072
    89
wenzelm@17244
    90
end
mueller@3072
    91
mueller@3072
    92
mueller@3072
    93
mueller@3072
    94
mueller@3072
    95
mueller@3072
    96
mueller@3072
    97
mueller@3072
    98
mueller@3072
    99
mueller@3072
   100
mueller@3072
   101
mueller@3072
   102
mueller@3072
   103