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