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/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 |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
4 |
|
12218 | 5 |
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
|
6 |
*) |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
7 |
|
4815
b8a32ef742d9
removed split_all_tac from claset() globally within IOA
oheimb
parents:
4681
diff
changeset
|
8 |
(* repeated from Traces.ML *) |
b8a32ef742d9
removed split_all_tac from claset() globally within IOA
oheimb
parents:
4681
diff
changeset
|
9 |
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
|
10 |
|
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 |
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
|
13 |
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
|
14 |
@ impl_ioas; |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
15 |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
16 |
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
|
17 |
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
|
18 |
|
4098 | 19 |
(* 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
|
20 |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
21 |
Delsimps [split_paired_All]; |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
22 |
|
4098 | 23 |
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
|
24 |
|
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 |
(* 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
|
27 |
* to that of the specification. |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
28 |
****************************) |
5068 | 29 |
Goal |
5857
701498a38a76
qualified the name "restrict" since Fun.restrict exists too
paulson
parents:
5192
diff
changeset
|
30 |
"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
|
31 |
\ (case a of \ |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
32 |
\ S_msg(m) => True \ |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
33 |
\ | R_msg(m) => True \ |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
34 |
\ | S_pkt(pkt) => False \ |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
35 |
\ | R_pkt(pkt) => False \ |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
36 |
\ | S_ack(b) => False \ |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
37 |
\ | R_ack(b) => False \ |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
38 |
\ | C_m_s => False \ |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
39 |
\ | C_m_r => False \ |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
40 |
\ | C_r_s => False \ |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
41 |
\ | C_r_r(m) => False)"; |
4098 | 42 |
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
|
43 |
restrict_asig_def, Spec.sig_def] |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
44 |
@asig_projections)) 1); |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
45 |
|
5192 | 46 |
by (induct_tac "a" 1); |
4098 | 47 |
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
|
48 |
(* 2 *) |
4098 | 49 |
by (simp_tac (simpset() addsimps impl_ioas) 1); |
50 |
by (simp_tac (simpset() addsimps impl_asigs) 1); |
|
51 |
by (simp_tac (simpset() addsimps |
|
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
52 |
[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
|
53 |
by (simp_tac rename_ss 1); |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
54 |
(* 1 *) |
4098 | 55 |
by (simp_tac (simpset() addsimps impl_ioas) 1); |
56 |
by (simp_tac (simpset() addsimps impl_asigs) 1); |
|
57 |
by (simp_tac (simpset() addsimps |
|
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
58 |
[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
|
59 |
qed "externals_lemma"; |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
60 |
|
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 |
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
|
63 |
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
|
64 |
|
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 |
(* Proof of correctness *) |
5068 | 67 |
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
|
68 |
"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
|
69 |
\ spec_ioa"; |
6916 | 70 |
by (simp_tac (simpset() delcongs [if_weak_cong] delsplits [split_if] |
71 |
addsimps [Correctness.hom_def, cancel_restrict, |
|
72 |
externals_lemma]) 1); |
|
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
73 |
by (rtac conjI 1); |
4681 | 74 |
by (simp_tac ss' 1); |
75 |
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
|
76 |
by (REPEAT(rtac allI 1)); |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
77 |
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
|
78 |
|
5192 | 79 |
by (induct_tac "a" 1); |
6916 | 80 |
by (ALLGOALS (asm_simp_tac ss')); |
7499 | 81 |
by (ftac inv4 1); |
6916 | 82 |
by (Force_tac 1); |
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
83 |
|
7499 | 84 |
by (ftac inv4 1); |
85 |
by (ftac inv2 1); |
|
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
86 |
by (etac disjE 1); |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
87 |
by (Asm_simp_tac 1); |
6916 | 88 |
by (Force_tac 1); |
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
89 |
|
7499 | 90 |
by (ftac inv2 1); |
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
91 |
by (etac disjE 1); |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
92 |
|
7499 | 93 |
by (ftac inv3 1); |
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
94 |
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
|
95 |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
96 |
by (asm_full_simp_tac ss' 1); |
6916 | 97 |
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
|
98 |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
99 |
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
|
100 |
|
6916 | 101 |
by (Force_tac 1); |
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
102 |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
103 |
by (Asm_full_simp_tac 1); |
6916 | 104 |
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
|
105 |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
106 |
by (Asm_full_simp_tac 1); |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
107 |
qed"ntp_correct"; |