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