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