1(*  Title:      HOL/HOLCF/IOA/NTP/Abschannel.thy
2    Author:     Olaf M��ller
3*)
4
5section \<open>The (faulty) transmission channel (both directions)\<close>
6
7theory Abschannel
8imports IOA.IOA Action
9begin
10
11datatype 'a abs_action = S 'a | R 'a
12
13definition
14  ch_asig :: "'a abs_action signature" where
15  "ch_asig = (UN b. {S(b)}, UN b. {R(b)}, {})"
16
17definition
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
27definition
28  ch_ioa :: "('a abs_action, 'a multiset)ioa" where
29  "ch_ioa = (ch_asig, {{|}}, ch_trans,{},{})"
30
31definition
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
46definition
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
61definition
62  srch_ioa :: "('m action, 'm packet multiset)ioa" where
63  "srch_ioa = rename ch_ioa srch_actions"
64
65definition
66  rsch_ioa :: "('m action, bool multiset)ioa" where
67  "rsch_ioa = rename ch_ioa rsch_actions"
68
69definition
70  srch_asig :: "'m action signature" where
71  "srch_asig = asig_of(srch_ioa)"
72
73definition
74  rsch_asig :: "'m action signature" where
75  "rsch_asig = asig_of(rsch_ioa)"
76
77definition
78  srch_wfair :: "('m action)set set" where
79  "srch_wfair = wfair_of(srch_ioa)"
80definition
81  srch_sfair :: "('m action)set set" where
82  "srch_sfair = sfair_of(srch_ioa)"
83definition
84  rsch_sfair :: "('m action)set set" where
85  "rsch_sfair = sfair_of(rsch_ioa)"
86definition
87  rsch_wfair :: "('m action)set set" where
88  "rsch_wfair = wfair_of(rsch_ioa)"
89
90definition
91  srch_trans :: "('m action, 'm packet multiset)transition set" where
92  "srch_trans = trans_of(srch_ioa)"
93definition
94  rsch_trans :: "('m action, bool multiset)transition set" where
95  "rsch_trans = trans_of(rsch_ioa)"
96
97
98lemmas 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
104lemma in_srch_asig: 
105     "S_msg(m) \<notin> actions(srch_asig)        \<and>
106       R_msg(m) \<notin> actions(srch_asig)        \<and>
107       S_pkt(pkt) \<in> actions(srch_asig)    \<and>
108       R_pkt(pkt) \<in> actions(srch_asig)    \<and>     
109       S_ack(b) \<notin> actions(srch_asig)     \<and>     
110       R_ack(b) \<notin> actions(srch_asig)     \<and>     
111       C_m_s \<notin> actions(srch_asig)           \<and>     
112       C_m_r \<notin> actions(srch_asig)           \<and>     
113       C_r_s \<notin> actions(srch_asig)  & C_r_r(m) \<notin> actions(srch_asig)"
114  by (simp add: unfold_renaming)
115
116lemma in_rsch_asig: 
117      "S_msg(m) \<notin> actions(rsch_asig)         \<and>
118       R_msg(m) \<notin> actions(rsch_asig)         \<and>
119       S_pkt(pkt) \<notin> actions(rsch_asig)    \<and>
120       R_pkt(pkt) \<notin> actions(rsch_asig)    \<and>
121       S_ack(b) \<in> actions(rsch_asig)       \<and>
122       R_ack(b) \<in> actions(rsch_asig)       \<and>
123       C_m_s \<notin> actions(rsch_asig)            \<and>
124       C_m_r \<notin> actions(rsch_asig)            \<and>
125       C_r_s \<notin> actions(rsch_asig)            \<and>
126       C_r_r(m) \<notin> actions(rsch_asig)"
127  by (simp add: unfold_renaming)
128
129lemma srch_ioa_thm: "srch_ioa =  
130    (srch_asig, {{|}}, srch_trans,srch_wfair,srch_sfair)"
131apply (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)
132apply (simp (no_asm) add: unfold_renaming)
133done
134
135lemma rsch_ioa_thm: "rsch_ioa =  
136     (rsch_asig, {{|}}, rsch_trans,rsch_wfair,rsch_sfair)"
137apply (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)
138apply (simp (no_asm) add: unfold_renaming)
139done
140
141end
142