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 Correctness.thy [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 [expand_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); |
75 by (asm_simp_tac (simpset() addsimps sels) 1); |
75 by (asm_simp_tac (simpset() addsimps sels) 1); |
76 by (REPEAT(rtac allI 1)); |
76 by (REPEAT(rtac allI 1)); |
77 by (rtac imp_conj_lemma 1); (* from lemmas.ML *) |
77 by (rtac imp_conj_lemma 1); (* from lemmas.ML *) |
78 |
78 |
79 by (Action.action.induct_tac "a" 1); |
79 by (Action.action.induct_tac "a" 1); |
80 by (asm_simp_tac (ss' setloop (split_tac [expand_if])) 1); |
80 by (asm_simp_tac (ss' addsplits [split_if]) 1); |
81 by (forward_tac [inv4] 1); |
81 by (forward_tac [inv4] 1); |
82 by (fast_tac (claset() addss (simpset() addsimps [neq_Nil_conv])) 1); |
82 by (fast_tac (claset() addss (simpset() addsimps [neq_Nil_conv])) 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); |