structure resolve_then :> resolve_then =
struct

open HolKernel boolSyntax Drule thmpos_dtype

fun match_subterm pat = find_term (can (match_term pat))

fun UDISCH' avoidnames th =
    let
      val (l,r) = dest_imp_only (concl th)
      fun buildcth nms0 t =
          case Lib.total dest_conj t of
              SOME (l,r) =>
              let
                val (lth, lcs, nms1) = buildcth nms0 l
                val (rth, rcs, nms2) = buildcth nms1 r
              in
                (CONJ lth rth, lcs @ rcs, nms2)
              end
            | NONE => (case Lib.total dest_exists t of
                           NONE => (ASSUME t, [t], nms0)
                         | SOME (bv, bod) =>
                           let
                             val (bvnm,bvty) = dest_var bv
                             val (c, cnm,bod') =
                                 let val cnm =
                                         Lexis.gen_variant Lexis.tmvar_vary
                                                           nms0
                                                           bvnm
                                     val c = mk_var(cnm, bvty)
                                 in
                                   (c, cnm, subst[bv |-> c] bod)
                                 end
                             val (bodth, bodcs, nms1) =
                                 buildcth (cnm::nms0) bod'
                           in
                             (EXISTS(t, c) bodth, bodcs, nms1)
                           end)
      val (th', conjuncts, nms') = buildcth avoidnames l
    in
      (PROVE_HYP th' (UNDISCH th), conjuncts, nms')
    end handle HOL_ERR _ => let
      val (bv,_) = dest_forall (concl th)
      val (bvnm, bvty) = dest_var bv
      val newnm = Lexis.gen_variant Lexis.tmvar_vary avoidnames bvnm
      val newv = mk_var(newnm, bvty)
    in
      (SPEC newv th, [], newnm::avoidnames)
    end

fun UDALL nms0 th0 =
    case Lib.total (UDISCH' nms0) th0 of
        NONE => (th0, [], nms0)
      | SOME (th', cs1, nms') =>
        let
          val (th, cs2, nms) = UDALL nms' th'
        in
          (th, cs1 @ cs2, nms)
        end

(* moves a bunch of hypotheses from a theorem into an implication, conjoining
   them all rather than creating iterated implications *)
fun DISCHl tms th =
    if null tms then th
    else
      let
        val cjt = list_mk_conj tms
      in
        th |> rev_itlist PROVE_HYP (CONJUNCTS $ ASSUME $ list_mk_conj tms)
           |> DISCH cjt
      end

(* turns G |- p   into G, ~p |- F, where p not negated; and
         G |- ~p  into G,  p |- F
   also returns the new hypothesis
*)
fun liftconcl th =
    let
      val c = concl th
    in
      let
        val c0 = dest_neg c
      in
        (UNDISCH th, c0)
      end handle HOL_ERR _ =>
                 let val h = mk_neg c
                 in
                   (EQ_MP (EQF_INTRO (ASSUME h)) th, h)
                 end
    end

(* val th2 = prim_recTheory.LESS_REFL
   val th1 = arithmeticTheory.LESS_TRANS
*)
fun resolve_then mpos ttac th1 th2 (g as (asl,w)) =
    (* conclusion of th1 unifies with some part of th2 *)
    let
      val th1 = GEN_ALL (GEN_TYVARIFY th1)
      val th2 = GEN_ALL (GEN_TYVARIFY th2)
      val fixed_tms1 = hyp_frees th1
      val fixed_tys1 = hyp_tyvars th1
      val fixed_tms2 = hyp_frees th2
      val fixed_tys2 = hyp_tyvars th2
      val fixed_tyl = HOLset.listItems (HOLset.union(fixed_tys1,fixed_tys2))
      val fixed_tms = HOLset.union(fixed_tms1,fixed_tms2)
      val fixed_tml = HOLset.listItems fixed_tms
      val hyps = HOLset.union(hypset th1, hypset th2)
      val badnames = HOLset.foldl(fn (v,A) =>HOLset.add(A,#1 (dest_var v)))
                                 (HOLset.empty String.compare)
                                 fixed_tms
      val (th1_ud, cs1, nms1) =
          UDALL (HOLset.listItems badnames) th1
      val (th2_ud, cs2, _) = UDALL nms1 th2
      val (th2_ud, con) =
          case mpos of
              Concl => liftconcl th2_ud
            | _ => (th2_ud, T)
      fun INSTT (tyi,tmi) th = th |> INST_TYPE tyi |> INST tmi
      fun instt (tyi,tmi) t = t |> Term.inst tyi |> Term.subst tmi
      open optmonad
      fun postprocess sigma th =
          let
            val thhyps = hypset th
            val dhyps0 = map (instt sigma) (cs1 @ cs2) |> op_mk_set aconv
            val dhyps =
                List.filter (fn t => not (HOLset.member(hyps,t)) andalso
                                     HOLset.member(thhyps, t))
                            dhyps0
          in
            DISCHl dhyps th |> GEN_ALL
          end
      fun try t k =
          case FullUnify.Env.fromEmpty
                 (FullUnify.unify fixed_tyl fixed_tml(t, concl th1_ud) >>
                                  FullUnify.collapse)
           of
              NONE => k()
            | SOME sigma =>
              let val kth =
                      PROVE_HYP (INSTT sigma th1_ud) (INSTT sigma th2_ud) |>
                      postprocess sigma
              in
                ttac kth g handle HOL_ERR _ => k()
              end
      val max = length cs2
      val fail = mk_HOL_ERR "resolve_then" "resolve_then" "No unifier"
    in
      case mpos of
          Any =>
          let
            fun doit n =
                if n > max then raise fail
                else try (el n cs2) (fn _ => doit (n + 1))
          in
            doit 1
          end
        | Pos f => try (f cs2) (fn _ => raise fail)
        | Pat q =>
          let
            open TermParse
            val pats =
                prim_ctxt_termS Parse.Absyn (Parse.term_grammar())
                                (HOLset.listItems (FVL (w::asl) empty_tmset))
                                q
            fun doit ps n =
                if n > max then raise fail
                else
                  case seq.cases ps of
                      NONE => doit pats (n + 1)
                    | SOME (pat, rest) =>
                      if can (match_subterm pat) (el n cs2) then
                        try (el n cs2) (fn _ => doit rest n)
                      else doit rest n
          in
            doit pats 1
          end
        | Concl => try con (fn _ => raise fail)
    end
end (* struct *)
