26 by (asm_full_simp_tac (simpset() addsimps [sim_relation_def,starts_of_def, |
26 by (asm_full_simp_tac (simpset() addsimps [sim_relation_def,starts_of_def, |
27 Spec.ioa_def,Impl.ioa_def]) 1); |
27 Spec.ioa_def,Impl.ioa_def]) 1); |
28 (* ---------------- main-part ------------------- *) |
28 (* ---------------- main-part ------------------- *) |
29 |
29 |
30 by (REPEAT (rtac allI 1)); |
30 by (REPEAT (rtac allI 1)); |
31 br imp_conj_lemma 1; |
31 by (rtac imp_conj_lemma 1); |
32 ren "k b used c k' b' a" 1; |
32 ren "k b used c k' b' a" 1; |
33 by (induct_tac "a" 1); |
33 by (induct_tac "a" 1); |
34 by (ALLGOALS (simp_tac (simpset() addsimps [sim_relation_def, |
34 by (ALLGOALS (simp_tac (simpset() addsimps [sim_relation_def, |
35 Impl.ioa_def,Impl.trans_def,trans_of_def]))); |
35 Impl.ioa_def,Impl.trans_def,trans_of_def]))); |
36 by (safe_tac set_cs); |
36 by (safe_tac set_cs); |
37 (* NEW *) |
37 (* NEW *) |
38 by (res_inst_tac [("x","(used,True)")] exI 1); |
38 by (res_inst_tac [("x","(used,True)")] exI 1); |
39 by (Asm_full_simp_tac 1); |
39 by (Asm_full_simp_tac 1); |
40 br transition_is_ex 1; |
40 by (rtac transition_is_ex 1); |
41 by (simp_tac (simpset() addsimps [ |
41 by (simp_tac (simpset() addsimps [ |
42 Spec.ioa_def,Spec.trans_def,trans_of_def])1); |
42 Spec.ioa_def,Spec.trans_def,trans_of_def])1); |
43 (* LOC *) |
43 (* LOC *) |
44 by (res_inst_tac [("x","(used Un {k},False)")] exI 1); |
44 by (res_inst_tac [("x","(used Un {k},False)")] exI 1); |
45 by (Asm_full_simp_tac 1); |
45 by (Asm_full_simp_tac 1); |
46 br transition_is_ex 1; |
46 by (rtac transition_is_ex 1); |
47 by (simp_tac (simpset() addsimps [ |
47 by (simp_tac (simpset() addsimps [ |
48 Spec.ioa_def,Spec.trans_def,trans_of_def])1); |
48 Spec.ioa_def,Spec.trans_def,trans_of_def])1); |
49 by (Fast_tac 1); |
49 by (Fast_tac 1); |
50 (* FREE *) |
50 (* FREE *) |
51 by (res_inst_tac [("x","(used - {nat},c)")] exI 1); |
51 by (res_inst_tac [("x","(used - {nat},c)")] exI 1); |
52 by (Asm_full_simp_tac 1); |
52 by (Asm_full_simp_tac 1); |
53 by (SELECT_GOAL (safe_tac set_cs) 1); |
53 by (SELECT_GOAL (safe_tac set_cs) 1); |
54 auto(); |
54 by Auto_tac; |
55 br transition_is_ex 1; |
55 by (rtac transition_is_ex 1); |
56 by (simp_tac (simpset() addsimps [ |
56 by (simp_tac (simpset() addsimps [ |
57 Spec.ioa_def,Spec.trans_def,trans_of_def])1); |
57 Spec.ioa_def,Spec.trans_def,trans_of_def])1); |
58 qed"issimulation"; |
58 qed"issimulation"; |
59 |
59 |
60 |
60 |
61 |
61 |
62 Goalw [ioa_implements_def] |
62 Goalw [ioa_implements_def] |
63 "impl_ioa =<| spec_ioa"; |
63 "impl_ioa =<| spec_ioa"; |
64 br conjI 1; |
64 by (rtac conjI 1); |
65 by (simp_tac (simpset() addsimps [Impl.sig_def,Spec.sig_def, |
65 by (simp_tac (simpset() addsimps [Impl.sig_def,Spec.sig_def, |
66 Impl.ioa_def,Spec.ioa_def, asig_outputs_def,asig_of_def, |
66 Impl.ioa_def,Spec.ioa_def, asig_outputs_def,asig_of_def, |
67 asig_inputs_def]) 1); |
67 asig_inputs_def]) 1); |
68 br trace_inclusion_for_simulations 1; |
68 by (rtac trace_inclusion_for_simulations 1); |
69 by (simp_tac (simpset() addsimps [Impl.sig_def,Spec.sig_def, |
69 by (simp_tac (simpset() addsimps [Impl.sig_def,Spec.sig_def, |
70 Impl.ioa_def,Spec.ioa_def, externals_def,asig_outputs_def,asig_of_def, |
70 Impl.ioa_def,Spec.ioa_def, externals_def,asig_outputs_def,asig_of_def, |
71 asig_inputs_def]) 1); |
71 asig_inputs_def]) 1); |
72 br issimulation 1; |
72 by (rtac issimulation 1); |
73 qed"implementation"; |
73 qed"implementation"; |
74 |
74 |