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