author | wenzelm |
Sat, 14 Jun 2008 23:19:51 +0200 | |
changeset 27208 | 5fe899199f85 |
parent 26359 | 6d437bde2f1d |
child 30607 | c3d1590debd8 |
permissions | -rw-r--r-- |
4559 | 1 |
(* Title: HOLCF/IOA/meta_theory/Abstraction.thy |
2 |
ID: $Id$ |
|
12218 | 3 |
Author: Olaf Müller |
17233 | 4 |
*) |
4559 | 5 |
|
17233 | 6 |
header {* Abstraction Theory -- tailored for I/O automata *} |
4559 | 7 |
|
17233 | 8 |
theory Abstraction |
9 |
imports LiveIOA |
|
23560 | 10 |
uses ("ioa_package.ML") |
17233 | 11 |
begin |
4559 | 12 |
|
17233 | 13 |
defaultsort type |
4559 | 14 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
15 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
16 |
cex_abs :: "('s1 => 's2) => ('a,'s1)execution => ('a,'s2)execution" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
17 |
"cex_abs f ex = (f (fst ex), Map (%(a,t). (a,f t))$(snd ex))" |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
18 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
19 |
-- {* equals cex_abs on Sequences -- after ex2seq application *} |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
20 |
cex_absSeq :: "('s1 => 's2) => ('a option,'s1)transition Seq => ('a option,'s2)transition Seq" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
21 |
"cex_absSeq f = (%s. Map (%(s,a,t). (f s,a,f t))$s)" |
4559 | 22 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
23 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
24 |
is_abstraction ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
25 |
"is_abstraction f C A = |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
26 |
((!s:starts_of(C). f(s):starts_of(A)) & |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
27 |
(!s t a. reachable C s & s -a--C-> t |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
28 |
--> (f s) -a--A-> (f t)))" |
4559 | 29 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
30 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
31 |
weakeningIOA :: "('a,'s2)ioa => ('a,'s1)ioa => ('s1 => 's2) => bool" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
32 |
"weakeningIOA A C h = (!ex. ex : executions C --> cex_abs h ex : executions A)" |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
33 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
34 |
temp_strengthening :: "('a,'s2)ioa_temp => ('a,'s1)ioa_temp => ('s1 => 's2) => bool" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
35 |
"temp_strengthening Q P h = (!ex. (cex_abs h ex |== Q) --> (ex |== P))" |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
36 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
37 |
temp_weakening :: "('a,'s2)ioa_temp => ('a,'s1)ioa_temp => ('s1 => 's2) => bool" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
38 |
"temp_weakening Q P h = temp_strengthening (.~ Q) (.~ P) h" |
4559 | 39 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
40 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
41 |
state_strengthening :: "('a,'s2)step_pred => ('a,'s1)step_pred => ('s1 => 's2) => bool" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
42 |
"state_strengthening Q P h = (!s t a. Q (h(s),a,h(t)) --> P (s,a,t))" |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
43 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
44 |
state_weakening :: "('a,'s2)step_pred => ('a,'s1)step_pred => ('s1 => 's2) => bool" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
45 |
"state_weakening Q P h = state_strengthening (.~Q) (.~P) h" |
4559 | 46 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
47 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
48 |
is_live_abstraction :: "('s1 => 's2) => ('a,'s1)live_ioa => ('a,'s2)live_ioa => bool" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
49 |
"is_live_abstraction h CL AM = |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
50 |
(is_abstraction h (fst CL) (fst AM) & |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
51 |
temp_weakening (snd AM) (snd CL) h)" |
4559 | 52 |
|
53 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
54 |
axiomatization where |
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
55 |
(* thm about ex2seq which is not provable by induction as ex2seq is not continous *) |
17233 | 56 |
ex2seq_abs_cex: |
57 |
"ex2seq (cex_abs h ex) = cex_absSeq h (ex2seq ex)" |
|
4559 | 58 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
59 |
axiomatization where |
5976 | 60 |
(* analog to the proved thm strength_Box - proof skipped as trivial *) |
17233 | 61 |
weak_Box: |
62 |
"temp_weakening P Q h |
|
4559 | 63 |
==> temp_weakening ([] P) ([] Q) h" |
64 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
65 |
axiomatization where |
5976 | 66 |
(* analog to the proved thm strength_Next - proof skipped as trivial *) |
17233 | 67 |
weak_Next: |
68 |
"temp_weakening P Q h |
|
4559 | 69 |
==> temp_weakening (Next P) (Next Q) h" |
70 |
||
19741 | 71 |
|
72 |
subsection "cex_abs" |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
73 |
|
19741 | 74 |
lemma cex_abs_UU: "cex_abs f (s,UU) = (f s, UU)" |
75 |
by (simp add: cex_abs_def) |
|
76 |
||
77 |
lemma cex_abs_nil: "cex_abs f (s,nil) = (f s, nil)" |
|
78 |
by (simp add: cex_abs_def) |
|
79 |
||
80 |
lemma cex_abs_cons: "cex_abs f (s,(a,t)>>ex) = (f s, (a,f t) >> (snd (cex_abs f (t,ex))))" |
|
81 |
by (simp add: cex_abs_def) |
|
82 |
||
83 |
declare cex_abs_UU [simp] cex_abs_nil [simp] cex_abs_cons [simp] |
|
84 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
85 |
|
19741 | 86 |
subsection "lemmas" |
87 |
||
88 |
lemma temp_weakening_def2: "temp_weakening Q P h = (! ex. (ex |== P) --> (cex_abs h ex |== Q))" |
|
89 |
apply (simp add: temp_weakening_def temp_strengthening_def NOT_def temp_sat_def satisfies_def) |
|
90 |
apply auto |
|
91 |
done |
|
92 |
||
93 |
lemma state_weakening_def2: "state_weakening Q P h = (! s t a. P (s,a,t) --> Q (h(s),a,h(t)))" |
|
94 |
apply (simp add: state_weakening_def state_strengthening_def NOT_def) |
|
95 |
apply auto |
|
96 |
done |
|
97 |
||
98 |
||
99 |
subsection "Abstraction Rules for Properties" |
|
100 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
101 |
lemma exec_frag_abstraction [rule_format]: |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
102 |
"[| is_abstraction h C A |] ==> |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
103 |
!s. reachable C s & is_exec_frag C (s,xs) |
19741 | 104 |
--> is_exec_frag A (cex_abs h (s,xs))" |
105 |
apply (unfold cex_abs_def) |
|
106 |
apply simp |
|
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
107 |
apply (tactic {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1 *}) |
19741 | 108 |
txt {* main case *} |
26359 | 109 |
apply (auto dest: reachable.reachable_n simp add: is_abstraction_def) |
19741 | 110 |
done |
111 |
||
112 |
||
113 |
lemma abs_is_weakening: "is_abstraction h C A ==> weakeningIOA A C h" |
|
114 |
apply (simp add: weakeningIOA_def) |
|
115 |
apply auto |
|
116 |
apply (simp add: executions_def) |
|
117 |
txt {* start state *} |
|
118 |
apply (rule conjI) |
|
119 |
apply (simp add: is_abstraction_def cex_abs_def) |
|
120 |
txt {* is-execution-fragment *} |
|
121 |
apply (erule exec_frag_abstraction) |
|
122 |
apply (simp add: reachable.reachable_0) |
|
123 |
done |
|
124 |
||
125 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
126 |
lemma AbsRuleT1: "[|is_abstraction h C A; validIOA A Q; temp_strengthening Q P h |] |
19741 | 127 |
==> validIOA C P" |
128 |
apply (drule abs_is_weakening) |
|
129 |
apply (simp add: weakeningIOA_def validIOA_def temp_strengthening_def) |
|
26359 | 130 |
apply (auto simp add: split_paired_all) |
19741 | 131 |
done |
132 |
||
133 |
||
134 |
(* FIX: Nach TLS.ML *) |
|
135 |
||
136 |
lemma IMPLIES_temp_sat: "(ex |== P .--> Q) = ((ex |== P) --> (ex |== Q))" |
|
137 |
by (simp add: IMPLIES_def temp_sat_def satisfies_def) |
|
138 |
||
139 |
lemma AND_temp_sat: "(ex |== P .& Q) = ((ex |== P) & (ex |== Q))" |
|
140 |
by (simp add: AND_def temp_sat_def satisfies_def) |
|
141 |
||
142 |
lemma OR_temp_sat: "(ex |== P .| Q) = ((ex |== P) | (ex |== Q))" |
|
143 |
by (simp add: OR_def temp_sat_def satisfies_def) |
|
144 |
||
145 |
lemma NOT_temp_sat: "(ex |== .~ P) = (~ (ex |== P))" |
|
146 |
by (simp add: NOT_def temp_sat_def satisfies_def) |
|
147 |
||
148 |
declare IMPLIES_temp_sat [simp] AND_temp_sat [simp] OR_temp_sat [simp] NOT_temp_sat [simp] |
|
149 |
||
150 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
151 |
lemma AbsRuleT2: |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
152 |
"[|is_live_abstraction h (C,L) (A,M); |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
153 |
validLIOA (A,M) Q; temp_strengthening Q P h |] |
19741 | 154 |
==> validLIOA (C,L) P" |
155 |
apply (unfold is_live_abstraction_def) |
|
156 |
apply auto |
|
157 |
apply (drule abs_is_weakening) |
|
158 |
apply (simp add: weakeningIOA_def temp_weakening_def2 validLIOA_def validIOA_def temp_strengthening_def) |
|
26359 | 159 |
apply (auto simp add: split_paired_all) |
19741 | 160 |
done |
161 |
||
162 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
163 |
lemma AbsRuleTImprove: |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
164 |
"[|is_live_abstraction h (C,L) (A,M); |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
165 |
validLIOA (A,M) (H1 .--> Q); temp_strengthening Q P h; |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
166 |
temp_weakening H1 H2 h; validLIOA (C,L) H2 |] |
19741 | 167 |
==> validLIOA (C,L) P" |
168 |
apply (unfold is_live_abstraction_def) |
|
169 |
apply auto |
|
170 |
apply (drule abs_is_weakening) |
|
171 |
apply (simp add: weakeningIOA_def temp_weakening_def2 validLIOA_def validIOA_def temp_strengthening_def) |
|
26359 | 172 |
apply (auto simp add: split_paired_all) |
19741 | 173 |
done |
174 |
||
175 |
||
176 |
subsection "Correctness of safe abstraction" |
|
177 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
178 |
lemma abstraction_is_ref_map: |
19741 | 179 |
"is_abstraction h C A ==> is_ref_map h C A" |
180 |
apply (unfold is_abstraction_def is_ref_map_def) |
|
26359 | 181 |
apply auto |
19741 | 182 |
apply (rule_tac x = "(a,h t) >>nil" in exI) |
183 |
apply (simp add: move_def) |
|
184 |
done |
|
185 |
||
186 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
187 |
lemma abs_safety: "[| inp(C)=inp(A); out(C)=out(A); |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
188 |
is_abstraction h C A |] |
19741 | 189 |
==> C =<| A" |
190 |
apply (simp add: ioa_implements_def) |
|
191 |
apply (rule trace_inclusion) |
|
192 |
apply (simp (no_asm) add: externals_def) |
|
193 |
apply (auto)[1] |
|
194 |
apply (erule abstraction_is_ref_map) |
|
195 |
done |
|
196 |
||
197 |
||
198 |
subsection "Correctness of life abstraction" |
|
199 |
||
200 |
(* Reduces to Filter (Map fst x) = Filter (Map fst (Map (%(a,t). (a,x)) x), |
|
201 |
that is to special Map Lemma *) |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
202 |
lemma traces_coincide_abs: |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
203 |
"ext C = ext A |
19741 | 204 |
==> mk_trace C$xs = mk_trace A$(snd (cex_abs f (s,xs)))" |
205 |
apply (unfold cex_abs_def mk_trace_def filter_act_def) |
|
206 |
apply simp |
|
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
207 |
apply (tactic {* pair_induct_tac @{context} "xs" [] 1 *}) |
19741 | 208 |
done |
209 |
||
210 |
||
211 |
(* Does not work with abstraction_is_ref_map as proof of abs_safety, because |
|
212 |
is_live_abstraction includes temp_strengthening which is necessarily based |
|
213 |
on cex_abs and not on corresp_ex. Thus, the proof is redoone in a more specific |
|
214 |
way for cex_abs *) |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
215 |
lemma abs_liveness: "[| inp(C)=inp(A); out(C)=out(A); |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
216 |
is_live_abstraction h (C,M) (A,L) |] |
19741 | 217 |
==> live_implements (C,M) (A,L)" |
218 |
apply (simp add: is_live_abstraction_def live_implements_def livetraces_def liveexecutions_def) |
|
26359 | 219 |
apply auto |
19741 | 220 |
apply (rule_tac x = "cex_abs h ex" in exI) |
26359 | 221 |
apply auto |
19741 | 222 |
(* Traces coincide *) |
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
223 |
apply (tactic {* pair_tac @{context} "ex" 1 *}) |
19741 | 224 |
apply (rule traces_coincide_abs) |
225 |
apply (simp (no_asm) add: externals_def) |
|
226 |
apply (auto)[1] |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
227 |
|
19741 | 228 |
(* cex_abs is execution *) |
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
229 |
apply (tactic {* pair_tac @{context} "ex" 1 *}) |
19741 | 230 |
apply (simp add: executions_def) |
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
231 |
(* start state *) |
19741 | 232 |
apply (rule conjI) |
233 |
apply (simp add: is_abstraction_def cex_abs_def) |
|
234 |
(* is-execution-fragment *) |
|
235 |
apply (erule exec_frag_abstraction) |
|
236 |
apply (simp add: reachable.reachable_0) |
|
237 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
238 |
(* Liveness *) |
19741 | 239 |
apply (simp add: temp_weakening_def2) |
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
240 |
apply (tactic {* pair_tac @{context} "ex" 1 *}) |
19741 | 241 |
done |
242 |
||
243 |
(* FIX: NAch Traces.ML bringen *) |
|
244 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
245 |
lemma implements_trans: |
19741 | 246 |
"[| A =<| B; B =<| C|] ==> A =<| C" |
26359 | 247 |
by (auto simp add: ioa_implements_def) |
19741 | 248 |
|
249 |
||
250 |
subsection "Abstraction Rules for Automata" |
|
251 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
252 |
lemma AbsRuleA1: "[| inp(C)=inp(A); out(C)=out(A); |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
253 |
inp(Q)=inp(P); out(Q)=out(P); |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
254 |
is_abstraction h1 C A; |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
255 |
A =<| Q ; |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
256 |
is_abstraction h2 Q P |] |
19741 | 257 |
==> C =<| P" |
258 |
apply (drule abs_safety) |
|
259 |
apply assumption+ |
|
260 |
apply (drule abs_safety) |
|
261 |
apply assumption+ |
|
262 |
apply (erule implements_trans) |
|
263 |
apply (erule implements_trans) |
|
264 |
apply assumption |
|
265 |
done |
|
266 |
||
267 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
268 |
lemma AbsRuleA2: "!!LC. [| inp(C)=inp(A); out(C)=out(A); |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
269 |
inp(Q)=inp(P); out(Q)=out(P); |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
270 |
is_live_abstraction h1 (C,LC) (A,LA); |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
271 |
live_implements (A,LA) (Q,LQ) ; |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
272 |
is_live_abstraction h2 (Q,LQ) (P,LP) |] |
19741 | 273 |
==> live_implements (C,LC) (P,LP)" |
274 |
apply (drule abs_liveness) |
|
275 |
apply assumption+ |
|
276 |
apply (drule abs_liveness) |
|
277 |
apply assumption+ |
|
278 |
apply (erule live_implements_trans) |
|
279 |
apply (erule live_implements_trans) |
|
280 |
apply assumption |
|
281 |
done |
|
282 |
||
283 |
||
284 |
declare split_paired_All [simp del] |
|
285 |
||
286 |
||
287 |
subsection "Localizing Temporal Strengthenings and Weakenings" |
|
288 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
289 |
lemma strength_AND: |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
290 |
"[| temp_strengthening P1 Q1 h; |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
291 |
temp_strengthening P2 Q2 h |] |
19741 | 292 |
==> temp_strengthening (P1 .& P2) (Q1 .& Q2) h" |
293 |
apply (unfold temp_strengthening_def) |
|
294 |
apply auto |
|
295 |
done |
|
296 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
297 |
lemma strength_OR: |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
298 |
"[| temp_strengthening P1 Q1 h; |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
299 |
temp_strengthening P2 Q2 h |] |
19741 | 300 |
==> temp_strengthening (P1 .| P2) (Q1 .| Q2) h" |
301 |
apply (unfold temp_strengthening_def) |
|
302 |
apply auto |
|
303 |
done |
|
304 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
305 |
lemma strength_NOT: |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
306 |
"[| temp_weakening P Q h |] |
19741 | 307 |
==> temp_strengthening (.~ P) (.~ Q) h" |
308 |
apply (unfold temp_strengthening_def) |
|
309 |
apply (simp add: temp_weakening_def2) |
|
310 |
apply auto |
|
311 |
done |
|
312 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
313 |
lemma strength_IMPLIES: |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
314 |
"[| temp_weakening P1 Q1 h; |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
315 |
temp_strengthening P2 Q2 h |] |
19741 | 316 |
==> temp_strengthening (P1 .--> P2) (Q1 .--> Q2) h" |
317 |
apply (unfold temp_strengthening_def) |
|
318 |
apply (simp add: temp_weakening_def2) |
|
319 |
done |
|
320 |
||
321 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
322 |
lemma weak_AND: |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
323 |
"[| temp_weakening P1 Q1 h; |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
324 |
temp_weakening P2 Q2 h |] |
19741 | 325 |
==> temp_weakening (P1 .& P2) (Q1 .& Q2) h" |
326 |
apply (simp add: temp_weakening_def2) |
|
327 |
done |
|
328 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
329 |
lemma weak_OR: |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
330 |
"[| temp_weakening P1 Q1 h; |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
331 |
temp_weakening P2 Q2 h |] |
19741 | 332 |
==> temp_weakening (P1 .| P2) (Q1 .| Q2) h" |
333 |
apply (simp add: temp_weakening_def2) |
|
334 |
done |
|
335 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
336 |
lemma weak_NOT: |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
337 |
"[| temp_strengthening P Q h |] |
19741 | 338 |
==> temp_weakening (.~ P) (.~ Q) h" |
339 |
apply (unfold temp_strengthening_def) |
|
340 |
apply (simp add: temp_weakening_def2) |
|
341 |
apply auto |
|
342 |
done |
|
343 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
344 |
lemma weak_IMPLIES: |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
345 |
"[| temp_strengthening P1 Q1 h; |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
346 |
temp_weakening P2 Q2 h |] |
19741 | 347 |
==> temp_weakening (P1 .--> P2) (Q1 .--> Q2) h" |
348 |
apply (unfold temp_strengthening_def) |
|
349 |
apply (simp add: temp_weakening_def2) |
|
350 |
done |
|
351 |
||
352 |
||
353 |
subsubsection {* Box *} |
|
354 |
||
355 |
(* FIX: should be same as nil_is_Conc2 when all nils are turned to right side !! *) |
|
356 |
lemma UU_is_Conc: "(UU = x @@ y) = (((x::'a Seq)= UU) | (x=nil & y=UU))" |
|
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
357 |
apply (tactic {* Seq_case_simp_tac @{context} "x" 1 *}) |
19741 | 358 |
done |
359 |
||
360 |
lemma ex2seqConc [rule_format]: |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
361 |
"Finite s1 --> |
19741 | 362 |
(! ex. (s~=nil & s~=UU & ex2seq ex = s1 @@ s) --> (? ex'. s = ex2seq ex'))" |
363 |
apply (rule impI) |
|
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
364 |
apply (tactic {* Seq_Finite_induct_tac @{context} 1 *}) |
19741 | 365 |
apply blast |
366 |
(* main case *) |
|
26359 | 367 |
apply clarify |
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
368 |
apply (tactic {* pair_tac @{context} "ex" 1 *}) |
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
369 |
apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *}) |
19741 | 370 |
(* UU case *) |
371 |
apply (simp add: nil_is_Conc) |
|
372 |
(* nil case *) |
|
373 |
apply (simp add: nil_is_Conc) |
|
374 |
(* cons case *) |
|
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
375 |
apply (tactic {* pair_tac @{context} "aa" 1 *}) |
19741 | 376 |
apply auto |
377 |
done |
|
378 |
||
379 |
(* important property of ex2seq: can be shiftet, as defined "pointwise" *) |
|
380 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
381 |
lemma ex2seq_tsuffix: |
19741 | 382 |
"tsuffix s (ex2seq ex) ==> ? ex'. s = (ex2seq ex')" |
383 |
apply (unfold tsuffix_def suffix_def) |
|
384 |
apply auto |
|
385 |
apply (drule ex2seqConc) |
|
386 |
apply auto |
|
387 |
done |
|
388 |
||
389 |
||
390 |
(* FIX: NAch Sequence.ML bringen *) |
|
391 |
||
392 |
lemma Mapnil: "(Map f$s = nil) = (s=nil)" |
|
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
393 |
apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *}) |
19741 | 394 |
done |
395 |
||
396 |
lemma MapUU: "(Map f$s = UU) = (s=UU)" |
|
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
397 |
apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *}) |
19741 | 398 |
done |
399 |
||
400 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
401 |
(* important property of cex_absSeq: As it is a 1to1 correspondence, |
19741 | 402 |
properties carry over *) |
403 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
404 |
lemma cex_absSeq_tsuffix: |
19741 | 405 |
"tsuffix s t ==> tsuffix (cex_absSeq h s) (cex_absSeq h t)" |
406 |
apply (unfold tsuffix_def suffix_def cex_absSeq_def) |
|
407 |
apply auto |
|
408 |
apply (simp add: Mapnil) |
|
409 |
apply (simp add: MapUU) |
|
410 |
apply (rule_tac x = "Map (% (s,a,t) . (h s,a, h t))$s1" in exI) |
|
411 |
apply (simp add: Map2Finite MapConc) |
|
412 |
done |
|
413 |
||
414 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
415 |
lemma strength_Box: |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
416 |
"[| temp_strengthening P Q h |] |
19741 | 417 |
==> temp_strengthening ([] P) ([] Q) h" |
418 |
apply (unfold temp_strengthening_def state_strengthening_def temp_sat_def satisfies_def Box_def) |
|
26359 | 419 |
apply clarify |
19741 | 420 |
apply (frule ex2seq_tsuffix) |
26359 | 421 |
apply clarify |
19741 | 422 |
apply (drule_tac h = "h" in cex_absSeq_tsuffix) |
423 |
apply (simp add: ex2seq_abs_cex) |
|
424 |
done |
|
425 |
||
426 |
||
427 |
subsubsection {* Init *} |
|
428 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
429 |
lemma strength_Init: |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
430 |
"[| state_strengthening P Q h |] |
19741 | 431 |
==> temp_strengthening (Init P) (Init Q) h" |
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
432 |
apply (unfold temp_strengthening_def state_strengthening_def |
19741 | 433 |
temp_sat_def satisfies_def Init_def unlift_def) |
26359 | 434 |
apply auto |
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
435 |
apply (tactic {* pair_tac @{context} "ex" 1 *}) |
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
436 |
apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *}) |
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
437 |
apply (tactic {* pair_tac @{context} "a" 1 *}) |
19741 | 438 |
done |
439 |
||
440 |
||
441 |
subsubsection {* Next *} |
|
442 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
443 |
lemma TL_ex2seq_UU: |
19741 | 444 |
"(TL$(ex2seq (cex_abs h ex))=UU) = (TL$(ex2seq ex)=UU)" |
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
445 |
apply (tactic {* pair_tac @{context} "ex" 1 *}) |
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
446 |
apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *}) |
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
447 |
apply (tactic {* pair_tac @{context} "a" 1 *}) |
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
448 |
apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *}) |
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
449 |
apply (tactic {* pair_tac @{context} "a" 1 *}) |
19741 | 450 |
done |
451 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
452 |
lemma TL_ex2seq_nil: |
19741 | 453 |
"(TL$(ex2seq (cex_abs h ex))=nil) = (TL$(ex2seq ex)=nil)" |
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
454 |
apply (tactic {* pair_tac @{context} "ex" 1 *}) |
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
455 |
apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *}) |
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
456 |
apply (tactic {* pair_tac @{context} "a" 1 *}) |
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
457 |
apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *}) |
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
458 |
apply (tactic {* pair_tac @{context} "a" 1 *}) |
19741 | 459 |
done |
460 |
||
461 |
(* FIX: put to Sequence Lemmas *) |
|
462 |
lemma MapTL: "Map f$(TL$s) = TL$(Map f$s)" |
|
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
463 |
apply (tactic {* Seq_induct_tac @{context} "s" [] 1 *}) |
19741 | 464 |
done |
465 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
466 |
(* important property of cex_absSeq: As it is a 1to1 correspondence, |
19741 | 467 |
properties carry over *) |
468 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
469 |
lemma cex_absSeq_TL: |
19741 | 470 |
"cex_absSeq h (TL$s) = (TL$(cex_absSeq h s))" |
471 |
apply (unfold cex_absSeq_def) |
|
472 |
apply (simp add: MapTL) |
|
473 |
done |
|
474 |
||
475 |
(* important property of ex2seq: can be shiftet, as defined "pointwise" *) |
|
476 |
||
477 |
lemma TLex2seq: "[| (snd ex)~=UU ; (snd ex)~=nil |] ==> (? ex'. TL$(ex2seq ex) = ex2seq ex')" |
|
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
478 |
apply (tactic {* pair_tac @{context} "ex" 1 *}) |
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
479 |
apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *}) |
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
480 |
apply (tactic {* pair_tac @{context} "a" 1 *}) |
19741 | 481 |
apply auto |
482 |
done |
|
483 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
484 |
|
19741 | 485 |
lemma ex2seqnilTL: "(TL$(ex2seq ex)~=nil) = ((snd ex)~=nil & (snd ex)~=UU)" |
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
486 |
apply (tactic {* pair_tac @{context} "ex" 1 *}) |
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
487 |
apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *}) |
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
488 |
apply (tactic {* pair_tac @{context} "a" 1 *}) |
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
489 |
apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *}) |
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
490 |
apply (tactic {* pair_tac @{context} "a" 1 *}) |
19741 | 491 |
done |
492 |
||
493 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
494 |
lemma strength_Next: |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
495 |
"[| temp_strengthening P Q h |] |
19741 | 496 |
==> temp_strengthening (Next P) (Next Q) h" |
497 |
apply (unfold temp_strengthening_def state_strengthening_def temp_sat_def satisfies_def Next_def) |
|
498 |
apply simp |
|
26359 | 499 |
apply auto |
19741 | 500 |
apply (simp add: TL_ex2seq_nil TL_ex2seq_UU) |
501 |
apply (simp add: TL_ex2seq_nil TL_ex2seq_UU) |
|
502 |
apply (simp add: TL_ex2seq_nil TL_ex2seq_UU) |
|
503 |
apply (simp add: TL_ex2seq_nil TL_ex2seq_UU) |
|
504 |
(* cons case *) |
|
505 |
apply (simp add: TL_ex2seq_nil TL_ex2seq_UU ex2seq_abs_cex cex_absSeq_TL [symmetric] ex2seqnilTL) |
|
506 |
apply (erule conjE) |
|
507 |
apply (drule TLex2seq) |
|
508 |
apply assumption |
|
509 |
apply auto |
|
510 |
done |
|
511 |
||
512 |
||
513 |
text {* Localizing Temporal Weakenings - 2 *} |
|
514 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
515 |
lemma weak_Init: |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
516 |
"[| state_weakening P Q h |] |
19741 | 517 |
==> temp_weakening (Init P) (Init Q) h" |
518 |
apply (simp add: temp_weakening_def2 state_weakening_def2 |
|
519 |
temp_sat_def satisfies_def Init_def unlift_def) |
|
26359 | 520 |
apply auto |
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
521 |
apply (tactic {* pair_tac @{context} "ex" 1 *}) |
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
522 |
apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *}) |
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
523 |
apply (tactic {* pair_tac @{context} "a" 1 *}) |
19741 | 524 |
done |
525 |
||
526 |
||
527 |
text {* Localizing Temproal Strengthenings - 3 *} |
|
528 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
529 |
lemma strength_Diamond: |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
530 |
"[| temp_strengthening P Q h |] |
19741 | 531 |
==> temp_strengthening (<> P) (<> Q) h" |
532 |
apply (unfold Diamond_def) |
|
533 |
apply (rule strength_NOT) |
|
534 |
apply (rule weak_Box) |
|
535 |
apply (erule weak_NOT) |
|
536 |
done |
|
537 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
538 |
lemma strength_Leadsto: |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
539 |
"[| temp_weakening P1 P2 h; |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
540 |
temp_strengthening Q1 Q2 h |] |
19741 | 541 |
==> temp_strengthening (P1 ~> Q1) (P2 ~> Q2) h" |
542 |
apply (unfold Leadsto_def) |
|
543 |
apply (rule strength_Box) |
|
544 |
apply (erule strength_IMPLIES) |
|
545 |
apply (erule strength_Diamond) |
|
546 |
done |
|
547 |
||
548 |
||
549 |
text {* Localizing Temporal Weakenings - 3 *} |
|
550 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
551 |
lemma weak_Diamond: |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
552 |
"[| temp_weakening P Q h |] |
19741 | 553 |
==> temp_weakening (<> P) (<> Q) h" |
554 |
apply (unfold Diamond_def) |
|
555 |
apply (rule weak_NOT) |
|
556 |
apply (rule strength_Box) |
|
557 |
apply (erule strength_NOT) |
|
558 |
done |
|
559 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
560 |
lemma weak_Leadsto: |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
561 |
"[| temp_strengthening P1 P2 h; |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
562 |
temp_weakening Q1 Q2 h |] |
19741 | 563 |
==> temp_weakening (P1 ~> Q1) (P2 ~> Q2) h" |
564 |
apply (unfold Leadsto_def) |
|
565 |
apply (rule weak_Box) |
|
566 |
apply (erule weak_IMPLIES) |
|
567 |
apply (erule weak_Diamond) |
|
568 |
done |
|
569 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
570 |
lemma weak_WF: |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
571 |
" !!A. [| !! s. Enabled A acts (h s) ==> Enabled C acts s|] |
19741 | 572 |
==> temp_weakening (WF A acts) (WF C acts) h" |
573 |
apply (unfold WF_def) |
|
574 |
apply (rule weak_IMPLIES) |
|
575 |
apply (rule strength_Diamond) |
|
576 |
apply (rule strength_Box) |
|
577 |
apply (rule strength_Init) |
|
578 |
apply (rule_tac [2] weak_Box) |
|
579 |
apply (rule_tac [2] weak_Diamond) |
|
580 |
apply (rule_tac [2] weak_Init) |
|
581 |
apply (auto simp add: state_weakening_def state_strengthening_def |
|
582 |
xt2_def plift_def option_lift_def NOT_def) |
|
583 |
done |
|
584 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
585 |
lemma weak_SF: |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
586 |
" !!A. [| !! s. Enabled A acts (h s) ==> Enabled C acts s|] |
19741 | 587 |
==> temp_weakening (SF A acts) (SF C acts) h" |
588 |
apply (unfold SF_def) |
|
589 |
apply (rule weak_IMPLIES) |
|
590 |
apply (rule strength_Box) |
|
591 |
apply (rule strength_Diamond) |
|
592 |
apply (rule strength_Init) |
|
593 |
apply (rule_tac [2] weak_Box) |
|
594 |
apply (rule_tac [2] weak_Diamond) |
|
595 |
apply (rule_tac [2] weak_Init) |
|
596 |
apply (auto simp add: state_weakening_def state_strengthening_def |
|
597 |
xt2_def plift_def option_lift_def NOT_def) |
|
598 |
done |
|
599 |
||
600 |
||
601 |
lemmas weak_strength_lemmas = |
|
602 |
weak_OR weak_AND weak_NOT weak_IMPLIES weak_Box weak_Next weak_Init |
|
603 |
weak_Diamond weak_Leadsto strength_OR strength_AND strength_NOT |
|
604 |
strength_IMPLIES strength_Box strength_Next strength_Init |
|
605 |
strength_Diamond strength_Leadsto weak_WF weak_SF |
|
606 |
||
607 |
ML {* |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
608 |
fun abstraction_tac i = |
19741 | 609 |
SELECT_GOAL (CLASIMPSET (fn (cs, ss) => |
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
610 |
auto_tac (cs addSIs @{thms weak_strength_lemmas}, |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
23560
diff
changeset
|
611 |
ss addsimps [@{thm state_strengthening_def}, @{thm state_weakening_def}]))) i |
19741 | 612 |
*} |
17233 | 613 |
|
23560 | 614 |
use "ioa_package.ML" |
615 |
||
17233 | 616 |
end |