# File rules.ML

    (*  Title:      TFL/rules.ML
        ID:         $Id: rules.ML,v 1.17 2005/08/31 13:46:42 wenzelm Exp $
        Author:     Konrad Slind, Cambridge University Computer Laboratory
        Copyright   1997  University of Cambridge

    Emulation of HOL inference rules for TFL
    *)

    signature RULES =
    sig
      val dest_thm : thm -> term list * term

      (* Inference rules *)
      val REFL      :cterm -> thm
      val ASSUME    :cterm -> thm
      val MP        :thm -> thm -> thm
      val MATCH_MP  :thm -> thm -> thm
      val CONJUNCT1 :thm -> thm
      val CONJUNCT2 :thm -> thm
      val CONJUNCTS :thm -> thm list
      val DISCH     :cterm -> thm -> thm
      val UNDISCH   :thm  -> thm
      val SPEC      :cterm -> thm -> thm
      val ISPEC     :cterm -> thm -> thm
      val ISPECL    :cterm list -> thm -> thm
      val GEN       :cterm -> thm -> thm
      val GENL      :cterm list -> thm -> thm
      val LIST_CONJ :thm list -> thm

      val SYM : thm -> thm
      val DISCH_ALL : thm -> thm
      val FILTER_DISCH_ALL : (term -> bool) -> thm -> thm
      val SPEC_ALL  : thm -> thm
      val GEN_ALL   : thm -> thm
      val IMP_TRANS : thm -> thm -> thm
      val PROVE_HYP : thm -> thm -> thm

      val CHOOSE : cterm * thm -> thm -> thm
      val EXISTS : cterm * cterm -> thm -> thm
      val EXISTL : cterm list -> thm -> thm
      val IT_EXISTS : (cterm*cterm) list -> thm -> thm

      val EVEN_ORS : thm list -> thm list
      val DISJ_CASESL : thm -> thm list -> thm

      val list_beta_conv : cterm -> cterm list -> thm
      val SUBS : thm list -> thm -> thm
      val simpl_conv : simpset -> thm list -> cterm -> thm

      val rbeta : thm -> thm
    (* For debugging my isabelle solver in the conditional rewriter *)
      val term_ref : term list ref
      val thm_ref : thm list ref
      val ss_ref : simpset list ref
      val tracing : bool ref
      val CONTEXT_REWRITE_RULE : term * term list * thm * thm list
                                 -> thm -> thm * term list
      val RIGHT_ASSOC : thm -> thm

      val prove : bool -> cterm * tactic -> thm
    end;

    structure Rules: RULES =
    struct

    structure S = USyntax;
    structure U = Utils;
    structure D = Dcterm;

    fun RULES_ERR func mesg = U.ERR {module = "Rules", func = func, mesg = mesg};

    fun cconcl thm = D.drop_prop (#prop (Thm.crep_thm thm));
    fun chyps thm = map D.drop_prop (#hyps (Thm.crep_thm thm));

    fun dest_thm thm =
      let val {prop,hyps,...} = Thm.rep_thm thm
      in (map HOLogic.dest_Trueprop hyps, HOLogic.dest_Trueprop prop) end
      handle TERM _ => raise RULES_ERR "dest_thm" "missing Trueprop";

    (* Inference rules *)

    (*---------------------------------------------------------------------------
     *        Equality (one step)
     *---------------------------------------------------------------------------*)

    fun REFL tm = Thm.reflexive tm RS meta_eq_to_obj_eq
      handle THM (msg, _, _) => raise RULES_ERR "REFL" msg;

    fun SYM thm = thm RS sym
      handle THM (msg, _, _) => raise RULES_ERR "SYM" msg;

    fun ALPHA thm ctm1 =
      let
        val ctm2 = Thm.cprop_of thm;
        val ctm2_eq = Thm.reflexive ctm2;
        val ctm1_eq = Thm.reflexive ctm1;
      in Thm.equal_elim (Thm.transitive ctm2_eq ctm1_eq) thm end
      handle THM (msg, _, _) => raise RULES_ERR "ALPHA" msg;

    fun rbeta th =
      (case D.strip_comb (cconcl th) of
        (_, [l, r]) => Thm.transitive th (Thm.beta_conversion false r)
      | _ => raise RULES_ERR "rbeta" "");

    (*----------------------------------------------------------------------------
     *        Implication and the assumption list
     *
     * Assumptions get stuck on the meta-language assumption list. Implications
     * are in the object language, so discharging an assumption "A" from theorem
     * "B" results in something that looks like "A --> B".
     *---------------------------------------------------------------------------*)

    fun ASSUME ctm = Thm.assume (D.mk_prop ctm);

    (*---------------------------------------------------------------------------
     * Implication in TFL is -->. Meta-language implication (==>) is only used
     * in the implementation of some of the inference rules below.
     *---------------------------------------------------------------------------*)
    fun MP th1 th2 = th2 RS (th1 RS mp)
      handle THM (msg, _, _) => raise RULES_ERR "MP" msg;

    (*forces the first argument to be a proposition if necessary*)
    fun DISCH tm thm = Thm.implies_intr (D.mk_prop tm) thm COMP impI
      handle THM (msg, _, _) => raise RULES_ERR "DISCH" msg;

    fun DISCH_ALL thm = fold_rev DISCH (#hyps (Thm.crep_thm thm)) thm;

    fun FILTER_DISCH_ALL P thm =
     let fun check tm = P (#t (Thm.rep_cterm tm))
     in  foldr (fn (tm,th) => if check tm then DISCH tm th else th)
                  thm (chyps thm)
     end;

    (* freezeT expensive! *)
    fun UNDISCH thm =
       let val tm = D.mk_prop (#1 (D.dest_imp (cconcl (Thm.freezeT thm))))
       in Thm.implies_elim (thm RS mp) (ASSUME tm) end
       handle U.ERR _ => raise RULES_ERR "UNDISCH" ""
         | THM _ => raise RULES_ERR "UNDISCH" "";

    fun PROVE_HYP ath bth = MP (DISCH (cconcl ath) bth) ath;

    fun IMP_TRANS th1 th2 = th2 RS (th1 RS Thms.imp_trans)
      handle THM (msg, _, _) => raise RULES_ERR "IMP_TRANS" msg;

    (*----------------------------------------------------------------------------
     *        Conjunction
     *---------------------------------------------------------------------------*)

    fun CONJUNCT1 thm = thm RS conjunct1
      handle THM (msg, _, _) => raise RULES_ERR "CONJUNCT1" msg;

    fun CONJUNCT2 thm = thm RS conjunct2
      handle THM (msg, _, _) => raise RULES_ERR "CONJUNCT2" msg;

    fun CONJUNCTS th = CONJUNCTS (CONJUNCT1 th) @ CONJUNCTS (CONJUNCT2 th) handle U.ERR _ => [th];

    fun LIST_CONJ [] = raise RULES_ERR "LIST_CONJ" "empty list"
      | LIST_CONJ [th] = th
      | LIST_CONJ (th :: rst) = MP (MP (conjI COMP (impI RS impI)) th) (LIST_CONJ rst)
          handle THM (msg, _, _) => raise RULES_ERR "LIST_CONJ" msg;

    (*----------------------------------------------------------------------------
     *        Disjunction
     *---------------------------------------------------------------------------*)
    local val {prop,sign,...} = rep_thm disjI1
          val [P,Q] = term_vars prop
          val disj1 = Thm.forall_intr (Thm.cterm_of sign Q) disjI1
    in
    fun DISJ1 thm tm = thm RS (forall_elim (D.drop_prop tm) disj1)
      handle THM (msg, _, _) => raise RULES_ERR "DISJ1" msg;
    end;

    local val {prop,sign,...} = rep_thm disjI2
          val [P,Q] = term_vars prop
          val disj2 = Thm.forall_intr (Thm.cterm_of sign P) disjI2
    in
    fun DISJ2 tm thm = thm RS (forall_elim (D.drop_prop tm) disj2)
      handle THM (msg, _, _) => raise RULES_ERR "DISJ2" msg;
    end;

    (*----------------------------------------------------------------------------
     *
     *                   A1 |- M1, ..., An |- Mn
     *     ---------------------------------------------------
     *     [A1 |- M1 \/ ... \/ Mn, ..., An |- M1 \/ ... \/ Mn]
     *
     *---------------------------------------------------------------------------*)

    fun EVEN_ORS thms =
      let fun blue ldisjs [] _ = []
            | blue ldisjs (th::rst) rdisjs =
                let val tail = tl rdisjs
                    val rdisj_tl = D.list_mk_disj tail
                in fold_rev DISJ2 ldisjs (DISJ1 th rdisj_tl)
                   :: blue (ldisjs @ [cconcl th]) rst tail
                end handle U.ERR _ => [fold_rev DISJ2 ldisjs th]
       in blue [] thms (map cconcl thms) end;

    (*----------------------------------------------------------------------------
     *
     *         A |- P \/ Q   B,P |- R    C,Q |- R
     *     ---------------------------------------------------
     *                     A U B U C |- R
     *
     *---------------------------------------------------------------------------*)

    fun DISJ_CASES th1 th2 th3 =
      let
        val c = D.drop_prop (cconcl th1);
        val (disj1, disj2) = D.dest_disj c;
        val th2' = DISCH disj1 th2;
        val th3' = DISCH disj2 th3;
      in
        th3' RS (th2' RS (th1 RS Thms.tfl_disjE))
          handle THM (msg, _, _) => raise RULES_ERR "DISJ_CASES" msg
      end;

    (*-----------------------------------------------------------------------------
     *
     *       |- A1 \/ ... \/ An     [A1 |- M, ..., An |- M]
     *     ---------------------------------------------------
     *                           |- M
     *
     * Note. The list of theorems may be all jumbled up, so we have to
     * first organize it to align with the first argument (the disjunctive
     * theorem).
     *---------------------------------------------------------------------------*)

    fun organize eq =    (* a bit slow - analogous to insertion sort *)
     let fun extract a alist =
         let fun ex (_,[]) = raise RULES_ERR "organize" "not a permutation.1"
               | ex(left,h::t) = if (eq h a) then (h,rev left@t) else ex(h::left,t)
         in ex ([],alist)
         end
         fun place [] [] = []
           | place (a::rst) alist =
               let val (item,next) = extract a alist
               in item::place rst next
               end
           | place _ _ = raise RULES_ERR "organize" "not a permutation.2"
     in place
     end;
    (* freezeT expensive! *)
    fun DISJ_CASESL disjth thl =
       let val c = cconcl disjth
           fun eq th atm = exists (fn t => HOLogic.dest_Trueprop t
                                           aconv term_of atm)
                                  (#hyps(rep_thm th))
           val tml = D.strip_disj c
           fun DL th [] = raise RULES_ERR "DISJ_CASESL" "no cases"
             | DL th [th1] = PROVE_HYP th th1
             | DL th [th1,th2] = DISJ_CASES th th1 th2
             | DL th (th1::rst) =
                let val tm = #2(D.dest_disj(D.drop_prop(cconcl th)))
                 in DISJ_CASES th th1 (DL (ASSUME tm) rst) end
       in DL (freezeT disjth) (organize eq tml thl)
       end;

    (*----------------------------------------------------------------------------
     *        Universals
     *---------------------------------------------------------------------------*)
    local (* this is fragile *)
          val {prop,sign,...} = rep_thm spec
          val x = hd (tl (term_vars prop))
          val cTV = ctyp_of sign (type_of x)
          val gspec = forall_intr (cterm_of sign x) spec
    in
    fun SPEC tm thm =
       let val {sign,T,...} = rep_cterm tm
           val gspec' = instantiate ([(cTV, ctyp_of sign T)], []) gspec
       in
          thm RS (forall_elim tm gspec')
       end
    end;

    fun SPEC_ALL thm = fold SPEC (#1(D.strip_forall(cconcl thm))) thm;

    val ISPEC = SPEC
    val ISPECL = fold ISPEC;

    (* Not optimized! Too complicated. *)
    local val {prop,sign,...} = rep_thm allI
          val [P] = add_term_vars (prop, [])
          fun cty_theta s = map (fn (i, (S, ty)) => (ctyp_of s (TVar (i, S)), ctyp_of s ty))
          fun ctm_theta s = map (fn (i, (_, tm2)) =>
                                 let val ctm2 = cterm_of s tm2
                                 in (cterm_of s (Var(i,#T(rep_cterm ctm2))), ctm2)
                                 end)
          fun certify s (ty_theta,tm_theta) =
            (cty_theta s (Vartab.dest ty_theta),
             ctm_theta s (Vartab.dest tm_theta))
    in
    fun GEN v th =
       let val gth = forall_intr v th
           val {prop=Const("all",_)$Abs(x,ty,rst),sign,...} = rep_thm gth
           val P' = Abs(x,ty, HOLogic.dest_Trueprop rst)  (* get rid of trueprop *)
           val theta = Pattern.match sign (P,P')
           val allI2 = instantiate (certify sign theta) allI
           val thm = Thm.implies_elim allI2 gth
           val {prop = tp $ (A $ Abs(_,_,M)),sign,...} = rep_thm thm
           val prop' = tp $ (A $ Abs(x,ty,M))
       in ALPHA thm (cterm_of sign prop')
       end
    end;

    val GENL = fold_rev GEN;

    fun GEN_ALL thm =
       let val {prop,sign,...} = rep_thm thm
           val tycheck = cterm_of sign
           val vlist = map tycheck (add_term_vars (prop, []))
      in GENL vlist thm
      end;

    fun MATCH_MP th1 th2 =
       if (D.is_forall (D.drop_prop(cconcl th1)))
       then MATCH_MP (th1 RS spec) th2
       else MP th1 th2;

    (*----------------------------------------------------------------------------
     *        Existentials
     *---------------------------------------------------------------------------*)

    (*---------------------------------------------------------------------------
     * Existential elimination
     *
     *      A1 |- ?x.t[x]   ,   A2, "t[v]" |- t'
     *      ------------------------------------     (variable v occurs nowhere)
     *                A1 u A2 |- t'
     *
     *---------------------------------------------------------------------------*)

    fun CHOOSE (fvar, exth) fact =
      let
        val lam = #2 (D.dest_comb (D.drop_prop (cconcl exth)))
        val redex = D.capply lam fvar
        val {sign, t = t$u,...} = Thm.rep_cterm redex
        val residue = Thm.cterm_of sign (betapply (t, u))
      in
        GEN fvar (DISCH residue fact) RS (exth RS Thms.choose_thm)
          handle THM (msg, _, _) => raise RULES_ERR "CHOOSE" msg
      end;

    local val {prop,sign,...} = rep_thm exI
          val [P,x] = term_vars prop
    in
    fun EXISTS (template,witness) thm =
       let val {prop,sign,...} = rep_thm thm
           val P' = cterm_of sign P
           val x' = cterm_of sign x
           val abstr = #2 (D.dest_comb template)
       in
       thm RS (cterm_instantiate[(P',abstr), (x',witness)] exI)
         handle THM (msg, _, _) => raise RULES_ERR "EXISTS" msg
       end
    end;

    (*----------------------------------------------------------------------------
     *
     *         A |- M
     *   -------------------   [v_1,...,v_n]
     *    A |- ?v1...v_n. M
     *
     *---------------------------------------------------------------------------*)

    fun EXISTL vlist th =
      fold_rev (fn v => fn thm => EXISTS(D.mk_exists(v,cconcl thm), v) thm)
               vlist th;

    (*----------------------------------------------------------------------------
     *
     *       A |- M[x_1,...,x_n]
     *   ----------------------------   [(x |-> y)_1,...,(x |-> y)_n]
     *       A |- ?y_1...y_n. M
     *
     *---------------------------------------------------------------------------*)
    (* Could be improved, but needs "subst_free" for certified terms *)

    fun IT_EXISTS blist th =
       let val {sign,...} = rep_thm th
           val tych = cterm_of sign
           val detype = #t o rep_cterm
           val blist' = map (fn (x,y) => (detype x, detype y)) blist
           fun ex v M  = cterm_of sign (S.mk_exists{Bvar=v,Body = M})

      in
      fold_rev (fn (b as (r1,r2)) => fn thm =>
            EXISTS(ex r2 (subst_free [b]
                       (HOLogic.dest_Trueprop(#prop(rep_thm thm)))), tych r1)
                  thm)
           blist' th
      end;

    (*---------------------------------------------------------------------------
     *  Faster version, that fails for some as yet unknown reason
     * fun IT_EXISTS blist th =
     *    let val {sign,...} = rep_thm th
     *        val tych = cterm_of sign
     *        fun detype (x,y) = ((#t o rep_cterm) x, (#t o rep_cterm) y)
     *   in
     *  fold (fn (b as (r1,r2), thm) =>
     *  EXISTS(D.mk_exists(r2, tych(subst_free[detype b](#t(rep_cterm(cconcl thm))))),
     *           r1) thm)  blist th
     *   end;
     *---------------------------------------------------------------------------*)

    (*----------------------------------------------------------------------------
     *        Rewriting
     *---------------------------------------------------------------------------*)

    fun SUBS thl =
      rewrite_rule (map (fn th => th RS eq_reflection handle THM _ => th) thl);

    val rew_conv = MetaSimplifier.rewrite_cterm (true, false, false) (K (K NONE));

    fun simpl_conv ss thl ctm =
     rew_conv (ss addsimps thl) ctm RS meta_eq_to_obj_eq;

    val RIGHT_ASSOC = rewrite_rule [Thms.disj_assoc];

    (*---------------------------------------------------------------------------
     *                  TERMINATION CONDITION EXTRACTION
     *---------------------------------------------------------------------------*)

    (* Object language quantifier, i.e., "!" *)
    fun Forall v M = S.mk_forall{Bvar=v, Body=M};

    (* Fragile: it's a cong if it is not "R y x ==> cut f R x y = f y" *)
    fun is_cong thm =
      let val {prop, ...} = rep_thm thm
      in case prop
         of (Const("==>",_)$(Const("Trueprop",_)$ _) $
             (Const("==",_) $ (Const ("Wellfounded_Recursion.cut",_) $ f $ R $ a $ x) $ _)) => false
          | _ => true
      end;

    fun dest_equal(Const ("==",_) $
                   (Const ("Trueprop",_) $ lhs)
                   $ (Const ("Trueprop",_) $ rhs)) = {lhs=lhs, rhs=rhs}
      | dest_equal(Const ("==",_) $ lhs $ rhs)  = {lhs=lhs, rhs=rhs}
      | dest_equal tm = S.dest_eq tm;

    fun get_lhs tm = #lhs(dest_equal (HOLogic.dest_Trueprop tm));

    fun dest_all used (Const("all",_) $ (a as Abs _)) = S.dest_abs used a
      | dest_all _ _ = raise RULES_ERR "dest_all" "not a !!";

    val is_all = can (dest_all []);

    fun strip_all used fm =
       if (is_all fm)
       then let val ({Bvar, Body}, used') = dest_all used fm
                val (bvs, core, used'') = strip_all used' Body
            in ((Bvar::bvs), core, used'')
            end
       else ([], fm, used);

    fun break_all(Const("all",_) $ Abs (_,_,body)) = body
      | break_all _ = raise RULES_ERR "break_all" "not a !!";

    fun list_break_all(Const("all",_) $ Abs (s,ty,body)) =
         let val (L,core) = list_break_all body
         in ((s,ty)::L, core)
         end
      | list_break_all tm = ([],tm);

    (*---------------------------------------------------------------------------
     * Rename a term of the form
     *
     *      !!x1 ...xn. x1=M1 ==> ... ==> xn=Mn
     *                  ==> ((%v1...vn. Q) x1 ... xn = g x1 ... xn.
     * to one of
     *
     *      !!v1 ... vn. v1=M1 ==> ... ==> vn=Mn
     *      ==> ((%v1...vn. Q) v1 ... vn = g v1 ... vn.
     *
     * This prevents name problems in extraction, and helps the result to read
     * better. There is a problem with varstructs, since they can introduce more
     * than n variables, and some extra reasoning needs to be done.
     *---------------------------------------------------------------------------*)

    fun get ([],_,L) = rev L
      | get (ant::rst,n,L) =
          case (list_break_all ant)
            of ([],_) => get (rst, n+1,L)
             | (vlist,body) =>
                let val eq = Logic.strip_imp_concl body
                    val (f,args) = S.strip_comb (get_lhs eq)
                    val (vstrl,_) = S.strip_abs f
                    val names  = variantlist (map (#1 o dest_Free) vstrl,
                                              add_term_names(body, []))
                in get (rst, n+1, (names,n)::L) end
                handle TERM _ => get (rst, n+1, L)
                  | U.ERR _ => get (rst, n+1, L);

    (* Note: rename_params_rule counts from 1, not 0 *)
    fun rename thm =
      let val {prop,sign,...} = rep_thm thm
          val tych = cterm_of sign
          val ants = Logic.strip_imp_prems prop
          val news = get (ants,1,[])
      in
      fold rename_params_rule news thm
      end;

    (*---------------------------------------------------------------------------
     * Beta-conversion to the rhs of an equation (taken from hol90/drule.sml)
     *---------------------------------------------------------------------------*)

    fun list_beta_conv tm =
      let fun rbeta th = Thm.transitive th (beta_conversion false (#2(D.dest_eq(cconcl th))))
          fun iter [] = Thm.reflexive tm
            | iter (v::rst) = rbeta (combination(iter rst) (Thm.reflexive v))
      in iter  end;

    (*---------------------------------------------------------------------------
     * Trace information for the rewriter
     *---------------------------------------------------------------------------*)
    val term_ref = ref[] : term list ref
    val ss_ref = ref [] : simpset list ref;
    val thm_ref = ref [] : thm list ref;
    val tracing = ref false;

    fun say s = if !tracing then writeln s else ();

    fun print_thms s L =
      say (cat_lines (s :: map string_of_thm L));

    fun print_cterms s L =
      say (cat_lines (s :: map string_of_cterm L));

    (*---------------------------------------------------------------------------
     * General abstraction handlers, should probably go in USyntax.
     *---------------------------------------------------------------------------*)
    fun mk_aabs (vstr, body) =
      S.mk_abs {Bvar = vstr, Body = body}
      handle U.ERR _ => S.mk_pabs {varstruct = vstr, body = body};

    fun list_mk_aabs (vstrl,tm) =
        fold_rev (fn vstr => fn tm => mk_aabs(vstr,tm)) vstrl tm;

    fun dest_aabs used tm =
       let val ({Bvar,Body}, used') = S.dest_abs used tm
       in (Bvar, Body, used') end
       handle U.ERR _ =>
         let val {varstruct, body, used} = S.dest_pabs used tm
         in (varstruct, body, used) end;

    fun strip_aabs used tm =
       let val (vstr, body, used') = dest_aabs used tm
           val (bvs, core, used'') = strip_aabs used' body
       in (vstr::bvs, core, used'') end
       handle U.ERR _ => ([], tm, used);

    fun dest_combn tm 0 = (tm,[])
      | dest_combn tm n =
         let val {Rator,Rand} = S.dest_comb tm
             val (f,rands) = dest_combn Rator (n-1)
         in (f,Rand::rands)
         end;

    local fun dest_pair M = let val {fst,snd} = S.dest_pair M in (fst,snd) end
          fun mk_fst tm =
              let val ty as Type("*", [fty,sty]) = type_of tm
              in  Const ("fst", ty --> fty) $ tm  end
          fun mk_snd tm =
              let val ty as Type("*", [fty,sty]) = type_of tm
              in  Const ("snd", ty --> sty) $ tm  end
    in
    fun XFILL tych x vstruct =
      let fun traverse p xocc L =
            if (is_Free p)
            then tych xocc::L
            else let val (p1,p2) = dest_pair p
                 in traverse p1 (mk_fst xocc) (traverse p2  (mk_snd xocc) L)
                 end
      in
      traverse vstruct x []
    end end;

    (*---------------------------------------------------------------------------
     * Replace a free tuple (vstr) by a universally quantified variable (a).
     * Note that the notion of "freeness" for a tuple is different than for a
     * variable: if variables in the tuple also occur in any other place than
     * an occurrences of the tuple, they aren't "free" (which is thus probably
     *  the wrong word to use).
     *---------------------------------------------------------------------------*)

    fun VSTRUCT_ELIM tych a vstr th =
      let val L = S.free_vars_lr vstr
          val bind1 = tych (HOLogic.mk_Trueprop (HOLogic.mk_eq(a,vstr)))
          val thm1 = implies_intr bind1 (SUBS [SYM(assume bind1)] th)
          val thm2 = forall_intr_list (map tych L) thm1
          val thm3 = forall_elim_list (XFILL tych a vstr) thm2
      in refl RS
         rewrite_rule [Thm.symmetric (surjective_pairing RS eq_reflection)] thm3
      end;

    fun PGEN tych a vstr th =
      let val a1 = tych a
          val vstr1 = tych vstr
      in
      forall_intr a1
         (if (is_Free vstr)
          then cterm_instantiate [(vstr1,a1)] th
          else VSTRUCT_ELIM tych a vstr th)
      end;

    (*---------------------------------------------------------------------------
     * Takes apart a paired beta-redex, looking like "(\(x,y).N) vstr", into
     *
     *     (([x,y],N),vstr)
     *---------------------------------------------------------------------------*)
    fun dest_pbeta_redex used M n =
      let val (f,args) = dest_combn M n
          val dummy = dest_aabs used f
      in (strip_aabs used f,args)
      end;

    fun pbeta_redex M n = can (U.C (dest_pbeta_redex []) n) M;

    fun dest_impl tm =
      let val ants = Logic.strip_imp_prems tm
          val eq = Logic.strip_imp_concl tm
      in (ants,get_lhs eq)
      end;

    fun restricted t = isSome (S.find_term
                                (fn (Const("Wellfounded_Recursion.cut",_)) =>true | _ => false)
                                t)

    fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th =
     let val globals = func::G
         val pbeta_reduce = simpl_conv empty_ss [split_conv RS eq_reflection];
         val tc_list = ref[]: term list ref
         val dummy = term_ref := []
         val dummy = thm_ref  := []
         val dummy = ss_ref  := []
         val cut_lemma' = cut_lemma RS eq_reflection
         fun prover used ss thm =
         let fun cong_prover ss thm =
             let val dummy = say "cong_prover:"
                 val cntxt = MetaSimplifier.prems_of_ss ss
                 val dummy = print_thms "cntxt:" cntxt
                 val dummy = say "cong rule:"
                 val dummy = say (string_of_thm thm)
                 val dummy = thm_ref := (thm :: !thm_ref)
                 val dummy = ss_ref := (ss :: !ss_ref)
                 (* Unquantified eliminate *)
                 fun uq_eliminate (thm,imp,sign) =
                     let val tych = cterm_of sign
                         val dummy = print_cterms "To eliminate:" [tych imp]
                         val ants = map tych (Logic.strip_imp_prems imp)
                         val eq = Logic.strip_imp_concl imp
                         val lhs = tych(get_lhs eq)
                         val ss' = MetaSimplifier.add_prems (map ASSUME ants) ss
                         val lhs_eq_lhs1 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used) ss' lhs
                           handle U.ERR _ => Thm.reflexive lhs
                         val dummy = print_thms "proven:" [lhs_eq_lhs1]
                         val lhs_eq_lhs2 = implies_intr_list ants lhs_eq_lhs1
                         val lhs_eeq_lhs2 = lhs_eq_lhs2 RS meta_eq_to_obj_eq
                      in
                      lhs_eeq_lhs2 COMP thm
                      end
                 fun pq_eliminate (thm,sign,vlist,imp_body,lhs_eq) =
                  let val ((vstrl, _, used'), args) = dest_pbeta_redex used lhs_eq (length vlist)
                      val dummy = assert (forall (op aconv)
                                          (ListPair.zip (vlist, args)))
                                   "assertion failed in CONTEXT_REWRITE_RULE"
                      val imp_body1 = subst_free (ListPair.zip (args, vstrl))
                                                 imp_body
                      val tych = cterm_of sign
                      val ants1 = map tych (Logic.strip_imp_prems imp_body1)
                      val eq1 = Logic.strip_imp_concl imp_body1
                      val Q = get_lhs eq1
                      val QeqQ1 = pbeta_reduce (tych Q)
                      val Q1 = #2(D.dest_eq(cconcl QeqQ1))
                      val ss' = MetaSimplifier.add_prems (map ASSUME ants1) ss
                      val Q1eeqQ2 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used') ss' Q1
                                    handle U.ERR _ => Thm.reflexive Q1
                      val Q2 = #2 (Logic.dest_equals (Thm.prop_of Q1eeqQ2))
                      val Q3 = tych(list_comb(list_mk_aabs(vstrl,Q2),vstrl))
                      val Q2eeqQ3 = Thm.symmetric(pbeta_reduce Q3 RS eq_reflection)
                      val thA = Thm.transitive(QeqQ1 RS eq_reflection) Q1eeqQ2
                      val QeeqQ3 = Thm.transitive thA Q2eeqQ3 handle THM _ =>
                                   ((Q2eeqQ3 RS meta_eq_to_obj_eq)
                                    RS ((thA RS meta_eq_to_obj_eq) RS trans))
                                    RS eq_reflection
                      val impth = implies_intr_list ants1 QeeqQ3
                      val impth1 = impth RS meta_eq_to_obj_eq
                      (* Need to abstract *)
                      val ant_th = U.itlist2 (PGEN tych) args vstrl impth1
                  in ant_th COMP thm
                  end
                 fun q_eliminate (thm,imp,sign) =
                  let val (vlist, imp_body, used') = strip_all used imp
                      val (ants,Q) = dest_impl imp_body
                  in if (pbeta_redex Q) (length vlist)
                     then pq_eliminate (thm,sign,vlist,imp_body,Q)
                     else
                     let val tych = cterm_of sign
                         val ants1 = map tych ants
                         val ss' = MetaSimplifier.add_prems (map ASSUME ants1) ss
                         val Q_eeq_Q1 = MetaSimplifier.rewrite_cterm
                            (false,true,false) (prover used') ss' (tych Q)
                          handle U.ERR _ => Thm.reflexive (tych Q)
                         val lhs_eeq_lhs2 = implies_intr_list ants1 Q_eeq_Q1
                         val lhs_eq_lhs2 = lhs_eeq_lhs2 RS meta_eq_to_obj_eq
                         val ant_th = forall_intr_list(map tych vlist)lhs_eq_lhs2
                     in
                     ant_th COMP thm
                  end end

                 fun eliminate thm =
                   case (rep_thm thm)
                   of {prop = (Const("==>",_) $ imp $ _), sign, ...} =>
                       eliminate
                        (if not(is_all imp)
                         then uq_eliminate (thm,imp,sign)
                         else q_eliminate (thm,imp,sign))
                                (* Assume that the leading constant is ==,   *)
                    | _ => thm  (* if it is not a ==>                        *)
             in SOME(eliminate (rename thm)) end
             handle U.ERR _ => NONE    (* FIXME handle THM as well?? *)

            fun restrict_prover ss thm =
              let val dummy = say "restrict_prover:"
                  val cntxt = rev(MetaSimplifier.prems_of_ss ss)
                  val dummy = print_thms "cntxt:" cntxt
                  val {prop = Const("==>",_) $ (Const("Trueprop",_) $ A) $ _,
                       sign,...} = rep_thm thm
                  fun genl tm = let val vlist = gen_rems (op aconv)
                                               (add_term_frees(tm,[]), globals)
                                in fold_rev Forall vlist tm
                                end
                  (*--------------------------------------------------------------
                   * This actually isn't quite right, since it will think that
                   * not-fully applied occs. of "f" in the context mean that the
                   * current call is nested. The real solution is to pass in a
                   * term "f v1..vn" which is a pattern that any full application
                   * of "f" will match.
                   *-------------------------------------------------------------*)
                  val func_name = #1(dest_Const func)
                  fun is_func (Const (name,_)) = (name = func_name)
                    | is_func _                = false
                  val rcontext = rev cntxt
                  val cncl = HOLogic.dest_Trueprop o Thm.prop_of
                  val antl = case rcontext of [] => []
                             | _   => [S.list_mk_conj(map cncl rcontext)]
                  val TC = genl(S.list_mk_imp(antl, A))
                  val dummy = print_cterms "func:" [cterm_of sign func]
                  val dummy = print_cterms "TC:"
                                  [cterm_of sign (HOLogic.mk_Trueprop TC)]
                  val dummy = tc_list := (TC :: !tc_list)
                  val nestedp = isSome (S.find_term is_func TC)
                  val dummy = if nestedp then say "nested" else say "not_nested"
                  val dummy = term_ref := ([func,TC]@(!term_ref))
                  val th' = if nestedp then raise RULES_ERR "solver" "nested function"
                            else let val cTC = cterm_of sign
                                                  (HOLogic.mk_Trueprop TC)
                                 in case rcontext of
                                    [] => SPEC_ALL(ASSUME cTC)
                                   | _ => MP (SPEC_ALL (ASSUME cTC))
                                             (LIST_CONJ rcontext)
                                 end
                  val th'' = th' RS thm
              in SOME (th'')
              end handle U.ERR _ => NONE    (* FIXME handle THM as well?? *)
        in
        (if (is_cong thm) then cong_prover else restrict_prover) ss thm
        end
        val ctm = cprop_of th
        val names = add_term_names (term_of ctm, [])
        val th1 = MetaSimplifier.rewrite_cterm(false,true,false)
          (prover names) (empty_ss addsimps [cut_lemma'] addeqcongs congs) ctm
        val th2 = equal_elim th1 th
     in
     (th2, List.filter (not o restricted) (!tc_list))
     end;

    fun prove strict (ptm, tac) =
      let val result =
        if strict then Goals.prove_goalw_cterm [] ptm (fn _ => [tac])
        else
          transform_error (fn () =>
            Goals.prove_goalw_cterm [] ptm (fn _ => [tac])) ()
          handle ERROR_MESSAGE msg => (warning msg; raise RULES_ERR "prove" msg);
      in #1 (freeze_thaw result) end;

    end;