src/HOL/Tools/metis_tools.ML
author wenzelm
Wed Jun 20 22:07:52 2007 +0200 (2007-06-20)
changeset 23442 028e39e5e8f3
child 23447 1f16190e3836
permissions -rw-r--r--
The Metis prover (slightly modified version from Larry);
wenzelm@23442
     1
(*  Title:      HOL/Tools/metis_tools.ML
wenzelm@23442
     2
    Author:     Kong W. Susanto and Lawrence C. Paulson, CU Computer Laboratory
wenzelm@23442
     3
    Copyright   Cambridge University 2007
wenzelm@23442
     4
*)
wenzelm@23442
     5
wenzelm@23442
     6
signature METIS_TOOLS =
wenzelm@23442
     7
sig
wenzelm@23442
     8
  val type_lits: bool ref
wenzelm@23442
     9
  val metis_tac : Thm.thm list -> int -> Tactical.tactic
wenzelm@23442
    10
  val setup : theory -> theory
wenzelm@23442
    11
end
wenzelm@23442
    12
wenzelm@23442
    13
structure MetisTools: METIS_TOOLS =
wenzelm@23442
    14
struct
wenzelm@23442
    15
wenzelm@23442
    16
  structure Rc = ResReconstruct;
wenzelm@23442
    17
wenzelm@23442
    18
  val type_lits = ref true;
wenzelm@23442
    19
wenzelm@23442
    20
  (* ------------------------------------------------------------------------- *)
wenzelm@23442
    21
  (* Useful Theorems                                                           *)
wenzelm@23442
    22
  (* ------------------------------------------------------------------------- *)
wenzelm@23442
    23
  val EXCLUDED_MIDDLE' = read_instantiate [("R","False")] notE;
wenzelm@23442
    24
  val EXCLUDED_MIDDLE  = rotate_prems 1 EXCLUDED_MIDDLE';
wenzelm@23442
    25
  val REFL_THM         = incr_indexes 2 (Meson.make_meta_clause refl);  (*Rename from 0,1*)
wenzelm@23442
    26
  val subst_em  = zero_var_indexes (subst RS EXCLUDED_MIDDLE);
wenzelm@23442
    27
  val ssubst_em  = read_instantiate [("t","?s"),("s","?t")] (sym RS subst_em);
wenzelm@23442
    28
wenzelm@23442
    29
  (* ------------------------------------------------------------------------- *)
wenzelm@23442
    30
  (* Useful Functions                                                          *)
wenzelm@23442
    31
  (* ------------------------------------------------------------------------- *)
wenzelm@23442
    32
wenzelm@23442
    33
  (* match untyped terms*)
wenzelm@23442
    34
  fun untyped_aconv (Const(a,_))   (Const(b,_))   = (a=b)
wenzelm@23442
    35
    | untyped_aconv (Free(a,_))    (Free(b,_))    = (a=b)
wenzelm@23442
    36
    | untyped_aconv (Var((a,_),_)) (Var((b,_),_)) = (a=b)   (*the index is ignored!*)
wenzelm@23442
    37
    | untyped_aconv (Bound i)      (Bound j)      = (i=j)
wenzelm@23442
    38
    | untyped_aconv (Abs(a,_,t))  (Abs(b,_,u))    = (a=b) andalso untyped_aconv t u
wenzelm@23442
    39
    | untyped_aconv (t1$t2) (u1$u2)  = untyped_aconv t1 u1 andalso untyped_aconv t2 u2
wenzelm@23442
    40
    | untyped_aconv _              _              = false;
wenzelm@23442
    41
wenzelm@23442
    42
  (* Finding the relative location of an untyped term within a list of terms *)
wenzelm@23442
    43
  fun get_index lit =
wenzelm@23442
    44
    let val lit = Envir.eta_contract lit
wenzelm@23442
    45
        fun get n [] = raise Empty
wenzelm@23442
    46
          | get n (x::xs) = if untyped_aconv lit (Envir.eta_contract (HOLogic.dest_Trueprop x))
wenzelm@23442
    47
                            then n  else get (n+1) xs
wenzelm@23442
    48
    in get 1 end;
wenzelm@23442
    49
wenzelm@23442
    50
  (* ------------------------------------------------------------------------- *)
wenzelm@23442
    51
  (* HOL to FOL  (Isabelle to Metis)                                           *)
wenzelm@23442
    52
  (* ------------------------------------------------------------------------- *)
wenzelm@23442
    53
wenzelm@23442
    54
  fun fn_isa_to_met "equal" = "="
wenzelm@23442
    55
    | fn_isa_to_met x       = x;
wenzelm@23442
    56
wenzelm@23442
    57
  fun metis_lit b c args = (b, (c, args));
wenzelm@23442
    58
wenzelm@23442
    59
  fun hol_type_to_fol (ResClause.AtomV x) = Metis.Term.Var x
wenzelm@23442
    60
    | hol_type_to_fol (ResClause.AtomF x) = Metis.Term.Fn(x,[])
wenzelm@23442
    61
    | hol_type_to_fol (ResClause.Comp(tc,tps)) = Metis.Term.Fn(tc, map hol_type_to_fol tps);
wenzelm@23442
    62
wenzelm@23442
    63
  (*These two functions insert type literals before the real literals. That is the
wenzelm@23442
    64
    opposite order from TPTP linkup, but maybe OK.*)
wenzelm@23442
    65
wenzelm@23442
    66
  fun hol_term_to_fol_FO tm =
wenzelm@23442
    67
    case ResHolClause.strip_comb tm of
wenzelm@23442
    68
        (ResHolClause.CombConst(c,_,tys), tms) =>
wenzelm@23442
    69
          let val tyargs = map hol_type_to_fol tys
wenzelm@23442
    70
              val args   = map hol_term_to_fol_FO tms
wenzelm@23442
    71
          in Metis.Term.Fn (c, tyargs @ args) end
wenzelm@23442
    72
      | (ResHolClause.CombVar(v,_), []) => Metis.Term.Var v
wenzelm@23442
    73
      | _ => error "hol_term_to_fol_FO";
wenzelm@23442
    74
wenzelm@23442
    75
  fun hol_term_to_fol_HO (ResHolClause.CombVar(a, ty)) = Metis.Term.Var a
wenzelm@23442
    76
    | hol_term_to_fol_HO (ResHolClause.CombConst(a, ty, tylist)) =
wenzelm@23442
    77
        Metis.Term.Fn(fn_isa_to_met a, map hol_type_to_fol tylist)
wenzelm@23442
    78
    | hol_term_to_fol_HO (ResHolClause.CombApp(tm1,tm2)) =
wenzelm@23442
    79
         Metis.Term.Fn(".", map hol_term_to_fol_HO [tm1,tm2]);
wenzelm@23442
    80
wenzelm@23442
    81
  fun hol_literal_to_fol true (ResHolClause.Literal (pol, tm)) =  (*first-order*)
wenzelm@23442
    82
        let val (ResHolClause.CombConst(p,_,tys), tms) = ResHolClause.strip_comb tm
wenzelm@23442
    83
            val tylits = if p = "equal" then [] else map hol_type_to_fol tys
wenzelm@23442
    84
            val lits = map hol_term_to_fol_FO tms
wenzelm@23442
    85
        in metis_lit pol (fn_isa_to_met p) (tylits @ lits) end
wenzelm@23442
    86
    | hol_literal_to_fol false (ResHolClause.Literal (pol, tm)) =    (*higher-order*)
wenzelm@23442
    87
        case ResHolClause.strip_comb tm of
wenzelm@23442
    88
            (ResHolClause.CombConst("equal",_,_), tms) =>
wenzelm@23442
    89
              metis_lit pol "=" (map hol_term_to_fol_HO tms)
wenzelm@23442
    90
          | _ => metis_lit pol "{}" [hol_term_to_fol_HO tm];
wenzelm@23442
    91
wenzelm@23442
    92
  fun literals_of_hol_thm isFO  t =
wenzelm@23442
    93
        let val (lits, types_sorts) = ResHolClause.literals_of_term t
wenzelm@23442
    94
        in  (map (hol_literal_to_fol isFO) lits, types_sorts) end;
wenzelm@23442
    95
wenzelm@23442
    96
  fun metis_of_typeLit (ResClause.LTVar (s,x))  = metis_lit false s [Metis.Term.Var x]
wenzelm@23442
    97
    | metis_of_typeLit (ResClause.LTFree (s,x)) = metis_lit true  s [Metis.Term.Fn(x,[])];
wenzelm@23442
    98
wenzelm@23442
    99
  fun metis_of_tfree tf = Metis.Thm.axiom (Metis.LiteralSet.singleton (metis_of_typeLit tf));
wenzelm@23442
   100
wenzelm@23442
   101
  fun hol_thm_to_fol isFO th =
wenzelm@23442
   102
    let val (mlits, types_sorts) =
wenzelm@23442
   103
               (literals_of_hol_thm isFO o HOLogic.dest_Trueprop o prop_of) th
wenzelm@23442
   104
        val (tvar_lits,tfree_lits) = ResClause.add_typs_aux types_sorts
wenzelm@23442
   105
        val tlits = if !type_lits then map metis_of_typeLit tvar_lits else []
wenzelm@23442
   106
    in  (Metis.Thm.axiom (Metis.LiteralSet.fromList(tlits@mlits)), tfree_lits)  end;
wenzelm@23442
   107
wenzelm@23442
   108
  (* ARITY CLAUSE *)
wenzelm@23442
   109
wenzelm@23442
   110
  fun m_arity_cls (ResClause.TConsLit (c,t,args)) =
wenzelm@23442
   111
        metis_lit true (ResClause.make_type_class c) [Metis.Term.Fn(t, map Metis.Term.Var args)]
wenzelm@23442
   112
    | m_arity_cls (ResClause.TVarLit (c,str))     =
wenzelm@23442
   113
        metis_lit false (ResClause.make_type_class c) [Metis.Term.Var str];
wenzelm@23442
   114
wenzelm@23442
   115
  (*TrueI is returned as the Isabelle counterpart because there isn't any.*)
wenzelm@23442
   116
  fun arity_cls thy (ResClause.ArityClause{kind,conclLit,premLits,...}) =
wenzelm@23442
   117
    (TrueI, Metis.Thm.axiom (Metis.LiteralSet.fromList (map m_arity_cls (conclLit :: premLits))));
wenzelm@23442
   118
wenzelm@23442
   119
  (* CLASSREL CLAUSE *)
wenzelm@23442
   120
wenzelm@23442
   121
  fun m_classrel_cls subclass superclass =
wenzelm@23442
   122
    [metis_lit false subclass [Metis.Term.Var "T"], metis_lit true superclass [Metis.Term.Var "T"]];
wenzelm@23442
   123
wenzelm@23442
   124
  fun classrel_cls thy (ResClause.ClassrelClause {axiom_name,subclass,superclass,...}) =
wenzelm@23442
   125
    (TrueI, Metis.Thm.axiom (Metis.LiteralSet.fromList (m_classrel_cls subclass superclass)));
wenzelm@23442
   126
wenzelm@23442
   127
  (* ------------------------------------------------------------------------- *)
wenzelm@23442
   128
  (* FOL to HOL  (Metis to Isabelle)                                           *)
wenzelm@23442
   129
  (* ------------------------------------------------------------------------- *)
wenzelm@23442
   130
wenzelm@23442
   131
 datatype term_or_type = Term of Term.term | Type of Term.typ;
wenzelm@23442
   132
wenzelm@23442
   133
  fun terms_of [] = []
wenzelm@23442
   134
    | terms_of (Term t :: tts) = t :: terms_of tts
wenzelm@23442
   135
    | terms_of (Type _ :: tts) = terms_of tts;
wenzelm@23442
   136
wenzelm@23442
   137
  fun types_of [] = []
wenzelm@23442
   138
    | types_of (Term (Term.Var((a,idx), T)) :: tts) =
wenzelm@23442
   139
        if String.isPrefix "_" a then
wenzelm@23442
   140
            (*Variable generated by Metis, which might have been a type variable.*)
wenzelm@23442
   141
            TVar(("'" ^ a, idx), HOLogic.typeS) :: types_of tts
wenzelm@23442
   142
        else types_of tts
wenzelm@23442
   143
    | types_of (Term _ :: tts) = types_of tts
wenzelm@23442
   144
    | types_of (Type T :: tts) = T :: types_of tts;
wenzelm@23442
   145
wenzelm@23442
   146
  fun apply_list rator nargs rands =
wenzelm@23442
   147
    let val trands = terms_of rands
wenzelm@23442
   148
    in  if length trands = nargs then Term (list_comb(rator, trands))
wenzelm@23442
   149
        else error ("apply_list: wrong number of arguments: " ^ Display.raw_string_of_term rator ^
wenzelm@23442
   150
                    " expected " ^
wenzelm@23442
   151
                    Int.toString nargs ^ " received " ^ commas (map Display.raw_string_of_term trands))
wenzelm@23442
   152
    end;
wenzelm@23442
   153
wenzelm@23442
   154
(*Instantiate constant c with the supplied types, but if they don't match its declared
wenzelm@23442
   155
  sort constraints, replace by a general type.*)
wenzelm@23442
   156
fun const_of ctxt (c,Ts) =  Const (c, dummyT)
wenzelm@23442
   157
(*Formerly, this code was used. Now, we just leave it all to type inference!
wenzelm@23442
   158
  let val thy = ProofContext.theory_of ctxt
wenzelm@23442
   159
      and (types, sorts) = Variable.constraints_of ctxt
wenzelm@23442
   160
      val declaredT = Consts.the_constraint (Sign.consts_of thy) c
wenzelm@23442
   161
      val t = Rc.fix_sorts sorts (Const(c, Sign.const_instance thy (c,Ts)))
wenzelm@23442
   162
  in
wenzelm@23442
   163
      Sign.typ_match thy (declaredT, type_of t) Vartab.empty;
wenzelm@23442
   164
      t
wenzelm@23442
   165
  end
wenzelm@23442
   166
  handle Type.TYPE_MATCH => Const (c, dummyT);
wenzelm@23442
   167
*)
wenzelm@23442
   168
wenzelm@23442
   169
  (*We use 1 rather than 0 because variable references in clauses may otherwise conflict
wenzelm@23442
   170
    with variable constraints in the goal...at least, type inference often fails otherwise.
wenzelm@23442
   171
    SEE ALSO axiom_inf below.*)
wenzelm@23442
   172
  fun mk_var w = Term.Var((w,1), HOLogic.typeT);
wenzelm@23442
   173
wenzelm@23442
   174
  (*include the default sort, if available*)
wenzelm@23442
   175
  fun mk_tfree ctxt w =
wenzelm@23442
   176
    let val ww = "'" ^ w
wenzelm@23442
   177
    in  TFree(ww, getOpt (Variable.def_sort ctxt (ww,~1), HOLogic.typeS))  end;
wenzelm@23442
   178
wenzelm@23442
   179
  (*Remove the "apply" operator from an HO term*)
wenzelm@23442
   180
  fun strip_happ args (Metis.Term.Fn(".",[t,u])) = strip_happ (u::args) t
wenzelm@23442
   181
    | strip_happ args x = (x, args);
wenzelm@23442
   182
wenzelm@23442
   183
  (*Maps metis terms to isabelle terms*)
wenzelm@23442
   184
  fun fol_term_to_hol_RAW ctxt fol_tm =
wenzelm@23442
   185
    let val thy = ProofContext.theory_of ctxt
wenzelm@23442
   186
        val _ = Output.debug (fn () => "fol_term_to_hol: " ^ Metis.Term.toString fol_tm)
wenzelm@23442
   187
        fun tm_to_tt (Metis.Term.Var v) =
wenzelm@23442
   188
               (case Rc.strip_prefix ResClause.tvar_prefix v of
wenzelm@23442
   189
                    SOME w => Type (Rc.make_tvar w)
wenzelm@23442
   190
                  | NONE =>
wenzelm@23442
   191
                case Rc.strip_prefix ResClause.schematic_var_prefix v of
wenzelm@23442
   192
                    SOME w => Term (mk_var w)
wenzelm@23442
   193
                  | NONE   => Term (mk_var v) )
wenzelm@23442
   194
                      (*Var from Metis with a name like _nnn; possibly a type variable*)
wenzelm@23442
   195
          | tm_to_tt (Metis.Term.Fn ("{}", [arg])) = tm_to_tt arg   (*hBOOL*)
wenzelm@23442
   196
          | tm_to_tt (t as Metis.Term.Fn (".",_)) =
wenzelm@23442
   197
              let val (rator,rands) = strip_happ [] t
wenzelm@23442
   198
              in  case rator of
wenzelm@23442
   199
                      Metis.Term.Fn(fname,ts) => applic_to_tt (fname, ts @ rands)
wenzelm@23442
   200
                    | _ => case tm_to_tt rator of
wenzelm@23442
   201
                               Term t => Term (list_comb(t, terms_of (map tm_to_tt rands)))
wenzelm@23442
   202
                             | _ => error "tm_to_tt: HO application"
wenzelm@23442
   203
              end
wenzelm@23442
   204
          | tm_to_tt (Metis.Term.Fn (fname, args)) = applic_to_tt (fname,args)
wenzelm@23442
   205
        and applic_to_tt ("=",ts) =
wenzelm@23442
   206
              Term (list_comb(Const ("op =", HOLogic.typeT), terms_of (map tm_to_tt ts)))
wenzelm@23442
   207
          | applic_to_tt (a,ts) =
wenzelm@23442
   208
              case Rc.strip_prefix ResClause.const_prefix a of
wenzelm@23442
   209
                  SOME b =>
wenzelm@23442
   210
                    let val c = Rc.invert_const b
wenzelm@23442
   211
                        val ntypes = Rc.num_typargs thy c
wenzelm@23442
   212
                        val nterms = length ts - ntypes
wenzelm@23442
   213
                        val tts = map tm_to_tt ts
wenzelm@23442
   214
                        val tys = types_of (List.take(tts,ntypes))
wenzelm@23442
   215
                        val ntyargs = Rc.num_typargs thy c
wenzelm@23442
   216
                    in if length tys = ntyargs then
wenzelm@23442
   217
                           apply_list (const_of ctxt (c, tys)) nterms (List.drop(tts,ntypes))
wenzelm@23442
   218
                       else error ("Constant " ^ c ^ " expects " ^ Int.toString ntyargs ^
wenzelm@23442
   219
                                   " but gets " ^ Int.toString (length tys) ^
wenzelm@23442
   220
                                   " type arguments\n" ^
wenzelm@23442
   221
                                   space_implode "\n" (map (ProofContext.string_of_typ ctxt) tys) ^
wenzelm@23442
   222
                                   " the terms are \n" ^
wenzelm@23442
   223
                                   space_implode "\n" (map (ProofContext.string_of_term ctxt) (terms_of tts)))
wenzelm@23442
   224
                       end
wenzelm@23442
   225
                | NONE => (*Not a constant. Is it a type constructor?*)
wenzelm@23442
   226
              case Rc.strip_prefix ResClause.tconst_prefix a of
wenzelm@23442
   227
                  SOME b => Type (Term.Type(Rc.invert_type_const b, types_of (map tm_to_tt ts)))
wenzelm@23442
   228
                | NONE => (*Maybe a TFree. Should then check that ts=[].*)
wenzelm@23442
   229
              case Rc.strip_prefix ResClause.tfree_prefix a of
wenzelm@23442
   230
                  SOME b => Type (mk_tfree ctxt b)
wenzelm@23442
   231
                | NONE => (*a fixed variable? They are Skolem functions.*)
wenzelm@23442
   232
              case Rc.strip_prefix ResClause.fixed_var_prefix a of
wenzelm@23442
   233
                  SOME b =>
wenzelm@23442
   234
                    let val opr = Term.Free(b, HOLogic.typeT)
wenzelm@23442
   235
                    in  apply_list opr (length ts) (map tm_to_tt ts)  end
wenzelm@23442
   236
                | NONE => error ("unexpected metis function: " ^ a)
wenzelm@23442
   237
    in  case tm_to_tt fol_tm of Term t => t | _ => error "fol_tm_to_tt: Term expected"  end;
wenzelm@23442
   238
wenzelm@23442
   239
  fun fol_terms_to_hol ctxt fol_tms =
wenzelm@23442
   240
    let val ts = map (fol_term_to_hol_RAW ctxt) fol_tms
wenzelm@23442
   241
        val _ = Output.debug (fn () => "  calling infer_types:")
wenzelm@23442
   242
        val _ = app (fn t => Output.debug (fn () => ProofContext.string_of_term ctxt t)) ts
wenzelm@23442
   243
        val ts' = ProofContext.infer_types_pats ctxt ts
wenzelm@23442
   244
                    (*DO NOT freeze TVars in the result*)
wenzelm@23442
   245
        val _ = app (fn t => Output.debug
wenzelm@23442
   246
                      (fn () => "  final term: " ^ ProofContext.string_of_term ctxt t ^
wenzelm@23442
   247
                                "  of type  " ^ ProofContext.string_of_typ ctxt (type_of t)))
wenzelm@23442
   248
                    ts'
wenzelm@23442
   249
    in  ts'  end;
wenzelm@23442
   250
wenzelm@23442
   251
  fun mk_not (Const ("Not", _) $ b) = b
wenzelm@23442
   252
    | mk_not b = HOLogic.mk_not b;
wenzelm@23442
   253
wenzelm@23442
   254
  (* ------------------------------------------------------------------------- *)
wenzelm@23442
   255
  (* FOL step Inference Rules                                                  *)
wenzelm@23442
   256
  (* ------------------------------------------------------------------------- *)
wenzelm@23442
   257
wenzelm@23442
   258
  (*for debugging only*)
wenzelm@23442
   259
  fun print_thpair (fth,th) =
wenzelm@23442
   260
    (Output.debug (fn () => "=============================================");
wenzelm@23442
   261
     Output.debug (fn () => "Metis: " ^ Metis.Thm.toString fth);
wenzelm@23442
   262
     Output.debug (fn () => "Isabelle: " ^ string_of_thm th));
wenzelm@23442
   263
wenzelm@23442
   264
  fun lookth thpairs (fth : Metis.Thm.thm) =
wenzelm@23442
   265
    valOf (AList.lookup (uncurry Metis.Thm.equal) thpairs fth)
wenzelm@23442
   266
    handle Option => error ("Failed to find a Metis theorem " ^ Metis.Thm.toString fth);
wenzelm@23442
   267
wenzelm@23442
   268
  fun is_TrueI th = Thm.eq_thm(TrueI,th);
wenzelm@23442
   269
wenzelm@23442
   270
fun inst_excluded_middle th thy i_atm =
wenzelm@23442
   271
    let val vx = hd (term_vars (prop_of th))
wenzelm@23442
   272
        val substs = [(cterm_of thy vx, cterm_of thy i_atm)]
wenzelm@23442
   273
    in  cterm_instantiate substs th  end;
wenzelm@23442
   274
wenzelm@23442
   275
  (* INFERENCE RULE: AXIOM *)
wenzelm@23442
   276
  fun axiom_inf ctxt thpairs th = incr_indexes 1 (lookth thpairs th);
wenzelm@23442
   277
      (*This causes variables to have an index of 1 by default. SEE ALSO mk_var above.*)
wenzelm@23442
   278
wenzelm@23442
   279
  (* INFERENCE RULE: ASSUME *)
wenzelm@23442
   280
  fun assume_inf ctxt atm =
wenzelm@23442
   281
    inst_excluded_middle EXCLUDED_MIDDLE
wenzelm@23442
   282
      (ProofContext.theory_of ctxt)
wenzelm@23442
   283
      (singleton (fol_terms_to_hol ctxt) (Metis.Term.Fn atm));
wenzelm@23442
   284
wenzelm@23442
   285
  (* INFERENCE RULE: INSTANTIATE. Type instantiations are ignored. Attempting to reconstruct
wenzelm@23442
   286
     them admits new possibilities of errors, e.g. concerning sorts. Instead we try to arrange
wenzelm@23442
   287
     that new TVars are distinct and that types can be inferred from terms.*)
wenzelm@23442
   288
  fun inst_inf ctxt thpairs fsubst th =
wenzelm@23442
   289
    let val thy = ProofContext.theory_of ctxt
wenzelm@23442
   290
        val i_th   = lookth thpairs th
wenzelm@23442
   291
        val i_th_vars = term_vars (prop_of i_th)
wenzelm@23442
   292
        fun find_var x = valOf (List.find (fn Term.Var((a,_),_) => a=x) i_th_vars)
wenzelm@23442
   293
        fun subst_translation (x,y) =
wenzelm@23442
   294
              let val v = find_var x
wenzelm@23442
   295
                  val t = fol_term_to_hol_RAW ctxt y
wenzelm@23442
   296
              in  SOME (cterm_of thy v, t)  end
wenzelm@23442
   297
              handle Option => NONE (*List.find failed for the variable.*)
wenzelm@23442
   298
        fun remove_typeinst (a, t) =
wenzelm@23442
   299
              case Rc.strip_prefix ResClause.schematic_var_prefix a of
wenzelm@23442
   300
                  SOME b => SOME (b, t)
wenzelm@23442
   301
                | NONE   => case Rc.strip_prefix ResClause.tvar_prefix a of
wenzelm@23442
   302
                  SOME _ => NONE          (*type instantiations are forbidden!*)
wenzelm@23442
   303
                | NONE   => SOME (a,t)    (*internal Metis var?*)
wenzelm@23442
   304
        val _ = Output.debug (fn () => "  isa th: " ^ string_of_thm i_th)
wenzelm@23442
   305
        val substs = List.mapPartial remove_typeinst (Metis.Subst.toList fsubst)
wenzelm@23442
   306
        val (vars,rawtms) = ListPair.unzip (List.mapPartial subst_translation substs)
wenzelm@23442
   307
        val tms = ProofContext.infer_types_pats ctxt rawtms
wenzelm@23442
   308
        val ctm_of = cterm_of thy o (map_types o Logic.incr_tvar) (1 + Thm.maxidx_of i_th)
wenzelm@23442
   309
        val substs' = ListPair.zip (vars, map ctm_of tms)
wenzelm@23442
   310
        val _ = Output.debug (fn() => "subst_translations:")
wenzelm@23442
   311
        val _ = app (fn (x,y) => Output.debug (fn () => string_of_cterm x ^ " |-> " ^
wenzelm@23442
   312
                                                        string_of_cterm y))
wenzelm@23442
   313
                  substs'
wenzelm@23442
   314
    in  cterm_instantiate substs' i_th  end;
wenzelm@23442
   315
wenzelm@23442
   316
  (* INFERENCE RULE: RESOLVE *)
wenzelm@23442
   317
wenzelm@23442
   318
  fun resolve_inf ctxt thpairs atm th1 th2 =
wenzelm@23442
   319
    let
wenzelm@23442
   320
      val thy = ProofContext.theory_of ctxt
wenzelm@23442
   321
      val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
wenzelm@23442
   322
      val _ = Output.debug (fn () => "  isa th1 (pos): " ^ string_of_thm i_th1)
wenzelm@23442
   323
      val _ = Output.debug (fn () => "  isa th2 (neg): " ^ string_of_thm i_th2)
wenzelm@23442
   324
    in
wenzelm@23442
   325
      if is_TrueI i_th1 then i_th2 (*Trivial cases where one operand is type info*)
wenzelm@23442
   326
      else if is_TrueI i_th2 then i_th1
wenzelm@23442
   327
      else
wenzelm@23442
   328
        let
wenzelm@23442
   329
          val i_atm = singleton (fol_terms_to_hol ctxt) (Metis.Term.Fn atm)
wenzelm@23442
   330
          val _ = Output.debug (fn () => "  atom: " ^ ProofContext.string_of_term ctxt i_atm)
wenzelm@23442
   331
          val prems_th1 = prems_of i_th1
wenzelm@23442
   332
          val prems_th2 = prems_of i_th2
wenzelm@23442
   333
          val index_th1 = get_index (mk_not i_atm) prems_th1
wenzelm@23442
   334
                handle Empty => error "Failed to find literal in th1"
wenzelm@23442
   335
          val _ = Output.debug (fn () => "  index_th1: " ^ Int.toString index_th1)
wenzelm@23442
   336
          val index_th2 = get_index i_atm prems_th2
wenzelm@23442
   337
                handle Empty => error "Failed to find literal in th2"
wenzelm@23442
   338
          val _ = Output.debug (fn () => "  index_th2: " ^ Int.toString index_th2)
wenzelm@23442
   339
      in  (select_literal index_th1 i_th1) RSN (index_th2, i_th2)  end
wenzelm@23442
   340
    end;
wenzelm@23442
   341
wenzelm@23442
   342
  (* INFERENCE RULE: REFL *)
wenzelm@23442
   343
  fun refl_inf ctxt lit =
wenzelm@23442
   344
    let val thy = ProofContext.theory_of ctxt
wenzelm@23442
   345
        val v_x = hd (term_vars (prop_of REFL_THM))
wenzelm@23442
   346
        val i_lit = singleton (fol_terms_to_hol ctxt) lit
wenzelm@23442
   347
    in  cterm_instantiate [(cterm_of thy v_x, cterm_of thy i_lit)] REFL_THM  end;
wenzelm@23442
   348
wenzelm@23442
   349
  fun get_ty_arg_size thy (Const("op =",_)) = 0  (*equality has no type arguments*)
wenzelm@23442
   350
    | get_ty_arg_size thy (Const(c,_))      = (Rc.num_typargs thy c handle TYPE _ => 0)
wenzelm@23442
   351
    | get_ty_arg_size thy _      = 0;
wenzelm@23442
   352
wenzelm@23442
   353
  (* INFERENCE RULE: EQUALITY *)
wenzelm@23442
   354
  fun equality_inf ctxt isFO thpairs (pos,atm) fp fr =
wenzelm@23442
   355
    let val thy = ProofContext.theory_of ctxt
wenzelm@23442
   356
        val [i_atm,i_tm] = fol_terms_to_hol ctxt [Metis.Term.Fn atm, fr]
wenzelm@23442
   357
        val _ = Output.debug (fn () => "sign of the literal: " ^ Bool.toString pos)
wenzelm@23442
   358
        fun replace_item_list lx 0 (l::ls) = lx::ls
wenzelm@23442
   359
          | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
wenzelm@23442
   360
        fun path_finder_FO tm (p::ps) =
wenzelm@23442
   361
              let val (tm1,args) = Term.strip_comb tm
wenzelm@23442
   362
                  val adjustment = get_ty_arg_size thy tm1
wenzelm@23442
   363
                  val p' = if adjustment > p then p else p-adjustment
wenzelm@23442
   364
                  val tm_p = List.nth(args,p')
wenzelm@23442
   365
                    handle Subscript => error ("equality_inf: " ^ Int.toString p ^ " adj " ^ Int.toString adjustment  ^ " term " ^  ProofContext.string_of_term ctxt tm)
wenzelm@23442
   366
              in
wenzelm@23442
   367
                  Output.debug (fn () => "path_finder: " ^ Int.toString p ^
wenzelm@23442
   368
                                        "  " ^ ProofContext.string_of_term ctxt tm_p);
wenzelm@23442
   369
                  if null ps   (*FIXME: why not use pattern-matching and avoid repetition*)
wenzelm@23442
   370
                  then (tm_p, list_comb (tm1, replace_item_list (Term.Bound 0) p' args))
wenzelm@23442
   371
                  else let val (r,t) = path_finder_FO tm_p ps
wenzelm@23442
   372
                       in (r, list_comb (tm1, replace_item_list t p' args)) end
wenzelm@23442
   373
              end
wenzelm@23442
   374
        fun path_finder_HO tm [] = (tm, Term.Bound 0)
wenzelm@23442
   375
          | path_finder_HO (t$u) (0::ps) = (fn(x,y) => (x, y$u)) (path_finder_HO t ps)
wenzelm@23442
   376
          | path_finder_HO (t$u) (p::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps)
wenzelm@23442
   377
        fun path_finder true tm ps = path_finder_FO tm ps
wenzelm@23442
   378
          | path_finder false (tm as Const("op =",_) $ _ $ _) (p::ps) =
wenzelm@23442
   379
               (*equality: not curried, as other predicates are*)
wenzelm@23442
   380
               if p=0 then path_finder_HO tm (0::1::ps)  (*select first operand*)
wenzelm@23442
   381
               else path_finder_HO tm (p::ps)        (*1 selects second operand*)
wenzelm@23442
   382
          | path_finder false tm (p::ps) =
wenzelm@23442
   383
               path_finder_HO tm ps      (*if not equality, ignore head to skip hBOOL*)
wenzelm@23442
   384
        fun path_finder_lit ((nt as Term.Const ("Not", _)) $ tm_a) idx =
wenzelm@23442
   385
              let val (tm, tm_rslt) = path_finder isFO tm_a idx
wenzelm@23442
   386
              in (tm, nt $ tm_rslt) end
wenzelm@23442
   387
          | path_finder_lit tm_a idx = path_finder isFO tm_a idx
wenzelm@23442
   388
        val (tm_subst, body) = path_finder_lit i_atm fp
wenzelm@23442
   389
        val tm_abs = Term.Abs("x", Term.type_of tm_subst, body)
wenzelm@23442
   390
        val _ = Output.debug (fn () => "abstraction: " ^ ProofContext.string_of_term ctxt tm_abs)
wenzelm@23442
   391
        val _ = Output.debug (fn () => "i_tm: " ^ ProofContext.string_of_term ctxt i_tm)
wenzelm@23442
   392
        val _ = Output.debug (fn () => "located term: " ^ ProofContext.string_of_term ctxt tm_subst)
wenzelm@23442
   393
        val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst)  (*ill typed but gives right max*)
wenzelm@23442
   394
        val subst' = incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
wenzelm@23442
   395
        val _ = Output.debug (fn () => "subst' " ^ string_of_thm subst')
wenzelm@23442
   396
        val eq_terms = map (pairself (cterm_of thy))
wenzelm@23442
   397
                           (ListPair.zip (term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
wenzelm@23442
   398
    in  cterm_instantiate eq_terms subst'  end;
wenzelm@23442
   399
wenzelm@23442
   400
  fun step ctxt isFO thpairs (fol_th, Metis.Proof.Axiom _)                        =
wenzelm@23442
   401
        axiom_inf ctxt thpairs fol_th
wenzelm@23442
   402
    | step ctxt isFO thpairs (_, Metis.Proof.Assume f_atm)                        =
wenzelm@23442
   403
        assume_inf ctxt f_atm
wenzelm@23442
   404
    | step ctxt isFO thpairs (_, Metis.Proof.Subst(f_subst, f_th1))                =
wenzelm@23442
   405
        inst_inf ctxt thpairs f_subst f_th1
wenzelm@23442
   406
    | step ctxt isFO thpairs (_, Metis.Proof.Resolve(f_atm, f_th1, f_th2))        =
wenzelm@23442
   407
        resolve_inf ctxt thpairs f_atm f_th1 f_th2
wenzelm@23442
   408
    | step ctxt isFO thpairs (_, Metis.Proof.Refl f_tm)                           =
wenzelm@23442
   409
        refl_inf ctxt f_tm
wenzelm@23442
   410
    | step ctxt isFO thpairs (_, Metis.Proof.Equality(f_lit, f_p, f_r)) =
wenzelm@23442
   411
        equality_inf ctxt isFO thpairs f_lit f_p f_r;
wenzelm@23442
   412
wenzelm@23442
   413
  val factor = Seq.hd o distinct_subgoals_tac;
wenzelm@23442
   414
wenzelm@23442
   415
  fun real_literal (b, (c, _)) = not (String.isPrefix ResClause.class_prefix c);
wenzelm@23442
   416
wenzelm@23442
   417
  fun translate isFO _    thpairs [] = thpairs
wenzelm@23442
   418
    | translate isFO ctxt thpairs ((fol_th, inf) :: infpairs) =
wenzelm@23442
   419
        let val _ = Output.debug (fn () => "=============================================")
wenzelm@23442
   420
            val _ = Output.debug (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th)
wenzelm@23442
   421
            val _ = Output.debug (fn () => "INFERENCE: " ^ Metis.Proof.inferenceToString inf)
wenzelm@23442
   422
            val th = Meson.flexflex_first_order (factor (step ctxt isFO thpairs (fol_th, inf)))
wenzelm@23442
   423
            val _ = Output.debug (fn () => "ISABELLE THM: " ^ string_of_thm th)
wenzelm@23442
   424
            val _ = Output.debug (fn () => "=============================================")
wenzelm@23442
   425
        in
wenzelm@23442
   426
            if nprems_of th =
wenzelm@23442
   427
        length (filter real_literal (Metis.LiteralSet.toList (Metis.Thm.clause fol_th))) then ()
wenzelm@23442
   428
            else error "Metis: proof reconstruction has gone wrong";
wenzelm@23442
   429
            translate isFO ctxt ((fol_th, th) :: thpairs) infpairs
wenzelm@23442
   430
        end;
wenzelm@23442
   431
wenzelm@23442
   432
  (* ------------------------------------------------------------------------- *)
wenzelm@23442
   433
  (* Translation of HO Clauses                                                 *)
wenzelm@23442
   434
  (* ------------------------------------------------------------------------- *)
wenzelm@23442
   435
wenzelm@23442
   436
  fun cnf_th th = hd (ResAxioms.cnf_axiom th);
wenzelm@23442
   437
wenzelm@23442
   438
  val equal_imp_fequal' = cnf_th (thm"equal_imp_fequal");
wenzelm@23442
   439
  val fequal_imp_equal' = cnf_th (thm"fequal_imp_equal");
wenzelm@23442
   440
wenzelm@23442
   441
  val comb_I  = ResHolClause.comb_I  RS meta_eq_to_obj_eq;
wenzelm@23442
   442
  val comb_K  = ResHolClause.comb_K  RS meta_eq_to_obj_eq;
wenzelm@23442
   443
  val comb_B  = ResHolClause.comb_B  RS meta_eq_to_obj_eq;
wenzelm@23442
   444
wenzelm@23442
   445
  val ext_thm = cnf_th ResHolClause.ext;
wenzelm@23442
   446
wenzelm@23442
   447
  fun dest_Arity (ResClause.ArityClause{premLits,...}) =
wenzelm@23442
   448
        map ResClause.class_of_arityLit premLits;
wenzelm@23442
   449
wenzelm@23442
   450
  fun type_ext thy tms =
wenzelm@23442
   451
    let val subs = ResAtp.tfree_classes_of_terms tms
wenzelm@23442
   452
        val supers = ResAtp.tvar_classes_of_terms tms
wenzelm@23442
   453
        and tycons = ResAtp.type_consts_of_terms thy tms
wenzelm@23442
   454
        val arity_clauses = ResClause.make_arity_clauses thy tycons supers
wenzelm@23442
   455
        val (supers',arity_clauses) = ResClause.make_arity_clauses thy tycons supers
wenzelm@23442
   456
        val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
wenzelm@23442
   457
    in  map (classrel_cls thy) classrel_clauses @ map (arity_cls thy) arity_clauses
wenzelm@23442
   458
    end;
wenzelm@23442
   459
wenzelm@23442
   460
  (* ------------------------------------------------------------------------- *)
wenzelm@23442
   461
  (* Logic maps manage the interface between HOL and first-order logic.        *)
wenzelm@23442
   462
  (* ------------------------------------------------------------------------- *)
wenzelm@23442
   463
wenzelm@23442
   464
  type logic_map =
wenzelm@23442
   465
    {isFO   : bool,
wenzelm@23442
   466
     axioms : (Metis.Thm.thm * Thm.thm) list,
wenzelm@23442
   467
     tfrees : ResClause.type_literal list};
wenzelm@23442
   468
wenzelm@23442
   469
  fun const_in_metis c (pol,(pred,tm_list)) =
wenzelm@23442
   470
    let
wenzelm@23442
   471
      fun in_mterm (Metis.Term.Var nm) = false
wenzelm@23442
   472
        | in_mterm (Metis.Term.Fn (".", tm_list)) = exists in_mterm tm_list
wenzelm@23442
   473
        | in_mterm (Metis.Term.Fn (nm, tm_list)) = c=nm orelse exists in_mterm tm_list
wenzelm@23442
   474
    in  c=pred orelse exists in_mterm tm_list  end;
wenzelm@23442
   475
wenzelm@23442
   476
  (*transform isabelle clause to metis clause *)
wenzelm@23442
   477
  fun add_thm thy (ith, {isFO, axioms, tfrees}) : logic_map =
wenzelm@23442
   478
    let val (mth, tfree_lits) = hol_thm_to_fol isFO ith
wenzelm@23442
   479
        fun add_tfree (tf, axs) =
wenzelm@23442
   480
              if member (op=) tfrees tf then axs
wenzelm@23442
   481
              else (metis_of_tfree tf, TrueI) :: axs
wenzelm@23442
   482
        val new_axioms = foldl add_tfree [] tfree_lits
wenzelm@23442
   483
    in
wenzelm@23442
   484
       {isFO = isFO,
wenzelm@23442
   485
        axioms = (mth, Meson.make_meta_clause ith) :: (new_axioms @ axioms),
wenzelm@23442
   486
        tfrees = tfree_lits union tfrees}
wenzelm@23442
   487
    end;
wenzelm@23442
   488
wenzelm@23442
   489
  (*transform isabelle type / arity clause to metis clause *)
wenzelm@23442
   490
  fun add_type_thm [] lmap = lmap
wenzelm@23442
   491
    | add_type_thm ((ith, mth) :: cls) {isFO, axioms, tfrees} =
wenzelm@23442
   492
        add_type_thm cls {isFO = isFO,
wenzelm@23442
   493
                          axioms = (mth, ith) :: axioms,
wenzelm@23442
   494
                          tfrees = tfrees}
wenzelm@23442
   495
wenzelm@23442
   496
  (* Function to generate metis clauses, including comb and type clauses *)
wenzelm@23442
   497
  fun build_map mode thy cls ths =
wenzelm@23442
   498
    let val isFO = (mode = ResAtp.Fol) orelse
wenzelm@23442
   499
                    (mode <> ResAtp.Hol andalso ResAtp.is_fol_thms (cls @ ths))
wenzelm@23442
   500
        val lmap = foldl (add_thm thy) {isFO = isFO, axioms = [], tfrees = []} (cls @ ths)
wenzelm@23442
   501
        val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap)
wenzelm@23442
   502
        fun used c = exists (Metis.LiteralSet.exists (const_in_metis c)) clause_lists
wenzelm@23442
   503
        (*Now check for the existence of certain combinators*)
wenzelm@23442
   504
        val IK    = if used "c_COMBI" orelse used "c_COMBK" then [comb_I,comb_K] else []
wenzelm@23442
   505
        val BC    = if used "c_COMBB" then [comb_B] else []
wenzelm@23442
   506
        val EQ    = if used "c_fequal" then [fequal_imp_equal', equal_imp_fequal'] else []
wenzelm@23442
   507
        val lmap' = if isFO then lmap else foldl (add_thm thy) lmap ([ext_thm] @ EQ @ IK @ BC)
wenzelm@23442
   508
    in
wenzelm@23442
   509
        add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap'
wenzelm@23442
   510
    end;
wenzelm@23442
   511
wenzelm@23442
   512
  fun refute cls =
wenzelm@23442
   513
      Metis.Resolution.loop (Metis.Resolution.new Metis.Resolution.default cls);
wenzelm@23442
   514
wenzelm@23442
   515
  fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const);
wenzelm@23442
   516
wenzelm@23442
   517
  (* Main function to start metis prove and reconstruction *)
wenzelm@23442
   518
  fun FOL_SOLVE mode ctxt cls ths =
wenzelm@23442
   519
    let val thy = ProofContext.theory_of ctxt
wenzelm@23442
   520
        val _ = if exists(is_false o prop_of) cls then error "problem contains the empty clause"
wenzelm@23442
   521
                else ();
wenzelm@23442
   522
        val _ = ResClause.init thy
wenzelm@23442
   523
        val _ = ResHolClause.init thy
wenzelm@23442
   524
        val _ = Output.debug (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
wenzelm@23442
   525
        val _ = app (fn th => Output.debug (fn () => string_of_thm th)) cls
wenzelm@23442
   526
        val _ = Output.debug (fn () => "THEOREM CLAUSES")
wenzelm@23442
   527
        val _ = app (fn th => Output.debug (fn () => string_of_thm th)) ths
wenzelm@23442
   528
        val {isFO,axioms,tfrees} = build_map mode thy cls ths
wenzelm@23442
   529
        val _ = if null tfrees then ()
wenzelm@23442
   530
                else (Output.debug (fn () => "TFREE CLAUSES");
wenzelm@23442
   531
                      app (fn tf => Output.debug (fn _ => ResClause.tptp_of_typeLit tf)) tfrees)
wenzelm@23442
   532
        val _ = Output.debug (fn () => "CLAUSES GIVEN TO METIS")
wenzelm@23442
   533
        val thms = map #1 axioms
wenzelm@23442
   534
        val _ = app (fn th => Output.debug (fn () => Metis.Thm.toString th)) thms
wenzelm@23442
   535
        val _ = if isFO
wenzelm@23442
   536
                then Output.debug (fn () => "goal is first-order")
wenzelm@23442
   537
                else Output.debug (fn () => "goal is higher-order")
wenzelm@23442
   538
        val _ = Output.debug (fn () => "START METIS PROVE PROCESS")
wenzelm@23442
   539
    in
wenzelm@23442
   540
        case refute thms of
wenzelm@23442
   541
            Metis.Resolution.Contradiction mth =>
wenzelm@23442
   542
              let val _ = Output.debug (fn () => "METIS RECONSTRUCTION START: " ^
wenzelm@23442
   543
                            Metis.Thm.toString mth)
wenzelm@23442
   544
                  val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
wenzelm@23442
   545
                               (*add constraints arising from converting goal to clause form*)
wenzelm@23442
   546
                  val result = translate isFO ctxt' axioms (Metis.Proof.proof mth)
wenzelm@23442
   547
                  val _ = Output.debug (fn () => "METIS COMPLETED")
wenzelm@23442
   548
              in
wenzelm@23442
   549
                  case result of
wenzelm@23442
   550
                      (_,ith)::_ => (Output.debug (fn () => "success: " ^ string_of_thm ith); ith)
wenzelm@23442
   551
                    | _ => error "METIS: no result"
wenzelm@23442
   552
              end
wenzelm@23442
   553
          | Metis.Resolution.Satisfiable _ => error "Metis finds the theorem to be invalid"
wenzelm@23442
   554
    end;
wenzelm@23442
   555
wenzelm@23442
   556
  fun metis_general_tac mode ctxt ths i st0 =
wenzelm@23442
   557
    let val _ = Output.debug (fn () => "Metis called with theorems " ^ cat_lines (map string_of_thm ths))
wenzelm@23442
   558
        val ths' = ResAxioms.cnf_rules_of_ths ths
wenzelm@23442
   559
    in
wenzelm@23442
   560
       (MESON ResAxioms.neg_clausify (fn cls => rtac (FOL_SOLVE mode ctxt cls ths') 1) i
wenzelm@23442
   561
        THEN ResAxioms.expand_defs_tac st0) st0
wenzelm@23442
   562
    end;
wenzelm@23442
   563
wenzelm@23442
   564
  fun metis_tac ths gno st =
wenzelm@23442
   565
    metis_general_tac ResAtp.Auto (ProofContext.init (theory_of_thm st)) ths gno st;
wenzelm@23442
   566
wenzelm@23442
   567
  fun metisF_tac ths gno st =
wenzelm@23442
   568
    metis_general_tac ResAtp.Fol (ProofContext.init (theory_of_thm st)) ths gno st;
wenzelm@23442
   569
wenzelm@23442
   570
  fun metisH_tac ths gno st =
wenzelm@23442
   571
    metis_general_tac ResAtp.Hol (ProofContext.init (theory_of_thm st)) ths gno st;
wenzelm@23442
   572
wenzelm@23442
   573
  fun metis_meth mode ths ctxt =
wenzelm@23442
   574
    Method.SIMPLE_METHOD'
wenzelm@23442
   575
      (setmp ResHolClause.typ_level ResHolClause.T_CONST  (*constant-typed*)
wenzelm@23442
   576
        (setmp ResHolClause.minimize_applies false        (*avoid this optimization*)
wenzelm@23442
   577
          (CHANGED_PROP o metis_general_tac mode ctxt ths)));
wenzelm@23442
   578
wenzelm@23442
   579
  fun metis  ths ctxt = metis_meth ResAtp.Auto ths ctxt;
wenzelm@23442
   580
  fun metisF ths ctxt = metis_meth ResAtp.Fol  ths ctxt;
wenzelm@23442
   581
  fun metisH ths ctxt = metis_meth ResAtp.Hol  ths ctxt;
wenzelm@23442
   582
wenzelm@23442
   583
  val setup =
wenzelm@23442
   584
    Method.add_methods
wenzelm@23442
   585
      [("metis",  Method.thms_ctxt_args metis,  "METIS for FOL & HOL problems"),
wenzelm@23442
   586
       ("metisF", Method.thms_ctxt_args metisF, "METIS for FOL problems"),
wenzelm@23442
   587
       ("metisH", Method.thms_ctxt_args metisH, "METIS for HOL problems"),
wenzelm@23442
   588
       ("finish_clausify",
wenzelm@23442
   589
         Method.no_args (Method.SIMPLE_METHOD' (K (ResAxioms.expand_defs_tac refl))),
wenzelm@23442
   590
    "cleanup after conversion to clauses")];
wenzelm@23442
   591
wenzelm@23442
   592
end;