author | wenzelm |
Sat, 14 Jun 2008 23:19:51 +0200 | |
changeset 27208 | 5fe899199f85 |
parent 26359 | 6d437bde2f1d |
child 35174 | e15040ae75d7 |
permissions | -rw-r--r-- |
3071 | 1 |
(* Title: HOLCF/IOA/meta_theory/RefCorrectness.thy |
3275 | 2 |
ID: $Id$ |
12218 | 3 |
Author: Olaf Müller |
3071 | 4 |
*) |
5 |
||
17233 | 6 |
header {* Correctness of Refinement Mappings in HOLCF/IOA *} |
3071 | 7 |
|
17233 | 8 |
theory RefCorrectness |
9 |
imports RefMappings |
|
10 |
begin |
|
11 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
12 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
13 |
corresp_exC :: "('a,'s2)ioa => ('s1 => 's2) => ('a,'s1)pairs |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
14 |
-> ('s1 => ('a,'s2)pairs)" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
15 |
"corresp_exC A f = (fix$(LAM h ex. (%s. case ex of |
3071 | 16 |
nil => nil |
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
17 |
| x##xs => (flift1 (%pr. (@cex. move A cex (f s) (fst pr) (f (snd pr))) |
10835 | 18 |
@@ ((h$xs) (snd pr))) |
19 |
$x) )))" |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
20 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
21 |
corresp_ex :: "('a,'s2)ioa => ('s1 => 's2) => |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
22 |
('a,'s1)execution => ('a,'s2)execution" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
23 |
"corresp_ex A f ex = (f (fst ex),(corresp_exC A f$(snd ex)) (fst ex))" |
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 |
is_fair_ref_map :: "('s1 => 's2) => ('a,'s1)ioa => ('a,'s2)ioa => bool" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
27 |
"is_fair_ref_map f C A = |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
28 |
(is_ref_map f C A & |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
29 |
(! ex : executions(C). fair_ex C ex --> fair_ex A (corresp_ex A f ex)))" |
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
30 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
31 |
(* Axioms for fair trace inclusion proof support, not for the correctness proof |
17233 | 32 |
of refinement mappings! |
5976 | 33 |
Note: Everything is superseded by LiveIOA.thy! *) |
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
34 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
35 |
axiomatization where |
17233 | 36 |
corresp_laststate: |
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
37 |
"Finite ex ==> laststate (corresp_ex A f (s,ex)) = f (laststate (s,ex))" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
38 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
39 |
axiomatization where |
17233 | 40 |
corresp_Finite: |
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
41 |
"Finite (snd (corresp_ex A f (s,ex))) = Finite ex" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
42 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
43 |
axiomatization where |
17233 | 44 |
FromAtoC: |
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
45 |
"fin_often (%x. P (snd x)) (snd (corresp_ex A f (s,ex))) ==> fin_often (%y. P (f (snd y))) ex" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
46 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
47 |
axiomatization where |
17233 | 48 |
FromCtoA: |
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
49 |
"inf_often (%y. P (fst y)) ex ==> inf_often (%x. P (fst x)) (snd (corresp_ex A f (s,ex)))" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
50 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
51 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
52 |
(* Proof by case on inf W in ex: If so, ok. If not, only fin W in ex, ie there is |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
53 |
an index i from which on no W in ex. But W inf enabled, ie at least once after i |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
54 |
W is enabled. As W does not occur after i and W is enabling_persistent, W keeps |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
55 |
enabled until infinity, ie. indefinitely *) |
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
56 |
axiomatization where |
17233 | 57 |
persistent: |
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
58 |
"[|inf_often (%x. Enabled A W (snd x)) ex; en_persistent A W|] |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
59 |
==> inf_often (%x. fst x :W) ex | fin_often (%x. ~Enabled A W (snd x)) ex" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
60 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
61 |
axiomatization where |
17233 | 62 |
infpostcond: |
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
63 |
"[| is_exec_frag A (s,ex); inf_often (%x. fst x:W) ex|] |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
64 |
==> inf_often (% x. set_was_enabled A W (snd x)) ex" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
65 |
|
19741 | 66 |
|
67 |
subsection "corresp_ex" |
|
68 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
69 |
lemma corresp_exC_unfold: "corresp_exC A f = (LAM ex. (%s. case ex of |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
70 |
nil => nil |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
71 |
| x##xs => (flift1 (%pr. (@cex. move A cex (f s) (fst pr) (f (snd pr))) |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
72 |
@@ ((corresp_exC A f $xs) (snd pr))) |
19741 | 73 |
$x) ))" |
74 |
apply (rule trans) |
|
75 |
apply (rule fix_eq2) |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
76 |
apply (simp only: corresp_exC_def) |
19741 | 77 |
apply (rule beta_cfun) |
78 |
apply (simp add: flift1_def) |
|
79 |
done |
|
80 |
||
81 |
lemma corresp_exC_UU: "(corresp_exC A f$UU) s=UU" |
|
82 |
apply (subst corresp_exC_unfold) |
|
83 |
apply simp |
|
84 |
done |
|
85 |
||
86 |
lemma corresp_exC_nil: "(corresp_exC A f$nil) s = nil" |
|
87 |
apply (subst corresp_exC_unfold) |
|
88 |
apply simp |
|
89 |
done |
|
90 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
91 |
lemma corresp_exC_cons: "(corresp_exC A f$(at>>xs)) s = |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
92 |
(@cex. move A cex (f s) (fst at) (f (snd at))) |
19741 | 93 |
@@ ((corresp_exC A f$xs) (snd at))" |
94 |
apply (rule trans) |
|
95 |
apply (subst corresp_exC_unfold) |
|
96 |
apply (simp add: Consq_def flift1_def) |
|
97 |
apply simp |
|
98 |
done |
|
99 |
||
100 |
||
101 |
declare corresp_exC_UU [simp] corresp_exC_nil [simp] corresp_exC_cons [simp] |
|
102 |
||
103 |
||
104 |
||
105 |
subsection "properties of move" |
|
106 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
107 |
lemma move_is_move: |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
108 |
"[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==> |
19741 | 109 |
move A (@x. move A x (f s) a (f t)) (f s) a (f t)" |
110 |
apply (unfold is_ref_map_def) |
|
111 |
apply (subgoal_tac "? ex. move A ex (f s) a (f t) ") |
|
112 |
prefer 2 |
|
113 |
apply simp |
|
114 |
apply (erule exE) |
|
115 |
apply (rule someI) |
|
116 |
apply assumption |
|
117 |
done |
|
118 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
119 |
lemma move_subprop1: |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
120 |
"[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==> |
19741 | 121 |
is_exec_frag A (f s,@x. move A x (f s) a (f t))" |
122 |
apply (cut_tac move_is_move) |
|
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_subprop2: |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
129 |
"[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==> |
19741 | 130 |
Finite ((@x. move A x (f s) a (f t)))" |
131 |
apply (cut_tac move_is_move) |
|
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_subprop3: |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
138 |
"[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==> |
19741 | 139 |
laststate (f s,@x. move A x (f s) a (f t)) = (f t)" |
140 |
apply (cut_tac move_is_move) |
|
141 |
defer |
|
142 |
apply assumption+ |
|
143 |
apply (simp add: move_def) |
|
144 |
done |
|
145 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
146 |
lemma move_subprop4: |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
147 |
"[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==> |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
148 |
mk_trace A$((@x. move A x (f s) a (f t))) = |
19741 | 149 |
(if a:ext A then a>>nil else nil)" |
150 |
apply (cut_tac move_is_move) |
|
151 |
defer |
|
152 |
apply assumption+ |
|
153 |
apply (simp add: move_def) |
|
154 |
done |
|
155 |
||
156 |
||
157 |
(* ------------------------------------------------------------------ *) |
|
158 |
(* The following lemmata contribute to *) |
|
159 |
(* TRACE INCLUSION Part 1: Traces coincide *) |
|
160 |
(* ------------------------------------------------------------------ *) |
|
161 |
||
162 |
section "Lemmata for <==" |
|
163 |
||
164 |
(* --------------------------------------------------- *) |
|
165 |
(* Lemma 1.1: Distribution of mk_trace and @@ *) |
|
166 |
(* --------------------------------------------------- *) |
|
167 |
||
168 |
lemma mk_traceConc: "mk_trace C$(ex1 @@ ex2)= (mk_trace C$ex1) @@ (mk_trace C$ex2)" |
|
169 |
apply (simp add: mk_trace_def filter_act_def FilterConc MapConc) |
|
170 |
done |
|
171 |
||
172 |
||
173 |
||
174 |
(* ------------------------------------------------------ |
|
175 |
Lemma 1 :Traces coincide |
|
176 |
------------------------------------------------------- *) |
|
177 |
declare split_if [split del] |
|
178 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
179 |
lemma lemma_1: |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
180 |
"[|is_ref_map f C A; ext C = ext A|] ==> |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
181 |
!s. reachable C s & is_exec_frag C (s,xs) --> |
19741 | 182 |
mk_trace C$xs = mk_trace A$(snd (corresp_ex A f (s,xs)))" |
183 |
apply (unfold corresp_ex_def) |
|
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
184 |
apply (tactic {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1 *}) |
19741 | 185 |
(* cons case *) |
26359 | 186 |
apply (auto simp add: mk_traceConc) |
19741 | 187 |
apply (frule reachable.reachable_n) |
188 |
apply assumption |
|
189 |
apply (erule_tac x = "y" in allE) |
|
190 |
apply (simp add: move_subprop4 split add: split_if) |
|
191 |
done |
|
192 |
||
193 |
declare split_if [split] |
|
194 |
||
195 |
(* ------------------------------------------------------------------ *) |
|
196 |
(* The following lemmata contribute to *) |
|
197 |
(* TRACE INCLUSION Part 2: corresp_ex is execution *) |
|
198 |
(* ------------------------------------------------------------------ *) |
|
199 |
||
200 |
section "Lemmata for ==>" |
|
201 |
||
202 |
(* -------------------------------------------------- *) |
|
203 |
(* Lemma 2.1 *) |
|
204 |
(* -------------------------------------------------- *) |
|
205 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
206 |
lemma lemma_2_1 [rule_format (no_asm)]: |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
207 |
"Finite xs --> |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
208 |
(!s .is_exec_frag A (s,xs) & is_exec_frag A (t,ys) & |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
209 |
t = laststate (s,xs) |
19741 | 210 |
--> is_exec_frag A (s,xs @@ ys))" |
211 |
||
212 |
apply (rule impI) |
|
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
213 |
apply (tactic {* Seq_Finite_induct_tac @{context} 1 *}) |
19741 | 214 |
(* main case *) |
26359 | 215 |
apply (auto simp add: split_paired_all) |
19741 | 216 |
done |
217 |
||
218 |
||
219 |
(* ----------------------------------------------------------- *) |
|
220 |
(* Lemma 2 : corresp_ex is execution *) |
|
221 |
(* ----------------------------------------------------------- *) |
|
222 |
||
223 |
||
224 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
225 |
lemma lemma_2: |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
226 |
"[| is_ref_map f C A |] ==> |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
227 |
!s. reachable C s & is_exec_frag C (s,xs) |
19741 | 228 |
--> is_exec_frag A (corresp_ex A f (s,xs))" |
229 |
||
230 |
apply (unfold corresp_ex_def) |
|
231 |
||
232 |
apply simp |
|
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
233 |
apply (tactic {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1 *}) |
19741 | 234 |
(* main case *) |
26359 | 235 |
apply auto |
19741 | 236 |
apply (rule_tac t = "f y" in lemma_2_1) |
237 |
||
238 |
(* Finite *) |
|
239 |
apply (erule move_subprop2) |
|
240 |
apply assumption+ |
|
241 |
apply (rule conjI) |
|
242 |
||
243 |
(* is_exec_frag *) |
|
244 |
apply (erule move_subprop1) |
|
245 |
apply assumption+ |
|
246 |
apply (rule conjI) |
|
247 |
||
248 |
(* Induction hypothesis *) |
|
249 |
(* reachable_n looping, therefore apply it manually *) |
|
250 |
apply (erule_tac x = "y" in allE) |
|
251 |
apply simp |
|
252 |
apply (frule reachable.reachable_n) |
|
253 |
apply assumption |
|
254 |
apply simp |
|
255 |
(* laststate *) |
|
256 |
apply (erule move_subprop3 [symmetric]) |
|
257 |
apply assumption+ |
|
258 |
done |
|
259 |
||
260 |
||
261 |
subsection "Main Theorem: TRACE - INCLUSION" |
|
262 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
263 |
lemma trace_inclusion: |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
264 |
"[| ext C = ext A; is_ref_map f C A |] |
19741 | 265 |
==> traces C <= traces A" |
266 |
||
267 |
apply (unfold traces_def) |
|
268 |
||
269 |
apply (simp (no_asm) add: has_trace_def2) |
|
26359 | 270 |
apply auto |
19741 | 271 |
|
272 |
(* give execution of abstract automata *) |
|
273 |
apply (rule_tac x = "corresp_ex A f ex" in bexI) |
|
274 |
||
275 |
(* Traces coincide, Lemma 1 *) |
|
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
276 |
apply (tactic {* pair_tac @{context} "ex" 1 *}) |
19741 | 277 |
apply (erule lemma_1 [THEN spec, THEN mp]) |
278 |
apply assumption+ |
|
279 |
apply (simp add: executions_def reachable.reachable_0) |
|
280 |
||
281 |
(* corresp_ex is execution, Lemma 2 *) |
|
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
282 |
apply (tactic {* pair_tac @{context} "ex" 1 *}) |
19741 | 283 |
apply (simp add: executions_def) |
284 |
(* start state *) |
|
285 |
apply (rule conjI) |
|
286 |
apply (simp add: is_ref_map_def corresp_ex_def) |
|
287 |
(* is-execution-fragment *) |
|
288 |
apply (erule lemma_2 [THEN spec, THEN mp]) |
|
289 |
apply (simp add: reachable.reachable_0) |
|
290 |
done |
|
291 |
||
292 |
||
293 |
subsection "Corollary: FAIR TRACE - INCLUSION" |
|
294 |
||
295 |
lemma fininf: "(~inf_often P s) = fin_often P s" |
|
296 |
apply (unfold fin_often_def) |
|
297 |
apply auto |
|
298 |
done |
|
299 |
||
300 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
301 |
lemma WF_alt: "is_wfair A W (s,ex) = |
19741 | 302 |
(fin_often (%x. ~Enabled A W (snd x)) ex --> inf_often (%x. fst x :W) ex)" |
303 |
apply (simp add: is_wfair_def fin_often_def) |
|
304 |
apply auto |
|
305 |
done |
|
306 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
307 |
lemma WF_persistent: "[|is_wfair A W (s,ex); inf_often (%x. Enabled A W (snd x)) ex; |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
308 |
en_persistent A W|] |
19741 | 309 |
==> inf_often (%x. fst x :W) ex" |
310 |
apply (drule persistent) |
|
311 |
apply assumption |
|
312 |
apply (simp add: WF_alt) |
|
313 |
apply auto |
|
314 |
done |
|
315 |
||
316 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
317 |
lemma fair_trace_inclusion: "!! C A. |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
318 |
[| is_ref_map f C A; ext C = ext A; |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
319 |
!! ex. [| ex:executions C; fair_ex C ex|] ==> fair_ex A (corresp_ex A f ex) |] |
19741 | 320 |
==> fairtraces C <= fairtraces A" |
321 |
apply (simp (no_asm) add: fairtraces_def fairexecutions_def) |
|
26359 | 322 |
apply auto |
19741 | 323 |
apply (rule_tac x = "corresp_ex A f ex" in exI) |
26359 | 324 |
apply auto |
19741 | 325 |
|
326 |
(* Traces coincide, Lemma 1 *) |
|
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
327 |
apply (tactic {* pair_tac @{context} "ex" 1 *}) |
19741 | 328 |
apply (erule lemma_1 [THEN spec, THEN mp]) |
329 |
apply assumption+ |
|
330 |
apply (simp add: executions_def reachable.reachable_0) |
|
331 |
||
332 |
(* corresp_ex is execution, Lemma 2 *) |
|
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
333 |
apply (tactic {* pair_tac @{context} "ex" 1 *}) |
19741 | 334 |
apply (simp add: executions_def) |
335 |
(* start state *) |
|
336 |
apply (rule conjI) |
|
337 |
apply (simp add: is_ref_map_def corresp_ex_def) |
|
338 |
(* is-execution-fragment *) |
|
339 |
apply (erule lemma_2 [THEN spec, THEN mp]) |
|
340 |
apply (simp add: reachable.reachable_0) |
|
341 |
||
342 |
done |
|
343 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
344 |
lemma fair_trace_inclusion2: "!! C A. |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
345 |
[| inp(C) = inp(A); out(C)=out(A); |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
346 |
is_fair_ref_map f C A |] |
19741 | 347 |
==> fair_implements C A" |
348 |
apply (simp add: is_fair_ref_map_def fair_implements_def fairtraces_def fairexecutions_def) |
|
26359 | 349 |
apply auto |
19741 | 350 |
apply (rule_tac x = "corresp_ex A f ex" in exI) |
26359 | 351 |
apply auto |
352 |
||
19741 | 353 |
(* Traces coincide, Lemma 1 *) |
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
354 |
apply (tactic {* pair_tac @{context} "ex" 1 *}) |
19741 | 355 |
apply (erule lemma_1 [THEN spec, THEN mp]) |
356 |
apply (simp (no_asm) add: externals_def) |
|
357 |
apply (auto)[1] |
|
358 |
apply (simp add: executions_def reachable.reachable_0) |
|
359 |
||
360 |
(* corresp_ex is execution, Lemma 2 *) |
|
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
361 |
apply (tactic {* pair_tac @{context} "ex" 1 *}) |
19741 | 362 |
apply (simp add: executions_def) |
363 |
(* start state *) |
|
364 |
apply (rule conjI) |
|
365 |
apply (simp add: is_ref_map_def corresp_ex_def) |
|
366 |
(* is-execution-fragment *) |
|
367 |
apply (erule lemma_2 [THEN spec, THEN mp]) |
|
368 |
apply (simp add: reachable.reachable_0) |
|
369 |
||
370 |
done |
|
371 |
||
17233 | 372 |
end |