author | wenzelm |
Tue, 07 Aug 2007 23:24:10 +0200 | |
changeset 24180 | 9f818139951b |
parent 21624 | 6f79647cf536 |
child 27104 | 791607529f6d |
permissions | -rw-r--r-- |
17309 | 1 |
(* |
2 |
File: TLA/Action.thy |
|
3 |
ID: $Id$ |
|
3807 | 4 |
Author: Stephan Merz |
6255 | 5 |
Copyright: 1998 University of Munich |
21624 | 6 |
*) |
3807 | 7 |
|
21624 | 8 |
header {* The action level of TLA as an Isabelle theory *} |
3807 | 9 |
|
17309 | 10 |
theory Action |
11 |
imports Stfun |
|
12 |
begin |
|
13 |
||
3807 | 14 |
|
6255 | 15 |
(** abstract syntax **) |
16 |
||
3807 | 17 |
types |
6255 | 18 |
'a trfun = "(state * state) => 'a" |
17309 | 19 |
action = "bool trfun" |
6255 | 20 |
|
21 |
instance |
|
17309 | 22 |
"*" :: (world, world) world .. |
3807 | 23 |
|
24 |
consts |
|
6255 | 25 |
(** abstract syntax **) |
17309 | 26 |
before :: "'a stfun => 'a trfun" |
27 |
after :: "'a stfun => 'a trfun" |
|
28 |
unch :: "'a stfun => action" |
|
6255 | 29 |
|
17309 | 30 |
SqAct :: "[action, 'a stfun] => action" |
31 |
AnAct :: "[action, 'a stfun] => action" |
|
32 |
enabled :: "action => stpred" |
|
6255 | 33 |
|
34 |
(** concrete syntax **) |
|
35 |
||
36 |
syntax |
|
37 |
(* Syntax for writing action expressions in arbitrary contexts *) |
|
17309 | 38 |
"ACT" :: "lift => 'a" ("(ACT _)") |
3807 | 39 |
|
17309 | 40 |
"_before" :: "lift => lift" ("($_)" [100] 99) |
41 |
"_after" :: "lift => lift" ("(_$)" [100] 99) |
|
42 |
"_unchanged" :: "lift => lift" ("(unchanged _)" [100] 99) |
|
6255 | 43 |
|
44 |
(*** Priming: same as "after" ***) |
|
17309 | 45 |
"_prime" :: "lift => lift" ("(_`)" [100] 99) |
6255 | 46 |
|
17309 | 47 |
"_SqAct" :: "[lift, lift] => lift" ("([_]'_(_))" [0,1000] 99) |
48 |
"_AnAct" :: "[lift, lift] => lift" ("(<_>'_(_))" [0,1000] 99) |
|
49 |
"_Enabled" :: "lift => lift" ("(Enabled _)" [100] 100) |
|
3807 | 50 |
|
6255 | 51 |
translations |
52 |
"ACT A" => "(A::state*state => _)" |
|
53 |
"_before" == "before" |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
54 |
"_after" == "after" |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
55 |
"_prime" => "_after" |
6255 | 56 |
"_unchanged" == "unch" |
57 |
"_SqAct" == "SqAct" |
|
58 |
"_AnAct" == "AnAct" |
|
59 |
"_Enabled" == "enabled" |
|
60 |
"w |= [A]_v" <= "_SqAct A v w" |
|
61 |
"w |= <A>_v" <= "_AnAct A v w" |
|
62 |
"s |= Enabled A" <= "_Enabled A s" |
|
63 |
"w |= unchanged f" <= "_unchanged f w" |
|
3807 | 64 |
|
17309 | 65 |
axioms |
66 |
unl_before: "(ACT $v) (s,t) == v s" |
|
67 |
unl_after: "(ACT v$) (s,t) == v t" |
|
3807 | 68 |
|
17309 | 69 |
unchanged_def: "(s,t) |= unchanged v == (v t = v s)" |
70 |
square_def: "ACT [A]_v == ACT (A | unchanged v)" |
|
71 |
angle_def: "ACT <A>_v == ACT (A & ~ unchanged v)" |
|
3807 | 72 |
|
17309 | 73 |
enabled_def: "s |= Enabled A == EX u. (s,u) |= A" |
74 |
||
21624 | 75 |
|
76 |
(* The following assertion specializes "intI" for any world type |
|
77 |
which is a pair, not just for "state * state". |
|
78 |
*) |
|
79 |
||
80 |
lemma actionI [intro!]: |
|
81 |
assumes "!!s t. (s,t) |= A" |
|
82 |
shows "|- A" |
|
83 |
apply (rule assms intI prod_induct)+ |
|
84 |
done |
|
85 |
||
86 |
lemma actionD [dest]: "|- A ==> (s,t) |= A" |
|
87 |
apply (erule intD) |
|
88 |
done |
|
89 |
||
90 |
lemma pr_rews [int_rewrite]: |
|
91 |
"|- (#c)` = #c" |
|
92 |
"!!f. |- f<x>` = f<x` >" |
|
93 |
"!!f. |- f<x,y>` = f<x`,y` >" |
|
94 |
"!!f. |- f<x,y,z>` = f<x`,y`,z` >" |
|
95 |
"|- (! x. P x)` = (! x. (P x)`)" |
|
96 |
"|- (? x. P x)` = (? x. (P x)`)" |
|
97 |
by (rule actionI, unfold unl_after intensional_rews, rule refl)+ |
|
98 |
||
99 |
||
100 |
lemmas act_rews [simp] = unl_before unl_after unchanged_def pr_rews |
|
101 |
||
102 |
lemmas action_rews = act_rews intensional_rews |
|
103 |
||
104 |
||
105 |
(* ================ Functions to "unlift" action theorems into HOL rules ================ *) |
|
106 |
||
107 |
ML {* |
|
108 |
(* The following functions are specialized versions of the corresponding |
|
109 |
functions defined in Intensional.ML in that they introduce a |
|
110 |
"world" parameter of the form (s,t) and apply additional rewrites. |
|
111 |
*) |
|
112 |
||
113 |
fun action_unlift th = |
|
24180 | 114 |
(rewrite_rule @{thms action_rews} (th RS @{thm actionD})) |
21624 | 115 |
handle THM _ => int_unlift th; |
116 |
||
117 |
(* Turn |- A = B into meta-level rewrite rule A == B *) |
|
118 |
val action_rewrite = int_rewrite |
|
119 |
||
120 |
fun action_use th = |
|
121 |
case (concl_of th) of |
|
122 |
Const _ $ (Const ("Intensional.Valid", _) $ _) => |
|
123 |
(flatten (action_unlift th) handle THM _ => th) |
|
124 |
| _ => th; |
|
125 |
*} |
|
126 |
||
127 |
setup {* |
|
128 |
Attrib.add_attributes [ |
|
129 |
("action_unlift", Attrib.no_args (Thm.rule_attribute (K action_unlift)), ""), |
|
130 |
("action_rewrite", Attrib.no_args (Thm.rule_attribute (K action_rewrite)), ""), |
|
131 |
("action_use", Attrib.no_args (Thm.rule_attribute (K action_use)), "")] |
|
132 |
*} |
|
133 |
||
134 |
||
135 |
(* =========================== square / angle brackets =========================== *) |
|
136 |
||
137 |
lemma idle_squareI: "(s,t) |= unchanged v ==> (s,t) |= [A]_v" |
|
138 |
by (simp add: square_def) |
|
139 |
||
140 |
lemma busy_squareI: "(s,t) |= A ==> (s,t) |= [A]_v" |
|
141 |
by (simp add: square_def) |
|
142 |
||
143 |
lemma squareE [elim]: |
|
144 |
"[| (s,t) |= [A]_v; A (s,t) ==> B (s,t); v t = v s ==> B (s,t) |] ==> B (s,t)" |
|
145 |
apply (unfold square_def action_rews) |
|
146 |
apply (erule disjE) |
|
147 |
apply simp_all |
|
148 |
done |
|
149 |
||
150 |
lemma squareCI [intro]: "[| v t ~= v s ==> A (s,t) |] ==> (s,t) |= [A]_v" |
|
151 |
apply (unfold square_def action_rews) |
|
152 |
apply (rule disjCI) |
|
153 |
apply (erule (1) meta_mp) |
|
154 |
done |
|
155 |
||
156 |
lemma angleI [intro]: "!!s t. [| A (s,t); v t ~= v s |] ==> (s,t) |= <A>_v" |
|
157 |
by (simp add: angle_def) |
|
158 |
||
159 |
lemma angleE [elim]: "[| (s,t) |= <A>_v; [| A (s,t); v t ~= v s |] ==> R |] ==> R" |
|
160 |
apply (unfold angle_def action_rews) |
|
161 |
apply (erule conjE) |
|
162 |
apply simp |
|
163 |
done |
|
164 |
||
165 |
lemma square_simulation: |
|
166 |
"!!f. [| |- unchanged f & ~B --> unchanged g; |
|
167 |
|- A & ~unchanged g --> B |
|
168 |
|] ==> |- [A]_f --> [B]_g" |
|
169 |
apply clarsimp |
|
170 |
apply (erule squareE) |
|
171 |
apply (auto simp add: square_def) |
|
172 |
done |
|
173 |
||
174 |
lemma not_square: "|- (~ [A]_v) = <~A>_v" |
|
175 |
by (auto simp: square_def angle_def) |
|
176 |
||
177 |
lemma not_angle: "|- (~ <A>_v) = [~A]_v" |
|
178 |
by (auto simp: square_def angle_def) |
|
179 |
||
180 |
||
181 |
(* ============================== Facts about ENABLED ============================== *) |
|
182 |
||
183 |
lemma enabledI: "|- A --> $Enabled A" |
|
184 |
by (auto simp add: enabled_def) |
|
185 |
||
186 |
lemma enabledE: "[| s |= Enabled A; !!u. A (s,u) ==> Q |] ==> Q" |
|
187 |
apply (unfold enabled_def) |
|
188 |
apply (erule exE) |
|
189 |
apply simp |
|
190 |
done |
|
191 |
||
192 |
lemma notEnabledD: "|- ~$Enabled G --> ~ G" |
|
193 |
by (auto simp add: enabled_def) |
|
194 |
||
195 |
(* Monotonicity *) |
|
196 |
lemma enabled_mono: |
|
197 |
assumes min: "s |= Enabled F" |
|
198 |
and maj: "|- F --> G" |
|
199 |
shows "s |= Enabled G" |
|
200 |
apply (rule min [THEN enabledE]) |
|
201 |
apply (rule enabledI [action_use]) |
|
202 |
apply (erule maj [action_use]) |
|
203 |
done |
|
204 |
||
205 |
(* stronger variant *) |
|
206 |
lemma enabled_mono2: |
|
207 |
assumes min: "s |= Enabled F" |
|
208 |
and maj: "!!t. F (s,t) ==> G (s,t)" |
|
209 |
shows "s |= Enabled G" |
|
210 |
apply (rule min [THEN enabledE]) |
|
211 |
apply (rule enabledI [action_use]) |
|
212 |
apply (erule maj) |
|
213 |
done |
|
214 |
||
215 |
lemma enabled_disj1: "|- Enabled F --> Enabled (F | G)" |
|
216 |
by (auto elim!: enabled_mono) |
|
217 |
||
218 |
lemma enabled_disj2: "|- Enabled G --> Enabled (F | G)" |
|
219 |
by (auto elim!: enabled_mono) |
|
220 |
||
221 |
lemma enabled_conj1: "|- Enabled (F & G) --> Enabled F" |
|
222 |
by (auto elim!: enabled_mono) |
|
223 |
||
224 |
lemma enabled_conj2: "|- Enabled (F & G) --> Enabled G" |
|
225 |
by (auto elim!: enabled_mono) |
|
226 |
||
227 |
lemma enabled_conjE: |
|
228 |
"[| s |= Enabled (F & G); [| s |= Enabled F; s |= Enabled G |] ==> Q |] ==> Q" |
|
229 |
apply (frule enabled_conj1 [action_use]) |
|
230 |
apply (drule enabled_conj2 [action_use]) |
|
231 |
apply simp |
|
232 |
done |
|
233 |
||
234 |
lemma enabled_disjD: "|- Enabled (F | G) --> Enabled F | Enabled G" |
|
235 |
by (auto simp add: enabled_def) |
|
236 |
||
237 |
lemma enabled_disj: "|- Enabled (F | G) = (Enabled F | Enabled G)" |
|
238 |
apply clarsimp |
|
239 |
apply (rule iffI) |
|
240 |
apply (erule enabled_disjD [action_use]) |
|
241 |
apply (erule disjE enabled_disj1 [action_use] enabled_disj2 [action_use])+ |
|
242 |
done |
|
243 |
||
244 |
lemma enabled_ex: "|- Enabled (EX x. F x) = (EX x. Enabled (F x))" |
|
245 |
by (force simp add: enabled_def) |
|
246 |
||
247 |
||
248 |
(* A rule that combines enabledI and baseE, but generates fewer instantiations *) |
|
249 |
lemma base_enabled: |
|
250 |
"[| basevars vs; EX c. ! u. vs u = c --> A(s,u) |] ==> s |= Enabled A" |
|
251 |
apply (erule exE) |
|
252 |
apply (erule baseE) |
|
253 |
apply (rule enabledI [action_use]) |
|
254 |
apply (erule allE) |
|
255 |
apply (erule mp) |
|
256 |
apply assumption |
|
257 |
done |
|
258 |
||
259 |
(* ======================= action_simp_tac ============================== *) |
|
260 |
||
261 |
ML {* |
|
262 |
(* A dumb simplification-based tactic with just a little first-order logic: |
|
263 |
should plug in only "very safe" rules that can be applied blindly. |
|
264 |
Note that it applies whatever simplifications are currently active. |
|
265 |
*) |
|
266 |
fun action_simp_tac ss intros elims = |
|
267 |
asm_full_simp_tac |
|
268 |
(ss setloop ((resolve_tac ((map action_use intros) |
|
24180 | 269 |
@ [refl,impI,conjI,@{thm actionI},@{thm intI},allI])) |
21624 | 270 |
ORELSE' (eresolve_tac ((map action_use elims) |
271 |
@ [conjE,disjE,exE])))); |
|
272 |
*} |
|
273 |
||
274 |
(* ---------------- enabled_tac: tactic to prove (Enabled A) -------------------- *) |
|
275 |
||
276 |
ML {* |
|
277 |
(* "Enabled A" can be proven as follows: |
|
278 |
- Assume that we know which state variables are "base variables" |
|
279 |
this should be expressed by a theorem of the form "basevars (x,y,z,...)". |
|
280 |
- Resolve this theorem with baseE to introduce a constant for the value of the |
|
281 |
variables in the successor state, and resolve the goal with the result. |
|
282 |
- Resolve with enabledI and do some rewriting. |
|
283 |
- Solve for the unknowns using standard HOL reasoning. |
|
284 |
The following tactic combines these steps except the final one. |
|
285 |
*) |
|
286 |
||
24180 | 287 |
fun enabled_tac (cs, ss) base_vars = |
288 |
clarsimp_tac (cs addSIs [base_vars RS @{thm base_enabled}], ss); |
|
21624 | 289 |
*} |
290 |
||
291 |
(* Example *) |
|
292 |
||
293 |
lemma |
|
294 |
assumes "basevars (x,y,z)" |
|
295 |
shows "|- x --> Enabled ($x & (y$ = #False))" |
|
24180 | 296 |
apply (tactic {* enabled_tac @{clasimpset} @{thm assms} 1 *}) |
21624 | 297 |
apply auto |
298 |
done |
|
299 |
||
300 |
end |