src/HOL/HOLCF/IOA/NTP/Abschannel.thy
author wenzelm
Wed, 30 Dec 2015 21:57:52 +0100
changeset 62002 f1599e98c4d0
parent 61032 b57df8eecad6
child 62008 cbedaddc9351
permissions -rw-r--r--
isabelle update_cartouches -c -t;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
42151
4da4fc77664b tuned headers;
wenzelm
parents: 40945
diff changeset
     1
(*  Title:      HOL/HOLCF/IOA/NTP/Abschannel.thy
40945
b8703f63bfb2 recoded latin1 as utf8;
wenzelm
parents: 40774
diff changeset
     2
    Author:     Olaf Müller
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
     3
*)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
     4
62002
f1599e98c4d0 isabelle update_cartouches -c -t;
wenzelm
parents: 61032
diff changeset
     5
section \<open>The (faulty) transmission channel (both directions)\<close>
17244
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     6
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     7
theory Abschannel
61032
b57df8eecad6 standardized some occurences of ancient "split" alias
haftmann
parents: 58880
diff changeset
     8
imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action
17244
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     9
begin
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    10
58310
91ea607a34d8 updated news
blanchet
parents: 58249
diff changeset
    11
datatype 'a abs_action = S 'a | R 'a
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    12
27361
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    13
definition
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    14
  ch_asig :: "'a abs_action signature" where
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    15
  "ch_asig = (UN b. {S(b)}, UN b. {R(b)}, {})"
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    16
27361
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    17
definition
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    18
  ch_trans :: "('a abs_action, 'a multiset)transition set" where
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    19
  "ch_trans =
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    20
    {tr. let s = fst(tr);
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    21
             t = snd(snd(tr))
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    22
         in
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    23
         case fst(snd(tr))
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    24
           of S(b) => t = addm s b |
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    25
              R(b) => count s b ~= 0 & t = delm s b}"
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    26
27361
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    27
definition
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    28
  ch_ioa :: "('a abs_action, 'a multiset)ioa" where
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    29
  "ch_ioa = (ch_asig, {{|}}, ch_trans,{},{})"
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    30
27361
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    31
definition
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    32
  rsch_actions :: "'m action => bool abs_action option" where
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    33
  "rsch_actions (akt) =
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    34
          (case akt of
17244
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    35
           S_msg(m) => None |
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    36
            R_msg(m) => None |
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    37
           S_pkt(packet) => None |
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    38
            R_pkt(packet) => None |
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    39
            S_ack(b) => Some(S(b)) |
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    40
            R_ack(b) => Some(R(b)) |
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    41
           C_m_s =>  None  |
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    42
           C_m_r =>  None |
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    43
           C_r_s =>  None  |
27361
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    44
           C_r_r(m) => None)"
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    45
27361
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    46
definition
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    47
  srch_actions :: "'m action =>(bool * 'm) abs_action option" where
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    48
  "srch_actions (akt) =
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    49
          (case akt of
17244
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    50
           S_msg(m) => None |
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    51
            R_msg(m) => None |
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    52
           S_pkt(p) => Some(S(p)) |
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    53
            R_pkt(p) => Some(R(p)) |
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    54
            S_ack(b) => None |
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    55
            R_ack(b) => None |
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    56
           C_m_s => None |
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    57
           C_m_r => None |
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    58
           C_r_s => None |
27361
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    59
           C_r_r(m) => None)"
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    60
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    61
definition
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    62
  srch_ioa :: "('m action, 'm packet multiset)ioa" where
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    63
  "srch_ioa = rename ch_ioa srch_actions"
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    64
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    65
definition
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    66
  rsch_ioa :: "('m action, bool multiset)ioa" where
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    67
  "rsch_ioa = rename ch_ioa rsch_actions"
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    68
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    69
definition
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    70
  srch_asig :: "'m action signature" where
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    71
  "srch_asig = asig_of(srch_ioa)"
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    72
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    73
definition
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    74
  rsch_asig :: "'m action signature" where
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    75
  "rsch_asig = asig_of(rsch_ioa)"
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    76
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    77
definition
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    78
  srch_wfair :: "('m action)set set" where
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    79
  "srch_wfair = wfair_of(srch_ioa)"
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    80
definition
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    81
  srch_sfair :: "('m action)set set" where
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    82
  "srch_sfair = sfair_of(srch_ioa)"
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    83
definition
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    84
  rsch_sfair :: "('m action)set set" where
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    85
  "rsch_sfair = sfair_of(rsch_ioa)"
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    86
definition
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    87
  rsch_wfair :: "('m action)set set" where
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    88
  "rsch_wfair = wfair_of(rsch_ioa)"
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    89
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    90
definition
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    91
  srch_trans :: "('m action, 'm packet multiset)transition set" where
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    92
  "srch_trans = trans_of(srch_ioa)"
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    93
definition
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    94
  rsch_trans :: "('m action, bool multiset)transition set" where
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    95
  "rsch_trans = trans_of(rsch_ioa)"
24ec32bee347 modernized specifications;
wenzelm
parents: 19739
diff changeset
    96
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    97
19739
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    98
lemmas unfold_renaming =
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    99
  srch_asig_def rsch_asig_def rsch_ioa_def srch_ioa_def ch_ioa_def
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   100
  ch_asig_def srch_actions_def rsch_actions_def rename_def rename_set_def asig_of_def
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   101
  actions_def srch_trans_def rsch_trans_def ch_trans_def starts_of_def
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   102
  trans_of_def asig_projections
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   103
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   104
lemma in_srch_asig: 
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   105
     "S_msg(m) ~: actions(srch_asig)        &     
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   106
       R_msg(m) ~: actions(srch_asig)        &     
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   107
       S_pkt(pkt) : actions(srch_asig)    &     
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   108
       R_pkt(pkt) : actions(srch_asig)    &     
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   109
       S_ack(b) ~: actions(srch_asig)     &     
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   110
       R_ack(b) ~: actions(srch_asig)     &     
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   111
       C_m_s ~: actions(srch_asig)           &     
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   112
       C_m_r ~: actions(srch_asig)           &     
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   113
       C_r_s ~: actions(srch_asig)  & C_r_r(m) ~: actions(srch_asig)"
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   114
  by (simp add: unfold_renaming)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   115
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   116
lemma in_rsch_asig: 
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   117
      "S_msg(m) ~: actions(rsch_asig)         &  
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   118
       R_msg(m) ~: actions(rsch_asig)         &  
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   119
       S_pkt(pkt) ~: actions(rsch_asig)    &  
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   120
       R_pkt(pkt) ~: actions(rsch_asig)    &  
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   121
       S_ack(b) : actions(rsch_asig)       &  
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   122
       R_ack(b) : actions(rsch_asig)       &  
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   123
       C_m_s ~: actions(rsch_asig)            &  
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   124
       C_m_r ~: actions(rsch_asig)            &  
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   125
       C_r_s ~: actions(rsch_asig)            &  
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   126
       C_r_r(m) ~: actions(rsch_asig)"
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   127
  by (simp add: unfold_renaming)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   128
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   129
lemma srch_ioa_thm: "srch_ioa =  
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   130
    (srch_asig, {{|}}, srch_trans,srch_wfair,srch_sfair)"
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   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)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   132
apply (simp (no_asm) add: unfold_renaming)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   133
done
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   134
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   135
lemma rsch_ioa_thm: "rsch_ioa =  
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   136
     (rsch_asig, {{|}}, rsch_trans,rsch_wfair,rsch_sfair)"
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   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)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   138
apply (simp (no_asm) add: unfold_renaming)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   139
done
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   140
17244
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
   141
end