3807
|
1 |
(*
|
|
2 |
File: IntLemmas.ML
|
|
3 |
Author: Stephan Merz
|
|
4 |
Copyright: 1997 University of Munich
|
|
5 |
|
|
6 |
Lemmas and tactics for "intensional" logics.
|
|
7 |
|
|
8 |
Mostly a lifting of standard HOL lemmas. They are not required in standard
|
|
9 |
reasoning about intensional logics, which starts by unlifting proof goals
|
|
10 |
to the HOL level.
|
|
11 |
*)
|
|
12 |
|
|
13 |
|
|
14 |
qed_goal "substW" Intensional.thy
|
|
15 |
"[| x .= y; w |= (P::[('v::world) => 'a, 'w::world] => bool)(x) |] ==> w |= P(y)"
|
|
16 |
(fn [prem1,prem2] => [rtac (rewrite_rule ([prem1] RL [inteq_reflection]) prem2) 1]);
|
|
17 |
|
|
18 |
|
|
19 |
(* Lift HOL rules to intensional reasoning *)
|
|
20 |
|
|
21 |
qed_goal "reflW" Intensional.thy "x .= x"
|
|
22 |
(fn _ => [ rtac intI 1,
|
|
23 |
rewrite_goals_tac intensional_rews,
|
|
24 |
rtac refl 1 ]);
|
|
25 |
|
|
26 |
|
|
27 |
qed_goal "symW" Intensional.thy "s .= t ==> t .= s"
|
|
28 |
(fn prems => [ cut_facts_tac prems 1,
|
|
29 |
rtac intI 1, dtac intD 1,
|
|
30 |
rewrite_goals_tac intensional_rews,
|
|
31 |
etac sym 1 ]);
|
|
32 |
|
|
33 |
qed_goal "not_symW" Intensional.thy "s .~= t ==> t .~= s"
|
|
34 |
(fn prems => [ cut_facts_tac prems 1,
|
|
35 |
rtac intI 1, dtac intD 1,
|
|
36 |
rewrite_goals_tac intensional_rews,
|
|
37 |
etac not_sym 1 ]);
|
|
38 |
|
|
39 |
qed_goal "transW" Intensional.thy
|
|
40 |
"[| r .= s; s .= t |] ==> r .= t"
|
|
41 |
(fn prems => [ cut_facts_tac prems 1,
|
|
42 |
rtac intI 1, REPEAT (dtac intD 1),
|
|
43 |
rewrite_goals_tac intensional_rews,
|
|
44 |
etac trans 1,
|
|
45 |
atac 1 ]);
|
|
46 |
|
|
47 |
qed_goal "box_equalsW" Intensional.thy
|
|
48 |
"[| a .= b; a .= c; b .= d |] ==> c .= d"
|
|
49 |
(fn prems => [ (rtac transW 1),
|
|
50 |
(rtac transW 1),
|
|
51 |
(rtac symW 1),
|
|
52 |
(REPEAT (resolve_tac prems 1)) ]);
|
|
53 |
|
|
54 |
|
|
55 |
qed_goal "fun_congW" Intensional.thy
|
|
56 |
"(f::('a => 'b)) = g ==> f[x] .= g[x]"
|
|
57 |
(fn prems => [ cut_facts_tac prems 1,
|
|
58 |
rtac intI 1,
|
|
59 |
rewrite_goals_tac intensional_rews,
|
|
60 |
etac fun_cong 1 ]);
|
|
61 |
|
|
62 |
qed_goal "fun_cong2W" Intensional.thy
|
|
63 |
"(f::(['a,'b] => 'c)) = g ==> f[x,y] .= g[x,y]"
|
|
64 |
(fn prems => [ cut_facts_tac prems 1,
|
|
65 |
rtac intI 1,
|
|
66 |
rewrite_goals_tac intensional_rews,
|
|
67 |
asm_full_simp_tac HOL_ss 1 ]);
|
|
68 |
|
|
69 |
qed_goal "fun_cong3W" Intensional.thy
|
|
70 |
"(f::(['a,'b,'c] => 'd)) = g ==> f[x,y,z] .= g[x,y,z]"
|
|
71 |
(fn prems => [ cut_facts_tac prems 1,
|
|
72 |
rtac intI 1,
|
|
73 |
rewrite_goals_tac intensional_rews,
|
|
74 |
asm_full_simp_tac HOL_ss 1 ]);
|
|
75 |
|
|
76 |
|
|
77 |
qed_goal "arg_congW" Intensional.thy "x .= y ==> (f::'a=>'b)[x] .= f[y]"
|
|
78 |
(fn prems => [ cut_facts_tac prems 1,
|
|
79 |
rtac intI 1,
|
|
80 |
dtac intD 1,
|
|
81 |
rewrite_goals_tac intensional_rews,
|
|
82 |
etac arg_cong 1 ]);
|
|
83 |
|
|
84 |
qed_goal "arg_cong2W" Intensional.thy
|
|
85 |
"[| u .= v; x .= y |] ==> (f::['a,'b]=>'c)[u,x] .= f[v,y]"
|
|
86 |
(fn prems => [ cut_facts_tac prems 1,
|
|
87 |
rtac intI 1,
|
|
88 |
REPEAT (dtac intD 1),
|
|
89 |
rewrite_goals_tac intensional_rews,
|
|
90 |
REPEAT (etac subst 1),
|
|
91 |
rtac refl 1 ]);
|
|
92 |
|
|
93 |
qed_goal "arg_cong3W" Intensional.thy
|
|
94 |
"[| r .= s; u .= v; x .= y |] ==> (f::['a,'b,'c]=>'d)[r,u,x] .= f[s,v,y]"
|
|
95 |
(fn prems => [ cut_facts_tac prems 1,
|
|
96 |
rtac intI 1,
|
|
97 |
REPEAT (dtac intD 1),
|
|
98 |
rewrite_goals_tac intensional_rews,
|
|
99 |
REPEAT (etac subst 1),
|
|
100 |
rtac refl 1 ]);
|
|
101 |
|
|
102 |
qed_goal "congW" Intensional.thy
|
|
103 |
"[| (f::'a=>'b) = g; x .= y |] ==> f[x] .= g[y]"
|
|
104 |
(fn prems => [ rtac box_equalsW 1,
|
|
105 |
rtac reflW 3,
|
|
106 |
rtac arg_congW 1,
|
|
107 |
resolve_tac prems 1,
|
|
108 |
rtac fun_congW 1,
|
|
109 |
rtac sym 1,
|
|
110 |
resolve_tac prems 1 ]);
|
|
111 |
|
|
112 |
qed_goal "cong2W" Intensional.thy
|
|
113 |
"[| (f::['a,'b]=>'c) = g; u .= v; x .= y |] ==> f[u,x] .= g[v,y]"
|
|
114 |
(fn prems => [ rtac box_equalsW 1,
|
|
115 |
rtac reflW 3,
|
|
116 |
rtac arg_cong2W 1,
|
|
117 |
REPEAT (resolve_tac prems 1),
|
|
118 |
rtac fun_cong2W 1,
|
|
119 |
rtac sym 1,
|
|
120 |
resolve_tac prems 1 ]);
|
|
121 |
|
|
122 |
qed_goal "cong3W" Intensional.thy
|
|
123 |
"[| (f::['a,'b,'c]=>'d) = g; r .= s; u .= v; x .= y |] ==> (f[r,u,x]) .= (g[s,v,y])"
|
|
124 |
(fn prems => [ rtac box_equalsW 1,
|
|
125 |
rtac reflW 3,
|
|
126 |
rtac arg_cong3W 1,
|
|
127 |
REPEAT (resolve_tac prems 1),
|
|
128 |
rtac fun_cong3W 1,
|
|
129 |
rtac sym 1,
|
|
130 |
resolve_tac prems 1 ]);
|
|
131 |
|
|
132 |
|
|
133 |
(** Lifted equivalence **)
|
|
134 |
|
|
135 |
(* Note the object-level implication in the hypothesis. Meta-level implication
|
|
136 |
would not be correct! *)
|
|
137 |
qed_goal "iffIW" Intensional.thy
|
|
138 |
"[| A .-> B; B .-> A |] ==> A .= B"
|
|
139 |
(fn prems => [ cut_facts_tac prems 1,
|
|
140 |
rtac intI 1,
|
|
141 |
REPEAT (dtac intD 1),
|
|
142 |
rewrite_goals_tac intensional_rews,
|
|
143 |
(fast_tac prop_cs 1) ]);
|
|
144 |
|
|
145 |
qed_goal "iffD2W" Intensional.thy
|
|
146 |
"[| (P::('w::world) form) .= Q; w |= Q |] ==> w |= P"
|
|
147 |
(fn prems =>
|
|
148 |
[cut_facts_tac prems 1,
|
|
149 |
dtac intD 1,
|
|
150 |
rewrite_goals_tac intensional_rews,
|
|
151 |
fast_tac prop_cs 1 ]);
|
|
152 |
|
|
153 |
val iffD1W = symW RS iffD2W;
|
|
154 |
|
|
155 |
(** #True **)
|
|
156 |
|
|
157 |
qed_goal "TrueIW" Intensional.thy "#True"
|
|
158 |
(fn _ => [rtac intI 1, rewrite_goals_tac intensional_rews, rtac TrueI 1]);
|
|
159 |
|
|
160 |
|
|
161 |
qed_goal "eqTrueIW" Intensional.thy "(P::('w::world) form) ==> P .= #True"
|
|
162 |
(fn prems => [cut_facts_tac prems 1,
|
|
163 |
rtac intI 1,
|
|
164 |
dtac intD 1,
|
|
165 |
rewrite_goals_tac intensional_rews,
|
|
166 |
asm_full_simp_tac HOL_ss 1] );
|
|
167 |
|
|
168 |
qed_goal "eqTrueEW" Intensional.thy "P .= #True ==> (P::('w::world) form)"
|
|
169 |
(fn prems => [cut_facts_tac prems 1,
|
|
170 |
rtac intI 1,
|
|
171 |
dtac intD 1,
|
|
172 |
rewrite_goals_tac intensional_rews,
|
|
173 |
asm_full_simp_tac HOL_ss 1] );
|
|
174 |
|
|
175 |
(** #False **)
|
|
176 |
|
|
177 |
qed_goal "FalseEW" Intensional.thy "#False ==> P::('w::world) form"
|
|
178 |
(fn prems => [cut_facts_tac prems 1,
|
|
179 |
rtac intI 1,
|
|
180 |
dtac intD 1,
|
|
181 |
rewrite_goals_tac intensional_rews,
|
|
182 |
etac FalseE 1]);
|
|
183 |
|
|
184 |
qed_goal "False_neq_TrueW" Intensional.thy
|
|
185 |
"(#False::('w::world) form) .= #True ==> P::('w::world) form"
|
|
186 |
(fn [prem] => [rtac (prem RS eqTrueEW RS FalseEW) 1]);
|
|
187 |
|
|
188 |
|
|
189 |
(** Negation **)
|
|
190 |
|
|
191 |
(* Again use object-level implication *)
|
|
192 |
qed_goal "notIW" Intensional.thy "(P .-> #False) ==> .~P"
|
|
193 |
(fn prems => [cut_facts_tac prems 1,
|
|
194 |
rtac intI 1,
|
|
195 |
dtac intD 1,
|
|
196 |
rewrite_goals_tac intensional_rews,
|
|
197 |
fast_tac prop_cs 1]);
|
|
198 |
|
|
199 |
|
|
200 |
qed_goal "notEWV" Intensional.thy
|
|
201 |
"[| .~P; P::('w::world) form |] ==> R::('w::world) form"
|
|
202 |
(fn prems => [cut_facts_tac prems 1,
|
|
203 |
rtac intI 1,
|
|
204 |
REPEAT (dtac intD 1),
|
|
205 |
rewrite_goals_tac intensional_rews,
|
|
206 |
etac notE 1, atac 1]);
|
|
207 |
|
|
208 |
(* The following rule is stronger: It is enough to detect an
|
|
209 |
inconsistency at *some* world to conclude R. Note also that P and R
|
|
210 |
are allowed to be (intensional) formulas of different types! *)
|
|
211 |
|
|
212 |
qed_goal "notEW" Intensional.thy
|
|
213 |
"[| w |= .~P; w |= P |] ==> R::('w::world) form"
|
|
214 |
(fn prems => [cut_facts_tac prems 1,
|
|
215 |
rtac intI 1,
|
|
216 |
rewrite_goals_tac intensional_rews,
|
|
217 |
etac notE 1, atac 1]);
|
|
218 |
|
|
219 |
(** Implication **)
|
|
220 |
|
|
221 |
qed_goal "impIW" Intensional.thy "(!!w. (w |= A) ==> (w |= B)) ==> A .-> B"
|
|
222 |
(fn [prem] => [ rtac intI 1,
|
|
223 |
rewrite_goals_tac intensional_rews,
|
|
224 |
rtac impI 1,
|
|
225 |
etac prem 1 ]);
|
|
226 |
|
|
227 |
|
|
228 |
qed_goal "mpW" Intensional.thy "[| A .-> B; w |= A |] ==> w |= B"
|
|
229 |
(fn prems => [ cut_facts_tac prems 1,
|
|
230 |
dtac intD 1,
|
|
231 |
rewrite_goals_tac intensional_rews,
|
|
232 |
etac mp 1,
|
|
233 |
atac 1 ]);
|
|
234 |
|
|
235 |
qed_goal "impEW" Intensional.thy
|
|
236 |
"[| A .-> B; w |= A; w |= B ==> w |= C |] ==> w |= (C::('w::world) form)"
|
|
237 |
(fn prems => [ (REPEAT (resolve_tac (prems@[mpW]) 1)) ]);
|
|
238 |
|
|
239 |
qed_goal "rev_mpW" Intensional.thy "[| w |= P; P .-> Q |] ==> w |= Q"
|
|
240 |
(fn prems => [ (REPEAT (resolve_tac (prems@[mpW]) 1)) ]);
|
|
241 |
|
|
242 |
qed_goal "contraposW" Intensional.thy "[| w |= .~Q; P .-> Q |] ==> w |= .~P"
|
|
243 |
(fn [major,minor] => [rewrite_goals_tac intensional_rews,
|
|
244 |
rtac contrapos 1,
|
|
245 |
rtac (rewrite_rule intensional_rews major) 1,
|
|
246 |
etac rev_mpW 1,
|
|
247 |
rtac minor 1]);
|
|
248 |
|
|
249 |
qed_goal "iffEW" Intensional.thy
|
|
250 |
"[| (P::('w::world) form) .= Q; [| P .-> Q; Q .-> P |] ==> R::('w::world) form |] ==> R"
|
|
251 |
(fn [p1,p2] => [REPEAT(ares_tac([p1 RS iffD2W, p1 RS iffD1W, p2, impIW])1)]);
|
|
252 |
|
|
253 |
|
|
254 |
(** Conjunction **)
|
|
255 |
|
|
256 |
qed_goal "conjIW" Intensional.thy "[| w |= P; w |= Q |] ==> w |= P .& Q"
|
|
257 |
(fn prems => [rewrite_goals_tac intensional_rews,
|
|
258 |
REPEAT (resolve_tac ([conjI]@prems) 1)]);
|
|
259 |
|
|
260 |
qed_goal "conjunct1W" Intensional.thy "(w |= P .& Q) ==> w |= P"
|
|
261 |
(fn prems => [cut_facts_tac prems 1,
|
|
262 |
rewrite_goals_tac intensional_rews,
|
|
263 |
etac conjunct1 1]);
|
|
264 |
|
|
265 |
qed_goal "conjunct2W" Intensional.thy "(w |= P .& Q) ==> w |= Q"
|
|
266 |
(fn prems => [cut_facts_tac prems 1,
|
|
267 |
rewrite_goals_tac intensional_rews,
|
|
268 |
etac conjunct2 1]);
|
|
269 |
|
|
270 |
qed_goal "conjEW" Intensional.thy
|
|
271 |
"[| w |= P .& Q; [| w |= P; w |= Q |] ==> w |= R |] ==> w |= (R::('w::world) form)"
|
|
272 |
(fn prems => [cut_facts_tac prems 1, resolve_tac prems 1,
|
|
273 |
etac conjunct1W 1, etac conjunct2W 1]);
|
|
274 |
|
|
275 |
|
|
276 |
(** Disjunction **)
|
|
277 |
|
|
278 |
qed_goal "disjI1W" Intensional.thy "w |= P ==> w |= P .| Q"
|
|
279 |
(fn [prem] => [rewrite_goals_tac intensional_rews,
|
|
280 |
rtac disjI1 1,
|
|
281 |
rtac prem 1]);
|
|
282 |
|
|
283 |
qed_goal "disjI2W" Intensional.thy "w |= Q ==> w |= P .| Q"
|
|
284 |
(fn [prem] => [rewrite_goals_tac intensional_rews,
|
|
285 |
rtac disjI2 1,
|
|
286 |
rtac prem 1]);
|
|
287 |
|
|
288 |
qed_goal "disjEW" Intensional.thy
|
|
289 |
"[| w |= P .| Q; P .-> R; Q .-> R |] ==> w |= R"
|
|
290 |
(fn prems => [cut_facts_tac prems 1,
|
|
291 |
REPEAT (dtac intD 1),
|
|
292 |
rewrite_goals_tac intensional_rews,
|
|
293 |
fast_tac prop_cs 1]);
|
|
294 |
|
|
295 |
(** Classical propositional logic **)
|
|
296 |
|
|
297 |
qed_goal "classicalW" Intensional.thy "(.~P .-> P) ==> P::('w::world)form"
|
|
298 |
(fn prems => [cut_facts_tac prems 1,
|
|
299 |
rtac intI 1,
|
|
300 |
dtac intD 1,
|
|
301 |
rewrite_goals_tac intensional_rews,
|
|
302 |
fast_tac prop_cs 1]);
|
|
303 |
|
|
304 |
qed_goal "notnotDW" Intensional.thy ".~.~P ==> P::('w::world) form"
|
|
305 |
(fn prems => [cut_facts_tac prems 1,
|
|
306 |
rtac intI 1,
|
|
307 |
dtac intD 1,
|
|
308 |
rewrite_goals_tac intensional_rews,
|
|
309 |
etac notnotD 1]);
|
|
310 |
|
|
311 |
qed_goal "disjCIW" Intensional.thy "(w |= .~Q .-> P) ==> (w |= P.|Q)"
|
|
312 |
(fn prems => [cut_facts_tac prems 1,
|
|
313 |
rewrite_goals_tac intensional_rews,
|
|
314 |
fast_tac prop_cs 1]);
|
|
315 |
|
|
316 |
qed_goal "impCEW" Intensional.thy
|
|
317 |
"[| P.->Q; (w |= .~P) ==> (w |= R); (w |= Q) ==> (w |= R) |] ==> w |= (R::('w::world) form)"
|
|
318 |
(fn [a1,a2,a3] =>
|
|
319 |
[rtac (excluded_middle RS disjE) 1,
|
|
320 |
etac (rewrite_rule intensional_rews a2) 1,
|
|
321 |
rtac a3 1,
|
|
322 |
etac (a1 RS mpW) 1]);
|
|
323 |
|
|
324 |
(* The following generates too many parse trees...
|
|
325 |
|
|
326 |
qed_goal "iffCEW" Intensional.thy
|
|
327 |
"[| P .= Q; \
|
|
328 |
\ [| (w |= P); (w |= Q) |] ==> (w |= R); \
|
|
329 |
\ [| (w |= .~P); (w |= .~Q) |] ==> (w |= R) \
|
|
330 |
\ |] ==> w |= (R::('w::world) form)"
|
|
331 |
|
|
332 |
*)
|
|
333 |
|
|
334 |
qed_goal "case_split_thmW" Intensional.thy
|
|
335 |
"[| P .-> Q; .~P .-> Q |] ==> Q::('w::world) form"
|
|
336 |
(fn prems => [cut_facts_tac prems 1,
|
|
337 |
rtac intI 1,
|
|
338 |
REPEAT (dtac intD 1),
|
|
339 |
rewrite_goals_tac intensional_rews,
|
|
340 |
fast_tac prop_cs 1]);
|
|
341 |
|
|
342 |
fun case_tacW a = res_inst_tac [("P",a)] case_split_thmW;
|
|
343 |
|
|
344 |
|
|
345 |
(** Rigid quantifiers **)
|
|
346 |
|
|
347 |
qed_goal "allIW" Intensional.thy "(!!x. P(x)) ==> RALL x. P(x)"
|
|
348 |
(fn [prem] => [rtac intI 1,
|
|
349 |
rewrite_goals_tac intensional_rews,
|
|
350 |
rtac allI 1,
|
|
351 |
rtac (prem RS intE) 1]);
|
|
352 |
|
|
353 |
qed_goal "specW" Intensional.thy "(RALL x. P(x)) ==> P(x)"
|
|
354 |
(fn prems => [cut_facts_tac prems 1,
|
|
355 |
rtac intI 1,
|
|
356 |
dtac intD 1,
|
|
357 |
rewrite_goals_tac intensional_rews,
|
|
358 |
etac spec 1]);
|
|
359 |
|
|
360 |
|
|
361 |
qed_goal "allEW" Intensional.thy
|
3842
|
362 |
"[| RALL x. P(x); P(x) ==> R |] ==> R::('w::world) form"
|
3807
|
363 |
(fn major::prems=>
|
|
364 |
[ (REPEAT (resolve_tac (prems @ [major RS specW]) 1)) ]);
|
|
365 |
|
|
366 |
qed_goal "all_dupEW" Intensional.thy
|
3842
|
367 |
"[| RALL x. P(x); [| P(x); RALL x. P(x) |] ==> R |] ==> R::('w::world) form"
|
3807
|
368 |
(fn prems =>
|
|
369 |
[ (REPEAT (resolve_tac (prems @ (prems RL [specW])) 1)) ]);
|
|
370 |
|
|
371 |
|
3842
|
372 |
qed_goal "exIW" Intensional.thy "P(x) ==> REX x. P(x)"
|
3807
|
373 |
(fn [prem] => [rtac intI 1,
|
|
374 |
rewrite_goals_tac intensional_rews,
|
|
375 |
rtac exI 1,
|
|
376 |
rtac (prem RS intD) 1]);
|
|
377 |
|
|
378 |
qed_goal "exEW" Intensional.thy
|
3842
|
379 |
"[| w |= REX x. P(x); !!x. P(x) .-> Q |] ==> w |= Q"
|
3807
|
380 |
(fn [major,minor] => [rtac exE 1,
|
|
381 |
rtac (rewrite_rule intensional_rews major) 1,
|
|
382 |
etac rev_mpW 1,
|
|
383 |
rtac minor 1]);
|
|
384 |
|
|
385 |
(** Classical quantifier reasoning **)
|
|
386 |
|
|
387 |
qed_goal "exCIW" Intensional.thy
|
3842
|
388 |
"(w |= (RALL x. .~P(x)) .-> P(a)) ==> w |= REX x. P(x)"
|
3807
|
389 |
(fn prems => [cut_facts_tac prems 1,
|
|
390 |
rewrite_goals_tac intensional_rews,
|
|
391 |
fast_tac HOL_cs 1]);
|
|
392 |
|