|
6008
|
1 |
(* Title: HOL/IOA/example/Correctness.ML
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Olaf Mueller
|
|
|
4 |
Copyright 1997 TU Muenchen
|
|
|
5 |
|
|
|
6 |
Correctness Proof
|
|
|
7 |
*)
|
|
|
8 |
|
|
|
9 |
|
|
|
10 |
Addsimps [split_paired_All];
|
|
|
11 |
Delsimps [split_paired_Ex];
|
|
|
12 |
|
|
|
13 |
|
|
|
14 |
(* Idea: instead of impl_con_lemma do not rewrite impl_ioa, but derive
|
|
|
15 |
simple lemmas asig_of impl_ioa = impl_sig, trans_of impl_ioa = impl_trans
|
|
|
16 |
Idea: ?ex. move .. should be generally replaced by a step via a subst tac if desired,
|
|
|
17 |
as this can be done globally *)
|
|
|
18 |
|
|
|
19 |
Goal
|
|
|
20 |
"is_simulation sim_relation impl_ioa spec_ioa";
|
|
|
21 |
by (simp_tac (simpset() addsimps [is_simulation_def]) 1);
|
|
|
22 |
by (rtac conjI 1);
|
|
|
23 |
(* -------------- start states ----------------- *)
|
|
|
24 |
by (SELECT_GOAL (safe_tac set_cs) 1);
|
|
|
25 |
by (res_inst_tac [("x","({},False)")] exI 1);
|
|
|
26 |
by (asm_full_simp_tac (simpset() addsimps [sim_relation_def,starts_of_def,
|
|
|
27 |
Spec.ioa_def,Impl.ioa_def]) 1);
|
|
|
28 |
(* ---------------- main-part ------------------- *)
|
|
|
29 |
|
|
|
30 |
by (REPEAT (rtac allI 1));
|
|
6161
|
31 |
by (rtac imp_conj_lemma 1);
|
|
6008
|
32 |
ren "k b used c k' b' a" 1;
|
|
|
33 |
by (induct_tac "a" 1);
|
|
|
34 |
by (ALLGOALS (simp_tac (simpset() addsimps [sim_relation_def,
|
|
|
35 |
Impl.ioa_def,Impl.trans_def,trans_of_def])));
|
|
|
36 |
by (safe_tac set_cs);
|
|
|
37 |
(* NEW *)
|
|
|
38 |
by (res_inst_tac [("x","(used,True)")] exI 1);
|
|
|
39 |
by (Asm_full_simp_tac 1);
|
|
6161
|
40 |
by (rtac transition_is_ex 1);
|
|
6008
|
41 |
by (simp_tac (simpset() addsimps [
|
|
|
42 |
Spec.ioa_def,Spec.trans_def,trans_of_def])1);
|
|
|
43 |
(* LOC *)
|
|
|
44 |
by (res_inst_tac [("x","(used Un {k},False)")] exI 1);
|
|
|
45 |
by (Asm_full_simp_tac 1);
|
|
6161
|
46 |
by (rtac transition_is_ex 1);
|
|
6008
|
47 |
by (simp_tac (simpset() addsimps [
|
|
|
48 |
Spec.ioa_def,Spec.trans_def,trans_of_def])1);
|
|
|
49 |
by (Fast_tac 1);
|
|
|
50 |
(* FREE *)
|
|
|
51 |
by (res_inst_tac [("x","(used - {nat},c)")] exI 1);
|
|
|
52 |
by (Asm_full_simp_tac 1);
|
|
|
53 |
by (SELECT_GOAL (safe_tac set_cs) 1);
|
|
6161
|
54 |
by Auto_tac;
|
|
|
55 |
by (rtac transition_is_ex 1);
|
|
6008
|
56 |
by (simp_tac (simpset() addsimps [
|
|
|
57 |
Spec.ioa_def,Spec.trans_def,trans_of_def])1);
|
|
|
58 |
qed"issimulation";
|
|
|
59 |
|
|
|
60 |
|
|
|
61 |
|
|
|
62 |
Goalw [ioa_implements_def]
|
|
|
63 |
"impl_ioa =<| spec_ioa";
|
|
6161
|
64 |
by (rtac conjI 1);
|
|
6008
|
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,
|
|
|
67 |
asig_inputs_def]) 1);
|
|
6161
|
68 |
by (rtac trace_inclusion_for_simulations 1);
|
|
6008
|
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,
|
|
|
71 |
asig_inputs_def]) 1);
|
|
6161
|
72 |
by (rtac issimulation 1);
|
|
6008
|
73 |
qed"implementation";
|
|
|
74 |
|