62 |
62 |
63 val sels = [Sender.sbit_def, Sender.sq_def, Sender.ssending_def, |
63 val sels = [Sender.sbit_def, Sender.sq_def, Sender.ssending_def, |
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 |
|
68 (* Proof of correctness *) |
67 (* Proof of correctness *) |
69 Goalw [Spec.ioa_def, is_weak_ref_map_def] |
68 Goalw [Spec.ioa_def, is_weak_ref_map_def] |
70 "is_weak_ref_map hom (Automata.restrict impl_ioa (externals spec_sig)) \ |
69 "is_weak_ref_map hom (Automata.restrict impl_ioa (externals spec_sig)) \ |
71 \ spec_ioa"; |
70 \ spec_ioa"; |
72 by (simp_tac (simpset() delsplits [split_if] addsimps |
71 by (simp_tac (simpset() delcongs [if_weak_cong] delsplits [split_if] |
73 [Correctness.hom_def, cancel_restrict, externals_lemma]) 1); |
72 addsimps [Correctness.hom_def, cancel_restrict, |
|
73 externals_lemma]) 1); |
74 by (rtac conjI 1); |
74 by (rtac conjI 1); |
75 by (simp_tac ss' 1); |
75 by (simp_tac ss' 1); |
76 by (asm_simp_tac (simpset() addsimps sels) 1); |
76 by (asm_simp_tac (simpset() addsimps sels) 1); |
77 by (REPEAT(rtac allI 1)); |
77 by (REPEAT(rtac allI 1)); |
78 by (rtac imp_conj_lemma 1); (* from lemmas.ML *) |
78 by (rtac imp_conj_lemma 1); (* from lemmas.ML *) |
79 |
79 |
80 by (induct_tac "a" 1); |
80 by (induct_tac "a" 1); |
81 by (asm_simp_tac (ss' addsplits [split_if]) 1); |
81 by (ALLGOALS (asm_simp_tac ss')); |
82 by (forward_tac [inv4] 1); |
82 by (forward_tac [inv4] 1); |
83 by (fast_tac (claset() addss (simpset() addsimps [neq_Nil_conv])) 1); |
83 by (Force_tac 1); |
84 by (simp_tac ss' 1); |
|
85 by (simp_tac ss' 1); |
|
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 |
84 |
92 by (asm_simp_tac ss' 1); |
|
93 by (forward_tac [inv4] 1); |
85 by (forward_tac [inv4] 1); |
94 by (forward_tac [inv2] 1); |
86 by (forward_tac [inv2] 1); |
95 by (etac disjE 1); |
87 by (etac disjE 1); |
96 by (Asm_simp_tac 1); |
88 by (Asm_simp_tac 1); |
97 by (fast_tac (claset() addss (simpset() addsimps [neq_Nil_conv])) 1); |
89 by (Force_tac 1); |
98 |
90 |
99 by (asm_simp_tac ss' 1); |
|
100 by (forward_tac [inv2] 1); |
91 by (forward_tac [inv2] 1); |
101 by (etac disjE 1); |
92 by (etac disjE 1); |
102 |
93 |
103 by (forward_tac [inv3] 1); |
94 by (forward_tac [inv3] 1); |
104 by (case_tac "sq(sen(s))=[]" 1); |
95 by (case_tac "sq(sen(s))=[]" 1); |
105 |
96 |
106 by (asm_full_simp_tac ss' 1); |
97 by (asm_full_simp_tac ss' 1); |
107 by (fast_tac (claset() addSDs [add_leD1 RS leD]) 1); |
98 by (blast_tac (claset() addSDs [add_leD1 RS leD]) 1); |
108 |
99 |
109 by (case_tac "m = hd(sq(sen(s)))" 1); |
100 by (case_tac "m = hd(sq(sen(s)))" 1); |
110 |
101 |
111 by (fast_tac (claset() addss (simpset() addsimps [neq_Nil_conv])) 1); |
102 by (Force_tac 1); |
112 |
103 |
113 by (Asm_full_simp_tac 1); |
104 by (Asm_full_simp_tac 1); |
114 by (fast_tac (claset() addSDs [add_leD1 RS leD]) 1); |
105 by (blast_tac (claset() addSDs [add_leD1 RS leD]) 1); |
115 |
106 |
116 by (Asm_full_simp_tac 1); |
107 by (Asm_full_simp_tac 1); |
117 qed"ntp_correct"; |
108 qed"ntp_correct"; |