author | hoelzl |
Thu, 09 Jun 2011 14:24:34 +0200 | |
changeset 43342 | 2929f96d3ae7 |
parent 42799 | 4e33894aec6d |
child 44121 | 44adaa6db327 |
permissions | -rw-r--r-- |
1477 | 1 |
(* Title: FOLP/IFOLP.thy |
2 |
Author: Martin D Coen, Cambridge University Computer Laboratory |
|
1142 | 3 |
Copyright 1992 University of Cambridge |
4 |
*) |
|
5 |
||
17480 | 6 |
header {* Intuitionistic First-Order Logic with Proofs *} |
7 |
||
8 |
theory IFOLP |
|
9 |
imports Pure |
|
26322 | 10 |
uses ("hypsubst.ML") ("intprover.ML") |
17480 | 11 |
begin |
0 | 12 |
|
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
38800
diff
changeset
|
13 |
setup Pure_Thy.old_appl_syntax_setup |
26956
1309a6a0a29f
setup PureThy.old_appl_syntax_setup -- theory Pure provides regular application syntax by default;
wenzelm
parents:
26480
diff
changeset
|
14 |
|
17480 | 15 |
classes "term" |
36452 | 16 |
default_sort "term" |
0 | 17 |
|
17480 | 18 |
typedecl p |
19 |
typedecl o |
|
0 | 20 |
|
17480 | 21 |
consts |
0 | 22 |
(*** Judgements ***) |
1477 | 23 |
Proof :: "[o,p]=>prop" |
0 | 24 |
EqProof :: "[p,p,o]=>prop" ("(3_ /= _ :/ _)" [10,10,10] 5) |
17480 | 25 |
|
0 | 26 |
(*** Logical Connectives -- Type Formers ***) |
41310 | 27 |
eq :: "['a,'a] => o" (infixl "=" 50) |
17480 | 28 |
True :: "o" |
29 |
False :: "o" |
|
2714 | 30 |
Not :: "o => o" ("~ _" [40] 40) |
41310 | 31 |
conj :: "[o,o] => o" (infixr "&" 35) |
32 |
disj :: "[o,o] => o" (infixr "|" 30) |
|
33 |
imp :: "[o,o] => o" (infixr "-->" 25) |
|
34 |
iff :: "[o,o] => o" (infixr "<->" 25) |
|
0 | 35 |
(*Quantifiers*) |
1477 | 36 |
All :: "('a => o) => o" (binder "ALL " 10) |
37 |
Ex :: "('a => o) => o" (binder "EX " 10) |
|
38 |
Ex1 :: "('a => o) => o" (binder "EX! " 10) |
|
0 | 39 |
(*Rewriting gadgets*) |
1477 | 40 |
NORM :: "o => o" |
41 |
norm :: "'a => 'a" |
|
0 | 42 |
|
648
e27c9ec2b48b
FOLP/IFOLP.thy: tightening precedences to eliminate syntactic ambiguities.
lcp
parents:
283
diff
changeset
|
43 |
(*** Proof Term Formers: precedence must exceed 50 ***) |
1477 | 44 |
tt :: "p" |
45 |
contr :: "p=>p" |
|
17480 | 46 |
fst :: "p=>p" |
47 |
snd :: "p=>p" |
|
1477 | 48 |
pair :: "[p,p]=>p" ("(1<_,/_>)") |
49 |
split :: "[p, [p,p]=>p] =>p" |
|
17480 | 50 |
inl :: "p=>p" |
51 |
inr :: "p=>p" |
|
1477 | 52 |
when :: "[p, p=>p, p=>p]=>p" |
53 |
lambda :: "(p => p) => p" (binder "lam " 55) |
|
41310 | 54 |
App :: "[p,p]=>p" (infixl "`" 60) |
648
e27c9ec2b48b
FOLP/IFOLP.thy: tightening precedences to eliminate syntactic ambiguities.
lcp
parents:
283
diff
changeset
|
55 |
alll :: "['a=>p]=>p" (binder "all " 55) |
41310 | 56 |
app :: "[p,'a]=>p" (infixl "^" 55) |
1477 | 57 |
exists :: "['a,p]=>p" ("(1[_,/_])") |
0 | 58 |
xsplit :: "[p,['a,p]=>p]=>p" |
59 |
ideq :: "'a=>p" |
|
60 |
idpeel :: "[p,'a=>p]=>p" |
|
17480 | 61 |
nrm :: p |
62 |
NRM :: p |
|
0 | 63 |
|
35113 | 64 |
syntax "_Proof" :: "[p,o]=>prop" ("(_ /: _)" [51, 10] 5) |
65 |
||
38800 | 66 |
parse_translation {* |
67 |
let fun proof_tr [p, P] = Const (@{const_syntax Proof}, dummyT) $ P $ p |
|
68 |
in [(@{syntax_const "_Proof"}, proof_tr)] end |
|
17480 | 69 |
*} |
70 |
||
38800 | 71 |
(*show_proofs = true displays the proof terms -- they are ENORMOUS*) |
42616
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
41310
diff
changeset
|
72 |
ML {* val show_proofs = Attrib.setup_config_bool @{binding show_proofs} (K false) *} |
38800 | 73 |
|
74 |
print_translation (advanced) {* |
|
75 |
let |
|
76 |
fun proof_tr' ctxt [P, p] = |
|
77 |
if Config.get ctxt show_proofs then Const (@{syntax_const "_Proof"}, dummyT) $ p $ P |
|
78 |
else P |
|
79 |
in [(@{const_syntax Proof}, proof_tr')] end |
|
80 |
*} |
|
17480 | 81 |
|
82 |
axioms |
|
0 | 83 |
|
84 |
(**** Propositional logic ****) |
|
85 |
||
86 |
(*Equality*) |
|
87 |
(* Like Intensional Equality in MLTT - but proofs distinct from terms *) |
|
88 |
||
17480 | 89 |
ieqI: "ideq(a) : a=a" |
90 |
ieqE: "[| p : a=b; !!x. f(x) : P(x,x) |] ==> idpeel(p,f) : P(a,b)" |
|
0 | 91 |
|
92 |
(* Truth and Falsity *) |
|
93 |
||
17480 | 94 |
TrueI: "tt : True" |
95 |
FalseE: "a:False ==> contr(a):P" |
|
0 | 96 |
|
97 |
(* Conjunction *) |
|
98 |
||
17480 | 99 |
conjI: "[| a:P; b:Q |] ==> <a,b> : P&Q" |
100 |
conjunct1: "p:P&Q ==> fst(p):P" |
|
101 |
conjunct2: "p:P&Q ==> snd(p):Q" |
|
0 | 102 |
|
103 |
(* Disjunction *) |
|
104 |
||
17480 | 105 |
disjI1: "a:P ==> inl(a):P|Q" |
106 |
disjI2: "b:Q ==> inr(b):P|Q" |
|
107 |
disjE: "[| a:P|Q; !!x. x:P ==> f(x):R; !!x. x:Q ==> g(x):R |
|
108 |
|] ==> when(a,f,g):R" |
|
0 | 109 |
|
110 |
(* Implication *) |
|
111 |
||
17480 | 112 |
impI: "(!!x. x:P ==> f(x):Q) ==> lam x. f(x):P-->Q" |
113 |
mp: "[| f:P-->Q; a:P |] ==> f`a:Q" |
|
0 | 114 |
|
115 |
(*Quantifiers*) |
|
116 |
||
17480 | 117 |
allI: "(!!x. f(x) : P(x)) ==> all x. f(x) : ALL x. P(x)" |
118 |
spec: "(f:ALL x. P(x)) ==> f^x : P(x)" |
|
0 | 119 |
|
17480 | 120 |
exI: "p : P(x) ==> [x,p] : EX x. P(x)" |
121 |
exE: "[| p: EX x. P(x); !!x u. u:P(x) ==> f(x,u) : R |] ==> xsplit(p,f):R" |
|
0 | 122 |
|
123 |
(**** Equality between proofs ****) |
|
124 |
||
17480 | 125 |
prefl: "a : P ==> a = a : P" |
126 |
psym: "a = b : P ==> b = a : P" |
|
127 |
ptrans: "[| a = b : P; b = c : P |] ==> a = c : P" |
|
0 | 128 |
|
17480 | 129 |
idpeelB: "[| !!x. f(x) : P(x,x) |] ==> idpeel(ideq(a),f) = f(a) : P(a,a)" |
0 | 130 |
|
17480 | 131 |
fstB: "a:P ==> fst(<a,b>) = a : P" |
132 |
sndB: "b:Q ==> snd(<a,b>) = b : Q" |
|
133 |
pairEC: "p:P&Q ==> p = <fst(p),snd(p)> : P&Q" |
|
0 | 134 |
|
17480 | 135 |
whenBinl: "[| a:P; !!x. x:P ==> f(x) : Q |] ==> when(inl(a),f,g) = f(a) : Q" |
136 |
whenBinr: "[| b:P; !!x. x:P ==> g(x) : Q |] ==> when(inr(b),f,g) = g(b) : Q" |
|
137 |
plusEC: "a:P|Q ==> when(a,%x. inl(x),%y. inr(y)) = a : P|Q" |
|
0 | 138 |
|
17480 | 139 |
applyB: "[| a:P; !!x. x:P ==> b(x) : Q |] ==> (lam x. b(x)) ` a = b(a) : Q" |
140 |
funEC: "f:P ==> f = lam x. f`x : P" |
|
0 | 141 |
|
17480 | 142 |
specB: "[| !!x. f(x) : P(x) |] ==> (all x. f(x)) ^ a = f(a) : P(a)" |
0 | 143 |
|
144 |
||
145 |
(**** Definitions ****) |
|
146 |
||
17480 | 147 |
not_def: "~P == P-->False" |
148 |
iff_def: "P<->Q == (P-->Q) & (Q-->P)" |
|
0 | 149 |
|
150 |
(*Unique existence*) |
|
17480 | 151 |
ex1_def: "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)" |
0 | 152 |
|
153 |
(*Rewriting -- special constants to flag normalized terms and formulae*) |
|
17480 | 154 |
norm_eq: "nrm : norm(x) = x" |
155 |
NORM_iff: "NRM : NORM(P) <-> P" |
|
156 |
||
26322 | 157 |
(*** Sequent-style elimination rules for & --> and ALL ***) |
158 |
||
36319 | 159 |
schematic_lemma conjE: |
26322 | 160 |
assumes "p:P&Q" |
161 |
and "!!x y.[| x:P; y:Q |] ==> f(x,y):R" |
|
162 |
shows "?a:R" |
|
163 |
apply (rule assms(2)) |
|
164 |
apply (rule conjunct1 [OF assms(1)]) |
|
165 |
apply (rule conjunct2 [OF assms(1)]) |
|
166 |
done |
|
167 |
||
36319 | 168 |
schematic_lemma impE: |
26322 | 169 |
assumes "p:P-->Q" |
170 |
and "q:P" |
|
171 |
and "!!x. x:Q ==> r(x):R" |
|
172 |
shows "?p:R" |
|
173 |
apply (rule assms mp)+ |
|
174 |
done |
|
175 |
||
36319 | 176 |
schematic_lemma allE: |
26322 | 177 |
assumes "p:ALL x. P(x)" |
178 |
and "!!y. y:P(x) ==> q(y):R" |
|
179 |
shows "?p:R" |
|
180 |
apply (rule assms spec)+ |
|
181 |
done |
|
182 |
||
183 |
(*Duplicates the quantifier; for use with eresolve_tac*) |
|
36319 | 184 |
schematic_lemma all_dupE: |
26322 | 185 |
assumes "p:ALL x. P(x)" |
186 |
and "!!y z.[| y:P(x); z:ALL x. P(x) |] ==> q(y,z):R" |
|
187 |
shows "?p:R" |
|
188 |
apply (rule assms spec)+ |
|
189 |
done |
|
190 |
||
191 |
||
192 |
(*** Negation rules, which translate between ~P and P-->False ***) |
|
193 |
||
36319 | 194 |
schematic_lemma notI: |
26322 | 195 |
assumes "!!x. x:P ==> q(x):False" |
196 |
shows "?p:~P" |
|
197 |
unfolding not_def |
|
198 |
apply (assumption | rule assms impI)+ |
|
199 |
done |
|
200 |
||
36319 | 201 |
schematic_lemma notE: "p:~P \<Longrightarrow> q:P \<Longrightarrow> ?p:R" |
26322 | 202 |
unfolding not_def |
203 |
apply (drule (1) mp) |
|
204 |
apply (erule FalseE) |
|
205 |
done |
|
206 |
||
207 |
(*This is useful with the special implication rules for each kind of P. *) |
|
36319 | 208 |
schematic_lemma not_to_imp: |
26322 | 209 |
assumes "p:~P" |
210 |
and "!!x. x:(P-->False) ==> q(x):Q" |
|
211 |
shows "?p:Q" |
|
212 |
apply (assumption | rule assms impI notE)+ |
|
213 |
done |
|
214 |
||
215 |
(* For substitution int an assumption P, reduce Q to P-->Q, substitute into |
|
27150 | 216 |
this implication, then apply impI to move P back into the assumptions.*) |
36319 | 217 |
schematic_lemma rev_mp: "[| p:P; q:P --> Q |] ==> ?p:Q" |
26322 | 218 |
apply (assumption | rule mp)+ |
219 |
done |
|
220 |
||
221 |
||
222 |
(*Contrapositive of an inference rule*) |
|
36319 | 223 |
schematic_lemma contrapos: |
26322 | 224 |
assumes major: "p:~Q" |
225 |
and minor: "!!y. y:P==>q(y):Q" |
|
226 |
shows "?a:~P" |
|
227 |
apply (rule major [THEN notE, THEN notI]) |
|
228 |
apply (erule minor) |
|
229 |
done |
|
230 |
||
231 |
(** Unique assumption tactic. |
|
232 |
Ignores proof objects. |
|
233 |
Fails unless one assumption is equal and exactly one is unifiable |
|
234 |
**) |
|
235 |
||
236 |
ML {* |
|
237 |
local |
|
238 |
fun discard_proof (Const (@{const_name Proof}, _) $ P $ _) = P; |
|
239 |
in |
|
240 |
val uniq_assume_tac = |
|
241 |
SUBGOAL |
|
242 |
(fn (prem,i) => |
|
243 |
let val hyps = map discard_proof (Logic.strip_assums_hyp prem) |
|
244 |
and concl = discard_proof (Logic.strip_assums_concl prem) |
|
245 |
in |
|
246 |
if exists (fn hyp => hyp aconv concl) hyps |
|
29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
27152
diff
changeset
|
247 |
then case distinct (op =) (filter (fn hyp => Term.could_unify (hyp, concl)) hyps) of |
26322 | 248 |
[_] => assume_tac i |
249 |
| _ => no_tac |
|
250 |
else no_tac |
|
251 |
end); |
|
252 |
end; |
|
253 |
*} |
|
254 |
||
255 |
||
256 |
(*** Modus Ponens Tactics ***) |
|
257 |
||
258 |
(*Finds P-->Q and P in the assumptions, replaces implication by Q *) |
|
259 |
ML {* |
|
260 |
fun mp_tac i = eresolve_tac [@{thm notE}, make_elim @{thm mp}] i THEN assume_tac i |
|
261 |
*} |
|
262 |
||
263 |
(*Like mp_tac but instantiates no variables*) |
|
264 |
ML {* |
|
265 |
fun int_uniq_mp_tac i = eresolve_tac [@{thm notE}, @{thm impE}] i THEN uniq_assume_tac i |
|
266 |
*} |
|
267 |
||
268 |
||
269 |
(*** If-and-only-if ***) |
|
270 |
||
36319 | 271 |
schematic_lemma iffI: |
26322 | 272 |
assumes "!!x. x:P ==> q(x):Q" |
273 |
and "!!x. x:Q ==> r(x):P" |
|
274 |
shows "?p:P<->Q" |
|
275 |
unfolding iff_def |
|
276 |
apply (assumption | rule assms conjI impI)+ |
|
277 |
done |
|
278 |
||
279 |
||
280 |
(*Observe use of rewrite_rule to unfold "<->" in meta-assumptions (prems) *) |
|
281 |
||
36319 | 282 |
schematic_lemma iffE: |
26322 | 283 |
assumes "p:P <-> Q" |
284 |
and "!!x y.[| x:P-->Q; y:Q-->P |] ==> q(x,y):R" |
|
285 |
shows "?p:R" |
|
286 |
apply (rule conjE) |
|
287 |
apply (rule assms(1) [unfolded iff_def]) |
|
288 |
apply (rule assms(2)) |
|
289 |
apply assumption+ |
|
290 |
done |
|
291 |
||
292 |
(* Destruct rules for <-> similar to Modus Ponens *) |
|
293 |
||
36319 | 294 |
schematic_lemma iffD1: "[| p:P <-> Q; q:P |] ==> ?p:Q" |
26322 | 295 |
unfolding iff_def |
296 |
apply (rule conjunct1 [THEN mp], assumption+) |
|
297 |
done |
|
298 |
||
36319 | 299 |
schematic_lemma iffD2: "[| p:P <-> Q; q:Q |] ==> ?p:P" |
26322 | 300 |
unfolding iff_def |
301 |
apply (rule conjunct2 [THEN mp], assumption+) |
|
302 |
done |
|
303 |
||
36319 | 304 |
schematic_lemma iff_refl: "?p:P <-> P" |
26322 | 305 |
apply (rule iffI) |
306 |
apply assumption+ |
|
307 |
done |
|
308 |
||
36319 | 309 |
schematic_lemma iff_sym: "p:Q <-> P ==> ?p:P <-> Q" |
26322 | 310 |
apply (erule iffE) |
311 |
apply (rule iffI) |
|
312 |
apply (erule (1) mp)+ |
|
313 |
done |
|
314 |
||
36319 | 315 |
schematic_lemma iff_trans: "[| p:P <-> Q; q:Q<-> R |] ==> ?p:P <-> R" |
26322 | 316 |
apply (rule iffI) |
317 |
apply (assumption | erule iffE | erule (1) impE)+ |
|
318 |
done |
|
319 |
||
320 |
(*** Unique existence. NOTE THAT the following 2 quantifications |
|
321 |
EX!x such that [EX!y such that P(x,y)] (sequential) |
|
322 |
EX!x,y such that P(x,y) (simultaneous) |
|
323 |
do NOT mean the same thing. The parser treats EX!x y.P(x,y) as sequential. |
|
324 |
***) |
|
325 |
||
36319 | 326 |
schematic_lemma ex1I: |
26322 | 327 |
assumes "p:P(a)" |
328 |
and "!!x u. u:P(x) ==> f(u) : x=a" |
|
329 |
shows "?p:EX! x. P(x)" |
|
330 |
unfolding ex1_def |
|
331 |
apply (assumption | rule assms exI conjI allI impI)+ |
|
332 |
done |
|
333 |
||
36319 | 334 |
schematic_lemma ex1E: |
26322 | 335 |
assumes "p:EX! x. P(x)" |
336 |
and "!!x u v. [| u:P(x); v:ALL y. P(y) --> y=x |] ==> f(x,u,v):R" |
|
337 |
shows "?a : R" |
|
338 |
apply (insert assms(1) [unfolded ex1_def]) |
|
339 |
apply (erule exE conjE | assumption | rule assms(1))+ |
|
29305 | 340 |
apply (erule assms(2), assumption) |
26322 | 341 |
done |
342 |
||
343 |
||
344 |
(*** <-> congruence rules for simplification ***) |
|
345 |
||
346 |
(*Use iffE on a premise. For conj_cong, imp_cong, all_cong, ex_cong*) |
|
347 |
ML {* |
|
348 |
fun iff_tac prems i = |
|
349 |
resolve_tac (prems RL [@{thm iffE}]) i THEN |
|
350 |
REPEAT1 (eresolve_tac [asm_rl, @{thm mp}] i) |
|
351 |
*} |
|
352 |
||
36319 | 353 |
schematic_lemma conj_cong: |
26322 | 354 |
assumes "p:P <-> P'" |
355 |
and "!!x. x:P' ==> q(x):Q <-> Q'" |
|
356 |
shows "?p:(P&Q) <-> (P'&Q')" |
|
357 |
apply (insert assms(1)) |
|
358 |
apply (assumption | rule iffI conjI | |
|
359 |
erule iffE conjE mp | tactic {* iff_tac @{thms assms} 1 *})+ |
|
360 |
done |
|
361 |
||
36319 | 362 |
schematic_lemma disj_cong: |
26322 | 363 |
"[| p:P <-> P'; q:Q <-> Q' |] ==> ?p:(P|Q) <-> (P'|Q')" |
364 |
apply (erule iffE disjE disjI1 disjI2 | assumption | rule iffI | tactic {* mp_tac 1 *})+ |
|
365 |
done |
|
366 |
||
36319 | 367 |
schematic_lemma imp_cong: |
26322 | 368 |
assumes "p:P <-> P'" |
369 |
and "!!x. x:P' ==> q(x):Q <-> Q'" |
|
370 |
shows "?p:(P-->Q) <-> (P'-->Q')" |
|
371 |
apply (insert assms(1)) |
|
372 |
apply (assumption | rule iffI impI | erule iffE | tactic {* mp_tac 1 *} | |
|
373 |
tactic {* iff_tac @{thms assms} 1 *})+ |
|
374 |
done |
|
375 |
||
36319 | 376 |
schematic_lemma iff_cong: |
26322 | 377 |
"[| p:P <-> P'; q:Q <-> Q' |] ==> ?p:(P<->Q) <-> (P'<->Q')" |
378 |
apply (erule iffE | assumption | rule iffI | tactic {* mp_tac 1 *})+ |
|
379 |
done |
|
380 |
||
36319 | 381 |
schematic_lemma not_cong: |
26322 | 382 |
"p:P <-> P' ==> ?p:~P <-> ~P'" |
383 |
apply (assumption | rule iffI notI | tactic {* mp_tac 1 *} | erule iffE notE)+ |
|
384 |
done |
|
385 |
||
36319 | 386 |
schematic_lemma all_cong: |
26322 | 387 |
assumes "!!x. f(x):P(x) <-> Q(x)" |
388 |
shows "?p:(ALL x. P(x)) <-> (ALL x. Q(x))" |
|
389 |
apply (assumption | rule iffI allI | tactic {* mp_tac 1 *} | erule allE | |
|
390 |
tactic {* iff_tac @{thms assms} 1 *})+ |
|
391 |
done |
|
392 |
||
36319 | 393 |
schematic_lemma ex_cong: |
26322 | 394 |
assumes "!!x. f(x):P(x) <-> Q(x)" |
395 |
shows "?p:(EX x. P(x)) <-> (EX x. Q(x))" |
|
396 |
apply (erule exE | assumption | rule iffI exI | tactic {* mp_tac 1 *} | |
|
397 |
tactic {* iff_tac @{thms assms} 1 *})+ |
|
398 |
done |
|
399 |
||
400 |
(*NOT PROVED |
|
401 |
bind_thm ("ex1_cong", prove_goal (the_context ()) |
|
402 |
"(!!x.f(x):P(x) <-> Q(x)) ==> ?p:(EX! x.P(x)) <-> (EX! x.Q(x))" |
|
403 |
(fn prems => |
|
404 |
[ (REPEAT (eresolve_tac [ex1E, spec RS mp] 1 ORELSE ares_tac [iffI,ex1I] 1 |
|
405 |
ORELSE mp_tac 1 |
|
406 |
ORELSE iff_tac prems 1)) ])) |
|
407 |
*) |
|
408 |
||
409 |
(*** Equality rules ***) |
|
410 |
||
411 |
lemmas refl = ieqI |
|
412 |
||
36319 | 413 |
schematic_lemma subst: |
26322 | 414 |
assumes prem1: "p:a=b" |
415 |
and prem2: "q:P(a)" |
|
416 |
shows "?p : P(b)" |
|
417 |
apply (rule prem2 [THEN rev_mp]) |
|
418 |
apply (rule prem1 [THEN ieqE]) |
|
419 |
apply (rule impI) |
|
420 |
apply assumption |
|
421 |
done |
|
422 |
||
36319 | 423 |
schematic_lemma sym: "q:a=b ==> ?c:b=a" |
26322 | 424 |
apply (erule subst) |
425 |
apply (rule refl) |
|
426 |
done |
|
427 |
||
36319 | 428 |
schematic_lemma trans: "[| p:a=b; q:b=c |] ==> ?d:a=c" |
26322 | 429 |
apply (erule (1) subst) |
430 |
done |
|
431 |
||
432 |
(** ~ b=a ==> ~ a=b **) |
|
36319 | 433 |
schematic_lemma not_sym: "p:~ b=a ==> ?q:~ a=b" |
26322 | 434 |
apply (erule contrapos) |
435 |
apply (erule sym) |
|
436 |
done |
|
437 |
||
438 |
(*calling "standard" reduces maxidx to 0*) |
|
439 |
lemmas ssubst = sym [THEN subst, standard] |
|
440 |
||
441 |
(*A special case of ex1E that would otherwise need quantifier expansion*) |
|
36319 | 442 |
schematic_lemma ex1_equalsE: "[| p:EX! x. P(x); q:P(a); r:P(b) |] ==> ?d:a=b" |
26322 | 443 |
apply (erule ex1E) |
444 |
apply (rule trans) |
|
445 |
apply (rule_tac [2] sym) |
|
446 |
apply (assumption | erule spec [THEN mp])+ |
|
447 |
done |
|
448 |
||
449 |
(** Polymorphic congruence rules **) |
|
450 |
||
36319 | 451 |
schematic_lemma subst_context: "[| p:a=b |] ==> ?d:t(a)=t(b)" |
26322 | 452 |
apply (erule ssubst) |
453 |
apply (rule refl) |
|
454 |
done |
|
455 |
||
36319 | 456 |
schematic_lemma subst_context2: "[| p:a=b; q:c=d |] ==> ?p:t(a,c)=t(b,d)" |
26322 | 457 |
apply (erule ssubst)+ |
458 |
apply (rule refl) |
|
459 |
done |
|
460 |
||
36319 | 461 |
schematic_lemma subst_context3: "[| p:a=b; q:c=d; r:e=f |] ==> ?p:t(a,c,e)=t(b,d,f)" |
26322 | 462 |
apply (erule ssubst)+ |
463 |
apply (rule refl) |
|
464 |
done |
|
465 |
||
466 |
(*Useful with eresolve_tac for proving equalties from known equalities. |
|
467 |
a = b |
|
468 |
| | |
|
469 |
c = d *) |
|
36319 | 470 |
schematic_lemma box_equals: "[| p:a=b; q:a=c; r:b=d |] ==> ?p:c=d" |
26322 | 471 |
apply (rule trans) |
472 |
apply (rule trans) |
|
473 |
apply (rule sym) |
|
474 |
apply assumption+ |
|
475 |
done |
|
476 |
||
477 |
(*Dual of box_equals: for proving equalities backwards*) |
|
36319 | 478 |
schematic_lemma simp_equals: "[| p:a=c; q:b=d; r:c=d |] ==> ?p:a=b" |
26322 | 479 |
apply (rule trans) |
480 |
apply (rule trans) |
|
481 |
apply (assumption | rule sym)+ |
|
482 |
done |
|
483 |
||
484 |
(** Congruence rules for predicate letters **) |
|
485 |
||
36319 | 486 |
schematic_lemma pred1_cong: "p:a=a' ==> ?p:P(a) <-> P(a')" |
26322 | 487 |
apply (rule iffI) |
488 |
apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE eresolve_tac [@{thm subst}, @{thm ssubst}] 1) *}) |
|
489 |
done |
|
490 |
||
36319 | 491 |
schematic_lemma pred2_cong: "[| p:a=a'; q:b=b' |] ==> ?p:P(a,b) <-> P(a',b')" |
26322 | 492 |
apply (rule iffI) |
493 |
apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE eresolve_tac [@{thm subst}, @{thm ssubst}] 1) *}) |
|
494 |
done |
|
495 |
||
36319 | 496 |
schematic_lemma pred3_cong: "[| p:a=a'; q:b=b'; r:c=c' |] ==> ?p:P(a,b,c) <-> P(a',b',c')" |
26322 | 497 |
apply (rule iffI) |
498 |
apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE eresolve_tac [@{thm subst}, @{thm ssubst}] 1) *}) |
|
499 |
done |
|
500 |
||
27152
192954a9a549
changed pred_congs: merely cover pred1_cong pred2_cong pred3_cong;
wenzelm
parents:
27150
diff
changeset
|
501 |
lemmas pred_congs = pred1_cong pred2_cong pred3_cong |
26322 | 502 |
|
503 |
(*special case for the equality predicate!*) |
|
504 |
lemmas eq_cong = pred2_cong [where P = "op =", standard] |
|
505 |
||
506 |
||
507 |
(*** Simplifications of assumed implications. |
|
508 |
Roy Dyckhoff has proved that conj_impE, disj_impE, and imp_impE |
|
509 |
used with mp_tac (restricted to atomic formulae) is COMPLETE for |
|
510 |
intuitionistic propositional logic. See |
|
511 |
R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic |
|
512 |
(preprint, University of St Andrews, 1991) ***) |
|
513 |
||
36319 | 514 |
schematic_lemma conj_impE: |
26322 | 515 |
assumes major: "p:(P&Q)-->S" |
516 |
and minor: "!!x. x:P-->(Q-->S) ==> q(x):R" |
|
517 |
shows "?p:R" |
|
518 |
apply (assumption | rule conjI impI major [THEN mp] minor)+ |
|
519 |
done |
|
520 |
||
36319 | 521 |
schematic_lemma disj_impE: |
26322 | 522 |
assumes major: "p:(P|Q)-->S" |
523 |
and minor: "!!x y.[| x:P-->S; y:Q-->S |] ==> q(x,y):R" |
|
524 |
shows "?p:R" |
|
525 |
apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE |
|
526 |
resolve_tac [@{thm disjI1}, @{thm disjI2}, @{thm impI}, |
|
527 |
@{thm major} RS @{thm mp}, @{thm minor}] 1) *}) |
|
528 |
done |
|
529 |
||
530 |
(*Simplifies the implication. Classical version is stronger. |
|
531 |
Still UNSAFE since Q must be provable -- backtracking needed. *) |
|
36319 | 532 |
schematic_lemma imp_impE: |
26322 | 533 |
assumes major: "p:(P-->Q)-->S" |
534 |
and r1: "!!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q" |
|
535 |
and r2: "!!x. x:S ==> r(x):R" |
|
536 |
shows "?p:R" |
|
537 |
apply (assumption | rule impI major [THEN mp] r1 r2)+ |
|
538 |
done |
|
539 |
||
540 |
(*Simplifies the implication. Classical version is stronger. |
|
541 |
Still UNSAFE since ~P must be provable -- backtracking needed. *) |
|
36319 | 542 |
schematic_lemma not_impE: |
26322 | 543 |
assumes major: "p:~P --> S" |
544 |
and r1: "!!y. y:P ==> q(y):False" |
|
545 |
and r2: "!!y. y:S ==> r(y):R" |
|
546 |
shows "?p:R" |
|
547 |
apply (assumption | rule notI impI major [THEN mp] r1 r2)+ |
|
548 |
done |
|
549 |
||
550 |
(*Simplifies the implication. UNSAFE. *) |
|
36319 | 551 |
schematic_lemma iff_impE: |
26322 | 552 |
assumes major: "p:(P<->Q)-->S" |
553 |
and r1: "!!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q" |
|
554 |
and r2: "!!x y.[| x:Q; y:P-->S |] ==> r(x,y):P" |
|
555 |
and r3: "!!x. x:S ==> s(x):R" |
|
556 |
shows "?p:R" |
|
557 |
apply (assumption | rule iffI impI major [THEN mp] r1 r2 r3)+ |
|
558 |
done |
|
559 |
||
560 |
(*What if (ALL x.~~P(x)) --> ~~(ALL x.P(x)) is an assumption? UNSAFE*) |
|
36319 | 561 |
schematic_lemma all_impE: |
26322 | 562 |
assumes major: "p:(ALL x. P(x))-->S" |
563 |
and r1: "!!x. q:P(x)" |
|
564 |
and r2: "!!y. y:S ==> r(y):R" |
|
565 |
shows "?p:R" |
|
566 |
apply (assumption | rule allI impI major [THEN mp] r1 r2)+ |
|
567 |
done |
|
568 |
||
569 |
(*Unsafe: (EX x.P(x))-->S is equivalent to ALL x.P(x)-->S. *) |
|
36319 | 570 |
schematic_lemma ex_impE: |
26322 | 571 |
assumes major: "p:(EX x. P(x))-->S" |
572 |
and r: "!!y. y:P(a)-->S ==> q(y):R" |
|
573 |
shows "?p:R" |
|
574 |
apply (assumption | rule exI impI major [THEN mp] r)+ |
|
575 |
done |
|
576 |
||
577 |
||
36319 | 578 |
schematic_lemma rev_cut_eq: |
26322 | 579 |
assumes "p:a=b" |
580 |
and "!!x. x:a=b ==> f(x):R" |
|
581 |
shows "?p:R" |
|
582 |
apply (rule assms)+ |
|
583 |
done |
|
584 |
||
585 |
lemma thin_refl: "!!X. [|p:x=x; PROP W|] ==> PROP W" . |
|
586 |
||
587 |
use "hypsubst.ML" |
|
588 |
||
589 |
ML {* |
|
42799 | 590 |
structure Hypsubst = Hypsubst |
591 |
( |
|
26322 | 592 |
(*Take apart an equality judgement; otherwise raise Match!*) |
593 |
fun dest_eq (Const (@{const_name Proof}, _) $ |
|
41310 | 594 |
(Const (@{const_name eq}, _) $ t $ u) $ _) = (t, u); |
26322 | 595 |
|
596 |
val imp_intr = @{thm impI} |
|
597 |
||
598 |
(*etac rev_cut_eq moves an equality to be the last premise. *) |
|
599 |
val rev_cut_eq = @{thm rev_cut_eq} |
|
600 |
||
601 |
val rev_mp = @{thm rev_mp} |
|
602 |
val subst = @{thm subst} |
|
603 |
val sym = @{thm sym} |
|
604 |
val thin_refl = @{thm thin_refl} |
|
42799 | 605 |
); |
26322 | 606 |
open Hypsubst; |
607 |
*} |
|
608 |
||
609 |
use "intprover.ML" |
|
610 |
||
611 |
||
612 |
(*** Rewrite rules ***) |
|
613 |
||
36319 | 614 |
schematic_lemma conj_rews: |
26322 | 615 |
"?p1 : P & True <-> P" |
616 |
"?p2 : True & P <-> P" |
|
617 |
"?p3 : P & False <-> False" |
|
618 |
"?p4 : False & P <-> False" |
|
619 |
"?p5 : P & P <-> P" |
|
620 |
"?p6 : P & ~P <-> False" |
|
621 |
"?p7 : ~P & P <-> False" |
|
622 |
"?p8 : (P & Q) & R <-> P & (Q & R)" |
|
623 |
apply (tactic {* fn st => IntPr.fast_tac 1 st *})+ |
|
624 |
done |
|
625 |
||
36319 | 626 |
schematic_lemma disj_rews: |
26322 | 627 |
"?p1 : P | True <-> True" |
628 |
"?p2 : True | P <-> True" |
|
629 |
"?p3 : P | False <-> P" |
|
630 |
"?p4 : False | P <-> P" |
|
631 |
"?p5 : P | P <-> P" |
|
632 |
"?p6 : (P | Q) | R <-> P | (Q | R)" |
|
633 |
apply (tactic {* IntPr.fast_tac 1 *})+ |
|
634 |
done |
|
635 |
||
36319 | 636 |
schematic_lemma not_rews: |
26322 | 637 |
"?p1 : ~ False <-> True" |
638 |
"?p2 : ~ True <-> False" |
|
639 |
apply (tactic {* IntPr.fast_tac 1 *})+ |
|
640 |
done |
|
641 |
||
36319 | 642 |
schematic_lemma imp_rews: |
26322 | 643 |
"?p1 : (P --> False) <-> ~P" |
644 |
"?p2 : (P --> True) <-> True" |
|
645 |
"?p3 : (False --> P) <-> True" |
|
646 |
"?p4 : (True --> P) <-> P" |
|
647 |
"?p5 : (P --> P) <-> True" |
|
648 |
"?p6 : (P --> ~P) <-> ~P" |
|
649 |
apply (tactic {* IntPr.fast_tac 1 *})+ |
|
650 |
done |
|
651 |
||
36319 | 652 |
schematic_lemma iff_rews: |
26322 | 653 |
"?p1 : (True <-> P) <-> P" |
654 |
"?p2 : (P <-> True) <-> P" |
|
655 |
"?p3 : (P <-> P) <-> True" |
|
656 |
"?p4 : (False <-> P) <-> ~P" |
|
657 |
"?p5 : (P <-> False) <-> ~P" |
|
658 |
apply (tactic {* IntPr.fast_tac 1 *})+ |
|
659 |
done |
|
660 |
||
36319 | 661 |
schematic_lemma quant_rews: |
26322 | 662 |
"?p1 : (ALL x. P) <-> P" |
663 |
"?p2 : (EX x. P) <-> P" |
|
664 |
apply (tactic {* IntPr.fast_tac 1 *})+ |
|
665 |
done |
|
666 |
||
667 |
(*These are NOT supplied by default!*) |
|
36319 | 668 |
schematic_lemma distrib_rews1: |
26322 | 669 |
"?p1 : ~(P|Q) <-> ~P & ~Q" |
670 |
"?p2 : P & (Q | R) <-> P&Q | P&R" |
|
671 |
"?p3 : (Q | R) & P <-> Q&P | R&P" |
|
672 |
"?p4 : (P | Q --> R) <-> (P --> R) & (Q --> R)" |
|
673 |
apply (tactic {* IntPr.fast_tac 1 *})+ |
|
674 |
done |
|
675 |
||
36319 | 676 |
schematic_lemma distrib_rews2: |
26322 | 677 |
"?p1 : ~(EX x. NORM(P(x))) <-> (ALL x. ~NORM(P(x)))" |
678 |
"?p2 : ((EX x. NORM(P(x))) --> Q) <-> (ALL x. NORM(P(x)) --> Q)" |
|
679 |
"?p3 : (EX x. NORM(P(x))) & NORM(Q) <-> (EX x. NORM(P(x)) & NORM(Q))" |
|
680 |
"?p4 : NORM(Q) & (EX x. NORM(P(x))) <-> (EX x. NORM(Q) & NORM(P(x)))" |
|
681 |
apply (tactic {* IntPr.fast_tac 1 *})+ |
|
682 |
done |
|
683 |
||
684 |
lemmas distrib_rews = distrib_rews1 distrib_rews2 |
|
685 |
||
36319 | 686 |
schematic_lemma P_Imp_P_iff_T: "p:P ==> ?p:(P <-> True)" |
26322 | 687 |
apply (tactic {* IntPr.fast_tac 1 *}) |
688 |
done |
|
689 |
||
36319 | 690 |
schematic_lemma not_P_imp_P_iff_F: "p:~P ==> ?p:(P <-> False)" |
26322 | 691 |
apply (tactic {* IntPr.fast_tac 1 *}) |
692 |
done |
|
0 | 693 |
|
694 |
end |