author | wenzelm |
Fri, 26 Jun 2015 15:55:44 +0200 | |
changeset 60591 | e0b77517f9a9 |
parent 60588 | 750c533459b1 |
child 60592 | c9bd1d902f04 |
permissions | -rw-r--r-- |
60587 | 1 |
(* Title: HOL/TLA/Action.thy |
35108 | 2 |
Author: Stephan Merz |
3 |
Copyright: 1998 University of Munich |
|
21624 | 4 |
*) |
3807 | 5 |
|
58889 | 6 |
section {* 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 |
||
60588 | 15 |
type_synonym 'a trfun = "(state * state) \<Rightarrow> 'a" |
42018 | 16 |
type_synonym action = "bool trfun" |
6255 | 17 |
|
55382
9218fa411c15
prefer vacuous definitional type classes over axiomatic ones;
wenzelm
parents:
54742
diff
changeset
|
18 |
instance prod :: (world, world) world .. |
3807 | 19 |
|
20 |
consts |
|
6255 | 21 |
(** abstract syntax **) |
60588 | 22 |
before :: "'a stfun \<Rightarrow> 'a trfun" |
23 |
after :: "'a stfun \<Rightarrow> 'a trfun" |
|
24 |
unch :: "'a stfun \<Rightarrow> action" |
|
6255 | 25 |
|
60588 | 26 |
SqAct :: "[action, 'a stfun] \<Rightarrow> action" |
27 |
AnAct :: "[action, 'a stfun] \<Rightarrow> action" |
|
28 |
enabled :: "action \<Rightarrow> stpred" |
|
6255 | 29 |
|
30 |
(** concrete syntax **) |
|
31 |
||
32 |
syntax |
|
33 |
(* Syntax for writing action expressions in arbitrary contexts *) |
|
60588 | 34 |
"_ACT" :: "lift \<Rightarrow> 'a" ("(ACT _)") |
3807 | 35 |
|
60588 | 36 |
"_before" :: "lift \<Rightarrow> lift" ("($_)" [100] 99) |
37 |
"_after" :: "lift \<Rightarrow> lift" ("(_$)" [100] 99) |
|
38 |
"_unchanged" :: "lift \<Rightarrow> lift" ("(unchanged _)" [100] 99) |
|
6255 | 39 |
|
40 |
(*** Priming: same as "after" ***) |
|
60588 | 41 |
"_prime" :: "lift \<Rightarrow> lift" ("(_`)" [100] 99) |
6255 | 42 |
|
60588 | 43 |
"_SqAct" :: "[lift, lift] \<Rightarrow> lift" ("([_]'_(_))" [0,1000] 99) |
44 |
"_AnAct" :: "[lift, lift] \<Rightarrow> lift" ("(<_>'_(_))" [0,1000] 99) |
|
45 |
"_Enabled" :: "lift \<Rightarrow> lift" ("(Enabled _)" [100] 100) |
|
3807 | 46 |
|
6255 | 47 |
translations |
60588 | 48 |
"ACT A" => "(A::state*state \<Rightarrow> _)" |
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" |
|
60591 | 56 |
"w \<Turnstile> [A]_v" <= "_SqAct A v w" |
57 |
"w \<Turnstile> <A>_v" <= "_AnAct A v w" |
|
58 |
"s \<Turnstile> Enabled A" <= "_Enabled A s" |
|
59 |
"w \<Turnstile> unchanged f" <= "_unchanged f w" |
|
3807 | 60 |
|
47968 | 61 |
axiomatization where |
60588 | 62 |
unl_before: "(ACT $v) (s,t) \<equiv> v s" and |
63 |
unl_after: "(ACT v$) (s,t) \<equiv> v t" and |
|
3807 | 64 |
|
60588 | 65 |
unchanged_def: "(s,t) \<Turnstile> unchanged v \<equiv> (v t = v s)" |
47968 | 66 |
|
67 |
defs |
|
60588 | 68 |
square_def: "ACT [A]_v \<equiv> ACT (A \<or> unchanged v)" |
69 |
angle_def: "ACT <A>_v \<equiv> ACT (A \<and> \<not> unchanged v)" |
|
3807 | 70 |
|
60588 | 71 |
enabled_def: "s \<Turnstile> Enabled A \<equiv> \<exists>u. (s,u) \<Turnstile> A" |
17309 | 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!]: |
|
60588 | 79 |
assumes "\<And>s t. (s,t) \<Turnstile> A" |
80 |
shows "\<turnstile> 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 |
||
60588 | 84 |
lemma actionD [dest]: "\<turnstile> A \<Longrightarrow> (s,t) \<Turnstile> A" |
21624 | 85 |
apply (erule intD) |
86 |
done |
|
87 |
||
88 |
lemma pr_rews [int_rewrite]: |
|
60588 | 89 |
"\<turnstile> (#c)` = #c" |
90 |
"\<And>f. \<turnstile> f<x>` = f<x` >" |
|
91 |
"\<And>f. \<turnstile> f<x,y>` = f<x`,y` >" |
|
92 |
"\<And>f. \<turnstile> f<x,y,z>` = f<x`,y`,z` >" |
|
93 |
"\<turnstile> (\<forall>x. P x)` = (\<forall>x. (P x)`)" |
|
94 |
"\<turnstile> (\<exists>x. P x)` = (\<exists>x. (P x)`)" |
|
21624 | 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 |
||
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52037
diff
changeset
|
111 |
fun action_unlift ctxt th = |
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52037
diff
changeset
|
112 |
(rewrite_rule ctxt @{thms action_rews} (th RS @{thm actionD})) |
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52037
diff
changeset
|
113 |
handle THM _ => int_unlift ctxt th; |
21624 | 114 |
|
60588 | 115 |
(* Turn \<turnstile> A = B into meta-level rewrite rule A == B *) |
21624 | 116 |
val action_rewrite = int_rewrite |
117 |
||
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52037
diff
changeset
|
118 |
fun action_use ctxt th = |
59582 | 119 |
case Thm.concl_of th of |
56256 | 120 |
Const _ $ (Const (@{const_name Valid}, _) $ _) => |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52037
diff
changeset
|
121 |
(flatten (action_unlift ctxt th) handle THM _ => th) |
21624 | 122 |
| _ => th; |
123 |
*} |
|
124 |
||
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52037
diff
changeset
|
125 |
attribute_setup action_unlift = |
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52037
diff
changeset
|
126 |
{* Scan.succeed (Thm.rule_attribute (action_unlift o Context.proof_of)) *} |
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52037
diff
changeset
|
127 |
attribute_setup action_rewrite = |
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52037
diff
changeset
|
128 |
{* Scan.succeed (Thm.rule_attribute (action_rewrite o Context.proof_of)) *} |
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52037
diff
changeset
|
129 |
attribute_setup action_use = |
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52037
diff
changeset
|
130 |
{* Scan.succeed (Thm.rule_attribute (action_use o Context.proof_of)) *} |
21624 | 131 |
|
132 |
||
133 |
(* =========================== square / angle brackets =========================== *) |
|
134 |
||
60588 | 135 |
lemma idle_squareI: "(s,t) \<Turnstile> unchanged v \<Longrightarrow> (s,t) \<Turnstile> [A]_v" |
21624 | 136 |
by (simp add: square_def) |
137 |
||
60588 | 138 |
lemma busy_squareI: "(s,t) \<Turnstile> A \<Longrightarrow> (s,t) \<Turnstile> [A]_v" |
21624 | 139 |
by (simp add: square_def) |
60587 | 140 |
|
21624 | 141 |
lemma squareE [elim]: |
60588 | 142 |
"\<lbrakk> (s,t) \<Turnstile> [A]_v; A (s,t) \<Longrightarrow> B (s,t); v t = v s \<Longrightarrow> B (s,t) \<rbrakk> \<Longrightarrow> B (s,t)" |
21624 | 143 |
apply (unfold square_def action_rews) |
144 |
apply (erule disjE) |
|
145 |
apply simp_all |
|
146 |
done |
|
147 |
||
60588 | 148 |
lemma squareCI [intro]: "\<lbrakk> v t \<noteq> v s \<Longrightarrow> A (s,t) \<rbrakk> \<Longrightarrow> (s,t) \<Turnstile> [A]_v" |
21624 | 149 |
apply (unfold square_def action_rews) |
150 |
apply (rule disjCI) |
|
151 |
apply (erule (1) meta_mp) |
|
152 |
done |
|
153 |
||
60588 | 154 |
lemma angleI [intro]: "\<And>s t. \<lbrakk> A (s,t); v t \<noteq> v s \<rbrakk> \<Longrightarrow> (s,t) \<Turnstile> <A>_v" |
21624 | 155 |
by (simp add: angle_def) |
156 |
||
60588 | 157 |
lemma angleE [elim]: "\<lbrakk> (s,t) \<Turnstile> <A>_v; \<lbrakk> A (s,t); v t \<noteq> v s \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R" |
21624 | 158 |
apply (unfold angle_def action_rews) |
159 |
apply (erule conjE) |
|
160 |
apply simp |
|
161 |
done |
|
162 |
||
163 |
lemma square_simulation: |
|
60591 | 164 |
"\<And>f. \<lbrakk> \<turnstile> unchanged f \<and> \<not>B \<longrightarrow> unchanged g; |
165 |
\<turnstile> A \<and> \<not>unchanged g \<longrightarrow> B |
|
60588 | 166 |
\<rbrakk> \<Longrightarrow> \<turnstile> [A]_f \<longrightarrow> [B]_g" |
21624 | 167 |
apply clarsimp |
168 |
apply (erule squareE) |
|
169 |
apply (auto simp add: square_def) |
|
170 |
done |
|
171 |
||
60588 | 172 |
lemma not_square: "\<turnstile> (\<not> [A]_v) = <\<not>A>_v" |
21624 | 173 |
by (auto simp: square_def angle_def) |
174 |
||
60588 | 175 |
lemma not_angle: "\<turnstile> (\<not> <A>_v) = [\<not>A]_v" |
21624 | 176 |
by (auto simp: square_def angle_def) |
177 |
||
178 |
||
179 |
(* ============================== Facts about ENABLED ============================== *) |
|
180 |
||
60588 | 181 |
lemma enabledI: "\<turnstile> A \<longrightarrow> $Enabled A" |
21624 | 182 |
by (auto simp add: enabled_def) |
183 |
||
60588 | 184 |
lemma enabledE: "\<lbrakk> s \<Turnstile> Enabled A; \<And>u. A (s,u) \<Longrightarrow> Q \<rbrakk> \<Longrightarrow> Q" |
21624 | 185 |
apply (unfold enabled_def) |
186 |
apply (erule exE) |
|
187 |
apply simp |
|
188 |
done |
|
189 |
||
60588 | 190 |
lemma notEnabledD: "\<turnstile> \<not>$Enabled G \<longrightarrow> \<not> G" |
21624 | 191 |
by (auto simp add: enabled_def) |
192 |
||
193 |
(* Monotonicity *) |
|
194 |
lemma enabled_mono: |
|
60588 | 195 |
assumes min: "s \<Turnstile> Enabled F" |
196 |
and maj: "\<turnstile> F \<longrightarrow> G" |
|
197 |
shows "s \<Turnstile> Enabled G" |
|
21624 | 198 |
apply (rule min [THEN enabledE]) |
199 |
apply (rule enabledI [action_use]) |
|
200 |
apply (erule maj [action_use]) |
|
201 |
done |
|
202 |
||
203 |
(* stronger variant *) |
|
204 |
lemma enabled_mono2: |
|
60588 | 205 |
assumes min: "s \<Turnstile> Enabled F" |
206 |
and maj: "\<And>t. F (s,t) \<Longrightarrow> G (s,t)" |
|
207 |
shows "s \<Turnstile> Enabled G" |
|
21624 | 208 |
apply (rule min [THEN enabledE]) |
209 |
apply (rule enabledI [action_use]) |
|
210 |
apply (erule maj) |
|
211 |
done |
|
212 |
||
60591 | 213 |
lemma enabled_disj1: "\<turnstile> Enabled F \<longrightarrow> Enabled (F \<or> G)" |
21624 | 214 |
by (auto elim!: enabled_mono) |
215 |
||
60591 | 216 |
lemma enabled_disj2: "\<turnstile> Enabled G \<longrightarrow> Enabled (F \<or> G)" |
21624 | 217 |
by (auto elim!: enabled_mono) |
218 |
||
60591 | 219 |
lemma enabled_conj1: "\<turnstile> Enabled (F \<and> G) \<longrightarrow> Enabled F" |
21624 | 220 |
by (auto elim!: enabled_mono) |
221 |
||
60591 | 222 |
lemma enabled_conj2: "\<turnstile> Enabled (F \<and> G) \<longrightarrow> Enabled G" |
21624 | 223 |
by (auto elim!: enabled_mono) |
224 |
||
225 |
lemma enabled_conjE: |
|
60591 | 226 |
"\<lbrakk> s \<Turnstile> Enabled (F \<and> G); \<lbrakk> s \<Turnstile> Enabled F; s \<Turnstile> Enabled G \<rbrakk> \<Longrightarrow> Q \<rbrakk> \<Longrightarrow> Q" |
21624 | 227 |
apply (frule enabled_conj1 [action_use]) |
228 |
apply (drule enabled_conj2 [action_use]) |
|
229 |
apply simp |
|
230 |
done |
|
231 |
||
60591 | 232 |
lemma enabled_disjD: "\<turnstile> Enabled (F \<or> G) \<longrightarrow> Enabled F \<or> Enabled G" |
21624 | 233 |
by (auto simp add: enabled_def) |
234 |
||
60591 | 235 |
lemma enabled_disj: "\<turnstile> Enabled (F \<or> G) = (Enabled F \<or> Enabled G)" |
21624 | 236 |
apply clarsimp |
237 |
apply (rule iffI) |
|
238 |
apply (erule enabled_disjD [action_use]) |
|
239 |
apply (erule disjE enabled_disj1 [action_use] enabled_disj2 [action_use])+ |
|
240 |
done |
|
241 |
||
60588 | 242 |
lemma enabled_ex: "\<turnstile> Enabled (\<exists>x. F x) = (\<exists>x. Enabled (F x))" |
21624 | 243 |
by (force simp add: enabled_def) |
244 |
||
245 |
||
246 |
(* A rule that combines enabledI and baseE, but generates fewer instantiations *) |
|
247 |
lemma base_enabled: |
|
60588 | 248 |
"\<lbrakk> basevars vs; \<exists>c. \<forall>u. vs u = c \<longrightarrow> A(s,u) \<rbrakk> \<Longrightarrow> s \<Turnstile> Enabled A" |
21624 | 249 |
apply (erule exE) |
250 |
apply (erule baseE) |
|
251 |
apply (rule enabledI [action_use]) |
|
252 |
apply (erule allE) |
|
253 |
apply (erule mp) |
|
254 |
apply assumption |
|
255 |
done |
|
256 |
||
257 |
(* ======================= action_simp_tac ============================== *) |
|
258 |
||
259 |
ML {* |
|
260 |
(* A dumb simplification-based tactic with just a little first-order logic: |
|
261 |
should plug in only "very safe" rules that can be applied blindly. |
|
262 |
Note that it applies whatever simplifications are currently active. |
|
263 |
*) |
|
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52037
diff
changeset
|
264 |
fun action_simp_tac ctxt intros elims = |
21624 | 265 |
asm_full_simp_tac |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58889
diff
changeset
|
266 |
(ctxt setloop (fn _ => (resolve_tac ctxt ((map (action_use ctxt) intros) |
24180 | 267 |
@ [refl,impI,conjI,@{thm actionI},@{thm intI},allI])) |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58889
diff
changeset
|
268 |
ORELSE' (eresolve_tac ctxt ((map (action_use ctxt) elims) |
21624 | 269 |
@ [conjE,disjE,exE])))); |
270 |
*} |
|
271 |
||
272 |
(* ---------------- enabled_tac: tactic to prove (Enabled A) -------------------- *) |
|
273 |
||
274 |
ML {* |
|
275 |
(* "Enabled A" can be proven as follows: |
|
276 |
- Assume that we know which state variables are "base variables" |
|
277 |
this should be expressed by a theorem of the form "basevars (x,y,z,...)". |
|
278 |
- Resolve this theorem with baseE to introduce a constant for the value of the |
|
279 |
variables in the successor state, and resolve the goal with the result. |
|
280 |
- Resolve with enabledI and do some rewriting. |
|
281 |
- Solve for the unknowns using standard HOL reasoning. |
|
282 |
The following tactic combines these steps except the final one. |
|
283 |
*) |
|
284 |
||
42785 | 285 |
fun enabled_tac ctxt base_vars = |
42793 | 286 |
clarsimp_tac (ctxt addSIs [base_vars RS @{thm base_enabled}]); |
21624 | 287 |
*} |
288 |
||
42785 | 289 |
method_setup enabled = {* |
290 |
Attrib.thm >> (fn th => fn ctxt => SIMPLE_METHOD' (enabled_tac ctxt th)) |
|
42814 | 291 |
*} |
42785 | 292 |
|
21624 | 293 |
(* Example *) |
294 |
||
295 |
lemma |
|
296 |
assumes "basevars (x,y,z)" |
|
60591 | 297 |
shows "\<turnstile> x \<longrightarrow> Enabled ($x \<and> (y$ = #False))" |
42785 | 298 |
apply (enabled assms) |
21624 | 299 |
apply auto |
300 |
done |
|
301 |
||
302 |
end |