1 (* |
|
2 File: Action.ML |
|
3 ID: $Id$ |
|
4 Author: Stephan Merz |
|
5 Copyright: 1997 University of Munich |
|
6 |
|
7 Lemmas and tactics for TLA actions. |
|
8 *) |
|
9 |
|
10 (* The following assertion specializes "intI" for any world type |
|
11 which is a pair, not just for "state * state". |
|
12 *) |
|
13 val [prem] = goal (the_context ()) "(!!s t. (s,t) |= A) ==> |- A"; |
|
14 by (REPEAT (resolve_tac [prem,intI,prod_induct] 1)); |
|
15 qed "actionI"; |
|
16 |
|
17 Goal "|- A ==> (s,t) |= A"; |
|
18 by (etac intD 1); |
|
19 qed "actionD"; |
|
20 |
|
21 local |
|
22 fun prover s = prove_goal (the_context ()) s |
|
23 (fn _ => [rtac actionI 1, |
|
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", |
|
29 "|- f<x>` = f<x` >", |
|
30 "|- f<x,y>` = f<x`,y` >", |
|
31 "|- f<x,y,z>` = f<x`,y`,z` >", |
|
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; |
|
39 |
|
40 val action_rews = act_rews @ intensional_rews; |
|
41 |
|
42 (* ================ Functions to "unlift" action theorems into HOL rules ================ *) |
|
43 |
|
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. |
|
47 *) |
|
48 fun action_unlift th = |
|
49 (rewrite_rule action_rews (th RS actionD)) |
|
50 handle _ => int_unlift th; |
|
51 |
|
52 (* Turn |- A = B into meta-level rewrite rule A == B *) |
|
53 val action_rewrite = int_rewrite; |
|
54 |
|
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; |
|
60 |
|
61 (* ===================== Update simpset and classical prover ============================= *) |
|
62 |
|
63 AddSIs [actionI]; |
|
64 AddDs [actionD]; |
|
65 |
|
66 (* =========================== square / angle brackets =========================== *) |
|
67 |
|
68 Goalw [square_def] "(s,t) |= unchanged v ==> (s,t) |= [A]_v"; |
|
69 by (Asm_full_simp_tac 1); |
|
70 qed "idle_squareI"; |
|
71 |
|
72 Goalw [square_def] "(s,t) |= A ==> (s,t) |= [A]_v"; |
|
73 by (Asm_simp_tac 1); |
|
74 qed "busy_squareI"; |
|
75 |
|
76 val prems = goal (the_context ()) |
|
77 "[| (s,t) |= [A]_v; A (s,t) ==> B (s,t); v t = v s ==> B (s,t) |] ==> B (s,t)"; |
|
78 by (cut_facts_tac prems 1); |
|
79 by (rewrite_goals_tac (square_def::action_rews)); |
|
80 by (etac disjE 1); |
|
81 by (REPEAT (eresolve_tac prems 1)); |
|
82 qed "squareE"; |
|
83 |
|
84 val prems = goalw (the_context ()) (square_def::action_rews) |
|
85 "[| v t ~= v s ==> A (s,t) |] ==> (s,t) |= [A]_v"; |
|
86 by (rtac disjCI 1); |
|
87 by (eresolve_tac prems 1); |
|
88 qed "squareCI"; |
|
89 |
|
90 goalw (the_context ()) [angle_def] |
|
91 "!!s t. [| A (s,t); v t ~= v s |] ==> (s,t) |= <A>_v"; |
|
92 by (Asm_simp_tac 1); |
|
93 qed "angleI"; |
|
94 |
|
95 val prems = goalw (the_context ()) (angle_def::action_rews) |
|
96 "[| (s,t) |= <A>_v; [| A (s,t); v t ~= v s |] ==> R |] ==> R"; |
|
97 by (cut_facts_tac prems 1); |
|
98 by (etac conjE 1); |
|
99 by (REPEAT (ares_tac prems 1)); |
|
100 qed "angleE"; |
|
101 |
|
102 AddIs [angleI, squareCI]; |
|
103 AddEs [angleE, squareE]; |
|
104 |
|
105 goal (the_context ()) |
|
106 "!!f. [| |- unchanged f & ~B --> unchanged g; \ |
|
107 \ |- A & ~unchanged g --> B \ |
|
108 \ |] ==> |- [A]_f --> [B]_g"; |
|
109 by (Clarsimp_tac 1); |
|
110 by (etac squareE 1); |
|
111 by (auto_tac (claset(), simpset() addsimps [square_def])); |
|
112 qed "square_simulation"; |
|
113 |
|
114 goalw (the_context ()) [square_def,angle_def] |
|
115 "|- (~ [A]_v) = <~A>_v"; |
|
116 by Auto_tac; |
|
117 qed "not_square"; |
|
118 |
|
119 goalw (the_context ()) [square_def,angle_def] |
|
120 "|- (~ <A>_v) = [~A]_v"; |
|
121 by Auto_tac; |
|
122 qed "not_angle"; |
|
123 |
|
124 (* ============================== Facts about ENABLED ============================== *) |
|
125 |
|
126 goal (the_context ()) "|- A --> $Enabled A"; |
|
127 by (auto_tac (claset(), simpset() addsimps [enabled_def])); |
|
128 qed "enabledI"; |
|
129 |
|
130 val prems = goalw (the_context ()) [enabled_def] |
|
131 "[| s |= Enabled A; !!u. A (s,u) ==> Q |] ==> Q"; |
|
132 by (cut_facts_tac prems 1); |
|
133 by (etac exE 1); |
|
134 by (resolve_tac prems 1); |
|
135 by (atac 1); |
|
136 qed "enabledE"; |
|
137 |
|
138 goal (the_context ()) "|- ~$Enabled G --> ~ G"; |
|
139 by (auto_tac (claset(), simpset() addsimps [enabled_def])); |
|
140 qed "notEnabledD"; |
|
141 |
|
142 (* Monotonicity *) |
|
143 val [min,maj] = goal (the_context ()) |
|
144 "[| s |= Enabled F; |- F --> G |] ==> s |= Enabled G"; |
|
145 by (rtac (min RS enabledE) 1); |
|
146 by (rtac (action_use enabledI) 1); |
|
147 by (etac (action_use maj) 1); |
|
148 qed "enabled_mono"; |
|
149 |
|
150 (* stronger variant *) |
|
151 val [min,maj] = goal (the_context ()) |
|
152 "[| s |= Enabled F; !!t. F (s,t) ==> G (s,t) |] ==> s |= Enabled G"; |
|
153 by (rtac (min RS enabledE) 1); |
|
154 by (rtac (action_use enabledI) 1); |
|
155 by (etac maj 1); |
|
156 qed "enabled_mono2"; |
|
157 |
|
158 goal (the_context ()) "|- Enabled F --> Enabled (F | G)"; |
|
159 by (auto_tac (claset() addSEs [enabled_mono], simpset())); |
|
160 qed "enabled_disj1"; |
|
161 |
|
162 goal (the_context ()) "|- Enabled G --> Enabled (F | G)"; |
|
163 by (auto_tac (claset() addSEs [enabled_mono], simpset())); |
|
164 qed "enabled_disj2"; |
|
165 |
|
166 goal (the_context ()) "|- Enabled (F & G) --> Enabled F"; |
|
167 by (auto_tac (claset() addSEs [enabled_mono], simpset())); |
|
168 qed "enabled_conj1"; |
|
169 |
|
170 goal (the_context ()) "|- Enabled (F & G) --> Enabled G"; |
|
171 by (auto_tac (claset() addSEs [enabled_mono], simpset())); |
|
172 qed "enabled_conj2"; |
|
173 |
|
174 val prems = goal (the_context ()) |
|
175 "[| s |= Enabled (F & G); [| s |= Enabled F; s |= Enabled G |] ==> Q |] ==> Q"; |
|
176 by (cut_facts_tac prems 1); |
|
177 by (resolve_tac prems 1); |
|
178 by (etac (action_use enabled_conj1) 1); |
|
179 by (etac (action_use enabled_conj2) 1); |
|
180 qed "enabled_conjE"; |
|
181 |
|
182 goal (the_context ()) "|- Enabled (F | G) --> Enabled F | Enabled G"; |
|
183 by (auto_tac (claset(), simpset() addsimps [enabled_def])); |
|
184 qed "enabled_disjD"; |
|
185 |
|
186 goal (the_context ()) "|- Enabled (F | G) = (Enabled F | Enabled G)"; |
|
187 by (Clarsimp_tac 1); |
|
188 by (rtac iffI 1); |
|
189 by (etac (action_use enabled_disjD) 1); |
|
190 by (REPEAT (eresolve_tac (disjE::map action_use [enabled_disj1,enabled_disj2]) 1)); |
|
191 qed "enabled_disj"; |
|
192 |
|
193 goal (the_context ()) "|- Enabled (EX x. F x) = (EX x. Enabled (F x))"; |
|
194 by (force_tac (claset(), simpset() addsimps [enabled_def]) 1); |
|
195 qed "enabled_ex"; |
|
196 |
|
197 |
|
198 (* A rule that combines enabledI and baseE, but generates fewer instantiations *) |
|
199 val prems = goal (the_context ()) |
|
200 "[| basevars vs; EX c. ! u. vs u = c --> A(s,u) |] ==> s |= Enabled A"; |
|
201 by (cut_facts_tac prems 1); |
|
202 by (etac exE 1); |
|
203 by (etac baseE 1); |
|
204 by (rtac (action_use enabledI) 1); |
|
205 by (etac allE 1); |
|
206 by (etac mp 1); |
|
207 by (atac 1); |
|
208 qed "base_enabled"; |
|
209 |
|
210 (* ======================= action_simp_tac ============================== *) |
|
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 = |
|
217 asm_full_simp_tac |
|
218 (ss setloop ((resolve_tac ((map action_use intros) |
|
219 @ [refl,impI,conjI,actionI,intI,allI])) |
|
220 ORELSE' (eresolve_tac ((map action_use elims) |
|
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 |
|
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"; |
|
231 this should be expressed by a theorem of the form "basevars (x,y,z,...)". |
|
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 |
|
239 fun enabled_tac base_vars = |
|
240 clarsimp_tac (claset() addSIs [base_vars RS base_enabled], simpset()); |
|
241 |
|
242 (* Example: |
|
243 |
|
244 val [prem] = goal (the_context ()) "basevars (x,y,z) ==> |- x --> Enabled ($x & (y$ = #False))"; |
|
245 by (enabled_tac prem 1); |
|
246 by Auto_tac; |
|
247 |
|
248 *) |
|