equal
deleted
inserted
replaced
25 |
25 |
26 |
26 |
27 (* A lemma about restricting the action signature of the implementation |
27 (* A lemma about restricting the action signature of the implementation |
28 * to that of the specification. |
28 * to that of the specification. |
29 ****************************) |
29 ****************************) |
30 goal Correctness.thy |
30 Goal |
31 "a:externals(asig_of(restrict impl_ioa (externals spec_sig))) = \ |
31 "a:externals(asig_of(restrict impl_ioa (externals spec_sig))) = \ |
32 \ (case a of \ |
32 \ (case a of \ |
33 \ S_msg(m) => True \ |
33 \ S_msg(m) => True \ |
34 \ | R_msg(m) => True \ |
34 \ | R_msg(m) => True \ |
35 \ | S_pkt(pkt) => False \ |
35 \ | S_pkt(pkt) => False \ |
64 Receiver.rbit_def, Receiver.rq_def, Receiver.rsending_def]; |
64 Receiver.rbit_def, Receiver.rq_def, Receiver.rsending_def]; |
65 |
65 |
66 |
66 |
67 |
67 |
68 (* Proof of correctness *) |
68 (* Proof of correctness *) |
69 goalw Correctness.thy [Spec.ioa_def, is_weak_ref_map_def] |
69 Goalw [Spec.ioa_def, is_weak_ref_map_def] |
70 "is_weak_ref_map hom (restrict impl_ioa (externals spec_sig)) spec_ioa"; |
70 "is_weak_ref_map hom (restrict impl_ioa (externals spec_sig)) spec_ioa"; |
71 by (simp_tac (simpset() delsplits [split_if] addsimps |
71 by (simp_tac (simpset() delsplits [split_if] addsimps |
72 [Correctness.hom_def, cancel_restrict, externals_lemma]) 1); |
72 [Correctness.hom_def, cancel_restrict, externals_lemma]) 1); |
73 by (rtac conjI 1); |
73 by (rtac conjI 1); |
74 by (simp_tac ss' 1); |
74 by (simp_tac ss' 1); |