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