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