author | oheimb |
Sat, 15 Feb 1997 17:55:11 +0100 | |
changeset 2638 | 6c6a44b5f757 |
parent 2513 | d708d8cdc8e8 |
permissions | -rw-r--r-- |
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)"; |
|
2513
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
1949
diff
changeset
|
42 |
by (simp_tac (!simpset addsimps ([externals_def, restrict_def, |
1328 | 43 |
restrict_asig_def, Spec.sig_def] |
44 |
@asig_projections)) 1); |
|
1051 | 45 |
|
2513
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
1949
diff
changeset
|
46 |
by (Action.action.induct_tac "a" 1); |
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
1949
diff
changeset
|
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"; |
|
2513
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
1949
diff
changeset
|
70 |
by (simp_tac (!simpset addsimps |
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
1949
diff
changeset
|
71 |
[Correctness.hom_def, cancel_restrict, externals_lemma]) 1); |
1465 | 72 |
by (rtac conjI 1); |
2513
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
1949
diff
changeset
|
73 |
by (simp_tac ss' 1); |
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
1949
diff
changeset
|
74 |
by (asm_simp_tac (!simpset addsimps sels) 1); |
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
1949
diff
changeset
|
75 |
by (REPEAT(rtac allI 1)); |
1465 | 76 |
by (rtac imp_conj_lemma 1); (* from lemmas.ML *) |
1328 | 77 |
|
2513
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
1949
diff
changeset
|
78 |
by (Action.action.induct_tac "a" 1); |
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
1949
diff
changeset
|
79 |
by (asm_simp_tac (ss' setloop (split_tac [expand_if])) 1); |
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
1949
diff
changeset
|
80 |
by (forward_tac [inv4] 1); |
2638
6c6a44b5f757
reflecting my recent changes of the classical reasoner
oheimb
parents:
2513
diff
changeset
|
81 |
by (fast_tac (!claset unsafe_addss (!simpset addsimps [neq_Nil_conv])) 1); |
2513
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
1949
diff
changeset
|
82 |
by (simp_tac ss' 1); |
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
1949
diff
changeset
|
83 |
by (simp_tac ss' 1); |
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
1949
diff
changeset
|
84 |
by (simp_tac ss' 1); |
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
1949
diff
changeset
|
85 |
by (simp_tac ss' 1); |
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
1949
diff
changeset
|
86 |
by (simp_tac ss' 1); |
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
1949
diff
changeset
|
87 |
by (simp_tac ss' 1); |
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
1949
diff
changeset
|
88 |
by (simp_tac ss' 1); |
1051 | 89 |
|
2513
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
1949
diff
changeset
|
90 |
by (asm_simp_tac ss' 1); |
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
1949
diff
changeset
|
91 |
by (forward_tac [inv4] 1); |
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
1949
diff
changeset
|
92 |
by (forward_tac [inv2] 1); |
1465 | 93 |
by (etac disjE 1); |
2513
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
1949
diff
changeset
|
94 |
by (Asm_simp_tac 1); |
2638
6c6a44b5f757
reflecting my recent changes of the classical reasoner
oheimb
parents:
2513
diff
changeset
|
95 |
by (fast_tac (!claset unsafe_addss (!simpset addsimps [neq_Nil_conv])) 1); |
1051 | 96 |
|
2513
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
1949
diff
changeset
|
97 |
by (asm_simp_tac ss' 1); |
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
1949
diff
changeset
|
98 |
by (forward_tac [inv2] 1); |
1465 | 99 |
by (etac disjE 1); |
1051 | 100 |
|
2513
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
1949
diff
changeset
|
101 |
by (forward_tac [inv3] 1); |
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
1949
diff
changeset
|
102 |
by (case_tac "sq(sen(s))=[]" 1); |
1051 | 103 |
|
2513
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
1949
diff
changeset
|
104 |
by (asm_full_simp_tac ss' 1); |
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
1949
diff
changeset
|
105 |
by (fast_tac (!claset addSDs [add_leD1 RS leD]) 1); |
1051 | 106 |
|
2513
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
1949
diff
changeset
|
107 |
by (case_tac "m = hd(sq(sen(s)))" 1); |
1051 | 108 |
|
2638
6c6a44b5f757
reflecting my recent changes of the classical reasoner
oheimb
parents:
2513
diff
changeset
|
109 |
by (fast_tac (!claset unsafe_addss (!simpset addsimps [neq_Nil_conv])) 1); |
1051 | 110 |
|
2513
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
1949
diff
changeset
|
111 |
by (Asm_full_simp_tac 1); |
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
1949
diff
changeset
|
112 |
by (fast_tac (!claset addSDs [add_leD1 RS leD]) 1); |
1051 | 113 |
|
2513
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
1949
diff
changeset
|
114 |
by (Asm_full_simp_tac 1); |
1342 | 115 |
qed"ntp_correct"; |