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