Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/HOL/HOLCF/IOA/NTP/Abschannel.thy
author huffman
Sat, 27 Nov 2010 16:08:10 -0800
changeset 41022 0437dbc127b3
parent 35174 src/HOLCF/IOA/NTP/Abschannel.thy@e15040ae75d7
child 41193 b8703f63bfb2
permissions -rw-r--r--
moved directory src/HOLCF to src/HOL/HOLCF;
added HOLCF theories to src/HOL/IsaMakefile; 
     1 (*  Title:      HOL/IOA/NTP/Abschannel.thy

     2     Author:     Olaf Müller

     3 *)

     4 

     5 header {* The (faulty) transmission channel (both directions) *}

     6 

     7 theory Abschannel

     8 imports IOA Action

     9 begin

    10 

    11 datatype 'a abs_action = S 'a | R 'a

    12 

    13 definition

    14   ch_asig :: "'a abs_action signature" where

    15   "ch_asig = (UN b. {S(b)}, UN b. {R(b)}, {})"

    16 

    17 definition

    18   ch_trans :: "('a abs_action, 'a multiset)transition set" where

    19   "ch_trans =

    20     {tr. let s = fst(tr);

    21              t = snd(snd(tr))

    22          in

    23          case fst(snd(tr))

    24            of S(b) => t = addm s b |

    25               R(b) => count s b ~= 0 & t = delm s b}"

    26 

    27 definition

    28   ch_ioa :: "('a abs_action, 'a multiset)ioa" where

    29   "ch_ioa = (ch_asig, {{|}}, ch_trans,{},{})"

    30 

    31 definition

    32   rsch_actions :: "'m action => bool abs_action option" where

    33   "rsch_actions (akt) =

    34           (case akt of

    35            S_msg(m) => None |

    36             R_msg(m) => None |

    37            S_pkt(packet) => None |

    38             R_pkt(packet) => None |

    39             S_ack(b) => Some(S(b)) |

    40             R_ack(b) => Some(R(b)) |

    41            C_m_s =>  None  |

    42            C_m_r =>  None |

    43            C_r_s =>  None  |

    44            C_r_r(m) => None)"

    45 

    46 definition

    47   srch_actions :: "'m action =>(bool * 'm) abs_action option" where

    48   "srch_actions (akt) =

    49           (case akt of

    50            S_msg(m) => None |

    51             R_msg(m) => None |

    52            S_pkt(p) => Some(S(p)) |

    53             R_pkt(p) => Some(R(p)) |

    54             S_ack(b) => None |

    55             R_ack(b) => None |

    56            C_m_s => None |

    57            C_m_r => None |

    58            C_r_s => None |

    59            C_r_r(m) => None)"

    60 

    61 definition

    62   srch_ioa :: "('m action, 'm packet multiset)ioa" where

    63   "srch_ioa = rename ch_ioa srch_actions"

    64 

    65 definition

    66   rsch_ioa :: "('m action, bool multiset)ioa" where

    67   "rsch_ioa = rename ch_ioa rsch_actions"

    68 

    69 definition

    70   srch_asig :: "'m action signature" where

    71   "srch_asig = asig_of(srch_ioa)"

    72 

    73 definition

    74   rsch_asig :: "'m action signature" where

    75   "rsch_asig = asig_of(rsch_ioa)"

    76 

    77 definition

    78   srch_wfair :: "('m action)set set" where

    79   "srch_wfair = wfair_of(srch_ioa)"

    80 definition

    81   srch_sfair :: "('m action)set set" where

    82   "srch_sfair = sfair_of(srch_ioa)"

    83 definition

    84   rsch_sfair :: "('m action)set set" where

    85   "rsch_sfair = sfair_of(rsch_ioa)"

    86 definition

    87   rsch_wfair :: "('m action)set set" where

    88   "rsch_wfair = wfair_of(rsch_ioa)"

    89 

    90 definition

    91   srch_trans :: "('m action, 'm packet multiset)transition set" where

    92   "srch_trans = trans_of(srch_ioa)"

    93 definition

    94   rsch_trans :: "('m action, bool multiset)transition set" where

    95   "rsch_trans = trans_of(rsch_ioa)"

    96 

    97 

    98 lemmas unfold_renaming =

    99   srch_asig_def rsch_asig_def rsch_ioa_def srch_ioa_def ch_ioa_def

   100   ch_asig_def srch_actions_def rsch_actions_def rename_def rename_set_def asig_of_def

   101   actions_def srch_trans_def rsch_trans_def ch_trans_def starts_of_def

   102   trans_of_def asig_projections

   103 

   104 lemma in_srch_asig: 

   105      "S_msg(m) ~: actions(srch_asig)        &     

   106        R_msg(m) ~: actions(srch_asig)        &     

   107        S_pkt(pkt) : actions(srch_asig)    &     

   108        R_pkt(pkt) : actions(srch_asig)    &     

   109        S_ack(b) ~: actions(srch_asig)     &     

   110        R_ack(b) ~: actions(srch_asig)     &     

   111        C_m_s ~: actions(srch_asig)           &     

   112        C_m_r ~: actions(srch_asig)           &     

   113        C_r_s ~: actions(srch_asig)  & C_r_r(m) ~: actions(srch_asig)"

   114   by (simp add: unfold_renaming)

   115 

   116 lemma in_rsch_asig: 

   117       "S_msg(m) ~: actions(rsch_asig)         &  

   118        R_msg(m) ~: actions(rsch_asig)         &  

   119        S_pkt(pkt) ~: actions(rsch_asig)    &  

   120        R_pkt(pkt) ~: actions(rsch_asig)    &  

   121        S_ack(b) : actions(rsch_asig)       &  

   122        R_ack(b) : actions(rsch_asig)       &  

   123        C_m_s ~: actions(rsch_asig)            &  

   124        C_m_r ~: actions(rsch_asig)            &  

   125        C_r_s ~: actions(rsch_asig)            &  

   126        C_r_r(m) ~: actions(rsch_asig)"

   127   by (simp add: unfold_renaming)

   128 

   129 lemma srch_ioa_thm: "srch_ioa =  

   130     (srch_asig, {{|}}, srch_trans,srch_wfair,srch_sfair)"

   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)

   132 apply (simp (no_asm) add: unfold_renaming)

   133 done

   134 

   135 lemma rsch_ioa_thm: "rsch_ioa =  

   136      (rsch_asig, {{|}}, rsch_trans,rsch_wfair,rsch_sfair)"

   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)

   138 apply (simp (no_asm) add: unfold_renaming)

   139 done

   140 

   141 end
wneuper/isa