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