src/HOL/Tools/metis_tools.ML
author wenzelm
Fri Oct 16 10:55:07 2009 +0200 (2009-10-16)
changeset 32956 c39860141415
parent 32955 4a78daeb012b
child 32994 ccc07fbbfefd
permissions -rw-r--r--
tuned white space;
     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;