src/HOL/Tools/Sledgehammer/metis_tactics.ML
author blanchet
Mon Apr 19 18:14:45 2010 +0200 (2010-04-19)
changeset 36230 43d10a494c91
parent 36170 0cdb76723c88
child 36383 6adf1068ac0f
permissions -rw-r--r--
added warning about inconsistent context to Metis;
it makes more sense here than in Sledgehammer, because Sledgehammer is unsound and there's no point in having people panicking about the consistency of their context when their context is in fact consistent
     1 (*  Title:      HOL/Tools/Sledgehammer/metis_tactics.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.
     6 *)
     7 
     8 signature METIS_TACTICS =
     9 sig
    10   val trace: bool Unsynchronized.ref
    11   val type_lits: bool Config.T
    12   val metis_tac: Proof.context -> thm list -> int -> tactic
    13   val metisF_tac: Proof.context -> thm list -> int -> tactic
    14   val metisFT_tac: Proof.context -> thm list -> int -> tactic
    15   val setup: theory -> theory
    16 end
    17 
    18 structure Metis_Tactics : METIS_TACTICS =
    19 struct
    20 
    21 open Sledgehammer_FOL_Clause
    22 open Sledgehammer_Fact_Preprocessor
    23 open Sledgehammer_HOL_Clause
    24 open Sledgehammer_Proof_Reconstruct
    25 open Sledgehammer_Fact_Filter
    26 
    27 val trace = Unsynchronized.ref false;
    28 fun trace_msg msg = if !trace then tracing (msg ()) else ();
    29 
    30 val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" (K true);
    31 
    32 datatype mode = FO | HO | FT  (* first-order, higher-order, fully-typed *)
    33 
    34 (* ------------------------------------------------------------------------- *)
    35 (* Useful Theorems                                                           *)
    36 (* ------------------------------------------------------------------------- *)
    37 val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)}
    38 val REFL_THM = incr_indexes 2 @{lemma "t ~= t ==> False" by simp}
    39 val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp}
    40 val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp}
    41 
    42 (* ------------------------------------------------------------------------- *)
    43 (* Useful Functions                                                          *)
    44 (* ------------------------------------------------------------------------- *)
    45 
    46 (* match untyped terms*)
    47 fun untyped_aconv (Const(a,_))   (Const(b,_))   = (a=b)
    48   | untyped_aconv (Free(a,_))    (Free(b,_))    = (a=b)
    49   | untyped_aconv (Var((a,_),_)) (Var((b,_),_)) = (a=b)   (*the index is ignored!*)
    50   | untyped_aconv (Bound i)      (Bound j)      = (i=j)
    51   | untyped_aconv (Abs(a,_,t))  (Abs(b,_,u))    = (a=b) andalso untyped_aconv t u
    52   | untyped_aconv (t1$t2) (u1$u2)  = untyped_aconv t1 u1 andalso untyped_aconv t2 u2
    53   | untyped_aconv _              _              = false;
    54 
    55 (* Finding the relative location of an untyped term within a list of terms *)
    56 fun get_index lit =
    57   let val lit = Envir.eta_contract lit
    58       fun get n [] = raise Empty
    59         | get n (x::xs) = if untyped_aconv lit (Envir.eta_contract (HOLogic.dest_Trueprop x))
    60                           then n  else get (n+1) xs
    61   in get 1 end;
    62 
    63 (* ------------------------------------------------------------------------- *)
    64 (* HOL to FOL  (Isabelle to Metis)                                           *)
    65 (* ------------------------------------------------------------------------- *)
    66 
    67 fun fn_isa_to_met "equal" = "="
    68   | fn_isa_to_met x       = x;
    69 
    70 fun metis_lit b c args = (b, (c, args));
    71 
    72 fun hol_type_to_fol (TyVar (x, _)) = Metis.Term.Var x
    73   | hol_type_to_fol (TyFree (s, _)) = Metis.Term.Fn (s, [])
    74   | hol_type_to_fol (TyConstr ((s, _), tps)) =
    75     Metis.Term.Fn (s, map hol_type_to_fol tps);
    76 
    77 (*These two functions insert type literals before the real literals. That is the
    78   opposite order from TPTP linkup, but maybe OK.*)
    79 
    80 fun hol_term_to_fol_FO tm =
    81   case strip_combterm_comb tm of
    82       (CombConst ((c, _), _, tys), tms) =>
    83         let val tyargs = map hol_type_to_fol tys
    84             val args   = map hol_term_to_fol_FO tms
    85         in Metis.Term.Fn (c, tyargs @ args) end
    86     | (CombVar ((v, _), _), []) => Metis.Term.Var v
    87     | _ => error "hol_term_to_fol_FO";
    88 
    89 fun hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis.Term.Var s
    90   | hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) =
    91       Metis.Term.Fn (fn_isa_to_met a, map hol_type_to_fol tylist)
    92   | hol_term_to_fol_HO (CombApp (tm1, tm2)) =
    93        Metis.Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]);
    94 
    95 (*The fully-typed translation, to avoid type errors*)
    96 fun wrap_type (tm, ty) = Metis.Term.Fn("ti", [tm, hol_type_to_fol ty]);
    97 
    98 fun hol_term_to_fol_FT (CombVar ((s, _), ty)) = wrap_type (Metis.Term.Var s, ty)
    99   | hol_term_to_fol_FT (CombConst((a, _), ty, _)) =
   100       wrap_type (Metis.Term.Fn(fn_isa_to_met a, []), ty)
   101   | hol_term_to_fol_FT (tm as CombApp(tm1,tm2)) =
   102        wrap_type (Metis.Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]),
   103                   type_of_combterm tm);
   104 
   105 fun hol_literal_to_fol FO (Literal (pol, tm)) =
   106       let val (CombConst((p, _), _, tys), tms) = strip_combterm_comb tm
   107           val tylits = if p = "equal" then [] else map hol_type_to_fol tys
   108           val lits = map hol_term_to_fol_FO tms
   109       in metis_lit pol (fn_isa_to_met p) (tylits @ lits) end
   110   | hol_literal_to_fol HO (Literal (pol, tm)) =
   111      (case strip_combterm_comb tm of
   112           (CombConst(("equal", _), _, _), tms) =>
   113             metis_lit pol "=" (map hol_term_to_fol_HO tms)
   114         | _ => metis_lit pol "{}" [hol_term_to_fol_HO tm])   (*hBOOL*)
   115   | hol_literal_to_fol FT (Literal (pol, tm)) =
   116      (case strip_combterm_comb tm of
   117           (CombConst(("equal", _), _, _), tms) =>
   118             metis_lit pol "=" (map hol_term_to_fol_FT tms)
   119         | _ => metis_lit pol "{}" [hol_term_to_fol_FT tm])   (*hBOOL*);
   120 
   121 fun literals_of_hol_thm thy mode t =
   122       let val (lits, types_sorts) = literals_of_term thy t
   123       in  (map (hol_literal_to_fol mode) lits, types_sorts) end;
   124 
   125 (*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*)
   126 fun metis_of_typeLit pos (LTVar (s,x))  = metis_lit pos s [Metis.Term.Var x]
   127   | metis_of_typeLit pos (LTFree (s,x)) = metis_lit pos s [Metis.Term.Fn(x,[])];
   128 
   129 fun default_sort _ (TVar _) = false
   130   | default_sort ctxt (TFree (x, s)) = (s = the_default [] (Variable.def_sort ctxt (x, ~1)));
   131 
   132 fun metis_of_tfree tf =
   133   Metis.Thm.axiom (Metis.LiteralSet.singleton (metis_of_typeLit true tf));
   134 
   135 fun hol_thm_to_fol is_conjecture ctxt mode th =
   136   let val thy = ProofContext.theory_of ctxt
   137       val (mlits, types_sorts) =
   138              (literals_of_hol_thm thy mode o HOLogic.dest_Trueprop o prop_of) th
   139   in
   140       if is_conjecture then
   141           (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits), add_typs types_sorts)
   142       else
   143         let val tylits = add_typs (filter (not o default_sort ctxt) types_sorts)
   144             val mtylits = if Config.get ctxt type_lits
   145                           then map (metis_of_typeLit false) tylits else []
   146         in
   147           (Metis.Thm.axiom (Metis.LiteralSet.fromList(mtylits @ mlits)), [])
   148         end
   149   end;
   150 
   151 (* ARITY CLAUSE *)
   152 
   153 fun m_arity_cls (TConsLit (c,t,args)) =
   154       metis_lit true (make_type_class c) [Metis.Term.Fn(t, map Metis.Term.Var args)]
   155   | m_arity_cls (TVarLit (c,str))     =
   156       metis_lit false (make_type_class c) [Metis.Term.Var str];
   157 
   158 (*TrueI is returned as the Isabelle counterpart because there isn't any.*)
   159 fun arity_cls (ArityClause {conclLit, premLits, ...}) =
   160   (TrueI,
   161    Metis.Thm.axiom (Metis.LiteralSet.fromList (map m_arity_cls (conclLit :: premLits))));
   162 
   163 (* CLASSREL CLAUSE *)
   164 
   165 fun m_classrel_cls subclass superclass =
   166   [metis_lit false subclass [Metis.Term.Var "T"], metis_lit true superclass [Metis.Term.Var "T"]];
   167 
   168 fun classrel_cls (ClassrelClause {subclass, superclass, ...}) =
   169   (TrueI, Metis.Thm.axiom (Metis.LiteralSet.fromList (m_classrel_cls subclass superclass)));
   170 
   171 (* ------------------------------------------------------------------------- *)
   172 (* FOL to HOL  (Metis to Isabelle)                                           *)
   173 (* ------------------------------------------------------------------------- *)
   174 
   175 datatype term_or_type = Term of Term.term | Type of Term.typ;
   176 
   177 fun terms_of [] = []
   178   | terms_of (Term t :: tts) = t :: terms_of tts
   179   | terms_of (Type _ :: tts) = terms_of tts;
   180 
   181 fun types_of [] = []
   182   | types_of (Term (Term.Var ((a,idx), _)) :: tts) =
   183       if String.isPrefix "_" a then
   184           (*Variable generated by Metis, which might have been a type variable.*)
   185           TVar (("'" ^ a, idx), HOLogic.typeS) :: types_of tts
   186       else types_of tts
   187   | types_of (Term _ :: tts) = types_of tts
   188   | types_of (Type T :: tts) = T :: types_of tts;
   189 
   190 fun apply_list rator nargs rands =
   191   let val trands = terms_of rands
   192   in  if length trands = nargs then Term (list_comb(rator, trands))
   193       else error
   194         ("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global Pure.thy rator ^
   195           " expected " ^ Int.toString nargs ^
   196           " received " ^ commas (map (Syntax.string_of_term_global Pure.thy) trands))
   197   end;
   198 
   199 fun infer_types ctxt =
   200   Syntax.check_terms (ProofContext.set_mode ProofContext.mode_pattern ctxt);
   201 
   202 (*We use 1 rather than 0 because variable references in clauses may otherwise conflict
   203   with variable constraints in the goal...at least, type inference often fails otherwise.
   204   SEE ALSO axiom_inf below.*)
   205 fun mk_var (w,T) = Term.Var((w,1), T);
   206 
   207 (*include the default sort, if available*)
   208 fun mk_tfree ctxt w =
   209   let val ww = "'" ^ w
   210   in  TFree(ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1)))  end;
   211 
   212 (*Remove the "apply" operator from an HO term*)
   213 fun strip_happ args (Metis.Term.Fn(".",[t,u])) = strip_happ (u::args) t
   214   | strip_happ args x = (x, args);
   215 
   216 fun fol_type_to_isa _ (Metis.Term.Var v) =
   217      (case strip_prefix tvar_prefix v of
   218           SOME w => make_tvar w
   219         | NONE   => make_tvar v)
   220   | fol_type_to_isa ctxt (Metis.Term.Fn(x, tys)) =
   221      (case strip_prefix tconst_prefix x of
   222           SOME tc => Term.Type (invert_type_const tc, map (fol_type_to_isa ctxt) tys)
   223         | NONE    =>
   224       case strip_prefix tfree_prefix x of
   225           SOME tf => mk_tfree ctxt tf
   226         | NONE    => error ("fol_type_to_isa: " ^ x));
   227 
   228 (*Maps metis terms to isabelle terms*)
   229 fun fol_term_to_hol_RAW ctxt fol_tm =
   230   let val thy = ProofContext.theory_of ctxt
   231       val _ = trace_msg (fn () => "fol_term_to_hol: " ^ Metis.Term.toString fol_tm)
   232       fun tm_to_tt (Metis.Term.Var v) =
   233              (case strip_prefix tvar_prefix v of
   234                   SOME w => Type (make_tvar w)
   235                 | NONE =>
   236               case strip_prefix schematic_var_prefix v of
   237                   SOME w => Term (mk_var (w, HOLogic.typeT))
   238                 | NONE   => Term (mk_var (v, HOLogic.typeT)) )
   239                     (*Var from Metis with a name like _nnn; possibly a type variable*)
   240         | tm_to_tt (Metis.Term.Fn ("{}", [arg])) = tm_to_tt arg   (*hBOOL*)
   241         | tm_to_tt (t as Metis.Term.Fn (".",_)) =
   242             let val (rator,rands) = strip_happ [] t
   243             in  case rator of
   244                     Metis.Term.Fn(fname,ts) => applic_to_tt (fname, ts @ rands)
   245                   | _ => case tm_to_tt rator of
   246                              Term t => Term (list_comb(t, terms_of (map tm_to_tt rands)))
   247                            | _ => error "tm_to_tt: HO application"
   248             end
   249         | tm_to_tt (Metis.Term.Fn (fname, args)) = applic_to_tt (fname,args)
   250       and applic_to_tt ("=",ts) =
   251             Term (list_comb(Const (@{const_name "op ="}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
   252         | applic_to_tt (a,ts) =
   253             case strip_prefix const_prefix a of
   254                 SOME b =>
   255                   let val c = invert_const b
   256                       val ntypes = num_typargs thy c
   257                       val nterms = length ts - ntypes
   258                       val tts = map tm_to_tt ts
   259                       val tys = types_of (List.take(tts,ntypes))
   260                       val ntyargs = num_typargs thy c
   261                   in if length tys = ntyargs then
   262                          apply_list (Const (c, dummyT)) nterms (List.drop(tts,ntypes))
   263                      else error ("Constant " ^ c ^ " expects " ^ Int.toString ntyargs ^
   264                                  " but gets " ^ Int.toString (length tys) ^
   265                                  " type arguments\n" ^
   266                                  cat_lines (map (Syntax.string_of_typ ctxt) tys) ^
   267                                  " the terms are \n" ^
   268                                  cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
   269                      end
   270               | NONE => (*Not a constant. Is it a type constructor?*)
   271             case strip_prefix tconst_prefix a of
   272                 SOME b =>
   273                   Type (Term.Type (invert_type_const b, types_of (map tm_to_tt ts)))
   274               | NONE => (*Maybe a TFree. Should then check that ts=[].*)
   275             case strip_prefix tfree_prefix a of
   276                 SOME b => Type (mk_tfree ctxt b)
   277               | NONE => (*a fixed variable? They are Skolem functions.*)
   278             case strip_prefix fixed_var_prefix a of
   279                 SOME b =>
   280                   let val opr = Term.Free(b, HOLogic.typeT)
   281                   in  apply_list opr (length ts) (map tm_to_tt ts)  end
   282               | NONE => error ("unexpected metis function: " ^ a)
   283   in  case tm_to_tt fol_tm of Term t => t | _ => error "fol_tm_to_tt: Term expected"  end;
   284 
   285 (*Maps fully-typed metis terms to isabelle terms*)
   286 fun fol_term_to_hol_FT ctxt fol_tm =
   287   let val _ = trace_msg (fn () => "fol_term_to_hol_FT: " ^ Metis.Term.toString fol_tm)
   288       fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) =
   289              (case strip_prefix schematic_var_prefix v of
   290                   SOME w =>  mk_var(w, dummyT)
   291                 | NONE   => mk_var(v, dummyT))
   292         | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) =
   293             Const ("op =", HOLogic.typeT)
   294         | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) =
   295            (case strip_prefix const_prefix x of
   296                 SOME c => Const (invert_const c, dummyT)
   297               | NONE => (*Not a constant. Is it a fixed variable??*)
   298             case strip_prefix fixed_var_prefix x of
   299                 SOME v => Free (v, fol_type_to_isa ctxt ty)
   300               | NONE => error ("fol_term_to_hol_FT bad constant: " ^ x))
   301         | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) =
   302             cvt tm1 $ cvt tm2
   303         | cvt (Metis.Term.Fn (".",[tm1,tm2])) = (*untyped application*)
   304             cvt tm1 $ cvt tm2
   305         | cvt (Metis.Term.Fn ("{}", [arg])) = cvt arg   (*hBOOL*)
   306         | cvt (Metis.Term.Fn ("=", [tm1,tm2])) =
   307             list_comb(Const (@{const_name "op ="}, HOLogic.typeT), map cvt [tm1,tm2])
   308         | cvt (t as Metis.Term.Fn (x, [])) =
   309            (case strip_prefix const_prefix x of
   310                 SOME c => Const (invert_const c, dummyT)
   311               | NONE => (*Not a constant. Is it a fixed variable??*)
   312             case strip_prefix fixed_var_prefix x of
   313                 SOME v => Free (v, dummyT)
   314               | NONE => (trace_msg (fn () => "fol_term_to_hol_FT bad const: " ^ x);
   315                   fol_term_to_hol_RAW ctxt t))
   316         | cvt t = (trace_msg (fn () => "fol_term_to_hol_FT bad term: " ^ Metis.Term.toString t);
   317             fol_term_to_hol_RAW ctxt t)
   318   in  cvt fol_tm   end;
   319 
   320 fun fol_term_to_hol ctxt FO = fol_term_to_hol_RAW ctxt
   321   | fol_term_to_hol ctxt HO = fol_term_to_hol_RAW ctxt
   322   | fol_term_to_hol ctxt FT = fol_term_to_hol_FT ctxt;
   323 
   324 fun fol_terms_to_hol ctxt mode fol_tms =
   325   let val ts = map (fol_term_to_hol ctxt mode) fol_tms
   326       val _ = trace_msg (fn () => "  calling type inference:")
   327       val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts
   328       val ts' = infer_types ctxt ts;
   329       val _ = app (fn t => trace_msg
   330                     (fn () => "  final term: " ^ Syntax.string_of_term ctxt t ^
   331                               "  of type  " ^ Syntax.string_of_typ ctxt (type_of t)))
   332                   ts'
   333   in  ts'  end;
   334 
   335 fun mk_not (Const (@{const_name Not}, _) $ b) = b
   336   | mk_not b = HOLogic.mk_not b;
   337 
   338 val metis_eq = Metis.Term.Fn ("=", []);
   339 
   340 (* ------------------------------------------------------------------------- *)
   341 (* FOL step Inference Rules                                                  *)
   342 (* ------------------------------------------------------------------------- *)
   343 
   344 (*for debugging only*)
   345 fun print_thpair (fth,th) =
   346   (trace_msg (fn () => "=============================================");
   347    trace_msg (fn () => "Metis: " ^ Metis.Thm.toString fth);
   348    trace_msg (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th));
   349 
   350 fun lookth thpairs (fth : Metis.Thm.thm) =
   351   the (AList.lookup (uncurry Metis.Thm.equal) thpairs fth)
   352   handle Option => error ("Failed to find a Metis theorem " ^ Metis.Thm.toString fth);
   353 
   354 fun is_TrueI th = Thm.eq_thm(TrueI,th);
   355 
   356 fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx));
   357 
   358 fun inst_excluded_middle thy i_atm =
   359   let val th = EXCLUDED_MIDDLE
   360       val [vx] = Term.add_vars (prop_of th) []
   361       val substs = [(cterm_of thy (Var vx), cterm_of thy i_atm)]
   362   in  cterm_instantiate substs th  end;
   363 
   364 (* INFERENCE RULE: AXIOM *)
   365 fun axiom_inf thpairs th = incr_indexes 1 (lookth thpairs th);
   366     (*This causes variables to have an index of 1 by default. SEE ALSO mk_var above.*)
   367 
   368 (* INFERENCE RULE: ASSUME *)
   369 fun assume_inf ctxt mode atm =
   370   inst_excluded_middle
   371     (ProofContext.theory_of ctxt)
   372     (singleton (fol_terms_to_hol ctxt mode) (Metis.Term.Fn atm));
   373 
   374 (* INFERENCE RULE: INSTANTIATE (Subst). Type instantiations are ignored. Trying to reconstruct
   375    them admits new possibilities of errors, e.g. concerning sorts. Instead we try to arrange
   376    that new TVars are distinct and that types can be inferred from terms.*)
   377 fun inst_inf ctxt mode thpairs fsubst th =
   378   let val thy = ProofContext.theory_of ctxt
   379       val i_th   = lookth thpairs th
   380       val i_th_vars = Term.add_vars (prop_of i_th) []
   381       fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars)
   382       fun subst_translation (x,y) =
   383             let val v = find_var x
   384                 val t = fol_term_to_hol ctxt mode y (*we call infer_types below*)
   385             in  SOME (cterm_of thy (Var v), t)  end
   386             handle Option =>
   387                 (trace_msg (fn() => "List.find failed for the variable " ^ x ^
   388                                        " in " ^ Display.string_of_thm ctxt i_th);
   389                  NONE)
   390       fun remove_typeinst (a, t) =
   391             case strip_prefix schematic_var_prefix a of
   392                 SOME b => SOME (b, t)
   393               | NONE   => case strip_prefix tvar_prefix a of
   394                 SOME _ => NONE          (*type instantiations are forbidden!*)
   395               | NONE   => SOME (a,t)    (*internal Metis var?*)
   396       val _ = trace_msg (fn () => "  isa th: " ^ Display.string_of_thm ctxt i_th)
   397       val substs = map_filter remove_typeinst (Metis.Subst.toList fsubst)
   398       val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs)
   399       val tms = infer_types ctxt rawtms;
   400       val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
   401       val substs' = ListPair.zip (vars, map ctm_of tms)
   402       val _ = trace_msg (fn () =>
   403         cat_lines ("subst_translations:" ::
   404           (substs' |> map (fn (x, y) =>
   405             Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^
   406             Syntax.string_of_term ctxt (term_of y)))));
   407   in  cterm_instantiate substs' i_th
   408       handle THM (msg, _, _) => error ("metis error (inst_inf): " ^ msg)
   409   end;
   410 
   411 (* INFERENCE RULE: RESOLVE *)
   412 
   413 (*Like RSN, but we rename apart only the type variables. Vars here typically have an index
   414   of 1, and the use of RSN would increase this typically to 3. Instantiations of those Vars
   415   could then fail. See comment on mk_var.*)
   416 fun resolve_inc_tyvars(tha,i,thb) =
   417   let val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha
   418       val ths = Seq.list_of (Thm.bicompose false (false,tha,nprems_of tha) i thb)
   419   in
   420       case distinct Thm.eq_thm ths of
   421         [th] => th
   422       | _ => raise THM ("resolve_inc_tyvars: unique result expected", i, [tha,thb])
   423   end;
   424 
   425 fun resolve_inf ctxt mode thpairs atm th1 th2 =
   426   let
   427     val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
   428     val _ = trace_msg (fn () => "  isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1)
   429     val _ = trace_msg (fn () => "  isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
   430   in
   431     if is_TrueI i_th1 then i_th2 (*Trivial cases where one operand is type info*)
   432     else if is_TrueI i_th2 then i_th1
   433     else
   434       let
   435         val i_atm = singleton (fol_terms_to_hol ctxt mode) (Metis.Term.Fn atm)
   436         val _ = trace_msg (fn () => "  atom: " ^ Syntax.string_of_term ctxt i_atm)
   437         val prems_th1 = prems_of i_th1
   438         val prems_th2 = prems_of i_th2
   439         val index_th1 = get_index (mk_not i_atm) prems_th1
   440               handle Empty => error "Failed to find literal in th1"
   441         val _ = trace_msg (fn () => "  index_th1: " ^ Int.toString index_th1)
   442         val index_th2 = get_index i_atm prems_th2
   443               handle Empty => error "Failed to find literal in th2"
   444         val _ = trace_msg (fn () => "  index_th2: " ^ Int.toString index_th2)
   445     in  resolve_inc_tyvars (Meson.select_literal index_th1 i_th1, index_th2, i_th2)  end
   446   end;
   447 
   448 (* INFERENCE RULE: REFL *)
   449 val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
   450 val refl_idx = 1 + Thm.maxidx_of REFL_THM;
   451 
   452 fun refl_inf ctxt mode t =
   453   let val thy = ProofContext.theory_of ctxt
   454       val i_t = singleton (fol_terms_to_hol ctxt mode) t
   455       val _ = trace_msg (fn () => "  term: " ^ Syntax.string_of_term ctxt i_t)
   456       val c_t = cterm_incr_types thy refl_idx i_t
   457   in  cterm_instantiate [(refl_x, c_t)] REFL_THM  end;
   458 
   459 fun get_ty_arg_size _ (Const (@{const_name "op ="}, _)) = 0  (*equality has no type arguments*)
   460   | get_ty_arg_size thy (Const (c, _)) = (num_typargs thy c handle TYPE _ => 0)
   461   | get_ty_arg_size _ _ = 0;
   462 
   463 (* INFERENCE RULE: EQUALITY *)
   464 fun equality_inf ctxt mode (pos, atm) fp fr =
   465   let val thy = ProofContext.theory_of ctxt
   466       val m_tm = Metis.Term.Fn atm
   467       val [i_atm,i_tm] = fol_terms_to_hol ctxt mode [m_tm, fr]
   468       val _ = trace_msg (fn () => "sign of the literal: " ^ Bool.toString pos)
   469       fun replace_item_list lx 0 (_::ls) = lx::ls
   470         | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
   471       fun path_finder_FO tm [] = (tm, Term.Bound 0)
   472         | path_finder_FO tm (p::ps) =
   473             let val (tm1,args) = strip_comb tm
   474                 val adjustment = get_ty_arg_size thy tm1
   475                 val p' = if adjustment > p then p else p-adjustment
   476                 val tm_p = List.nth(args,p')
   477                   handle Subscript => error ("equality_inf: " ^ Int.toString p ^ " adj " ^
   478                     Int.toString adjustment  ^ " term " ^  Syntax.string_of_term ctxt tm)
   479                 val _ = trace_msg (fn () => "path_finder: " ^ Int.toString p ^
   480                                       "  " ^ Syntax.string_of_term ctxt tm_p)
   481                 val (r,t) = path_finder_FO tm_p ps
   482             in
   483                 (r, list_comb (tm1, replace_item_list t p' args))
   484             end
   485       fun path_finder_HO tm [] = (tm, Term.Bound 0)
   486         | path_finder_HO (t$u) (0::ps) = (fn(x,y) => (x, y$u)) (path_finder_HO t ps)
   487         | path_finder_HO (t$u) (_::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps)
   488       fun path_finder_FT tm [] _ = (tm, Term.Bound 0)
   489         | path_finder_FT tm (0::ps) (Metis.Term.Fn ("ti", [t1, _])) =
   490             path_finder_FT tm ps t1
   491         | path_finder_FT (t$u) (0::ps) (Metis.Term.Fn (".", [t1, _])) =
   492             (fn(x,y) => (x, y$u)) (path_finder_FT t ps t1)
   493         | path_finder_FT (t$u) (1::ps) (Metis.Term.Fn (".", [_, t2])) =
   494             (fn(x,y) => (x, t$y)) (path_finder_FT u ps t2)
   495         | path_finder_FT tm ps t = error ("equality_inf, path_finder_FT: path = " ^
   496                                         space_implode " " (map Int.toString ps) ^
   497                                         " isa-term: " ^  Syntax.string_of_term ctxt tm ^
   498                                         " fol-term: " ^ Metis.Term.toString t)
   499       fun path_finder FO tm ps _ = path_finder_FO tm ps
   500         | path_finder HO (tm as Const(@{const_name "op ="},_) $ _ $ _) (p::ps) _ =
   501              (*equality: not curried, as other predicates are*)
   502              if p=0 then path_finder_HO tm (0::1::ps)  (*select first operand*)
   503              else path_finder_HO tm (p::ps)        (*1 selects second operand*)
   504         | path_finder HO tm (_ :: ps) (Metis.Term.Fn ("{}", [_])) =
   505              path_finder_HO tm ps      (*if not equality, ignore head to skip hBOOL*)
   506         | path_finder FT (tm as Const(@{const_name "op ="}, _) $ _ $ _) (p::ps)
   507                             (Metis.Term.Fn ("=", [t1,t2])) =
   508              (*equality: not curried, as other predicates are*)
   509              if p=0 then path_finder_FT tm (0::1::ps)
   510                           (Metis.Term.Fn (".", [Metis.Term.Fn (".", [metis_eq,t1]), t2]))
   511                           (*select first operand*)
   512              else path_finder_FT tm (p::ps)
   513                    (Metis.Term.Fn (".", [metis_eq,t2]))
   514                    (*1 selects second operand*)
   515         | path_finder FT tm (_ :: ps) (Metis.Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1
   516              (*if not equality, ignore head to skip the hBOOL predicate*)
   517         | path_finder FT tm ps t = path_finder_FT tm ps t  (*really an error case!*)
   518       fun path_finder_lit ((nt as Const (@{const_name Not}, _)) $ tm_a) idx =
   519             let val (tm, tm_rslt) = path_finder mode tm_a idx m_tm
   520             in (tm, nt $ tm_rslt) end
   521         | path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm
   522       val (tm_subst, body) = path_finder_lit i_atm fp
   523       val tm_abs = Term.Abs("x", Term.type_of tm_subst, body)
   524       val _ = trace_msg (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
   525       val _ = trace_msg (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
   526       val _ = trace_msg (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
   527       val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst)  (*ill typed but gives right max*)
   528       val subst' = incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
   529       val _ = trace_msg (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
   530       val eq_terms = map (pairself (cterm_of thy))
   531         (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
   532   in  cterm_instantiate eq_terms subst'  end;
   533 
   534 val factor = Seq.hd o distinct_subgoals_tac;
   535 
   536 fun step _ _ thpairs (fol_th, Metis.Proof.Axiom _) = factor (axiom_inf thpairs fol_th)
   537   | step ctxt mode _ (_, Metis.Proof.Assume f_atm) = assume_inf ctxt mode f_atm
   538   | step ctxt mode thpairs (_, Metis.Proof.Subst (f_subst, f_th1)) =
   539       factor (inst_inf ctxt mode thpairs f_subst f_th1)
   540   | step ctxt mode thpairs (_, Metis.Proof.Resolve(f_atm, f_th1, f_th2)) =
   541       factor (resolve_inf ctxt mode thpairs f_atm f_th1 f_th2)
   542   | step ctxt mode _ (_, Metis.Proof.Refl f_tm) = refl_inf ctxt mode f_tm
   543   | step ctxt mode _ (_, Metis.Proof.Equality (f_lit, f_p, f_r)) =
   544       equality_inf ctxt mode f_lit f_p f_r;
   545 
   546 fun real_literal (_, (c, _)) = not (String.isPrefix class_prefix c);
   547 
   548 fun translate _ _ thpairs [] = thpairs
   549   | translate mode ctxt thpairs ((fol_th, inf) :: infpairs) =
   550       let val _ = trace_msg (fn () => "=============================================")
   551           val _ = trace_msg (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th)
   552           val _ = trace_msg (fn () => "INFERENCE: " ^ Metis.Proof.inferenceToString inf)
   553           val th = Meson.flexflex_first_order (step ctxt mode thpairs (fol_th, inf))
   554           val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
   555           val _ = trace_msg (fn () => "=============================================")
   556           val n_metis_lits =
   557             length (filter real_literal (Metis.LiteralSet.toList (Metis.Thm.clause fol_th)))
   558       in
   559           if nprems_of th = n_metis_lits then ()
   560           else error "Metis: proof reconstruction has gone wrong";
   561           translate mode ctxt ((fol_th, th) :: thpairs) infpairs
   562       end;
   563 
   564 (*Determining which axiom clauses are actually used*)
   565 fun used_axioms axioms (th, Metis.Proof.Axiom _) = SOME (lookth axioms th)
   566   | used_axioms _ _ = NONE;
   567 
   568 (* ------------------------------------------------------------------------- *)
   569 (* Translation of HO Clauses                                                 *)
   570 (* ------------------------------------------------------------------------- *)
   571 
   572 fun cnf_th thy th = hd (cnf_axiom thy th);
   573 
   574 fun type_ext thy tms =
   575   let val subs = tfree_classes_of_terms tms
   576       val supers = tvar_classes_of_terms tms
   577       and tycons = type_consts_of_terms thy tms
   578       val (supers', arity_clauses) = make_arity_clauses thy tycons supers
   579       val classrel_clauses = make_classrel_clauses thy subs supers'
   580   in  map classrel_cls classrel_clauses @ map arity_cls arity_clauses
   581   end;
   582 
   583 (* ------------------------------------------------------------------------- *)
   584 (* Logic maps manage the interface between HOL and first-order logic.        *)
   585 (* ------------------------------------------------------------------------- *)
   586 
   587 type logic_map =
   588   {axioms: (Metis.Thm.thm * thm) list,
   589    tfrees: type_literal list};
   590 
   591 fun const_in_metis c (pred, tm_list) =
   592   let
   593     fun in_mterm (Metis.Term.Var _) = false
   594       | in_mterm (Metis.Term.Fn (".", tm_list)) = exists in_mterm tm_list
   595       | in_mterm (Metis.Term.Fn (nm, tm_list)) = c=nm orelse exists in_mterm tm_list
   596   in  c = pred orelse exists in_mterm tm_list  end;
   597 
   598 (*Extract TFree constraints from context to include as conjecture clauses*)
   599 fun init_tfrees ctxt =
   600   let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts
   601   in  add_typs (Vartab.fold add (#2 (Variable.constraints_of ctxt)) []) end;
   602 
   603 (*transform isabelle type / arity clause to metis clause *)
   604 fun add_type_thm [] lmap = lmap
   605   | add_type_thm ((ith, mth) :: cls) {axioms, tfrees} =
   606       add_type_thm cls {axioms = (mth, ith) :: axioms,
   607                         tfrees = tfrees}
   608 
   609 (*Insert non-logical axioms corresponding to all accumulated TFrees*)
   610 fun add_tfrees {axioms, tfrees} : logic_map =
   611      {axioms = (map (fn tf => (metis_of_tfree tf, TrueI)) (distinct op= tfrees)) @ axioms,
   612       tfrees = tfrees};
   613 
   614 fun string_of_mode FO = "FO"
   615   | string_of_mode HO = "HO"
   616   | string_of_mode FT = "FT"
   617 
   618 (* Function to generate metis clauses, including comb and type clauses *)
   619 fun build_map mode0 ctxt cls ths =
   620   let val thy = ProofContext.theory_of ctxt
   621       (*The modes FO and FT are sticky. HO can be downgraded to FO.*)
   622       fun set_mode FO = FO
   623         | set_mode HO = if forall (Meson.is_fol_term thy o prop_of) (cls@ths) then FO else HO
   624         | set_mode FT = FT
   625       val mode = set_mode mode0
   626       (*transform isabelle clause to metis clause *)
   627       fun add_thm is_conjecture ith {axioms, tfrees} : logic_map =
   628         let val (mth, tfree_lits) = hol_thm_to_fol is_conjecture ctxt mode ith
   629         in
   630            {axioms = (mth, Meson.make_meta_clause ith) :: axioms,
   631             tfrees = union (op =) tfree_lits tfrees}
   632         end;
   633       val lmap0 = fold (add_thm true) cls {axioms = [], tfrees = init_tfrees ctxt}
   634       val lmap = fold (add_thm false) ths (add_tfrees lmap0)
   635       val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap)
   636       fun used c = exists (Metis.LiteralSet.exists (const_in_metis c o #2)) clause_lists
   637       (*Now check for the existence of certain combinators*)
   638       val thI  = if used "c_COMBI" then [cnf_th @{theory} @{thm COMBI_def}] else []
   639       val thK  = if used "c_COMBK" then [cnf_th @{theory} @{thm COMBK_def}] else []
   640       val thB   = if used "c_COMBB" then [cnf_th @{theory} @{thm COMBB_def}] else []
   641       val thC   = if used "c_COMBC" then [cnf_th @{theory} @{thm COMBC_def}] else []
   642       val thS   = if used "c_COMBS" then [cnf_th @{theory} @{thm COMBS_def}] else []
   643       val thEQ  = if used "c_fequal" then [cnf_th @{theory} @{thm fequal_imp_equal}, cnf_th @{theory} @{thm equal_imp_fequal}] else []
   644       val lmap' = if mode=FO then lmap
   645                   else fold (add_thm false) (thEQ @ thS @ thC @ thB @ thK @ thI) lmap
   646   in
   647       (mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap')
   648   end;
   649 
   650 fun refute cls =
   651     Metis.Resolution.loop (Metis.Resolution.new Metis.Resolution.default cls);
   652 
   653 fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const);
   654 
   655 fun common_thm ths1 ths2 = exists (member Thm.eq_thm ths1) (map Meson.make_meta_clause ths2);
   656 
   657 exception METIS of string;
   658 
   659 (* Main function to start metis prove and reconstruction *)
   660 fun FOL_SOLVE mode ctxt cls ths0 =
   661   let val thy = ProofContext.theory_of ctxt
   662       val th_cls_pairs =
   663         map (fn th => (Thm.get_name_hint th, cnf_axiom thy th)) ths0
   664       val ths = maps #2 th_cls_pairs
   665       val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
   666       val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls
   667       val _ = trace_msg (fn () => "THEOREM CLAUSES")
   668       val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) ths
   669       val (mode, {axioms,tfrees}) = build_map mode ctxt cls ths
   670       val _ = if null tfrees then ()
   671               else (trace_msg (fn () => "TFREE CLAUSES");
   672                     app (fn tf => trace_msg (fn _ => tptp_of_typeLit true tf)) tfrees)
   673       val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS")
   674       val thms = map #1 axioms
   675       val _ = app (fn th => trace_msg (fn () => Metis.Thm.toString th)) thms
   676       val _ = trace_msg (fn () => "mode = " ^ string_of_mode mode)
   677       val _ = trace_msg (fn () => "START METIS PROVE PROCESS")
   678   in
   679       case filter (is_false o prop_of) cls of
   680           false_th::_ => [false_th RS @{thm FalseE}]
   681         | [] =>
   682       case refute thms of
   683           Metis.Resolution.Contradiction mth =>
   684             let val _ = trace_msg (fn () => "METIS RECONSTRUCTION START: " ^
   685                           Metis.Thm.toString mth)
   686                 val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
   687                              (*add constraints arising from converting goal to clause form*)
   688                 val proof = Metis.Proof.proof mth
   689                 val result = translate mode ctxt' axioms proof
   690                 and used = map_filter (used_axioms axioms) proof
   691                 val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:")
   692                 val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used
   693                 val unused = th_cls_pairs |> map_filter (fn (name, cls) =>
   694                   if common_thm used cls then NONE else SOME name)
   695             in
   696                 if not (common_thm used cls) then
   697                   warning "Metis: The goal is provable because the context is \
   698                           \inconsistent."
   699                 else if not (null unused) then
   700                   warning ("Metis: Unused theorems: " ^ commas_quote unused
   701                            ^ ".")
   702                 else
   703                   ();
   704                 case result of
   705                     (_,ith)::_ =>
   706                         (trace_msg (fn () => "Success: " ^ Display.string_of_thm ctxt ith);
   707                          [ith])
   708                   | _ => (trace_msg (fn () => "Metis: No result");
   709                           [])
   710             end
   711         | Metis.Resolution.Satisfiable _ =>
   712             (trace_msg (fn () => "Metis: No first-order proof with the lemmas supplied");
   713              [])
   714   end;
   715 
   716 fun metis_general_tac mode ctxt ths i st0 =
   717   let val _ = trace_msg (fn () =>
   718         "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
   719   in
   720     if exists_type type_has_topsort (prop_of st0)
   721     then raise METIS "Metis: Proof state contains the universal sort {}"
   722     else
   723       (Meson.MESON neg_clausify
   724         (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) ctxt i
   725           THEN Meson_Tactic.expand_defs_tac st0) st0
   726   end
   727   handle METIS s => (warning ("Metis: " ^ s); Seq.empty);
   728 
   729 val metis_tac = metis_general_tac HO;
   730 val metisF_tac = metis_general_tac FO;
   731 val metisFT_tac = metis_general_tac FT;
   732 
   733 fun method name mode comment = Method.setup name (Attrib.thms >> (fn ths => fn ctxt =>
   734   SIMPLE_METHOD' (CHANGED_PROP o metis_general_tac mode ctxt ths))) comment;
   735 
   736 val setup =
   737   type_lits_setup #>
   738   method @{binding metis} HO "METIS for FOL and HOL problems" #>
   739   method @{binding metisF} FO "METIS for FOL problems" #>
   740   method @{binding metisFT} FT "METIS with fully-typed translation" #>
   741   Method.setup @{binding finish_clausify}
   742     (Scan.succeed (K (SIMPLE_METHOD (Meson_Tactic.expand_defs_tac refl))))
   743     "cleanup after conversion to clauses";
   744 
   745 end;