src/HOL/HOLCF/IOA/NTP/Abschannel.thy
author wenzelm
Sun Nov 02 17:16:01 2014 +0100 (2014-11-02)
changeset 58880 0baae4311a9f
parent 58310 91ea607a34d8
child 61032 b57df8eecad6
permissions -rw-r--r--
modernized header;
wenzelm@42151
     1
(*  Title:      HOL/HOLCF/IOA/NTP/Abschannel.thy
wenzelm@40945
     2
    Author:     Olaf Müller
mueller@3073
     3
*)
mueller@3073
     4
wenzelm@58880
     5
section {* The (faulty) transmission channel (both directions) *}
wenzelm@17244
     6
wenzelm@17244
     7
theory Abschannel
wenzelm@17244
     8
imports IOA Action
wenzelm@17244
     9
begin
wenzelm@17244
    10
blanchet@58310
    11
datatype 'a abs_action = S 'a | R 'a
mueller@3073
    12
wenzelm@27361
    13
definition
wenzelm@27361
    14
  ch_asig :: "'a abs_action signature" where
wenzelm@27361
    15
  "ch_asig = (UN b. {S(b)}, UN b. {R(b)}, {})"
mueller@3073
    16
wenzelm@27361
    17
definition
wenzelm@27361
    18
  ch_trans :: "('a abs_action, 'a multiset)transition set" where
wenzelm@27361
    19
  "ch_trans =
wenzelm@27361
    20
    {tr. let s = fst(tr);
wenzelm@27361
    21
             t = snd(snd(tr))
wenzelm@27361
    22
         in
wenzelm@27361
    23
         case fst(snd(tr))
wenzelm@27361
    24
           of S(b) => t = addm s b |
wenzelm@27361
    25
              R(b) => count s b ~= 0 & t = delm s b}"
mueller@3073
    26
wenzelm@27361
    27
definition
wenzelm@27361
    28
  ch_ioa :: "('a abs_action, 'a multiset)ioa" where
wenzelm@27361
    29
  "ch_ioa = (ch_asig, {{|}}, ch_trans,{},{})"
mueller@3073
    30
wenzelm@27361
    31
definition
wenzelm@27361
    32
  rsch_actions :: "'m action => bool abs_action option" where
wenzelm@27361
    33
  "rsch_actions (akt) =
wenzelm@27361
    34
          (case akt of
wenzelm@17244
    35
           S_msg(m) => None |
wenzelm@17244
    36
            R_msg(m) => None |
wenzelm@17244
    37
           S_pkt(packet) => None |
wenzelm@17244
    38
            R_pkt(packet) => None |
wenzelm@17244
    39
            S_ack(b) => Some(S(b)) |
wenzelm@17244
    40
            R_ack(b) => Some(R(b)) |
wenzelm@17244
    41
           C_m_s =>  None  |
wenzelm@17244
    42
           C_m_r =>  None |
wenzelm@17244
    43
           C_r_s =>  None  |
wenzelm@27361
    44
           C_r_r(m) => None)"
mueller@3073
    45
wenzelm@27361
    46
definition
wenzelm@27361
    47
  srch_actions :: "'m action =>(bool * 'm) abs_action option" where
wenzelm@27361
    48
  "srch_actions (akt) =
wenzelm@27361
    49
          (case akt of
wenzelm@17244
    50
           S_msg(m) => None |
wenzelm@17244
    51
            R_msg(m) => None |
wenzelm@17244
    52
           S_pkt(p) => Some(S(p)) |
wenzelm@17244
    53
            R_pkt(p) => Some(R(p)) |
wenzelm@17244
    54
            S_ack(b) => None |
wenzelm@17244
    55
            R_ack(b) => None |
wenzelm@17244
    56
           C_m_s => None |
wenzelm@17244
    57
           C_m_r => None |
wenzelm@17244
    58
           C_r_s => None |
wenzelm@27361
    59
           C_r_r(m) => None)"
wenzelm@27361
    60
wenzelm@27361
    61
definition
wenzelm@27361
    62
  srch_ioa :: "('m action, 'm packet multiset)ioa" where
wenzelm@27361
    63
  "srch_ioa = rename ch_ioa srch_actions"
wenzelm@27361
    64
wenzelm@27361
    65
definition
wenzelm@27361
    66
  rsch_ioa :: "('m action, bool multiset)ioa" where
wenzelm@27361
    67
  "rsch_ioa = rename ch_ioa rsch_actions"
wenzelm@27361
    68
wenzelm@27361
    69
definition
wenzelm@27361
    70
  srch_asig :: "'m action signature" where
wenzelm@27361
    71
  "srch_asig = asig_of(srch_ioa)"
wenzelm@27361
    72
wenzelm@27361
    73
definition
wenzelm@27361
    74
  rsch_asig :: "'m action signature" where
wenzelm@27361
    75
  "rsch_asig = asig_of(rsch_ioa)"
wenzelm@27361
    76
wenzelm@27361
    77
definition
wenzelm@27361
    78
  srch_wfair :: "('m action)set set" where
wenzelm@27361
    79
  "srch_wfair = wfair_of(srch_ioa)"
wenzelm@27361
    80
definition
wenzelm@27361
    81
  srch_sfair :: "('m action)set set" where
wenzelm@27361
    82
  "srch_sfair = sfair_of(srch_ioa)"
wenzelm@27361
    83
definition
wenzelm@27361
    84
  rsch_sfair :: "('m action)set set" where
wenzelm@27361
    85
  "rsch_sfair = sfair_of(rsch_ioa)"
wenzelm@27361
    86
definition
wenzelm@27361
    87
  rsch_wfair :: "('m action)set set" where
wenzelm@27361
    88
  "rsch_wfair = wfair_of(rsch_ioa)"
wenzelm@27361
    89
wenzelm@27361
    90
definition
wenzelm@27361
    91
  srch_trans :: "('m action, 'm packet multiset)transition set" where
wenzelm@27361
    92
  "srch_trans = trans_of(srch_ioa)"
wenzelm@27361
    93
definition
wenzelm@27361
    94
  rsch_trans :: "('m action, bool multiset)transition set" where
wenzelm@27361
    95
  "rsch_trans = trans_of(rsch_ioa)"
wenzelm@27361
    96
mueller@3073
    97
wenzelm@19739
    98
lemmas unfold_renaming =
wenzelm@19739
    99
  srch_asig_def rsch_asig_def rsch_ioa_def srch_ioa_def ch_ioa_def
wenzelm@19739
   100
  ch_asig_def srch_actions_def rsch_actions_def rename_def rename_set_def asig_of_def
wenzelm@19739
   101
  actions_def srch_trans_def rsch_trans_def ch_trans_def starts_of_def
wenzelm@19739
   102
  trans_of_def asig_projections
wenzelm@19739
   103
wenzelm@19739
   104
lemma in_srch_asig: 
wenzelm@19739
   105
     "S_msg(m) ~: actions(srch_asig)        &     
wenzelm@19739
   106
       R_msg(m) ~: actions(srch_asig)        &     
wenzelm@19739
   107
       S_pkt(pkt) : actions(srch_asig)    &     
wenzelm@19739
   108
       R_pkt(pkt) : actions(srch_asig)    &     
wenzelm@19739
   109
       S_ack(b) ~: actions(srch_asig)     &     
wenzelm@19739
   110
       R_ack(b) ~: actions(srch_asig)     &     
wenzelm@19739
   111
       C_m_s ~: actions(srch_asig)           &     
wenzelm@19739
   112
       C_m_r ~: actions(srch_asig)           &     
wenzelm@19739
   113
       C_r_s ~: actions(srch_asig)  & C_r_r(m) ~: actions(srch_asig)"
wenzelm@19739
   114
  by (simp add: unfold_renaming)
wenzelm@19739
   115
wenzelm@19739
   116
lemma in_rsch_asig: 
wenzelm@19739
   117
      "S_msg(m) ~: actions(rsch_asig)         &  
wenzelm@19739
   118
       R_msg(m) ~: actions(rsch_asig)         &  
wenzelm@19739
   119
       S_pkt(pkt) ~: actions(rsch_asig)    &  
wenzelm@19739
   120
       R_pkt(pkt) ~: actions(rsch_asig)    &  
wenzelm@19739
   121
       S_ack(b) : actions(rsch_asig)       &  
wenzelm@19739
   122
       R_ack(b) : actions(rsch_asig)       &  
wenzelm@19739
   123
       C_m_s ~: actions(rsch_asig)            &  
wenzelm@19739
   124
       C_m_r ~: actions(rsch_asig)            &  
wenzelm@19739
   125
       C_r_s ~: actions(rsch_asig)            &  
wenzelm@19739
   126
       C_r_r(m) ~: actions(rsch_asig)"
wenzelm@19739
   127
  by (simp add: unfold_renaming)
wenzelm@19739
   128
wenzelm@19739
   129
lemma srch_ioa_thm: "srch_ioa =  
wenzelm@19739
   130
    (srch_asig, {{|}}, srch_trans,srch_wfair,srch_sfair)"
wenzelm@19739
   131
apply (simp (no_asm) add: srch_asig_def srch_trans_def asig_of_def trans_of_def wfair_of_def sfair_of_def srch_wfair_def srch_sfair_def)
wenzelm@19739
   132
apply (simp (no_asm) add: unfold_renaming)
wenzelm@19739
   133
done
wenzelm@19739
   134
wenzelm@19739
   135
lemma rsch_ioa_thm: "rsch_ioa =  
wenzelm@19739
   136
     (rsch_asig, {{|}}, rsch_trans,rsch_wfair,rsch_sfair)"
wenzelm@19739
   137
apply (simp (no_asm) add: rsch_asig_def rsch_trans_def asig_of_def trans_of_def wfair_of_def sfair_of_def rsch_wfair_def rsch_sfair_def)
wenzelm@19739
   138
apply (simp (no_asm) add: unfold_renaming)
wenzelm@19739
   139
done
mueller@3073
   140
wenzelm@17244
   141
end