author | haftmann |
Thu, 20 Mar 2008 12:09:20 +0100 | |
changeset 26359 | 6d437bde2f1d |
parent 25135 | 4f8176c940cf |
child 27208 | 5fe899199f85 |
permissions | -rw-r--r-- |
4565 | 1 |
(* Title: HOLCF/IOA/meta_theory/SimCorrectness.thy |
2 |
ID: $Id$ |
|
12218 | 3 |
Author: Olaf Müller |
4565 | 4 |
*) |
5 |
||
17233 | 6 |
header {* Correctness of Simulations in HOLCF/IOA *} |
4565 | 7 |
|
17233 | 8 |
theory SimCorrectness |
9 |
imports Simulations |
|
10 |
begin |
|
11 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
12 |
definition |
4565 | 13 |
(* Note: s2 instead of s1 in last argument type !! *) |
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
14 |
corresp_ex_simC :: "('a,'s2)ioa => (('s1 * 's2)set) => ('a,'s1)pairs |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
15 |
-> ('s2 => ('a,'s2)pairs)" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
16 |
"corresp_ex_simC A R = (fix$(LAM h ex. (%s. case ex of |
4565 | 17 |
nil => nil |
18 |
| x##xs => (flift1 (%pr. let a = (fst pr); t = (snd pr); |
|
17233 | 19 |
T' = @t'. ? ex1. (t,t'):R & move A ex1 s a t' |
4565 | 20 |
in |
21 |
(@cex. move A cex s a T') |
|
10835 | 22 |
@@ ((h$xs) T')) |
23 |
$x) )))" |
|
17233 | 24 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
25 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
26 |
corresp_ex_sim :: "('a,'s2)ioa => (('s1 *'s2)set) => |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
27 |
('a,'s1)execution => ('a,'s2)execution" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
28 |
"corresp_ex_sim A R ex == let S'= (@s'.(fst ex,s'):R & s': starts_of A) |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
29 |
in |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
30 |
(S',(corresp_ex_simC A R$(snd ex)) S')" |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
31 |
|
19741 | 32 |
|
33 |
subsection "corresp_ex_sim" |
|
34 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
35 |
lemma corresp_ex_simC_unfold: "corresp_ex_simC A R = (LAM ex. (%s. case ex of |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
36 |
nil => nil |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
37 |
| x##xs => (flift1 (%pr. let a = (fst pr); t = (snd pr); |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
38 |
T' = @t'. ? ex1. (t,t'):R & move A ex1 s a t' |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
39 |
in |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
40 |
(@cex. move A cex s a T') |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
41 |
@@ ((corresp_ex_simC A R $xs) T')) |
19741 | 42 |
$x) ))" |
43 |
apply (rule trans) |
|
44 |
apply (rule fix_eq2) |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
45 |
apply (simp only: corresp_ex_simC_def) |
19741 | 46 |
apply (rule beta_cfun) |
47 |
apply (simp add: flift1_def) |
|
48 |
done |
|
49 |
||
50 |
lemma corresp_ex_simC_UU: "(corresp_ex_simC A R$UU) s=UU" |
|
51 |
apply (subst corresp_ex_simC_unfold) |
|
52 |
apply simp |
|
53 |
done |
|
54 |
||
55 |
lemma corresp_ex_simC_nil: "(corresp_ex_simC A R$nil) s = nil" |
|
56 |
apply (subst corresp_ex_simC_unfold) |
|
57 |
apply simp |
|
58 |
done |
|
59 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
60 |
lemma corresp_ex_simC_cons: "(corresp_ex_simC A R$((a,t)>>xs)) s = |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
61 |
(let T' = @t'. ? ex1. (t,t'):R & move A ex1 s a t' |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
62 |
in |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
63 |
(@cex. move A cex s a T') |
19741 | 64 |
@@ ((corresp_ex_simC A R$xs) T'))" |
65 |
apply (rule trans) |
|
66 |
apply (subst corresp_ex_simC_unfold) |
|
67 |
apply (simp add: Consq_def flift1_def) |
|
68 |
apply simp |
|
69 |
done |
|
70 |
||
71 |
||
72 |
declare corresp_ex_simC_UU [simp] corresp_ex_simC_nil [simp] corresp_ex_simC_cons [simp] |
|
73 |
||
74 |
||
75 |
subsection "properties of move" |
|
76 |
||
77 |
declare Let_def [simp del] |
|
78 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
79 |
lemma move_is_move_sim: |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
80 |
"[|is_simulation R C A; reachable C s; s -a--C-> t; (s,s'):R|] ==> |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
81 |
let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in |
19741 | 82 |
(t,T'): R & move A (@ex2. move A ex2 s' a T') s' a T'" |
83 |
apply (unfold is_simulation_def) |
|
84 |
||
85 |
(* Does not perform conditional rewriting on assumptions automatically as |
|
86 |
usual. Instantiate all variables per hand. Ask Tobias?? *) |
|
87 |
apply (subgoal_tac "? t' ex. (t,t') :R & move A ex s' a t'") |
|
88 |
prefer 2 |
|
89 |
apply simp |
|
90 |
apply (erule conjE) |
|
91 |
apply (erule_tac x = "s" in allE) |
|
92 |
apply (erule_tac x = "s'" in allE) |
|
93 |
apply (erule_tac x = "t" in allE) |
|
94 |
apply (erule_tac x = "a" in allE) |
|
95 |
apply simp |
|
96 |
(* Go on as usual *) |
|
97 |
apply (erule exE) |
|
98 |
apply (drule_tac x = "t'" and P = "%t'. ? ex. (t,t') :R & move A ex s' a t'" in someI) |
|
99 |
apply (erule exE) |
|
100 |
apply (erule conjE) |
|
101 |
apply (simp add: Let_def) |
|
102 |
apply (rule_tac x = "ex" in someI) |
|
103 |
apply (erule conjE) |
|
104 |
apply assumption |
|
105 |
done |
|
106 |
||
107 |
declare Let_def [simp] |
|
108 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
109 |
lemma move_subprop1_sim: |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
110 |
"[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==> |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
111 |
let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in |
19741 | 112 |
is_exec_frag A (s',@x. move A x s' a T')" |
113 |
apply (cut_tac move_is_move_sim) |
|
114 |
defer |
|
115 |
apply assumption+ |
|
116 |
apply (simp add: move_def) |
|
117 |
done |
|
118 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
119 |
lemma move_subprop2_sim: |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
120 |
"[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==> |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
121 |
let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in |
19741 | 122 |
Finite (@x. move A x s' a T')" |
123 |
apply (cut_tac move_is_move_sim) |
|
124 |
defer |
|
125 |
apply assumption+ |
|
126 |
apply (simp add: move_def) |
|
127 |
done |
|
128 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
129 |
lemma move_subprop3_sim: |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
130 |
"[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==> |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
131 |
let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in |
19741 | 132 |
laststate (s',@x. move A x s' a T') = T'" |
133 |
apply (cut_tac move_is_move_sim) |
|
134 |
defer |
|
135 |
apply assumption+ |
|
136 |
apply (simp add: move_def) |
|
137 |
done |
|
138 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
139 |
lemma move_subprop4_sim: |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
140 |
"[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==> |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
141 |
let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
142 |
mk_trace A$((@x. move A x s' a T')) = |
19741 | 143 |
(if a:ext A then a>>nil else nil)" |
144 |
apply (cut_tac move_is_move_sim) |
|
145 |
defer |
|
146 |
apply assumption+ |
|
147 |
apply (simp add: move_def) |
|
148 |
done |
|
149 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
150 |
lemma move_subprop5_sim: |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
151 |
"[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==> |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
152 |
let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in |
19741 | 153 |
(t,T'):R" |
154 |
apply (cut_tac move_is_move_sim) |
|
155 |
defer |
|
156 |
apply assumption+ |
|
157 |
apply (simp add: move_def) |
|
158 |
done |
|
159 |
||
160 |
||
161 |
subsection {* TRACE INCLUSION Part 1: Traces coincide *} |
|
162 |
||
163 |
subsubsection "Lemmata for <==" |
|
164 |
||
165 |
(* ------------------------------------------------------ |
|
166 |
Lemma 1 :Traces coincide |
|
167 |
------------------------------------------------------- *) |
|
168 |
||
169 |
declare split_if [split del] |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
170 |
lemma traces_coincide_sim [rule_format (no_asm)]: |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
171 |
"[|is_simulation R C A; ext C = ext A|] ==> |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
172 |
!s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'): R --> |
19741 | 173 |
mk_trace C$ex = mk_trace A$((corresp_ex_simC A R$ex) s')" |
174 |
||
175 |
apply (tactic {* pair_induct_tac "ex" [thm "is_exec_frag_def"] 1 *}) |
|
176 |
(* cons case *) |
|
26359 | 177 |
apply auto |
19741 | 178 |
apply (rename_tac ex a t s s') |
179 |
apply (simp add: mk_traceConc) |
|
180 |
apply (frule reachable.reachable_n) |
|
181 |
apply assumption |
|
182 |
apply (erule_tac x = "t" in allE) |
|
183 |
apply (erule_tac x = "@t'. ? ex1. (t,t') :R & move A ex1 s' a t'" in allE) |
|
184 |
apply (simp add: move_subprop5_sim [unfolded Let_def] |
|
185 |
move_subprop4_sim [unfolded Let_def] split add: split_if) |
|
186 |
done |
|
187 |
declare split_if [split] |
|
188 |
||
189 |
||
190 |
(* ----------------------------------------------------------- *) |
|
191 |
(* Lemma 2 : corresp_ex_sim is execution *) |
|
192 |
(* ----------------------------------------------------------- *) |
|
193 |
||
194 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
195 |
lemma correspsim_is_execution [rule_format (no_asm)]: |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
196 |
"[| is_simulation R C A |] ==> |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
197 |
!s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'):R |
19741 | 198 |
--> is_exec_frag A (s',(corresp_ex_simC A R$ex) s')" |
199 |
||
200 |
apply (tactic {* pair_induct_tac "ex" [thm "is_exec_frag_def"] 1 *}) |
|
201 |
(* main case *) |
|
26359 | 202 |
apply auto |
19741 | 203 |
apply (rename_tac ex a t s s') |
204 |
apply (rule_tac t = "@t'. ? ex1. (t,t') :R & move A ex1 s' a t'" in lemma_2_1) |
|
205 |
||
206 |
(* Finite *) |
|
207 |
apply (erule move_subprop2_sim [unfolded Let_def]) |
|
208 |
apply assumption+ |
|
209 |
apply (rule conjI) |
|
210 |
||
211 |
(* is_exec_frag *) |
|
212 |
apply (erule move_subprop1_sim [unfolded Let_def]) |
|
213 |
apply assumption+ |
|
214 |
apply (rule conjI) |
|
215 |
||
216 |
(* Induction hypothesis *) |
|
217 |
(* reachable_n looping, therefore apply it manually *) |
|
218 |
apply (erule_tac x = "t" in allE) |
|
219 |
apply (erule_tac x = "@t'. ? ex1. (t,t') :R & move A ex1 s' a t'" in allE) |
|
220 |
apply simp |
|
221 |
apply (frule reachable.reachable_n) |
|
222 |
apply assumption |
|
223 |
apply (simp add: move_subprop5_sim [unfolded Let_def]) |
|
224 |
(* laststate *) |
|
225 |
apply (erule move_subprop3_sim [unfolded Let_def, symmetric]) |
|
226 |
apply assumption+ |
|
227 |
done |
|
228 |
||
229 |
||
230 |
subsection "Main Theorem: TRACE - INCLUSION" |
|
231 |
||
232 |
(* -------------------------------------------------------------------------------- *) |
|
233 |
||
234 |
(* generate condition (s,S'):R & S':starts_of A, the first being intereting |
|
235 |
for the induction cases concerning the two lemmas correpsim_is_execution and |
|
236 |
traces_coincide_sim, the second for the start state case. |
|
237 |
S':= @s'. (s,s'):R & s':starts_of A, where s:starts_of C *) |
|
238 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
239 |
lemma simulation_starts: |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
240 |
"[| is_simulation R C A; s:starts_of C |] |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
241 |
==> let S' = @s'. (s,s'):R & s':starts_of A in |
19741 | 242 |
(s,S'):R & S':starts_of A" |
243 |
apply (simp add: is_simulation_def corresp_ex_sim_def Int_non_empty Image_def) |
|
244 |
apply (erule conjE)+ |
|
245 |
apply (erule ballE) |
|
246 |
prefer 2 apply (blast) |
|
247 |
apply (erule exE) |
|
248 |
apply (rule someI2) |
|
249 |
apply assumption |
|
250 |
apply blast |
|
251 |
done |
|
252 |
||
253 |
lemmas sim_starts1 = simulation_starts [unfolded Let_def, THEN conjunct1, standard] |
|
254 |
lemmas sim_starts2 = simulation_starts [unfolded Let_def, THEN conjunct2, standard] |
|
255 |
||
256 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
257 |
lemma trace_inclusion_for_simulations: |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
258 |
"[| ext C = ext A; is_simulation R C A |] |
19741 | 259 |
==> traces C <= traces A" |
260 |
||
261 |
apply (unfold traces_def) |
|
262 |
||
263 |
apply (simp (no_asm) add: has_trace_def2) |
|
26359 | 264 |
apply auto |
19741 | 265 |
|
266 |
(* give execution of abstract automata *) |
|
267 |
apply (rule_tac x = "corresp_ex_sim A R ex" in bexI) |
|
268 |
||
269 |
(* Traces coincide, Lemma 1 *) |
|
270 |
apply (tactic {* pair_tac "ex" 1 *}) |
|
271 |
apply (rename_tac s ex) |
|
272 |
apply (simp (no_asm) add: corresp_ex_sim_def) |
|
273 |
apply (rule_tac s = "s" in traces_coincide_sim) |
|
274 |
apply assumption+ |
|
275 |
apply (simp add: executions_def reachable.reachable_0 sim_starts1) |
|
276 |
||
277 |
(* corresp_ex_sim is execution, Lemma 2 *) |
|
278 |
apply (tactic {* pair_tac "ex" 1 *}) |
|
279 |
apply (simp add: executions_def) |
|
280 |
apply (rename_tac s ex) |
|
281 |
||
282 |
(* start state *) |
|
283 |
apply (rule conjI) |
|
284 |
apply (simp add: sim_starts2 corresp_ex_sim_def) |
|
285 |
||
286 |
(* is-execution-fragment *) |
|
287 |
apply (simp add: corresp_ex_sim_def) |
|
288 |
apply (rule_tac s = s in correspsim_is_execution) |
|
289 |
apply assumption |
|
290 |
apply (simp add: reachable.reachable_0 sim_starts1) |
|
291 |
done |
|
17233 | 292 |
|
293 |
end |