|
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 open Impl; |
|
10 open Spec; |
|
11 |
|
12 val hom_ss = impl_ss; |
|
13 val hom_ioas = [Spec.ioa_def, Spec.trans_def, |
|
14 Sender.sender_trans_def,Receiver.receiver_trans_def] |
|
15 @ impl_ioas; |
|
16 |
|
17 val hom_ss' = hom_ss addsimps hom_ioas; |
|
18 |
|
19 val impl_asigs = [Sender.sender_asig_def,Receiver.receiver_asig_def, |
|
20 Abschannel.srch_asig_def,Abschannel.rsch_asig_def]; |
|
21 |
|
22 |
|
23 (* A lemma about restricting the action signature of the implementation |
|
24 * to that of the specification. |
|
25 ****************************) |
|
26 goal Correctness.thy |
|
27 "a:externals(asig_of(restrict impl_ioa (externals spec_sig))) = \ |
|
28 \ (case a of \ |
|
29 \ S_msg(m) => True \ |
|
30 \ | R_msg(m) => True \ |
|
31 \ | S_pkt(pkt) => False \ |
|
32 \ | R_pkt(pkt) => False \ |
|
33 \ | S_ack(b) => False \ |
|
34 \ | R_ack(b) => False \ |
|
35 \ | C_m_s => False \ |
|
36 \ | C_m_r => False \ |
|
37 \ | C_r_s => False \ |
|
38 \ | C_r_r(m) => False)"; |
|
39 by(simp_tac (hom_ss addcongs [if_weak_cong] |
|
40 addsimps ([externals_def, restrict_def, restrict_asig_def, |
|
41 Spec.sig_def] @ asig_projections)) 1); |
|
42 |
|
43 by(Action.action.induct_tac "a" 1); |
|
44 by(ALLGOALS(simp_tac (action_ss addsimps |
|
45 (actions_def :: asig_projections @ set_lemmas)))); |
|
46 (* 2 *) |
|
47 by (simp_tac (hom_ss addsimps impl_ioas) 1); |
|
48 by (simp_tac (hom_ss addsimps impl_asigs) 1); |
|
49 by(simp_tac (hom_ss addsimps ([asig_of_par, asig_comp_def] |
|
50 @ asig_projections)) 1); |
|
51 by (simp_tac abschannel_ss 1); |
|
52 (* 1 *) |
|
53 by (simp_tac (hom_ss addsimps impl_ioas) 1); |
|
54 by (simp_tac (hom_ss addsimps impl_asigs) 1); |
|
55 by(simp_tac (hom_ss addsimps ([asig_of_par, asig_comp_def] |
|
56 @ asig_projections)) 1); |
|
57 by (simp_tac abschannel_ss 1); |
|
58 qed "externals_lemma"; |
|
59 |
|
60 |
|
61 val sels = [Sender.sbit_def, Sender.sq_def, Sender.ssending_def, |
|
62 Receiver.rbit_def, Receiver.rq_def, Receiver.rsending_def]; |
|
63 |
|
64 (* Proof of correctness *) |
|
65 goalw Correctness.thy [Spec.ioa_def, Solve.is_weak_pmap_def] |
|
66 "is_weak_pmap hom (restrict impl_ioa (externals spec_sig)) spec_ioa"; |
|
67 by(simp_tac (hom_ss addsimps |
|
68 (Correctness.hom_def::[cancel_restrict,externals_lemma])) 1); |
|
69 br conjI 1; |
|
70 by(simp_tac (hom_ss addsimps impl_ioas) 1); |
|
71 br ballI 1; |
|
72 bd CollectD 1; |
|
73 by(asm_simp_tac (hom_ss addsimps sels) 1); |
|
74 by(REPEAT(rtac allI 1)); |
|
75 br imp_conj_lemma 1; (* from lemmas.ML *) |
|
76 by(Action.action.induct_tac "a" 1); |
|
77 by(asm_simp_tac (hom_ss' setloop (split_tac [expand_if])) 1); |
|
78 by(forward_tac [inv4] 1); |
|
79 by(asm_full_simp_tac (hom_ss addsimps |
|
80 [imp_ex_equiv,neq_Nil_conv,ex_all_equiv]) 1); |
|
81 by(simp_tac hom_ss' 1); |
|
82 by(simp_tac hom_ss' 1); |
|
83 by(simp_tac hom_ss' 1); |
|
84 by(simp_tac hom_ss' 1); |
|
85 by(simp_tac hom_ss' 1); |
|
86 by(simp_tac hom_ss' 1); |
|
87 by(simp_tac hom_ss' 1); |
|
88 |
|
89 by(asm_simp_tac hom_ss' 1); |
|
90 by(forward_tac [inv4] 1); |
|
91 by(forward_tac [inv2] 1); |
|
92 be disjE 1; |
|
93 by(asm_simp_tac hom_ss 1); |
|
94 by(asm_full_simp_tac (hom_ss addsimps |
|
95 [imp_ex_equiv,neq_Nil_conv,ex_all_equiv]) 1); |
|
96 |
|
97 by(asm_simp_tac hom_ss' 1); |
|
98 by(forward_tac [inv2] 1); |
|
99 be disjE 1; |
|
100 |
|
101 by(forward_tac [inv3] 1); |
|
102 by(case_tac "sq(sen(s))=[]" 1); |
|
103 |
|
104 by(asm_full_simp_tac hom_ss' 1); |
|
105 by(fast_tac (HOL_cs addSDs [add_leD1 RS leD]) 1); |
|
106 |
|
107 by(case_tac "m = hd(sq(sen(s)))" 1); |
|
108 |
|
109 by(asm_full_simp_tac (hom_ss addsimps |
|
110 [imp_ex_equiv,neq_Nil_conv,ex_all_equiv]) 1); |
|
111 |
|
112 by(asm_full_simp_tac hom_ss 1); |
|
113 by(fast_tac (HOL_cs addSDs [add_leD1 RS leD]) 1); |
|
114 |
|
115 by(asm_full_simp_tac hom_ss 1); |
|
116 result(); |