1 (* ========================================================================= *)
2 (* Additional theorems, mainly about quantifiers, and additional tactics. *)
4 (* John Harrison, University of Cambridge Computer Laboratory *)
6 (* (c) Copyright, University of Cambridge 1998 *)
7 (* (c) Copyright, John Harrison 1998-2007 *)
8 (* (c) Copyright, Marco Maggesi 2012 *)
9 (* ========================================================================= *)
13 (* ------------------------------------------------------------------------- *)
14 (* More stuff about equality. *)
15 (* ------------------------------------------------------------------------- *)
19 GEN_TAC THEN REFL_TAC);;
21 let REFL_CLAUSE = prove
22 (`!x:A. (x = x) <=> T`,
23 GEN_TAC THEN MATCH_ACCEPT_TAC(EQT_INTRO(SPEC_ALL EQ_REFL)));;
26 (`!(x:A) y. (x = y) ==> (y = x)`,
27 REPEAT GEN_TAC THEN DISCH_THEN(ACCEPT_TAC o SYM));;
30 (`!(x:A) y. (x = y) <=> (y = x)`,
31 REPEAT GEN_TAC THEN EQ_TAC THEN MATCH_ACCEPT_TAC EQ_SYM);;
34 (`!(x:A) y z. (x = y) /\ (y = z) ==> (x = z)`,
35 REPEAT STRIP_TAC THEN PURE_ASM_REWRITE_TAC[] THEN REFL_TAC);;
37 (* ------------------------------------------------------------------------- *)
38 (* The following is a common special case of ordered rewriting. *)
39 (* ------------------------------------------------------------------------- *)
41 let AC acsuite = EQT_ELIM o PURE_REWRITE_CONV[acsuite; REFL_CLAUSE];;
43 (* ------------------------------------------------------------------------- *)
44 (* A couple of theorems about beta reduction. *)
45 (* ------------------------------------------------------------------------- *)
48 (`!(f:A->B) y. (\x. (f:A->B) x) y = f y`,
49 REPEAT GEN_TAC THEN BETA_TAC THEN REFL_TAC);;
52 (`!(t1:A) (t2:B). (\x. t1) t2 = t1`,
53 REPEAT GEN_TAC THEN REWRITE_TAC[BETA_THM; REFL_CLAUSE]);;
55 (* ------------------------------------------------------------------------- *)
56 (* A few "big name" intuitionistic tautologies. *)
57 (* ------------------------------------------------------------------------- *)
59 let CONJ_ASSOC = prove
60 (`!t1 t2 t3. t1 /\ t2 /\ t3 <=> (t1 /\ t2) /\ t3`,
64 (`!t1 t2. t1 /\ t2 <=> t2 /\ t1`,
68 (`(p /\ q <=> q /\ p) /\
69 ((p /\ q) /\ r <=> p /\ (q /\ r)) /\
70 (p /\ (q /\ r) <=> q /\ (p /\ r)) /\
72 (p /\ (p /\ q) <=> p /\ q)`,
75 let DISJ_ASSOC = prove
76 (`!t1 t2 t3. t1 \/ t2 \/ t3 <=> (t1 \/ t2) \/ t3`,
80 (`!t1 t2. t1 \/ t2 <=> t2 \/ t1`,
84 (`(p \/ q <=> q \/ p) /\
85 ((p \/ q) \/ r <=> p \/ (q \/ r)) /\
86 (p \/ (q \/ r) <=> q \/ (p \/ r)) /\
88 (p \/ (p \/ q) <=> p \/ q)`,
92 (`p /\ q ==> r <=> p ==> q ==> r`,
95 let IMP_IMP = GSYM IMP_CONJ;;
97 let IMP_CONJ_ALT = prove
98 (`p /\ q ==> r <=> q ==> p ==> r`,
101 (* ------------------------------------------------------------------------- *)
102 (* A couple of "distribution" tautologies are useful. *)
103 (* ------------------------------------------------------------------------- *)
105 let LEFT_OR_DISTRIB = prove
106 (`!p q r. p /\ (q \/ r) <=> p /\ q \/ p /\ r`,
109 let RIGHT_OR_DISTRIB = prove
110 (`!p q r. (p \/ q) /\ r <=> p /\ r \/ q /\ r`,
113 (* ------------------------------------------------------------------------- *)
114 (* Degenerate cases of quantifiers. *)
115 (* ------------------------------------------------------------------------- *)
117 let FORALL_SIMP = prove
118 (`!t. (!x:A. t) = t`,
121 let EXISTS_SIMP = prove
122 (`!t. (?x:A. t) = t`,
125 (* ------------------------------------------------------------------------- *)
126 (* I also use this a lot (as a prelude to congruence reasoning). *)
127 (* ------------------------------------------------------------------------- *)
129 let EQ_IMP = ITAUT `(a <=> b) ==> a ==> b`;;
131 (* ------------------------------------------------------------------------- *)
132 (* Start building up the basic rewrites; we add a few more later. *)
133 (* ------------------------------------------------------------------------- *)
135 let EQ_CLAUSES = prove
136 (`!t. ((T <=> t) <=> t) /\ ((t <=> T) <=> t) /\
137 ((F <=> t) <=> ~t) /\ ((t <=> F) <=> ~t)`,
140 let NOT_CLAUSES_WEAK = prove
141 (`(~T <=> F) /\ (~F <=> T)`,
144 let AND_CLAUSES = prove
145 (`!t. (T /\ t <=> t) /\ (t /\ T <=> t) /\ (F /\ t <=> F) /\
146 (t /\ F <=> F) /\ (t /\ t <=> t)`,
149 let OR_CLAUSES = prove
150 (`!t. (T \/ t <=> T) /\ (t \/ T <=> T) /\ (F \/ t <=> t) /\
151 (t \/ F <=> t) /\ (t \/ t <=> t)`,
154 let IMP_CLAUSES = prove
155 (`!t. (T ==> t <=> t) /\ (t ==> T <=> T) /\ (F ==> t <=> T) /\
156 (t ==> t <=> T) /\ (t ==> F <=> ~t)`,
159 extend_basic_rewrites
169 let IMP_EQ_CLAUSE = prove
170 (`((x = x) ==> p) <=> p`,
171 REWRITE_TAC[EQT_INTRO(SPEC_ALL EQ_REFL); IMP_CLAUSES]) in
175 [ITAUT `(p <=> p') ==> (p' ==> (q <=> q')) ==> (p ==> q <=> p' ==> q')`];;
177 (* ------------------------------------------------------------------------- *)
178 (* Rewrite rule for unique existence. *)
179 (* ------------------------------------------------------------------------- *)
181 let EXISTS_UNIQUE_THM = prove
182 (`!P. (?!x:A. P x) <=> (?x. P x) /\ (!x x'. P x /\ P x' ==> (x = x'))`,
183 GEN_TAC THEN REWRITE_TAC[EXISTS_UNIQUE_DEF]);;
185 (* ------------------------------------------------------------------------- *)
186 (* Trivial instances of existence. *)
187 (* ------------------------------------------------------------------------- *)
189 let EXISTS_REFL = prove
191 GEN_TAC THEN EXISTS_TAC `a:A` THEN REFL_TAC);;
193 let EXISTS_UNIQUE_REFL = prove
195 GEN_TAC THEN REWRITE_TAC[EXISTS_UNIQUE_THM] THEN
196 REPEAT(EQ_TAC ORELSE STRIP_TAC) THENL
197 [EXISTS_TAC `a:A`; ASM_REWRITE_TAC[]] THEN
200 (* ------------------------------------------------------------------------- *)
202 (* ------------------------------------------------------------------------- *)
204 let UNWIND_THM1 = prove
205 (`!P (a:A). (?x. a = x /\ P x) <=> P a`,
206 REPEAT GEN_TAC THEN EQ_TAC THENL
207 [DISCH_THEN(CHOOSE_THEN (CONJUNCTS_THEN2 SUBST1_TAC ACCEPT_TAC));
208 DISCH_TAC THEN EXISTS_TAC `a:A` THEN
209 CONJ_TAC THEN TRY(FIRST_ASSUM MATCH_ACCEPT_TAC) THEN
212 let UNWIND_THM2 = prove
213 (`!P (a:A). (?x. x = a /\ P x) <=> P a`,
214 REPEAT GEN_TAC THEN CONV_TAC(LAND_CONV(ONCE_DEPTH_CONV SYM_CONV)) THEN
215 MATCH_ACCEPT_TAC UNWIND_THM1);;
217 let FORALL_UNWIND_THM2 = prove
218 (`!P (a:A). (!x. x = a ==> P x) <=> P a`,
219 REPEAT GEN_TAC THEN EQ_TAC THENL
220 [DISCH_THEN(MP_TAC o SPEC `a:A`) THEN REWRITE_TAC[];
221 DISCH_TAC THEN GEN_TAC THEN DISCH_THEN SUBST1_TAC THEN
222 ASM_REWRITE_TAC[]]);;
224 let FORALL_UNWIND_THM1 = prove
225 (`!P a. (!x. a = x ==> P x) <=> P a`,
226 REPEAT GEN_TAC THEN CONV_TAC(LAND_CONV(ONCE_DEPTH_CONV SYM_CONV)) THEN
227 MATCH_ACCEPT_TAC FORALL_UNWIND_THM2);;
229 (* ------------------------------------------------------------------------- *)
230 (* Permuting quantifiers. *)
231 (* ------------------------------------------------------------------------- *)
233 let SWAP_FORALL_THM = prove
234 (`!P:A->B->bool. (!x y. P x y) <=> (!y x. P x y)`,
237 let SWAP_EXISTS_THM = prove
238 (`!P:A->B->bool. (?x y. P x y) <=> (?y x. P x y)`,
241 (* ------------------------------------------------------------------------- *)
242 (* Universal quantifier and conjunction. *)
243 (* ------------------------------------------------------------------------- *)
245 let FORALL_AND_THM = prove
246 (`!P Q. (!x:A. P x /\ Q x) <=> (!x. P x) /\ (!x. Q x)`,
249 let AND_FORALL_THM = prove
250 (`!P Q. (!x. P x) /\ (!x. Q x) <=> (!x:A. P x /\ Q x)`,
253 let LEFT_AND_FORALL_THM = prove
254 (`!P Q. (!x:A. P x) /\ Q <=> (!x:A. P x /\ Q)`,
257 let RIGHT_AND_FORALL_THM = prove
258 (`!P Q. P /\ (!x:A. Q x) <=> (!x. P /\ Q x)`,
261 (* ------------------------------------------------------------------------- *)
262 (* Existential quantifier and disjunction. *)
263 (* ------------------------------------------------------------------------- *)
265 let EXISTS_OR_THM = prove
266 (`!P Q. (?x:A. P x \/ Q x) <=> (?x. P x) \/ (?x. Q x)`,
269 let OR_EXISTS_THM = prove
270 (`!P Q. (?x. P x) \/ (?x. Q x) <=> (?x:A. P x \/ Q x)`,
273 let LEFT_OR_EXISTS_THM = prove
274 (`!P Q. (?x. P x) \/ Q <=> (?x:A. P x \/ Q)`,
277 let RIGHT_OR_EXISTS_THM = prove
278 (`!P Q. P \/ (?x. Q x) <=> (?x:A. P \/ Q x)`,
281 (* ------------------------------------------------------------------------- *)
282 (* Existential quantifier and conjunction. *)
283 (* ------------------------------------------------------------------------- *)
285 let LEFT_EXISTS_AND_THM = prove
286 (`!P Q. (?x:A. P x /\ Q) <=> (?x:A. P x) /\ Q`,
289 let RIGHT_EXISTS_AND_THM = prove
290 (`!P Q. (?x:A. P /\ Q x) <=> P /\ (?x:A. Q x)`,
293 let TRIV_EXISTS_AND_THM = prove
294 (`!P Q. (?x:A. P /\ Q) <=> (?x:A. P) /\ (?x:A. Q)`,
297 let LEFT_AND_EXISTS_THM = prove
298 (`!P Q. (?x:A. P x) /\ Q <=> (?x:A. P x /\ Q)`,
301 let RIGHT_AND_EXISTS_THM = prove
302 (`!P Q. P /\ (?x:A. Q x) <=> (?x:A. P /\ Q x)`,
305 let TRIV_AND_EXISTS_THM = prove
306 (`!P Q. (?x:A. P) /\ (?x:A. Q) <=> (?x:A. P /\ Q)`,
309 (* ------------------------------------------------------------------------- *)
310 (* Only trivial instances of universal quantifier and disjunction. *)
311 (* ------------------------------------------------------------------------- *)
313 let TRIV_FORALL_OR_THM = prove
314 (`!P Q. (!x:A. P \/ Q) <=> (!x:A. P) \/ (!x:A. Q)`,
317 let TRIV_OR_FORALL_THM = prove
318 (`!P Q. (!x:A. P) \/ (!x:A. Q) <=> (!x:A. P \/ Q)`,
321 (* ------------------------------------------------------------------------- *)
322 (* Implication and quantifiers. *)
323 (* ------------------------------------------------------------------------- *)
325 let RIGHT_IMP_FORALL_THM = prove
326 (`!P Q. (P ==> !x:A. Q x) <=> (!x. P ==> Q x)`,
329 let RIGHT_FORALL_IMP_THM = prove
330 (`!P Q. (!x. P ==> Q x) <=> (P ==> !x:A. Q x)`,
333 let LEFT_IMP_EXISTS_THM = prove
334 (`!P Q. ((?x:A. P x) ==> Q) <=> (!x. P x ==> Q)`,
337 let LEFT_FORALL_IMP_THM = prove
338 (`!P Q. (!x. P x ==> Q) <=> ((?x:A. P x) ==> Q)`,
341 let TRIV_FORALL_IMP_THM = prove
342 (`!P Q. (!x:A. P ==> Q) <=> ((?x:A. P) ==> (!x:A. Q))`,
345 let TRIV_EXISTS_IMP_THM = prove
346 (`!P Q. (?x:A. P ==> Q) <=> ((!x:A. P) ==> (?x:A. Q))`,
349 (* ------------------------------------------------------------------------- *)
350 (* Alternative versions of unique existence. *)
351 (* ------------------------------------------------------------------------- *)
353 let EXISTS_UNIQUE_ALT = prove
354 (`!P:A->bool. (?!x. P x) <=> (?x. !y. P y <=> (x = y))`,
355 GEN_TAC THEN REWRITE_TAC[EXISTS_UNIQUE_THM] THEN EQ_TAC THENL
356 [DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `x:A`) ASSUME_TAC) THEN
357 EXISTS_TAC `x:A` THEN GEN_TAC THEN EQ_TAC THENL
358 [DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
359 DISCH_THEN(SUBST1_TAC o SYM) THEN FIRST_ASSUM MATCH_ACCEPT_TAC];
360 DISCH_THEN(X_CHOOSE_TAC `x:A`) THEN
361 ASM_REWRITE_TAC[GSYM EXISTS_REFL] THEN REPEAT GEN_TAC THEN
362 DISCH_THEN(CONJUNCTS_THEN (SUBST1_TAC o SYM)) THEN REFL_TAC]);;
364 let EXISTS_UNIQUE = prove
365 (`!P:A->bool. (?!x. P x) <=> (?x. P x /\ !y. P y ==> (y = x))`,
366 GEN_TAC THEN REWRITE_TAC[EXISTS_UNIQUE_ALT] THEN
367 AP_TERM_TAC THEN ABS_TAC THEN
368 GEN_REWRITE_TAC (LAND_CONV o BINDER_CONV)
369 [ITAUT `(a <=> b) <=> (a ==> b) /\ (b ==> a)`] THEN
370 GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [EQ_SYM_EQ] THEN
371 REWRITE_TAC[FORALL_AND_THM] THEN SIMP_TAC[] THEN
372 REWRITE_TAC[LEFT_FORALL_IMP_THM; EXISTS_REFL] THEN
373 REWRITE_TAC[CONJ_ACI]);;
375 (* ------------------------------------------------------------------------- *)
376 (* DESTRUCT_TAC, FIX_TAC and INTRO_TAC, giving more brief and elegant ways *)
377 (* of naming introduced variables and assumptions (from Marco Maggesi). *)
378 (* ------------------------------------------------------------------------- *)
380 let DESTRUCT_TAC,FIX_TAC,INTRO_TAC =
381 let NAME_GEN_TAC s gl =
382 let ty = (snd o dest_var o fst o dest_forall o snd) gl in
383 X_GEN_TAC (mk_var(s,ty)) gl
384 and OBTAIN_THEN v ttac th =
385 let ty = (snd o dest_var o fst o dest_exists o concl) th in
386 X_CHOOSE_THEN (mk_var(v,ty)) ttac th
387 and CONJ_LIST_TAC = end_itlist (fun t1 t2 -> CONJ_TAC THENL [t1; t2])
389 if n <= 0 then failwith "NUM_DISJ_TAC" else
390 REPLICATE_TAC (n-1) DISJ2_TAC THEN REPEAT DISJ1_TAC
391 and NAME_PULL_FORALL_CONV =
392 let SWAP_FORALL_CONV = REWR_CONV SWAP_FORALL_THM
393 and AND_FORALL_CONV = GEN_REWRITE_CONV I [AND_FORALL_THM]
394 and RIGHT_IMP_FORALL_CONV = GEN_REWRITE_CONV I [RIGHT_IMP_FORALL_THM] in
396 let rec PULL_FORALL tm =
398 if name_of(fst(dest_forall tm)) = s then REFL tm else
399 (BINDER_CONV PULL_FORALL THENC SWAP_FORALL_CONV) tm
400 else if is_imp tm then
401 (RAND_CONV PULL_FORALL THENC RIGHT_IMP_FORALL_CONV) tm
402 else if is_conj tm then
403 (BINOP_CONV PULL_FORALL THENC AND_FORALL_CONV) tm
409 Ident s::rest when isalpha s -> s,rest
410 | _ -> raise Noparse in
412 let old_name = possibly (a(Ident "/") ++ ident >> snd) in
413 (a(Resword "[") ++ ident >> snd) ++ old_name ++ a(Resword "]") >> fst in
414 let mk_var v = CONV_TAC (NAME_PULL_FORALL_CONV v) THEN GEN_TAC
416 function u,[v] -> CONV_TAC (NAME_PULL_FORALL_CONV v) THEN NAME_GEN_TAC u
417 | u,_ -> NAME_GEN_TAC u in
418 let vars = many (rename >> mk_rename || ident >> mk_var) >> EVERY
419 and star = possibly (a (Ident "*") >> K (REPEAT GEN_TAC)) in
420 vars ++ star >> function tac,[] -> tac | tac,_ -> tac THEN REPEAT GEN_TAC
422 let OBTAINL_THEN : string list -> thm_tactical =
423 EVERY_TCL o map OBTAIN_THEN in
424 let ident p = function
425 Ident s::rest when p s -> s,rest
426 | _ -> raise Noparse in
427 let rec destruct inp = disj inp
429 let DISJ_CASES_LIST = end_itlist DISJ_CASES_THEN2 in
430 (listof conj (a(Resword "|")) "Disjunction" >> DISJ_CASES_LIST) inp
431 and conj inp = (atleast 1 atom >> end_itlist CONJUNCTS_THEN2) inp
434 let var_list = atleast 1 (ident isalpha) in
435 (a(Ident "@") ++ var_list >> snd) ++ a(Resword ".") >> fst in
436 (obtain_prfx ++ destruct >> uncurry OBTAINL_THEN) inp
438 let label = ident isalnum >> LABEL_TAC in
440 (a(Resword "(") ++ destruct >> snd) ++ a(Resword ")") >> fst in
441 (label || obtain || paren) inp in
444 let number = function
447 let n = int_of_string s in
448 if n < 1 then raise Noparse else n,rest
449 with Failure _ -> raise Noparse)
451 and pa_fix = a(Ident "!") ++ parse_fix >> snd
452 and pa_dest = parse_destruct >> DISCH_THEN in
454 elistof (pa_fix || pa_dest) (a(Resword ";")) "Prefix intro pattern" in
455 let rec pa_intro toks =
456 (pa_prefix ++ possibly pa_postfix >> uncurry (@) >> EVERY) toks
457 and pa_postfix toks = (pa_conj || pa_disj) toks
460 listof pa_intro (a(Ident "&")) "Intro pattern" >> CONJ_LIST_TAC in
461 ((a(Resword "{") ++ conjs >> snd) ++ a(Resword "}") >> fst) toks
463 let disj = number >> NUM_DISJ_TAC in
464 ((a(Ident "#") ++ disj >> snd) ++ pa_intro >> uncurry (THEN)) toks in
468 (fix "Destruct pattern" parse_destruct o lex o explode) s in
469 if rest=[] then tac else failwith "Garbage after destruct pattern"
472 (fix "Introduction pattern" parse_intro o lex o explode) s in
473 if rest=[] then tac else failwith "Garbage after intro pattern"
475 let tac,rest = (parse_fix o lex o explode) s in
476 if rest=[] then tac else failwith "FIX_TAC: invalid pattern" in
477 DESTRUCT_TAC,FIX_TAC,INTRO_TAC;;