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