1 (* ========================================================================= *)
2 (* Boolean theory including (intuitionistic) defs of logical connectives. *)
4 (* John Harrison, University of Cambridge Computer Laboratory *)
6 (* (c) Copyright, University of Cambridge 1998 *)
7 (* (c) Copyright, John Harrison 1998-2006 *)
8 (* ========================================================================= *)
10 (* ------------------------------------------------------------------------- *)
11 (* Set up parse status of basic and derived logical constants. *)
12 (* ------------------------------------------------------------------------- *)
16 map parse_as_binder ["\\"; "!"; "?"; "?!"];;
18 map parse_as_infix ["==>",(4,"right"); "\\/",(6,"right"); "/\\",(8,"right")];;
20 (* ------------------------------------------------------------------------- *)
21 (* Set up more orthodox notation for equations and equivalence. *)
22 (* ------------------------------------------------------------------------- *)
24 parse_as_infix("<=>",(2,"right"));;
25 override_interface ("<=>",`(=):bool->bool->bool`);;
26 parse_as_infix("=",(12,"right"));;
28 (* ------------------------------------------------------------------------- *)
29 (* Special syntax for Boolean equations (IFF). *)
30 (* ------------------------------------------------------------------------- *)
34 Comb(Comb(Const("=",Tyapp("fun",[Tyapp("bool",[]);_])),l),r) -> true
39 Comb(Comb(Const("=",Tyapp("fun",[Tyapp("bool",[]);_])),l),r) -> (l,r)
40 | _ -> failwith "dest_iff";;
43 let eq_tm = `(<=>)` in
44 fun (l,r) -> mk_comb(mk_comb(eq_tm,l),r);;
46 (* ------------------------------------------------------------------------- *)
47 (* Rule allowing easy instantiation of polymorphic proformas. *)
48 (* ------------------------------------------------------------------------- *)
51 let iterm_fn = INST (map (I F_F (inst tyin)) tmin)
52 and itype_fn = INST_TYPE tyin in
53 fun th -> try iterm_fn (itype_fn th)
54 with Failure _ -> failwith "PINST";;
56 (* ------------------------------------------------------------------------- *)
57 (* Useful derived deductive rule. *)
58 (* ------------------------------------------------------------------------- *)
60 let PROVE_HYP ath bth =
61 if exists (aconv (concl ath)) (hyp bth)
62 then EQ_MP (DEDUCT_ANTISYM_RULE ath bth) ath
65 (* ------------------------------------------------------------------------- *)
67 (* ------------------------------------------------------------------------- *)
69 let T_DEF = new_basic_definition
70 `T = ((\p:bool. p) = (\p:bool. p))`;;
72 let TRUTH = EQ_MP (SYM T_DEF) (REFL `\p:bool. p`);;
75 try EQ_MP (SYM th) TRUTH
76 with Failure _ -> failwith "EQT_ELIM";;
79 let t = `t:bool` and T = `T` in
81 let th1 = DEDUCT_ANTISYM_RULE (ASSUME t) TRUTH in
82 let th2 = EQT_ELIM(ASSUME(concl th1)) in
83 DEDUCT_ANTISYM_RULE th2 th1 in
84 fun th -> EQ_MP (INST[concl th,t] pth) th;;
86 (* ------------------------------------------------------------------------- *)
88 (* ------------------------------------------------------------------------- *)
90 let AND_DEF = new_basic_definition
91 `(/\) = \p q. (\f:bool->bool->bool. f p q) = (\f. f T T)`;;
93 let mk_conj = mk_binary "/\\";;
94 let list_mk_conj = end_itlist (curry mk_conj);;
97 let f = `f:bool->bool->bool`
102 and qth = ASSUME q in
103 let th1 = MK_COMB(AP_TERM f (EQT_INTRO pth),EQT_INTRO qth) in
104 let th2 = ABS f th1 in
105 let th3 = BETA_RULE (AP_THM (AP_THM AND_DEF p) q) in
106 EQ_MP (SYM th3) th2 in
107 fun th1 th2 -> substitute_proof (
108 let th = INST [concl th1,p; concl th2,q] pth in
109 PROVE_HYP th2 (PROVE_HYP th1 th))
110 (proof_CONJ (proof_of th1) (proof_of th2));;
113 let P = `P:bool` and Q = `Q:bool` in
115 let th1 = CONV_RULE (RAND_CONV BETA_CONV) (AP_THM AND_DEF `P:bool`) in
116 let th2 = CONV_RULE (RAND_CONV BETA_CONV) (AP_THM th1 `Q:bool`) in
117 let th3 = EQ_MP th2 (ASSUME `P /\ Q`) in
118 EQT_ELIM(BETA_RULE (AP_THM th3 `\(p:bool) (q:bool). p`)) in
119 fun th -> substitute_proof (
120 try let l,r = dest_conj(concl th) in
121 PROVE_HYP th (INST [l,P; r,Q] pth)
122 with Failure _ -> failwith "CONJUNCT1") (proof_CONJUNCT1 (proof_of th));;
125 let P = `P:bool` and Q = `Q:bool` in
127 let th1 = CONV_RULE (RAND_CONV BETA_CONV) (AP_THM AND_DEF `P:bool`) in
128 let th2 = CONV_RULE (RAND_CONV BETA_CONV) (AP_THM th1 `Q:bool`) in
129 let th3 = EQ_MP th2 (ASSUME `P /\ Q`) in
130 EQT_ELIM(BETA_RULE (AP_THM th3 `\(p:bool) (q:bool). q`)) in
131 fun th -> substitute_proof (
132 try let l,r = dest_conj(concl th) in
133 PROVE_HYP th (INST [l,P; r,Q] pth)
134 with Failure _ -> failwith "CONJUNCT2") (proof_CONJUNCT2 (proof_of th));;
137 try CONJUNCT1 th,CONJUNCT2 th
138 with Failure _ -> failwith "CONJ_PAIR: Not a conjunction";;
140 let CONJUNCTS = striplist CONJ_PAIR;;
142 (* ------------------------------------------------------------------------- *)
144 (* ------------------------------------------------------------------------- *)
146 let IMP_DEF = new_basic_definition
147 `(==>) = \p q. p /\ q <=> p`;;
149 let mk_imp = mk_binary "==>";;
155 let th1 = BETA_RULE (AP_THM (AP_THM IMP_DEF p) q) in
156 let th2 = EQ_MP th1 (ASSUME `p ==> q`) in
157 CONJUNCT2 (EQ_MP (SYM th2) (ASSUME `p:bool`)) in
159 let ant,con = dest_imp (concl ith) in
160 if aconv ant (concl th) then
161 PROVE_HYP th (PROVE_HYP ith (INST [ant,p; con,q] pth))
162 else failwith "MP: theorems do not agree";;
167 let pth = SYM(BETA_RULE (AP_THM (AP_THM IMP_DEF p) q)) in
168 fun a th -> substitute_proof (
169 let th1 = CONJ (ASSUME a) th in
170 let th2 = CONJUNCT1 (ASSUME (concl th1)) in
171 let th3 = DEDUCT_ANTISYM_RULE th1 th2 in
172 let th4 = INST [a,p; concl th,q] pth in
173 EQ_MP th4 th3) (proof_DISCH (proof_of th) a);;
175 let rec DISCH_ALL th =
176 try DISCH_ALL (DISCH (hd (hyp th)) th)
177 with Failure _ -> th;;
180 try MP th (ASSUME(rand(rator(concl th))))
181 with Failure _ -> failwith "UNDISCH";;
183 let rec UNDISCH_ALL th =
184 if is_imp (concl th) then UNDISCH_ALL (UNDISCH th)
187 let IMP_ANTISYM_RULE th1 th2 =
188 substitute_proof (DEDUCT_ANTISYM_RULE (UNDISCH th2) (UNDISCH th1))
189 (proof_IMPAS (proof_of th2) (proof_of th1));;
191 let ADD_ASSUM tm th = MP (DISCH tm th) (ASSUME tm);;
194 try let l,r = dest_eq(concl th) in
195 DISCH l (EQ_MP th (ASSUME l)), DISCH r (EQ_MP(SYM th)(ASSUME r))
196 with Failure _ -> failwith "EQ_IMP_RULE";;
198 let IMP_TRANS th1 th2 =
199 try let ant = rand(rator(concl th1)) in
200 DISCH ant (MP th2 (MP th1 (ASSUME ant)))
201 with Failure _ -> failwith "IMP_TRANS";;
203 (* ------------------------------------------------------------------------- *)
205 (* ------------------------------------------------------------------------- *)
207 let FORALL_DEF = new_basic_definition
208 `(!) = \P:A->bool. P = \x. T`;;
210 let mk_forall = mk_binder "!";;
211 let list_mk_forall(vs,bod) = itlist (curry mk_forall) vs bod;;
217 let th1 = EQ_MP(AP_THM FORALL_DEF `P:A->bool`) (ASSUME `(!)(P:A->bool)`) in
218 let th2 = AP_THM (CONV_RULE BETA_CONV th1) `x:A` in
219 let th3 = CONV_RULE (RAND_CONV BETA_CONV) th2 in
220 DISCH_ALL (EQT_ELIM th3) in
222 (substitute_proof (try let abs = rand(concl th) in
224 (MP (PINST [snd(dest_var(bndvar abs)),aty] [abs,P; tm,x] pth) th)
225 with Failure _ -> failwith "SPEC") (proof_SPEC tm (proof_of th)));;
228 try rev_itlist SPEC tms th
229 with Failure _ -> failwith "SPECL";;
232 let bv = variant (thm_frees th) (bndvar(rand(concl th))) in
235 let rec SPEC_ALL th =
236 if is_forall(concl th) then SPEC_ALL(snd(SPEC_VAR th)) else th;;
239 let x,_ = try dest_forall(concl th) with Failure _ ->
240 failwith "ISPEC: input theorem not universally quantified" in
241 let tyins = try type_match (snd(dest_var x)) (type_of t) [] with Failure _ ->
242 failwith "ISPEC can't type-instantiate input theorem" in
243 try SPEC t (INST_TYPE tyins th)
244 with Failure _ -> failwith "ISPEC: type variable(s) free in assumptions";;
247 try if tms = [] then th else
248 let avs = fst (chop_list (length tms) (fst(strip_forall(concl th)))) in
249 let tyins = itlist2 type_match (map (snd o dest_var) avs)
250 (map type_of tms) [] in
251 SPECL tms (INST_TYPE tyins th)
252 with Failure _ -> failwith "ISPECL";;
255 let P = `P:A->bool` and true_tm = `T` in
257 let th1 = ASSUME `P = \x:A. T` in
258 let th2 = AP_THM FORALL_DEF `P:A->bool` in
259 DISCH_ALL (EQ_MP (SYM(CONV_RULE(RAND_CONV BETA_CONV) th2)) th1) in
260 fun x th -> substitute_proof (
261 try let th1 = ABS x (EQT_INTRO th) in
262 let tm1 = mk_abs(mk_var("x",type_of x),true_tm) in
263 let th2 = TRANS th1 (REFL tm1) in
264 let th3 = PINST [snd(dest_var x),aty] [rand(rator(concl th1)),P] pth in
266 with Failure _ -> failwith "GEN") (proof_GEN (proof_of th) x);;
268 let GENL = itlist GEN;;
271 let asl,c = dest_thm th in
272 let vars = subtract (frees c) (freesl asl) in
275 (* ------------------------------------------------------------------------- *)
277 (* ------------------------------------------------------------------------- *)
279 let EXISTS_DEF = new_basic_definition
280 `(?) = \P:A->bool. !q. (!x. P x ==> q) ==> q`;;
282 let mk_exists = mk_binder "?";;
283 let list_mk_exists(vs,bod) = itlist (curry mk_exists) vs bod;;
286 let P = `P:A->bool` and x = `x:A` and PX = `(P:A->bool) x` in
288 let th1 = CONV_RULE (RAND_CONV BETA_CONV) (AP_THM EXISTS_DEF P) in
289 let th2 = SPEC `x:A` (ASSUME `!x:A. P x ==> Q`) in
290 let th3 = DISCH `!x:A. P x ==> Q` (MP th2 (ASSUME `(P:A->bool) x`)) in
291 DISCH_ALL (EQ_MP (SYM th1) (GEN `Q:bool` th3)) in
292 fun (etm,stm) th -> substitute_proof (
293 try let qf,abs = dest_comb etm in
294 let bth = BETA_CONV(mk_comb(abs,stm)) in
295 let cth = PINST [type_of stm,aty] [abs,P; stm,x] pth in
296 MP cth (EQ_MP (SYM bth) th)
297 with Failure _ -> failwith "EXISTS") (proof_EXISTS etm stm (proof_of th));;
299 let SIMPLE_EXISTS v th =
300 EXISTS (mk_exists(v,concl th),v) th;;
303 let P = `P:A->bool` and Q = `Q:bool` in
305 let th1 = CONV_RULE (RAND_CONV BETA_CONV) (AP_THM EXISTS_DEF P) in
306 let th2 = SPEC `Q:bool` (UNDISCH(fst(EQ_IMP_RULE th1))) in
307 DISCH_ALL (DISCH `(?) (P:A->bool)` (UNDISCH th2)) in
308 fun (v,th1) th2 -> substitute_proof (
309 try let abs = rand(concl th1) in
310 let bv,bod = dest_abs abs in
311 let cmb = mk_comb(abs,v) in
312 let pat = vsubst[v,bv] bod in
313 let th3 = CONV_RULE BETA_CONV (ASSUME cmb) in
314 let th4 = GEN v (DISCH cmb (MP (DISCH pat th2) th3)) in
315 let th5 = PINST [snd(dest_var v),aty] [abs,P; concl th2,Q] pth in
317 with Failure _ -> failwith "CHOOSE")
318 (proof_CHOOSE v (proof_of th1) (proof_of th2));;
320 let SIMPLE_CHOOSE v th =
321 CHOOSE(v,ASSUME (mk_exists(v,hd(hyp th)))) th;;
323 (* ------------------------------------------------------------------------- *)
325 (* ------------------------------------------------------------------------- *)
327 let OR_DEF = new_basic_definition
328 `(\/) = \p q. !r. (p ==> r) ==> (q ==> r) ==> r`;;
330 let mk_disj = mk_binary "\\/";;
331 let list_mk_disj = end_itlist (curry mk_disj);;
334 let P = `P:bool` and Q = `Q:bool` in
336 let th1 = CONV_RULE (RAND_CONV BETA_CONV) (AP_THM OR_DEF `P:bool`) in
337 let th2 = CONV_RULE (RAND_CONV BETA_CONV) (AP_THM th1 `Q:bool`) in
338 let th3 = MP (ASSUME `P ==> t`) (ASSUME `P:bool`) in
339 let th4 = GEN `t:bool` (DISCH `P ==> t` (DISCH `Q ==> t` th3)) in
340 DISCH_ALL (EQ_MP (SYM th2) th4) in
341 fun th tm -> substitute_proof (
342 try MP (INST [concl th,P; tm,Q] pth) th
343 with Failure _ -> failwith "DISJ1") (proof_DISJ1 (proof_of th) tm);;
346 let P = `P:bool` and Q = `Q:bool` in
348 let th1 = CONV_RULE (RAND_CONV BETA_CONV) (AP_THM OR_DEF `P:bool`) in
349 let th2 = CONV_RULE (RAND_CONV BETA_CONV) (AP_THM th1 `Q:bool`) in
350 let th3 = MP (ASSUME `Q ==> t`) (ASSUME `Q:bool`) in
351 let th4 = GEN `t:bool` (DISCH `P ==> t` (DISCH `Q ==> t` th3)) in
352 DISCH_ALL (EQ_MP (SYM th2) th4) in
353 fun tm th -> substitute_proof (
354 try MP (INST [tm,P; concl th,Q] pth) th
355 with Failure _ -> failwith "DISJ2") (proof_DISJ2 (proof_of th) tm);;
358 let P = `P:bool` and Q = `Q:bool` and R = `R:bool` in
360 let th1 = CONV_RULE (RAND_CONV BETA_CONV) (AP_THM OR_DEF `P:bool`) in
361 let th2 = CONV_RULE (RAND_CONV BETA_CONV) (AP_THM th1 `Q:bool`) in
362 let th3 = SPEC `R:bool` (EQ_MP th2 (ASSUME `P \/ Q`)) in
363 UNDISCH (UNDISCH th3) in
364 fun th0 th1 th2 -> substitute_proof (
365 try let c1 = concl th1 and c2 = concl th2 in
366 if not (aconv c1 c2) then failwith "DISJ_CASES" else
367 let l,r = dest_disj (concl th0) in
368 let th = INST [l,P; r,Q; c1,R] pth in
369 PROVE_HYP (DISCH r th2) (PROVE_HYP (DISCH l th1) (PROVE_HYP th0 th))
370 with Failure _ -> failwith "DISJ_CASES")
371 (proof_DISJCASES (proof_of th0) (proof_of th1) (proof_of th2));;
373 let SIMPLE_DISJ_CASES th1 th2 =
374 DISJ_CASES (ASSUME(mk_disj(hd(hyp th1),hd(hyp th2)))) th1 th2;;
376 (* ------------------------------------------------------------------------- *)
377 (* Rules for negation and falsity. *)
378 (* ------------------------------------------------------------------------- *)
380 let F_DEF = new_basic_definition
383 let NOT_DEF = new_basic_definition
384 `(~) = \p. p ==> F`;;
387 let neg_tm = `(~)` in
388 fun tm -> try mk_comb(neg_tm,tm)
389 with Failure _ -> failwith "mk_neg";;
393 let pth = CONV_RULE(RAND_CONV BETA_CONV) (AP_THM NOT_DEF P) in
394 fun th -> substitute_proof (
395 try EQ_MP (INST [rand(concl th),P] pth) th
396 with Failure _ -> failwith "NOT_ELIM") (proof_NOTE (proof_of th));;
400 let pth = SYM(CONV_RULE(RAND_CONV BETA_CONV) (AP_THM NOT_DEF P)) in
401 fun th -> substitute_proof (
402 try EQ_MP (INST [rand(rator(concl th)),P] pth) th
403 with Failure _ -> failwith "NOT_ELIM") (proof_NOTI (proof_of th));;
408 let th1 = NOT_ELIM (ASSUME `~ P`)
409 and th2 = DISCH `F` (SPEC P (EQ_MP F_DEF (ASSUME `F`))) in
410 DISCH_ALL (IMP_ANTISYM_RULE th1 th2) in
412 try MP (INST [rand(concl th),P] pth) th
413 with Failure _ -> failwith "EQF_INTRO";;
418 let th1 = EQ_MP (ASSUME `P = F`) (ASSUME `P:bool`) in
419 let th2 = DISCH P (SPEC `F` (EQ_MP F_DEF th1)) in
420 DISCH_ALL (NOT_INTRO th2) in
422 try MP (INST [rand(rator(concl th)),P] pth) th
423 with Failure _ -> failwith "EQF_ELIM";;
426 let P = `P:bool` and f_tm = `F` in
427 let pth = SPEC P (EQ_MP F_DEF (ASSUME `F`)) in
428 fun tm th -> substitute_proof (
429 if concl th <> f_tm then failwith "CONTR"
430 else PROVE_HYP th (INST [tm,P] pth)) (proof_CONTR (proof_of th) tm);;
432 (* ------------------------------------------------------------------------- *)
433 (* Rules for unique existence. *)
434 (* ------------------------------------------------------------------------- *)
436 let EXISTS_UNIQUE_DEF = new_basic_definition
437 `(?!) = \P:A->bool. ((?) P) /\ (!x y. P x /\ P y ==> x = y)`;;
439 let mk_uexists = mk_binder "?!";;
442 let P = `P:A->bool` in
444 let th1 = CONV_RULE (RAND_CONV BETA_CONV) (AP_THM EXISTS_UNIQUE_DEF P) in
445 let th2 = UNDISCH (fst(EQ_IMP_RULE th1)) in
446 DISCH_ALL (CONJUNCT1 th2) in
448 try let abs = rand(concl th) in
449 let ty = snd(dest_var(bndvar abs)) in
450 MP (PINST [ty,aty] [abs,P] pth) th
451 with Failure _ -> failwith "EXISTENCE";;