1 (* Title: HOLCF/IOA/meta_theory/SimCorrectness.ML |
|
2 ID: $Id$ |
|
3 Author: Olaf Mueller |
|
4 *) |
|
5 |
|
6 (* -------------------------------------------------------------------------------- *) |
|
7 |
|
8 section "corresp_ex_sim"; |
|
9 |
|
10 |
|
11 (* ---------------------------------------------------------------- *) |
|
12 (* corresp_ex_simC *) |
|
13 (* ---------------------------------------------------------------- *) |
|
14 |
|
15 |
|
16 Goal "corresp_ex_simC A R = (LAM ex. (%s. case ex of \ |
|
17 \ nil => nil \ |
|
18 \ | x##xs => (flift1 (%pr. let a = (fst pr); t = (snd pr); \ |
|
19 \ T' = @t'. ? ex1. (t,t'):R & move A ex1 s a t' \ |
|
20 \ in \ |
|
21 \ (@cex. move A cex s a T') \ |
|
22 \ @@ ((corresp_ex_simC A R $xs) T')) \ |
|
23 \ $x) ))"; |
|
24 by (rtac trans 1); |
|
25 by (rtac fix_eq2 1); |
|
26 by (rtac corresp_ex_simC_def 1); |
|
27 by (rtac beta_cfun 1); |
|
28 by (simp_tac (simpset() addsimps [flift1_def]) 1); |
|
29 qed"corresp_ex_simC_unfold"; |
|
30 |
|
31 Goal "(corresp_ex_simC A R$UU) s=UU"; |
|
32 by (stac corresp_ex_simC_unfold 1); |
|
33 by (Simp_tac 1); |
|
34 qed"corresp_ex_simC_UU"; |
|
35 |
|
36 Goal "(corresp_ex_simC A R$nil) s = nil"; |
|
37 by (stac corresp_ex_simC_unfold 1); |
|
38 by (Simp_tac 1); |
|
39 qed"corresp_ex_simC_nil"; |
|
40 |
|
41 Goal "(corresp_ex_simC A R$((a,t)>>xs)) s = \ |
|
42 \ (let T' = @t'. ? ex1. (t,t'):R & move A ex1 s a t' \ |
|
43 \ in \ |
|
44 \ (@cex. move A cex s a T') \ |
|
45 \ @@ ((corresp_ex_simC A R$xs) T'))"; |
|
46 by (rtac trans 1); |
|
47 by (stac corresp_ex_simC_unfold 1); |
|
48 by (asm_full_simp_tac (simpset() addsimps [Consq_def,flift1_def]) 1); |
|
49 by (Simp_tac 1); |
|
50 qed"corresp_ex_simC_cons"; |
|
51 |
|
52 |
|
53 Addsimps [corresp_ex_simC_UU,corresp_ex_simC_nil,corresp_ex_simC_cons]; |
|
54 |
|
55 |
|
56 |
|
57 (* ------------------------------------------------------------------ *) |
|
58 (* The following lemmata describe the definition *) |
|
59 (* of move in more detail *) |
|
60 (* ------------------------------------------------------------------ *) |
|
61 |
|
62 section"properties of move"; |
|
63 |
|
64 Delsimps [Let_def]; |
|
65 |
|
66 Goalw [is_simulation_def] |
|
67 "[|is_simulation R C A; reachable C s; s -a--C-> t; (s,s'):R|] ==>\ |
|
68 \ let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in \ |
|
69 \ (t,T'): R & move A (@ex2. move A ex2 s' a T') s' a T'"; |
|
70 |
|
71 (* Does not perform conditional rewriting on assumptions automatically as |
|
72 usual. Instantiate all variables per hand. Ask Tobias?? *) |
|
73 by (subgoal_tac "? t' ex. (t,t'):R & move A ex s' a t'" 1); |
|
74 by (Asm_full_simp_tac 2); |
|
75 by (etac conjE 2); |
|
76 by (eres_inst_tac [("x","s")] allE 2); |
|
77 by (eres_inst_tac [("x","s'")] allE 2); |
|
78 by (eres_inst_tac [("x","t")] allE 2); |
|
79 by (eres_inst_tac [("x","a")] allE 2); |
|
80 by (Asm_full_simp_tac 2); |
|
81 (* Go on as usual *) |
|
82 by (etac exE 1); |
|
83 by (dres_inst_tac [("x","t'"), |
|
84 ("P","%t'. ? ex.(t,t'):R & move A ex s' a t'")] someI 1); |
|
85 by (etac exE 1); |
|
86 by (etac conjE 1); |
|
87 by (asm_full_simp_tac (simpset() addsimps [Let_def]) 1); |
|
88 by (res_inst_tac [("x","ex")] someI 1); |
|
89 by (etac conjE 1); |
|
90 by (assume_tac 1); |
|
91 qed"move_is_move_sim"; |
|
92 |
|
93 |
|
94 Addsimps [Let_def]; |
|
95 |
|
96 Goal |
|
97 "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\ |
|
98 \ let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in \ |
|
99 \ is_exec_frag A (s',@x. move A x s' a T')"; |
|
100 by (cut_inst_tac [] move_is_move_sim 1); |
|
101 by (REPEAT (assume_tac 1)); |
|
102 by (asm_full_simp_tac (simpset() addsimps [move_def,Let_def]) 1); |
|
103 qed"move_subprop1_sim"; |
|
104 |
|
105 Goal |
|
106 "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\ |
|
107 \ let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in \ |
|
108 \ Finite (@x. move A x s' a T')"; |
|
109 by (cut_inst_tac [] move_is_move_sim 1); |
|
110 by (REPEAT (assume_tac 1)); |
|
111 by (asm_full_simp_tac (simpset() addsimps [move_def,Let_def]) 1); |
|
112 qed"move_subprop2_sim"; |
|
113 |
|
114 Goal |
|
115 "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\ |
|
116 \ let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in \ |
|
117 \ laststate (s',@x. move A x s' a T') = T'"; |
|
118 by (cut_inst_tac [] move_is_move_sim 1); |
|
119 by (REPEAT (assume_tac 1)); |
|
120 by (asm_full_simp_tac (simpset() addsimps [move_def,Let_def]) 1); |
|
121 qed"move_subprop3_sim"; |
|
122 |
|
123 Goal |
|
124 "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\ |
|
125 \ let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in \ |
|
126 \ mk_trace A$((@x. move A x s' a T')) = \ |
|
127 \ (if a:ext A then a>>nil else nil)"; |
|
128 by (cut_inst_tac [] move_is_move_sim 1); |
|
129 by (REPEAT (assume_tac 1)); |
|
130 by (asm_full_simp_tac (simpset() addsimps [move_def,Let_def]) 1); |
|
131 qed"move_subprop4_sim"; |
|
132 |
|
133 Goal |
|
134 "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\ |
|
135 \ let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in \ |
|
136 \ (t,T'):R"; |
|
137 by (cut_inst_tac [] move_is_move_sim 1); |
|
138 by (REPEAT (assume_tac 1)); |
|
139 by (asm_full_simp_tac (simpset() addsimps [move_def,Let_def]) 1); |
|
140 qed"move_subprop5_sim"; |
|
141 |
|
142 (* ------------------------------------------------------------------ *) |
|
143 (* The following lemmata contribute to *) |
|
144 (* TRACE INCLUSION Part 1: Traces coincide *) |
|
145 (* ------------------------------------------------------------------ *) |
|
146 |
|
147 section "Lemmata for <=="; |
|
148 |
|
149 |
|
150 (* ------------------------------------------------------ |
|
151 Lemma 1 :Traces coincide |
|
152 ------------------------------------------------------- *) |
|
153 |
|
154 Delsplits[split_if]; |
|
155 Goal |
|
156 "[|is_simulation R C A; ext C = ext A|] ==> \ |
|
157 \ !s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'): R --> \ |
|
158 \ mk_trace C$ex = mk_trace A$((corresp_ex_simC A R$ex) s')"; |
|
159 |
|
160 by (pair_induct_tac "ex" [is_exec_frag_def] 1); |
|
161 (* cons case *) |
|
162 by (safe_tac set_cs); |
|
163 by (rename_tac "ex a t s s'" 1); |
|
164 by (asm_full_simp_tac (simpset() addsimps [mk_traceConc]) 1); |
|
165 by (forward_tac [reachable.reachable_n] 1); |
|
166 by (assume_tac 1); |
|
167 by (eres_inst_tac [("x","t")] allE 1); |
|
168 by (eres_inst_tac [("x", |
|
169 "@t'. ? ex1. (t,t'):R & move A ex1 s' a t'")] |
|
170 allE 1); |
|
171 by (Asm_full_simp_tac 1); |
|
172 by (asm_full_simp_tac (simpset() addsimps |
|
173 [rewrite_rule [Let_def] move_subprop5_sim, |
|
174 rewrite_rule [Let_def] move_subprop4_sim] |
|
175 addsplits [split_if]) 1); |
|
176 qed_spec_mp"traces_coincide_sim"; |
|
177 Addsplits[split_if]; |
|
178 |
|
179 |
|
180 (* ----------------------------------------------------------- *) |
|
181 (* Lemma 2 : corresp_ex_sim is execution *) |
|
182 (* ----------------------------------------------------------- *) |
|
183 |
|
184 |
|
185 Goal |
|
186 "[| is_simulation R C A |] ==>\ |
|
187 \ !s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'):R \ |
|
188 \ --> is_exec_frag A (s',(corresp_ex_simC A R$ex) s')"; |
|
189 |
|
190 by (Asm_full_simp_tac 1); |
|
191 by (pair_induct_tac "ex" [is_exec_frag_def] 1); |
|
192 (* main case *) |
|
193 by (safe_tac set_cs); |
|
194 by (rename_tac "ex a t s s'" 1); |
|
195 by (res_inst_tac [("t", |
|
196 "@t'. ? ex1. (t,t'):R & move A ex1 s' a t'")] |
|
197 lemma_2_1 1); |
|
198 |
|
199 (* Finite *) |
|
200 by (etac (rewrite_rule [Let_def] move_subprop2_sim) 1); |
|
201 by (REPEAT (atac 1)); |
|
202 by (rtac conjI 1); |
|
203 |
|
204 (* is_exec_frag *) |
|
205 by (etac (rewrite_rule [Let_def] move_subprop1_sim) 1); |
|
206 by (REPEAT (atac 1)); |
|
207 by (rtac conjI 1); |
|
208 |
|
209 (* Induction hypothesis *) |
|
210 (* reachable_n looping, therefore apply it manually *) |
|
211 by (eres_inst_tac [("x","t")] allE 1); |
|
212 by (eres_inst_tac [("x", |
|
213 "@t'. ? ex1. (t,t'):R & move A ex1 s' a t'")] |
|
214 allE 1); |
|
215 by (Asm_full_simp_tac 1); |
|
216 by (forward_tac [reachable.reachable_n] 1); |
|
217 by (assume_tac 1); |
|
218 by (asm_full_simp_tac (simpset() addsimps |
|
219 [rewrite_rule [Let_def] move_subprop5_sim]) 1); |
|
220 (* laststate *) |
|
221 by (etac ((rewrite_rule [Let_def] move_subprop3_sim) RS sym) 1); |
|
222 by (REPEAT (atac 1)); |
|
223 qed_spec_mp"correspsim_is_execution"; |
|
224 |
|
225 |
|
226 (* -------------------------------------------------------------------------------- *) |
|
227 |
|
228 section "Main Theorem: T R A C E - I N C L U S I O N"; |
|
229 |
|
230 (* -------------------------------------------------------------------------------- *) |
|
231 |
|
232 (* generate condition (s,S'):R & S':starts_of A, the first being intereting |
|
233 for the induction cases concerning the two lemmas correpsim_is_execution and |
|
234 traces_coincide_sim, the second for the start state case. |
|
235 S':= @s'. (s,s'):R & s':starts_of A, where s:starts_of C *) |
|
236 |
|
237 Goal |
|
238 "[| is_simulation R C A; s:starts_of C |] \ |
|
239 \ ==> let S' = @s'. (s,s'):R & s':starts_of A in \ |
|
240 \ (s,S'):R & S':starts_of A"; |
|
241 by (asm_full_simp_tac (simpset() addsimps [is_simulation_def, |
|
242 corresp_ex_sim_def, Int_non_empty,Image_def]) 1); |
|
243 by (REPEAT (etac conjE 1)); |
|
244 by (etac ballE 1); |
|
245 by (Blast_tac 2); |
|
246 by (etac exE 1); |
|
247 by (rtac someI2 1); |
|
248 by (assume_tac 1); |
|
249 by (Blast_tac 1); |
|
250 qed"simulation_starts"; |
|
251 |
|
252 bind_thm("sim_starts1",(rewrite_rule [Let_def] simulation_starts) RS conjunct1); |
|
253 bind_thm("sim_starts2",(rewrite_rule [Let_def] simulation_starts) RS conjunct2); |
|
254 |
|
255 |
|
256 Goalw [traces_def] |
|
257 "[| ext C = ext A; is_simulation R C A |] \ |
|
258 \ ==> traces C <= traces A"; |
|
259 |
|
260 by (simp_tac(simpset() addsimps [has_trace_def2])1); |
|
261 by (safe_tac set_cs); |
|
262 |
|
263 (* give execution of abstract automata *) |
|
264 by (res_inst_tac[("x","corresp_ex_sim A R ex")] bexI 1); |
|
265 |
|
266 (* Traces coincide, Lemma 1 *) |
|
267 by (pair_tac "ex" 1); |
|
268 by (rename_tac "s ex" 1); |
|
269 by (simp_tac (simpset() addsimps [corresp_ex_sim_def]) 1); |
|
270 by (res_inst_tac [("s","s")] traces_coincide_sim 1); |
|
271 by (REPEAT (atac 1)); |
|
272 by (asm_full_simp_tac (simpset() addsimps [executions_def, |
|
273 reachable.reachable_0,sim_starts1]) 1); |
|
274 |
|
275 (* corresp_ex_sim is execution, Lemma 2 *) |
|
276 by (pair_tac "ex" 1); |
|
277 by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1); |
|
278 by (rename_tac "s ex" 1); |
|
279 |
|
280 (* start state *) |
|
281 by (rtac conjI 1); |
|
282 by (asm_full_simp_tac (simpset() addsimps [sim_starts2, |
|
283 corresp_ex_sim_def]) 1); |
|
284 |
|
285 (* is-execution-fragment *) |
|
286 by (asm_full_simp_tac (simpset() addsimps [corresp_ex_sim_def]) 1); |
|
287 by (res_inst_tac [("s","s")] correspsim_is_execution 1); |
|
288 by (assume_tac 1); |
|
289 by (asm_full_simp_tac (simpset() addsimps [reachable.reachable_0,sim_starts1]) 1); |
|
290 qed"trace_inclusion_for_simulations"; |
|