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