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