src/HOL/Tools/metis_tools.ML
author wenzelm
Wed Jun 20 22:07:52 2007 +0200 (2007-06-20)
changeset 23442 028e39e5e8f3
child 23447 1f16190e3836
permissions -rw-r--r--
The Metis prover (slightly modified version from Larry);
     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 
     6 signature METIS_TOOLS =
     7 sig
     8   val type_lits: bool ref
     9   val metis_tac : Thm.thm list -> int -> Tactical.tactic
    10   val setup : theory -> theory
    11 end
    12 
    13 structure MetisTools: METIS_TOOLS =
    14 struct
    15 
    16   structure Rc = ResReconstruct;
    17 
    18   val type_lits = ref true;
    19 
    20   (* ------------------------------------------------------------------------- *)
    21   (* Useful Theorems                                                           *)
    22   (* ------------------------------------------------------------------------- *)
    23   val EXCLUDED_MIDDLE' = read_instantiate [("R","False")] notE;
    24   val EXCLUDED_MIDDLE  = rotate_prems 1 EXCLUDED_MIDDLE';
    25   val REFL_THM         = incr_indexes 2 (Meson.make_meta_clause refl);  (*Rename from 0,1*)
    26   val subst_em  = zero_var_indexes (subst RS EXCLUDED_MIDDLE);
    27   val ssubst_em  = read_instantiate [("t","?s"),("s","?t")] (sym RS subst_em);
    28 
    29   (* ------------------------------------------------------------------------- *)
    30   (* Useful Functions                                                          *)
    31   (* ------------------------------------------------------------------------- *)
    32 
    33   (* match untyped terms*)
    34   fun untyped_aconv (Const(a,_))   (Const(b,_))   = (a=b)
    35     | untyped_aconv (Free(a,_))    (Free(b,_))    = (a=b)
    36     | untyped_aconv (Var((a,_),_)) (Var((b,_),_)) = (a=b)   (*the index is ignored!*)
    37     | untyped_aconv (Bound i)      (Bound j)      = (i=j)
    38     | untyped_aconv (Abs(a,_,t))  (Abs(b,_,u))    = (a=b) andalso untyped_aconv t u
    39     | untyped_aconv (t1$t2) (u1$u2)  = untyped_aconv t1 u1 andalso untyped_aconv t2 u2
    40     | untyped_aconv _              _              = false;
    41 
    42   (* Finding the relative location of an untyped term within a list of terms *)
    43   fun get_index lit =
    44     let val lit = Envir.eta_contract lit
    45         fun get n [] = raise Empty
    46           | get n (x::xs) = if untyped_aconv lit (Envir.eta_contract (HOLogic.dest_Trueprop x))
    47                             then n  else get (n+1) xs
    48     in get 1 end;
    49 
    50   (* ------------------------------------------------------------------------- *)
    51   (* HOL to FOL  (Isabelle to Metis)                                           *)
    52   (* ------------------------------------------------------------------------- *)
    53 
    54   fun fn_isa_to_met "equal" = "="
    55     | fn_isa_to_met x       = x;
    56 
    57   fun metis_lit b c args = (b, (c, args));
    58 
    59   fun hol_type_to_fol (ResClause.AtomV x) = Metis.Term.Var x
    60     | hol_type_to_fol (ResClause.AtomF x) = Metis.Term.Fn(x,[])
    61     | hol_type_to_fol (ResClause.Comp(tc,tps)) = Metis.Term.Fn(tc, map hol_type_to_fol tps);
    62 
    63   (*These two functions insert type literals before the real literals. That is the
    64     opposite order from TPTP linkup, but maybe OK.*)
    65 
    66   fun hol_term_to_fol_FO tm =
    67     case ResHolClause.strip_comb tm of
    68         (ResHolClause.CombConst(c,_,tys), tms) =>
    69           let val tyargs = map hol_type_to_fol tys
    70               val args   = map hol_term_to_fol_FO tms
    71           in Metis.Term.Fn (c, tyargs @ args) end
    72       | (ResHolClause.CombVar(v,_), []) => Metis.Term.Var v
    73       | _ => error "hol_term_to_fol_FO";
    74 
    75   fun hol_term_to_fol_HO (ResHolClause.CombVar(a, ty)) = Metis.Term.Var a
    76     | hol_term_to_fol_HO (ResHolClause.CombConst(a, ty, tylist)) =
    77         Metis.Term.Fn(fn_isa_to_met a, map hol_type_to_fol tylist)
    78     | hol_term_to_fol_HO (ResHolClause.CombApp(tm1,tm2)) =
    79          Metis.Term.Fn(".", map hol_term_to_fol_HO [tm1,tm2]);
    80 
    81   fun hol_literal_to_fol true (ResHolClause.Literal (pol, tm)) =  (*first-order*)
    82         let val (ResHolClause.CombConst(p,_,tys), tms) = ResHolClause.strip_comb tm
    83             val tylits = if p = "equal" then [] else map hol_type_to_fol tys
    84             val lits = map hol_term_to_fol_FO tms
    85         in metis_lit pol (fn_isa_to_met p) (tylits @ lits) end
    86     | hol_literal_to_fol false (ResHolClause.Literal (pol, tm)) =    (*higher-order*)
    87         case ResHolClause.strip_comb tm of
    88             (ResHolClause.CombConst("equal",_,_), tms) =>
    89               metis_lit pol "=" (map hol_term_to_fol_HO tms)
    90           | _ => metis_lit pol "{}" [hol_term_to_fol_HO tm];
    91 
    92   fun literals_of_hol_thm isFO  t =
    93         let val (lits, types_sorts) = ResHolClause.literals_of_term t
    94         in  (map (hol_literal_to_fol isFO) lits, types_sorts) end;
    95 
    96   fun metis_of_typeLit (ResClause.LTVar (s,x))  = metis_lit false s [Metis.Term.Var x]
    97     | metis_of_typeLit (ResClause.LTFree (s,x)) = metis_lit true  s [Metis.Term.Fn(x,[])];
    98 
    99   fun metis_of_tfree tf = Metis.Thm.axiom (Metis.LiteralSet.singleton (metis_of_typeLit tf));
   100 
   101   fun hol_thm_to_fol isFO th =
   102     let val (mlits, types_sorts) =
   103                (literals_of_hol_thm isFO o HOLogic.dest_Trueprop o prop_of) th
   104         val (tvar_lits,tfree_lits) = ResClause.add_typs_aux types_sorts
   105         val tlits = if !type_lits then map metis_of_typeLit tvar_lits else []
   106     in  (Metis.Thm.axiom (Metis.LiteralSet.fromList(tlits@mlits)), tfree_lits)  end;
   107 
   108   (* ARITY CLAUSE *)
   109 
   110   fun m_arity_cls (ResClause.TConsLit (c,t,args)) =
   111         metis_lit true (ResClause.make_type_class c) [Metis.Term.Fn(t, map Metis.Term.Var args)]
   112     | m_arity_cls (ResClause.TVarLit (c,str))     =
   113         metis_lit false (ResClause.make_type_class c) [Metis.Term.Var str];
   114 
   115   (*TrueI is returned as the Isabelle counterpart because there isn't any.*)
   116   fun arity_cls thy (ResClause.ArityClause{kind,conclLit,premLits,...}) =
   117     (TrueI, Metis.Thm.axiom (Metis.LiteralSet.fromList (map m_arity_cls (conclLit :: premLits))));
   118 
   119   (* CLASSREL CLAUSE *)
   120 
   121   fun m_classrel_cls subclass superclass =
   122     [metis_lit false subclass [Metis.Term.Var "T"], metis_lit true superclass [Metis.Term.Var "T"]];
   123 
   124   fun classrel_cls thy (ResClause.ClassrelClause {axiom_name,subclass,superclass,...}) =
   125     (TrueI, Metis.Thm.axiom (Metis.LiteralSet.fromList (m_classrel_cls subclass superclass)));
   126 
   127   (* ------------------------------------------------------------------------- *)
   128   (* FOL to HOL  (Metis to Isabelle)                                           *)
   129   (* ------------------------------------------------------------------------- *)
   130 
   131  datatype term_or_type = Term of Term.term | Type of Term.typ;
   132 
   133   fun terms_of [] = []
   134     | terms_of (Term t :: tts) = t :: terms_of tts
   135     | terms_of (Type _ :: tts) = terms_of tts;
   136 
   137   fun types_of [] = []
   138     | types_of (Term (Term.Var((a,idx), T)) :: tts) =
   139         if String.isPrefix "_" a then
   140             (*Variable generated by Metis, which might have been a type variable.*)
   141             TVar(("'" ^ a, idx), HOLogic.typeS) :: types_of tts
   142         else types_of tts
   143     | types_of (Term _ :: tts) = types_of tts
   144     | types_of (Type T :: tts) = T :: types_of tts;
   145 
   146   fun apply_list rator nargs rands =
   147     let val trands = terms_of rands
   148     in  if length trands = nargs then Term (list_comb(rator, trands))
   149         else error ("apply_list: wrong number of arguments: " ^ Display.raw_string_of_term rator ^
   150                     " expected " ^
   151                     Int.toString nargs ^ " received " ^ commas (map Display.raw_string_of_term trands))
   152     end;
   153 
   154 (*Instantiate constant c with the supplied types, but if they don't match its declared
   155   sort constraints, replace by a general type.*)
   156 fun const_of ctxt (c,Ts) =  Const (c, dummyT)
   157 (*Formerly, this code was used. Now, we just leave it all to type inference!
   158   let val thy = ProofContext.theory_of ctxt
   159       and (types, sorts) = Variable.constraints_of ctxt
   160       val declaredT = Consts.the_constraint (Sign.consts_of thy) c
   161       val t = Rc.fix_sorts sorts (Const(c, Sign.const_instance thy (c,Ts)))
   162   in
   163       Sign.typ_match thy (declaredT, type_of t) Vartab.empty;
   164       t
   165   end
   166   handle Type.TYPE_MATCH => Const (c, dummyT);
   167 *)
   168 
   169   (*We use 1 rather than 0 because variable references in clauses may otherwise conflict
   170     with variable constraints in the goal...at least, type inference often fails otherwise.
   171     SEE ALSO axiom_inf below.*)
   172   fun mk_var w = Term.Var((w,1), HOLogic.typeT);
   173 
   174   (*include the default sort, if available*)
   175   fun mk_tfree ctxt w =
   176     let val ww = "'" ^ w
   177     in  TFree(ww, getOpt (Variable.def_sort ctxt (ww,~1), HOLogic.typeS))  end;
   178 
   179   (*Remove the "apply" operator from an HO term*)
   180   fun strip_happ args (Metis.Term.Fn(".",[t,u])) = strip_happ (u::args) t
   181     | strip_happ args x = (x, args);
   182 
   183   (*Maps metis terms to isabelle terms*)
   184   fun fol_term_to_hol_RAW ctxt fol_tm =
   185     let val thy = ProofContext.theory_of ctxt
   186         val _ = Output.debug (fn () => "fol_term_to_hol: " ^ Metis.Term.toString fol_tm)
   187         fun tm_to_tt (Metis.Term.Var v) =
   188                (case Rc.strip_prefix ResClause.tvar_prefix v of
   189                     SOME w => Type (Rc.make_tvar w)
   190                   | NONE =>
   191                 case Rc.strip_prefix ResClause.schematic_var_prefix v of
   192                     SOME w => Term (mk_var w)
   193                   | NONE   => Term (mk_var v) )
   194                       (*Var from Metis with a name like _nnn; possibly a type variable*)
   195           | tm_to_tt (Metis.Term.Fn ("{}", [arg])) = tm_to_tt arg   (*hBOOL*)
   196           | tm_to_tt (t as Metis.Term.Fn (".",_)) =
   197               let val (rator,rands) = strip_happ [] t
   198               in  case rator of
   199                       Metis.Term.Fn(fname,ts) => applic_to_tt (fname, ts @ rands)
   200                     | _ => case tm_to_tt rator of
   201                                Term t => Term (list_comb(t, terms_of (map tm_to_tt rands)))
   202                              | _ => error "tm_to_tt: HO application"
   203               end
   204           | tm_to_tt (Metis.Term.Fn (fname, args)) = applic_to_tt (fname,args)
   205         and applic_to_tt ("=",ts) =
   206               Term (list_comb(Const ("op =", HOLogic.typeT), terms_of (map tm_to_tt ts)))
   207           | applic_to_tt (a,ts) =
   208               case Rc.strip_prefix ResClause.const_prefix a of
   209                   SOME b =>
   210                     let val c = Rc.invert_const b
   211                         val ntypes = Rc.num_typargs thy c
   212                         val nterms = length ts - ntypes
   213                         val tts = map tm_to_tt ts
   214                         val tys = types_of (List.take(tts,ntypes))
   215                         val ntyargs = Rc.num_typargs thy c
   216                     in if length tys = ntyargs then
   217                            apply_list (const_of ctxt (c, tys)) nterms (List.drop(tts,ntypes))
   218                        else error ("Constant " ^ c ^ " expects " ^ Int.toString ntyargs ^
   219                                    " but gets " ^ Int.toString (length tys) ^
   220                                    " type arguments\n" ^
   221                                    space_implode "\n" (map (ProofContext.string_of_typ ctxt) tys) ^
   222                                    " the terms are \n" ^
   223                                    space_implode "\n" (map (ProofContext.string_of_term ctxt) (terms_of tts)))
   224                        end
   225                 | NONE => (*Not a constant. Is it a type constructor?*)
   226               case Rc.strip_prefix ResClause.tconst_prefix a of
   227                   SOME b => Type (Term.Type(Rc.invert_type_const b, types_of (map tm_to_tt ts)))
   228                 | NONE => (*Maybe a TFree. Should then check that ts=[].*)
   229               case Rc.strip_prefix ResClause.tfree_prefix a of
   230                   SOME b => Type (mk_tfree ctxt b)
   231                 | NONE => (*a fixed variable? They are Skolem functions.*)
   232               case Rc.strip_prefix ResClause.fixed_var_prefix a of
   233                   SOME b =>
   234                     let val opr = Term.Free(b, HOLogic.typeT)
   235                     in  apply_list opr (length ts) (map tm_to_tt ts)  end
   236                 | NONE => error ("unexpected metis function: " ^ a)
   237     in  case tm_to_tt fol_tm of Term t => t | _ => error "fol_tm_to_tt: Term expected"  end;
   238 
   239   fun fol_terms_to_hol ctxt fol_tms =
   240     let val ts = map (fol_term_to_hol_RAW ctxt) fol_tms
   241         val _ = Output.debug (fn () => "  calling infer_types:")
   242         val _ = app (fn t => Output.debug (fn () => ProofContext.string_of_term ctxt t)) ts
   243         val ts' = ProofContext.infer_types_pats ctxt ts
   244                     (*DO NOT freeze TVars in the result*)
   245         val _ = app (fn t => Output.debug
   246                       (fn () => "  final term: " ^ ProofContext.string_of_term ctxt t ^
   247                                 "  of type  " ^ ProofContext.string_of_typ ctxt (type_of t)))
   248                     ts'
   249     in  ts'  end;
   250 
   251   fun mk_not (Const ("Not", _) $ b) = b
   252     | mk_not b = HOLogic.mk_not b;
   253 
   254   (* ------------------------------------------------------------------------- *)
   255   (* FOL step Inference Rules                                                  *)
   256   (* ------------------------------------------------------------------------- *)
   257 
   258   (*for debugging only*)
   259   fun print_thpair (fth,th) =
   260     (Output.debug (fn () => "=============================================");
   261      Output.debug (fn () => "Metis: " ^ Metis.Thm.toString fth);
   262      Output.debug (fn () => "Isabelle: " ^ string_of_thm th));
   263 
   264   fun lookth thpairs (fth : Metis.Thm.thm) =
   265     valOf (AList.lookup (uncurry Metis.Thm.equal) thpairs fth)
   266     handle Option => error ("Failed to find a Metis theorem " ^ Metis.Thm.toString fth);
   267 
   268   fun is_TrueI th = Thm.eq_thm(TrueI,th);
   269 
   270 fun inst_excluded_middle th thy i_atm =
   271     let val vx = hd (term_vars (prop_of th))
   272         val substs = [(cterm_of thy vx, cterm_of thy i_atm)]
   273     in  cterm_instantiate substs th  end;
   274 
   275   (* INFERENCE RULE: AXIOM *)
   276   fun axiom_inf ctxt thpairs th = incr_indexes 1 (lookth thpairs th);
   277       (*This causes variables to have an index of 1 by default. SEE ALSO mk_var above.*)
   278 
   279   (* INFERENCE RULE: ASSUME *)
   280   fun assume_inf ctxt atm =
   281     inst_excluded_middle EXCLUDED_MIDDLE
   282       (ProofContext.theory_of ctxt)
   283       (singleton (fol_terms_to_hol ctxt) (Metis.Term.Fn atm));
   284 
   285   (* INFERENCE RULE: INSTANTIATE. Type instantiations are ignored. Attempting to reconstruct
   286      them admits new possibilities of errors, e.g. concerning sorts. Instead we try to arrange
   287      that new TVars are distinct and that types can be inferred from terms.*)
   288   fun inst_inf ctxt thpairs fsubst th =
   289     let val thy = ProofContext.theory_of ctxt
   290         val i_th   = lookth thpairs th
   291         val i_th_vars = term_vars (prop_of i_th)
   292         fun find_var x = valOf (List.find (fn Term.Var((a,_),_) => a=x) i_th_vars)
   293         fun subst_translation (x,y) =
   294               let val v = find_var x
   295                   val t = fol_term_to_hol_RAW ctxt y
   296               in  SOME (cterm_of thy v, t)  end
   297               handle Option => NONE (*List.find failed for the variable.*)
   298         fun remove_typeinst (a, t) =
   299               case Rc.strip_prefix ResClause.schematic_var_prefix a of
   300                   SOME b => SOME (b, t)
   301                 | NONE   => case Rc.strip_prefix ResClause.tvar_prefix a of
   302                   SOME _ => NONE          (*type instantiations are forbidden!*)
   303                 | NONE   => SOME (a,t)    (*internal Metis var?*)
   304         val _ = Output.debug (fn () => "  isa th: " ^ string_of_thm i_th)
   305         val substs = List.mapPartial remove_typeinst (Metis.Subst.toList fsubst)
   306         val (vars,rawtms) = ListPair.unzip (List.mapPartial subst_translation substs)
   307         val tms = ProofContext.infer_types_pats ctxt rawtms
   308         val ctm_of = cterm_of thy o (map_types o Logic.incr_tvar) (1 + Thm.maxidx_of i_th)
   309         val substs' = ListPair.zip (vars, map ctm_of tms)
   310         val _ = Output.debug (fn() => "subst_translations:")
   311         val _ = app (fn (x,y) => Output.debug (fn () => string_of_cterm x ^ " |-> " ^
   312                                                         string_of_cterm y))
   313                   substs'
   314     in  cterm_instantiate substs' i_th  end;
   315 
   316   (* INFERENCE RULE: RESOLVE *)
   317 
   318   fun resolve_inf ctxt thpairs atm th1 th2 =
   319     let
   320       val thy = ProofContext.theory_of ctxt
   321       val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
   322       val _ = Output.debug (fn () => "  isa th1 (pos): " ^ string_of_thm i_th1)
   323       val _ = Output.debug (fn () => "  isa th2 (neg): " ^ string_of_thm i_th2)
   324     in
   325       if is_TrueI i_th1 then i_th2 (*Trivial cases where one operand is type info*)
   326       else if is_TrueI i_th2 then i_th1
   327       else
   328         let
   329           val i_atm = singleton (fol_terms_to_hol ctxt) (Metis.Term.Fn atm)
   330           val _ = Output.debug (fn () => "  atom: " ^ ProofContext.string_of_term ctxt i_atm)
   331           val prems_th1 = prems_of i_th1
   332           val prems_th2 = prems_of i_th2
   333           val index_th1 = get_index (mk_not i_atm) prems_th1
   334                 handle Empty => error "Failed to find literal in th1"
   335           val _ = Output.debug (fn () => "  index_th1: " ^ Int.toString index_th1)
   336           val index_th2 = get_index i_atm prems_th2
   337                 handle Empty => error "Failed to find literal in th2"
   338           val _ = Output.debug (fn () => "  index_th2: " ^ Int.toString index_th2)
   339       in  (select_literal index_th1 i_th1) RSN (index_th2, i_th2)  end
   340     end;
   341 
   342   (* INFERENCE RULE: REFL *)
   343   fun refl_inf ctxt lit =
   344     let val thy = ProofContext.theory_of ctxt
   345         val v_x = hd (term_vars (prop_of REFL_THM))
   346         val i_lit = singleton (fol_terms_to_hol ctxt) lit
   347     in  cterm_instantiate [(cterm_of thy v_x, cterm_of thy i_lit)] REFL_THM  end;
   348 
   349   fun get_ty_arg_size thy (Const("op =",_)) = 0  (*equality has no type arguments*)
   350     | get_ty_arg_size thy (Const(c,_))      = (Rc.num_typargs thy c handle TYPE _ => 0)
   351     | get_ty_arg_size thy _      = 0;
   352 
   353   (* INFERENCE RULE: EQUALITY *)
   354   fun equality_inf ctxt isFO thpairs (pos,atm) fp fr =
   355     let val thy = ProofContext.theory_of ctxt
   356         val [i_atm,i_tm] = fol_terms_to_hol ctxt [Metis.Term.Fn atm, fr]
   357         val _ = Output.debug (fn () => "sign of the literal: " ^ Bool.toString pos)
   358         fun replace_item_list lx 0 (l::ls) = lx::ls
   359           | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
   360         fun path_finder_FO tm (p::ps) =
   361               let val (tm1,args) = Term.strip_comb tm
   362                   val adjustment = get_ty_arg_size thy tm1
   363                   val p' = if adjustment > p then p else p-adjustment
   364                   val tm_p = List.nth(args,p')
   365                     handle Subscript => error ("equality_inf: " ^ Int.toString p ^ " adj " ^ Int.toString adjustment  ^ " term " ^  ProofContext.string_of_term ctxt tm)
   366               in
   367                   Output.debug (fn () => "path_finder: " ^ Int.toString p ^
   368                                         "  " ^ ProofContext.string_of_term ctxt tm_p);
   369                   if null ps   (*FIXME: why not use pattern-matching and avoid repetition*)
   370                   then (tm_p, list_comb (tm1, replace_item_list (Term.Bound 0) p' args))
   371                   else let val (r,t) = path_finder_FO tm_p ps
   372                        in (r, list_comb (tm1, replace_item_list t p' args)) end
   373               end
   374         fun path_finder_HO tm [] = (tm, Term.Bound 0)
   375           | path_finder_HO (t$u) (0::ps) = (fn(x,y) => (x, y$u)) (path_finder_HO t ps)
   376           | path_finder_HO (t$u) (p::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps)
   377         fun path_finder true tm ps = path_finder_FO tm ps
   378           | path_finder false (tm as Const("op =",_) $ _ $ _) (p::ps) =
   379                (*equality: not curried, as other predicates are*)
   380                if p=0 then path_finder_HO tm (0::1::ps)  (*select first operand*)
   381                else path_finder_HO tm (p::ps)        (*1 selects second operand*)
   382           | path_finder false tm (p::ps) =
   383                path_finder_HO tm ps      (*if not equality, ignore head to skip hBOOL*)
   384         fun path_finder_lit ((nt as Term.Const ("Not", _)) $ tm_a) idx =
   385               let val (tm, tm_rslt) = path_finder isFO tm_a idx
   386               in (tm, nt $ tm_rslt) end
   387           | path_finder_lit tm_a idx = path_finder isFO tm_a idx
   388         val (tm_subst, body) = path_finder_lit i_atm fp
   389         val tm_abs = Term.Abs("x", Term.type_of tm_subst, body)
   390         val _ = Output.debug (fn () => "abstraction: " ^ ProofContext.string_of_term ctxt tm_abs)
   391         val _ = Output.debug (fn () => "i_tm: " ^ ProofContext.string_of_term ctxt i_tm)
   392         val _ = Output.debug (fn () => "located term: " ^ ProofContext.string_of_term ctxt tm_subst)
   393         val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst)  (*ill typed but gives right max*)
   394         val subst' = incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
   395         val _ = Output.debug (fn () => "subst' " ^ string_of_thm subst')
   396         val eq_terms = map (pairself (cterm_of thy))
   397                            (ListPair.zip (term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
   398     in  cterm_instantiate eq_terms subst'  end;
   399 
   400   fun step ctxt isFO thpairs (fol_th, Metis.Proof.Axiom _)                        =
   401         axiom_inf ctxt thpairs fol_th
   402     | step ctxt isFO thpairs (_, Metis.Proof.Assume f_atm)                        =
   403         assume_inf ctxt f_atm
   404     | step ctxt isFO thpairs (_, Metis.Proof.Subst(f_subst, f_th1))                =
   405         inst_inf ctxt thpairs f_subst f_th1
   406     | step ctxt isFO thpairs (_, Metis.Proof.Resolve(f_atm, f_th1, f_th2))        =
   407         resolve_inf ctxt thpairs f_atm f_th1 f_th2
   408     | step ctxt isFO thpairs (_, Metis.Proof.Refl f_tm)                           =
   409         refl_inf ctxt f_tm
   410     | step ctxt isFO thpairs (_, Metis.Proof.Equality(f_lit, f_p, f_r)) =
   411         equality_inf ctxt isFO thpairs f_lit f_p f_r;
   412 
   413   val factor = Seq.hd o distinct_subgoals_tac;
   414 
   415   fun real_literal (b, (c, _)) = not (String.isPrefix ResClause.class_prefix c);
   416 
   417   fun translate isFO _    thpairs [] = thpairs
   418     | translate isFO ctxt thpairs ((fol_th, inf) :: infpairs) =
   419         let val _ = Output.debug (fn () => "=============================================")
   420             val _ = Output.debug (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th)
   421             val _ = Output.debug (fn () => "INFERENCE: " ^ Metis.Proof.inferenceToString inf)
   422             val th = Meson.flexflex_first_order (factor (step ctxt isFO thpairs (fol_th, inf)))
   423             val _ = Output.debug (fn () => "ISABELLE THM: " ^ string_of_thm th)
   424             val _ = Output.debug (fn () => "=============================================")
   425         in
   426             if nprems_of th =
   427         length (filter real_literal (Metis.LiteralSet.toList (Metis.Thm.clause fol_th))) then ()
   428             else error "Metis: proof reconstruction has gone wrong";
   429             translate isFO ctxt ((fol_th, th) :: thpairs) infpairs
   430         end;
   431 
   432   (* ------------------------------------------------------------------------- *)
   433   (* Translation of HO Clauses                                                 *)
   434   (* ------------------------------------------------------------------------- *)
   435 
   436   fun cnf_th th = hd (ResAxioms.cnf_axiom th);
   437 
   438   val equal_imp_fequal' = cnf_th (thm"equal_imp_fequal");
   439   val fequal_imp_equal' = cnf_th (thm"fequal_imp_equal");
   440 
   441   val comb_I  = ResHolClause.comb_I  RS meta_eq_to_obj_eq;
   442   val comb_K  = ResHolClause.comb_K  RS meta_eq_to_obj_eq;
   443   val comb_B  = ResHolClause.comb_B  RS meta_eq_to_obj_eq;
   444 
   445   val ext_thm = cnf_th ResHolClause.ext;
   446 
   447   fun dest_Arity (ResClause.ArityClause{premLits,...}) =
   448         map ResClause.class_of_arityLit premLits;
   449 
   450   fun type_ext thy tms =
   451     let val subs = ResAtp.tfree_classes_of_terms tms
   452         val supers = ResAtp.tvar_classes_of_terms tms
   453         and tycons = ResAtp.type_consts_of_terms thy tms
   454         val arity_clauses = ResClause.make_arity_clauses thy tycons supers
   455         val (supers',arity_clauses) = ResClause.make_arity_clauses thy tycons supers
   456         val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
   457     in  map (classrel_cls thy) classrel_clauses @ map (arity_cls thy) arity_clauses
   458     end;
   459 
   460   (* ------------------------------------------------------------------------- *)
   461   (* Logic maps manage the interface between HOL and first-order logic.        *)
   462   (* ------------------------------------------------------------------------- *)
   463 
   464   type logic_map =
   465     {isFO   : bool,
   466      axioms : (Metis.Thm.thm * Thm.thm) list,
   467      tfrees : ResClause.type_literal list};
   468 
   469   fun const_in_metis c (pol,(pred,tm_list)) =
   470     let
   471       fun in_mterm (Metis.Term.Var nm) = false
   472         | in_mterm (Metis.Term.Fn (".", tm_list)) = exists in_mterm tm_list
   473         | in_mterm (Metis.Term.Fn (nm, tm_list)) = c=nm orelse exists in_mterm tm_list
   474     in  c=pred orelse exists in_mterm tm_list  end;
   475 
   476   (*transform isabelle clause to metis clause *)
   477   fun add_thm thy (ith, {isFO, axioms, tfrees}) : logic_map =
   478     let val (mth, tfree_lits) = hol_thm_to_fol isFO ith
   479         fun add_tfree (tf, axs) =
   480               if member (op=) tfrees tf then axs
   481               else (metis_of_tfree tf, TrueI) :: axs
   482         val new_axioms = foldl add_tfree [] tfree_lits
   483     in
   484        {isFO = isFO,
   485         axioms = (mth, Meson.make_meta_clause ith) :: (new_axioms @ axioms),
   486         tfrees = tfree_lits union tfrees}
   487     end;
   488 
   489   (*transform isabelle type / arity clause to metis clause *)
   490   fun add_type_thm [] lmap = lmap
   491     | add_type_thm ((ith, mth) :: cls) {isFO, axioms, tfrees} =
   492         add_type_thm cls {isFO = isFO,
   493                           axioms = (mth, ith) :: axioms,
   494                           tfrees = tfrees}
   495 
   496   (* Function to generate metis clauses, including comb and type clauses *)
   497   fun build_map mode thy cls ths =
   498     let val isFO = (mode = ResAtp.Fol) orelse
   499                     (mode <> ResAtp.Hol andalso ResAtp.is_fol_thms (cls @ ths))
   500         val lmap = foldl (add_thm thy) {isFO = isFO, axioms = [], tfrees = []} (cls @ ths)
   501         val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap)
   502         fun used c = exists (Metis.LiteralSet.exists (const_in_metis c)) clause_lists
   503         (*Now check for the existence of certain combinators*)
   504         val IK    = if used "c_COMBI" orelse used "c_COMBK" then [comb_I,comb_K] else []
   505         val BC    = if used "c_COMBB" then [comb_B] else []
   506         val EQ    = if used "c_fequal" then [fequal_imp_equal', equal_imp_fequal'] else []
   507         val lmap' = if isFO then lmap else foldl (add_thm thy) lmap ([ext_thm] @ EQ @ IK @ BC)
   508     in
   509         add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap'
   510     end;
   511 
   512   fun refute cls =
   513       Metis.Resolution.loop (Metis.Resolution.new Metis.Resolution.default cls);
   514 
   515   fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const);
   516 
   517   (* Main function to start metis prove and reconstruction *)
   518   fun FOL_SOLVE mode ctxt cls ths =
   519     let val thy = ProofContext.theory_of ctxt
   520         val _ = if exists(is_false o prop_of) cls then error "problem contains the empty clause"
   521                 else ();
   522         val _ = ResClause.init thy
   523         val _ = ResHolClause.init thy
   524         val _ = Output.debug (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
   525         val _ = app (fn th => Output.debug (fn () => string_of_thm th)) cls
   526         val _ = Output.debug (fn () => "THEOREM CLAUSES")
   527         val _ = app (fn th => Output.debug (fn () => string_of_thm th)) ths
   528         val {isFO,axioms,tfrees} = build_map mode thy cls ths
   529         val _ = if null tfrees then ()
   530                 else (Output.debug (fn () => "TFREE CLAUSES");
   531                       app (fn tf => Output.debug (fn _ => ResClause.tptp_of_typeLit tf)) tfrees)
   532         val _ = Output.debug (fn () => "CLAUSES GIVEN TO METIS")
   533         val thms = map #1 axioms
   534         val _ = app (fn th => Output.debug (fn () => Metis.Thm.toString th)) thms
   535         val _ = if isFO
   536                 then Output.debug (fn () => "goal is first-order")
   537                 else Output.debug (fn () => "goal is higher-order")
   538         val _ = Output.debug (fn () => "START METIS PROVE PROCESS")
   539     in
   540         case refute thms of
   541             Metis.Resolution.Contradiction mth =>
   542               let val _ = Output.debug (fn () => "METIS RECONSTRUCTION START: " ^
   543                             Metis.Thm.toString mth)
   544                   val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
   545                                (*add constraints arising from converting goal to clause form*)
   546                   val result = translate isFO ctxt' axioms (Metis.Proof.proof mth)
   547                   val _ = Output.debug (fn () => "METIS COMPLETED")
   548               in
   549                   case result of
   550                       (_,ith)::_ => (Output.debug (fn () => "success: " ^ string_of_thm ith); ith)
   551                     | _ => error "METIS: no result"
   552               end
   553           | Metis.Resolution.Satisfiable _ => error "Metis finds the theorem to be invalid"
   554     end;
   555 
   556   fun metis_general_tac mode ctxt ths i st0 =
   557     let val _ = Output.debug (fn () => "Metis called with theorems " ^ cat_lines (map string_of_thm ths))
   558         val ths' = ResAxioms.cnf_rules_of_ths ths
   559     in
   560        (MESON ResAxioms.neg_clausify (fn cls => rtac (FOL_SOLVE mode ctxt cls ths') 1) i
   561         THEN ResAxioms.expand_defs_tac st0) st0
   562     end;
   563 
   564   fun metis_tac ths gno st =
   565     metis_general_tac ResAtp.Auto (ProofContext.init (theory_of_thm st)) ths gno st;
   566 
   567   fun metisF_tac ths gno st =
   568     metis_general_tac ResAtp.Fol (ProofContext.init (theory_of_thm st)) ths gno st;
   569 
   570   fun metisH_tac ths gno st =
   571     metis_general_tac ResAtp.Hol (ProofContext.init (theory_of_thm st)) ths gno st;
   572 
   573   fun metis_meth mode ths ctxt =
   574     Method.SIMPLE_METHOD'
   575       (setmp ResHolClause.typ_level ResHolClause.T_CONST  (*constant-typed*)
   576         (setmp ResHolClause.minimize_applies false        (*avoid this optimization*)
   577           (CHANGED_PROP o metis_general_tac mode ctxt ths)));
   578 
   579   fun metis  ths ctxt = metis_meth ResAtp.Auto ths ctxt;
   580   fun metisF ths ctxt = metis_meth ResAtp.Fol  ths ctxt;
   581   fun metisH ths ctxt = metis_meth ResAtp.Hol  ths ctxt;
   582 
   583   val setup =
   584     Method.add_methods
   585       [("metis",  Method.thms_ctxt_args metis,  "METIS for FOL & HOL problems"),
   586        ("metisF", Method.thms_ctxt_args metisF, "METIS for FOL problems"),
   587        ("metisH", Method.thms_ctxt_args metisH, "METIS for HOL problems"),
   588        ("finish_clausify",
   589          Method.no_args (Method.SIMPLE_METHOD' (K (ResAxioms.expand_defs_tac refl))),
   590     "cleanup after conversion to clauses")];
   591 
   592 end;