src/HOL/Tools/metis_tools.ML
author haftmann
Tue Oct 20 16:13:01 2009 +0200 (2009-10-20)
changeset 33037 b22e44496dc2
parent 32994 ccc07fbbfefd
child 33038 8f9594c31de4
permissions -rw-r--r--
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
     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, _)) = Metis.Term.Var a
    85   | hol_term_to_fol_HO (ResHolClause.CombConst (a, _, 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 _ (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 {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), _)) :: 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 _ (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, _])) =
   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 ("=",[]), _])) =
   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 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 i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
   422     val _ = trace_msg (fn () => "  isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1)
   423     val _ = trace_msg (fn () => "  isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
   424   in
   425     if is_TrueI i_th1 then i_th2 (*Trivial cases where one operand is type info*)
   426     else if is_TrueI i_th2 then i_th1
   427     else
   428       let
   429         val i_atm = singleton (fol_terms_to_hol ctxt mode) (Metis.Term.Fn atm)
   430         val _ = trace_msg (fn () => "  atom: " ^ Syntax.string_of_term ctxt i_atm)
   431         val prems_th1 = prems_of i_th1
   432         val prems_th2 = prems_of i_th2
   433         val index_th1 = get_index (mk_not i_atm) prems_th1
   434               handle Empty => error "Failed to find literal in th1"
   435         val _ = trace_msg (fn () => "  index_th1: " ^ Int.toString index_th1)
   436         val index_th2 = get_index i_atm prems_th2
   437               handle Empty => error "Failed to find literal in th2"
   438         val _ = trace_msg (fn () => "  index_th2: " ^ Int.toString index_th2)
   439     in  resolve_inc_tyvars (Meson.select_literal index_th1 i_th1, index_th2, i_th2)  end
   440   end;
   441 
   442 (* INFERENCE RULE: REFL *)
   443 val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
   444 val refl_idx = 1 + Thm.maxidx_of REFL_THM;
   445 
   446 fun refl_inf ctxt mode t =
   447   let val thy = ProofContext.theory_of ctxt
   448       val i_t = singleton (fol_terms_to_hol ctxt mode) t
   449       val _ = trace_msg (fn () => "  term: " ^ Syntax.string_of_term ctxt i_t)
   450       val c_t = cterm_incr_types thy refl_idx i_t
   451   in  cterm_instantiate [(refl_x, c_t)] REFL_THM  end;
   452 
   453 fun get_ty_arg_size _ (Const ("op =", _)) = 0  (*equality has no type arguments*)
   454   | get_ty_arg_size thy (Const (c, _)) = (Recon.num_typargs thy c handle TYPE _ => 0)
   455   | get_ty_arg_size _ _ = 0;
   456 
   457 (* INFERENCE RULE: EQUALITY *)
   458 fun equality_inf ctxt mode (pos, atm) fp fr =
   459   let val thy = ProofContext.theory_of ctxt
   460       val m_tm = Metis.Term.Fn atm
   461       val [i_atm,i_tm] = fol_terms_to_hol ctxt mode [m_tm, fr]
   462       val _ = trace_msg (fn () => "sign of the literal: " ^ Bool.toString pos)
   463       fun replace_item_list lx 0 (_::ls) = lx::ls
   464         | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
   465       fun path_finder_FO tm [] = (tm, Term.Bound 0)
   466         | path_finder_FO tm (p::ps) =
   467             let val (tm1,args) = Term.strip_comb tm
   468                 val adjustment = get_ty_arg_size thy tm1
   469                 val p' = if adjustment > p then p else p-adjustment
   470                 val tm_p = List.nth(args,p')
   471                   handle Subscript => error ("equality_inf: " ^ Int.toString p ^ " adj " ^
   472                     Int.toString adjustment  ^ " term " ^  Syntax.string_of_term ctxt tm)
   473                 val _ = trace_msg (fn () => "path_finder: " ^ Int.toString p ^
   474                                       "  " ^ Syntax.string_of_term ctxt tm_p)
   475                 val (r,t) = path_finder_FO tm_p ps
   476             in
   477                 (r, list_comb (tm1, replace_item_list t p' args))
   478             end
   479       fun path_finder_HO tm [] = (tm, Term.Bound 0)
   480         | path_finder_HO (t$u) (0::ps) = (fn(x,y) => (x, y$u)) (path_finder_HO t ps)
   481         | path_finder_HO (t$u) (_::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps)
   482       fun path_finder_FT tm [] _ = (tm, Term.Bound 0)
   483         | path_finder_FT tm (0::ps) (Metis.Term.Fn ("ti", [t1, _])) =
   484             path_finder_FT tm ps t1
   485         | path_finder_FT (t$u) (0::ps) (Metis.Term.Fn (".", [t1, _])) =
   486             (fn(x,y) => (x, y$u)) (path_finder_FT t ps t1)
   487         | path_finder_FT (t$u) (1::ps) (Metis.Term.Fn (".", [_, t2])) =
   488             (fn(x,y) => (x, t$y)) (path_finder_FT u ps t2)
   489         | path_finder_FT tm ps t = error ("equality_inf, path_finder_FT: path = " ^
   490                                         space_implode " " (map Int.toString ps) ^
   491                                         " isa-term: " ^  Syntax.string_of_term ctxt tm ^
   492                                         " fol-term: " ^ Metis.Term.toString t)
   493       fun path_finder FO tm ps _ = path_finder_FO tm ps
   494         | path_finder HO (tm as Const("op =",_) $ _ $ _) (p::ps) _ =
   495              (*equality: not curried, as other predicates are*)
   496              if p=0 then path_finder_HO tm (0::1::ps)  (*select first operand*)
   497              else path_finder_HO tm (p::ps)        (*1 selects second operand*)
   498         | path_finder HO tm (_ :: ps) (Metis.Term.Fn ("{}", [_])) =
   499              path_finder_HO tm ps      (*if not equality, ignore head to skip hBOOL*)
   500         | path_finder FT (tm as Const("op =",_) $ _ $ _) (p::ps)
   501                             (Metis.Term.Fn ("=", [t1,t2])) =
   502              (*equality: not curried, as other predicates are*)
   503              if p=0 then path_finder_FT tm (0::1::ps)
   504                           (Metis.Term.Fn (".", [Metis.Term.Fn (".", [metis_eq,t1]), t2]))
   505                           (*select first operand*)
   506              else path_finder_FT tm (p::ps)
   507                    (Metis.Term.Fn (".", [metis_eq,t2]))
   508                    (*1 selects second operand*)
   509         | path_finder FT tm (_ :: ps) (Metis.Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1
   510              (*if not equality, ignore head to skip the hBOOL predicate*)
   511         | path_finder FT tm ps t = path_finder_FT tm ps t  (*really an error case!*)
   512       fun path_finder_lit ((nt as Term.Const ("Not", _)) $ tm_a) idx =
   513             let val (tm, tm_rslt) = path_finder mode tm_a idx m_tm
   514             in (tm, nt $ tm_rslt) end
   515         | path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm
   516       val (tm_subst, body) = path_finder_lit i_atm fp
   517       val tm_abs = Term.Abs("x", Term.type_of tm_subst, body)
   518       val _ = trace_msg (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
   519       val _ = trace_msg (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
   520       val _ = trace_msg (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
   521       val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst)  (*ill typed but gives right max*)
   522       val subst' = incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
   523       val _ = trace_msg (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
   524       val eq_terms = map (pairself (cterm_of thy))
   525                          (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
   526   in  cterm_instantiate eq_terms subst'  end;
   527 
   528 val factor = Seq.hd o distinct_subgoals_tac;
   529 
   530 fun step _ _ thpairs (fol_th, Metis.Proof.Axiom _) = factor (axiom_inf thpairs fol_th)
   531   | step ctxt mode _ (_, Metis.Proof.Assume f_atm) = assume_inf ctxt mode f_atm
   532   | step ctxt mode thpairs (_, Metis.Proof.Subst (f_subst, f_th1)) =
   533       factor (inst_inf ctxt mode thpairs f_subst f_th1)
   534   | step ctxt mode thpairs (_, Metis.Proof.Resolve(f_atm, f_th1, f_th2)) =
   535       factor (resolve_inf ctxt mode thpairs f_atm f_th1 f_th2)
   536   | step ctxt mode _ (_, Metis.Proof.Refl f_tm) = refl_inf ctxt mode f_tm
   537   | step ctxt mode _ (_, Metis.Proof.Equality (f_lit, f_p, f_r)) =
   538       equality_inf ctxt mode f_lit f_p f_r;
   539 
   540 fun real_literal (_, (c, _)) = not (String.isPrefix ResClause.class_prefix c);
   541 
   542 fun translate _ _ thpairs [] = thpairs
   543   | translate mode ctxt thpairs ((fol_th, inf) :: infpairs) =
   544       let val _ = trace_msg (fn () => "=============================================")
   545           val _ = trace_msg (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th)
   546           val _ = trace_msg (fn () => "INFERENCE: " ^ Metis.Proof.inferenceToString inf)
   547           val th = Meson.flexflex_first_order (step ctxt mode thpairs (fol_th, inf))
   548           val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
   549           val _ = trace_msg (fn () => "=============================================")
   550           val n_metis_lits =
   551             length (filter real_literal (Metis.LiteralSet.toList (Metis.Thm.clause fol_th)))
   552       in
   553           if nprems_of th = n_metis_lits then ()
   554           else error "Metis: proof reconstruction has gone wrong";
   555           translate mode ctxt ((fol_th, th) :: thpairs) infpairs
   556       end;
   557 
   558 (*Determining which axiom clauses are actually used*)
   559 fun used_axioms axioms (th, Metis.Proof.Axiom _) = SOME (lookth axioms th)
   560   | used_axioms _ _ = NONE;
   561 
   562 (* ------------------------------------------------------------------------- *)
   563 (* Translation of HO Clauses                                                 *)
   564 (* ------------------------------------------------------------------------- *)
   565 
   566 fun cnf_th thy th = hd (ResAxioms.cnf_axiom thy th);
   567 
   568 val equal_imp_fequal' = cnf_th @{theory} @{thm equal_imp_fequal};
   569 val fequal_imp_equal' = cnf_th @{theory} @{thm fequal_imp_equal};
   570 
   571 val comb_I = cnf_th @{theory} ResHolClause.comb_I;
   572 val comb_K = cnf_th @{theory} ResHolClause.comb_K;
   573 val comb_B = cnf_th @{theory} ResHolClause.comb_B;
   574 val comb_C = cnf_th @{theory} ResHolClause.comb_C;
   575 val comb_S = cnf_th @{theory} ResHolClause.comb_S;
   576 
   577 fun type_ext thy tms =
   578   let val subs = ResAtp.tfree_classes_of_terms tms
   579       val supers = ResAtp.tvar_classes_of_terms tms
   580       and tycons = ResAtp.type_consts_of_terms thy tms
   581       val (supers', arity_clauses) = ResClause.make_arity_clauses thy tycons supers
   582       val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
   583   in  map classrel_cls classrel_clauses @ map arity_cls arity_clauses
   584   end;
   585 
   586 (* ------------------------------------------------------------------------- *)
   587 (* Logic maps manage the interface between HOL and first-order logic.        *)
   588 (* ------------------------------------------------------------------------- *)
   589 
   590 type logic_map =
   591   {axioms : (Metis.Thm.thm * Thm.thm) list,
   592    tfrees : ResClause.type_literal list};
   593 
   594 fun const_in_metis c (pred, tm_list) =
   595   let
   596     fun in_mterm (Metis.Term.Var _) = false
   597       | in_mterm (Metis.Term.Fn (".", tm_list)) = exists in_mterm tm_list
   598       | in_mterm (Metis.Term.Fn (nm, tm_list)) = c=nm orelse exists in_mterm tm_list
   599   in  c = pred orelse exists in_mterm tm_list  end;
   600 
   601 (*Extract TFree constraints from context to include as conjecture clauses*)
   602 fun init_tfrees ctxt =
   603   let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts
   604   in  ResClause.add_typs (Vartab.fold add (#2 (Variable.constraints_of ctxt)) []) end;
   605 
   606 (*transform isabelle type / arity clause to metis clause *)
   607 fun add_type_thm [] lmap = lmap
   608   | add_type_thm ((ith, mth) :: cls) {axioms, tfrees} =
   609       add_type_thm cls {axioms = (mth, ith) :: axioms,
   610                         tfrees = tfrees}
   611 
   612 (*Insert non-logical axioms corresponding to all accumulated TFrees*)
   613 fun add_tfrees {axioms, tfrees} : logic_map =
   614      {axioms = (map (fn tf => (metis_of_tfree tf, TrueI)) (distinct op= tfrees)) @ axioms,
   615       tfrees = tfrees};
   616 
   617 fun string_of_mode FO = "FO"
   618   | string_of_mode HO = "HO"
   619   | string_of_mode FT = "FT"
   620 
   621 (* Function to generate metis clauses, including comb and type clauses *)
   622 fun build_map mode0 ctxt cls ths =
   623   let val thy = ProofContext.theory_of ctxt
   624       (*The modes FO and FT are sticky. HO can be downgraded to FO.*)
   625       fun set_mode FO = FO
   626         | set_mode HO = if forall (Meson.is_fol_term thy o prop_of) (cls@ths) then FO else HO
   627         | set_mode FT = FT
   628       val mode = set_mode mode0
   629       (*transform isabelle clause to metis clause *)
   630       fun add_thm is_conjecture (ith, {axioms, tfrees}) : logic_map =
   631         let val (mth, tfree_lits) = hol_thm_to_fol is_conjecture ctxt mode ith
   632         in
   633            {axioms = (mth, Meson.make_meta_clause ith) :: axioms,
   634             tfrees = gen_union (op =) (tfree_lits, tfrees)}
   635         end;
   636       val lmap0 = List.foldl (add_thm true)
   637                         {axioms = [], tfrees = init_tfrees ctxt} cls
   638       val lmap = List.foldl (add_thm false) (add_tfrees lmap0) ths
   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 List.foldl (add_thm false) lmap (thEQ @ thS @ thC @ thB @ thK @ thI)
   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, ResAxioms.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 _ => ResClause.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 List.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 = filter (fn (_, cls) => not (common_thm used cls)) th_cls_pairs
   697             in
   698                 if null unused then ()
   699                 else warning ("Metis: unused theorems " ^ commas_quote (map #1 unused));
   700                 case result of
   701                     (_,ith)::_ =>
   702                         (trace_msg (fn () => "success: " ^ Display.string_of_thm ctxt ith);
   703                          [ith])
   704                   | _ => (trace_msg (fn () => "Metis: no result");
   705                           [])
   706             end
   707         | Metis.Resolution.Satisfiable _ =>
   708             (trace_msg (fn () => "Metis: No first-order proof with the lemmas supplied");
   709              [])
   710   end;
   711 
   712 fun metis_general_tac mode ctxt ths i st0 =
   713   let val _ = trace_msg (fn () =>
   714         "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
   715   in
   716      if exists_type ResAxioms.type_has_empty_sort (prop_of st0)
   717      then (warning "Proof state contains the empty sort"; Seq.empty)
   718      else
   719        (Meson.MESON ResAxioms.neg_clausify
   720          (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) ctxt i
   721         THEN ResAxioms.expand_defs_tac st0) st0
   722   end
   723   handle METIS s => (warning ("Metis: " ^ s); Seq.empty);
   724 
   725 val metis_tac = metis_general_tac HO;
   726 val metisF_tac = metis_general_tac FO;
   727 val metisFT_tac = metis_general_tac FT;
   728 
   729 fun method name mode comment = Method.setup name (Attrib.thms >> (fn ths => fn ctxt =>
   730   SIMPLE_METHOD' (CHANGED_PROP o metis_general_tac mode ctxt ths))) comment;
   731 
   732 val setup =
   733   type_lits_setup #>
   734   method @{binding metis} HO "METIS for FOL & HOL problems" #>
   735   method @{binding metisF} FO "METIS for FOL problems" #>
   736   method @{binding metisFT} FT "METIS With-fully typed translation" #>
   737   Method.setup @{binding finish_clausify}
   738     (Scan.succeed (K (SIMPLE_METHOD (ResAxioms.expand_defs_tac refl))))
   739     "cleanup after conversion to clauses";
   740 
   741 end;