1051
|
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();
|