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