src/HOL/HOLCF/IOA/ABP/Abschannel.thy
author huffman
Sat Nov 27 16:08:10 2010 -0800 (2010-11-27)
changeset 40774 0437dbc127b3
parent 35174 src/HOLCF/IOA/ABP/Abschannel.thy@e15040ae75d7
child 40945 b8703f63bfb2
permissions -rw-r--r--
moved directory src/HOLCF to src/HOL/HOLCF;
added HOLCF theories to src/HOL/IsaMakefile;
mueller@3072
     1
(*  Title:      HOLCF/IOA/ABP/Abschannel.thy
wenzelm@12218
     2
    Author:     Olaf Müller
mueller@3072
     3
*)
mueller@3072
     4
wenzelm@17244
     5
header {* The transmission channel *}
mueller@3072
     6
wenzelm@17244
     7
theory Abschannel
wenzelm@17244
     8
imports IOA Action Lemmas
wenzelm@17244
     9
begin
mueller@3072
    10
wenzelm@17244
    11
datatype 'a abs_action = S 'a | R 'a
mueller@3072
    12
mueller@3072
    13
mueller@3072
    14
(**********************************************************
mueller@3072
    15
       G e n e r i c   C h a n n e l
mueller@3072
    16
 *********************************************************)
wenzelm@17244
    17
wenzelm@25135
    18
definition
wenzelm@25135
    19
  ch_asig :: "'a abs_action signature" where
wenzelm@25135
    20
  "ch_asig = (UN b. {S(b)}, UN b. {R(b)}, {})"
mueller@3072
    21
wenzelm@25135
    22
definition
wenzelm@25135
    23
  ch_trans :: "('a abs_action, 'a list)transition set" where
wenzelm@25135
    24
  "ch_trans =
wenzelm@25135
    25
   {tr. let s = fst(tr);
wenzelm@25135
    26
            t = snd(snd(tr))
wenzelm@25135
    27
        in
wenzelm@25135
    28
        case fst(snd(tr))
wenzelm@25135
    29
          of S(b) => ((t = s) | (t = s @ [b]))  |
wenzelm@25135
    30
             R(b) => s ~= [] &
wenzelm@25135
    31
                      b = hd(s) &
wenzelm@25135
    32
                      ((t = s) | (t = tl(s)))}"
wenzelm@17244
    33
wenzelm@25135
    34
definition
wenzelm@25135
    35
  ch_ioa :: "('a abs_action, 'a list)ioa" where
wenzelm@25135
    36
  "ch_ioa = (ch_asig, {[]}, ch_trans,{},{})"
wenzelm@25135
    37
mueller@3072
    38
mueller@3072
    39
(**********************************************************
wenzelm@17244
    40
  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
    41
 *********************************************************)
wenzelm@17244
    42
wenzelm@25135
    43
definition
wenzelm@25135
    44
  rsch_actions :: "'m action => bool abs_action option" where
wenzelm@25135
    45
  "rsch_actions (akt) =
wenzelm@25135
    46
          (case akt of
wenzelm@17244
    47
           Next    =>  None |
wenzelm@17244
    48
           S_msg(m) => None |
wenzelm@17244
    49
            R_msg(m) => None |
wenzelm@17244
    50
           S_pkt(packet) => None |
wenzelm@17244
    51
            R_pkt(packet) => None |
wenzelm@17244
    52
            S_ack(b) => Some(S(b)) |
wenzelm@25135
    53
            R_ack(b) => Some(R(b)))"
mueller@3072
    54
wenzelm@25135
    55
definition
wenzelm@25135
    56
  srch_actions :: "'m action =>(bool * 'm) abs_action option" where
wenzelm@25135
    57
  "srch_actions akt =
wenzelm@25135
    58
          (case akt of
wenzelm@17244
    59
            Next    =>  None |
wenzelm@17244
    60
           S_msg(m) => None |
wenzelm@17244
    61
            R_msg(m) => None |
wenzelm@17244
    62
           S_pkt(p) => Some(S(p)) |
wenzelm@17244
    63
            R_pkt(p) => Some(R(p)) |
wenzelm@17244
    64
            S_ack(b) => None |
wenzelm@25135
    65
            R_ack(b) => None)"
wenzelm@25135
    66
wenzelm@25135
    67
definition
wenzelm@25135
    68
  srch_ioa :: "('m action, 'm packet list)ioa" where
wenzelm@25135
    69
  "srch_ioa = rename ch_ioa srch_actions"
wenzelm@25135
    70
definition
wenzelm@25135
    71
  rsch_ioa :: "('m action, bool list)ioa" where
wenzelm@25135
    72
  "rsch_ioa = rename ch_ioa rsch_actions"
wenzelm@25135
    73
wenzelm@25135
    74
definition
wenzelm@25135
    75
  srch_asig :: "'m action signature" where
wenzelm@25135
    76
  "srch_asig = asig_of(srch_ioa)"
wenzelm@25135
    77
wenzelm@25135
    78
definition
wenzelm@25135
    79
  rsch_asig :: "'m action signature" where
wenzelm@25135
    80
  "rsch_asig = asig_of(rsch_ioa)"
wenzelm@25135
    81
wenzelm@25135
    82
definition
wenzelm@25135
    83
  srch_trans :: "('m action, 'm packet list)transition set" where
wenzelm@25135
    84
  "srch_trans = trans_of(srch_ioa)"
wenzelm@25135
    85
definition
wenzelm@25135
    86
  rsch_trans :: "('m action, bool list)transition set" where
wenzelm@25135
    87
  "rsch_trans = trans_of(rsch_ioa)"
mueller@3072
    88
wenzelm@17244
    89
end