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