1(*  Title:      HOL/TLA/TLA.thy
2    Author:     Stephan Merz
3    Copyright:  1998 University of Munich
4*)
5
6section \<open>The temporal level of TLA\<close>
7
8theory TLA
9imports Init
10begin
11
12consts
13  (** abstract syntax **)
14  Box        :: "('w::world) form \<Rightarrow> temporal"
15  Dmd        :: "('w::world) form \<Rightarrow> temporal"
16  leadsto    :: "['w::world form, 'v::world form] \<Rightarrow> temporal"
17  Stable     :: "stpred \<Rightarrow> temporal"
18  WF         :: "[action, 'a stfun] \<Rightarrow> temporal"
19  SF         :: "[action, 'a stfun] \<Rightarrow> temporal"
20
21  (* Quantification over (flexible) state variables *)
22  EEx        :: "('a stfun \<Rightarrow> temporal) \<Rightarrow> temporal"       (binder "Eex " 10)
23  AAll       :: "('a stfun \<Rightarrow> temporal) \<Rightarrow> temporal"       (binder "Aall " 10)
24
25  (** concrete syntax **)
26syntax
27  "_Box"     :: "lift \<Rightarrow> lift"                        ("(\<box>_)" [40] 40)
28  "_Dmd"     :: "lift \<Rightarrow> lift"                        ("(\<diamond>_)" [40] 40)
29  "_leadsto" :: "[lift,lift] \<Rightarrow> lift"                 ("(_ \<leadsto> _)" [23,22] 22)
30  "_stable"  :: "lift \<Rightarrow> lift"                        ("(stable/ _)")
31  "_WF"      :: "[lift,lift] \<Rightarrow> lift"                 ("(WF'(_')'_(_))" [0,60] 55)
32  "_SF"      :: "[lift,lift] \<Rightarrow> lift"                 ("(SF'(_')'_(_))" [0,60] 55)
33
34  "_EEx"     :: "[idts, lift] \<Rightarrow> lift"                ("(3\<exists>\<exists> _./ _)" [0,10] 10)
35  "_AAll"    :: "[idts, lift] \<Rightarrow> lift"                ("(3\<forall>\<forall> _./ _)" [0,10] 10)
36
37translations
38  "_Box"      ==   "CONST Box"
39  "_Dmd"      ==   "CONST Dmd"
40  "_leadsto"  ==   "CONST leadsto"
41  "_stable"   ==   "CONST Stable"
42  "_WF"       ==   "CONST WF"
43  "_SF"       ==   "CONST SF"
44  "_EEx v A"  ==   "Eex v. A"
45  "_AAll v A" ==   "Aall v. A"
46
47  "sigma \<Turnstile> \<box>F"         <= "_Box F sigma"
48  "sigma \<Turnstile> \<diamond>F"         <= "_Dmd F sigma"
49  "sigma \<Turnstile> F \<leadsto> G"      <= "_leadsto F G sigma"
50  "sigma \<Turnstile> stable P"    <= "_stable P sigma"
51  "sigma \<Turnstile> WF(A)_v"     <= "_WF A v sigma"
52  "sigma \<Turnstile> SF(A)_v"     <= "_SF A v sigma"
53  "sigma \<Turnstile> \<exists>\<exists>x. F"    <= "_EEx x F sigma"
54  "sigma \<Turnstile> \<forall>\<forall>x. F"    <= "_AAll x F sigma"
55
56axiomatization where
57  (* Definitions of derived operators *)
58  dmd_def:      "\<And>F. TEMP \<diamond>F  ==  TEMP \<not>\<box>\<not>F"
59
60axiomatization where
61  boxInit:      "\<And>F. TEMP \<box>F  ==  TEMP \<box>Init F" and
62  leadsto_def:  "\<And>F G. TEMP F \<leadsto> G  ==  TEMP \<box>(Init F \<longrightarrow> \<diamond>G)" and
63  stable_def:   "\<And>P. TEMP stable P  ==  TEMP \<box>($P \<longrightarrow> P$)" and
64  WF_def:       "TEMP WF(A)_v  ==  TEMP \<diamond>\<box> Enabled(<A>_v) \<longrightarrow> \<box>\<diamond><A>_v" and
65  SF_def:       "TEMP SF(A)_v  ==  TEMP \<box>\<diamond> Enabled(<A>_v) \<longrightarrow> \<box>\<diamond><A>_v" and
66  aall_def:     "TEMP (\<forall>\<forall>x. F x)  ==  TEMP \<not> (\<exists>\<exists>x. \<not> F x)"
67
68axiomatization where
69(* Base axioms for raw TLA. *)
70  normalT:    "\<And>F G. \<turnstile> \<box>(F \<longrightarrow> G) \<longrightarrow> (\<box>F \<longrightarrow> \<box>G)" and    (* polymorphic *)
71  reflT:      "\<And>F. \<turnstile> \<box>F \<longrightarrow> F" and         (* F::temporal *)
72  transT:     "\<And>F. \<turnstile> \<box>F \<longrightarrow> \<box>\<box>F" and     (* polymorphic *)
73  linT:       "\<And>F G. \<turnstile> \<diamond>F \<and> \<diamond>G \<longrightarrow> (\<diamond>(F \<and> \<diamond>G)) \<or> (\<diamond>(G \<and> \<diamond>F))" and
74  discT:      "\<And>F. \<turnstile> \<box>(F \<longrightarrow> \<diamond>(\<not>F \<and> \<diamond>F)) \<longrightarrow> (F \<longrightarrow> \<box>\<diamond>F)" and
75  primeI:     "\<And>P. \<turnstile> \<box>P \<longrightarrow> Init P`" and
76  primeE:     "\<And>P F. \<turnstile> \<box>(Init P \<longrightarrow> \<box>F) \<longrightarrow> Init P` \<longrightarrow> (F \<longrightarrow> \<box>F)" and
77  indT:       "\<And>P F. \<turnstile> \<box>(Init P \<and> \<not>\<box>F \<longrightarrow> Init P` \<and> F) \<longrightarrow> Init P \<longrightarrow> \<box>F" and
78  allT:       "\<And>F. \<turnstile> (\<forall>x. \<box>(F x)) = (\<box>(\<forall> x. F x))"
79
80axiomatization where
81  necT:       "\<And>F. \<turnstile> F \<Longrightarrow> \<turnstile> \<box>F"      (* polymorphic *)
82
83axiomatization where
84(* Flexible quantification: refinement mappings, history variables *)
85  eexI:       "\<turnstile> F x \<longrightarrow> (\<exists>\<exists>x. F x)" and
86  eexE:       "\<lbrakk> sigma \<Turnstile> (\<exists>\<exists>x. F x); basevars vs;
87                 (\<And>x. \<lbrakk> basevars (x, vs); sigma \<Turnstile> F x \<rbrakk> \<Longrightarrow> (G sigma)::bool)
88              \<rbrakk> \<Longrightarrow> G sigma" and
89  history:    "\<turnstile> \<exists>\<exists>h. Init(h = ha) \<and> \<box>(\<forall>x. $h = #x \<longrightarrow> h` = hb x)"
90
91
92(* Specialize intensional introduction/elimination rules for temporal formulas *)
93
94lemma tempI [intro!]: "(\<And>sigma. sigma \<Turnstile> (F::temporal)) \<Longrightarrow> \<turnstile> F"
95  apply (rule intI)
96  apply (erule meta_spec)
97  done
98
99lemma tempD [dest]: "\<turnstile> (F::temporal) \<Longrightarrow> sigma \<Turnstile> F"
100  by (erule intD)
101
102
103(* ======== Functions to "unlift" temporal theorems ====== *)
104
105ML \<open>
106(* The following functions are specialized versions of the corresponding
107   functions defined in theory Intensional in that they introduce a
108   "world" parameter of type "behavior".
109*)
110fun temp_unlift ctxt th =
111  (rewrite_rule ctxt @{thms action_rews} (th RS @{thm tempD}))
112    handle THM _ => action_unlift ctxt th;
113
114(* Turn  \<turnstile> F = G  into meta-level rewrite rule  F == G *)
115val temp_rewrite = int_rewrite
116
117fun temp_use ctxt th =
118  case Thm.concl_of th of
119    Const _ $ (Const (\<^const_name>\<open>Intensional.Valid\<close>, _) $ _) =>
120            ((flatten (temp_unlift ctxt th)) handle THM _ => th)
121  | _ => th;
122
123fun try_rewrite ctxt th = temp_rewrite ctxt th handle THM _ => temp_use ctxt th;
124\<close>
125
126attribute_setup temp_unlift =
127  \<open>Scan.succeed (Thm.rule_attribute [] (temp_unlift o Context.proof_of))\<close>
128attribute_setup temp_rewrite =
129  \<open>Scan.succeed (Thm.rule_attribute [] (temp_rewrite o Context.proof_of))\<close>
130attribute_setup temp_use =
131  \<open>Scan.succeed (Thm.rule_attribute [] (temp_use o Context.proof_of))\<close>
132attribute_setup try_rewrite =
133  \<open>Scan.succeed (Thm.rule_attribute [] (try_rewrite o Context.proof_of))\<close>
134
135
136(* ------------------------------------------------------------------------- *)
137(***           "Simple temporal logic": only \<box> and \<diamond>                     ***)
138(* ------------------------------------------------------------------------- *)
139section "Simple temporal logic"
140
141(* \<box>\<not>F == \<box>\<not>Init F *)
142lemmas boxNotInit = boxInit [of "LIFT \<not>F", unfolded Init_simps] for F
143
144lemma dmdInit: "TEMP \<diamond>F == TEMP \<diamond> Init F"
145  apply (unfold dmd_def)
146  apply (unfold boxInit [of "LIFT \<not>F"])
147  apply (simp (no_asm) add: Init_simps)
148  done
149
150lemmas dmdNotInit = dmdInit [of "LIFT \<not>F", unfolded Init_simps] for F
151
152(* boxInit and dmdInit cannot be used as rewrites, because they loop.
153   Non-looping instances for state predicates and actions are occasionally useful.
154*)
155lemmas boxInit_stp = boxInit [where 'a = state]
156lemmas boxInit_act = boxInit [where 'a = "state * state"]
157lemmas dmdInit_stp = dmdInit [where 'a = state]
158lemmas dmdInit_act = dmdInit [where 'a = "state * state"]
159
160(* The symmetric equations can be used to get rid of Init *)
161lemmas boxInitD = boxInit [symmetric]
162lemmas dmdInitD = dmdInit [symmetric]
163lemmas boxNotInitD = boxNotInit [symmetric]
164lemmas dmdNotInitD = dmdNotInit [symmetric]
165
166lemmas Init_simps = Init_simps boxInitD dmdInitD boxNotInitD dmdNotInitD
167
168(* ------------------------ STL2 ------------------------------------------- *)
169lemmas STL2 = reflT
170
171(* The "polymorphic" (generic) variant *)
172lemma STL2_gen: "\<turnstile> \<box>F \<longrightarrow> Init F"
173  apply (unfold boxInit [of F])
174  apply (rule STL2)
175  done
176
177(* see also STL2_pr below: "\<turnstile> \<box>P \<longrightarrow> Init P & Init (P`)" *)
178
179
180(* Dual versions for \<diamond> *)
181lemma InitDmd: "\<turnstile> F \<longrightarrow> \<diamond> F"
182  apply (unfold dmd_def)
183  apply (auto dest!: STL2 [temp_use])
184  done
185
186lemma InitDmd_gen: "\<turnstile> Init F \<longrightarrow> \<diamond>F"
187  apply clarsimp
188  apply (drule InitDmd [temp_use])
189  apply (simp add: dmdInitD)
190  done
191
192
193(* ------------------------ STL3 ------------------------------------------- *)
194lemma STL3: "\<turnstile> (\<box>\<box>F) = (\<box>F)"
195  by (auto elim: transT [temp_use] STL2 [temp_use])
196
197(* corresponding elimination rule introduces double boxes:
198   \<lbrakk> (sigma \<Turnstile> \<box>F); (sigma \<Turnstile> \<box>\<box>F) \<Longrightarrow> PROP W \<rbrakk> \<Longrightarrow> PROP W
199*)
200lemmas dup_boxE = STL3 [temp_unlift, THEN iffD2, elim_format]
201lemmas dup_boxD = STL3 [temp_unlift, THEN iffD1]
202
203(* dual versions for \<diamond> *)
204lemma DmdDmd: "\<turnstile> (\<diamond>\<diamond>F) = (\<diamond>F)"
205  by (auto simp add: dmd_def [try_rewrite] STL3 [try_rewrite])
206
207lemmas dup_dmdE = DmdDmd [temp_unlift, THEN iffD2, elim_format]
208lemmas dup_dmdD = DmdDmd [temp_unlift, THEN iffD1]
209
210
211(* ------------------------ STL4 ------------------------------------------- *)
212lemma STL4:
213  assumes "\<turnstile> F \<longrightarrow> G"
214  shows "\<turnstile> \<box>F \<longrightarrow> \<box>G"
215  apply clarsimp
216  apply (rule normalT [temp_use])
217   apply (rule assms [THEN necT, temp_use])
218  apply assumption
219  done
220
221(* Unlifted version as an elimination rule *)
222lemma STL4E: "\<lbrakk> sigma \<Turnstile> \<box>F; \<turnstile> F \<longrightarrow> G \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<box>G"
223  by (erule (1) STL4 [temp_use])
224
225lemma STL4_gen: "\<turnstile> Init F \<longrightarrow> Init G \<Longrightarrow> \<turnstile> \<box>F \<longrightarrow> \<box>G"
226  apply (drule STL4)
227  apply (simp add: boxInitD)
228  done
229
230lemma STL4E_gen: "\<lbrakk> sigma \<Turnstile> \<box>F; \<turnstile> Init F \<longrightarrow> Init G \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<box>G"
231  by (erule (1) STL4_gen [temp_use])
232
233(* see also STL4Edup below, which allows an auxiliary boxed formula:
234       \<box>A /\ F => G
235     -----------------
236     \<box>A /\ \<box>F => \<box>G
237*)
238
239(* The dual versions for \<diamond> *)
240lemma DmdImpl:
241  assumes prem: "\<turnstile> F \<longrightarrow> G"
242  shows "\<turnstile> \<diamond>F \<longrightarrow> \<diamond>G"
243  apply (unfold dmd_def)
244  apply (fastforce intro!: prem [temp_use] elim!: STL4E [temp_use])
245  done
246
247lemma DmdImplE: "\<lbrakk> sigma \<Turnstile> \<diamond>F; \<turnstile> F \<longrightarrow> G \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<diamond>G"
248  by (erule (1) DmdImpl [temp_use])
249
250(* ------------------------ STL5 ------------------------------------------- *)
251lemma STL5: "\<turnstile> (\<box>F \<and> \<box>G) = (\<box>(F \<and> G))"
252  apply auto
253  apply (subgoal_tac "sigma \<Turnstile> \<box> (G \<longrightarrow> (F \<and> G))")
254     apply (erule normalT [temp_use])
255     apply (fastforce elim!: STL4E [temp_use])+
256  done
257
258(* rewrite rule to split conjunctions under boxes *)
259lemmas split_box_conj = STL5 [temp_unlift, symmetric]
260
261
262(* the corresponding elimination rule allows to combine boxes in the hypotheses
263   (NB: F and G must have the same type, i.e., both actions or temporals.)
264   Use "addSE2" etc. if you want to add this to a claset, otherwise it will loop!
265*)
266lemma box_conjE:
267  assumes "sigma \<Turnstile> \<box>F"
268     and "sigma \<Turnstile> \<box>G"
269  and "sigma \<Turnstile> \<box>(F\<and>G) \<Longrightarrow> PROP R"
270  shows "PROP R"
271  by (rule assms STL5 [temp_unlift, THEN iffD1] conjI)+
272
273(* Instances of box_conjE for state predicates, actions, and temporals
274   in case the general rule is "too polymorphic".
275*)
276lemmas box_conjE_temp = box_conjE [where 'a = behavior]
277lemmas box_conjE_stp = box_conjE [where 'a = state]
278lemmas box_conjE_act = box_conjE [where 'a = "state * state"]
279
280(* Define a tactic that tries to merge all boxes in an antecedent. The definition is
281   a bit kludgy in order to simulate "double elim-resolution".
282*)
283
284lemma box_thin: "\<lbrakk> sigma \<Turnstile> \<box>F; PROP W \<rbrakk> \<Longrightarrow> PROP W" .
285
286ML \<open>
287fun merge_box_tac ctxt i =
288   REPEAT_DETERM (EVERY [eresolve_tac ctxt @{thms box_conjE} i, assume_tac ctxt i,
289    eresolve_tac ctxt @{thms box_thin} i])
290
291fun merge_temp_box_tac ctxt i =
292  REPEAT_DETERM (EVERY [eresolve_tac ctxt @{thms box_conjE_temp} i, assume_tac ctxt i,
293    Rule_Insts.eres_inst_tac ctxt [((("'a", 0), Position.none), "behavior")] [] @{thm box_thin} i])
294
295fun merge_stp_box_tac ctxt i =
296  REPEAT_DETERM (EVERY [eresolve_tac ctxt @{thms box_conjE_stp} i, assume_tac ctxt i,
297    Rule_Insts.eres_inst_tac ctxt [((("'a", 0), Position.none), "state")] [] @{thm box_thin} i])
298
299fun merge_act_box_tac ctxt i =
300  REPEAT_DETERM (EVERY [eresolve_tac ctxt @{thms box_conjE_act} i, assume_tac ctxt i,
301    Rule_Insts.eres_inst_tac ctxt [((("'a", 0), Position.none), "state * state")] [] @{thm box_thin} i])
302\<close>
303
304method_setup merge_box = \<open>Scan.succeed (SIMPLE_METHOD' o merge_box_tac)\<close>
305method_setup merge_temp_box = \<open>Scan.succeed (SIMPLE_METHOD' o merge_temp_box_tac)\<close>
306method_setup merge_stp_box = \<open>Scan.succeed (SIMPLE_METHOD' o merge_stp_box_tac)\<close>
307method_setup merge_act_box = \<open>Scan.succeed (SIMPLE_METHOD' o merge_act_box_tac)\<close>
308
309(* rewrite rule to push universal quantification through box:
310      (sigma \<Turnstile> \<box>(\<forall>x. F x)) = (\<forall>x. (sigma \<Turnstile> \<box>F x))
311*)
312lemmas all_box = allT [temp_unlift, symmetric]
313
314lemma DmdOr: "\<turnstile> (\<diamond>(F \<or> G)) = (\<diamond>F \<or> \<diamond>G)"
315  apply (auto simp add: dmd_def split_box_conj [try_rewrite])
316  apply (erule contrapos_np, merge_box, fastforce elim!: STL4E [temp_use])+
317  done
318
319lemma exT: "\<turnstile> (\<exists>x. \<diamond>(F x)) = (\<diamond>(\<exists>x. F x))"
320  by (auto simp: dmd_def Not_Rex [try_rewrite] all_box [try_rewrite])
321
322lemmas ex_dmd = exT [temp_unlift, symmetric]
323
324lemma STL4Edup: "\<And>sigma. \<lbrakk> sigma \<Turnstile> \<box>A; sigma \<Turnstile> \<box>F; \<turnstile> F \<and> \<box>A \<longrightarrow> G \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<box>G"
325  apply (erule dup_boxE)
326  apply merge_box
327  apply (erule STL4E)
328  apply assumption
329  done
330
331lemma DmdImpl2:
332    "\<And>sigma. \<lbrakk> sigma \<Turnstile> \<diamond>F; sigma \<Turnstile> \<box>(F \<longrightarrow> G) \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<diamond>G"
333  apply (unfold dmd_def)
334  apply auto
335  apply (erule notE)
336  apply merge_box
337  apply (fastforce elim!: STL4E [temp_use])
338  done
339
340lemma InfImpl:
341  assumes 1: "sigma \<Turnstile> \<box>\<diamond>F"
342    and 2: "sigma \<Turnstile> \<box>G"
343    and 3: "\<turnstile> F \<and> G \<longrightarrow> H"
344  shows "sigma \<Turnstile> \<box>\<diamond>H"
345  apply (insert 1 2)
346  apply (erule_tac F = G in dup_boxE)
347  apply merge_box
348  apply (fastforce elim!: STL4E [temp_use] DmdImpl2 [temp_use] intro!: 3 [temp_use])
349  done
350
351(* ------------------------ STL6 ------------------------------------------- *)
352(* Used in the proof of STL6, but useful in itself. *)
353lemma BoxDmd: "\<turnstile> \<box>F \<and> \<diamond>G \<longrightarrow> \<diamond>(\<box>F \<and> G)"
354  apply (unfold dmd_def)
355  apply clarsimp
356  apply (erule dup_boxE)
357  apply merge_box
358  apply (erule contrapos_np)
359  apply (fastforce elim!: STL4E [temp_use])
360  done
361
362(* weaker than BoxDmd, but more polymorphic (and often just right) *)
363lemma BoxDmd_simple: "\<turnstile> \<box>F \<and> \<diamond>G \<longrightarrow> \<diamond>(F \<and> G)"
364  apply (unfold dmd_def)
365  apply clarsimp
366  apply merge_box
367  apply (fastforce elim!: notE STL4E [temp_use])
368  done
369
370lemma BoxDmd2_simple: "\<turnstile> \<box>F \<and> \<diamond>G \<longrightarrow> \<diamond>(G \<and> F)"
371  apply (unfold dmd_def)
372  apply clarsimp
373  apply merge_box
374  apply (fastforce elim!: notE STL4E [temp_use])
375  done
376
377lemma DmdImpldup:
378  assumes 1: "sigma \<Turnstile> \<box>A"
379    and 2: "sigma \<Turnstile> \<diamond>F"
380    and 3: "\<turnstile> \<box>A \<and> F \<longrightarrow> G"
381  shows "sigma \<Turnstile> \<diamond>G"
382  apply (rule 2 [THEN 1 [THEN BoxDmd [temp_use]], THEN DmdImplE])
383  apply (rule 3)
384  done
385
386lemma STL6: "\<turnstile> \<diamond>\<box>F \<and> \<diamond>\<box>G \<longrightarrow> \<diamond>\<box>(F \<and> G)"
387  apply (auto simp: STL5 [temp_rewrite, symmetric])
388  apply (drule linT [temp_use])
389   apply assumption
390  apply (erule thin_rl)
391  apply (rule DmdDmd [temp_unlift, THEN iffD1])
392  apply (erule disjE)
393   apply (erule DmdImplE)
394   apply (rule BoxDmd)
395  apply (erule DmdImplE)
396  apply auto
397  apply (drule BoxDmd [temp_use])
398   apply assumption
399  apply (erule thin_rl)
400  apply (fastforce elim!: DmdImplE [temp_use])
401  done
402
403
404(* ------------------------ True / False ----------------------------------------- *)
405section "Simplification of constants"
406
407lemma BoxConst: "\<turnstile> (\<box>#P) = #P"
408  apply (rule tempI)
409  apply (cases P)
410   apply (auto intro!: necT [temp_use] dest: STL2_gen [temp_use] simp: Init_simps)
411  done
412
413lemma DmdConst: "\<turnstile> (\<diamond>#P) = #P"
414  apply (unfold dmd_def)
415  apply (cases P)
416  apply (simp_all add: BoxConst [try_rewrite])
417  done
418
419lemmas temp_simps [temp_rewrite, simp] = BoxConst DmdConst
420
421
422(* ------------------------ Further rewrites ----------------------------------------- *)
423section "Further rewrites"
424
425lemma NotBox: "\<turnstile> (\<not>\<box>F) = (\<diamond>\<not>F)"
426  by (simp add: dmd_def)
427
428lemma NotDmd: "\<turnstile> (\<not>\<diamond>F) = (\<box>\<not>F)"
429  by (simp add: dmd_def)
430
431(* These are not declared by default, because they could be harmful,
432   e.g. \<box>F & \<not>\<box>F becomes \<box>F & \<diamond>\<not>F !! *)
433lemmas more_temp_simps1 =
434  STL3 [temp_rewrite] DmdDmd [temp_rewrite] NotBox [temp_rewrite] NotDmd [temp_rewrite]
435  NotBox [temp_unlift, THEN eq_reflection]
436  NotDmd [temp_unlift, THEN eq_reflection]
437
438lemma BoxDmdBox: "\<turnstile> (\<box>\<diamond>\<box>F) = (\<diamond>\<box>F)"
439  apply (auto dest!: STL2 [temp_use])
440  apply (rule ccontr)
441  apply (subgoal_tac "sigma \<Turnstile> \<diamond>\<box>\<box>F \<and> \<diamond>\<box>\<not>\<box>F")
442   apply (erule thin_rl)
443   apply auto
444    apply (drule STL6 [temp_use])
445     apply assumption
446    apply simp
447   apply (simp_all add: more_temp_simps1)
448  done
449
450lemma DmdBoxDmd: "\<turnstile> (\<diamond>\<box>\<diamond>F) = (\<box>\<diamond>F)"
451  apply (unfold dmd_def)
452  apply (auto simp: BoxDmdBox [unfolded dmd_def, try_rewrite])
453  done
454
455lemmas more_temp_simps2 = more_temp_simps1 BoxDmdBox [temp_rewrite] DmdBoxDmd [temp_rewrite]
456
457
458(* ------------------------ Miscellaneous ----------------------------------- *)
459
460lemma BoxOr: "\<And>sigma. \<lbrakk> sigma \<Turnstile> \<box>F \<or> \<box>G \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<box>(F \<or> G)"
461  by (fastforce elim!: STL4E [temp_use])
462
463(* "persistently implies infinitely often" *)
464lemma DBImplBD: "\<turnstile> \<diamond>\<box>F \<longrightarrow> \<box>\<diamond>F"
465  apply clarsimp
466  apply (rule ccontr)
467  apply (simp add: more_temp_simps2)
468  apply (drule STL6 [temp_use])
469   apply assumption
470  apply simp
471  done
472
473lemma BoxDmdDmdBox: "\<turnstile> \<box>\<diamond>F \<and> \<diamond>\<box>G \<longrightarrow> \<box>\<diamond>(F \<and> G)"
474  apply clarsimp
475  apply (rule ccontr)
476  apply (unfold more_temp_simps2)
477  apply (drule STL6 [temp_use])
478   apply assumption
479  apply (subgoal_tac "sigma \<Turnstile> \<diamond>\<box>\<not>F")
480   apply (force simp: dmd_def)
481  apply (fastforce elim: DmdImplE [temp_use] STL4E [temp_use])
482  done
483
484
485(* ------------------------------------------------------------------------- *)
486(***          TLA-specific theorems: primed formulas                       ***)
487(* ------------------------------------------------------------------------- *)
488section "priming"
489
490(* ------------------------ TLA2 ------------------------------------------- *)
491lemma STL2_pr: "\<turnstile> \<box>P \<longrightarrow> Init P \<and> Init P`"
492  by (fastforce intro!: STL2_gen [temp_use] primeI [temp_use])
493
494(* Auxiliary lemma allows priming of boxed actions *)
495lemma BoxPrime: "\<turnstile> \<box>P \<longrightarrow> \<box>($P \<and> P$)"
496  apply clarsimp
497  apply (erule dup_boxE)
498  apply (unfold boxInit_act)
499  apply (erule STL4E)
500  apply (auto simp: Init_simps dest!: STL2_pr [temp_use])
501  done
502
503lemma TLA2:
504  assumes "\<turnstile> $P \<and> P$ \<longrightarrow> A"
505  shows "\<turnstile> \<box>P \<longrightarrow> \<box>A"
506  apply clarsimp
507  apply (drule BoxPrime [temp_use])
508  apply (auto simp: Init_stp_act_rev [try_rewrite] intro!: assms [temp_use]
509    elim!: STL4E [temp_use])
510  done
511
512lemma TLA2E: "\<lbrakk> sigma \<Turnstile> \<box>P; \<turnstile> $P \<and> P$ \<longrightarrow> A \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<box>A"
513  by (erule (1) TLA2 [temp_use])
514
515lemma DmdPrime: "\<turnstile> (\<diamond>P`) \<longrightarrow> (\<diamond>P)"
516  apply (unfold dmd_def)
517  apply (fastforce elim!: TLA2E [temp_use])
518  done
519
520lemmas PrimeDmd = InitDmd_gen [temp_use, THEN DmdPrime [temp_use]]
521
522(* ------------------------ INV1, stable --------------------------------------- *)
523section "stable, invariant"
524
525lemma ind_rule:
526   "\<lbrakk> sigma \<Turnstile> \<box>H; sigma \<Turnstile> Init P; \<turnstile> H \<longrightarrow> (Init P \<and> \<not>\<box>F \<longrightarrow> Init(P`) \<and> F) \<rbrakk>
527    \<Longrightarrow> sigma \<Turnstile> \<box>F"
528  apply (rule indT [temp_use])
529   apply (erule (2) STL4E)
530  done
531
532lemma box_stp_act: "\<turnstile> (\<box>$P) = (\<box>P)"
533  by (simp add: boxInit_act Init_simps)
534
535lemmas box_stp_actI = box_stp_act [temp_use, THEN iffD2]
536lemmas box_stp_actD = box_stp_act [temp_use, THEN iffD1]
537
538lemmas more_temp_simps3 = box_stp_act [temp_rewrite] more_temp_simps2
539
540lemma INV1:
541  "\<turnstile> (Init P) \<longrightarrow> (stable P) \<longrightarrow> \<box>P"
542  apply (unfold stable_def boxInit_stp boxInit_act)
543  apply clarsimp
544  apply (erule ind_rule)
545   apply (auto simp: Init_simps elim: ind_rule)
546  done
547
548lemma StableT:
549    "\<And>P. \<turnstile> $P \<and> A \<longrightarrow> P` \<Longrightarrow> \<turnstile> \<box>A \<longrightarrow> stable P"
550  apply (unfold stable_def)
551  apply (fastforce elim!: STL4E [temp_use])
552  done
553
554lemma Stable: "\<lbrakk> sigma \<Turnstile> \<box>A; \<turnstile> $P \<and> A \<longrightarrow> P` \<rbrakk> \<Longrightarrow> sigma \<Turnstile> stable P"
555  by (erule (1) StableT [temp_use])
556
557(* Generalization of INV1 *)
558lemma StableBox: "\<turnstile> (stable P) \<longrightarrow> \<box>(Init P \<longrightarrow> \<box>P)"
559  apply (unfold stable_def)
560  apply clarsimp
561  apply (erule dup_boxE)
562  apply (force simp: stable_def elim: STL4E [temp_use] INV1 [temp_use])
563  done
564
565lemma DmdStable: "\<turnstile> (stable P) \<and> \<diamond>P \<longrightarrow> \<diamond>\<box>P"
566  apply clarsimp
567  apply (rule DmdImpl2)
568   prefer 2
569   apply (erule StableBox [temp_use])
570  apply (simp add: dmdInitD)
571  done
572
573(* ---------------- (Semi-)automatic invariant tactics ---------------------- *)
574
575ML \<open>
576(* inv_tac reduces goals of the form ... \<Longrightarrow> sigma \<Turnstile> \<box>P *)
577fun inv_tac ctxt =
578  SELECT_GOAL
579    (EVERY
580     [auto_tac ctxt,
581      TRY (merge_box_tac ctxt 1),
582      resolve_tac ctxt [temp_use ctxt @{thm INV1}] 1, (* fail if the goal is not a box *)
583      TRYALL (eresolve_tac ctxt @{thms Stable})]);
584
585(* auto_inv_tac applies inv_tac and then tries to attack the subgoals
586   in simple cases it may be able to handle goals like \<turnstile> MyProg \<longrightarrow> \<box>Inv.
587   In these simple cases the simplifier seems to be more useful than the
588   auto-tactic, which applies too much propositional logic and simplifies
589   too late.
590*)
591fun auto_inv_tac ctxt =
592  SELECT_GOAL
593    (inv_tac ctxt 1 THEN
594      (TRYALL (action_simp_tac
595        (ctxt addsimps [@{thm Init_stp}, @{thm Init_act}]) [] [@{thm squareE}])));
596\<close>
597
598method_setup invariant = \<open>
599  Method.sections Clasimp.clasimp_modifiers >> (K (SIMPLE_METHOD' o inv_tac))
600\<close>
601
602method_setup auto_invariant = \<open>
603  Method.sections Clasimp.clasimp_modifiers >> (K (SIMPLE_METHOD' o auto_inv_tac))
604\<close>
605
606lemma unless: "\<turnstile> \<box>($P \<longrightarrow> P` \<or> Q`) \<longrightarrow> (stable P) \<or> \<diamond>Q"
607  apply (unfold dmd_def)
608  apply (clarsimp dest!: BoxPrime [temp_use])
609  apply merge_box
610  apply (erule contrapos_np)
611  apply (fastforce elim!: Stable [temp_use])
612  done
613
614
615(* --------------------- Recursive expansions --------------------------------------- *)
616section "recursive expansions"
617
618(* Recursive expansions of \<box> and \<diamond> for state predicates *)
619lemma BoxRec: "\<turnstile> (\<box>P) = (Init P \<and> \<box>P`)"
620  apply (auto intro!: STL2_gen [temp_use])
621   apply (fastforce elim!: TLA2E [temp_use])
622  apply (auto simp: stable_def elim!: INV1 [temp_use] STL4E [temp_use])
623  done
624
625lemma DmdRec: "\<turnstile> (\<diamond>P) = (Init P \<or> \<diamond>P`)"
626  apply (unfold dmd_def BoxRec [temp_rewrite])
627  apply (auto simp: Init_simps)
628  done
629
630lemma DmdRec2: "\<And>sigma. \<lbrakk> sigma \<Turnstile> \<diamond>P; sigma \<Turnstile> \<box>\<not>P` \<rbrakk> \<Longrightarrow> sigma \<Turnstile> Init P"
631  apply (force simp: DmdRec [temp_rewrite] dmd_def)
632  done
633
634lemma InfinitePrime: "\<turnstile> (\<box>\<diamond>P) = (\<box>\<diamond>P`)"
635  apply auto
636   apply (rule classical)
637   apply (rule DBImplBD [temp_use])
638   apply (subgoal_tac "sigma \<Turnstile> \<diamond>\<box>P")
639    apply (fastforce elim!: DmdImplE [temp_use] TLA2E [temp_use])
640   apply (subgoal_tac "sigma \<Turnstile> \<diamond>\<box> (\<diamond>P \<and> \<box>\<not>P`)")
641    apply (force simp: boxInit_stp [temp_use]
642      elim!: DmdImplE [temp_use] STL4E [temp_use] DmdRec2 [temp_use])
643   apply (force intro!: STL6 [temp_use] simp: more_temp_simps3)
644  apply (fastforce intro: DmdPrime [temp_use] elim!: STL4E [temp_use])
645  done
646
647lemma InfiniteEnsures:
648  "\<lbrakk> sigma \<Turnstile> \<box>N; sigma \<Turnstile> \<box>\<diamond>A; \<turnstile> A \<and> N \<longrightarrow> P` \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<box>\<diamond>P"
649  apply (unfold InfinitePrime [temp_rewrite])
650  apply (rule InfImpl)
651    apply assumption+
652  done
653
654(* ------------------------ fairness ------------------------------------------- *)
655section "fairness"
656
657(* alternative definitions of fairness *)
658lemma WF_alt: "\<turnstile> WF(A)_v = (\<box>\<diamond>\<not>Enabled(<A>_v) \<or> \<box>\<diamond><A>_v)"
659  apply (unfold WF_def dmd_def)
660  apply fastforce
661  done
662
663lemma SF_alt: "\<turnstile> SF(A)_v = (\<diamond>\<box>\<not>Enabled(<A>_v) \<or> \<box>\<diamond><A>_v)"
664  apply (unfold SF_def dmd_def)
665  apply fastforce
666  done
667
668(* theorems to "box" fairness conditions *)
669lemma BoxWFI: "\<turnstile> WF(A)_v \<longrightarrow> \<box>WF(A)_v"
670  by (auto simp: WF_alt [try_rewrite] more_temp_simps3 intro!: BoxOr [temp_use])
671
672lemma WF_Box: "\<turnstile> (\<box>WF(A)_v) = WF(A)_v"
673  by (fastforce intro!: BoxWFI [temp_use] dest!: STL2 [temp_use])
674
675lemma BoxSFI: "\<turnstile> SF(A)_v \<longrightarrow> \<box>SF(A)_v"
676  by (auto simp: SF_alt [try_rewrite] more_temp_simps3 intro!: BoxOr [temp_use])
677
678lemma SF_Box: "\<turnstile> (\<box>SF(A)_v) = SF(A)_v"
679  by (fastforce intro!: BoxSFI [temp_use] dest!: STL2 [temp_use])
680
681lemmas more_temp_simps = more_temp_simps3 WF_Box [temp_rewrite] SF_Box [temp_rewrite]
682
683lemma SFImplWF: "\<turnstile> SF(A)_v \<longrightarrow> WF(A)_v"
684  apply (unfold SF_def WF_def)
685  apply (fastforce dest!: DBImplBD [temp_use])
686  done
687
688(* A tactic that "boxes" all fairness conditions. Apply more_temp_simps to "unbox". *)
689ML \<open>
690fun box_fair_tac ctxt =
691  SELECT_GOAL (REPEAT (dresolve_tac ctxt [@{thm BoxWFI}, @{thm BoxSFI}] 1))
692\<close>
693
694
695(* ------------------------------ leads-to ------------------------------ *)
696
697section "\<leadsto>"
698
699lemma leadsto_init: "\<turnstile> (Init F) \<and> (F \<leadsto> G) \<longrightarrow> \<diamond>G"
700  apply (unfold leadsto_def)
701  apply (auto dest!: STL2 [temp_use])
702  done
703
704(* \<turnstile> F & (F \<leadsto> G) \<longrightarrow> \<diamond>G *)
705lemmas leadsto_init_temp = leadsto_init [where 'a = behavior, unfolded Init_simps]
706
707lemma streett_leadsto: "\<turnstile> (\<box>\<diamond>Init F \<longrightarrow> \<box>\<diamond>G) = (\<diamond>(F \<leadsto> G))"
708  apply (unfold leadsto_def)
709  apply auto
710    apply (simp add: more_temp_simps)
711    apply (fastforce elim!: DmdImplE [temp_use] STL4E [temp_use])
712   apply (fastforce intro!: InitDmd [temp_use] elim!: STL4E [temp_use])
713  apply (subgoal_tac "sigma \<Turnstile> \<box>\<diamond>\<diamond>G")
714   apply (simp add: more_temp_simps)
715  apply (drule BoxDmdDmdBox [temp_use])
716   apply assumption
717  apply (fastforce elim!: DmdImplE [temp_use] STL4E [temp_use])
718  done
719
720lemma leadsto_infinite: "\<turnstile> \<box>\<diamond>F \<and> (F \<leadsto> G) \<longrightarrow> \<box>\<diamond>G"
721  apply clarsimp
722  apply (erule InitDmd [temp_use, THEN streett_leadsto [temp_unlift, THEN iffD2, THEN mp]])
723  apply (simp add: dmdInitD)
724  done
725
726(* In particular, strong fairness is a Streett condition. The following
727   rules are sometimes easier to use than WF2 or SF2 below.
728*)
729lemma leadsto_SF: "\<turnstile> (Enabled(<A>_v) \<leadsto> <A>_v) \<longrightarrow> SF(A)_v"
730  apply (unfold SF_def)
731  apply (clarsimp elim!: leadsto_infinite [temp_use])
732  done
733
734lemma leadsto_WF: "\<turnstile> (Enabled(<A>_v) \<leadsto> <A>_v) \<longrightarrow> WF(A)_v"
735  by (clarsimp intro!: SFImplWF [temp_use] leadsto_SF [temp_use])
736
737(* introduce an invariant into the proof of a leadsto assertion.
738   \<box>I \<longrightarrow> ((P \<leadsto> Q)  =  (P /\ I \<leadsto> Q))
739*)
740lemma INV_leadsto: "\<turnstile> \<box>I \<and> (P \<and> I \<leadsto> Q) \<longrightarrow> (P \<leadsto> Q)"
741  apply (unfold leadsto_def)
742  apply clarsimp
743  apply (erule STL4Edup)
744   apply assumption
745  apply (auto simp: Init_simps dest!: STL2_gen [temp_use])
746  done
747
748lemma leadsto_classical: "\<turnstile> (Init F \<and> \<box>\<not>G \<leadsto> G) \<longrightarrow> (F \<leadsto> G)"
749  apply (unfold leadsto_def dmd_def)
750  apply (force simp: Init_simps elim!: STL4E [temp_use])
751  done
752
753lemma leadsto_false: "\<turnstile> (F \<leadsto> #False) = (\<box>\<not>F)"
754  apply (unfold leadsto_def)
755  apply (simp add: boxNotInitD)
756  done
757
758lemma leadsto_exists: "\<turnstile> ((\<exists>x. F x) \<leadsto> G) = (\<forall>x. (F x \<leadsto> G))"
759  apply (unfold leadsto_def)
760  apply (auto simp: allT [try_rewrite] Init_simps elim!: STL4E [temp_use])
761  done
762
763(* basic leadsto properties, cf. Unity *)
764
765lemma ImplLeadsto_gen: "\<turnstile> \<box>(Init F \<longrightarrow> Init G) \<longrightarrow> (F \<leadsto> G)"
766  apply (unfold leadsto_def)
767  apply (auto intro!: InitDmd_gen [temp_use]
768    elim!: STL4E_gen [temp_use] simp: Init_simps)
769  done
770
771lemmas ImplLeadsto =
772  ImplLeadsto_gen [where 'a = behavior and 'b = behavior, unfolded Init_simps]
773
774lemma ImplLeadsto_simple: "\<And>F G. \<turnstile> F \<longrightarrow> G \<Longrightarrow> \<turnstile> F \<leadsto> G"
775  by (auto simp: Init_def intro!: ImplLeadsto_gen [temp_use] necT [temp_use])
776
777lemma EnsuresLeadsto:
778  assumes "\<turnstile> A \<and> $P \<longrightarrow> Q`"
779  shows "\<turnstile> \<box>A \<longrightarrow> (P \<leadsto> Q)"
780  apply (unfold leadsto_def)
781  apply (clarsimp elim!: INV_leadsto [temp_use])
782  apply (erule STL4E_gen)
783  apply (auto simp: Init_defs intro!: PrimeDmd [temp_use] assms [temp_use])
784  done
785
786lemma EnsuresLeadsto2: "\<turnstile> \<box>($P \<longrightarrow> Q`) \<longrightarrow> (P \<leadsto> Q)"
787  apply (unfold leadsto_def)
788  apply clarsimp
789  apply (erule STL4E_gen)
790  apply (auto simp: Init_simps intro!: PrimeDmd [temp_use])
791  done
792
793lemma ensures:
794  assumes 1: "\<turnstile> $P \<and> N \<longrightarrow> P` \<or> Q`"
795    and 2: "\<turnstile> ($P \<and> N) \<and> A \<longrightarrow> Q`"
796  shows "\<turnstile> \<box>N \<and> \<box>(\<box>P \<longrightarrow> \<diamond>A) \<longrightarrow> (P \<leadsto> Q)"
797  apply (unfold leadsto_def)
798  apply clarsimp
799  apply (erule STL4Edup)
800   apply assumption
801  apply clarsimp
802  apply (subgoal_tac "sigmaa \<Turnstile> \<box>($P \<longrightarrow> P` \<or> Q`) ")
803   apply (drule unless [temp_use])
804   apply (clarsimp dest!: INV1 [temp_use])
805  apply (rule 2 [THEN DmdImpl, temp_use, THEN DmdPrime [temp_use]])
806   apply (force intro!: BoxDmd_simple [temp_use]
807     simp: split_box_conj [try_rewrite] box_stp_act [try_rewrite])
808  apply (force elim: STL4E [temp_use] dest: 1 [temp_use])
809  done
810
811lemma ensures_simple:
812  "\<lbrakk> \<turnstile> $P \<and> N \<longrightarrow> P` \<or> Q`;
813      \<turnstile> ($P \<and> N) \<and> A \<longrightarrow> Q`
814   \<rbrakk> \<Longrightarrow> \<turnstile> \<box>N \<and> \<box>\<diamond>A \<longrightarrow> (P \<leadsto> Q)"
815  apply clarsimp
816  apply (erule (2) ensures [temp_use])
817  apply (force elim!: STL4E [temp_use])
818  done
819
820lemma EnsuresInfinite:
821    "\<lbrakk> sigma \<Turnstile> \<box>\<diamond>P; sigma \<Turnstile> \<box>A; \<turnstile> A \<and> $P \<longrightarrow> Q` \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<box>\<diamond>Q"
822  apply (erule leadsto_infinite [temp_use])
823  apply (erule EnsuresLeadsto [temp_use])
824  apply assumption
825  done
826
827
828(*** Gronning's lattice rules (taken from TLP) ***)
829section "Lattice rules"
830
831lemma LatticeReflexivity: "\<turnstile> F \<leadsto> F"
832  apply (unfold leadsto_def)
833  apply (rule necT InitDmd_gen)+
834  done
835
836lemma LatticeTransitivity: "\<turnstile> (G \<leadsto> H) \<and> (F \<leadsto> G) \<longrightarrow> (F \<leadsto> H)"
837  apply (unfold leadsto_def)
838  apply clarsimp
839  apply (erule dup_boxE) (* \<box>\<box>(Init G \<longrightarrow> H) *)
840  apply merge_box
841  apply (clarsimp elim!: STL4E [temp_use])
842  apply (rule dup_dmdD)
843  apply (subgoal_tac "sigmaa \<Turnstile> \<diamond>Init G")
844   apply (erule DmdImpl2)
845   apply assumption
846  apply (simp add: dmdInitD)
847  done
848
849lemma LatticeDisjunctionElim1: "\<turnstile> (F \<or> G \<leadsto> H) \<longrightarrow> (F \<leadsto> H)"
850  apply (unfold leadsto_def)
851  apply (auto simp: Init_simps elim!: STL4E [temp_use])
852  done
853
854lemma LatticeDisjunctionElim2: "\<turnstile> (F \<or> G \<leadsto> H) \<longrightarrow> (G \<leadsto> H)"
855  apply (unfold leadsto_def)
856  apply (auto simp: Init_simps elim!: STL4E [temp_use])
857  done
858
859lemma LatticeDisjunctionIntro: "\<turnstile> (F \<leadsto> H) \<and> (G \<leadsto> H) \<longrightarrow> (F \<or> G \<leadsto> H)"
860  apply (unfold leadsto_def)
861  apply clarsimp
862  apply merge_box
863  apply (auto simp: Init_simps elim!: STL4E [temp_use])
864  done
865
866lemma LatticeDisjunction: "\<turnstile> (F \<or> G \<leadsto> H) = ((F \<leadsto> H) \<and> (G \<leadsto> H))"
867  by (auto intro: LatticeDisjunctionIntro [temp_use]
868    LatticeDisjunctionElim1 [temp_use]
869    LatticeDisjunctionElim2 [temp_use])
870
871lemma LatticeDiamond: "\<turnstile> (A \<leadsto> B \<or> C) \<and> (B \<leadsto> D) \<and> (C \<leadsto> D) \<longrightarrow> (A \<leadsto> D)"
872  apply clarsimp
873  apply (subgoal_tac "sigma \<Turnstile> (B \<or> C) \<leadsto> D")
874  apply (erule_tac G = "LIFT (B \<or> C)" in LatticeTransitivity [temp_use])
875   apply (fastforce intro!: LatticeDisjunctionIntro [temp_use])+
876  done
877
878lemma LatticeTriangle: "\<turnstile> (A \<leadsto> D \<or> B) \<and> (B \<leadsto> D) \<longrightarrow> (A \<leadsto> D)"
879  apply clarsimp
880  apply (subgoal_tac "sigma \<Turnstile> (D \<or> B) \<leadsto> D")
881   apply (erule_tac G = "LIFT (D \<or> B)" in LatticeTransitivity [temp_use])
882  apply assumption
883  apply (auto intro: LatticeDisjunctionIntro [temp_use] LatticeReflexivity [temp_use])
884  done
885
886lemma LatticeTriangle2: "\<turnstile> (A \<leadsto> B \<or> D) \<and> (B \<leadsto> D) \<longrightarrow> (A \<leadsto> D)"
887  apply clarsimp
888  apply (subgoal_tac "sigma \<Turnstile> B \<or> D \<leadsto> D")
889   apply (erule_tac G = "LIFT (B \<or> D)" in LatticeTransitivity [temp_use])
890   apply assumption
891  apply (auto intro: LatticeDisjunctionIntro [temp_use] LatticeReflexivity [temp_use])
892  done
893
894(*** Lamport's fairness rules ***)
895section "Fairness rules"
896
897lemma WF1:
898  "\<lbrakk> \<turnstile> $P \<and> N  \<longrightarrow> P` \<or> Q`;
899      \<turnstile> ($P \<and> N) \<and> <A>_v \<longrightarrow> Q`;
900      \<turnstile> $P \<and> N \<longrightarrow> $(Enabled(<A>_v)) \<rbrakk>
901  \<Longrightarrow> \<turnstile> \<box>N \<and> WF(A)_v \<longrightarrow> (P \<leadsto> Q)"
902  apply (clarsimp dest!: BoxWFI [temp_use])
903  apply (erule (2) ensures [temp_use])
904  apply (erule (1) STL4Edup)
905  apply (clarsimp simp: WF_def)
906  apply (rule STL2 [temp_use])
907  apply (clarsimp elim!: mp intro!: InitDmd [temp_use])
908  apply (erule STL4 [temp_use, THEN box_stp_actD [temp_use]])
909  apply (simp add: split_box_conj box_stp_actI)
910  done
911
912(* Sometimes easier to use; designed for action B rather than state predicate Q *)
913lemma WF_leadsto:
914  assumes 1: "\<turnstile> N \<and> $P \<longrightarrow> $Enabled (<A>_v)"
915    and 2: "\<turnstile> N \<and> <A>_v \<longrightarrow> B"
916    and 3: "\<turnstile> \<box>(N \<and> [\<not>A]_v) \<longrightarrow> stable P"
917  shows "\<turnstile> \<box>N \<and> WF(A)_v \<longrightarrow> (P \<leadsto> B)"
918  apply (unfold leadsto_def)
919  apply (clarsimp dest!: BoxWFI [temp_use])
920  apply (erule (1) STL4Edup)
921  apply clarsimp
922  apply (rule 2 [THEN DmdImpl, temp_use])
923  apply (rule BoxDmd_simple [temp_use])
924   apply assumption
925  apply (rule classical)
926  apply (rule STL2 [temp_use])
927  apply (clarsimp simp: WF_def elim!: mp intro!: InitDmd [temp_use])
928  apply (rule 1 [THEN STL4, temp_use, THEN box_stp_actD])
929  apply (simp (no_asm_simp) add: split_box_conj [try_rewrite] box_stp_act [try_rewrite])
930  apply (erule INV1 [temp_use])
931  apply (rule 3 [temp_use])
932  apply (simp add: split_box_conj [try_rewrite] NotDmd [temp_use] not_angle [try_rewrite])
933  done
934
935lemma SF1:
936  "\<lbrakk> \<turnstile> $P \<and> N  \<longrightarrow> P` \<or> Q`;
937      \<turnstile> ($P \<and> N) \<and> <A>_v \<longrightarrow> Q`;
938      \<turnstile> \<box>P \<and> \<box>N \<and> \<box>F \<longrightarrow> \<diamond>Enabled(<A>_v) \<rbrakk>
939  \<Longrightarrow> \<turnstile> \<box>N \<and> SF(A)_v \<and> \<box>F \<longrightarrow> (P \<leadsto> Q)"
940  apply (clarsimp dest!: BoxSFI [temp_use])
941  apply (erule (2) ensures [temp_use])
942  apply (erule_tac F = F in dup_boxE)
943  apply merge_temp_box
944  apply (erule STL4Edup)
945  apply assumption
946  apply (clarsimp simp: SF_def)
947  apply (rule STL2 [temp_use])
948  apply (erule mp)
949  apply (erule STL4 [temp_use])
950  apply (simp add: split_box_conj [try_rewrite] STL3 [try_rewrite])
951  done
952
953lemma WF2:
954  assumes 1: "\<turnstile> N \<and> <B>_f \<longrightarrow> <M>_g"
955    and 2: "\<turnstile> $P \<and> P` \<and> <N \<and> A>_f \<longrightarrow> B"
956    and 3: "\<turnstile> P \<and> Enabled(<M>_g) \<longrightarrow> Enabled(<A>_f)"
957    and 4: "\<turnstile> \<box>(N \<and> [\<not>B]_f) \<and> WF(A)_f \<and> \<box>F \<and> \<diamond>\<box>Enabled(<M>_g) \<longrightarrow> \<diamond>\<box>P"
958  shows "\<turnstile> \<box>N \<and> WF(A)_f \<and> \<box>F \<longrightarrow> WF(M)_g"
959  apply (clarsimp dest!: BoxWFI [temp_use] BoxDmdBox [temp_use, THEN iffD2]
960    simp: WF_def [where A = M])
961  apply (erule_tac F = F in dup_boxE)
962  apply merge_temp_box
963  apply (erule STL4Edup)
964   apply assumption
965  apply (clarsimp intro!: BoxDmd_simple [temp_use, THEN 1 [THEN DmdImpl, temp_use]])
966  apply (rule classical)
967  apply (subgoal_tac "sigmaa \<Turnstile> \<diamond> (($P \<and> P` \<and> N) \<and> <A>_f)")
968   apply (force simp: angle_def intro!: 2 [temp_use] elim!: DmdImplE [temp_use])
969  apply (rule BoxDmd_simple [THEN DmdImpl, unfolded DmdDmd [temp_rewrite], temp_use])
970  apply (simp add: NotDmd [temp_use] not_angle [try_rewrite])
971  apply merge_act_box
972  apply (frule 4 [temp_use])
973     apply assumption+
974  apply (drule STL6 [temp_use])
975   apply assumption
976  apply (erule_tac V = "sigmaa \<Turnstile> \<diamond>\<box>P" in thin_rl)
977  apply (erule_tac V = "sigmaa \<Turnstile> \<box>F" in thin_rl)
978  apply (drule BoxWFI [temp_use])
979  apply (erule_tac F = "ACT N \<and> [\<not>B]_f" in dup_boxE)
980  apply merge_temp_box
981  apply (erule DmdImpldup)
982   apply assumption
983  apply (auto simp: split_box_conj [try_rewrite] STL3 [try_rewrite]
984    WF_Box [try_rewrite] box_stp_act [try_rewrite])
985   apply (force elim!: TLA2E [where P = P, temp_use])
986  apply (rule STL2 [temp_use])
987  apply (force simp: WF_def split_box_conj [try_rewrite]
988    elim!: mp intro!: InitDmd [temp_use] 3 [THEN STL4, temp_use])
989  done
990
991lemma SF2:
992  assumes 1: "\<turnstile> N \<and> <B>_f \<longrightarrow> <M>_g"
993    and 2: "\<turnstile> $P \<and> P` \<and> <N \<and> A>_f \<longrightarrow> B"
994    and 3: "\<turnstile> P \<and> Enabled(<M>_g) \<longrightarrow> Enabled(<A>_f)"
995    and 4: "\<turnstile> \<box>(N \<and> [\<not>B]_f) \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled(<M>_g) \<longrightarrow> \<diamond>\<box>P"
996  shows "\<turnstile> \<box>N \<and> SF(A)_f \<and> \<box>F \<longrightarrow> SF(M)_g"
997  apply (clarsimp dest!: BoxSFI [temp_use] simp: 2 [try_rewrite] SF_def [where A = M])
998  apply (erule_tac F = F in dup_boxE)
999  apply (erule_tac F = "TEMP \<diamond>Enabled (<M>_g) " in dup_boxE)
1000  apply merge_temp_box
1001  apply (erule STL4Edup)
1002   apply assumption
1003  apply (clarsimp intro!: BoxDmd_simple [temp_use, THEN 1 [THEN DmdImpl, temp_use]])
1004  apply (rule classical)
1005  apply (subgoal_tac "sigmaa \<Turnstile> \<diamond> (($P \<and> P` \<and> N) \<and> <A>_f)")
1006   apply (force simp: angle_def intro!: 2 [temp_use] elim!: DmdImplE [temp_use])
1007  apply (rule BoxDmd_simple [THEN DmdImpl, unfolded DmdDmd [temp_rewrite], temp_use])
1008  apply (simp add: NotDmd [temp_use] not_angle [try_rewrite])
1009  apply merge_act_box
1010  apply (frule 4 [temp_use])
1011     apply assumption+
1012  apply (erule_tac V = "sigmaa \<Turnstile> \<box>F" in thin_rl)
1013  apply (drule BoxSFI [temp_use])
1014  apply (erule_tac F = "TEMP \<diamond>Enabled (<M>_g)" in dup_boxE)
1015  apply (erule_tac F = "ACT N \<and> [\<not>B]_f" in dup_boxE)
1016  apply merge_temp_box
1017  apply (erule DmdImpldup)
1018   apply assumption
1019  apply (auto simp: split_box_conj [try_rewrite] STL3 [try_rewrite]
1020    SF_Box [try_rewrite] box_stp_act [try_rewrite])
1021   apply (force elim!: TLA2E [where P = P, temp_use])
1022  apply (rule STL2 [temp_use])
1023  apply (force simp: SF_def split_box_conj [try_rewrite]
1024    elim!: mp InfImpl [temp_use] intro!: 3 [temp_use])
1025  done
1026
1027(* ------------------------------------------------------------------------- *)
1028(***           Liveness proofs by well-founded orderings                   ***)
1029(* ------------------------------------------------------------------------- *)
1030section "Well-founded orderings"
1031
1032lemma wf_leadsto:
1033  assumes 1: "wf r"
1034    and 2: "\<And>x. sigma \<Turnstile> F x \<leadsto> (G \<or> (\<exists>y. #((y,x)\<in>r) \<and> F y))    "
1035  shows "sigma \<Turnstile> F x \<leadsto> G"
1036  apply (rule 1 [THEN wf_induct])
1037  apply (rule LatticeTriangle [temp_use])
1038   apply (rule 2)
1039  apply (auto simp: leadsto_exists [try_rewrite])
1040  apply (case_tac "(y,x) \<in> r")
1041   apply force
1042  apply (force simp: leadsto_def Init_simps intro!: necT [temp_use])
1043  done
1044
1045(* If r is well-founded, state function v cannot decrease forever *)
1046lemma wf_not_box_decrease: "\<And>r. wf r \<Longrightarrow> \<turnstile> \<box>[ (v`, $v) \<in> #r ]_v \<longrightarrow> \<diamond>\<box>[#False]_v"
1047  apply clarsimp
1048  apply (rule ccontr)
1049  apply (subgoal_tac "sigma \<Turnstile> (\<exists>x. v=#x) \<leadsto> #False")
1050   apply (drule leadsto_false [temp_use, THEN iffD1, THEN STL2_gen [temp_use]])
1051   apply (force simp: Init_defs)
1052  apply (clarsimp simp: leadsto_exists [try_rewrite] not_square [try_rewrite] more_temp_simps)
1053  apply (erule wf_leadsto)
1054  apply (rule ensures_simple [temp_use])
1055   apply (auto simp: square_def angle_def)
1056  done
1057
1058(* "wf r  \<Longrightarrow>  \<turnstile> \<diamond>\<box>[ (v`, $v) : #r ]_v \<longrightarrow> \<diamond>\<box>[#False]_v" *)
1059lemmas wf_not_dmd_box_decrease =
1060  wf_not_box_decrease [THEN DmdImpl, unfolded more_temp_simps]
1061
1062(* If there are infinitely many steps where v decreases, then there
1063   have to be infinitely many non-stuttering steps where v doesn't decrease.
1064*)
1065lemma wf_box_dmd_decrease:
1066  assumes 1: "wf r"
1067  shows "\<turnstile> \<box>\<diamond>((v`, $v) \<in> #r) \<longrightarrow> \<box>\<diamond><(v`, $v) \<notin> #r>_v"
1068  apply clarsimp
1069  apply (rule ccontr)
1070  apply (simp add: not_angle [try_rewrite] more_temp_simps)
1071  apply (drule 1 [THEN wf_not_dmd_box_decrease [temp_use]])
1072  apply (drule BoxDmdDmdBox [temp_use])
1073   apply assumption
1074  apply (subgoal_tac "sigma \<Turnstile> \<box>\<diamond> ((#False) ::action)")
1075   apply force
1076  apply (erule STL4E)
1077  apply (rule DmdImpl)
1078  apply (force intro: 1 [THEN wf_irrefl, temp_use])
1079  done
1080
1081(* In particular, for natural numbers, if n decreases infinitely often
1082   then it has to increase infinitely often.
1083*)
1084lemma nat_box_dmd_decrease: "\<And>n::nat stfun. \<turnstile> \<box>\<diamond>(n` < $n) \<longrightarrow> \<box>\<diamond>($n < n`)"
1085  apply clarsimp
1086  apply (subgoal_tac "sigma \<Turnstile> \<box>\<diamond><\<not> ((n`,$n) \<in> #less_than)>_n")
1087   apply (erule thin_rl)
1088   apply (erule STL4E)
1089   apply (rule DmdImpl)
1090   apply (clarsimp simp: angle_def [try_rewrite])
1091  apply (rule wf_box_dmd_decrease [temp_use])
1092   apply (auto elim!: STL4E [temp_use] DmdImplE [temp_use])
1093  done
1094
1095
1096(* ------------------------------------------------------------------------- *)
1097(***           Flexible quantification over state variables                ***)
1098(* ------------------------------------------------------------------------- *)
1099section "Flexible quantification"
1100
1101lemma aallI:
1102  assumes 1: "basevars vs"
1103    and 2: "(\<And>x. basevars (x,vs) \<Longrightarrow> sigma \<Turnstile> F x)"
1104  shows "sigma \<Turnstile> (\<forall>\<forall>x. F x)"
1105  by (auto simp: aall_def elim!: eexE [temp_use] intro!: 1 dest!: 2 [temp_use])
1106
1107lemma aallE: "\<turnstile> (\<forall>\<forall>x. F x) \<longrightarrow> F x"
1108  apply (unfold aall_def)
1109  apply clarsimp
1110  apply (erule contrapos_np)
1111  apply (force intro!: eexI [temp_use])
1112  done
1113
1114(* monotonicity of quantification *)
1115lemma eex_mono:
1116  assumes 1: "sigma \<Turnstile> \<exists>\<exists>x. F x"
1117    and 2: "\<And>x. sigma \<Turnstile> F x \<longrightarrow> G x"
1118  shows "sigma \<Turnstile> \<exists>\<exists>x. G x"
1119  apply (rule unit_base [THEN 1 [THEN eexE]])
1120  apply (rule eexI [temp_use])
1121  apply (erule 2 [unfolded intensional_rews, THEN mp])
1122  done
1123
1124lemma aall_mono:
1125  assumes 1: "sigma \<Turnstile> \<forall>\<forall>x. F(x)"
1126    and 2: "\<And>x. sigma \<Turnstile> F(x) \<longrightarrow> G(x)"
1127  shows "sigma \<Turnstile> \<forall>\<forall>x. G(x)"
1128  apply (rule unit_base [THEN aallI])
1129  apply (rule 2 [unfolded intensional_rews, THEN mp])
1130  apply (rule 1 [THEN aallE [temp_use]])
1131  done
1132
1133(* Derived history introduction rule *)
1134lemma historyI:
1135  assumes 1: "sigma \<Turnstile> Init I"
1136    and 2: "sigma \<Turnstile> \<box>N"
1137    and 3: "basevars vs"
1138    and 4: "\<And>h. basevars(h,vs) \<Longrightarrow> \<turnstile> I \<and> h = ha \<longrightarrow> HI h"
1139    and 5: "\<And>h s t. \<lbrakk> basevars(h,vs); N (s,t); h t = hb (h s) (s,t) \<rbrakk> \<Longrightarrow> HN h (s,t)"
1140  shows "sigma \<Turnstile> \<exists>\<exists>h. Init (HI h) \<and> \<box>(HN h)"
1141  apply (rule history [temp_use, THEN eexE])
1142  apply (rule 3)
1143  apply (rule eexI [temp_use])
1144  apply clarsimp
1145  apply (rule conjI)
1146   prefer 2
1147   apply (insert 2)
1148   apply merge_box
1149   apply (force elim!: STL4E [temp_use] 5 [temp_use])
1150  apply (insert 1)
1151  apply (force simp: Init_defs elim!: 4 [temp_use])
1152  done
1153
1154(* ----------------------------------------------------------------------
1155   example of a history variable: existence of a clock
1156*)
1157
1158lemma "\<turnstile> \<exists>\<exists>h. Init(h = #True) \<and> \<box>(h` = (\<not>$h))"
1159  apply (rule tempI)
1160  apply (rule historyI)
1161  apply (force simp: Init_defs intro!: unit_base [temp_use] necT [temp_use])+
1162  done
1163
1164end
1165