| author | wenzelm |
| Thu, 15 Feb 2001 17:18:54 +0100 | |
| changeset 11145 | 3e47692e3a3e |
| parent 8741 | 61bc5ed22b62 |
| child 12218 | 6597093b77e7 |
| permissions | -rw-r--r-- |
| 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);
|
|
|
8741
61bc5ed22b62
removal of less_SucI, le_SucI from default simpset
paulson
parents:
6161
diff
changeset
|
45 |
by (asm_full_simp_tac (simpset() addsimps [less_SucI]) 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 |