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