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