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