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