author | wenzelm |
Thu, 31 Dec 2015 12:43:09 +0100 | |
changeset 62008 | cbedaddc9351 |
parent 62003 | src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy@ba465fcd0267 |
child 62192 | bdaa0eb0fc74 |
permissions | -rw-r--r-- |
62008 | 1 |
(* Title: HOL/HOLCF/IOA/SimCorrectness.thy |
40945 | 2 |
Author: Olaf Müller |
4565 | 3 |
*) |
4 |
||
62002 | 5 |
section \<open>Correctness of Simulations in HOLCF/IOA\<close> |
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 |
||
62001 | 59 |
lemma corresp_ex_simC_cons: "(corresp_ex_simC A R$((a,t)\<leadsto>xs)) s = |
25135
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: |
62003 | 79 |
"[|is_simulation R C A; reachable C s; s \<midarrow>a\<midarrow>C\<rightarrow> t; (s,s'):R|] ==> |
25135
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 assumption |
|
103 |
done |
|
104 |
||
105 |
declare Let_def [simp] |
|
106 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
107 |
lemma move_subprop1_sim: |
62003 | 108 |
"[|is_simulation R C A; reachable C s; s \<midarrow>a\<midarrow>C\<rightarrow> t; (s,s'):R|] ==> |
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
109 |
let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in |
19741 | 110 |
is_exec_frag A (s',@x. move A x s' a T')" |
111 |
apply (cut_tac move_is_move_sim) |
|
112 |
defer |
|
113 |
apply assumption+ |
|
114 |
apply (simp add: move_def) |
|
115 |
done |
|
116 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
117 |
lemma move_subprop2_sim: |
62003 | 118 |
"[|is_simulation R C A; reachable C s; s \<midarrow>a\<midarrow>C\<rightarrow> t; (s,s'):R|] ==> |
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
119 |
let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in |
19741 | 120 |
Finite (@x. move A x s' a T')" |
121 |
apply (cut_tac move_is_move_sim) |
|
122 |
defer |
|
123 |
apply assumption+ |
|
124 |
apply (simp add: move_def) |
|
125 |
done |
|
126 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
127 |
lemma move_subprop3_sim: |
62003 | 128 |
"[|is_simulation R C A; reachable C s; s \<midarrow>a\<midarrow>C\<rightarrow> t; (s,s'):R|] ==> |
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
129 |
let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in |
19741 | 130 |
laststate (s',@x. move A x s' a T') = T'" |
131 |
apply (cut_tac move_is_move_sim) |
|
132 |
defer |
|
133 |
apply assumption+ |
|
134 |
apply (simp add: move_def) |
|
135 |
done |
|
136 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
137 |
lemma move_subprop4_sim: |
62003 | 138 |
"[|is_simulation R C A; reachable C s; s \<midarrow>a\<midarrow>C\<rightarrow> t; (s,s'):R|] ==> |
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
139 |
let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
140 |
mk_trace A$((@x. move A x s' a T')) = |
62001 | 141 |
(if a:ext A then a\<leadsto>nil else nil)" |
19741 | 142 |
apply (cut_tac move_is_move_sim) |
143 |
defer |
|
144 |
apply assumption+ |
|
145 |
apply (simp add: move_def) |
|
146 |
done |
|
147 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
148 |
lemma move_subprop5_sim: |
62003 | 149 |
"[|is_simulation R C A; reachable C s; s \<midarrow>a\<midarrow>C\<rightarrow> t; (s,s'):R|] ==> |
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
150 |
let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in |
19741 | 151 |
(t,T'):R" |
152 |
apply (cut_tac move_is_move_sim) |
|
153 |
defer |
|
154 |
apply assumption+ |
|
155 |
apply (simp add: move_def) |
|
156 |
done |
|
157 |
||
158 |
||
62002 | 159 |
subsection \<open>TRACE INCLUSION Part 1: Traces coincide\<close> |
19741 | 160 |
|
161 |
subsubsection "Lemmata for <==" |
|
162 |
||
163 |
(* ------------------------------------------------------ |
|
164 |
Lemma 1 :Traces coincide |
|
165 |
------------------------------------------------------- *) |
|
166 |
||
167 |
declare split_if [split del] |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
168 |
lemma traces_coincide_sim [rule_format (no_asm)]: |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
169 |
"[|is_simulation R C A; ext C = ext A|] ==> |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
170 |
!s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'): R --> |
19741 | 171 |
mk_trace C$ex = mk_trace A$((corresp_ex_simC A R$ex) s')" |
172 |
||
62002 | 173 |
apply (tactic \<open>pair_induct_tac @{context} "ex" [@{thm is_exec_frag_def}] 1\<close>) |
19741 | 174 |
(* cons case *) |
26359 | 175 |
apply auto |
19741 | 176 |
apply (rename_tac ex a t s s') |
177 |
apply (simp add: mk_traceConc) |
|
178 |
apply (frule reachable.reachable_n) |
|
179 |
apply assumption |
|
180 |
apply (erule_tac x = "t" in allE) |
|
181 |
apply (erule_tac x = "@t'. ? ex1. (t,t') :R & move A ex1 s' a t'" in allE) |
|
182 |
apply (simp add: move_subprop5_sim [unfolded Let_def] |
|
183 |
move_subprop4_sim [unfolded Let_def] split add: split_if) |
|
184 |
done |
|
185 |
declare split_if [split] |
|
186 |
||
187 |
||
188 |
(* ----------------------------------------------------------- *) |
|
189 |
(* Lemma 2 : corresp_ex_sim is execution *) |
|
190 |
(* ----------------------------------------------------------- *) |
|
191 |
||
192 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
193 |
lemma correspsim_is_execution [rule_format (no_asm)]: |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
194 |
"[| is_simulation R C A |] ==> |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
195 |
!s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'):R |
19741 | 196 |
--> is_exec_frag A (s',(corresp_ex_simC A R$ex) s')" |
197 |
||
62002 | 198 |
apply (tactic \<open>pair_induct_tac @{context} "ex" [@{thm is_exec_frag_def}] 1\<close>) |
19741 | 199 |
(* main case *) |
26359 | 200 |
apply auto |
19741 | 201 |
apply (rename_tac ex a t s s') |
202 |
apply (rule_tac t = "@t'. ? ex1. (t,t') :R & move A ex1 s' a t'" in lemma_2_1) |
|
203 |
||
204 |
(* Finite *) |
|
205 |
apply (erule move_subprop2_sim [unfolded Let_def]) |
|
206 |
apply assumption+ |
|
207 |
apply (rule conjI) |
|
208 |
||
209 |
(* is_exec_frag *) |
|
210 |
apply (erule move_subprop1_sim [unfolded Let_def]) |
|
211 |
apply assumption+ |
|
212 |
apply (rule conjI) |
|
213 |
||
214 |
(* Induction hypothesis *) |
|
215 |
(* reachable_n looping, therefore apply it manually *) |
|
216 |
apply (erule_tac x = "t" in allE) |
|
217 |
apply (erule_tac x = "@t'. ? ex1. (t,t') :R & move A ex1 s' a t'" in allE) |
|
218 |
apply simp |
|
219 |
apply (frule reachable.reachable_n) |
|
220 |
apply assumption |
|
221 |
apply (simp add: move_subprop5_sim [unfolded Let_def]) |
|
222 |
(* laststate *) |
|
223 |
apply (erule move_subprop3_sim [unfolded Let_def, symmetric]) |
|
224 |
apply assumption+ |
|
225 |
done |
|
226 |
||
227 |
||
228 |
subsection "Main Theorem: TRACE - INCLUSION" |
|
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 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
237 |
lemma simulation_starts: |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
238 |
"[| is_simulation R C A; s:starts_of C |] |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
239 |
==> let S' = @s'. (s,s'):R & s':starts_of A in |
19741 | 240 |
(s,S'):R & S':starts_of A" |
241 |
apply (simp add: is_simulation_def corresp_ex_sim_def Int_non_empty Image_def) |
|
242 |
apply (erule conjE)+ |
|
243 |
apply (erule ballE) |
|
244 |
prefer 2 apply (blast) |
|
245 |
apply (erule exE) |
|
246 |
apply (rule someI2) |
|
247 |
apply assumption |
|
248 |
apply blast |
|
249 |
done |
|
250 |
||
45606 | 251 |
lemmas sim_starts1 = simulation_starts [unfolded Let_def, THEN conjunct1] |
252 |
lemmas sim_starts2 = simulation_starts [unfolded Let_def, THEN conjunct2] |
|
19741 | 253 |
|
254 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
255 |
lemma trace_inclusion_for_simulations: |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
256 |
"[| ext C = ext A; is_simulation R C A |] |
19741 | 257 |
==> traces C <= traces A" |
258 |
||
259 |
apply (unfold traces_def) |
|
260 |
||
261 |
apply (simp (no_asm) add: has_trace_def2) |
|
26359 | 262 |
apply auto |
19741 | 263 |
|
264 |
(* give execution of abstract automata *) |
|
265 |
apply (rule_tac x = "corresp_ex_sim A R ex" in bexI) |
|
266 |
||
267 |
(* Traces coincide, Lemma 1 *) |
|
62002 | 268 |
apply (tactic \<open>pair_tac @{context} "ex" 1\<close>) |
19741 | 269 |
apply (rename_tac s ex) |
270 |
apply (simp (no_asm) add: corresp_ex_sim_def) |
|
271 |
apply (rule_tac s = "s" in traces_coincide_sim) |
|
272 |
apply assumption+ |
|
273 |
apply (simp add: executions_def reachable.reachable_0 sim_starts1) |
|
274 |
||
275 |
(* corresp_ex_sim is execution, Lemma 2 *) |
|
62002 | 276 |
apply (tactic \<open>pair_tac @{context} "ex" 1\<close>) |
19741 | 277 |
apply (simp add: executions_def) |
278 |
apply (rename_tac s ex) |
|
279 |
||
280 |
(* start state *) |
|
281 |
apply (rule conjI) |
|
282 |
apply (simp add: sim_starts2 corresp_ex_sim_def) |
|
283 |
||
284 |
(* is-execution-fragment *) |
|
285 |
apply (simp add: corresp_ex_sim_def) |
|
286 |
apply (rule_tac s = s in correspsim_is_execution) |
|
287 |
apply assumption |
|
288 |
apply (simp add: reachable.reachable_0 sim_starts1) |
|
289 |
done |
|
17233 | 290 |
|
291 |
end |