author | wenzelm |
Wed, 07 Sep 2005 20:22:39 +0200 | |
changeset 17309 | c43ed29bd197 |
parent 14100 | 804be4c4b642 |
permissions | -rw-r--r-- |
17309 | 1 |
(* |
2 |
File: Action.ML |
|
3 |
ID: $Id$ |
|
3807 | 4 |
Author: Stephan Merz |
5 |
Copyright: 1997 University of Munich |
|
6 |
||
7 |
Lemmas and tactics for TLA actions. |
|
8 |
*) |
|
9 |
||
17309 | 10 |
(* The following assertion specializes "intI" for any world type |
6255 | 11 |
which is a pair, not just for "state * state". |
12 |
*) |
|
17309 | 13 |
val [prem] = goal (the_context ()) "(!!s t. (s,t) |= A) ==> |- A"; |
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
14 |
by (REPEAT (resolve_tac [prem,intI,prod_induct] 1)); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
15 |
qed "actionI"; |
6255 | 16 |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
17 |
Goal "|- A ==> (s,t) |= A"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
18 |
by (etac intD 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
19 |
qed "actionD"; |
6255 | 20 |
|
21 |
local |
|
17309 | 22 |
fun prover s = prove_goal (the_context ()) s |
23 |
(fn _ => [rtac actionI 1, |
|
6255 | 24 |
rewrite_goals_tac (unl_after::intensional_rews), |
25 |
rtac refl 1]) |
|
26 |
in |
|
27 |
val pr_rews = map (int_rewrite o prover) |
|
28 |
[ "|- (#c)` = #c", |
|
14100 | 29 |
"|- f<x>` = f<x` >", |
30 |
"|- f<x,y>` = f<x`,y` >", |
|
31 |
"|- f<x,y,z>` = f<x`,y`,z` >", |
|
6255 | 32 |
"|- (! x. P x)` = (! x. (P x)`)", |
33 |
"|- (? x. P x)` = (? x. (P x)`)" |
|
34 |
] |
|
35 |
end; |
|
36 |
||
37 |
val act_rews = [unl_before,unl_after,unchanged_def] @ pr_rews; |
|
38 |
Addsimps act_rews; |
|
3807 | 39 |
|
40 |
val action_rews = act_rews @ intensional_rews; |
|
41 |
||
42 |
(* ================ Functions to "unlift" action theorems into HOL rules ================ *) |
|
43 |
||
6255 | 44 |
(* The following functions are specialized versions of the corresponding |
45 |
functions defined in Intensional.ML in that they introduce a |
|
46 |
"world" parameter of the form (s,t) and apply additional rewrites. |
|
3807 | 47 |
*) |
17309 | 48 |
fun action_unlift th = |
49 |
(rewrite_rule action_rews (th RS actionD)) |
|
6255 | 50 |
handle _ => int_unlift th; |
3807 | 51 |
|
6255 | 52 |
(* Turn |- A = B into meta-level rewrite rule A == B *) |
53 |
val action_rewrite = int_rewrite; |
|
3807 | 54 |
|
6255 | 55 |
fun action_use th = |
56 |
case (concl_of th) of |
|
57 |
Const _ $ (Const ("Intensional.Valid", _) $ _) => |
|
58 |
((flatten (action_unlift th)) handle _ => th) |
|
59 |
| _ => th; |
|
3807 | 60 |
|
61 |
(* ===================== Update simpset and classical prover ============================= *) |
|
62 |
||
6255 | 63 |
AddSIs [actionI]; |
64 |
AddDs [actionD]; |
|
3807 | 65 |
|
66 |
(* =========================== square / angle brackets =========================== *) |
|
67 |
||
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
68 |
Goalw [square_def] "(s,t) |= unchanged v ==> (s,t) |= [A]_v"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
69 |
by (Asm_full_simp_tac 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
70 |
qed "idle_squareI"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
71 |
|
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
72 |
Goalw [square_def] "(s,t) |= A ==> (s,t) |= [A]_v"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
73 |
by (Asm_simp_tac 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
74 |
qed "busy_squareI"; |
3807 | 75 |
|
17309 | 76 |
val prems = goal (the_context ()) |
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
77 |
"[| (s,t) |= [A]_v; A (s,t) ==> B (s,t); v t = v s ==> B (s,t) |] ==> B (s,t)"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
78 |
by (cut_facts_tac prems 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
79 |
by (rewrite_goals_tac (square_def::action_rews)); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
80 |
by (etac disjE 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
81 |
by (REPEAT (eresolve_tac prems 1)); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
82 |
qed "squareE"; |
6255 | 83 |
|
17309 | 84 |
val prems = goalw (the_context ()) (square_def::action_rews) |
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
85 |
"[| v t ~= v s ==> A (s,t) |] ==> (s,t) |= [A]_v"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
86 |
by (rtac disjCI 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
87 |
by (eresolve_tac prems 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
88 |
qed "squareCI"; |
6255 | 89 |
|
17309 | 90 |
goalw (the_context ()) [angle_def] |
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
91 |
"!!s t. [| A (s,t); v t ~= v s |] ==> (s,t) |= <A>_v"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
92 |
by (Asm_simp_tac 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
93 |
qed "angleI"; |
3807 | 94 |
|
17309 | 95 |
val prems = goalw (the_context ()) (angle_def::action_rews) |
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
96 |
"[| (s,t) |= <A>_v; [| A (s,t); v t ~= v s |] ==> R |] ==> R"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
97 |
by (cut_facts_tac prems 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
98 |
by (etac conjE 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
99 |
by (REPEAT (ares_tac prems 1)); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
100 |
qed "angleE"; |
6255 | 101 |
|
102 |
AddIs [angleI, squareCI]; |
|
103 |
AddEs [angleE, squareE]; |
|
104 |
||
17309 | 105 |
goal (the_context ()) |
6255 | 106 |
"!!f. [| |- unchanged f & ~B --> unchanged g; \ |
107 |
\ |- A & ~unchanged g --> B \ |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
108 |
\ |] ==> |- [A]_f --> [B]_g"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
109 |
by (Clarsimp_tac 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
110 |
by (etac squareE 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
111 |
by (auto_tac (claset(), simpset() addsimps [square_def])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
112 |
qed "square_simulation"; |
6255 | 113 |
|
17309 | 114 |
goalw (the_context ()) [square_def,angle_def] |
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
115 |
"|- (~ [A]_v) = <~A>_v"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
116 |
by Auto_tac; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
117 |
qed "not_square"; |
3807 | 118 |
|
17309 | 119 |
goalw (the_context ()) [square_def,angle_def] |
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
120 |
"|- (~ <A>_v) = [~A]_v"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
121 |
by Auto_tac; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
122 |
qed "not_angle"; |
3807 | 123 |
|
124 |
(* ============================== Facts about ENABLED ============================== *) |
|
125 |
||
17309 | 126 |
goal (the_context ()) "|- A --> $Enabled A"; |
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
127 |
by (auto_tac (claset(), simpset() addsimps [enabled_def])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
128 |
qed "enabledI"; |
3807 | 129 |
|
17309 | 130 |
val prems = goalw (the_context ()) [enabled_def] |
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
131 |
"[| s |= Enabled A; !!u. A (s,u) ==> Q |] ==> Q"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
132 |
by (cut_facts_tac prems 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
133 |
by (etac exE 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
134 |
by (resolve_tac prems 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
135 |
by (atac 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
136 |
qed "enabledE"; |
3807 | 137 |
|
17309 | 138 |
goal (the_context ()) "|- ~$Enabled G --> ~ G"; |
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
139 |
by (auto_tac (claset(), simpset() addsimps [enabled_def])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
140 |
qed "notEnabledD"; |
3807 | 141 |
|
142 |
(* Monotonicity *) |
|
17309 | 143 |
val [min,maj] = goal (the_context ()) |
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
144 |
"[| s |= Enabled F; |- F --> G |] ==> s |= Enabled G"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
145 |
by (rtac (min RS enabledE) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
146 |
by (rtac (action_use enabledI) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
147 |
by (etac (action_use maj) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
148 |
qed "enabled_mono"; |
3807 | 149 |
|
150 |
(* stronger variant *) |
|
17309 | 151 |
val [min,maj] = goal (the_context ()) |
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
152 |
"[| s |= Enabled F; !!t. F (s,t) ==> G (s,t) |] ==> s |= Enabled G"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
153 |
by (rtac (min RS enabledE) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
154 |
by (rtac (action_use enabledI) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
155 |
by (etac maj 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
156 |
qed "enabled_mono2"; |
3807 | 157 |
|
17309 | 158 |
goal (the_context ()) "|- Enabled F --> Enabled (F | G)"; |
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
159 |
by (auto_tac (claset() addSEs [enabled_mono], simpset())); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
160 |
qed "enabled_disj1"; |
3807 | 161 |
|
17309 | 162 |
goal (the_context ()) "|- Enabled G --> Enabled (F | G)"; |
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
163 |
by (auto_tac (claset() addSEs [enabled_mono], simpset())); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
164 |
qed "enabled_disj2"; |
3807 | 165 |
|
17309 | 166 |
goal (the_context ()) "|- Enabled (F & G) --> Enabled F"; |
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
167 |
by (auto_tac (claset() addSEs [enabled_mono], simpset())); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
168 |
qed "enabled_conj1"; |
3807 | 169 |
|
17309 | 170 |
goal (the_context ()) "|- Enabled (F & G) --> Enabled G"; |
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
171 |
by (auto_tac (claset() addSEs [enabled_mono], simpset())); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
172 |
qed "enabled_conj2"; |
3807 | 173 |
|
17309 | 174 |
val prems = goal (the_context ()) |
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
175 |
"[| s |= Enabled (F & G); [| s |= Enabled F; s |= Enabled G |] ==> Q |] ==> Q"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
176 |
by (cut_facts_tac prems 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
177 |
by (resolve_tac prems 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
178 |
by (etac (action_use enabled_conj1) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
179 |
by (etac (action_use enabled_conj2) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
180 |
qed "enabled_conjE"; |
3807 | 181 |
|
17309 | 182 |
goal (the_context ()) "|- Enabled (F | G) --> Enabled F | Enabled G"; |
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
183 |
by (auto_tac (claset(), simpset() addsimps [enabled_def])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
184 |
qed "enabled_disjD"; |
3807 | 185 |
|
17309 | 186 |
goal (the_context ()) "|- Enabled (F | G) = (Enabled F | Enabled G)"; |
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
187 |
by (Clarsimp_tac 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
188 |
by (rtac iffI 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
189 |
by (etac (action_use enabled_disjD) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
190 |
by (REPEAT (eresolve_tac (disjE::map action_use [enabled_disj1,enabled_disj2]) 1)); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
191 |
qed "enabled_disj"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
192 |
|
17309 | 193 |
goal (the_context ()) "|- Enabled (EX x. F x) = (EX x. Enabled (F x))"; |
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
194 |
by (force_tac (claset(), simpset() addsimps [enabled_def]) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
195 |
qed "enabled_ex"; |
6255 | 196 |
|
3807 | 197 |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
198 |
(* A rule that combines enabledI and baseE, but generates fewer instantiations *) |
17309 | 199 |
val prems = goal (the_context ()) |
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
200 |
"[| basevars vs; EX c. ! u. vs u = c --> A(s,u) |] ==> s |= Enabled A"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
201 |
by (cut_facts_tac prems 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
202 |
by (etac exE 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
203 |
by (etac baseE 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
204 |
by (rtac (action_use enabledI) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
205 |
by (etac allE 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
206 |
by (etac mp 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
207 |
by (atac 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
208 |
qed "base_enabled"; |
3807 | 209 |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
210 |
(* ======================= action_simp_tac ============================== *) |
6255 | 211 |
|
212 |
(* A dumb simplification-based tactic with just a little first-order logic: |
|
213 |
should plug in only "very safe" rules that can be applied blindly. |
|
214 |
Note that it applies whatever simplifications are currently active. |
|
215 |
*) |
|
216 |
fun action_simp_tac ss intros elims = |
|
17309 | 217 |
asm_full_simp_tac |
6255 | 218 |
(ss setloop ((resolve_tac ((map action_use intros) |
219 |
@ [refl,impI,conjI,actionI,intI,allI])) |
|
17309 | 220 |
ORELSE' (eresolve_tac ((map action_use elims) |
6255 | 221 |
@ [conjE,disjE,exE])))); |
222 |
||
223 |
(* default version without additional plug-in rules *) |
|
224 |
val Action_simp_tac = action_simp_tac (simpset()) [] []; |
|
225 |
||
226 |
||
227 |
||
3807 | 228 |
(* ---------------- enabled_tac: tactic to prove (Enabled A) -------------------- *) |
229 |
(* "Enabled A" can be proven as follows: |
|
230 |
- Assume that we know which state variables are "base variables"; |
|
6255 | 231 |
this should be expressed by a theorem of the form "basevars (x,y,z,...)". |
3807 | 232 |
- Resolve this theorem with baseE to introduce a constant for the value of the |
233 |
variables in the successor state, and resolve the goal with the result. |
|
234 |
- Resolve with enabledI and do some rewriting. |
|
235 |
- Solve for the unknowns using standard HOL reasoning. |
|
236 |
The following tactic combines these steps except the final one. |
|
237 |
*) |
|
238 |
||
6255 | 239 |
fun enabled_tac base_vars = |
240 |
clarsimp_tac (claset() addSIs [base_vars RS base_enabled], simpset()); |
|
3807 | 241 |
|
6255 | 242 |
(* Example: |
243 |
||
17309 | 244 |
val [prem] = goal (the_context ()) "basevars (x,y,z) ==> |- x --> Enabled ($x & (y$ = #False))"; |
6255 | 245 |
by (enabled_tac prem 1); |
6301 | 246 |
by Auto_tac; |
3807 | 247 |
|
248 |
*) |