author | wenzelm |
Sun, 20 Mar 2011 23:07:06 +0100 | |
changeset 42018 | 878f33040280 |
parent 37678 | 0040bafffdef |
child 42785 | 15ec9b3c14cc |
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 |
|
17309 | 61 |
axioms |
62 |
unl_before: "(ACT $v) (s,t) == v s" |
|
63 |
unl_after: "(ACT v$) (s,t) == v t" |
|
3807 | 64 |
|
17309 | 65 |
unchanged_def: "(s,t) |= unchanged v == (v t = v s)" |
66 |
square_def: "ACT [A]_v == ACT (A | unchanged v)" |
|
67 |
angle_def: "ACT <A>_v == ACT (A & ~ unchanged v)" |
|
3807 | 68 |
|
17309 | 69 |
enabled_def: "s |= Enabled A == EX u. (s,u) |= A" |
70 |
||
21624 | 71 |
|
72 |
(* The following assertion specializes "intI" for any world type |
|
73 |
which is a pair, not just for "state * state". |
|
74 |
*) |
|
75 |
||
76 |
lemma actionI [intro!]: |
|
77 |
assumes "!!s t. (s,t) |= A" |
|
78 |
shows "|- A" |
|
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
24180
diff
changeset
|
79 |
apply (rule assms intI prod.induct)+ |
21624 | 80 |
done |
81 |
||
82 |
lemma actionD [dest]: "|- A ==> (s,t) |= A" |
|
83 |
apply (erule intD) |
|
84 |
done |
|
85 |
||
86 |
lemma pr_rews [int_rewrite]: |
|
87 |
"|- (#c)` = #c" |
|
88 |
"!!f. |- f<x>` = f<x` >" |
|
89 |
"!!f. |- f<x,y>` = f<x`,y` >" |
|
90 |
"!!f. |- f<x,y,z>` = f<x`,y`,z` >" |
|
91 |
"|- (! x. P x)` = (! x. (P x)`)" |
|
92 |
"|- (? x. P x)` = (? x. (P x)`)" |
|
93 |
by (rule actionI, unfold unl_after intensional_rews, rule refl)+ |
|
94 |
||
95 |
||
96 |
lemmas act_rews [simp] = unl_before unl_after unchanged_def pr_rews |
|
97 |
||
98 |
lemmas action_rews = act_rews intensional_rews |
|
99 |
||
100 |
||
101 |
(* ================ Functions to "unlift" action theorems into HOL rules ================ *) |
|
102 |
||
103 |
ML {* |
|
104 |
(* The following functions are specialized versions of the corresponding |
|
105 |
functions defined in Intensional.ML in that they introduce a |
|
106 |
"world" parameter of the form (s,t) and apply additional rewrites. |
|
107 |
*) |
|
108 |
||
109 |
fun action_unlift th = |
|
24180 | 110 |
(rewrite_rule @{thms action_rews} (th RS @{thm actionD})) |
21624 | 111 |
handle THM _ => int_unlift th; |
112 |
||
113 |
(* Turn |- A = B into meta-level rewrite rule A == B *) |
|
114 |
val action_rewrite = int_rewrite |
|
115 |
||
116 |
fun action_use th = |
|
117 |
case (concl_of th) of |
|
118 |
Const _ $ (Const ("Intensional.Valid", _) $ _) => |
|
119 |
(flatten (action_unlift th) handle THM _ => th) |
|
120 |
| _ => th; |
|
121 |
*} |
|
122 |
||
30528 | 123 |
attribute_setup action_unlift = {* Scan.succeed (Thm.rule_attribute (K action_unlift)) *} "" |
124 |
attribute_setup action_rewrite = {* Scan.succeed (Thm.rule_attribute (K action_rewrite)) *} "" |
|
125 |
attribute_setup action_use = {* Scan.succeed (Thm.rule_attribute (K action_use)) *} "" |
|
21624 | 126 |
|
127 |
||
128 |
(* =========================== square / angle brackets =========================== *) |
|
129 |
||
130 |
lemma idle_squareI: "(s,t) |= unchanged v ==> (s,t) |= [A]_v" |
|
131 |
by (simp add: square_def) |
|
132 |
||
133 |
lemma busy_squareI: "(s,t) |= A ==> (s,t) |= [A]_v" |
|
134 |
by (simp add: square_def) |
|
135 |
||
136 |
lemma squareE [elim]: |
|
137 |
"[| (s,t) |= [A]_v; A (s,t) ==> B (s,t); v t = v s ==> B (s,t) |] ==> B (s,t)" |
|
138 |
apply (unfold square_def action_rews) |
|
139 |
apply (erule disjE) |
|
140 |
apply simp_all |
|
141 |
done |
|
142 |
||
143 |
lemma squareCI [intro]: "[| v t ~= v s ==> A (s,t) |] ==> (s,t) |= [A]_v" |
|
144 |
apply (unfold square_def action_rews) |
|
145 |
apply (rule disjCI) |
|
146 |
apply (erule (1) meta_mp) |
|
147 |
done |
|
148 |
||
149 |
lemma angleI [intro]: "!!s t. [| A (s,t); v t ~= v s |] ==> (s,t) |= <A>_v" |
|
150 |
by (simp add: angle_def) |
|
151 |
||
152 |
lemma angleE [elim]: "[| (s,t) |= <A>_v; [| A (s,t); v t ~= v s |] ==> R |] ==> R" |
|
153 |
apply (unfold angle_def action_rews) |
|
154 |
apply (erule conjE) |
|
155 |
apply simp |
|
156 |
done |
|
157 |
||
158 |
lemma square_simulation: |
|
159 |
"!!f. [| |- unchanged f & ~B --> unchanged g; |
|
160 |
|- A & ~unchanged g --> B |
|
161 |
|] ==> |- [A]_f --> [B]_g" |
|
162 |
apply clarsimp |
|
163 |
apply (erule squareE) |
|
164 |
apply (auto simp add: square_def) |
|
165 |
done |
|
166 |
||
167 |
lemma not_square: "|- (~ [A]_v) = <~A>_v" |
|
168 |
by (auto simp: square_def angle_def) |
|
169 |
||
170 |
lemma not_angle: "|- (~ <A>_v) = [~A]_v" |
|
171 |
by (auto simp: square_def angle_def) |
|
172 |
||
173 |
||
174 |
(* ============================== Facts about ENABLED ============================== *) |
|
175 |
||
176 |
lemma enabledI: "|- A --> $Enabled A" |
|
177 |
by (auto simp add: enabled_def) |
|
178 |
||
179 |
lemma enabledE: "[| s |= Enabled A; !!u. A (s,u) ==> Q |] ==> Q" |
|
180 |
apply (unfold enabled_def) |
|
181 |
apply (erule exE) |
|
182 |
apply simp |
|
183 |
done |
|
184 |
||
185 |
lemma notEnabledD: "|- ~$Enabled G --> ~ G" |
|
186 |
by (auto simp add: enabled_def) |
|
187 |
||
188 |
(* Monotonicity *) |
|
189 |
lemma enabled_mono: |
|
190 |
assumes min: "s |= Enabled F" |
|
191 |
and maj: "|- F --> G" |
|
192 |
shows "s |= Enabled G" |
|
193 |
apply (rule min [THEN enabledE]) |
|
194 |
apply (rule enabledI [action_use]) |
|
195 |
apply (erule maj [action_use]) |
|
196 |
done |
|
197 |
||
198 |
(* stronger variant *) |
|
199 |
lemma enabled_mono2: |
|
200 |
assumes min: "s |= Enabled F" |
|
201 |
and maj: "!!t. F (s,t) ==> G (s,t)" |
|
202 |
shows "s |= Enabled G" |
|
203 |
apply (rule min [THEN enabledE]) |
|
204 |
apply (rule enabledI [action_use]) |
|
205 |
apply (erule maj) |
|
206 |
done |
|
207 |
||
208 |
lemma enabled_disj1: "|- Enabled F --> Enabled (F | G)" |
|
209 |
by (auto elim!: enabled_mono) |
|
210 |
||
211 |
lemma enabled_disj2: "|- Enabled G --> Enabled (F | G)" |
|
212 |
by (auto elim!: enabled_mono) |
|
213 |
||
214 |
lemma enabled_conj1: "|- Enabled (F & G) --> Enabled F" |
|
215 |
by (auto elim!: enabled_mono) |
|
216 |
||
217 |
lemma enabled_conj2: "|- Enabled (F & G) --> Enabled G" |
|
218 |
by (auto elim!: enabled_mono) |
|
219 |
||
220 |
lemma enabled_conjE: |
|
221 |
"[| s |= Enabled (F & G); [| s |= Enabled F; s |= Enabled G |] ==> Q |] ==> Q" |
|
222 |
apply (frule enabled_conj1 [action_use]) |
|
223 |
apply (drule enabled_conj2 [action_use]) |
|
224 |
apply simp |
|
225 |
done |
|
226 |
||
227 |
lemma enabled_disjD: "|- Enabled (F | G) --> Enabled F | Enabled G" |
|
228 |
by (auto simp add: enabled_def) |
|
229 |
||
230 |
lemma enabled_disj: "|- Enabled (F | G) = (Enabled F | Enabled G)" |
|
231 |
apply clarsimp |
|
232 |
apply (rule iffI) |
|
233 |
apply (erule enabled_disjD [action_use]) |
|
234 |
apply (erule disjE enabled_disj1 [action_use] enabled_disj2 [action_use])+ |
|
235 |
done |
|
236 |
||
237 |
lemma enabled_ex: "|- Enabled (EX x. F x) = (EX x. Enabled (F x))" |
|
238 |
by (force simp add: enabled_def) |
|
239 |
||
240 |
||
241 |
(* A rule that combines enabledI and baseE, but generates fewer instantiations *) |
|
242 |
lemma base_enabled: |
|
243 |
"[| basevars vs; EX c. ! u. vs u = c --> A(s,u) |] ==> s |= Enabled A" |
|
244 |
apply (erule exE) |
|
245 |
apply (erule baseE) |
|
246 |
apply (rule enabledI [action_use]) |
|
247 |
apply (erule allE) |
|
248 |
apply (erule mp) |
|
249 |
apply assumption |
|
250 |
done |
|
251 |
||
252 |
(* ======================= action_simp_tac ============================== *) |
|
253 |
||
254 |
ML {* |
|
255 |
(* A dumb simplification-based tactic with just a little first-order logic: |
|
256 |
should plug in only "very safe" rules that can be applied blindly. |
|
257 |
Note that it applies whatever simplifications are currently active. |
|
258 |
*) |
|
259 |
fun action_simp_tac ss intros elims = |
|
260 |
asm_full_simp_tac |
|
261 |
(ss setloop ((resolve_tac ((map action_use intros) |
|
24180 | 262 |
@ [refl,impI,conjI,@{thm actionI},@{thm intI},allI])) |
21624 | 263 |
ORELSE' (eresolve_tac ((map action_use elims) |
264 |
@ [conjE,disjE,exE])))); |
|
265 |
*} |
|
266 |
||
267 |
(* ---------------- enabled_tac: tactic to prove (Enabled A) -------------------- *) |
|
268 |
||
269 |
ML {* |
|
270 |
(* "Enabled A" can be proven as follows: |
|
271 |
- Assume that we know which state variables are "base variables" |
|
272 |
this should be expressed by a theorem of the form "basevars (x,y,z,...)". |
|
273 |
- Resolve this theorem with baseE to introduce a constant for the value of the |
|
274 |
variables in the successor state, and resolve the goal with the result. |
|
275 |
- Resolve with enabledI and do some rewriting. |
|
276 |
- Solve for the unknowns using standard HOL reasoning. |
|
277 |
The following tactic combines these steps except the final one. |
|
278 |
*) |
|
279 |
||
24180 | 280 |
fun enabled_tac (cs, ss) base_vars = |
281 |
clarsimp_tac (cs addSIs [base_vars RS @{thm base_enabled}], ss); |
|
21624 | 282 |
*} |
283 |
||
284 |
(* Example *) |
|
285 |
||
286 |
lemma |
|
287 |
assumes "basevars (x,y,z)" |
|
288 |
shows "|- x --> Enabled ($x & (y$ = #False))" |
|
24180 | 289 |
apply (tactic {* enabled_tac @{clasimpset} @{thm assms} 1 *}) |
21624 | 290 |
apply auto |
291 |
done |
|
292 |
||
293 |
end |