diff -r ee218296d635 -r 028e39e5e8f3 src/HOL/Tools/metis_tools.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/metis_tools.ML Wed Jun 20 22:07:52 2007 +0200 @@ -0,0 +1,592 @@ +(* Title: HOL/Tools/metis_tools.ML + Author: Kong W. Susanto and Lawrence C. Paulson, CU Computer Laboratory + Copyright Cambridge University 2007 +*) + +signature METIS_TOOLS = +sig + val type_lits: bool ref + val metis_tac : Thm.thm list -> int -> Tactical.tactic + val setup : theory -> theory +end + +structure MetisTools: METIS_TOOLS = +struct + + structure Rc = ResReconstruct; + + val type_lits = ref true; + + (* ------------------------------------------------------------------------- *) + (* Useful Theorems *) + (* ------------------------------------------------------------------------- *) + val EXCLUDED_MIDDLE' = read_instantiate [("R","False")] notE; + val EXCLUDED_MIDDLE = rotate_prems 1 EXCLUDED_MIDDLE'; + val REFL_THM = incr_indexes 2 (Meson.make_meta_clause refl); (*Rename from 0,1*) + val subst_em = zero_var_indexes (subst RS EXCLUDED_MIDDLE); + val ssubst_em = read_instantiate [("t","?s"),("s","?t")] (sym RS subst_em); + + (* ------------------------------------------------------------------------- *) + (* Useful Functions *) + (* ------------------------------------------------------------------------- *) + + (* match untyped terms*) + fun untyped_aconv (Const(a,_)) (Const(b,_)) = (a=b) + | untyped_aconv (Free(a,_)) (Free(b,_)) = (a=b) + | untyped_aconv (Var((a,_),_)) (Var((b,_),_)) = (a=b) (*the index is ignored!*) + | untyped_aconv (Bound i) (Bound j) = (i=j) + | untyped_aconv (Abs(a,_,t)) (Abs(b,_,u)) = (a=b) andalso untyped_aconv t u + | untyped_aconv (t1$t2) (u1$u2) = untyped_aconv t1 u1 andalso untyped_aconv t2 u2 + | untyped_aconv _ _ = false; + + (* Finding the relative location of an untyped term within a list of terms *) + fun get_index lit = + let val lit = Envir.eta_contract lit + fun get n [] = raise Empty + | get n (x::xs) = if untyped_aconv lit (Envir.eta_contract (HOLogic.dest_Trueprop x)) + then n else get (n+1) xs + in get 1 end; + + (* ------------------------------------------------------------------------- *) + (* HOL to FOL (Isabelle to Metis) *) + (* ------------------------------------------------------------------------- *) + + fun fn_isa_to_met "equal" = "=" + | fn_isa_to_met x = x; + + fun metis_lit b c args = (b, (c, args)); + + fun hol_type_to_fol (ResClause.AtomV x) = Metis.Term.Var x + | hol_type_to_fol (ResClause.AtomF x) = Metis.Term.Fn(x,[]) + | hol_type_to_fol (ResClause.Comp(tc,tps)) = Metis.Term.Fn(tc, map hol_type_to_fol tps); + + (*These two functions insert type literals before the real literals. That is the + opposite order from TPTP linkup, but maybe OK.*) + + fun hol_term_to_fol_FO tm = + case ResHolClause.strip_comb tm of + (ResHolClause.CombConst(c,_,tys), tms) => + let val tyargs = map hol_type_to_fol tys + val args = map hol_term_to_fol_FO tms + in Metis.Term.Fn (c, tyargs @ args) end + | (ResHolClause.CombVar(v,_), []) => Metis.Term.Var v + | _ => error "hol_term_to_fol_FO"; + + fun hol_term_to_fol_HO (ResHolClause.CombVar(a, ty)) = Metis.Term.Var a + | hol_term_to_fol_HO (ResHolClause.CombConst(a, ty, tylist)) = + Metis.Term.Fn(fn_isa_to_met a, map hol_type_to_fol tylist) + | hol_term_to_fol_HO (ResHolClause.CombApp(tm1,tm2)) = + Metis.Term.Fn(".", map hol_term_to_fol_HO [tm1,tm2]); + + fun hol_literal_to_fol true (ResHolClause.Literal (pol, tm)) = (*first-order*) + let val (ResHolClause.CombConst(p,_,tys), tms) = ResHolClause.strip_comb tm + val tylits = if p = "equal" then [] else map hol_type_to_fol tys + val lits = map hol_term_to_fol_FO tms + in metis_lit pol (fn_isa_to_met p) (tylits @ lits) end + | hol_literal_to_fol false (ResHolClause.Literal (pol, tm)) = (*higher-order*) + case ResHolClause.strip_comb tm of + (ResHolClause.CombConst("equal",_,_), tms) => + metis_lit pol "=" (map hol_term_to_fol_HO tms) + | _ => metis_lit pol "{}" [hol_term_to_fol_HO tm]; + + fun literals_of_hol_thm isFO t = + let val (lits, types_sorts) = ResHolClause.literals_of_term t + in (map (hol_literal_to_fol isFO) lits, types_sorts) end; + + fun metis_of_typeLit (ResClause.LTVar (s,x)) = metis_lit false s [Metis.Term.Var x] + | metis_of_typeLit (ResClause.LTFree (s,x)) = metis_lit true s [Metis.Term.Fn(x,[])]; + + fun metis_of_tfree tf = Metis.Thm.axiom (Metis.LiteralSet.singleton (metis_of_typeLit tf)); + + fun hol_thm_to_fol isFO th = + let val (mlits, types_sorts) = + (literals_of_hol_thm isFO o HOLogic.dest_Trueprop o prop_of) th + val (tvar_lits,tfree_lits) = ResClause.add_typs_aux types_sorts + val tlits = if !type_lits then map metis_of_typeLit tvar_lits else [] + in (Metis.Thm.axiom (Metis.LiteralSet.fromList(tlits@mlits)), tfree_lits) end; + + (* ARITY CLAUSE *) + + fun m_arity_cls (ResClause.TConsLit (c,t,args)) = + metis_lit true (ResClause.make_type_class c) [Metis.Term.Fn(t, map Metis.Term.Var args)] + | m_arity_cls (ResClause.TVarLit (c,str)) = + metis_lit false (ResClause.make_type_class c) [Metis.Term.Var str]; + + (*TrueI is returned as the Isabelle counterpart because there isn't any.*) + fun arity_cls thy (ResClause.ArityClause{kind,conclLit,premLits,...}) = + (TrueI, Metis.Thm.axiom (Metis.LiteralSet.fromList (map m_arity_cls (conclLit :: premLits)))); + + (* CLASSREL CLAUSE *) + + fun m_classrel_cls subclass superclass = + [metis_lit false subclass [Metis.Term.Var "T"], metis_lit true superclass [Metis.Term.Var "T"]]; + + fun classrel_cls thy (ResClause.ClassrelClause {axiom_name,subclass,superclass,...}) = + (TrueI, Metis.Thm.axiom (Metis.LiteralSet.fromList (m_classrel_cls subclass superclass))); + + (* ------------------------------------------------------------------------- *) + (* FOL to HOL (Metis to Isabelle) *) + (* ------------------------------------------------------------------------- *) + + datatype term_or_type = Term of Term.term | Type of Term.typ; + + fun terms_of [] = [] + | terms_of (Term t :: tts) = t :: terms_of tts + | terms_of (Type _ :: tts) = terms_of tts; + + fun types_of [] = [] + | types_of (Term (Term.Var((a,idx), T)) :: tts) = + if String.isPrefix "_" a then + (*Variable generated by Metis, which might have been a type variable.*) + TVar(("'" ^ a, idx), HOLogic.typeS) :: types_of tts + else types_of tts + | types_of (Term _ :: tts) = types_of tts + | types_of (Type T :: tts) = T :: types_of tts; + + fun apply_list rator nargs rands = + let val trands = terms_of rands + in if length trands = nargs then Term (list_comb(rator, trands)) + else error ("apply_list: wrong number of arguments: " ^ Display.raw_string_of_term rator ^ + " expected " ^ + Int.toString nargs ^ " received " ^ commas (map Display.raw_string_of_term trands)) + end; + +(*Instantiate constant c with the supplied types, but if they don't match its declared + sort constraints, replace by a general type.*) +fun const_of ctxt (c,Ts) = Const (c, dummyT) +(*Formerly, this code was used. Now, we just leave it all to type inference! + let val thy = ProofContext.theory_of ctxt + and (types, sorts) = Variable.constraints_of ctxt + val declaredT = Consts.the_constraint (Sign.consts_of thy) c + val t = Rc.fix_sorts sorts (Const(c, Sign.const_instance thy (c,Ts))) + in + Sign.typ_match thy (declaredT, type_of t) Vartab.empty; + t + end + handle Type.TYPE_MATCH => Const (c, dummyT); +*) + + (*We use 1 rather than 0 because variable references in clauses may otherwise conflict + with variable constraints in the goal...at least, type inference often fails otherwise. + SEE ALSO axiom_inf below.*) + fun mk_var w = Term.Var((w,1), HOLogic.typeT); + + (*include the default sort, if available*) + fun mk_tfree ctxt w = + let val ww = "'" ^ w + in TFree(ww, getOpt (Variable.def_sort ctxt (ww,~1), HOLogic.typeS)) end; + + (*Remove the "apply" operator from an HO term*) + fun strip_happ args (Metis.Term.Fn(".",[t,u])) = strip_happ (u::args) t + | strip_happ args x = (x, args); + + (*Maps metis terms to isabelle terms*) + fun fol_term_to_hol_RAW ctxt fol_tm = + let val thy = ProofContext.theory_of ctxt + val _ = Output.debug (fn () => "fol_term_to_hol: " ^ Metis.Term.toString fol_tm) + fun tm_to_tt (Metis.Term.Var v) = + (case Rc.strip_prefix ResClause.tvar_prefix v of + SOME w => Type (Rc.make_tvar w) + | NONE => + case Rc.strip_prefix ResClause.schematic_var_prefix v of + SOME w => Term (mk_var w) + | NONE => Term (mk_var v) ) + (*Var from Metis with a name like _nnn; possibly a type variable*) + | tm_to_tt (Metis.Term.Fn ("{}", [arg])) = tm_to_tt arg (*hBOOL*) + | tm_to_tt (t as Metis.Term.Fn (".",_)) = + let val (rator,rands) = strip_happ [] t + in case rator of + Metis.Term.Fn(fname,ts) => applic_to_tt (fname, ts @ rands) + | _ => case tm_to_tt rator of + Term t => Term (list_comb(t, terms_of (map tm_to_tt rands))) + | _ => error "tm_to_tt: HO application" + end + | tm_to_tt (Metis.Term.Fn (fname, args)) = applic_to_tt (fname,args) + and applic_to_tt ("=",ts) = + Term (list_comb(Const ("op =", HOLogic.typeT), terms_of (map tm_to_tt ts))) + | applic_to_tt (a,ts) = + case Rc.strip_prefix ResClause.const_prefix a of + SOME b => + let val c = Rc.invert_const b + val ntypes = Rc.num_typargs thy c + val nterms = length ts - ntypes + val tts = map tm_to_tt ts + val tys = types_of (List.take(tts,ntypes)) + val ntyargs = Rc.num_typargs thy c + in if length tys = ntyargs then + apply_list (const_of ctxt (c, tys)) nterms (List.drop(tts,ntypes)) + else error ("Constant " ^ c ^ " expects " ^ Int.toString ntyargs ^ + " but gets " ^ Int.toString (length tys) ^ + " type arguments\n" ^ + space_implode "\n" (map (ProofContext.string_of_typ ctxt) tys) ^ + " the terms are \n" ^ + space_implode "\n" (map (ProofContext.string_of_term ctxt) (terms_of tts))) + end + | NONE => (*Not a constant. Is it a type constructor?*) + case Rc.strip_prefix ResClause.tconst_prefix a of + SOME b => Type (Term.Type(Rc.invert_type_const b, types_of (map tm_to_tt ts))) + | NONE => (*Maybe a TFree. Should then check that ts=[].*) + case Rc.strip_prefix ResClause.tfree_prefix a of + SOME b => Type (mk_tfree ctxt b) + | NONE => (*a fixed variable? They are Skolem functions.*) + case Rc.strip_prefix ResClause.fixed_var_prefix a of + SOME b => + let val opr = Term.Free(b, HOLogic.typeT) + in apply_list opr (length ts) (map tm_to_tt ts) end + | NONE => error ("unexpected metis function: " ^ a) + in case tm_to_tt fol_tm of Term t => t | _ => error "fol_tm_to_tt: Term expected" end; + + fun fol_terms_to_hol ctxt fol_tms = + let val ts = map (fol_term_to_hol_RAW ctxt) fol_tms + val _ = Output.debug (fn () => " calling infer_types:") + val _ = app (fn t => Output.debug (fn () => ProofContext.string_of_term ctxt t)) ts + val ts' = ProofContext.infer_types_pats ctxt ts + (*DO NOT freeze TVars in the result*) + val _ = app (fn t => Output.debug + (fn () => " final term: " ^ ProofContext.string_of_term ctxt t ^ + " of type " ^ ProofContext.string_of_typ ctxt (type_of t))) + ts' + in ts' end; + + fun mk_not (Const ("Not", _) $ b) = b + | mk_not b = HOLogic.mk_not b; + + (* ------------------------------------------------------------------------- *) + (* FOL step Inference Rules *) + (* ------------------------------------------------------------------------- *) + + (*for debugging only*) + fun print_thpair (fth,th) = + (Output.debug (fn () => "============================================="); + Output.debug (fn () => "Metis: " ^ Metis.Thm.toString fth); + Output.debug (fn () => "Isabelle: " ^ string_of_thm th)); + + fun lookth thpairs (fth : Metis.Thm.thm) = + valOf (AList.lookup (uncurry Metis.Thm.equal) thpairs fth) + handle Option => error ("Failed to find a Metis theorem " ^ Metis.Thm.toString fth); + + fun is_TrueI th = Thm.eq_thm(TrueI,th); + +fun inst_excluded_middle th thy i_atm = + let val vx = hd (term_vars (prop_of th)) + val substs = [(cterm_of thy vx, cterm_of thy i_atm)] + in cterm_instantiate substs th end; + + (* INFERENCE RULE: AXIOM *) + fun axiom_inf ctxt thpairs th = incr_indexes 1 (lookth thpairs th); + (*This causes variables to have an index of 1 by default. SEE ALSO mk_var above.*) + + (* INFERENCE RULE: ASSUME *) + fun assume_inf ctxt atm = + inst_excluded_middle EXCLUDED_MIDDLE + (ProofContext.theory_of ctxt) + (singleton (fol_terms_to_hol ctxt) (Metis.Term.Fn atm)); + + (* INFERENCE RULE: INSTANTIATE. Type instantiations are ignored. Attempting to reconstruct + them admits new possibilities of errors, e.g. concerning sorts. Instead we try to arrange + that new TVars are distinct and that types can be inferred from terms.*) + fun inst_inf ctxt thpairs fsubst th = + let val thy = ProofContext.theory_of ctxt + val i_th = lookth thpairs th + val i_th_vars = term_vars (prop_of i_th) + fun find_var x = valOf (List.find (fn Term.Var((a,_),_) => a=x) i_th_vars) + fun subst_translation (x,y) = + let val v = find_var x + val t = fol_term_to_hol_RAW ctxt y + in SOME (cterm_of thy v, t) end + handle Option => NONE (*List.find failed for the variable.*) + fun remove_typeinst (a, t) = + case Rc.strip_prefix ResClause.schematic_var_prefix a of + SOME b => SOME (b, t) + | NONE => case Rc.strip_prefix ResClause.tvar_prefix a of + SOME _ => NONE (*type instantiations are forbidden!*) + | NONE => SOME (a,t) (*internal Metis var?*) + val _ = Output.debug (fn () => " isa th: " ^ string_of_thm i_th) + val substs = List.mapPartial remove_typeinst (Metis.Subst.toList fsubst) + val (vars,rawtms) = ListPair.unzip (List.mapPartial subst_translation substs) + val tms = ProofContext.infer_types_pats ctxt rawtms + val ctm_of = cterm_of thy o (map_types o Logic.incr_tvar) (1 + Thm.maxidx_of i_th) + val substs' = ListPair.zip (vars, map ctm_of tms) + val _ = Output.debug (fn() => "subst_translations:") + val _ = app (fn (x,y) => Output.debug (fn () => string_of_cterm x ^ " |-> " ^ + string_of_cterm y)) + substs' + in cterm_instantiate substs' i_th end; + + (* INFERENCE RULE: RESOLVE *) + + fun resolve_inf ctxt thpairs atm th1 th2 = + let + val thy = ProofContext.theory_of ctxt + val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2 + val _ = Output.debug (fn () => " isa th1 (pos): " ^ string_of_thm i_th1) + val _ = Output.debug (fn () => " isa th2 (neg): " ^ string_of_thm i_th2) + in + if is_TrueI i_th1 then i_th2 (*Trivial cases where one operand is type info*) + else if is_TrueI i_th2 then i_th1 + else + let + val i_atm = singleton (fol_terms_to_hol ctxt) (Metis.Term.Fn atm) + val _ = Output.debug (fn () => " atom: " ^ ProofContext.string_of_term ctxt i_atm) + val prems_th1 = prems_of i_th1 + val prems_th2 = prems_of i_th2 + val index_th1 = get_index (mk_not i_atm) prems_th1 + handle Empty => error "Failed to find literal in th1" + val _ = Output.debug (fn () => " index_th1: " ^ Int.toString index_th1) + val index_th2 = get_index i_atm prems_th2 + handle Empty => error "Failed to find literal in th2" + val _ = Output.debug (fn () => " index_th2: " ^ Int.toString index_th2) + in (select_literal index_th1 i_th1) RSN (index_th2, i_th2) end + end; + + (* INFERENCE RULE: REFL *) + fun refl_inf ctxt lit = + let val thy = ProofContext.theory_of ctxt + val v_x = hd (term_vars (prop_of REFL_THM)) + val i_lit = singleton (fol_terms_to_hol ctxt) lit + in cterm_instantiate [(cterm_of thy v_x, cterm_of thy i_lit)] REFL_THM end; + + fun get_ty_arg_size thy (Const("op =",_)) = 0 (*equality has no type arguments*) + | get_ty_arg_size thy (Const(c,_)) = (Rc.num_typargs thy c handle TYPE _ => 0) + | get_ty_arg_size thy _ = 0; + + (* INFERENCE RULE: EQUALITY *) + fun equality_inf ctxt isFO thpairs (pos,atm) fp fr = + let val thy = ProofContext.theory_of ctxt + val [i_atm,i_tm] = fol_terms_to_hol ctxt [Metis.Term.Fn atm, fr] + val _ = Output.debug (fn () => "sign of the literal: " ^ Bool.toString pos) + fun replace_item_list lx 0 (l::ls) = lx::ls + | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls + fun path_finder_FO tm (p::ps) = + let val (tm1,args) = Term.strip_comb tm + val adjustment = get_ty_arg_size thy tm1 + val p' = if adjustment > p then p else p-adjustment + val tm_p = List.nth(args,p') + handle Subscript => error ("equality_inf: " ^ Int.toString p ^ " adj " ^ Int.toString adjustment ^ " term " ^ ProofContext.string_of_term ctxt tm) + in + Output.debug (fn () => "path_finder: " ^ Int.toString p ^ + " " ^ ProofContext.string_of_term ctxt tm_p); + if null ps (*FIXME: why not use pattern-matching and avoid repetition*) + then (tm_p, list_comb (tm1, replace_item_list (Term.Bound 0) p' args)) + else let val (r,t) = path_finder_FO tm_p ps + in (r, list_comb (tm1, replace_item_list t p' args)) end + end + fun path_finder_HO tm [] = (tm, Term.Bound 0) + | path_finder_HO (t$u) (0::ps) = (fn(x,y) => (x, y$u)) (path_finder_HO t ps) + | path_finder_HO (t$u) (p::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps) + fun path_finder true tm ps = path_finder_FO tm ps + | path_finder false (tm as Const("op =",_) $ _ $ _) (p::ps) = + (*equality: not curried, as other predicates are*) + if p=0 then path_finder_HO tm (0::1::ps) (*select first operand*) + else path_finder_HO tm (p::ps) (*1 selects second operand*) + | path_finder false tm (p::ps) = + path_finder_HO tm ps (*if not equality, ignore head to skip hBOOL*) + fun path_finder_lit ((nt as Term.Const ("Not", _)) $ tm_a) idx = + let val (tm, tm_rslt) = path_finder isFO tm_a idx + in (tm, nt $ tm_rslt) end + | path_finder_lit tm_a idx = path_finder isFO tm_a idx + val (tm_subst, body) = path_finder_lit i_atm fp + val tm_abs = Term.Abs("x", Term.type_of tm_subst, body) + val _ = Output.debug (fn () => "abstraction: " ^ ProofContext.string_of_term ctxt tm_abs) + val _ = Output.debug (fn () => "i_tm: " ^ ProofContext.string_of_term ctxt i_tm) + val _ = Output.debug (fn () => "located term: " ^ ProofContext.string_of_term ctxt tm_subst) + val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst) (*ill typed but gives right max*) + val subst' = incr_indexes (imax+1) (if pos then subst_em else ssubst_em) + val _ = Output.debug (fn () => "subst' " ^ string_of_thm subst') + val eq_terms = map (pairself (cterm_of thy)) + (ListPair.zip (term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm])) + in cterm_instantiate eq_terms subst' end; + + fun step ctxt isFO thpairs (fol_th, Metis.Proof.Axiom _) = + axiom_inf ctxt thpairs fol_th + | step ctxt isFO thpairs (_, Metis.Proof.Assume f_atm) = + assume_inf ctxt f_atm + | step ctxt isFO thpairs (_, Metis.Proof.Subst(f_subst, f_th1)) = + inst_inf ctxt thpairs f_subst f_th1 + | step ctxt isFO thpairs (_, Metis.Proof.Resolve(f_atm, f_th1, f_th2)) = + resolve_inf ctxt thpairs f_atm f_th1 f_th2 + | step ctxt isFO thpairs (_, Metis.Proof.Refl f_tm) = + refl_inf ctxt f_tm + | step ctxt isFO thpairs (_, Metis.Proof.Equality(f_lit, f_p, f_r)) = + equality_inf ctxt isFO thpairs f_lit f_p f_r; + + val factor = Seq.hd o distinct_subgoals_tac; + + fun real_literal (b, (c, _)) = not (String.isPrefix ResClause.class_prefix c); + + fun translate isFO _ thpairs [] = thpairs + | translate isFO ctxt thpairs ((fol_th, inf) :: infpairs) = + let val _ = Output.debug (fn () => "=============================================") + val _ = Output.debug (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th) + val _ = Output.debug (fn () => "INFERENCE: " ^ Metis.Proof.inferenceToString inf) + val th = Meson.flexflex_first_order (factor (step ctxt isFO thpairs (fol_th, inf))) + val _ = Output.debug (fn () => "ISABELLE THM: " ^ string_of_thm th) + val _ = Output.debug (fn () => "=============================================") + in + if nprems_of th = + length (filter real_literal (Metis.LiteralSet.toList (Metis.Thm.clause fol_th))) then () + else error "Metis: proof reconstruction has gone wrong"; + translate isFO ctxt ((fol_th, th) :: thpairs) infpairs + end; + + (* ------------------------------------------------------------------------- *) + (* Translation of HO Clauses *) + (* ------------------------------------------------------------------------- *) + + fun cnf_th th = hd (ResAxioms.cnf_axiom th); + + val equal_imp_fequal' = cnf_th (thm"equal_imp_fequal"); + val fequal_imp_equal' = cnf_th (thm"fequal_imp_equal"); + + val comb_I = ResHolClause.comb_I RS meta_eq_to_obj_eq; + val comb_K = ResHolClause.comb_K RS meta_eq_to_obj_eq; + val comb_B = ResHolClause.comb_B RS meta_eq_to_obj_eq; + + val ext_thm = cnf_th ResHolClause.ext; + + fun dest_Arity (ResClause.ArityClause{premLits,...}) = + map ResClause.class_of_arityLit premLits; + + fun type_ext thy tms = + let val subs = ResAtp.tfree_classes_of_terms tms + val supers = ResAtp.tvar_classes_of_terms tms + and tycons = ResAtp.type_consts_of_terms thy tms + val arity_clauses = ResClause.make_arity_clauses thy tycons supers + val (supers',arity_clauses) = ResClause.make_arity_clauses thy tycons supers + val classrel_clauses = ResClause.make_classrel_clauses thy subs supers' + in map (classrel_cls thy) classrel_clauses @ map (arity_cls thy) arity_clauses + end; + + (* ------------------------------------------------------------------------- *) + (* Logic maps manage the interface between HOL and first-order logic. *) + (* ------------------------------------------------------------------------- *) + + type logic_map = + {isFO : bool, + axioms : (Metis.Thm.thm * Thm.thm) list, + tfrees : ResClause.type_literal list}; + + fun const_in_metis c (pol,(pred,tm_list)) = + let + fun in_mterm (Metis.Term.Var nm) = false + | in_mterm (Metis.Term.Fn (".", tm_list)) = exists in_mterm tm_list + | in_mterm (Metis.Term.Fn (nm, tm_list)) = c=nm orelse exists in_mterm tm_list + in c=pred orelse exists in_mterm tm_list end; + + (*transform isabelle clause to metis clause *) + fun add_thm thy (ith, {isFO, axioms, tfrees}) : logic_map = + let val (mth, tfree_lits) = hol_thm_to_fol isFO ith + fun add_tfree (tf, axs) = + if member (op=) tfrees tf then axs + else (metis_of_tfree tf, TrueI) :: axs + val new_axioms = foldl add_tfree [] tfree_lits + in + {isFO = isFO, + axioms = (mth, Meson.make_meta_clause ith) :: (new_axioms @ axioms), + tfrees = tfree_lits union tfrees} + end; + + (*transform isabelle type / arity clause to metis clause *) + fun add_type_thm [] lmap = lmap + | add_type_thm ((ith, mth) :: cls) {isFO, axioms, tfrees} = + add_type_thm cls {isFO = isFO, + axioms = (mth, ith) :: axioms, + tfrees = tfrees} + + (* Function to generate metis clauses, including comb and type clauses *) + fun build_map mode thy cls ths = + let val isFO = (mode = ResAtp.Fol) orelse + (mode <> ResAtp.Hol andalso ResAtp.is_fol_thms (cls @ ths)) + val lmap = foldl (add_thm thy) {isFO = isFO, axioms = [], tfrees = []} (cls @ ths) + val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap) + fun used c = exists (Metis.LiteralSet.exists (const_in_metis c)) clause_lists + (*Now check for the existence of certain combinators*) + val IK = if used "c_COMBI" orelse used "c_COMBK" then [comb_I,comb_K] else [] + val BC = if used "c_COMBB" then [comb_B] else [] + val EQ = if used "c_fequal" then [fequal_imp_equal', equal_imp_fequal'] else [] + val lmap' = if isFO then lmap else foldl (add_thm thy) lmap ([ext_thm] @ EQ @ IK @ BC) + in + add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap' + end; + + fun refute cls = + Metis.Resolution.loop (Metis.Resolution.new Metis.Resolution.default cls); + + fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const); + + (* Main function to start metis prove and reconstruction *) + fun FOL_SOLVE mode ctxt cls ths = + let val thy = ProofContext.theory_of ctxt + val _ = if exists(is_false o prop_of) cls then error "problem contains the empty clause" + else (); + val _ = ResClause.init thy + val _ = ResHolClause.init thy + val _ = Output.debug (fn () => "FOL_SOLVE: CONJECTURE CLAUSES") + val _ = app (fn th => Output.debug (fn () => string_of_thm th)) cls + val _ = Output.debug (fn () => "THEOREM CLAUSES") + val _ = app (fn th => Output.debug (fn () => string_of_thm th)) ths + val {isFO,axioms,tfrees} = build_map mode thy cls ths + val _ = if null tfrees then () + else (Output.debug (fn () => "TFREE CLAUSES"); + app (fn tf => Output.debug (fn _ => ResClause.tptp_of_typeLit tf)) tfrees) + val _ = Output.debug (fn () => "CLAUSES GIVEN TO METIS") + val thms = map #1 axioms + val _ = app (fn th => Output.debug (fn () => Metis.Thm.toString th)) thms + val _ = if isFO + then Output.debug (fn () => "goal is first-order") + else Output.debug (fn () => "goal is higher-order") + val _ = Output.debug (fn () => "START METIS PROVE PROCESS") + in + case refute thms of + Metis.Resolution.Contradiction mth => + let val _ = Output.debug (fn () => "METIS RECONSTRUCTION START: " ^ + Metis.Thm.toString mth) + val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt + (*add constraints arising from converting goal to clause form*) + val result = translate isFO ctxt' axioms (Metis.Proof.proof mth) + val _ = Output.debug (fn () => "METIS COMPLETED") + in + case result of + (_,ith)::_ => (Output.debug (fn () => "success: " ^ string_of_thm ith); ith) + | _ => error "METIS: no result" + end + | Metis.Resolution.Satisfiable _ => error "Metis finds the theorem to be invalid" + end; + + fun metis_general_tac mode ctxt ths i st0 = + let val _ = Output.debug (fn () => "Metis called with theorems " ^ cat_lines (map string_of_thm ths)) + val ths' = ResAxioms.cnf_rules_of_ths ths + in + (MESON ResAxioms.neg_clausify (fn cls => rtac (FOL_SOLVE mode ctxt cls ths') 1) i + THEN ResAxioms.expand_defs_tac st0) st0 + end; + + fun metis_tac ths gno st = + metis_general_tac ResAtp.Auto (ProofContext.init (theory_of_thm st)) ths gno st; + + fun metisF_tac ths gno st = + metis_general_tac ResAtp.Fol (ProofContext.init (theory_of_thm st)) ths gno st; + + fun metisH_tac ths gno st = + metis_general_tac ResAtp.Hol (ProofContext.init (theory_of_thm st)) ths gno st; + + fun metis_meth mode ths ctxt = + Method.SIMPLE_METHOD' + (setmp ResHolClause.typ_level ResHolClause.T_CONST (*constant-typed*) + (setmp ResHolClause.minimize_applies false (*avoid this optimization*) + (CHANGED_PROP o metis_general_tac mode ctxt ths))); + + fun metis ths ctxt = metis_meth ResAtp.Auto ths ctxt; + fun metisF ths ctxt = metis_meth ResAtp.Fol ths ctxt; + fun metisH ths ctxt = metis_meth ResAtp.Hol ths ctxt; + + val setup = + Method.add_methods + [("metis", Method.thms_ctxt_args metis, "METIS for FOL & HOL problems"), + ("metisF", Method.thms_ctxt_args metisF, "METIS for FOL problems"), + ("metisH", Method.thms_ctxt_args metisH, "METIS for HOL problems"), + ("finish_clausify", + Method.no_args (Method.SIMPLE_METHOD' (K (ResAxioms.expand_defs_tac refl))), + "cleanup after conversion to clauses")]; + +end;