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 |
|
1328
|
9 |
|
|
10 |
open Impl Spec;
|
1051
|
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,
|
1328
|
17 |
Abschannel.srch_asig_def,Abschannel.rsch_asig_def];
|
1051
|
18 |
|
1328
|
19 |
(* Two simpsets: - !simpset is basic, ss' unfolds hom_ioas *)
|
1266
|
20 |
|
1328
|
21 |
Delsimps [split_paired_All];
|
|
22 |
|
|
23 |
val ss' = (!simpset addsimps hom_ioas);
|
1266
|
24 |
|
1051
|
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)";
|
1328
|
42 |
by(simp_tac (!simpset addsimps ([externals_def, restrict_def,
|
|
43 |
restrict_asig_def, Spec.sig_def]
|
|
44 |
@asig_projections)) 1);
|
1051
|
45 |
|
|
46 |
by(Action.action.induct_tac "a" 1);
|
1328
|
47 |
by(ALLGOALS(simp_tac (!simpset addsimps [actions_def]@asig_projections)));
|
1051
|
48 |
(* 2 *)
|
1328
|
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);
|
1051
|
54 |
(* 1 *)
|
1328
|
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);
|
1051
|
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 |
|
1328
|
65 |
|
|
66 |
|
1051
|
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";
|
1328
|
70 |
by(simp_tac (!simpset addsimps
|
|
71 |
[Correctness.hom_def,
|
|
72 |
cancel_restrict,externals_lemma]) 1);
|
1051
|
73 |
br conjI 1;
|
1328
|
74 |
by(simp_tac ss' 1);
|
1051
|
75 |
br ballI 1;
|
|
76 |
bd CollectD 1;
|
1266
|
77 |
by(asm_simp_tac (!simpset addsimps sels) 1);
|
1051
|
78 |
by(REPEAT(rtac allI 1));
|
|
79 |
br imp_conj_lemma 1; (* from lemmas.ML *)
|
1328
|
80 |
|
1051
|
81 |
by(Action.action.induct_tac "a" 1);
|
1266
|
82 |
by(asm_simp_tac (ss' setloop (split_tac [expand_if])) 1);
|
1051
|
83 |
by(forward_tac [inv4] 1);
|
1328
|
84 |
by(asm_full_simp_tac (!simpset addsimps
|
|
85 |
[imp_ex_equiv,neq_Nil_conv,ex_all_equiv]) 1);
|
1266
|
86 |
by(simp_tac ss' 1);
|
|
87 |
by(simp_tac ss' 1);
|
|
88 |
by(simp_tac ss' 1);
|
|
89 |
by(simp_tac ss' 1);
|
|
90 |
by(simp_tac ss' 1);
|
|
91 |
by(simp_tac ss' 1);
|
|
92 |
by(simp_tac ss' 1);
|
1051
|
93 |
|
1266
|
94 |
by(asm_simp_tac ss' 1);
|
1051
|
95 |
by(forward_tac [inv4] 1);
|
|
96 |
by(forward_tac [inv2] 1);
|
|
97 |
be disjE 1;
|
1328
|
98 |
by(Asm_simp_tac 1);
|
|
99 |
by(asm_full_simp_tac (!simpset addsimps [imp_ex_equiv,neq_Nil_conv,ex_all_equiv]) 1);
|
1051
|
100 |
|
1266
|
101 |
by(asm_simp_tac ss' 1);
|
1051
|
102 |
by(forward_tac [inv2] 1);
|
|
103 |
be disjE 1;
|
|
104 |
|
|
105 |
by(forward_tac [inv3] 1);
|
|
106 |
by(case_tac "sq(sen(s))=[]" 1);
|
|
107 |
|
1266
|
108 |
by(asm_full_simp_tac ss' 1);
|
1051
|
109 |
by(fast_tac (HOL_cs addSDs [add_leD1 RS leD]) 1);
|
|
110 |
|
|
111 |
by(case_tac "m = hd(sq(sen(s)))" 1);
|
|
112 |
|
1328
|
113 |
by(asm_full_simp_tac (!simpset addsimps
|
1051
|
114 |
[imp_ex_equiv,neq_Nil_conv,ex_all_equiv]) 1);
|
|
115 |
|
1328
|
116 |
by(Asm_full_simp_tac 1);
|
1051
|
117 |
by(fast_tac (HOL_cs addSDs [add_leD1 RS leD]) 1);
|
|
118 |
|
1328
|
119 |
by(Asm_full_simp_tac 1);
|
1051
|
120 |
result();
|