Proofrecording/diffs/bool.ml

   1 (* ========================================================================= *)
   2 (* Boolean theory including (intuitionistic) defs of logical connectives.    *)
   3 (*                                                                           *)
   4 (*       John Harrison, University of Cambridge Computer Laboratory          *)
   5 (*                                                                           *)
   6 (*            (c) Copyright, University of Cambridge 1998                    *)
   7 (*              (c) Copyright, John Harrison 1998-2006                       *)
   8 (* ========================================================================= *)
   9
  10 (* ------------------------------------------------------------------------- *)
  11 (* Set up parse status of basic and derived logical constants.               *)
  12 (* ------------------------------------------------------------------------- *)
  13
  14 parse_as_prefix "~";;
  15
  16 map parse_as_binder ["\\"; "!"; "?"; "?!"];;
  17
  18 map parse_as_infix ["==>",(4,"right"); "\\/",(6,"right"); "/\\",(8,"right")];;
  19
  20 (* ------------------------------------------------------------------------- *)
  21 (* Set up more orthodox notation for equations and equivalence.              *)
  22 (* ------------------------------------------------------------------------- *)
  23
  24 parse_as_infix("<=>",(2,"right"));;
  25 override_interface ("<=>",`(=):bool->bool->bool`);;
  26 parse_as_infix("=",(12,"right"));;
  27
  28 (* ------------------------------------------------------------------------- *)
  29 (* Special syntax for Boolean equations (IFF).                               *)
  30 (* ------------------------------------------------------------------------- *)
  31
  32 let is_iff tm =
  33   match tm with
  34     Comb(Comb(Const("=",Tyapp("fun",[Tyapp("bool",[]);_])),l),r) -> true
  35   | _ -> false;;
  36
  37 let dest_iff tm =
  38   match tm with
  39     Comb(Comb(Const("=",Tyapp("fun",[Tyapp("bool",[]);_])),l),r) -> (l,r)
  40   | _ -> failwith "dest_iff";;
  41
  42 let mk_iff =
  43   let eq_tm = `(<=>)` in
  44   fun (l,r) -> mk_comb(mk_comb(eq_tm,l),r);;
  45
  46 (* ------------------------------------------------------------------------- *)
  47 (* Rule allowing easy instantiation of polymorphic proformas.                *)
  48 (* ------------------------------------------------------------------------- *)
  49
  50 let PINST tyin tmin =
  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";;
  55
  56 (* ------------------------------------------------------------------------- *)
  57 (* Useful derived deductive rule.                                            *)
  58 (* ------------------------------------------------------------------------- *)
  59
  60 let PROVE_HYP ath bth =
  61   if exists (aconv (concl ath)) (hyp bth)
  62   then EQ_MP (DEDUCT_ANTISYM_RULE ath bth) ath
  63   else bth;;
  64
  65 (* ------------------------------------------------------------------------- *)
  66 (* Rules for T                                                               *)
  67 (* ------------------------------------------------------------------------- *)
  68
  69 let T_DEF = new_basic_definition
  70  `T = ((\p:bool. p) = (\p:bool. p))`;;
  71
  72 let TRUTH = EQ_MP (SYM T_DEF) (REFL `\p:bool. p`);;
  73
  74 let EQT_ELIM th =
  75   try EQ_MP (SYM th) TRUTH
  76   with Failure _ -> failwith "EQT_ELIM";;
  77
  78 let EQT_INTRO =
  79   let t = `t:bool` and T = `T` in
  80   let pth =
  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;;
  85
  86 (* ------------------------------------------------------------------------- *)
  87 (* Rules for /\                                                              *)
  88 (* ------------------------------------------------------------------------- *)
  89
  90 let AND_DEF = new_basic_definition
  91  `(/\) = \p q. (\f:bool->bool->bool. f p q) = (\f. f T T)`;;
  92
  93 let mk_conj = mk_binary "/\\";;
  94 let list_mk_conj = end_itlist (curry mk_conj);;
  95
  96 let CONJ =
  97   let f = `f:bool->bool->bool`
  98   and p = `p:bool`
  99   and q = `q:bool` in
 100   let pth =
 101     let pth = ASSUME p
 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));;
 111
 112 let CONJUNCT1 =
 113   let P = `P:bool` and Q = `Q:bool` in
 114   let pth =
 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));;
 123
 124 let CONJUNCT2 =
 125   let P = `P:bool` and Q = `Q:bool` in
 126   let pth =
 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));;
 135
 136 let CONJ_PAIR th =
 137   try CONJUNCT1 th,CONJUNCT2 th
 138   with Failure _ -> failwith "CONJ_PAIR: Not a conjunction";;
 139
 140 let CONJUNCTS = striplist CONJ_PAIR;;
 141
 142 (* ------------------------------------------------------------------------- *)
 143 (* Rules for ==>                                                             *)
 144 (* ------------------------------------------------------------------------- *)
 145
 146 let IMP_DEF = new_basic_definition
 147   `(==>) = \p q. p /\ q <=> p`;;
 148
 149 let mk_imp = mk_binary "==>";;
 150
 151 let MP =
 152   let p = `p:bool`
 153   and q = `q:bool` in
 154   let pth =
 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
 158   fun ith th ->
 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";;
 163
 164 let DISCH =
 165   let p = `p:bool`
 166   and q = `q:bool` in
 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);;
 174
 175 let rec DISCH_ALL th =
 176   try DISCH_ALL (DISCH (hd (hyp th)) th)
 177   with Failure _ -> th;;
 178
 179 let UNDISCH th =
 180   try MP th (ASSUME(rand(rator(concl th))))
 181   with Failure _ -> failwith "UNDISCH";;
 182
 183 let rec UNDISCH_ALL th =
 184   if is_imp (concl th) then UNDISCH_ALL (UNDISCH th)
 185   else th;;
 186
 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));;
 190
 191 let ADD_ASSUM tm th = MP (DISCH tm th) (ASSUME tm);;
 192
 193 let EQ_IMP_RULE th =
 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";;
 197
 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";;
 202
 203 (* ------------------------------------------------------------------------- *)
 204 (* Rules for !                                                               *)
 205 (* ------------------------------------------------------------------------- *)
 206
 207 let FORALL_DEF = new_basic_definition
 208  `(!) = \P:A->bool. P = \x. T`;;
 209
 210 let mk_forall = mk_binder "!";;
 211 let list_mk_forall(vs,bod) = itlist (curry mk_forall) vs bod;;
 212
 213 let SPEC =
 214   let P = `P:A->bool`
 215   and x = `x:A` in
 216   let pth =
 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
 221   fun tm th ->
 222     (substitute_proof (try let abs = rand(concl th) in
 223         CONV_RULE BETA_CONV
 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)));;
 226
 227 let SPECL tms th =
 228   try rev_itlist SPEC tms th
 229   with Failure _ -> failwith "SPECL";;
 230
 231 let SPEC_VAR th =
 232   let bv = variant (thm_frees th) (bndvar(rand(concl th))) in
 233   bv,SPEC bv th;;
 234
 235 let rec SPEC_ALL th =
 236   if is_forall(concl th) then SPEC_ALL(snd(SPEC_VAR th)) else th;;
 237
 238 let ISPEC t 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";;
 245
 246 let ISPECL tms th =
 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";;
 253
 254 let GEN =
 255   let P = `P:A->bool` and true_tm = `T` in
 256   let pth =
 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
 265         MP th3 th2
 266     with Failure _ -> failwith "GEN") (proof_GEN (proof_of th) x);;
 267
 268 let GENL = itlist GEN;;
 269
 270 let GEN_ALL th =
 271   let asl,c = dest_thm th in
 272   let vars = subtract (frees c) (freesl asl) in
 273   GENL vars th;;
 274
 275 (* ------------------------------------------------------------------------- *)
 276 (* Rules for ?                                                               *)
 277 (* ------------------------------------------------------------------------- *)
 278
 279 let EXISTS_DEF = new_basic_definition
 280  `(?) = \P:A->bool. !q. (!x. P x ==> q) ==> q`;;
 281
 282 let mk_exists =  mk_binder "?";;
 283 let list_mk_exists(vs,bod) =  itlist (curry mk_exists) vs bod;;
 284
 285 let EXISTS =
 286   let P = `P:A->bool` and x = `x:A` and PX = `(P:A->bool) x` in
 287   let pth =
 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));;
 298
 299 let SIMPLE_EXISTS v th =
 300   EXISTS (mk_exists(v,concl th),v) th;;
 301
 302 let CHOOSE =
 303   let P = `P:A->bool` and Q = `Q:bool` in
 304   let pth =
 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
 316         MP (MP th5 th4) th1
 317     with Failure _ -> failwith "CHOOSE")
 318       (proof_CHOOSE v (proof_of th1) (proof_of th2));;
 319
 320 let SIMPLE_CHOOSE v th =
 321   CHOOSE(v,ASSUME (mk_exists(v,hd(hyp th)))) th;;
 322
 323 (* ------------------------------------------------------------------------- *)
 324 (* Rules for \/                                                              *)
 325 (* ------------------------------------------------------------------------- *)
 326
 327 let OR_DEF = new_basic_definition
 328  `(\/) = \p q. !r. (p ==> r) ==> (q ==> r) ==> r`;;
 329
 330 let mk_disj = mk_binary "\\/";;
 331 let list_mk_disj = end_itlist (curry mk_disj);;
 332
 333 let DISJ1 =
 334   let P = `P:bool` and Q = `Q:bool` in
 335   let pth =
 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);;
 344
 345 let DISJ2 =
 346   let P = `P:bool` and Q = `Q:bool` in
 347   let pth =
 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);;
 356
 357 let DISJ_CASES =
 358   let P = `P:bool` and Q = `Q:bool` and R = `R:bool` in
 359   let pth =
 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));;
 372
 373 let SIMPLE_DISJ_CASES th1 th2 =
 374   DISJ_CASES (ASSUME(mk_disj(hd(hyp th1),hd(hyp th2)))) th1 th2;;
 375
 376 (* ------------------------------------------------------------------------- *)
 377 (* Rules for negation and falsity.                                           *)
 378 (* ------------------------------------------------------------------------- *)
 379
 380 let F_DEF = new_basic_definition
 381  `F = !p:bool. p`;;
 382
 383 let NOT_DEF = new_basic_definition
 384  `(~) = \p. p ==> F`;;
 385
 386 let mk_neg =
 387   let neg_tm = `(~)` in
 388   fun tm -> try mk_comb(neg_tm,tm)
 389             with Failure _ -> failwith "mk_neg";;
 390
 391 let NOT_ELIM =
 392   let P = `P:bool` in
 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));;
 397
 398 let NOT_INTRO =
 399   let P = `P:bool` in
 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));;
 404
 405 let EQF_INTRO =
 406   let P = `P:bool` in
 407   let pth =
 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
 411   fun th ->
 412     try MP (INST [rand(concl th),P] pth) th
 413     with Failure _ -> failwith "EQF_INTRO";;
 414
 415 let EQF_ELIM =
 416   let P = `P:bool` in
 417   let pth =
 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
 421   fun th ->
 422     try MP (INST [rand(rator(concl th)),P] pth) th
 423     with Failure _ -> failwith "EQF_ELIM";;
 424
 425 let CONTR =
 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);;
 431
 432 (* ------------------------------------------------------------------------- *)
 433 (* Rules for unique existence.                                               *)
 434 (* ------------------------------------------------------------------------- *)
 435
 436 let EXISTS_UNIQUE_DEF = new_basic_definition
 437  `(?!) = \P:A->bool. ((?) P) /\ (!x y. P x /\ P y ==> x = y)`;;
 438
 439 let mk_uexists = mk_binder "?!";;
 440
 441 let EXISTENCE =
 442   let P = `P:A->bool` in
 443   let pth =
 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
 447   fun th ->
 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";;