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