13 @ impl_ioas; |
13 @ impl_ioas; |
14 |
14 |
15 val impl_asigs = [Sender.sender_asig_def,Receiver.receiver_asig_def, |
15 val impl_asigs = [Sender.sender_asig_def,Receiver.receiver_asig_def, |
16 Abschannel.srch_asig_def,Abschannel.rsch_asig_def]; |
16 Abschannel.srch_asig_def,Abschannel.rsch_asig_def]; |
17 |
17 |
18 (* Two simpsets: - !simpset is basic, ss' unfolds hom_ioas *) |
18 (* Two simpsets: - simpset() is basic, ss' unfolds hom_ioas *) |
19 |
19 |
20 Delsimps [split_paired_All]; |
20 Delsimps [split_paired_All]; |
21 |
21 |
22 val ss' = (!simpset addsimps hom_ioas); |
22 val ss' = (simpset() addsimps hom_ioas); |
23 |
23 |
24 |
24 |
25 (* A lemma about restricting the action signature of the implementation |
25 (* A lemma about restricting the action signature of the implementation |
26 * to that of the specification. |
26 * to that of the specification. |
27 ****************************) |
27 ****************************) |
36 \ | R_ack(b) => False \ |
36 \ | R_ack(b) => False \ |
37 \ | C_m_s => False \ |
37 \ | C_m_s => False \ |
38 \ | C_m_r => False \ |
38 \ | C_m_r => False \ |
39 \ | C_r_s => False \ |
39 \ | C_r_s => False \ |
40 \ | C_r_r(m) => False)"; |
40 \ | C_r_r(m) => False)"; |
41 by (simp_tac (!simpset addsimps ([externals_def, restrict_def, |
41 by (simp_tac (simpset() addsimps ([externals_def, restrict_def, |
42 restrict_asig_def, Spec.sig_def] |
42 restrict_asig_def, Spec.sig_def] |
43 @asig_projections)) 1); |
43 @asig_projections)) 1); |
44 |
44 |
45 by (Action.action.induct_tac "a" 1); |
45 by (Action.action.induct_tac "a" 1); |
46 by (ALLGOALS(simp_tac (!simpset addsimps [actions_def]@asig_projections))); |
46 by (ALLGOALS(simp_tac (simpset() addsimps [actions_def]@asig_projections))); |
47 (* 2 *) |
47 (* 2 *) |
48 by (simp_tac (!simpset addsimps impl_ioas) 1); |
48 by (simp_tac (simpset() addsimps impl_ioas) 1); |
49 by (simp_tac (!simpset addsimps impl_asigs) 1); |
49 by (simp_tac (simpset() addsimps impl_asigs) 1); |
50 by (simp_tac (!simpset addsimps |
50 by (simp_tac (simpset() addsimps |
51 [asig_of_par, asig_comp_def]@asig_projections) 1); |
51 [asig_of_par, asig_comp_def]@asig_projections) 1); |
52 by (simp_tac rename_ss 1); |
52 by (simp_tac rename_ss 1); |
53 (* 1 *) |
53 (* 1 *) |
54 by (simp_tac (!simpset addsimps impl_ioas) 1); |
54 by (simp_tac (simpset() addsimps impl_ioas) 1); |
55 by (simp_tac (!simpset addsimps impl_asigs) 1); |
55 by (simp_tac (simpset() addsimps impl_asigs) 1); |
56 by (simp_tac (!simpset addsimps |
56 by (simp_tac (simpset() addsimps |
57 [asig_of_par, asig_comp_def]@asig_projections) 1); |
57 [asig_of_par, asig_comp_def]@asig_projections) 1); |
58 qed "externals_lemma"; |
58 qed "externals_lemma"; |
59 |
59 |
60 |
60 |
61 val sels = [Sender.sbit_def, Sender.sq_def, Sender.ssending_def, |
61 val sels = [Sender.sbit_def, Sender.sq_def, Sender.ssending_def, |
64 |
64 |
65 |
65 |
66 (* Proof of correctness *) |
66 (* Proof of correctness *) |
67 goalw Correctness.thy [Spec.ioa_def, is_weak_ref_map_def] |
67 goalw Correctness.thy [Spec.ioa_def, is_weak_ref_map_def] |
68 "is_weak_ref_map hom (restrict impl_ioa (externals spec_sig)) spec_ioa"; |
68 "is_weak_ref_map hom (restrict impl_ioa (externals spec_sig)) spec_ioa"; |
69 by (simp_tac (!simpset addsimps |
69 by (simp_tac (simpset() addsimps |
70 [Correctness.hom_def, cancel_restrict, externals_lemma]) 1); |
70 [Correctness.hom_def, cancel_restrict, externals_lemma]) 1); |
71 by (rtac conjI 1); |
71 by (rtac conjI 1); |
72 by (simp_tac ss' 1); |
72 by (simp_tac ss' 1); |
73 by (asm_simp_tac (!simpset addsimps sels) 1); |
73 by (asm_simp_tac (simpset() addsimps sels) 1); |
74 by (REPEAT(rtac allI 1)); |
74 by (REPEAT(rtac allI 1)); |
75 by (rtac imp_conj_lemma 1); (* from lemmas.ML *) |
75 by (rtac imp_conj_lemma 1); (* from lemmas.ML *) |
76 |
76 |
77 by (Action.action.induct_tac "a" 1); |
77 by (Action.action.induct_tac "a" 1); |
78 by (asm_simp_tac (ss' setloop (split_tac [expand_if])) 1); |
78 by (asm_simp_tac (ss' setloop (split_tac [expand_if])) 1); |
79 by (forward_tac [inv4] 1); |
79 by (forward_tac [inv4] 1); |
80 by (fast_tac (!claset addss (!simpset addsimps [neq_Nil_conv])) 1); |
80 by (fast_tac (claset() addss (simpset() addsimps [neq_Nil_conv])) 1); |
81 by (simp_tac ss' 1); |
81 by (simp_tac ss' 1); |
82 by (simp_tac ss' 1); |
82 by (simp_tac ss' 1); |
83 by (simp_tac ss' 1); |
83 by (simp_tac ss' 1); |
84 by (simp_tac ss' 1); |
84 by (simp_tac ss' 1); |
85 by (simp_tac ss' 1); |
85 by (simp_tac ss' 1); |
89 by (asm_simp_tac ss' 1); |
89 by (asm_simp_tac ss' 1); |
90 by (forward_tac [inv4] 1); |
90 by (forward_tac [inv4] 1); |
91 by (forward_tac [inv2] 1); |
91 by (forward_tac [inv2] 1); |
92 by (etac disjE 1); |
92 by (etac disjE 1); |
93 by (Asm_simp_tac 1); |
93 by (Asm_simp_tac 1); |
94 by (fast_tac (!claset addss (!simpset addsimps [neq_Nil_conv])) 1); |
94 by (fast_tac (claset() addss (simpset() addsimps [neq_Nil_conv])) 1); |
95 |
95 |
96 by (asm_simp_tac ss' 1); |
96 by (asm_simp_tac ss' 1); |
97 by (forward_tac [inv2] 1); |
97 by (forward_tac [inv2] 1); |
98 by (etac disjE 1); |
98 by (etac disjE 1); |
99 |
99 |
100 by (forward_tac [inv3] 1); |
100 by (forward_tac [inv3] 1); |
101 by (case_tac "sq(sen(s))=[]" 1); |
101 by (case_tac "sq(sen(s))=[]" 1); |
102 |
102 |
103 by (asm_full_simp_tac ss' 1); |
103 by (asm_full_simp_tac ss' 1); |
104 by (fast_tac (!claset addSDs [add_leD1 RS leD]) 1); |
104 by (fast_tac (claset() addSDs [add_leD1 RS leD]) 1); |
105 |
105 |
106 by (case_tac "m = hd(sq(sen(s)))" 1); |
106 by (case_tac "m = hd(sq(sen(s)))" 1); |
107 |
107 |
108 by (fast_tac (!claset addss (!simpset addsimps [neq_Nil_conv])) 1); |
108 by (fast_tac (claset() addss (simpset() addsimps [neq_Nil_conv])) 1); |
109 |
109 |
110 by (Asm_full_simp_tac 1); |
110 by (Asm_full_simp_tac 1); |
111 by (fast_tac (!claset addSDs [add_leD1 RS leD]) 1); |
111 by (fast_tac (claset() addSDs [add_leD1 RS leD]) 1); |
112 |
112 |
113 by (Asm_full_simp_tac 1); |
113 by (Asm_full_simp_tac 1); |
114 qed"ntp_correct"; |
114 qed"ntp_correct"; |