(* ========================================================================= *)
(* Reasonably efficient conversions for various canonical forms.             *)
(*                                                                           *)
(*       John Harrison, University of Cambridge Computer Laboratory          *)
(*                                                                           *)
(*            (c) Copyright, University of Cambridge 1998                    *)
(*              (c) Copyright, John Harrison 1998-2007                       *)
(* ========================================================================= *)

needs "trivia.ml";;

(* ------------------------------------------------------------------------- *)
(* Pre-simplification.                                                       *)
(* ------------------------------------------------------------------------- *)

let PRESIMP_CONV =
  GEN_REWRITE_CONV TOP_DEPTH_CONV
   [NOT_CLAUSES; AND_CLAUSES; OR_CLAUSES; IMP_CLAUSES; EQ_CLAUSES;
    FORALL_SIMP; EXISTS_SIMP; EXISTS_OR_THM; FORALL_AND_THM;
    LEFT_EXISTS_AND_THM; RIGHT_EXISTS_AND_THM;
    LEFT_FORALL_OR_THM; RIGHT_FORALL_OR_THM];;

(* ------------------------------------------------------------------------- *)
(* ACI rearrangements of conjunctions and disjunctions. This is much faster  *)
(* than AC xxx_ACI on large problems, as well as being more controlled.      *)
(* ------------------------------------------------------------------------- *)

let CONJ_ACI_RULE =
  let rec mk_fun th fn =
    let tm = concl th in
    if is_conj tm then
      let th1,th2 = CONJ_PAIR th in
      mk_fun th1 (mk_fun th2 fn)
    else (tm |-> th) fn
  and use_fun fn tm =
    if is_conj tm then
      let l,r = dest_conj tm in CONJ (use_fun fn l) (use_fun fn r)
    else apply fn tm in
  fun fm ->
    let p,p' = dest_eq fm in
    if p = p' then REFL p else
    let th = use_fun (mk_fun (ASSUME p) undefined) p'
    and th' = use_fun (mk_fun (ASSUME p') undefined) p in
    IMP_ANTISYM_RULE (DISCH_ALL th) (DISCH_ALL th');;

let DISJ_ACI_RULE =
  let pth_left = UNDISCH(TAUT `~(a \/ b) ==> ~a`)
  and pth_right = UNDISCH(TAUT `~(a \/ b) ==> ~b`)
  and pth = repeat UNDISCH (TAUT `~a ==> ~b ==> ~(a \/ b)`)
  and pth_neg = UNDISCH(TAUT `(~a <=> ~b) ==> (a <=> b)`)
  and a_tm = `a:bool` and b_tm = `b:bool` in
  let NOT_DISJ_PAIR th =
    let p,q = dest_disj(rand(concl th)) in
    let ilist = [p,a_tm; q,b_tm] in
    PROVE_HYP th (INST ilist pth_left),
    PROVE_HYP th (INST ilist pth_right)
  and NOT_DISJ th1 th2 =
    let th3 = INST [rand(concl th1),a_tm; rand(concl th2),b_tm] pth in
    PROVE_HYP th1 (PROVE_HYP th2 th3) in
  let rec mk_fun th fn =
    let tm = rand(concl th) in
    if is_disj tm then
      let th1,th2 = NOT_DISJ_PAIR th in
      mk_fun th1 (mk_fun th2 fn)
    else (tm |-> th) fn
  and use_fun fn tm =
    if is_disj tm then
      let l,r = dest_disj tm in NOT_DISJ (use_fun fn l) (use_fun fn r)
    else apply fn tm in
  fun fm ->
    let p,p' = dest_eq fm in
    if p = p' then REFL p else
    let th = use_fun (mk_fun (ASSUME(mk_neg p)) undefined) p'
    and th' = use_fun (mk_fun (ASSUME(mk_neg p')) undefined) p in
    let th1 = IMP_ANTISYM_RULE (DISCH_ALL th) (DISCH_ALL th') in
    PROVE_HYP th1 (INST [p,a_tm; p',b_tm] pth_neg);;

(* ------------------------------------------------------------------------- *)
(* Order canonically, right-associate and remove duplicates.                 *)
(* ------------------------------------------------------------------------- *)

let CONJ_CANON_CONV tm =
  let tm' = list_mk_conj(setify(conjuncts tm)) in
  CONJ_ACI_RULE(mk_eq(tm,tm'));;

let DISJ_CANON_CONV tm =
  let tm' = list_mk_disj(setify(disjuncts tm)) in
  DISJ_ACI_RULE(mk_eq(tm,tm'));;

(* ------------------------------------------------------------------------- *)
(* General NNF conversion. The user supplies some conversion to be applied   *)
(* to atomic formulas.                                                       *)
(*                                                                           *)
(* "Iff"s are split conjunctively or disjunctively according to the flag     *)
(* argument (conjuctively = true) until a universal quantifier (modulo       *)
(* current parity) is passed; after that they are split conjunctively. This  *)
(* is appropriate when the result is passed to a disjunctive splitter        *)
(* followed by a clausal form inner core, such as MESON.                     *)
(*                                                                           *)
(* To avoid some duplicate computation, this function will in general        *)
(* enter a recursion where it simultaneously computes NNF representations    *)
(* for "p" and "~p", so the user needs to supply an atomic "conversion"      *)
(* that does the same.                                                       *)
(* ------------------------------------------------------------------------- *)

let (GEN_NNF_CONV:bool->conv*(term->thm*thm)->conv) =
  let and_tm = `(/\)` and or_tm = `(\/)` and not_tm = `(~)`
  and pth_not_not = TAUT `~ ~ p = p`
  and pth_not_and = TAUT `~(p /\ q) <=> ~p \/ ~q`
  and pth_not_or = TAUT `~(p \/ q) <=> ~p /\ ~q`
  and pth_imp = TAUT `p ==> q <=> ~p \/ q`
  and pth_not_imp = TAUT `~(p ==> q) <=> p /\ ~q`
  and pth_eq = TAUT `(p <=> q) <=> p /\ q \/ ~p /\ ~q`
  and pth_not_eq = TAUT `~(p <=> q) <=> p /\ ~q \/ ~p /\ q`
  and pth_eq' = TAUT `(p <=> q) <=> (p \/ ~q) /\ (~p \/ q)`
  and pth_not_eq' = TAUT `~(p <=> q) <=> (p \/ q) /\ (~p \/ ~q)`
  and [pth_not_forall; pth_not_exists; pth_not_exu] =
   (CONJUNCTS o prove)
   (`(~((!) P) <=> ?x:A. ~(P x)) /\
     (~((?) P) <=> !x:A. ~(P x)) /\
     (~((?!) P) <=> (!x:A. ~(P x)) \/ ?x y. P x /\ P y /\ ~(y = x))`,
    REPEAT CONJ_TAC THEN
    GEN_REWRITE_TAC (LAND_CONV o funpow 2 RAND_CONV) [GSYM ETA_AX] THEN
    REWRITE_TAC[NOT_EXISTS_THM; NOT_FORALL_THM; EXISTS_UNIQUE_DEF;
                DE_MORGAN_THM; NOT_IMP] THEN
    REWRITE_TAC[CONJ_ASSOC; EQ_SYM_EQ])
  and pth_exu = prove
   (`((?!) P) <=> (?x:A. P x) /\ !x y. ~(P x) \/ ~(P y) \/ (y = x)`,
    GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM ETA_AX] THEN
    REWRITE_TAC[EXISTS_UNIQUE_DEF; TAUT `a /\ b ==> c <=> ~a \/ ~b \/ c`] THEN
    REWRITE_TAC[EQ_SYM_EQ])
  and p_tm = `p:bool` and q_tm = `q:bool` in
  let rec NNF_DCONV cf baseconvs tm =
    match tm with
      Comb(Comb(Const("/\\",_),l),r) ->
          let th_lp,th_ln = NNF_DCONV cf baseconvs l
          and th_rp,th_rn = NNF_DCONV cf baseconvs r in
          MK_COMB(AP_TERM and_tm th_lp,th_rp),
          TRANS (INST [l,p_tm; r,q_tm] pth_not_and)
                (MK_COMB(AP_TERM or_tm th_ln,th_rn))
    | Comb(Comb(Const("\\/",_),l),r) ->
          let th_lp,th_ln = NNF_DCONV cf baseconvs l
          and th_rp,th_rn = NNF_DCONV cf baseconvs r in
          MK_COMB(AP_TERM or_tm th_lp,th_rp),
          TRANS (INST [l,p_tm; r,q_tm] pth_not_or)
                (MK_COMB(AP_TERM and_tm th_ln,th_rn))
    | Comb(Comb(Const("==>",_),l),r) ->
          let th_lp,th_ln = NNF_DCONV cf baseconvs l
          and th_rp,th_rn = NNF_DCONV cf baseconvs r in
          TRANS (INST [l,p_tm; r,q_tm] pth_imp)
                (MK_COMB(AP_TERM or_tm th_ln,th_rp)),
          TRANS (INST [l,p_tm; r,q_tm] pth_not_imp)
                (MK_COMB(AP_TERM and_tm th_lp,th_rn))
    | Comb(Comb(Const("=",Tyapp("fun",Tyapp("bool",_)::_)),l),r) ->
          let th_lp,th_ln = NNF_DCONV cf baseconvs l
          and th_rp,th_rn = NNF_DCONV cf baseconvs r in
          if cf then
            TRANS (INST [l,p_tm; r,q_tm] pth_eq')
                  (MK_COMB(AP_TERM and_tm (MK_COMB(AP_TERM or_tm th_lp,th_rn)),
                           MK_COMB(AP_TERM or_tm th_ln,th_rp))),
            TRANS (INST [l,p_tm; r,q_tm] pth_not_eq')
                  (MK_COMB(AP_TERM and_tm (MK_COMB(AP_TERM or_tm th_lp,th_rp)),
                           MK_COMB(AP_TERM or_tm th_ln,th_rn)))
          else
            TRANS (INST [l,p_tm; r,q_tm] pth_eq)
                  (MK_COMB(AP_TERM or_tm (MK_COMB(AP_TERM and_tm th_lp,th_rp)),
                           MK_COMB(AP_TERM and_tm th_ln,th_rn))),
            TRANS (INST [l,p_tm; r,q_tm] pth_not_eq)
                  (MK_COMB(AP_TERM or_tm (MK_COMB(AP_TERM and_tm th_lp,th_rn)),
                           MK_COMB(AP_TERM and_tm th_ln,th_rp)))
    | Comb(Const("!",Tyapp("fun",Tyapp("fun",ty::_)::_)) as q,
           (Abs(x,t) as bod)) ->
          let th_p,th_n = NNF_DCONV true baseconvs t in
          AP_TERM q (ABS x th_p),
          let th1 = INST [bod,mk_var("P",mk_fun_ty ty bool_ty)]
                         (INST_TYPE [ty,aty] pth_not_forall)
          and th2 = TRANS (AP_TERM not_tm (BETA(mk_comb(bod,x)))) th_n in
          TRANS th1 (MK_EXISTS x th2)
    | Comb(Const("?",Tyapp("fun",Tyapp("fun",ty::_)::_)) as q,
           (Abs(x,t) as bod)) ->
          let th_p,th_n = NNF_DCONV cf baseconvs t in
          AP_TERM q (ABS x th_p),
          let th1 = INST [bod,mk_var("P",mk_fun_ty ty bool_ty)]
                         (INST_TYPE [ty,aty] pth_not_exists)
          and th2 = TRANS (AP_TERM not_tm (BETA(mk_comb(bod,x)))) th_n in
          TRANS th1 (MK_FORALL x th2)
    | Comb(Const("?!",Tyapp("fun",Tyapp("fun",ty::_)::_)),
           (Abs(x,t) as bod)) ->
          let y = variant (x::frees t) x
          and th_p,th_n = NNF_DCONV cf baseconvs t in
          let eq = mk_eq(y,x) in
          let eth_p,eth_n = baseconvs eq
          and bth = BETA (mk_comb(bod,x))
          and bth' = BETA_CONV(mk_comb(bod,y)) in
          let th_p' = INST [y,x] th_p and th_n' = INST [y,x] th_n in
          let th1 = INST [bod,mk_var("P",mk_fun_ty ty bool_ty)]
                         (INST_TYPE [ty,aty] pth_exu)
          and th1' = INST [bod,mk_var("P",mk_fun_ty ty bool_ty)]
                          (INST_TYPE [ty,aty] pth_not_exu)
          and th2 =
            MK_COMB(AP_TERM and_tm
                        (MK_EXISTS x (TRANS bth th_p)),
                    MK_FORALL x (MK_FORALL y
                     (MK_COMB(AP_TERM or_tm (TRANS (AP_TERM not_tm bth) th_n),
                              MK_COMB(AP_TERM or_tm
                                    (TRANS (AP_TERM not_tm bth') th_n'),
                                      eth_p)))))
          and th2' =
            MK_COMB(AP_TERM or_tm
                        (MK_FORALL x (TRANS (AP_TERM not_tm bth) th_n)),
                    MK_EXISTS x (MK_EXISTS y
                     (MK_COMB(AP_TERM and_tm (TRANS bth th_p),
                              MK_COMB(AP_TERM and_tm (TRANS bth' th_p'),
                                      eth_n))))) in
          TRANS th1 th2,TRANS th1' th2'
    | Comb(Const("~",_),t) ->
          let th1,th2 = NNF_DCONV cf baseconvs t in
          th2,TRANS (INST [t,p_tm] pth_not_not) th1
    | _ -> try baseconvs tm
           with Failure _ -> REFL tm,REFL(mk_neg tm) in
  let rec NNF_CONV cf (base1,base2 as baseconvs) tm =
    match tm with
      Comb(Comb(Const("/\\",_),l),r) ->
          let th_lp = NNF_CONV cf baseconvs l
          and th_rp = NNF_CONV cf baseconvs r in
          MK_COMB(AP_TERM and_tm th_lp,th_rp)
    | Comb(Comb(Const("\\/",_),l),r) ->
          let th_lp = NNF_CONV cf baseconvs l
          and th_rp = NNF_CONV cf baseconvs r in
          MK_COMB(AP_TERM or_tm th_lp,th_rp)
    | Comb(Comb(Const("==>",_),l),r) ->
          let th_ln = NNF_CONV' cf baseconvs l
          and th_rp = NNF_CONV cf baseconvs r in
          TRANS (INST [l,p_tm; r,q_tm] pth_imp)
                (MK_COMB(AP_TERM or_tm th_ln,th_rp))
    | Comb(Comb(Const("=",Tyapp("fun",Tyapp("bool",_)::_)),l),r) ->
          let th_lp,th_ln = NNF_DCONV cf base2 l
          and th_rp,th_rn = NNF_DCONV cf base2 r in
          if cf then
            TRANS (INST [l,p_tm; r,q_tm] pth_eq')
                  (MK_COMB(AP_TERM and_tm (MK_COMB(AP_TERM or_tm th_lp,th_rn)),
                           MK_COMB(AP_TERM or_tm th_ln,th_rp)))
          else
            TRANS (INST [l,p_tm; r,q_tm] pth_eq)
                  (MK_COMB(AP_TERM or_tm (MK_COMB(AP_TERM and_tm th_lp,th_rp)),
                           MK_COMB(AP_TERM and_tm th_ln,th_rn)))
    | Comb(Const("!",Tyapp("fun",Tyapp("fun",ty::_)::_)) as q,
           (Abs(x,t))) ->
          let th_p = NNF_CONV true baseconvs t in
          AP_TERM q (ABS x th_p)
    | Comb(Const("?",Tyapp("fun",Tyapp("fun",ty::_)::_)) as q,
           (Abs(x,t))) ->
          let th_p = NNF_CONV cf baseconvs t in
          AP_TERM q (ABS x th_p)
    | Comb(Const("?!",Tyapp("fun",Tyapp("fun",ty::_)::_)),
           (Abs(x,t) as bod)) ->
          let y = variant (x::frees t) x
          and th_p,th_n = NNF_DCONV cf base2 t in
          let eq = mk_eq(y,x) in
          let eth_p,eth_n = base2 eq
          and bth = BETA (mk_comb(bod,x))
          and bth' = BETA_CONV(mk_comb(bod,y)) in
          let th_n' = INST [y,x] th_n in
          let th1 = INST [bod,mk_var("P",mk_fun_ty ty bool_ty)]
                         (INST_TYPE [ty,aty] pth_exu)
          and th2 =
            MK_COMB(AP_TERM and_tm
                        (MK_EXISTS x (TRANS bth th_p)),
                    MK_FORALL x (MK_FORALL y
                     (MK_COMB(AP_TERM or_tm (TRANS (AP_TERM not_tm bth) th_n),
                              MK_COMB(AP_TERM or_tm
                                    (TRANS (AP_TERM not_tm bth') th_n'),
                                      eth_p))))) in
          TRANS th1 th2
    | Comb(Const("~",_),t) -> NNF_CONV' cf baseconvs t
    | _ -> try base1 tm with Failure _ -> REFL tm
  and NNF_CONV' cf (base1,base2 as baseconvs) tm =
    match tm with
      Comb(Comb(Const("/\\",_),l),r) ->
          let th_ln = NNF_CONV' cf baseconvs l
          and th_rn = NNF_CONV' cf baseconvs r in
          TRANS (INST [l,p_tm; r,q_tm] pth_not_and)
                (MK_COMB(AP_TERM or_tm th_ln,th_rn))
    | Comb(Comb(Const("\\/",_),l),r) ->
          let th_ln = NNF_CONV' cf baseconvs l
          and th_rn = NNF_CONV' cf baseconvs r in
          TRANS (INST [l,p_tm; r,q_tm] pth_not_or)
                (MK_COMB(AP_TERM and_tm th_ln,th_rn))
    | Comb(Comb(Const("==>",_),l),r) ->
          let th_lp = NNF_CONV cf baseconvs l
          and th_rn = NNF_CONV' cf baseconvs r in
          TRANS (INST [l,p_tm; r,q_tm] pth_not_imp)
                (MK_COMB(AP_TERM and_tm th_lp,th_rn))
    | Comb(Comb(Const("=",Tyapp("fun",Tyapp("bool",_)::_)),l),r) ->
          let th_lp,th_ln = NNF_DCONV cf base2 l
          and th_rp,th_rn = NNF_DCONV cf base2 r in
          if cf then
            TRANS (INST [l,p_tm; r,q_tm] pth_not_eq')
                  (MK_COMB(AP_TERM and_tm (MK_COMB(AP_TERM or_tm th_lp,th_rp)),
                           MK_COMB(AP_TERM or_tm th_ln,th_rn)))
          else
            TRANS (INST [l,p_tm; r,q_tm] pth_not_eq)
                  (MK_COMB(AP_TERM or_tm (MK_COMB(AP_TERM and_tm th_lp,th_rn)),
                           MK_COMB(AP_TERM and_tm th_ln,th_rp)))
    | Comb(Const("!",Tyapp("fun",Tyapp("fun",ty::_)::_)),
           (Abs(x,t) as bod)) ->
          let th_n = NNF_CONV' cf baseconvs t in
          let th1 = INST [bod,mk_var("P",mk_fun_ty ty bool_ty)]
                         (INST_TYPE [ty,aty] pth_not_forall)
          and th2 = TRANS (AP_TERM not_tm (BETA(mk_comb(bod,x)))) th_n in
          TRANS th1 (MK_EXISTS x th2)
    | Comb(Const("?",Tyapp("fun",Tyapp("fun",ty::_)::_)),
           (Abs(x,t) as bod)) ->
          let th_n = NNF_CONV' true baseconvs t in
          let th1 = INST [bod,mk_var("P",mk_fun_ty ty bool_ty)]
                         (INST_TYPE [ty,aty] pth_not_exists)
          and th2 = TRANS (AP_TERM not_tm (BETA(mk_comb(bod,x)))) th_n in
          TRANS th1 (MK_FORALL x th2)
    | Comb(Const("?!",Tyapp("fun",Tyapp("fun",ty::_)::_)),
           (Abs(x,t) as bod)) ->
          let y = variant (x::frees t) x
          and th_p,th_n = NNF_DCONV cf base2 t in
          let eq = mk_eq(y,x) in
          let eth_p,eth_n = base2 eq
          and bth = BETA (mk_comb(bod,x))
          and bth' = BETA_CONV(mk_comb(bod,y)) in
          let th_p' = INST [y,x] th_p in
          let th1' = INST [bod,mk_var("P",mk_fun_ty ty bool_ty)]
                          (INST_TYPE [ty,aty] pth_not_exu)
          and th2' =
            MK_COMB(AP_TERM or_tm
                        (MK_FORALL x (TRANS (AP_TERM not_tm bth) th_n)),
                    MK_EXISTS x (MK_EXISTS y
                     (MK_COMB(AP_TERM and_tm (TRANS bth th_p),
                              MK_COMB(AP_TERM and_tm (TRANS bth' th_p'),
                                      eth_n))))) in
          TRANS th1' th2'
    | Comb(Const("~",_),t) ->
          let th1 = NNF_CONV cf baseconvs t in
          TRANS (INST [t,p_tm] pth_not_not) th1
    | _ -> let tm' = mk_neg tm in try base1 tm' with Failure _ -> REFL tm' in
  NNF_CONV;;

(* ------------------------------------------------------------------------- *)
(* Some common special cases.                                                *)
(* ------------------------------------------------------------------------- *)

let NNF_CONV =
  (GEN_NNF_CONV false (ALL_CONV,fun t -> REFL t,REFL(mk_neg t)) :conv);;

let NNFC_CONV =
  (GEN_NNF_CONV true (ALL_CONV,fun t -> REFL t,REFL(mk_neg t)) :conv);;

(* ------------------------------------------------------------------------- *)
(* Skolemize a term already in NNF (doesn't matter if it's not prenex).      *)
(* ------------------------------------------------------------------------- *)

let SKOLEM_CONV =
  GEN_REWRITE_CONV TOP_DEPTH_CONV
   [EXISTS_OR_THM; LEFT_EXISTS_AND_THM; RIGHT_EXISTS_AND_THM;
    FORALL_AND_THM; LEFT_FORALL_OR_THM; RIGHT_FORALL_OR_THM;
    FORALL_SIMP; EXISTS_SIMP] THENC
  GEN_REWRITE_CONV REDEPTH_CONV
   [RIGHT_AND_EXISTS_THM;
    LEFT_AND_EXISTS_THM;
    OR_EXISTS_THM;
    RIGHT_OR_EXISTS_THM;
    LEFT_OR_EXISTS_THM;
    SKOLEM_THM];;

(* ------------------------------------------------------------------------- *)
(* Put a term already in NNF into prenex form.                               *)
(* ------------------------------------------------------------------------- *)

let PRENEX_CONV =
  GEN_REWRITE_CONV REDEPTH_CONV
   [AND_FORALL_THM; LEFT_AND_FORALL_THM; RIGHT_AND_FORALL_THM;
    LEFT_OR_FORALL_THM; RIGHT_OR_FORALL_THM;
    OR_EXISTS_THM; LEFT_OR_EXISTS_THM; RIGHT_OR_EXISTS_THM;
    LEFT_AND_EXISTS_THM; RIGHT_AND_EXISTS_THM];;

(* ------------------------------------------------------------------------- *)
(* Weak and normal DNF conversion. The "weak" form gives a disjunction of    *)
(* conjunctions, but has no particular associativity at either level and     *)
(* may contain duplicates. The regular forms give canonical right-associate  *)
(* lists without duplicates, but do not remove subsumed disjuncts.           *)
(*                                                                           *)
(* In both cases the input term is supposed to be in NNF already. We do go   *)
(* inside quantifiers and transform their body, but don't move them.         *)
(* ------------------------------------------------------------------------- *)

let WEAK_DNF_CONV,DNF_CONV =
  let pth1 = TAUT `a /\ (b \/ c) <=> a /\ b \/ a /\ c`
  and pth2 = TAUT `(a \/ b) /\ c <=> a /\ c \/ b /\ c`
  and a_tm = `a:bool` and b_tm = `b:bool` and c_tm = `c:bool` in
  let rec distribute tm =
    match tm with
      Comb(Comb(Const("/\\",_),a),Comb(Comb(Const("\\/",_),b),c)) ->
          let th = INST [a,a_tm; b,b_tm; c,c_tm] pth1 in
          TRANS th (BINOP_CONV distribute (rand(concl th)))
    | Comb(Comb(Const("/\\",_),Comb(Comb(Const("\\/",_),a),b)),c) ->
          let th = INST [a,a_tm; b,b_tm; c,c_tm] pth2 in
          TRANS th (BINOP_CONV distribute (rand(concl th)))
    | _ -> REFL tm in
  let strengthen =
    DEPTH_BINOP_CONV `(\/)` CONJ_CANON_CONV THENC DISJ_CANON_CONV in
  let rec weakdnf tm =
    match tm with
      Comb(Const("!",_),Abs(_,_))
    | Comb(Const("?",_),Abs(_,_)) -> BINDER_CONV weakdnf tm
    | Comb(Comb(Const("\\/",_),_),_) -> BINOP_CONV weakdnf tm
    | Comb(Comb(Const("/\\",_) as op,l),r) ->
          let th = MK_COMB(AP_TERM op (weakdnf l),weakdnf r) in
          TRANS th (distribute(rand(concl th)))
    | _ -> REFL tm
  and substrongdnf tm =
    match tm with
      Comb(Const("!",_),Abs(_,_))
    | Comb(Const("?",_),Abs(_,_)) -> BINDER_CONV strongdnf tm
    | Comb(Comb(Const("\\/",_),_),_) -> BINOP_CONV substrongdnf tm
    | Comb(Comb(Const("/\\",_) as op,l),r) ->
          let th = MK_COMB(AP_TERM op (substrongdnf l),substrongdnf r) in
          TRANS th (distribute(rand(concl th)))
    | _ -> REFL tm
  and strongdnf tm =
    let th = substrongdnf tm in
    TRANS th (strengthen(rand(concl th))) in
  weakdnf,strongdnf;;

(* ------------------------------------------------------------------------- *)
(* Likewise for CNF.                                                         *)
(* ------------------------------------------------------------------------- *)

let WEAK_CNF_CONV,CNF_CONV =
  let pth1 = TAUT `a \/ (b /\ c) <=> (a \/ b) /\ (a \/ c)`
  and pth2 = TAUT `(a /\ b) \/ c <=> (a \/ c) /\ (b \/ c)`
  and a_tm = `a:bool` and b_tm = `b:bool` and c_tm = `c:bool` in
  let rec distribute tm =
    match tm with
      Comb(Comb(Const("\\/",_),a),Comb(Comb(Const("/\\",_),b),c)) ->
          let th = INST [a,a_tm; b,b_tm; c,c_tm] pth1 in
          TRANS th (BINOP_CONV distribute (rand(concl th)))
    | Comb(Comb(Const("\\/",_),Comb(Comb(Const("/\\",_),a),b)),c) ->
          let th = INST [a,a_tm; b,b_tm; c,c_tm] pth2 in
          TRANS th (BINOP_CONV distribute (rand(concl th)))
    | _ -> REFL tm in
  let strengthen =
    DEPTH_BINOP_CONV `(/\)` DISJ_CANON_CONV THENC CONJ_CANON_CONV in
  let rec weakcnf tm =
    match tm with
      Comb(Const("!",_),Abs(_,_))
    | Comb(Const("?",_),Abs(_,_)) -> BINDER_CONV weakcnf tm
    | Comb(Comb(Const("/\\",_),_),_) -> BINOP_CONV weakcnf tm
    | Comb(Comb(Const("\\/",_) as op,l),r) ->
          let th = MK_COMB(AP_TERM op (weakcnf l),weakcnf r) in
          TRANS th (distribute(rand(concl th)))
    | _ -> REFL tm
  and substrongcnf tm =
    match tm with
      Comb(Const("!",_),Abs(_,_))
    | Comb(Const("?",_),Abs(_,_)) -> BINDER_CONV strongcnf tm
    | Comb(Comb(Const("/\\",_),_),_) -> BINOP_CONV substrongcnf tm
    | Comb(Comb(Const("\\/",_) as op,l),r) ->
          let th = MK_COMB(AP_TERM op (substrongcnf l),substrongcnf r) in
          TRANS th (distribute(rand(concl th)))
    | _ -> REFL tm
  and strongcnf tm =
    let th = substrongcnf tm in
    TRANS th (strengthen(rand(concl th))) in
  weakcnf,strongcnf;;

(* ------------------------------------------------------------------------- *)
(* Simply right-associate w.r.t. a binary operator.                          *)
(* ------------------------------------------------------------------------- *)

let ASSOC_CONV th =
  let th' = SYM(SPEC_ALL th) in
  let opx,yopz = dest_comb(rhs(concl th')) in
  let op,x = dest_comb opx in
  let y = lhand yopz and z = rand yopz in
  let rec distrib tm =
    match tm with
      Comb(Comb(op',Comb(Comb(op'',p),q)),r) when op' = op & op'' = op ->
          let th1 = INST [p,x; q,y; r,z] th' in
          let l,r' = dest_comb(rand(concl th1)) in
          let th2 = AP_TERM l (distrib r') in
          let th3 = distrib(rand(concl th2)) in
          TRANS th1 (TRANS th2 th3)
    | _ -> REFL tm in
  let rec assoc tm =
    match tm with
      Comb(Comb(op',p) as l,q) when op' = op ->
          let th = AP_TERM l (assoc q) in
          TRANS th (distrib(rand(concl th)))
    | _ -> REFL tm in
  assoc;;

(* ------------------------------------------------------------------------- *)
(* Eliminate select terms from a goal.                                       *)
(* ------------------------------------------------------------------------- *)

let SELECT_ELIM_TAC =
  let SELECT_ELIM_CONV =
    let SELECT_ELIM_THM =
      
let pth = 
prove (`(P:A->bool)((@) P) <=> (?) P`,
REWRITE_TAC[EXISTS_THM] THEN BETA_TAC THEN REFL_TAC) and ptm = `P:A->bool` in fun tm -> let stm,atm = dest_comb tm in if is_const stm & fst(dest_const stm) = "@" then CONV_RULE(LAND_CONV BETA_CONV) (PINST [type_of(bndvar atm),aty] [atm,ptm] pth) else failwith "SELECT_ELIM_THM: not a select-term" in fun tm -> PURE_REWRITE_CONV (map SELECT_ELIM_THM (find_terms is_select tm)) tm in let SELECT_ELIM_ICONV = let SELECT_AX_THM = let pth = ISPEC `P:A->bool` SELECT_AX and ptm = `P:A->bool` in fun tm -> let stm,atm = dest_comb tm in if is_const stm & fst(dest_const stm) = "@" then let fvs = frees atm in let th1 = PINST [type_of(bndvar atm),aty] [atm,ptm] pth in let th2 = CONV_RULE(BINDER_CONV (BINOP_CONV BETA_CONV)) th1 in GENL fvs th2 else failwith "SELECT_AX_THM: not a select-term" in let SELECT_ELIM_ICONV tm = let t = find_term is_select tm in let th1 = SELECT_AX_THM t in let itm = mk_imp(concl th1,tm) in let th2 = DISCH_ALL (MP (ASSUME itm) th1) in let fvs = frees t in let fty = itlist (mk_fun_ty o type_of) fvs (type_of t) in let fn = genvar fty and atm = list_mk_abs(fvs,t) in let rawdef = mk_eq(fn,atm) in let def = GENL fvs (SYM(RIGHT_BETAS fvs (ASSUME rawdef))) in let th3 = PURE_REWRITE_CONV[def] (lhand(concl th2)) in let gtm = mk_forall(fn,rand(concl th3)) in let th4 = EQ_MP (SYM th3) (SPEC fn (ASSUME gtm)) in let th5 = IMP_TRANS (DISCH gtm th4) th2 in MP (INST [atm,fn] (DISCH rawdef th5)) (REFL atm) in let rec SELECT_ELIMS_ICONV tm = try let th = SELECT_ELIM_ICONV tm in let tm' = lhand(concl th) in IMP_TRANS (SELECT_ELIMS_ICONV tm') th with Failure _ -> DISCH tm (ASSUME tm) in SELECT_ELIMS_ICONV in CONV_TAC SELECT_ELIM_CONV THEN W(MATCH_MP_TAC o SELECT_ELIM_ICONV o snd);;
(* ------------------------------------------------------------------------- *) (* Eliminate all lambda-terms except those part of quantifiers. *) (* ------------------------------------------------------------------------- *) let LAMBDA_ELIM_CONV = let HALF_MK_ABS_CONV =
let pth = 
prove (`(s = \x. t x) <=> (!x. s x = t x)`,
REWRITE_TAC[FUN_EQ_THM]) in let rec conv vs tm = if vs = [] then REFL tm else (GEN_REWRITE_CONV I [pth] THENC BINDER_CONV(conv (tl vs))) tm in conv in let rec find_lambda tm = if is_abs tm then tm else if is_var tm or is_const tm then failwith "find_lambda" else if is_abs tm then tm else if is_forall tm or is_exists tm or is_uexists tm then find_lambda (body(rand tm)) else let l,r = dest_comb tm in try find_lambda l with Failure _ -> find_lambda r in let rec ELIM_LAMBDA conv tm = try conv tm with Failure _ -> if is_abs tm then ABS_CONV (ELIM_LAMBDA conv) tm else if is_var tm or is_const tm then REFL tm else if is_forall tm or is_exists tm or is_uexists tm then BINDER_CONV (ELIM_LAMBDA conv) tm else COMB_CONV (ELIM_LAMBDA conv) tm in let APPLY_PTH =
let pth = prove
     (`(!a. (a = c) ==> (P = Q a)) ==> (P <=> !a. (a = c) ==> Q a)`,
      SIMP_TAC[LEFT_FORALL_IMP_THM; EXISTS_REFL]) in
    MATCH_MP pth in
  let LAMB1_CONV tm =
    let atm = find_lambda tm in
    let v,bod = dest_abs atm in
    let vs = frees atm in
    let vs' = vs @ [v] in
    let aatm = list_mk_abs(vs,atm) in
    let f = genvar(type_of aatm) in
    let eq = mk_eq(f,aatm) in
    let th1 = SYM(RIGHT_BETAS vs (ASSUME eq)) in
    let th2 = ELIM_LAMBDA(GEN_REWRITE_CONV I [th1]) tm in
    let th3 = APPLY_PTH (GEN f (DISCH_ALL th2)) in
    CONV_RULE(RAND_CONV(BINDER_CONV(LAND_CONV (HALF_MK_ABS_CONV vs')))) th3 in
  let rec conv tm =
    try (LAMB1_CONV THENC conv) tm with Failure _ -> REFL tm in
  conv;;
(* ------------------------------------------------------------------------- *) (* Eliminate conditionals; CONDS_ELIM_CONV aims for disjunctive splitting, *) (* for refutation procedures, and CONDS_CELIM_CONV for conjunctive. *) (* Both switch modes "sensibly" when going through a quantifier. *) (* ------------------------------------------------------------------------- *) let CONDS_ELIM_CONV,CONDS_CELIM_CONV =
let th_cond = 
prove (`((b <=> F) ==> x = x0) /\ ((b <=> T) ==> x = x1) ==> x = (b /\ x1 \/ ~b /\ x0)`,
BOOL_CASES_TAC `b:bool` THEN ASM_REWRITE_TAC[]) and th_cond' = prove (`((b <=> F) ==> x = x0) /\ ((b <=> T) ==> x = x1) ==> x = ((~b \/ x1) /\ (b \/ x0))`, BOOL_CASES_TAC `b:bool` THEN ASM_REWRITE_TAC[]) and propsimps = basic_net() and false_tm = `F` and true_tm = `T` in let match_th = MATCH_MP th_cond and match_th' = MATCH_MP th_cond' and propsimp_conv = DEPTH_CONV(REWRITES_CONV propsimps) and proptsimp_conv = let cnv = TRY_CONV(REWRITES_CONV propsimps) in BINOP_CONV cnv THENC cnv in let rec find_conditional fvs tm = match tm with Comb(s,t) -> if is_cond tm & intersect (frees(lhand s)) fvs = [] then tm else (try (find_conditional fvs s) with Failure _ -> find_conditional fvs t) | Abs(x,t) -> find_conditional (x::fvs) t | _ -> failwith "find_conditional" in let rec CONDS_ELIM_CONV dfl tm = try let t = find_conditional [] tm in let p = lhand(rator t) in let th_new = if p = false_tm or p = true_tm then propsimp_conv tm else let asm_0 = mk_eq(p,false_tm) and asm_1 = mk_eq(p,true_tm) in let simp_0 = net_of_thm false (ASSUME asm_0) propsimps and simp_1 = net_of_thm false (ASSUME asm_1) propsimps in let th_0 = DISCH asm_0 (DEPTH_CONV(REWRITES_CONV simp_0) tm) and th_1 = DISCH asm_1 (DEPTH_CONV(REWRITES_CONV simp_1) tm) in let th_2 = CONJ th_0 th_1 in let th_3 = if dfl then match_th th_2 else match_th' th_2 in TRANS th_3 (proptsimp_conv(rand(concl th_3))) in CONV_RULE (RAND_CONV (CONDS_ELIM_CONV dfl)) th_new with Failure _ -> if is_neg tm then RAND_CONV (CONDS_ELIM_CONV (not dfl)) tm else if is_conj tm or is_disj tm then BINOP_CONV (CONDS_ELIM_CONV dfl) tm else if is_imp tm or is_iff tm then COMB2_CONV (RAND_CONV (CONDS_ELIM_CONV (not dfl))) (CONDS_ELIM_CONV dfl) tm else if is_forall tm then BINDER_CONV (CONDS_ELIM_CONV false) tm else if is_exists tm or is_uexists tm then BINDER_CONV (CONDS_ELIM_CONV true) tm else REFL tm in CONDS_ELIM_CONV true,CONDS_ELIM_CONV false;;
(* ------------------------------------------------------------------------- *) (* Fix up all head arities to be consistent, in "first order logic" style. *) (* Applied to the assumptions (not conclusion) in a goal. *) (* ------------------------------------------------------------------------- *) let ASM_FOL_TAC = let rec get_heads lconsts tm (cheads,vheads as sofar) = try let v,bod = dest_forall tm in get_heads (subtract lconsts [v]) bod sofar with Failure _ -> try let l,r = try dest_conj tm with Failure _ -> dest_disj tm in get_heads lconsts l (get_heads lconsts r sofar) with Failure _ -> try let tm' = dest_neg tm in get_heads lconsts tm' sofar with Failure _ -> let hop,args = strip_comb tm in let len = length args in let newheads = if is_const hop or mem hop lconsts then (insert (hop,len) cheads,vheads) else if len > 0 then (cheads,insert (hop,len) vheads) else sofar in itlist (get_heads lconsts) args newheads in let get_thm_heads th sofar = get_heads (freesl(hyp th)) (concl th) sofar in let APP_CONV =
let th = 
prove (`!(f:A->B) x. f x = I f x`,
REWRITE_TAC[I_THM]) in REWR_CONV th in let rec APP_N_CONV n tm = if n = 1 then APP_CONV tm else (RATOR_CONV (APP_N_CONV (n - 1)) THENC APP_CONV) tm in let rec FOL_CONV hddata tm = if is_forall tm then BINDER_CONV (FOL_CONV hddata) tm else if is_conj tm or is_disj tm then BINOP_CONV (FOL_CONV hddata) tm else let op,args = strip_comb tm in let th = rev_itlist (C (curry MK_COMB)) (map (FOL_CONV hddata) args) (REFL op) in let tm' = rand(concl th) in let n = try length args - assoc op hddata with Failure _ -> 0 in if n = 0 then th else TRANS th (APP_N_CONV n tm') in let GEN_FOL_CONV (cheads,vheads) = let hddata = if vheads = [] then let hops = setify (map fst cheads) in let getmin h = let ns = mapfilter (fun (k,n) -> if k = h then n else fail()) cheads in if length ns < 2 then fail() else h,end_itlist min ns in mapfilter getmin hops else map (fun t -> if is_const t & fst(dest_const t) = "=" then t,2 else t,0) (setify (map fst (vheads @ cheads))) in FOL_CONV hddata in fun (asl,w as gl) -> let headsp = itlist (get_thm_heads o snd) asl ([],[]) in RULE_ASSUM_TAC(CONV_RULE(GEN_FOL_CONV headsp)) gl;;
(* ------------------------------------------------------------------------- *) (* Depth conversion to apply at "atomic" formulas in "first-order" term. *) (* ------------------------------------------------------------------------- *) let rec PROP_ATOM_CONV conv tm = match tm with Comb((Const("!",_) | Const("?",_) | Const("?!",_)),Abs(_,_)) -> BINDER_CONV (PROP_ATOM_CONV conv) tm | Comb(Comb ((Const("/\\",_) | Const("\\/",_) | Const("==>",_) | (Const("=",Tyapp("fun",[Tyapp("bool",[]);_])))),_),_) -> BINOP_CONV (PROP_ATOM_CONV conv) tm | Comb(Const("~",_),_) -> RAND_CONV (PROP_ATOM_CONV conv) tm | _ -> TRY_CONV conv tm;;