| changeset 19739 | c58ef2aa5430 |
| parent 17244 | 0b2ff9541727 |
| child 27361 | 24ec32bee347 |
| 19738:1ac610922636 | 19739:c58ef2aa5430 |
|---|---|
85 |
85 |
86 |
86 |
87 receiver_ioa_def: "receiver_ioa == |
87 receiver_ioa_def: "receiver_ioa == |
88 (receiver_asig, {([],{|},{|},False,False)}, receiver_trans,{},{})" |
88 (receiver_asig, {([],{|},{|},False,False)}, receiver_trans,{},{})" |
89 |
89 |
90 ML {* use_legacy_bindings (the_context ()) *} |
90 lemma in_receiver_asig: |
91 "S_msg(m) ~: actions(receiver_asig)" |
|
92 "R_msg(m) : actions(receiver_asig)" |
|
93 "S_pkt(pkt) ~: actions(receiver_asig)" |
|
94 "R_pkt(pkt) : actions(receiver_asig)" |
|
95 "S_ack(b) : actions(receiver_asig)" |
|
96 "R_ack(b) ~: actions(receiver_asig)" |
|
97 "C_m_s ~: actions(receiver_asig)" |
|
98 "C_m_r : actions(receiver_asig)" |
|
99 "C_r_s ~: actions(receiver_asig)" |
|
100 "C_r_r(m) : actions(receiver_asig)" |
|
101 by (simp_all add: receiver_asig_def actions_def asig_projections) |
|
102 |
|
103 lemmas receiver_projections = rq_def rsent_def rrcvd_def rbit_def rsending_def |
|
91 |
104 |
92 end |
105 end |