author | kleing |
Mon, 21 Jun 2004 10:25:57 +0200 | |
changeset 14981 | e73f8140af78 |
parent 12218 | 6597093b77e7 |
child 17244 | 0b2ff9541727 |
permissions | -rw-r--r-- |
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
1 |
(* Title: HOL/IOA/NTP/Abschannel.ML |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
2 |
ID: $Id$ |
12218 | 3 |
Author: Olaf Müller |
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
4 |
|
12218 | 5 |
Derived rules. |
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
6 |
*) |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
7 |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
8 |
open Abschannel; |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
9 |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
10 |
val unfold_renaming = |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
11 |
[srch_asig_def, rsch_asig_def, rsch_ioa_def, srch_ioa_def, ch_ioa_def, |
3523 | 12 |
ch_asig_def, srch_actions_def, rsch_actions_def, rename_def, rename_set_def, asig_of_def, |
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
13 |
actions_def, srch_trans_def, rsch_trans_def, ch_trans_def,starts_of_def, |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
14 |
trans_of_def] @ asig_projections; |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
15 |
|
5068 | 16 |
Goal |
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
17 |
"S_msg(m) ~: actions(srch_asig) & \ |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
18 |
\ R_msg(m) ~: actions(srch_asig) & \ |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
19 |
\ S_pkt(pkt) : actions(srch_asig) & \ |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
20 |
\ R_pkt(pkt) : actions(srch_asig) & \ |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
21 |
\ S_ack(b) ~: actions(srch_asig) & \ |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
22 |
\ R_ack(b) ~: actions(srch_asig) & \ |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
23 |
\ C_m_s ~: actions(srch_asig) & \ |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
24 |
\ C_m_r ~: actions(srch_asig) & \ |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
25 |
\ C_r_s ~: actions(srch_asig) & C_r_r(m) ~: actions(srch_asig)"; |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
26 |
|
4423 | 27 |
by (simp_tac (simpset() addsimps unfold_renaming) 1); |
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
28 |
qed"in_srch_asig"; |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
29 |
|
5068 | 30 |
Goal |
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
31 |
"S_msg(m) ~: actions(rsch_asig) & \ |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
32 |
\ R_msg(m) ~: actions(rsch_asig) & \ |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
33 |
\ S_pkt(pkt) ~: actions(rsch_asig) & \ |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
34 |
\ R_pkt(pkt) ~: actions(rsch_asig) & \ |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
35 |
\ S_ack(b) : actions(rsch_asig) & \ |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
36 |
\ R_ack(b) : actions(rsch_asig) & \ |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
37 |
\ C_m_s ~: actions(rsch_asig) & \ |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
38 |
\ C_m_r ~: actions(rsch_asig) & \ |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
39 |
\ C_r_s ~: actions(rsch_asig) & \ |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
40 |
\ C_r_r(m) ~: actions(rsch_asig)"; |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
41 |
|
4423 | 42 |
by (simp_tac (simpset() addsimps unfold_renaming) 1); |
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
43 |
qed"in_rsch_asig"; |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
44 |
|
5068 | 45 |
Goal "srch_ioa = \ |
3523 | 46 |
\ (srch_asig, {{|}}, srch_trans,srch_wfair,srch_sfair)"; |
4098 | 47 |
by (simp_tac (simpset() addsimps [srch_asig_def,srch_trans_def, asig_of_def, trans_of_def, |
3523 | 48 |
wfair_of_def, sfair_of_def,srch_wfair_def,srch_sfair_def]) 1); |
4423 | 49 |
by (simp_tac (simpset() addsimps unfold_renaming) 1); |
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
50 |
qed"srch_ioa_thm"; |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
51 |
|
5068 | 52 |
Goal "rsch_ioa = \ |
3523 | 53 |
\ (rsch_asig, {{|}}, rsch_trans,rsch_wfair,rsch_sfair)"; |
4098 | 54 |
by (simp_tac (simpset() addsimps [rsch_asig_def,rsch_trans_def, asig_of_def, trans_of_def, |
3523 | 55 |
wfair_of_def, sfair_of_def,rsch_wfair_def,rsch_sfair_def]) 1); |
4423 | 56 |
by (simp_tac (simpset() addsimps unfold_renaming) 1); |
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
57 |
qed"rsch_ioa_thm"; |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
58 |