canon.ml

   1 (* ========================================================================= *)
   2 (* Reasonably efficient conversions for various canonical forms.             *)
   3 (*                                                                           *)
   4 (*       John Harrison, University of Cambridge Computer Laboratory          *)
   5 (*                                                                           *)
   6 (*            (c) Copyright, University of Cambridge 1998                    *)
   7 (*              (c) Copyright, John Harrison 1998-2007                       *)
   8 (* ========================================================================= *)
   9
  10 needs "trivia.ml";;
  11
  12 (* ------------------------------------------------------------------------- *)
  13 (* Pre-simplification.                                                       *)
  14 (* ------------------------------------------------------------------------- *)
  15
  16 let PRESIMP_CONV =
  17   GEN_REWRITE_CONV TOP_DEPTH_CONV
  18    [NOT_CLAUSES; AND_CLAUSES; OR_CLAUSES; IMP_CLAUSES; EQ_CLAUSES;
  19     FORALL_SIMP; EXISTS_SIMP; EXISTS_OR_THM; FORALL_AND_THM;
  20     LEFT_EXISTS_AND_THM; RIGHT_EXISTS_AND_THM;
  21     LEFT_FORALL_OR_THM; RIGHT_FORALL_OR_THM];;
  22
  23 (* ------------------------------------------------------------------------- *)
  24 (* ACI rearrangements of conjunctions and disjunctions. This is much faster  *)
  25 (* than AC xxx_ACI on large problems, as well as being more controlled.      *)
  26 (* ------------------------------------------------------------------------- *)
  27
  28 let CONJ_ACI_RULE =
  29   let rec mk_fun th fn =
  30     let tm = concl th in
  31     if is_conj tm then
  32       let th1,th2 = CONJ_PAIR th in
  33       mk_fun th1 (mk_fun th2 fn)
  34     else (tm |-> th) fn
  35   and use_fun fn tm =
  36     if is_conj tm then
  37       let l,r = dest_conj tm in CONJ (use_fun fn l) (use_fun fn r)
  38     else apply fn tm in
  39   fun fm ->
  40     let p,p' = dest_eq fm in
  41     if p = p' then REFL p else
  42     let th = use_fun (mk_fun (ASSUME p) undefined) p'
  43     and th' = use_fun (mk_fun (ASSUME p') undefined) p in
  44     IMP_ANTISYM_RULE (DISCH_ALL th) (DISCH_ALL th');;
  45
  46 let DISJ_ACI_RULE =
  47   let pth_left = UNDISCH(TAUT `~(a \/ b) ==> ~a`)
  48   and pth_right = UNDISCH(TAUT `~(a \/ b) ==> ~b`)
  49   and pth = repeat UNDISCH (TAUT `~a ==> ~b ==> ~(a \/ b)`)
  50   and pth_neg = UNDISCH(TAUT `(~a <=> ~b) ==> (a <=> b)`)
  51   and a_tm = `a:bool` and b_tm = `b:bool` in
  52   let NOT_DISJ_PAIR th =
  53     let p,q = dest_disj(rand(concl th)) in
  54     let ilist = [p,a_tm; q,b_tm] in
  55     PROVE_HYP th (INST ilist pth_left),
  56     PROVE_HYP th (INST ilist pth_right)
  57   and NOT_DISJ th1 th2 =
  58     let th3 = INST [rand(concl th1),a_tm; rand(concl th2),b_tm] pth in
  59     PROVE_HYP th1 (PROVE_HYP th2 th3) in
  60   let rec mk_fun th fn =
  61     let tm = rand(concl th) in
  62     if is_disj tm then
  63       let th1,th2 = NOT_DISJ_PAIR th in
  64       mk_fun th1 (mk_fun th2 fn)
  65     else (tm |-> th) fn
  66   and use_fun fn tm =
  67     if is_disj tm then
  68       let l,r = dest_disj tm in NOT_DISJ (use_fun fn l) (use_fun fn r)
  69     else apply fn tm in
  70   fun fm ->
  71     let p,p' = dest_eq fm in
  72     if p = p' then REFL p else
  73     let th = use_fun (mk_fun (ASSUME(mk_neg p)) undefined) p'
  74     and th' = use_fun (mk_fun (ASSUME(mk_neg p')) undefined) p in
  75     let th1 = IMP_ANTISYM_RULE (DISCH_ALL th) (DISCH_ALL th') in
  76     PROVE_HYP th1 (INST [p,a_tm; p',b_tm] pth_neg);;
  77
  78 (* ------------------------------------------------------------------------- *)
  79 (* Order canonically, right-associate and remove duplicates.                 *)
  80 (* ------------------------------------------------------------------------- *)
  81
  82 let CONJ_CANON_CONV tm =
  83   let tm' = list_mk_conj(setify(conjuncts tm)) in
  84   CONJ_ACI_RULE(mk_eq(tm,tm'));;
  85
  86 let DISJ_CANON_CONV tm =
  87   let tm' = list_mk_disj(setify(disjuncts tm)) in
  88   DISJ_ACI_RULE(mk_eq(tm,tm'));;
  89
  90 (* ------------------------------------------------------------------------- *)
  91 (* General NNF conversion. The user supplies some conversion to be applied   *)
  92 (* to atomic formulas.                                                       *)
  93 (*                                                                           *)
  94 (* "Iff"s are split conjunctively or disjunctively according to the flag     *)
  95 (* argument (conjuctively = true) until a universal quantifier (modulo       *)
  96 (* current parity) is passed; after that they are split conjunctively. This  *)
  97 (* is appropriate when the result is passed to a disjunctive splitter        *)
  98 (* followed by a clausal form inner core, such as MESON.                     *)
  99 (*                                                                           *)
 100 (* To avoid some duplicate computation, this function will in general        *)
 101 (* enter a recursion where it simultaneously computes NNF representations    *)
 102 (* for "p" and "~p", so the user needs to supply an atomic "conversion"      *)
 103 (* that does the same.                                                       *)
 104 (* ------------------------------------------------------------------------- *)
 105
 106 let (GEN_NNF_CONV:bool->conv*(term->thm*thm)->conv) =
 107   let and_tm = `(/\)` and or_tm = `(\/)` and not_tm = `(~)`
 108   and pth_not_not = TAUT `~ ~ p = p`
 109   and pth_not_and = TAUT `~(p /\ q) <=> ~p \/ ~q`
 110   and pth_not_or = TAUT `~(p \/ q) <=> ~p /\ ~q`
 111   and pth_imp = TAUT `p ==> q <=> ~p \/ q`
 112   and pth_not_imp = TAUT `~(p ==> q) <=> p /\ ~q`
 113   and pth_eq = TAUT `(p <=> q) <=> p /\ q \/ ~p /\ ~q`
 114   and pth_not_eq = TAUT `~(p <=> q) <=> p /\ ~q \/ ~p /\ q`
 115   and pth_eq' = TAUT `(p <=> q) <=> (p \/ ~q) /\ (~p \/ q)`
 116   and pth_not_eq' = TAUT `~(p <=> q) <=> (p \/ q) /\ (~p \/ ~q)`
 117   and [pth_not_forall; pth_not_exists; pth_not_exu] =
 118    (CONJUNCTS o prove)
 119    (`(~((!) P) <=> ?x:A. ~(P x)) /\
 120      (~((?) P) <=> !x:A. ~(P x)) /\
 121      (~((?!) P) <=> (!x:A. ~(P x)) \/ ?x y. P x /\ P y /\ ~(y = x))`,
 122     REPEAT CONJ_TAC THEN
 123     GEN_REWRITE_TAC (LAND_CONV o funpow 2 RAND_CONV) [GSYM ETA_AX] THEN
 124     REWRITE_TAC[NOT_EXISTS_THM; NOT_FORALL_THM; EXISTS_UNIQUE_DEF;
 125                 DE_MORGAN_THM; NOT_IMP] THEN
 126     REWRITE_TAC[CONJ_ASSOC; EQ_SYM_EQ])
 127   and pth_exu = prove
 128    (`((?!) P) <=> (?x:A. P x) /\ !x y. ~(P x) \/ ~(P y) \/ (y = x)`,
 129     GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM ETA_AX] THEN
 130     REWRITE_TAC[EXISTS_UNIQUE_DEF; TAUT `a /\ b ==> c <=> ~a \/ ~b \/ c`] THEN
 131     REWRITE_TAC[EQ_SYM_EQ])
 132   and p_tm = `p:bool` and q_tm = `q:bool` in
 133   let rec NNF_DCONV cf baseconvs tm =
 134     match tm with
 135       Comb(Comb(Const("/\\",_),l),r) ->
 136           let th_lp,th_ln = NNF_DCONV cf baseconvs l
 137           and th_rp,th_rn = NNF_DCONV cf baseconvs r in
 138           MK_COMB(AP_TERM and_tm th_lp,th_rp),
 139           TRANS (INST [l,p_tm; r,q_tm] pth_not_and)
 140                 (MK_COMB(AP_TERM or_tm th_ln,th_rn))
 141     | Comb(Comb(Const("\\/",_),l),r) ->
 142           let th_lp,th_ln = NNF_DCONV cf baseconvs l
 143           and th_rp,th_rn = NNF_DCONV cf baseconvs r in
 144           MK_COMB(AP_TERM or_tm th_lp,th_rp),
 145           TRANS (INST [l,p_tm; r,q_tm] pth_not_or)
 146                 (MK_COMB(AP_TERM and_tm th_ln,th_rn))
 147     | Comb(Comb(Const("==>",_),l),r) ->
 148           let th_lp,th_ln = NNF_DCONV cf baseconvs l
 149           and th_rp,th_rn = NNF_DCONV cf baseconvs r in
 150           TRANS (INST [l,p_tm; r,q_tm] pth_imp)
 151                 (MK_COMB(AP_TERM or_tm th_ln,th_rp)),
 152           TRANS (INST [l,p_tm; r,q_tm] pth_not_imp)
 153                 (MK_COMB(AP_TERM and_tm th_lp,th_rn))
 154     | Comb(Comb(Const("=",Tyapp("fun",Tyapp("bool",_)::_)),l),r) ->
 155           let th_lp,th_ln = NNF_DCONV cf baseconvs l
 156           and th_rp,th_rn = NNF_DCONV cf baseconvs r in
 157           if cf then
 158             TRANS (INST [l,p_tm; r,q_tm] pth_eq')
 159                   (MK_COMB(AP_TERM and_tm (MK_COMB(AP_TERM or_tm th_lp,th_rn)),
 160                            MK_COMB(AP_TERM or_tm th_ln,th_rp))),
 161             TRANS (INST [l,p_tm; r,q_tm] pth_not_eq')
 162                   (MK_COMB(AP_TERM and_tm (MK_COMB(AP_TERM or_tm th_lp,th_rp)),
 163                            MK_COMB(AP_TERM or_tm th_ln,th_rn)))
 164           else
 165             TRANS (INST [l,p_tm; r,q_tm] pth_eq)
 166                   (MK_COMB(AP_TERM or_tm (MK_COMB(AP_TERM and_tm th_lp,th_rp)),
 167                            MK_COMB(AP_TERM and_tm th_ln,th_rn))),
 168             TRANS (INST [l,p_tm; r,q_tm] pth_not_eq)
 169                   (MK_COMB(AP_TERM or_tm (MK_COMB(AP_TERM and_tm th_lp,th_rn)),
 170                            MK_COMB(AP_TERM and_tm th_ln,th_rp)))
 171     | Comb(Const("!",Tyapp("fun",Tyapp("fun",ty::_)::_)) as q,
 172            (Abs(x,t) as bod)) ->
 173           let th_p,th_n = NNF_DCONV true baseconvs t in
 174           AP_TERM q (ABS x th_p),
 175           let th1 = INST [bod,mk_var("P",mk_fun_ty ty bool_ty)]
 176                          (INST_TYPE [ty,aty] pth_not_forall)
 177           and th2 = TRANS (AP_TERM not_tm (BETA(mk_comb(bod,x)))) th_n in
 178           TRANS th1 (MK_EXISTS x th2)
 179     | Comb(Const("?",Tyapp("fun",Tyapp("fun",ty::_)::_)) as q,
 180            (Abs(x,t) as bod)) ->
 181           let th_p,th_n = NNF_DCONV cf baseconvs t in
 182           AP_TERM q (ABS x th_p),
 183           let th1 = INST [bod,mk_var("P",mk_fun_ty ty bool_ty)]
 184                          (INST_TYPE [ty,aty] pth_not_exists)
 185           and th2 = TRANS (AP_TERM not_tm (BETA(mk_comb(bod,x)))) th_n in
 186           TRANS th1 (MK_FORALL x th2)
 187     | Comb(Const("?!",Tyapp("fun",Tyapp("fun",ty::_)::_)),
 188            (Abs(x,t) as bod)) ->
 189           let y = variant (x::frees t) x
 190           and th_p,th_n = NNF_DCONV cf baseconvs t in
 191           let eq = mk_eq(y,x) in
 192           let eth_p,eth_n = baseconvs eq
 193           and bth = BETA (mk_comb(bod,x))
 194           and bth' = BETA_CONV(mk_comb(bod,y)) in
 195           let th_p' = INST [y,x] th_p and th_n' = INST [y,x] th_n in
 196           let th1 = INST [bod,mk_var("P",mk_fun_ty ty bool_ty)]
 197                          (INST_TYPE [ty,aty] pth_exu)
 198           and th1' = INST [bod,mk_var("P",mk_fun_ty ty bool_ty)]
 199                           (INST_TYPE [ty,aty] pth_not_exu)
 200           and th2 =
 201             MK_COMB(AP_TERM and_tm
 202                         (MK_EXISTS x (TRANS bth th_p)),
 203                     MK_FORALL x (MK_FORALL y
 204                      (MK_COMB(AP_TERM or_tm (TRANS (AP_TERM not_tm bth) th_n),
 205                               MK_COMB(AP_TERM or_tm
 206                                     (TRANS (AP_TERM not_tm bth') th_n'),
 207                                       eth_p)))))
 208           and th2' =
 209             MK_COMB(AP_TERM or_tm
 210                         (MK_FORALL x (TRANS (AP_TERM not_tm bth) th_n)),
 211                     MK_EXISTS x (MK_EXISTS y
 212                      (MK_COMB(AP_TERM and_tm (TRANS bth th_p),
 213                               MK_COMB(AP_TERM and_tm (TRANS bth' th_p'),
 214                                       eth_n))))) in
 215           TRANS th1 th2,TRANS th1' th2'
 216     | Comb(Const("~",_),t) ->
 217           let th1,th2 = NNF_DCONV cf baseconvs t in
 218           th2,TRANS (INST [t,p_tm] pth_not_not) th1
 219     | _ -> try baseconvs tm
 220            with Failure _ -> REFL tm,REFL(mk_neg tm) in
 221   let rec NNF_CONV cf (base1,base2 as baseconvs) tm =
 222     match tm with
 223       Comb(Comb(Const("/\\",_),l),r) ->
 224           let th_lp = NNF_CONV cf baseconvs l
 225           and th_rp = NNF_CONV cf baseconvs r in
 226           MK_COMB(AP_TERM and_tm th_lp,th_rp)
 227     | Comb(Comb(Const("\\/",_),l),r) ->
 228           let th_lp = NNF_CONV cf baseconvs l
 229           and th_rp = NNF_CONV cf baseconvs r in
 230           MK_COMB(AP_TERM or_tm th_lp,th_rp)
 231     | Comb(Comb(Const("==>",_),l),r) ->
 232           let th_ln = NNF_CONV' cf baseconvs l
 233           and th_rp = NNF_CONV cf baseconvs r in
 234           TRANS (INST [l,p_tm; r,q_tm] pth_imp)
 235                 (MK_COMB(AP_TERM or_tm th_ln,th_rp))
 236     | Comb(Comb(Const("=",Tyapp("fun",Tyapp("bool",_)::_)),l),r) ->
 237           let th_lp,th_ln = NNF_DCONV cf base2 l
 238           and th_rp,th_rn = NNF_DCONV cf base2 r in
 239           if cf then
 240             TRANS (INST [l,p_tm; r,q_tm] pth_eq')
 241                   (MK_COMB(AP_TERM and_tm (MK_COMB(AP_TERM or_tm th_lp,th_rn)),
 242                            MK_COMB(AP_TERM or_tm th_ln,th_rp)))
 243           else
 244             TRANS (INST [l,p_tm; r,q_tm] pth_eq)
 245                   (MK_COMB(AP_TERM or_tm (MK_COMB(AP_TERM and_tm th_lp,th_rp)),
 246                            MK_COMB(AP_TERM and_tm th_ln,th_rn)))
 247     | Comb(Const("!",Tyapp("fun",Tyapp("fun",ty::_)::_)) as q,
 248            (Abs(x,t))) ->
 249           let th_p = NNF_CONV true baseconvs t in
 250           AP_TERM q (ABS x th_p)
 251     | Comb(Const("?",Tyapp("fun",Tyapp("fun",ty::_)::_)) as q,
 252            (Abs(x,t))) ->
 253           let th_p = NNF_CONV cf baseconvs t in
 254           AP_TERM q (ABS x th_p)
 255     | Comb(Const("?!",Tyapp("fun",Tyapp("fun",ty::_)::_)),
 256            (Abs(x,t) as bod)) ->
 257           let y = variant (x::frees t) x
 258           and th_p,th_n = NNF_DCONV cf base2 t in
 259           let eq = mk_eq(y,x) in
 260           let eth_p,eth_n = base2 eq
 261           and bth = BETA (mk_comb(bod,x))
 262           and bth' = BETA_CONV(mk_comb(bod,y)) in
 263           let th_n' = INST [y,x] th_n in
 264           let th1 = INST [bod,mk_var("P",mk_fun_ty ty bool_ty)]
 265                          (INST_TYPE [ty,aty] pth_exu)
 266           and th2 =
 267             MK_COMB(AP_TERM and_tm
 268                         (MK_EXISTS x (TRANS bth th_p)),
 269                     MK_FORALL x (MK_FORALL y
 270                      (MK_COMB(AP_TERM or_tm (TRANS (AP_TERM not_tm bth) th_n),
 271                               MK_COMB(AP_TERM or_tm
 272                                     (TRANS (AP_TERM not_tm bth') th_n'),
 273                                       eth_p))))) in
 274           TRANS th1 th2
 275     | Comb(Const("~",_),t) -> NNF_CONV' cf baseconvs t
 276     | _ -> try base1 tm with Failure _ -> REFL tm
 277   and NNF_CONV' cf (base1,base2 as baseconvs) tm =
 278     match tm with
 279       Comb(Comb(Const("/\\",_),l),r) ->
 280           let th_ln = NNF_CONV' cf baseconvs l
 281           and th_rn = NNF_CONV' cf baseconvs r in
 282           TRANS (INST [l,p_tm; r,q_tm] pth_not_and)
 283                 (MK_COMB(AP_TERM or_tm th_ln,th_rn))
 284     | Comb(Comb(Const("\\/",_),l),r) ->
 285           let th_ln = NNF_CONV' cf baseconvs l
 286           and th_rn = NNF_CONV' cf baseconvs r in
 287           TRANS (INST [l,p_tm; r,q_tm] pth_not_or)
 288                 (MK_COMB(AP_TERM and_tm th_ln,th_rn))
 289     | Comb(Comb(Const("==>",_),l),r) ->
 290           let th_lp = NNF_CONV cf baseconvs l
 291           and th_rn = NNF_CONV' cf baseconvs r in
 292           TRANS (INST [l,p_tm; r,q_tm] pth_not_imp)
 293                 (MK_COMB(AP_TERM and_tm th_lp,th_rn))
 294     | Comb(Comb(Const("=",Tyapp("fun",Tyapp("bool",_)::_)),l),r) ->
 295           let th_lp,th_ln = NNF_DCONV cf base2 l
 296           and th_rp,th_rn = NNF_DCONV cf base2 r in
 297           if cf then
 298             TRANS (INST [l,p_tm; r,q_tm] pth_not_eq')
 299                   (MK_COMB(AP_TERM and_tm (MK_COMB(AP_TERM or_tm th_lp,th_rp)),
 300                            MK_COMB(AP_TERM or_tm th_ln,th_rn)))
 301           else
 302             TRANS (INST [l,p_tm; r,q_tm] pth_not_eq)
 303                   (MK_COMB(AP_TERM or_tm (MK_COMB(AP_TERM and_tm th_lp,th_rn)),
 304                            MK_COMB(AP_TERM and_tm th_ln,th_rp)))
 305     | Comb(Const("!",Tyapp("fun",Tyapp("fun",ty::_)::_)),
 306            (Abs(x,t) as bod)) ->
 307           let th_n = NNF_CONV' cf baseconvs t in
 308           let th1 = INST [bod,mk_var("P",mk_fun_ty ty bool_ty)]
 309                          (INST_TYPE [ty,aty] pth_not_forall)
 310           and th2 = TRANS (AP_TERM not_tm (BETA(mk_comb(bod,x)))) th_n in
 311           TRANS th1 (MK_EXISTS x th2)
 312     | Comb(Const("?",Tyapp("fun",Tyapp("fun",ty::_)::_)),
 313            (Abs(x,t) as bod)) ->
 314           let th_n = NNF_CONV' true baseconvs t in
 315           let th1 = INST [bod,mk_var("P",mk_fun_ty ty bool_ty)]
 316                          (INST_TYPE [ty,aty] pth_not_exists)
 317           and th2 = TRANS (AP_TERM not_tm (BETA(mk_comb(bod,x)))) th_n in
 318           TRANS th1 (MK_FORALL x th2)
 319     | Comb(Const("?!",Tyapp("fun",Tyapp("fun",ty::_)::_)),
 320            (Abs(x,t) as bod)) ->
 321           let y = variant (x::frees t) x
 322           and th_p,th_n = NNF_DCONV cf base2 t in
 323           let eq = mk_eq(y,x) in
 324           let eth_p,eth_n = base2 eq
 325           and bth = BETA (mk_comb(bod,x))
 326           and bth' = BETA_CONV(mk_comb(bod,y)) in
 327           let th_p' = INST [y,x] th_p in
 328           let th1' = INST [bod,mk_var("P",mk_fun_ty ty bool_ty)]
 329                           (INST_TYPE [ty,aty] pth_not_exu)
 330           and th2' =
 331             MK_COMB(AP_TERM or_tm
 332                         (MK_FORALL x (TRANS (AP_TERM not_tm bth) th_n)),
 333                     MK_EXISTS x (MK_EXISTS y
 334                      (MK_COMB(AP_TERM and_tm (TRANS bth th_p),
 335                               MK_COMB(AP_TERM and_tm (TRANS bth' th_p'),
 336                                       eth_n))))) in
 337           TRANS th1' th2'
 338     | Comb(Const("~",_),t) ->
 339           let th1 = NNF_CONV cf baseconvs t in
 340           TRANS (INST [t,p_tm] pth_not_not) th1
 341     | _ -> let tm' = mk_neg tm in try base1 tm' with Failure _ -> REFL tm' in
 342   NNF_CONV;;
 343
 344 (* ------------------------------------------------------------------------- *)
 345 (* Some common special cases.                                                *)
 346 (* ------------------------------------------------------------------------- *)
 347
 348 let NNF_CONV =
 349   (GEN_NNF_CONV false (ALL_CONV,fun t -> REFL t,REFL(mk_neg t)) :conv);;
 350
 351 let NNFC_CONV =
 352   (GEN_NNF_CONV true (ALL_CONV,fun t -> REFL t,REFL(mk_neg t)) :conv);;
 353
 354 (* ------------------------------------------------------------------------- *)
 355 (* Skolemize a term already in NNF (doesn't matter if it's not prenex).      *)
 356 (* ------------------------------------------------------------------------- *)
 357
 358 let SKOLEM_CONV =
 359   GEN_REWRITE_CONV TOP_DEPTH_CONV
 360    [EXISTS_OR_THM; LEFT_EXISTS_AND_THM; RIGHT_EXISTS_AND_THM;
 361     FORALL_AND_THM; LEFT_FORALL_OR_THM; RIGHT_FORALL_OR_THM;
 362     FORALL_SIMP; EXISTS_SIMP] THENC
 363   GEN_REWRITE_CONV REDEPTH_CONV
 364    [RIGHT_AND_EXISTS_THM;
 365     LEFT_AND_EXISTS_THM;
 366     OR_EXISTS_THM;
 367     RIGHT_OR_EXISTS_THM;
 368     LEFT_OR_EXISTS_THM;
 369     SKOLEM_THM];;
 370
 371 (* ------------------------------------------------------------------------- *)
 372 (* Put a term already in NNF into prenex form.                               *)
 373 (* ------------------------------------------------------------------------- *)
 374
 375 let PRENEX_CONV =
 376   GEN_REWRITE_CONV REDEPTH_CONV
 377    [AND_FORALL_THM; LEFT_AND_FORALL_THM; RIGHT_AND_FORALL_THM;
 378     LEFT_OR_FORALL_THM; RIGHT_OR_FORALL_THM;
 379     OR_EXISTS_THM; LEFT_OR_EXISTS_THM; RIGHT_OR_EXISTS_THM;
 380     LEFT_AND_EXISTS_THM; RIGHT_AND_EXISTS_THM];;
 381
 382 (* ------------------------------------------------------------------------- *)
 383 (* Weak and normal DNF conversion. The "weak" form gives a disjunction of    *)
 384 (* conjunctions, but has no particular associativity at either level and     *)
 385 (* may contain duplicates. The regular forms give canonical right-associate  *)
 386 (* lists without duplicates, but do not remove subsumed disjuncts.           *)
 387 (*                                                                           *)
 388 (* In both cases the input term is supposed to be in NNF already. We do go   *)
 389 (* inside quantifiers and transform their body, but don't move them.         *)
 390 (* ------------------------------------------------------------------------- *)
 391
 392 let WEAK_DNF_CONV,DNF_CONV =
 393   let pth1 = TAUT `a /\ (b \/ c) <=> a /\ b \/ a /\ c`
 394   and pth2 = TAUT `(a \/ b) /\ c <=> a /\ c \/ b /\ c`
 395   and a_tm = `a:bool` and b_tm = `b:bool` and c_tm = `c:bool` in
 396   let rec distribute tm =
 397     match tm with
 398       Comb(Comb(Const("/\\",_),a),Comb(Comb(Const("\\/",_),b),c)) ->
 399           let th = INST [a,a_tm; b,b_tm; c,c_tm] pth1 in
 400           TRANS th (BINOP_CONV distribute (rand(concl th)))
 401     | Comb(Comb(Const("/\\",_),Comb(Comb(Const("\\/",_),a),b)),c) ->
 402           let th = INST [a,a_tm; b,b_tm; c,c_tm] pth2 in
 403           TRANS th (BINOP_CONV distribute (rand(concl th)))
 404     | _ -> REFL tm in
 405   let strengthen =
 406     DEPTH_BINOP_CONV `(\/)` CONJ_CANON_CONV THENC DISJ_CANON_CONV in
 407   let rec weakdnf tm =
 408     match tm with
 409       Comb(Const("!",_),Abs(_,_))
 410     | Comb(Const("?",_),Abs(_,_)) -> BINDER_CONV weakdnf tm
 411     | Comb(Comb(Const("\\/",_),_),_) -> BINOP_CONV weakdnf tm
 412     | Comb(Comb(Const("/\\",_) as op,l),r) ->
 413           let th = MK_COMB(AP_TERM op (weakdnf l),weakdnf r) in
 414           TRANS th (distribute(rand(concl th)))
 415     | _ -> REFL tm
 416   and substrongdnf tm =
 417     match tm with
 418       Comb(Const("!",_),Abs(_,_))
 419     | Comb(Const("?",_),Abs(_,_)) -> BINDER_CONV strongdnf tm
 420     | Comb(Comb(Const("\\/",_),_),_) -> BINOP_CONV substrongdnf tm
 421     | Comb(Comb(Const("/\\",_) as op,l),r) ->
 422           let th = MK_COMB(AP_TERM op (substrongdnf l),substrongdnf r) in
 423           TRANS th (distribute(rand(concl th)))
 424     | _ -> REFL tm
 425   and strongdnf tm =
 426     let th = substrongdnf tm in
 427     TRANS th (strengthen(rand(concl th))) in
 428   weakdnf,strongdnf;;
 429
 430 (* ------------------------------------------------------------------------- *)
 431 (* Likewise for CNF.                                                         *)
 432 (* ------------------------------------------------------------------------- *)
 433
 434 let WEAK_CNF_CONV,CNF_CONV =
 435   let pth1 = TAUT `a \/ (b /\ c) <=> (a \/ b) /\ (a \/ c)`
 436   and pth2 = TAUT `(a /\ b) \/ c <=> (a \/ c) /\ (b \/ c)`
 437   and a_tm = `a:bool` and b_tm = `b:bool` and c_tm = `c:bool` in
 438   let rec distribute tm =
 439     match tm with
 440       Comb(Comb(Const("\\/",_),a),Comb(Comb(Const("/\\",_),b),c)) ->
 441           let th = INST [a,a_tm; b,b_tm; c,c_tm] pth1 in
 442           TRANS th (BINOP_CONV distribute (rand(concl th)))
 443     | Comb(Comb(Const("\\/",_),Comb(Comb(Const("/\\",_),a),b)),c) ->
 444           let th = INST [a,a_tm; b,b_tm; c,c_tm] pth2 in
 445           TRANS th (BINOP_CONV distribute (rand(concl th)))
 446     | _ -> REFL tm in
 447   let strengthen =
 448     DEPTH_BINOP_CONV `(/\)` DISJ_CANON_CONV THENC CONJ_CANON_CONV in
 449   let rec weakcnf tm =
 450     match tm with
 451       Comb(Const("!",_),Abs(_,_))
 452     | Comb(Const("?",_),Abs(_,_)) -> BINDER_CONV weakcnf tm
 453     | Comb(Comb(Const("/\\",_),_),_) -> BINOP_CONV weakcnf tm
 454     | Comb(Comb(Const("\\/",_) as op,l),r) ->
 455           let th = MK_COMB(AP_TERM op (weakcnf l),weakcnf r) in
 456           TRANS th (distribute(rand(concl th)))
 457     | _ -> REFL tm
 458   and substrongcnf tm =
 459     match tm with
 460       Comb(Const("!",_),Abs(_,_))
 461     | Comb(Const("?",_),Abs(_,_)) -> BINDER_CONV strongcnf tm
 462     | Comb(Comb(Const("/\\",_),_),_) -> BINOP_CONV substrongcnf tm
 463     | Comb(Comb(Const("\\/",_) as op,l),r) ->
 464           let th = MK_COMB(AP_TERM op (substrongcnf l),substrongcnf r) in
 465           TRANS th (distribute(rand(concl th)))
 466     | _ -> REFL tm
 467   and strongcnf tm =
 468     let th = substrongcnf tm in
 469     TRANS th (strengthen(rand(concl th))) in
 470   weakcnf,strongcnf;;
 471
 472 (* ------------------------------------------------------------------------- *)
 473 (* Simply right-associate w.r.t. a binary operator.                          *)
 474 (* ------------------------------------------------------------------------- *)
 475
 476 let ASSOC_CONV th =
 477   let th' = SYM(SPEC_ALL th) in
 478   let opx,yopz = dest_comb(rhs(concl th')) in
 479   let op,x = dest_comb opx in
 480   let y = lhand yopz and z = rand yopz in
 481   let rec distrib tm =
 482     match tm with
 483       Comb(Comb(op',Comb(Comb(op'',p),q)),r) when op' = op & op'' = op ->
 484           let th1 = INST [p,x; q,y; r,z] th' in
 485           let l,r' = dest_comb(rand(concl th1)) in
 486           let th2 = AP_TERM l (distrib r') in
 487           let th3 = distrib(rand(concl th2)) in
 488           TRANS th1 (TRANS th2 th3)
 489     | _ -> REFL tm in
 490   let rec assoc tm =
 491     match tm with
 492       Comb(Comb(op',p) as l,q) when op' = op ->
 493           let th = AP_TERM l (assoc q) in
 494           TRANS th (distrib(rand(concl th)))
 495     | _ -> REFL tm in
 496   assoc;;
 497
 498 (* ------------------------------------------------------------------------- *)
 499 (* Eliminate select terms from a goal.                                       *)
 500 (* ------------------------------------------------------------------------- *)
 501
 502 let SELECT_ELIM_TAC =
 503   let SELECT_ELIM_CONV =
 504     let SELECT_ELIM_THM =
 505       let pth = prove
 506        (`(P:A->bool)((@) P) <=> (?) P`,
 507         REWRITE_TAC[EXISTS_THM] THEN BETA_TAC THEN REFL_TAC)
 508       and ptm = `P:A->bool` in
 509       fun tm -> let stm,atm = dest_comb tm in
 510                 if is_const stm & fst(dest_const stm) = "@" then
 511                  CONV_RULE(LAND_CONV BETA_CONV)
 512                    (PINST [type_of(bndvar atm),aty] [atm,ptm] pth)
 513                 else failwith "SELECT_ELIM_THM: not a select-term" in
 514     fun tm ->
 515       PURE_REWRITE_CONV (map SELECT_ELIM_THM (find_terms is_select tm)) tm in
 516   let SELECT_ELIM_ICONV =
 517     let SELECT_AX_THM =
 518       let pth = ISPEC `P:A->bool` SELECT_AX
 519       and ptm = `P:A->bool` in
 520       fun tm -> let stm,atm = dest_comb tm in
 521                 if is_const stm & fst(dest_const stm) = "@" then
 522                   let fvs = frees atm in
 523                   let th1 = PINST [type_of(bndvar atm),aty] [atm,ptm] pth in
 524                   let th2 = CONV_RULE(BINDER_CONV (BINOP_CONV BETA_CONV)) th1 in
 525                   GENL fvs th2
 526                 else failwith "SELECT_AX_THM: not a select-term" in
 527     let SELECT_ELIM_ICONV tm =
 528       let t = find_term is_select tm in
 529       let th1 = SELECT_AX_THM t in
 530       let itm = mk_imp(concl th1,tm) in
 531       let th2 = DISCH_ALL (MP (ASSUME itm) th1) in
 532       let fvs = frees t in
 533       let fty = itlist (mk_fun_ty o type_of) fvs (type_of t) in
 534       let fn = genvar fty
 535       and atm = list_mk_abs(fvs,t) in
 536       let rawdef = mk_eq(fn,atm) in
 537       let def = GENL fvs (SYM(RIGHT_BETAS fvs (ASSUME rawdef))) in
 538       let th3 = PURE_REWRITE_CONV[def] (lhand(concl th2)) in
 539       let gtm = mk_forall(fn,rand(concl th3)) in
 540       let th4 = EQ_MP (SYM th3) (SPEC fn (ASSUME gtm)) in
 541       let th5 = IMP_TRANS (DISCH gtm th4) th2 in
 542       MP (INST [atm,fn] (DISCH rawdef th5)) (REFL atm) in
 543     let rec SELECT_ELIMS_ICONV tm =
 544       try let th = SELECT_ELIM_ICONV tm in
 545           let tm' = lhand(concl th) in
 546           IMP_TRANS (SELECT_ELIMS_ICONV tm') th
 547       with Failure _ -> DISCH tm (ASSUME tm) in
 548     SELECT_ELIMS_ICONV in
 549   CONV_TAC SELECT_ELIM_CONV THEN W(MATCH_MP_TAC o SELECT_ELIM_ICONV o snd);;
 550
 551 (* ------------------------------------------------------------------------- *)
 552 (* Eliminate all lambda-terms except those part of quantifiers.              *)
 553 (* ------------------------------------------------------------------------- *)
 554
 555 let LAMBDA_ELIM_CONV =
 556   let HALF_MK_ABS_CONV =
 557     let pth = prove
 558      (`(s = \x. t x) <=> (!x. s x = t x)`,
 559       REWRITE_TAC[FUN_EQ_THM]) in
 560     let rec conv vs tm =
 561       if vs = [] then REFL tm else
 562       (GEN_REWRITE_CONV I [pth] THENC BINDER_CONV(conv (tl vs))) tm in
 563     conv in
 564   let rec find_lambda tm =
 565     if is_abs tm then tm
 566     else if is_var tm or is_const tm then failwith "find_lambda"
 567     else if is_abs tm then tm else
 568     if is_forall tm or is_exists tm or is_uexists tm
 569     then find_lambda (body(rand tm)) else
 570     let l,r = dest_comb tm in
 571     try find_lambda l with Failure _ -> find_lambda r in
 572   let rec ELIM_LAMBDA conv tm =
 573     try conv tm with Failure _ ->
 574     if is_abs tm then ABS_CONV (ELIM_LAMBDA conv) tm
 575     else if is_var tm or is_const tm then REFL tm else
 576     if is_forall tm or is_exists tm or is_uexists tm
 577     then BINDER_CONV (ELIM_LAMBDA conv) tm
 578     else COMB_CONV (ELIM_LAMBDA conv) tm in
 579   let APPLY_PTH =
 580     let pth = prove
 581      (`(!a. (a = c) ==> (P = Q a)) ==> (P <=> !a. (a = c) ==> Q a)`,
 582       SIMP_TAC[LEFT_FORALL_IMP_THM; EXISTS_REFL]) in
 583     MATCH_MP pth in
 584   let LAMB1_CONV tm =
 585     let atm = find_lambda tm in
 586     let v,bod = dest_abs atm in
 587     let vs = frees atm in
 588     let vs' = vs @ [v] in
 589     let aatm = list_mk_abs(vs,atm) in
 590     let f = genvar(type_of aatm) in
 591     let eq = mk_eq(f,aatm) in
 592     let th1 = SYM(RIGHT_BETAS vs (ASSUME eq)) in
 593     let th2 = ELIM_LAMBDA(GEN_REWRITE_CONV I [th1]) tm in
 594     let th3 = APPLY_PTH (GEN f (DISCH_ALL th2)) in
 595     CONV_RULE(RAND_CONV(BINDER_CONV(LAND_CONV (HALF_MK_ABS_CONV vs')))) th3 in
 596   let rec conv tm =
 597     try (LAMB1_CONV THENC conv) tm with Failure _ -> REFL tm in
 598   conv;;
 599
 600 (* ------------------------------------------------------------------------- *)
 601 (* Eliminate conditionals; CONDS_ELIM_CONV aims for disjunctive splitting,   *)
 602 (* for refutation procedures, and CONDS_CELIM_CONV for conjunctive.          *)
 603 (* Both switch modes "sensibly" when going through a quantifier.             *)
 604 (* ------------------------------------------------------------------------- *)
 605
 606 let CONDS_ELIM_CONV,CONDS_CELIM_CONV =
 607   let th_cond = prove
 608    (`((b <=> F) ==> x = x0) /\ ((b <=> T) ==> x = x1)
 609      ==> x = (b /\ x1 \/ ~b /\ x0)`,
 610     BOOL_CASES_TAC `b:bool` THEN ASM_REWRITE_TAC[])
 611   and th_cond' = prove
 612    (`((b <=> F) ==> x = x0) /\ ((b <=> T) ==> x = x1)
 613      ==> x = ((~b \/ x1) /\ (b \/ x0))`,
 614     BOOL_CASES_TAC `b:bool` THEN ASM_REWRITE_TAC[])
 615   and propsimps = basic_net()
 616   and false_tm = `F` and true_tm = `T` in
 617   let match_th = MATCH_MP th_cond and match_th' = MATCH_MP th_cond'
 618   and propsimp_conv = DEPTH_CONV(REWRITES_CONV propsimps)
 619   and proptsimp_conv =
 620     let cnv = TRY_CONV(REWRITES_CONV propsimps) in
 621     BINOP_CONV cnv THENC cnv in
 622   let rec find_conditional fvs tm =
 623     match tm with
 624       Comb(s,t) ->
 625         if is_cond tm & intersect (frees(lhand s)) fvs = [] then tm
 626         else (try (find_conditional fvs s)
 627               with Failure _ -> find_conditional fvs t)
 628     | Abs(x,t) -> find_conditional (x::fvs) t
 629     | _ -> failwith "find_conditional" in
 630   let rec CONDS_ELIM_CONV dfl tm =
 631     try let t = find_conditional [] tm in
 632         let p = lhand(rator t) in
 633         let th_new =
 634           if p = false_tm or p = true_tm then propsimp_conv tm else
 635           let asm_0 = mk_eq(p,false_tm) and asm_1 = mk_eq(p,true_tm) in
 636           let simp_0 = net_of_thm false (ASSUME asm_0) propsimps
 637           and simp_1 = net_of_thm false (ASSUME asm_1) propsimps in
 638           let th_0 = DISCH asm_0 (DEPTH_CONV(REWRITES_CONV simp_0) tm)
 639           and th_1 = DISCH asm_1 (DEPTH_CONV(REWRITES_CONV simp_1) tm) in
 640           let th_2 = CONJ th_0 th_1 in
 641           let th_3 = if dfl then match_th th_2 else match_th' th_2 in
 642           TRANS th_3 (proptsimp_conv(rand(concl th_3))) in
 643         CONV_RULE (RAND_CONV (CONDS_ELIM_CONV dfl)) th_new
 644     with Failure _ ->
 645     if is_neg tm then
 646        RAND_CONV (CONDS_ELIM_CONV (not dfl)) tm
 647     else if is_conj tm or is_disj tm then
 648        BINOP_CONV (CONDS_ELIM_CONV dfl) tm
 649     else if is_imp tm or is_iff tm then
 650        COMB2_CONV (RAND_CONV (CONDS_ELIM_CONV (not dfl)))
 651                   (CONDS_ELIM_CONV dfl) tm
 652     else if is_forall tm then
 653          BINDER_CONV (CONDS_ELIM_CONV false) tm
 654     else if is_exists tm or is_uexists tm then
 655          BINDER_CONV (CONDS_ELIM_CONV true) tm
 656     else REFL tm in
 657   CONDS_ELIM_CONV true,CONDS_ELIM_CONV false;;
 658
 659 (* ------------------------------------------------------------------------- *)
 660 (* Fix up all head arities to be consistent, in "first order logic" style.   *)
 661 (* Applied to the assumptions (not conclusion) in a goal.                    *)
 662 (* ------------------------------------------------------------------------- *)
 663
 664 let ASM_FOL_TAC =
 665   let rec get_heads lconsts tm (cheads,vheads as sofar) =
 666     try let v,bod = dest_forall tm in
 667         get_heads (subtract lconsts [v]) bod sofar
 668     with Failure _ -> try
 669         let l,r = try dest_conj tm with Failure _ -> dest_disj tm in
 670         get_heads lconsts l (get_heads lconsts r sofar)
 671     with Failure _ -> try
 672         let tm' = dest_neg tm in
 673         get_heads lconsts tm' sofar
 674     with Failure _ ->
 675         let hop,args = strip_comb tm in
 676         let len = length args in
 677         let newheads =
 678           if is_const hop or mem hop lconsts
 679           then (insert (hop,len) cheads,vheads)
 680           else if len > 0 then (cheads,insert (hop,len) vheads) else sofar in
 681         itlist (get_heads lconsts) args newheads in
 682   let get_thm_heads th sofar =
 683     get_heads (freesl(hyp th)) (concl th) sofar in
 684   let APP_CONV =
 685     let th = prove
 686      (`!(f:A->B) x. f x = I f x`,
 687       REWRITE_TAC[I_THM]) in
 688     REWR_CONV th in
 689   let rec APP_N_CONV n tm =
 690     if n = 1 then APP_CONV tm
 691     else (RATOR_CONV (APP_N_CONV (n - 1)) THENC APP_CONV) tm in
 692   let rec FOL_CONV hddata tm =
 693     if is_forall tm then BINDER_CONV (FOL_CONV hddata) tm
 694     else if is_conj tm or is_disj tm then BINOP_CONV (FOL_CONV hddata) tm else
 695     let op,args = strip_comb tm in
 696     let th = rev_itlist (C (curry MK_COMB))
 697                         (map (FOL_CONV hddata) args) (REFL op) in
 698     let tm' = rand(concl th) in
 699     let n = try length args - assoc op hddata with Failure _ -> 0 in
 700     if n = 0 then th
 701     else TRANS th (APP_N_CONV n tm') in
 702   let GEN_FOL_CONV (cheads,vheads) =
 703     let hddata =
 704       if vheads = [] then
 705         let hops = setify (map fst cheads) in
 706         let getmin h =
 707           let ns = mapfilter
 708             (fun (k,n) -> if k = h then n else fail()) cheads in
 709           if length ns < 2 then fail() else h,end_itlist min ns in
 710         mapfilter getmin hops
 711       else
 712         map (fun t -> if is_const t & fst(dest_const t) = "="
 713                       then t,2 else t,0)
 714             (setify (map fst (vheads @ cheads))) in
 715     FOL_CONV hddata in
 716   fun (asl,w as gl) ->
 717     let headsp = itlist (get_thm_heads o snd) asl ([],[]) in
 718     RULE_ASSUM_TAC(CONV_RULE(GEN_FOL_CONV headsp)) gl;;
 719
 720 (* ------------------------------------------------------------------------- *)
 721 (* Depth conversion to apply at "atomic" formulas in "first-order" term.     *)
 722 (* ------------------------------------------------------------------------- *)
 723
 724 let rec PROP_ATOM_CONV conv tm =
 725   match tm with
 726     Comb((Const("!",_) | Const("?",_) | Const("?!",_)),Abs(_,_))
 727       -> BINDER_CONV (PROP_ATOM_CONV conv) tm
 728   | Comb(Comb
 729      ((Const("/\\",_) | Const("\\/",_) | Const("==>",_) |
 730        (Const("=",Tyapp("fun",[Tyapp("bool",[]);_])))),_),_)
 731         -> BINOP_CONV (PROP_ATOM_CONV conv) tm
 732   | Comb(Const("~",_),_) -> RAND_CONV (PROP_ATOM_CONV conv) tm
 733   | _ -> TRY_CONV conv tm;;