author | wenzelm |
Thu, 15 Nov 2001 23:25:46 +0100 | |
changeset 12218 | 6597093b77e7 |
parent 7499 | 23e090051cb8 |
child 14981 | e73f8140af78 |
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/Correctness.ML |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
2 |
ID: $Id$ |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
3 |
Author: Tobias Nipkow & Konrad Slind |
12218 | 4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
5 |
|
12218 | 6 |
The main correctness proof: Impl implements Spec. |
3073
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 |
|
4815
b8a32ef742d9
removed split_all_tac from claset() globally within IOA
oheimb
parents:
4681
diff
changeset
|
9 |
(* repeated from Traces.ML *) |
b8a32ef742d9
removed split_all_tac from claset() globally within IOA
oheimb
parents:
4681
diff
changeset
|
10 |
claset_ref() := claset() delSWrapper "split_all_tac"; |
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
11 |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
12 |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
13 |
val hom_ioas = [Spec.ioa_def, Spec.trans_def, |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
14 |
Sender.sender_trans_def,Receiver.receiver_trans_def] |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
15 |
@ impl_ioas; |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
16 |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
17 |
val impl_asigs = [Sender.sender_asig_def,Receiver.receiver_asig_def, |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
18 |
Abschannel.srch_asig_def,Abschannel.rsch_asig_def]; |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
19 |
|
4098 | 20 |
(* Two simpsets: - simpset() is basic, ss' unfolds hom_ioas *) |
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
21 |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
22 |
Delsimps [split_paired_All]; |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
23 |
|
4098 | 24 |
val ss' = (simpset() addsimps hom_ioas); |
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
25 |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
26 |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
27 |
(* A lemma about restricting the action signature of the implementation |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
28 |
* to that of the specification. |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
29 |
****************************) |
5068 | 30 |
Goal |
5857
701498a38a76
qualified the name "restrict" since Fun.restrict exists too
paulson
parents:
5192
diff
changeset
|
31 |
"a:externals(asig_of(Automata.restrict impl_ioa (externals spec_sig))) = \ |
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
32 |
\ (case a of \ |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
33 |
\ S_msg(m) => True \ |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
34 |
\ | R_msg(m) => True \ |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
35 |
\ | S_pkt(pkt) => False \ |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
36 |
\ | R_pkt(pkt) => False \ |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
37 |
\ | S_ack(b) => False \ |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
38 |
\ | R_ack(b) => False \ |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
39 |
\ | C_m_s => False \ |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
40 |
\ | C_m_r => False \ |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
41 |
\ | C_r_s => False \ |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
42 |
\ | C_r_r(m) => False)"; |
4098 | 43 |
by (simp_tac (simpset() addsimps ([externals_def, restrict_def, |
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
44 |
restrict_asig_def, Spec.sig_def] |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
45 |
@asig_projections)) 1); |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
46 |
|
5192 | 47 |
by (induct_tac "a" 1); |
4098 | 48 |
by (ALLGOALS(simp_tac (simpset() addsimps [actions_def]@asig_projections))); |
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
49 |
(* 2 *) |
4098 | 50 |
by (simp_tac (simpset() addsimps impl_ioas) 1); |
51 |
by (simp_tac (simpset() addsimps impl_asigs) 1); |
|
52 |
by (simp_tac (simpset() addsimps |
|
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
53 |
[asig_of_par, asig_comp_def]@asig_projections) 1); |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
54 |
by (simp_tac rename_ss 1); |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
55 |
(* 1 *) |
4098 | 56 |
by (simp_tac (simpset() addsimps impl_ioas) 1); |
57 |
by (simp_tac (simpset() addsimps impl_asigs) 1); |
|
58 |
by (simp_tac (simpset() addsimps |
|
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
59 |
[asig_of_par, asig_comp_def]@asig_projections) 1); |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
60 |
qed "externals_lemma"; |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
61 |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
62 |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
63 |
val sels = [Sender.sbit_def, Sender.sq_def, Sender.ssending_def, |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
64 |
Receiver.rbit_def, Receiver.rq_def, Receiver.rsending_def]; |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
65 |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
66 |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
67 |
(* Proof of correctness *) |
5068 | 68 |
Goalw [Spec.ioa_def, is_weak_ref_map_def] |
5857
701498a38a76
qualified the name "restrict" since Fun.restrict exists too
paulson
parents:
5192
diff
changeset
|
69 |
"is_weak_ref_map hom (Automata.restrict impl_ioa (externals spec_sig)) \ |
701498a38a76
qualified the name "restrict" since Fun.restrict exists too
paulson
parents:
5192
diff
changeset
|
70 |
\ spec_ioa"; |
6916 | 71 |
by (simp_tac (simpset() delcongs [if_weak_cong] delsplits [split_if] |
72 |
addsimps [Correctness.hom_def, cancel_restrict, |
|
73 |
externals_lemma]) 1); |
|
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
74 |
by (rtac conjI 1); |
4681 | 75 |
by (simp_tac ss' 1); |
76 |
by (asm_simp_tac (simpset() addsimps sels) 1); |
|
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
77 |
by (REPEAT(rtac allI 1)); |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
78 |
by (rtac imp_conj_lemma 1); (* from lemmas.ML *) |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
79 |
|
5192 | 80 |
by (induct_tac "a" 1); |
6916 | 81 |
by (ALLGOALS (asm_simp_tac ss')); |
7499 | 82 |
by (ftac inv4 1); |
6916 | 83 |
by (Force_tac 1); |
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
84 |
|
7499 | 85 |
by (ftac inv4 1); |
86 |
by (ftac inv2 1); |
|
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
87 |
by (etac disjE 1); |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
88 |
by (Asm_simp_tac 1); |
6916 | 89 |
by (Force_tac 1); |
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
90 |
|
7499 | 91 |
by (ftac inv2 1); |
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
92 |
by (etac disjE 1); |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
93 |
|
7499 | 94 |
by (ftac inv3 1); |
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
95 |
by (case_tac "sq(sen(s))=[]" 1); |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
96 |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
97 |
by (asm_full_simp_tac ss' 1); |
6916 | 98 |
by (blast_tac (claset() addSDs [add_leD1 RS leD]) 1); |
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
99 |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
100 |
by (case_tac "m = hd(sq(sen(s)))" 1); |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
101 |
|
6916 | 102 |
by (Force_tac 1); |
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
103 |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
104 |
by (Asm_full_simp_tac 1); |
6916 | 105 |
by (blast_tac (claset() addSDs [add_leD1 RS leD]) 1); |
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
106 |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
107 |
by (Asm_full_simp_tac 1); |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
108 |
qed"ntp_correct"; |