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