1 (* Title: HOL/IOA/NTP/Correctness.ML |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow & Konrad Slind |
|
4 *) |
|
5 |
|
6 (* repeated from Traces.ML *) |
|
7 change_claset (fn cs => cs delSWrapper "split_all_tac"); |
|
8 |
|
9 |
|
10 val hom_ioas = [thm "Spec.ioa_def", thm "Spec.trans_def", |
|
11 sender_trans_def,receiver_trans_def] |
|
12 @ impl_ioas; |
|
13 |
|
14 val impl_asigs = [sender_asig_def,receiver_asig_def, |
|
15 srch_asig_def,rsch_asig_def]; |
|
16 |
|
17 (* Two simpsets: - simpset() is basic, ss' unfolds hom_ioas *) |
|
18 |
|
19 Delsimps [split_paired_All]; |
|
20 |
|
21 val ss' = (simpset() addsimps hom_ioas); |
|
22 |
|
23 |
|
24 (* A lemma about restricting the action signature of the implementation |
|
25 * to that of the specification. |
|
26 ****************************) |
|
27 Goal |
|
28 "a:externals(asig_of(Automata.restrict impl_ioa (externals spec_sig))) = \ |
|
29 \ (case a of \ |
|
30 \ S_msg(m) => True \ |
|
31 \ | R_msg(m) => True \ |
|
32 \ | S_pkt(pkt) => False \ |
|
33 \ | R_pkt(pkt) => False \ |
|
34 \ | S_ack(b) => False \ |
|
35 \ | R_ack(b) => False \ |
|
36 \ | C_m_s => False \ |
|
37 \ | C_m_r => False \ |
|
38 \ | C_r_s => False \ |
|
39 \ | C_r_r(m) => False)"; |
|
40 by (simp_tac (simpset() addsimps ([externals_def, restrict_def, |
|
41 restrict_asig_def, thm "Spec.sig_def"] |
|
42 @asig_projections)) 1); |
|
43 |
|
44 by (induct_tac "a" 1); |
|
45 by (ALLGOALS(simp_tac (simpset() addsimps [actions_def]@asig_projections))); |
|
46 (* 2 *) |
|
47 by (simp_tac (simpset() addsimps impl_ioas) 1); |
|
48 by (simp_tac (simpset() addsimps impl_asigs) 1); |
|
49 by (simp_tac (simpset() addsimps |
|
50 [asig_of_par, asig_comp_def]@asig_projections) 1); |
|
51 by (simp_tac rename_ss 1); |
|
52 (* 1 *) |
|
53 by (simp_tac (simpset() addsimps impl_ioas) 1); |
|
54 by (simp_tac (simpset() addsimps impl_asigs) 1); |
|
55 by (simp_tac (simpset() addsimps |
|
56 [asig_of_par, asig_comp_def]@asig_projections) 1); |
|
57 qed "externals_lemma"; |
|
58 |
|
59 |
|
60 val sels = [sbit_def, sq_def, ssending_def, |
|
61 rbit_def, rq_def, rsending_def]; |
|
62 |
|
63 |
|
64 (* Proof of correctness *) |
|
65 Goalw [thm "Spec.ioa_def", is_weak_ref_map_def] |
|
66 "is_weak_ref_map hom (Automata.restrict impl_ioa (externals spec_sig)) \ |
|
67 \ spec_ioa"; |
|
68 by (simp_tac (simpset() delcongs [if_weak_cong] delsplits [split_if] |
|
69 addsimps [thm "Correctness.hom_def", cancel_restrict, |
|
70 externals_lemma]) 1); |
|
71 by (rtac conjI 1); |
|
72 by (simp_tac ss' 1); |
|
73 by (asm_simp_tac (simpset() addsimps sels) 1); |
|
74 by (REPEAT(rtac allI 1)); |
|
75 by (rtac imp_conj_lemma 1); (* from lemmas.ML *) |
|
76 |
|
77 by (induct_tac "a" 1); |
|
78 by (ALLGOALS (asm_simp_tac ss')); |
|
79 by (ftac inv4 1); |
|
80 by (Force_tac 1); |
|
81 |
|
82 by (ftac inv4 1); |
|
83 by (ftac inv2 1); |
|
84 by (etac disjE 1); |
|
85 by (Asm_simp_tac 1); |
|
86 by (Force_tac 1); |
|
87 |
|
88 by (ftac inv2 1); |
|
89 by (etac disjE 1); |
|
90 |
|
91 by (ftac inv3 1); |
|
92 by (case_tac "sq(sen(s))=[]" 1); |
|
93 |
|
94 by (asm_full_simp_tac ss' 1); |
|
95 by (blast_tac (claset() addSDs [add_leD1 RS leD]) 1); |
|
96 |
|
97 by (case_tac "m = hd(sq(sen(s)))" 1); |
|
98 |
|
99 by (Force_tac 1); |
|
100 |
|
101 by (Asm_full_simp_tac 1); |
|
102 by (blast_tac (claset() addSDs [add_leD1 RS leD]) 1); |
|
103 |
|
104 by (Asm_full_simp_tac 1); |
|
105 qed"ntp_correct"; |
|