# HG changeset patch # User blanchet # Date 1284651029 -7200 # Node ID fa16349939b7b7370e340b014684161f9a81a946 # Parent a52a4e4399c19b1e30630ee1325923e5f36a32f9 complete refactoring of Metis along the lines of Sledgehammer diff -r a52a4e4399c1 -r fa16349939b7 src/HOL/Tools/Sledgehammer/metis_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/metis_reconstruct.ML Thu Sep 16 16:54:42 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_reconstruct.ML Thu Sep 16 17:30:29 2010 +0200 @@ -9,9 +9,500 @@ signature METIS_RECONSTRUCT = sig + type mode = Metis_Translate.mode + + val trace: bool Unsynchronized.ref + val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a + val replay_one_inference : + Proof.context -> mode -> (string * term) list + -> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list + -> (Metis_Thm.thm * thm) list end; structure Metis_Reconstruct : METIS_RECONSTRUCT = struct +open Metis_Translate + +val trace = Unsynchronized.ref false +fun trace_msg msg = if !trace then tracing (msg ()) else () + +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), _)) :: 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 raise Fail + ("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global Pure.thy rator ^ + " expected " ^ Int.toString nargs ^ + " received " ^ commas (map (Syntax.string_of_term_global Pure.thy) trands)) + end; + +fun infer_types ctxt = + Syntax.check_terms (ProofContext.set_mode ProofContext.mode_pattern ctxt); + +(*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,T) = Term.Var((w,1), T); + +(*include the default sort, if available*) +fun mk_tfree ctxt w = + let val ww = "'" ^ w + in TFree(ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1))) 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); + +fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS) + +fun smart_invert_const "fequal" = @{const_name HOL.eq} + | smart_invert_const s = invert_const s + +fun hol_type_from_metis_term _ (Metis_Term.Var v) = + (case strip_prefix_and_unascii tvar_prefix v of + SOME w => make_tvar w + | NONE => make_tvar v) + | hol_type_from_metis_term ctxt (Metis_Term.Fn(x, tys)) = + (case strip_prefix_and_unascii type_const_prefix x of + SOME tc => Term.Type (smart_invert_const tc, + map (hol_type_from_metis_term ctxt) tys) + | NONE => + case strip_prefix_and_unascii tfree_prefix x of + SOME tf => mk_tfree ctxt tf + | NONE => raise Fail ("hol_type_from_metis_term: " ^ x)); + +(*Maps metis terms to isabelle terms*) +fun hol_term_from_metis_PT ctxt fol_tm = + let val thy = ProofContext.theory_of ctxt + val _ = trace_msg (fn () => "hol_term_from_metis_PT: " ^ + Metis_Term.toString fol_tm) + fun tm_to_tt (Metis_Term.Var v) = + (case strip_prefix_and_unascii tvar_prefix v of + SOME w => Type (make_tvar w) + | NONE => + case strip_prefix_and_unascii schematic_var_prefix v of + SOME w => Term (mk_var (w, HOLogic.typeT)) + | NONE => Term (mk_var (v, HOLogic.typeT)) ) + (*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))) + | _ => raise Fail "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 (@{const_name HOL.eq}, HOLogic.typeT), terms_of (map tm_to_tt ts))) + | applic_to_tt (a,ts) = + case strip_prefix_and_unascii const_prefix a of + SOME b => + let val c = smart_invert_const b + val ntypes = num_type_args thy c + val nterms = length ts - ntypes + val tts = map tm_to_tt ts + val tys = types_of (List.take(tts,ntypes)) + in if length tys = ntypes then + apply_list (Const (c, dummyT)) nterms (List.drop(tts,ntypes)) + else + raise Fail ("Constant " ^ c ^ " expects " ^ Int.toString ntypes ^ + " but gets " ^ Int.toString (length tys) ^ + " type arguments\n" ^ + cat_lines (map (Syntax.string_of_typ ctxt) tys) ^ + " the terms are \n" ^ + cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts))) + end + | NONE => (*Not a constant. Is it a type constructor?*) + case strip_prefix_and_unascii type_const_prefix a of + SOME b => + Type (Term.Type (smart_invert_const b, types_of (map tm_to_tt ts))) + | NONE => (*Maybe a TFree. Should then check that ts=[].*) + case strip_prefix_and_unascii tfree_prefix a of + SOME b => Type (mk_tfree ctxt b) + | NONE => (*a fixed variable? They are Skolem functions.*) + case strip_prefix_and_unascii 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 => raise Fail ("unexpected metis function: " ^ a) + in + case tm_to_tt fol_tm of + Term t => t + | _ => raise Fail "fol_tm_to_tt: Term expected" + end + +(*Maps fully-typed metis terms to isabelle terms*) +fun hol_term_from_metis_FT ctxt fol_tm = + let val _ = trace_msg (fn () => "hol_term_from_metis_FT: " ^ + Metis_Term.toString fol_tm) + fun cvt (Metis_Term.Fn ("ti", [Metis_Term.Var v, _])) = + (case strip_prefix_and_unascii schematic_var_prefix v of + SOME w => mk_var(w, dummyT) + | NONE => mk_var(v, dummyT)) + | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn ("=",[]), _])) = + Const (@{const_name HOL.eq}, HOLogic.typeT) + | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn (x,[]), ty])) = + (case strip_prefix_and_unascii const_prefix x of + SOME c => Const (smart_invert_const c, dummyT) + | NONE => (*Not a constant. Is it a fixed variable??*) + case strip_prefix_and_unascii fixed_var_prefix x of + SOME v => Free (v, hol_type_from_metis_term ctxt ty) + | NONE => raise Fail ("hol_term_from_metis_FT bad constant: " ^ x)) + | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn (".",[tm1,tm2]), _])) = + cvt tm1 $ cvt tm2 + | cvt (Metis_Term.Fn (".",[tm1,tm2])) = (*untyped application*) + cvt tm1 $ cvt tm2 + | cvt (Metis_Term.Fn ("{}", [arg])) = cvt arg (*hBOOL*) + | cvt (Metis_Term.Fn ("=", [tm1,tm2])) = + list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), map cvt [tm1,tm2]) + | cvt (t as Metis_Term.Fn (x, [])) = + (case strip_prefix_and_unascii const_prefix x of + SOME c => Const (smart_invert_const c, dummyT) + | NONE => (*Not a constant. Is it a fixed variable??*) + case strip_prefix_and_unascii fixed_var_prefix x of + SOME v => Free (v, dummyT) + | NONE => (trace_msg (fn () => "hol_term_from_metis_FT bad const: " ^ x); + hol_term_from_metis_PT ctxt t)) + | cvt t = (trace_msg (fn () => "hol_term_from_metis_FT bad term: " ^ Metis_Term.toString t); + hol_term_from_metis_PT ctxt t) + in fol_tm |> cvt end + +fun hol_term_from_metis FT = hol_term_from_metis_FT + | hol_term_from_metis _ = hol_term_from_metis_PT + +fun hol_terms_from_fol ctxt mode skolems fol_tms = + let val ts = map (hol_term_from_metis mode ctxt) fol_tms + val _ = trace_msg (fn () => " calling type inference:") + val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts + val ts' = ts |> map (reveal_skolem_terms skolems) |> infer_types ctxt + val _ = app (fn t => trace_msg + (fn () => " final term: " ^ Syntax.string_of_term ctxt t ^ + " of type " ^ Syntax.string_of_typ ctxt (type_of t))) + ts' + in ts' end; + +(* ------------------------------------------------------------------------- *) +(* FOL step Inference Rules *) +(* ------------------------------------------------------------------------- *) + +(*for debugging only*) +(* +fun print_thpair (fth,th) = + (trace_msg (fn () => "============================================="); + trace_msg (fn () => "Metis: " ^ Metis_Thm.toString fth); + trace_msg (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th)); +*) + +fun lookth thpairs (fth : Metis_Thm.thm) = + the (AList.lookup (uncurry Metis_Thm.equal) thpairs fth) + handle Option.Option => + raise Fail ("Failed to find Metis theorem " ^ Metis_Thm.toString fth) + +fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx)); + +(* INFERENCE RULE: AXIOM *) + +fun axiom_inf thpairs th = Thm.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 *) + +val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)} + +fun inst_excluded_middle thy i_atm = + let val th = EXCLUDED_MIDDLE + val [vx] = Term.add_vars (prop_of th) [] + val substs = [(cterm_of thy (Var vx), cterm_of thy i_atm)] + in cterm_instantiate substs th end; + +fun assume_inf ctxt mode skolems atm = + inst_excluded_middle + (ProofContext.theory_of ctxt) + (singleton (hol_terms_from_fol ctxt mode skolems) (Metis_Term.Fn atm)) + +(* INFERENCE RULE: INSTANTIATE (Subst). Type instantiations are ignored. Trying + 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 mode skolems thpairs fsubst th = + let val thy = ProofContext.theory_of ctxt + val i_th = lookth thpairs th + val i_th_vars = Term.add_vars (prop_of i_th) [] + fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars) + fun subst_translation (x,y) = + let val v = find_var x + (* We call "reveal_skolem_terms" and "infer_types" below. *) + val t = hol_term_from_metis mode ctxt y + in SOME (cterm_of thy (Var v), t) end + handle Option => + (trace_msg (fn() => "\"find_var\" failed for the variable " ^ x ^ + " in " ^ Display.string_of_thm ctxt i_th); + NONE) + fun remove_typeinst (a, t) = + case strip_prefix_and_unascii schematic_var_prefix a of + SOME b => SOME (b, t) + | NONE => case strip_prefix_and_unascii tvar_prefix a of + SOME _ => NONE (*type instantiations are forbidden!*) + | NONE => SOME (a,t) (*internal Metis var?*) + val _ = trace_msg (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th) + val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst) + val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs) + val tms = rawtms |> map (reveal_skolem_terms skolems) |> infer_types ctxt + val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th) + val substs' = ListPair.zip (vars, map ctm_of tms) + val _ = trace_msg (fn () => + cat_lines ("subst_translations:" :: + (substs' |> map (fn (x, y) => + Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^ + Syntax.string_of_term ctxt (term_of y))))); + in cterm_instantiate substs' i_th end + handle THM (msg, _, _) => + error ("Cannot replay Metis proof in Isabelle:\n" ^ msg) + +(* INFERENCE RULE: RESOLVE *) + +(* Like RSN, but we rename apart only the type variables. Vars here typically + have an index of 1, and the use of RSN would increase this typically to 3. + Instantiations of those Vars could then fail. See comment on "mk_var". *) +fun resolve_inc_tyvars thy tha i thb = + let + val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha + fun aux tha thb = + case Thm.bicompose false (false, tha, nprems_of tha) i thb + |> Seq.list_of |> distinct Thm.eq_thm of + [th] => th + | _ => raise THM ("resolve_inc_tyvars: unique result expected", i, + [tha, thb]) + in + aux tha thb + handle TERM z => + (* The unifier, which is invoked from "Thm.bicompose", will sometimes + refuse to unify "?a::?'a" with "?a::?'b" or "?a::nat" and throw a + "TERM" exception (with "add_ffpair" as first argument). We then + perform unification of the types of variables by hand and try + again. We could do this the first time around but this error + occurs seldom and we don't want to break existing proofs in subtle + ways or slow them down needlessly. *) + case [] |> fold (Term.add_vars o prop_of) [tha, thb] + |> AList.group (op =) + |> maps (fn ((s, _), T :: Ts) => + map (fn T' => (Free (s, T), Free (s, T'))) Ts) + |> rpair (Envir.empty ~1) + |-> fold (Pattern.unify thy) + |> Envir.type_env |> Vartab.dest + |> map (fn (x, (S, T)) => + pairself (ctyp_of thy) (TVar (x, S), T)) of + [] => raise TERM z + | ps => aux (instantiate (ps, []) tha) (instantiate (ps, []) thb) + end + +fun mk_not (Const (@{const_name Not}, _) $ b) = b + | mk_not b = HOLogic.mk_not b + +(* 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, for some reason. *) + | untyped_aconv (Bound i) (Bound j) = (i = j) + | untyped_aconv (Abs (_, _, t)) (Abs (_, _, u)) = 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 literal_index lit = + let + val lit = Envir.eta_contract lit + fun get _ [] = 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 + +fun resolve_inf ctxt mode skolems thpairs atm th1 th2 = + let + val thy = ProofContext.theory_of ctxt + val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2 + val _ = trace_msg (fn () => " isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1) + val _ = trace_msg (fn () => " isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2) + in + (* Trivial cases where one operand is type info *) + if Thm.eq_thm (TrueI, i_th1) then + i_th2 + else if Thm.eq_thm (TrueI, i_th2) then + i_th1 + else + let + val i_atm = singleton (hol_terms_from_fol ctxt mode skolems) + (Metis_Term.Fn atm) + val _ = trace_msg (fn () => " atom: " ^ Syntax.string_of_term ctxt i_atm) + val prems_th1 = prems_of i_th1 + val prems_th2 = prems_of i_th2 + val index_th1 = literal_index (mk_not i_atm) prems_th1 + handle Empty => raise Fail "Failed to find literal in th1" + val _ = trace_msg (fn () => " index_th1: " ^ Int.toString index_th1) + val index_th2 = literal_index i_atm prems_th2 + handle Empty => raise Fail "Failed to find literal in th2" + val _ = trace_msg (fn () => " index_th2: " ^ Int.toString index_th2) + in + resolve_inc_tyvars thy (Meson.select_literal index_th1 i_th1) index_th2 + i_th2 + end + end; + +(* INFERENCE RULE: REFL *) + +val REFL_THM = Thm.incr_indexes 2 @{lemma "t ~= t ==> False" by simp} + +val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) []))); +val refl_idx = 1 + Thm.maxidx_of REFL_THM; + +fun refl_inf ctxt mode skolems t = + let val thy = ProofContext.theory_of ctxt + val i_t = singleton (hol_terms_from_fol ctxt mode skolems) t + val _ = trace_msg (fn () => " term: " ^ Syntax.string_of_term ctxt i_t) + val c_t = cterm_incr_types thy refl_idx i_t + in cterm_instantiate [(refl_x, c_t)] REFL_THM end; + +(* INFERENCE RULE: EQUALITY *) + +val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp} +val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp} + +val metis_eq = Metis_Term.Fn ("=", []); + +fun get_ty_arg_size _ (Const (@{const_name HOL.eq}, _)) = 0 (*equality has no type arguments*) + | get_ty_arg_size thy (Const (c, _)) = (num_type_args thy c handle TYPE _ => 0) + | get_ty_arg_size _ _ = 0; + +fun equality_inf ctxt mode skolems (pos, atm) fp fr = + let val thy = ProofContext.theory_of ctxt + val m_tm = Metis_Term.Fn atm + val [i_atm,i_tm] = hol_terms_from_fol ctxt mode skolems [m_tm, fr] + val _ = trace_msg (fn () => "sign of the literal: " ^ Bool.toString pos) + fun replace_item_list lx 0 (_::ls) = lx::ls + | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls + fun path_finder_FO tm [] = (tm, Term.Bound 0) + | path_finder_FO tm (p::ps) = + let val (tm1,args) = 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 ("Cannot replay Metis proof in Isabelle:\n" ^ + "equality_inf: " ^ Int.toString p ^ " adj " ^ + Int.toString adjustment ^ " term " ^ + Syntax.string_of_term ctxt tm) + val _ = trace_msg (fn () => "path_finder: " ^ Int.toString p ^ + " " ^ Syntax.string_of_term ctxt tm_p) + val (r,t) = path_finder_FO tm_p ps + in + (r, list_comb (tm1, replace_item_list t p' args)) + 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) (_::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps) + | path_finder_HO tm ps = + raise Fail ("equality_inf, path_finder_HO: path = " ^ + space_implode " " (map Int.toString ps) ^ + " isa-term: " ^ Syntax.string_of_term ctxt tm) + fun path_finder_FT tm [] _ = (tm, Term.Bound 0) + | path_finder_FT tm (0::ps) (Metis_Term.Fn ("ti", [t1, _])) = + path_finder_FT tm ps t1 + | path_finder_FT (t$u) (0::ps) (Metis_Term.Fn (".", [t1, _])) = + (fn(x,y) => (x, y$u)) (path_finder_FT t ps t1) + | path_finder_FT (t$u) (1::ps) (Metis_Term.Fn (".", [_, t2])) = + (fn(x,y) => (x, t$y)) (path_finder_FT u ps t2) + | path_finder_FT tm ps t = + raise Fail ("equality_inf, path_finder_FT: path = " ^ + space_implode " " (map Int.toString ps) ^ + " isa-term: " ^ Syntax.string_of_term ctxt tm ^ + " fol-term: " ^ Metis_Term.toString t) + fun path_finder FO tm ps _ = path_finder_FO tm ps + | path_finder HO (tm as Const(@{const_name HOL.eq},_) $ _ $ _) (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 HO tm (_ :: ps) (Metis_Term.Fn ("{}", [_])) = + path_finder_HO tm ps (*if not equality, ignore head to skip hBOOL*) + | path_finder FT (tm as Const(@{const_name HOL.eq}, _) $ _ $ _) (p::ps) + (Metis_Term.Fn ("=", [t1,t2])) = + (*equality: not curried, as other predicates are*) + if p=0 then path_finder_FT tm (0::1::ps) + (Metis_Term.Fn (".", [Metis_Term.Fn (".", [metis_eq,t1]), t2])) + (*select first operand*) + else path_finder_FT tm (p::ps) + (Metis_Term.Fn (".", [metis_eq,t2])) + (*1 selects second operand*) + | path_finder FT tm (_ :: ps) (Metis_Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1 + (*if not equality, ignore head to skip the hBOOL predicate*) + | path_finder FT tm ps t = path_finder_FT tm ps t (*really an error case!*) + fun path_finder_lit ((nt as Const (@{const_name Not}, _)) $ tm_a) idx = + let val (tm, tm_rslt) = path_finder mode tm_a idx m_tm + in (tm, nt $ tm_rslt) end + | path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm + val (tm_subst, body) = path_finder_lit i_atm fp + val tm_abs = Term.Abs ("x", type_of tm_subst, body) + val _ = trace_msg (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs) + val _ = trace_msg (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm) + val _ = trace_msg (fn () => "located term: " ^ Syntax.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' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em) + val _ = trace_msg (fn () => "subst' " ^ Display.string_of_thm ctxt subst') + val eq_terms = map (pairself (cterm_of thy)) + (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm])) + in cterm_instantiate eq_terms subst' end; + +val factor = Seq.hd o distinct_subgoals_tac; + +fun step ctxt mode skolems thpairs p = + case p of + (fol_th, Metis_Proof.Axiom _) => factor (axiom_inf thpairs fol_th) + | (_, Metis_Proof.Assume f_atm) => assume_inf ctxt mode skolems f_atm + | (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) => + factor (inst_inf ctxt mode skolems thpairs f_subst f_th1) + | (_, Metis_Proof.Resolve(f_atm, f_th1, f_th2)) => + factor (resolve_inf ctxt mode skolems thpairs f_atm f_th1 f_th2) + | (_, Metis_Proof.Refl f_tm) => refl_inf ctxt mode skolems f_tm + | (_, Metis_Proof.Equality (f_lit, f_p, f_r)) => + equality_inf ctxt mode skolems f_lit f_p f_r + +fun is_real_literal (_, (c, _)) = not (String.isPrefix class_prefix c) + +fun replay_one_inference ctxt mode skolems (fol_th, inf) thpairs = + let + val _ = trace_msg (fn () => "=============================================") + val _ = trace_msg (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th) + val _ = trace_msg (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf) + val th = Meson.flexflex_first_order (step ctxt mode skolems + thpairs (fol_th, inf)) + val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th) + val _ = trace_msg (fn () => "=============================================") + val n_metis_lits = + length (filter is_real_literal (Metis_LiteralSet.toList (Metis_Thm.clause fol_th))) + val _ = if nprems_of th = n_metis_lits then () + else error "Cannot replay Metis proof in Isabelle." + in (fol_th, th) :: thpairs end + end; diff -r a52a4e4399c1 -r fa16349939b7 src/HOL/Tools/Sledgehammer/metis_tactics.ML --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Thu Sep 16 16:54:42 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Thu Sep 16 17:30:29 2010 +0200 @@ -9,733 +9,34 @@ signature METIS_TACTICS = sig - val trace: bool Unsynchronized.ref - val type_lits: bool Config.T - val metis_tac: Proof.context -> thm list -> int -> tactic - val metisF_tac: Proof.context -> thm list -> int -> tactic - val metisFT_tac: Proof.context -> thm list -> int -> tactic - val setup: theory -> theory + val trace : bool Unsynchronized.ref + val type_lits : bool Config.T + val metis_tac : Proof.context -> thm list -> int -> tactic + val metisF_tac : Proof.context -> thm list -> int -> tactic + val metisFT_tac : Proof.context -> thm list -> int -> tactic + val setup : theory -> theory end structure Metis_Tactics : METIS_TACTICS = struct open Metis_Translate +open Metis_Reconstruct -val trace = Unsynchronized.ref false; -fun trace_msg msg = if !trace then tracing (msg ()) else (); +val trace = Unsynchronized.ref false +fun trace_msg msg = if !trace then tracing (msg ()) else () val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" (K true); -datatype mode = FO | HO | FT (* first-order, higher-order, fully-typed *) - -(* ------------------------------------------------------------------------- *) -(* Useful Theorems *) -(* ------------------------------------------------------------------------- *) -val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)} -val REFL_THM = Thm.incr_indexes 2 @{lemma "t ~= t ==> False" by simp} -val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp} -val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp} - -(* ------------------------------------------------------------------------- *) -(* 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, for some reason. *) - | untyped_aconv (Bound i) (Bound j) = (i = j) - | untyped_aconv (Abs (_, _, t)) (Abs (_, _, u)) = 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 _ [] = 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_sublevel "equal" = "=" (* FIXME: "c_fequal" *) - | fn_isa_to_met_sublevel x = x -fun fn_isa_to_met_toplevel "equal" = "=" - | fn_isa_to_met_toplevel x = x - -fun metis_lit b c args = (b, (c, args)); - -fun metis_term_from_combtyp (CombTVar (s, _)) = Metis_Term.Var s - | metis_term_from_combtyp (CombTFree (s, _)) = Metis_Term.Fn (s, []) - | metis_term_from_combtyp (CombType ((s, _), tps)) = - Metis_Term.Fn (s, map metis_term_from_combtyp 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 strip_combterm_comb tm of - (CombConst ((c, _), _, tys), tms) => - let val tyargs = map metis_term_from_combtyp tys - val args = map hol_term_to_fol_FO tms - in Metis_Term.Fn (c, tyargs @ args) end - | (CombVar ((v, _), _), []) => Metis_Term.Var v - | _ => raise Fail "non-first-order combterm" - -fun hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) = - Metis_Term.Fn (fn_isa_to_met_sublevel a, map metis_term_from_combtyp tylist) - | hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis_Term.Var s - | hol_term_to_fol_HO (CombApp (tm1, tm2)) = - Metis_Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]); - -(*The fully-typed translation, to avoid type errors*) -fun wrap_type (tm, ty) = Metis_Term.Fn("ti", [tm, metis_term_from_combtyp ty]); - -fun hol_term_to_fol_FT (CombVar ((s, _), ty)) = wrap_type (Metis_Term.Var s, ty) - | hol_term_to_fol_FT (CombConst((a, _), ty, _)) = - wrap_type (Metis_Term.Fn(fn_isa_to_met_sublevel a, []), ty) - | hol_term_to_fol_FT (tm as CombApp(tm1,tm2)) = - wrap_type (Metis_Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]), - combtyp_of tm) - -fun hol_literal_to_fol FO (FOLLiteral (pos, tm)) = - let val (CombConst((p, _), _, tys), tms) = strip_combterm_comb tm - val tylits = if p = "equal" then [] else map metis_term_from_combtyp tys - val lits = map hol_term_to_fol_FO tms - in metis_lit pos (fn_isa_to_met_toplevel p) (tylits @ lits) end - | hol_literal_to_fol HO (FOLLiteral (pos, tm)) = - (case strip_combterm_comb tm of - (CombConst(("equal", _), _, _), tms) => - metis_lit pos "=" (map hol_term_to_fol_HO tms) - | _ => metis_lit pos "{}" [hol_term_to_fol_HO tm]) (*hBOOL*) - | hol_literal_to_fol FT (FOLLiteral (pos, tm)) = - (case strip_combterm_comb tm of - (CombConst(("equal", _), _, _), tms) => - metis_lit pos "=" (map hol_term_to_fol_FT tms) - | _ => metis_lit pos "{}" [hol_term_to_fol_FT tm]) (*hBOOL*); - -fun literals_of_hol_term thy mode t = - let val (lits, types_sorts) = literals_of_term thy t - in (map (hol_literal_to_fol mode) lits, types_sorts) end; - -(*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*) -fun metis_of_type_literals pos (TyLitVar ((s, _), (s', _))) = - metis_lit pos s [Metis_Term.Var s'] - | metis_of_type_literals pos (TyLitFree ((s, _), (s', _))) = - metis_lit pos s [Metis_Term.Fn (s',[])] - -fun default_sort _ (TVar _) = false - | default_sort ctxt (TFree (x, s)) = (s = the_default [] (Variable.def_sort ctxt (x, ~1))); - -fun metis_of_tfree tf = - Metis_Thm.axiom (Metis_LiteralSet.singleton (metis_of_type_literals true tf)); - -fun hol_thm_to_fol is_conjecture ctxt mode j skolems th = - let - val thy = ProofContext.theory_of ctxt - val (skolems, (mlits, types_sorts)) = - th |> prop_of |> conceal_skolem_terms j skolems - ||> (HOLogic.dest_Trueprop #> literals_of_hol_term thy mode) - in - if is_conjecture then - (Metis_Thm.axiom (Metis_LiteralSet.fromList mlits), - type_literals_for_types types_sorts, skolems) - else - let val tylits = filter_out (default_sort ctxt) types_sorts - |> type_literals_for_types - val mtylits = if Config.get ctxt type_lits - then map (metis_of_type_literals false) tylits else [] - in - (Metis_Thm.axiom (Metis_LiteralSet.fromList(mtylits @ mlits)), [], - skolems) - end - end; - -(* ARITY CLAUSE *) - -fun m_arity_cls (TConsLit ((c, _), (t, _), args)) = - metis_lit true c [Metis_Term.Fn(t, map (Metis_Term.Var o fst) args)] - | m_arity_cls (TVarLit ((c, _), (s, _))) = - metis_lit false c [Metis_Term.Var s] - -(*TrueI is returned as the Isabelle counterpart because there isn't any.*) -fun arity_cls (ArityClause {conclLit, premLits, ...}) = - (TrueI, - Metis_Thm.axiom (Metis_LiteralSet.fromList (map m_arity_cls (conclLit :: premLits)))); - -(* CLASSREL CLAUSE *) - -fun m_class_rel_cls (subclass, _) (superclass, _) = - [metis_lit false subclass [Metis_Term.Var "T"], metis_lit true superclass [Metis_Term.Var "T"]]; - -fun class_rel_cls (ClassRelClause {subclass, superclass, ...}) = - (TrueI, Metis_Thm.axiom (Metis_LiteralSet.fromList (m_class_rel_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), _)) :: 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 raise Fail - ("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global Pure.thy rator ^ - " expected " ^ Int.toString nargs ^ - " received " ^ commas (map (Syntax.string_of_term_global Pure.thy) trands)) - end; - -fun infer_types ctxt = - Syntax.check_terms (ProofContext.set_mode ProofContext.mode_pattern ctxt); - -(*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,T) = Term.Var((w,1), T); - -(*include the default sort, if available*) -fun mk_tfree ctxt w = - let val ww = "'" ^ w - in TFree(ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1))) 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); - -fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS) - -fun smart_invert_const "fequal" = @{const_name HOL.eq} - | smart_invert_const s = invert_const s - -fun hol_type_from_metis_term _ (Metis_Term.Var v) = - (case strip_prefix_and_unascii tvar_prefix v of - SOME w => make_tvar w - | NONE => make_tvar v) - | hol_type_from_metis_term ctxt (Metis_Term.Fn(x, tys)) = - (case strip_prefix_and_unascii type_const_prefix x of - SOME tc => Term.Type (smart_invert_const tc, - map (hol_type_from_metis_term ctxt) tys) - | NONE => - case strip_prefix_and_unascii tfree_prefix x of - SOME tf => mk_tfree ctxt tf - | NONE => raise Fail ("hol_type_from_metis_term: " ^ x)); - -(*Maps metis terms to isabelle terms*) -fun hol_term_from_metis_PT ctxt fol_tm = - let val thy = ProofContext.theory_of ctxt - val _ = trace_msg (fn () => "hol_term_from_metis_PT: " ^ - Metis_Term.toString fol_tm) - fun tm_to_tt (Metis_Term.Var v) = - (case strip_prefix_and_unascii tvar_prefix v of - SOME w => Type (make_tvar w) - | NONE => - case strip_prefix_and_unascii schematic_var_prefix v of - SOME w => Term (mk_var (w, HOLogic.typeT)) - | NONE => Term (mk_var (v, HOLogic.typeT)) ) - (*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))) - | _ => raise Fail "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 (@{const_name HOL.eq}, HOLogic.typeT), terms_of (map tm_to_tt ts))) - | applic_to_tt (a,ts) = - case strip_prefix_and_unascii const_prefix a of - SOME b => - let val c = smart_invert_const b - val ntypes = num_type_args thy c - val nterms = length ts - ntypes - val tts = map tm_to_tt ts - val tys = types_of (List.take(tts,ntypes)) - in if length tys = ntypes then - apply_list (Const (c, dummyT)) nterms (List.drop(tts,ntypes)) - else - raise Fail ("Constant " ^ c ^ " expects " ^ Int.toString ntypes ^ - " but gets " ^ Int.toString (length tys) ^ - " type arguments\n" ^ - cat_lines (map (Syntax.string_of_typ ctxt) tys) ^ - " the terms are \n" ^ - cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts))) - end - | NONE => (*Not a constant. Is it a type constructor?*) - case strip_prefix_and_unascii type_const_prefix a of - SOME b => - Type (Term.Type (smart_invert_const b, types_of (map tm_to_tt ts))) - | NONE => (*Maybe a TFree. Should then check that ts=[].*) - case strip_prefix_and_unascii tfree_prefix a of - SOME b => Type (mk_tfree ctxt b) - | NONE => (*a fixed variable? They are Skolem functions.*) - case strip_prefix_and_unascii 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 => raise Fail ("unexpected metis function: " ^ a) - in - case tm_to_tt fol_tm of - Term t => t - | _ => raise Fail "fol_tm_to_tt: Term expected" - end +fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const); -(*Maps fully-typed metis terms to isabelle terms*) -fun hol_term_from_metis_FT ctxt fol_tm = - let val _ = trace_msg (fn () => "hol_term_from_metis_FT: " ^ - Metis_Term.toString fol_tm) - fun cvt (Metis_Term.Fn ("ti", [Metis_Term.Var v, _])) = - (case strip_prefix_and_unascii schematic_var_prefix v of - SOME w => mk_var(w, dummyT) - | NONE => mk_var(v, dummyT)) - | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn ("=",[]), _])) = - Const (@{const_name HOL.eq}, HOLogic.typeT) - | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn (x,[]), ty])) = - (case strip_prefix_and_unascii const_prefix x of - SOME c => Const (smart_invert_const c, dummyT) - | NONE => (*Not a constant. Is it a fixed variable??*) - case strip_prefix_and_unascii fixed_var_prefix x of - SOME v => Free (v, hol_type_from_metis_term ctxt ty) - | NONE => raise Fail ("hol_term_from_metis_FT bad constant: " ^ x)) - | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn (".",[tm1,tm2]), _])) = - cvt tm1 $ cvt tm2 - | cvt (Metis_Term.Fn (".",[tm1,tm2])) = (*untyped application*) - cvt tm1 $ cvt tm2 - | cvt (Metis_Term.Fn ("{}", [arg])) = cvt arg (*hBOOL*) - | cvt (Metis_Term.Fn ("=", [tm1,tm2])) = - list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), map cvt [tm1,tm2]) - | cvt (t as Metis_Term.Fn (x, [])) = - (case strip_prefix_and_unascii const_prefix x of - SOME c => Const (smart_invert_const c, dummyT) - | NONE => (*Not a constant. Is it a fixed variable??*) - case strip_prefix_and_unascii fixed_var_prefix x of - SOME v => Free (v, dummyT) - | NONE => (trace_msg (fn () => "hol_term_from_metis_FT bad const: " ^ x); - hol_term_from_metis_PT ctxt t)) - | cvt t = (trace_msg (fn () => "hol_term_from_metis_FT bad term: " ^ Metis_Term.toString t); - hol_term_from_metis_PT ctxt t) - in fol_tm |> cvt end - -fun hol_term_from_metis FT = hol_term_from_metis_FT - | hol_term_from_metis _ = hol_term_from_metis_PT - -fun hol_terms_from_fol ctxt mode skolems fol_tms = - let val ts = map (hol_term_from_metis mode ctxt) fol_tms - val _ = trace_msg (fn () => " calling type inference:") - val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts - val ts' = ts |> map (reveal_skolem_terms skolems) |> infer_types ctxt - val _ = app (fn t => trace_msg - (fn () => " final term: " ^ Syntax.string_of_term ctxt t ^ - " of type " ^ Syntax.string_of_typ ctxt (type_of t))) - ts' - in ts' end; - -fun mk_not (Const (@{const_name Not}, _) $ b) = b - | mk_not b = HOLogic.mk_not b; - -val metis_eq = Metis_Term.Fn ("=", []); - -(* ------------------------------------------------------------------------- *) -(* FOL step Inference Rules *) -(* ------------------------------------------------------------------------- *) - -(*for debugging only*) -(* -fun print_thpair (fth,th) = - (trace_msg (fn () => "============================================="); - trace_msg (fn () => "Metis: " ^ Metis_Thm.toString fth); - trace_msg (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th)); -*) - -fun lookth thpairs (fth : Metis_Thm.thm) = - the (AList.lookup (uncurry Metis_Thm.equal) thpairs fth) - handle Option => - raise Fail ("Failed to find a Metis theorem " ^ Metis_Thm.toString fth); - -fun is_TrueI th = Thm.eq_thm(TrueI,th); - -fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx)); - -fun inst_excluded_middle thy i_atm = - let val th = EXCLUDED_MIDDLE - val [vx] = Term.add_vars (prop_of th) [] - val substs = [(cterm_of thy (Var vx), cterm_of thy i_atm)] - in cterm_instantiate substs th end; - -(* INFERENCE RULE: AXIOM *) -fun axiom_inf thpairs th = Thm.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 mode skolems atm = - inst_excluded_middle - (ProofContext.theory_of ctxt) - (singleton (hol_terms_from_fol ctxt mode skolems) (Metis_Term.Fn atm)) - -(* INFERENCE RULE: INSTANTIATE (Subst). Type instantiations are ignored. Trying 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 mode skolems thpairs fsubst th = - let val thy = ProofContext.theory_of ctxt - val i_th = lookth thpairs th - val i_th_vars = Term.add_vars (prop_of i_th) [] - fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars) - fun subst_translation (x,y) = - let val v = find_var x - (* We call "reveal_skolem_terms" and "infer_types" below. *) - val t = hol_term_from_metis mode ctxt y - in SOME (cterm_of thy (Var v), t) end - handle Option => - (trace_msg (fn() => "\"find_var\" failed for the variable " ^ x ^ - " in " ^ Display.string_of_thm ctxt i_th); - NONE) - fun remove_typeinst (a, t) = - case strip_prefix_and_unascii schematic_var_prefix a of - SOME b => SOME (b, t) - | NONE => case strip_prefix_and_unascii tvar_prefix a of - SOME _ => NONE (*type instantiations are forbidden!*) - | NONE => SOME (a,t) (*internal Metis var?*) - val _ = trace_msg (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th) - val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst) - val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs) - val tms = rawtms |> map (reveal_skolem_terms skolems) |> infer_types ctxt - val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th) - val substs' = ListPair.zip (vars, map ctm_of tms) - val _ = trace_msg (fn () => - cat_lines ("subst_translations:" :: - (substs' |> map (fn (x, y) => - Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^ - Syntax.string_of_term ctxt (term_of y))))); - in cterm_instantiate substs' i_th end - handle THM (msg, _, _) => - error ("Cannot replay Metis proof in Isabelle:\n" ^ msg) - -(* INFERENCE RULE: RESOLVE *) - -(* Like RSN, but we rename apart only the type variables. Vars here typically - have an index of 1, and the use of RSN would increase this typically to 3. - Instantiations of those Vars could then fail. See comment on "mk_var". *) -fun resolve_inc_tyvars thy tha i thb = - let - val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha - fun aux tha thb = - case Thm.bicompose false (false, tha, nprems_of tha) i thb - |> Seq.list_of |> distinct Thm.eq_thm of - [th] => th - | _ => raise THM ("resolve_inc_tyvars: unique result expected", i, - [tha, thb]) - in - aux tha thb - handle TERM z => - (* The unifier, which is invoked from "Thm.bicompose", will sometimes - refuse to unify "?a::?'a" with "?a::?'b" or "?a::nat" and throw a - "TERM" exception (with "add_ffpair" as first argument). We then - perform unification of the types of variables by hand and try - again. We could do this the first time around but this error - occurs seldom and we don't want to break existing proofs in subtle - ways or slow them down needlessly. *) - case [] |> fold (Term.add_vars o prop_of) [tha, thb] - |> AList.group (op =) - |> maps (fn ((s, _), T :: Ts) => - map (fn T' => (Free (s, T), Free (s, T'))) Ts) - |> rpair (Envir.empty ~1) - |-> fold (Pattern.unify thy) - |> Envir.type_env |> Vartab.dest - |> map (fn (x, (S, T)) => - pairself (ctyp_of thy) (TVar (x, S), T)) of - [] => raise TERM z - | ps => aux (instantiate (ps, []) tha) (instantiate (ps, []) thb) - end - -fun resolve_inf ctxt mode skolems thpairs atm th1 th2 = - let - val thy = ProofContext.theory_of ctxt - val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2 - val _ = trace_msg (fn () => " isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1) - val _ = trace_msg (fn () => " isa th2 (neg): " ^ Display.string_of_thm ctxt 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 (hol_terms_from_fol ctxt mode skolems) - (Metis_Term.Fn atm) - val _ = trace_msg (fn () => " atom: " ^ Syntax.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 => raise Fail "Failed to find literal in th1" - val _ = trace_msg (fn () => " index_th1: " ^ Int.toString index_th1) - val index_th2 = get_index i_atm prems_th2 - handle Empty => raise Fail "Failed to find literal in th2" - val _ = trace_msg (fn () => " index_th2: " ^ Int.toString index_th2) - in - resolve_inc_tyvars thy (Meson.select_literal index_th1 i_th1) index_th2 - i_th2 - end - end; - -(* INFERENCE RULE: REFL *) -val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) []))); -val refl_idx = 1 + Thm.maxidx_of REFL_THM; - -fun refl_inf ctxt mode skolems t = - let val thy = ProofContext.theory_of ctxt - val i_t = singleton (hol_terms_from_fol ctxt mode skolems) t - val _ = trace_msg (fn () => " term: " ^ Syntax.string_of_term ctxt i_t) - val c_t = cterm_incr_types thy refl_idx i_t - in cterm_instantiate [(refl_x, c_t)] REFL_THM end; - -fun get_ty_arg_size _ (Const (@{const_name HOL.eq}, _)) = 0 (*equality has no type arguments*) - | get_ty_arg_size thy (Const (c, _)) = (num_type_args thy c handle TYPE _ => 0) - | get_ty_arg_size _ _ = 0; - -(* INFERENCE RULE: EQUALITY *) -fun equality_inf ctxt mode skolems (pos, atm) fp fr = - let val thy = ProofContext.theory_of ctxt - val m_tm = Metis_Term.Fn atm - val [i_atm,i_tm] = hol_terms_from_fol ctxt mode skolems [m_tm, fr] - val _ = trace_msg (fn () => "sign of the literal: " ^ Bool.toString pos) - fun replace_item_list lx 0 (_::ls) = lx::ls - | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls - fun path_finder_FO tm [] = (tm, Term.Bound 0) - | path_finder_FO tm (p::ps) = - let val (tm1,args) = 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 ("Cannot replay Metis proof in Isabelle:\n" ^ - "equality_inf: " ^ Int.toString p ^ " adj " ^ - Int.toString adjustment ^ " term " ^ - Syntax.string_of_term ctxt tm) - val _ = trace_msg (fn () => "path_finder: " ^ Int.toString p ^ - " " ^ Syntax.string_of_term ctxt tm_p) - val (r,t) = path_finder_FO tm_p ps - in - (r, list_comb (tm1, replace_item_list t p' args)) - 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) (_::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps) - | path_finder_HO tm ps = - raise Fail ("equality_inf, path_finder_HO: path = " ^ - space_implode " " (map Int.toString ps) ^ - " isa-term: " ^ Syntax.string_of_term ctxt tm) - fun path_finder_FT tm [] _ = (tm, Term.Bound 0) - | path_finder_FT tm (0::ps) (Metis_Term.Fn ("ti", [t1, _])) = - path_finder_FT tm ps t1 - | path_finder_FT (t$u) (0::ps) (Metis_Term.Fn (".", [t1, _])) = - (fn(x,y) => (x, y$u)) (path_finder_FT t ps t1) - | path_finder_FT (t$u) (1::ps) (Metis_Term.Fn (".", [_, t2])) = - (fn(x,y) => (x, t$y)) (path_finder_FT u ps t2) - | path_finder_FT tm ps t = - raise Fail ("equality_inf, path_finder_FT: path = " ^ - space_implode " " (map Int.toString ps) ^ - " isa-term: " ^ Syntax.string_of_term ctxt tm ^ - " fol-term: " ^ Metis_Term.toString t) - fun path_finder FO tm ps _ = path_finder_FO tm ps - | path_finder HO (tm as Const(@{const_name HOL.eq},_) $ _ $ _) (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 HO tm (_ :: ps) (Metis_Term.Fn ("{}", [_])) = - path_finder_HO tm ps (*if not equality, ignore head to skip hBOOL*) - | path_finder FT (tm as Const(@{const_name HOL.eq}, _) $ _ $ _) (p::ps) - (Metis_Term.Fn ("=", [t1,t2])) = - (*equality: not curried, as other predicates are*) - if p=0 then path_finder_FT tm (0::1::ps) - (Metis_Term.Fn (".", [Metis_Term.Fn (".", [metis_eq,t1]), t2])) - (*select first operand*) - else path_finder_FT tm (p::ps) - (Metis_Term.Fn (".", [metis_eq,t2])) - (*1 selects second operand*) - | path_finder FT tm (_ :: ps) (Metis_Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1 - (*if not equality, ignore head to skip the hBOOL predicate*) - | path_finder FT tm ps t = path_finder_FT tm ps t (*really an error case!*) - fun path_finder_lit ((nt as Const (@{const_name Not}, _)) $ tm_a) idx = - let val (tm, tm_rslt) = path_finder mode tm_a idx m_tm - in (tm, nt $ tm_rslt) end - | path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm - val (tm_subst, body) = path_finder_lit i_atm fp - val tm_abs = Term.Abs("x", Term.type_of tm_subst, body) - val _ = trace_msg (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs) - val _ = trace_msg (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm) - val _ = trace_msg (fn () => "located term: " ^ Syntax.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' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em) - val _ = trace_msg (fn () => "subst' " ^ Display.string_of_thm ctxt subst') - val eq_terms = map (pairself (cterm_of thy)) - (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm])) - in cterm_instantiate eq_terms subst' end; - -val factor = Seq.hd o distinct_subgoals_tac; - -fun step ctxt mode skolems thpairs p = - case p of - (fol_th, Metis_Proof.Axiom _) => factor (axiom_inf thpairs fol_th) - | (_, Metis_Proof.Assume f_atm) => assume_inf ctxt mode skolems f_atm - | (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) => - factor (inst_inf ctxt mode skolems thpairs f_subst f_th1) - | (_, Metis_Proof.Resolve(f_atm, f_th1, f_th2)) => - factor (resolve_inf ctxt mode skolems thpairs f_atm f_th1 f_th2) - | (_, Metis_Proof.Refl f_tm) => refl_inf ctxt mode skolems f_tm - | (_, Metis_Proof.Equality (f_lit, f_p, f_r)) => - equality_inf ctxt mode skolems f_lit f_p f_r - -fun real_literal (_, (c, _)) = not (String.isPrefix class_prefix c); - -fun translate_one ctxt mode skolems (fol_th, inf) thpairs = - let - val _ = trace_msg (fn () => "=============================================") - val _ = trace_msg (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th) - val _ = trace_msg (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf) - val th = Meson.flexflex_first_order (step ctxt mode skolems - thpairs (fol_th, inf)) - val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th) - val _ = trace_msg (fn () => "=============================================") - val n_metis_lits = - length (filter real_literal (Metis_LiteralSet.toList (Metis_Thm.clause fol_th))) - val _ = if nprems_of th = n_metis_lits then () - else error "Cannot replay Metis proof in Isabelle." - in (fol_th, th) :: thpairs end +fun have_common_thm ths1 ths2 = + exists (member Thm.eq_thm ths1) (map Meson.make_meta_clause ths2) (*Determining which axiom clauses are actually used*) fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th) | used_axioms _ _ = NONE; -(* ------------------------------------------------------------------------- *) -(* Translation of HO Clauses *) -(* ------------------------------------------------------------------------- *) - -fun type_ext thy tms = - let val subs = tfree_classes_of_terms tms - val supers = tvar_classes_of_terms tms - and tycons = type_consts_of_terms thy tms - val (supers', arity_clauses) = make_arity_clauses thy tycons supers - val class_rel_clauses = make_class_rel_clauses thy subs supers' - in map class_rel_cls class_rel_clauses @ map arity_cls arity_clauses - end; - -(* ------------------------------------------------------------------------- *) -(* Logic maps manage the interface between HOL and first-order logic. *) -(* ------------------------------------------------------------------------- *) - -type logic_map = - {axioms: (Metis_Thm.thm * thm) list, - tfrees: type_literal list, - skolems: (string * term) list} - -fun const_in_metis c (pred, tm_list) = - let - fun in_mterm (Metis_Term.Var _) = 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; - -(*Extract TFree constraints from context to include as conjecture clauses*) -fun init_tfrees ctxt = - let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts in - Vartab.fold add (#2 (Variable.constraints_of ctxt)) [] - |> type_literals_for_types - end; - -(*transform isabelle type / arity clause to metis clause *) -fun add_type_thm [] lmap = lmap - | add_type_thm ((ith, mth) :: cls) {axioms, tfrees, skolems} = - add_type_thm cls {axioms = (mth, ith) :: axioms, tfrees = tfrees, - skolems = skolems} - -(*Insert non-logical axioms corresponding to all accumulated TFrees*) -fun add_tfrees {axioms, tfrees, skolems} : logic_map = - {axioms = map (rpair TrueI o metis_of_tfree) (distinct (op =) tfrees) @ - axioms, - tfrees = tfrees, skolems = skolems} - -fun string_of_mode FO = "FO" - | string_of_mode HO = "HO" - | string_of_mode FT = "FT" - -val helpers = - [("c_COMBI", (false, map (`I) @{thms COMBI_def})), - ("c_COMBK", (false, map (`I) @{thms COMBK_def})), - ("c_COMBB", (false, map (`I) @{thms COMBB_def})), - ("c_COMBC", (false, map (`I) @{thms COMBC_def})), - ("c_COMBS", (false, map (`I) @{thms COMBS_def})), - ("c_fequal", (false, map (rpair @{thm equal_imp_equal}) - @{thms fequal_imp_equal equal_imp_fequal})), - ("c_True", (true, map (`I) @{thms True_or_False})), - ("c_False", (true, map (`I) @{thms True_or_False})), - ("c_If", (true, map (`I) @{thms if_True if_False True_or_False}))] - -fun is_quasi_fol_clause thy = - Meson.is_fol_term thy o snd o conceal_skolem_terms ~1 [] o prop_of - -(* Function to generate metis clauses, including comb and type clauses *) -fun build_map mode0 ctxt cls ths = - let val thy = ProofContext.theory_of ctxt - (*The modes FO and FT are sticky. HO can be downgraded to FO.*) - fun set_mode FO = FO - | set_mode HO = - if forall (is_quasi_fol_clause thy) (cls @ ths) then FO else HO - | set_mode FT = FT - val mode = set_mode mode0 - (*transform isabelle clause to metis clause *) - fun add_thm is_conjecture (metis_ith, isa_ith) {axioms, tfrees, skolems} - : logic_map = - let - val (mth, tfree_lits, skolems) = - hol_thm_to_fol is_conjecture ctxt mode (length axioms) skolems - metis_ith - in - {axioms = (mth, Meson.make_meta_clause isa_ith) :: axioms, - tfrees = union (op =) tfree_lits tfrees, skolems = skolems} - end; - val lmap = {axioms = [], tfrees = init_tfrees ctxt, skolems = []} - |> fold (add_thm true o `I) cls - |> add_tfrees - |> fold (add_thm false o `I) ths - val clause_lists = map (Metis_Thm.clause o #1) (#axioms lmap) - fun is_used c = - exists (Metis_LiteralSet.exists (const_in_metis c o #2)) clause_lists - val lmap = - if mode = FO then - lmap - else - let - val helper_ths = - helpers |> filter (is_used o fst) - |> maps (fn (c, (needs_full_types, thms)) => - if not (is_used c) orelse - needs_full_types andalso mode <> FT then - [] - else - thms) - in lmap |> fold (add_thm false) helper_ths end - in (mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap) end - val clause_params = {ordering = Metis_KnuthBendixOrder.default, orderLiterals = Metis_Clause.UnsignedLiteralOrder, @@ -749,20 +50,12 @@ variablesWeight = 0.0, literalsWeight = 0.0, models = []} -val refute_params = {active = active_params, waiting = waiting_params} - -fun refute cls = - Metis_Resolution.new refute_params {axioms = cls, conjecture = []} - |> Metis_Resolution.loop - -fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const); - -fun common_thm ths1 ths2 = exists (member Thm.eq_thm ths1) (map Meson.make_meta_clause ths2); - +val resolution_params = {active = active_params, waiting = waiting_params} (* Main function to start Metis proof and reconstruction *) fun FOL_SOLVE mode ctxt cls ths0 = let val thy = ProofContext.theory_of ctxt + val type_lits = Config.get ctxt type_lits val th_cls_pairs = map (fn th => (Thm.get_name_hint th, Clausifier.cnf_axiom thy th)) ths0 val ths = maps #2 th_cls_pairs @@ -770,7 +63,8 @@ val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls val _ = trace_msg (fn () => "THEOREM CLAUSES") val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) ths - val (mode, {axioms, tfrees, skolems}) = build_map mode ctxt cls ths + val (mode, {axioms, tfrees, skolems}) = + build_logic_map mode ctxt type_lits cls ths val _ = if null tfrees then () else (trace_msg (fn () => "TFREE CLAUSES"); app (fn TyLitFree ((s, _), (s', _)) => @@ -784,21 +78,22 @@ case filter (is_false o prop_of) cls of false_th::_ => [false_th RS @{thm FalseE}] | [] => - case refute thms of + case Metis_Resolution.new resolution_params {axioms = thms, conjecture = []} + |> Metis_Resolution.loop of Metis_Resolution.Contradiction mth => let val _ = trace_msg (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 proof = Metis_Proof.proof mth - val result = fold (translate_one ctxt' mode skolems) proof axioms + val result = fold (replay_one_inference ctxt' mode skolems) proof axioms and used = map_filter (used_axioms axioms) proof val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:") val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used val unused = th_cls_pairs |> map_filter (fn (name, cls) => - if common_thm used cls then NONE else SOME name) + if have_common_thm used cls then NONE else SOME name) in - if not (null cls) andalso not (common_thm used cls) then + if not (null cls) andalso not (have_common_thm used cls) then warning "Metis: The assumptions are inconsistent." else (); diff -r a52a4e4399c1 -r fa16349939b7 src/HOL/Tools/Sledgehammer/metis_translate.ML --- a/src/HOL/Tools/Sledgehammer/metis_translate.ML Thu Sep 16 16:54:42 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_translate.ML Thu Sep 16 17:30:29 2010 +0200 @@ -1,5 +1,7 @@ (* Title: HOL/Tools/Sledgehammer/metis_translate.ML Author: Jia Meng, Cambridge University Computer Laboratory and NICTA + Author: Kong W. Susanto, Cambridge University Computer Laboratory + Author: Lawrence C. Paulson, Cambridge University Computer Laboratory Author: Jasmin Blanchette, TU Muenchen Translation of HOL to FOL for Metis. @@ -28,6 +30,12 @@ CombApp of combterm * combterm datatype fol_literal = FOLLiteral of bool * combterm + datatype mode = FO | HO | FT + type logic_map = + {axioms: (Metis_Thm.thm * thm) list, + tfrees: type_literal list, + skolems: (string * term) list} + val type_wrapper_name : string val bound_var_prefix : string val schematic_var_prefix: string @@ -68,6 +76,10 @@ val tfree_classes_of_terms : term list -> string list val tvar_classes_of_terms : term list -> string list val type_consts_of_terms : theory -> term list -> string list + val string_of_mode : mode -> string + val build_logic_map : + mode -> Proof.context -> bool -> thm list -> thm list + -> mode * logic_map end structure Metis_Translate : METIS_TRANSLATE = @@ -369,23 +381,23 @@ | stripc x = x in stripc(u,[]) end -fun type_of (Type (a, Ts)) = - let val (folTypes,ts) = types_of Ts in +fun combtype_of (Type (a, Ts)) = + let val (folTypes, ts) = combtypes_of Ts in (CombType (`make_fixed_type_const a, folTypes), ts) end - | type_of (tp as TFree (a, _)) = (CombTFree (`make_fixed_type_var a), [tp]) - | type_of (tp as TVar (x, _)) = + | combtype_of (tp as TFree (a, _)) = (CombTFree (`make_fixed_type_var a), [tp]) + | combtype_of (tp as TVar (x, _)) = (CombTVar (make_schematic_type_var x, string_of_indexname x), [tp]) -and types_of Ts = - let val (folTyps, ts) = ListPair.unzip (map type_of Ts) in - (folTyps, union_all ts) - end +and combtypes_of Ts = + let val (folTyps, ts) = ListPair.unzip (map combtype_of Ts) in + (folTyps, union_all ts) + end (* same as above, but no gathering of sort information *) -fun simp_type_of (Type (a, Ts)) = - CombType (`make_fixed_type_const a, map simp_type_of Ts) - | simp_type_of (TFree (a, _)) = CombTFree (`make_fixed_type_var a) - | simp_type_of (TVar (x, _)) = +fun simple_combtype_of (Type (a, Ts)) = + CombType (`make_fixed_type_const a, map simple_combtype_of Ts) + | simple_combtype_of (TFree (a, _)) = CombTFree (`make_fixed_type_var a) + | simple_combtype_of (TVar (x, _)) = CombTVar (make_schematic_type_var x, string_of_indexname x) (* Converts a term (with combinators) into a combterm. Also accummulates sort @@ -396,27 +408,27 @@ in (CombApp (P', Q'), union (op =) tsP tsQ) end | combterm_from_term thy _ (Const (c, T)) = let - val (tp, ts) = type_of T + val (tp, ts) = combtype_of T val tvar_list = (if String.isPrefix skolem_theory_name c then [] |> Term.add_tvarsT T |> map TVar else (c, T) |> Sign.const_typargs thy) - |> map simp_type_of + |> map simple_combtype_of val c' = CombConst (`make_fixed_const c, tp, tvar_list) in (c',ts) end | combterm_from_term _ _ (Free (v, T)) = - let val (tp,ts) = type_of T + let val (tp, ts) = combtype_of T val v' = CombConst (`make_fixed_var v, tp, []) in (v',ts) end | combterm_from_term _ _ (Var (v, T)) = - let val (tp,ts) = type_of T + let val (tp,ts) = combtype_of T val v' = CombVar ((make_schematic_var v, string_of_indexname v), tp) in (v',ts) end | combterm_from_term _ bs (Bound j) = let val (s, T) = nth bs j - val (tp, ts) = type_of T + val (tp, ts) = combtype_of T val v' = CombConst (`make_bound_var s, tp, []) in (v', ts) end | combterm_from_term _ _ (Abs _) = raise Fail "HOL clause: Abs" @@ -518,4 +530,226 @@ fun type_consts_of_terms thy ts = Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty); +(* ------------------------------------------------------------------------- *) +(* HOL to FOL (Isabelle to Metis) *) +(* ------------------------------------------------------------------------- *) + +datatype mode = FO | HO | FT (* first-order, higher-order, fully-typed *) + +fun string_of_mode FO = "FO" + | string_of_mode HO = "HO" + | string_of_mode FT = "FT" + +fun fn_isa_to_met_sublevel "equal" = "=" (* FIXME: "c_fequal" *) + | fn_isa_to_met_sublevel x = x +fun fn_isa_to_met_toplevel "equal" = "=" + | fn_isa_to_met_toplevel x = x + +fun metis_lit b c args = (b, (c, args)); + +fun metis_term_from_combtyp (CombTVar (s, _)) = Metis_Term.Var s + | metis_term_from_combtyp (CombTFree (s, _)) = Metis_Term.Fn (s, []) + | metis_term_from_combtyp (CombType ((s, _), tps)) = + Metis_Term.Fn (s, map metis_term_from_combtyp 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 strip_combterm_comb tm of + (CombConst ((c, _), _, tys), tms) => + let val tyargs = map metis_term_from_combtyp tys + val args = map hol_term_to_fol_FO tms + in Metis_Term.Fn (c, tyargs @ args) end + | (CombVar ((v, _), _), []) => Metis_Term.Var v + | _ => raise Fail "non-first-order combterm" + +fun hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) = + Metis_Term.Fn (fn_isa_to_met_sublevel a, map metis_term_from_combtyp tylist) + | hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis_Term.Var s + | hol_term_to_fol_HO (CombApp (tm1, tm2)) = + Metis_Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]); + +(*The fully-typed translation, to avoid type errors*) +fun wrap_type (tm, ty) = Metis_Term.Fn("ti", [tm, metis_term_from_combtyp ty]); + +fun hol_term_to_fol_FT (CombVar ((s, _), ty)) = wrap_type (Metis_Term.Var s, ty) + | hol_term_to_fol_FT (CombConst((a, _), ty, _)) = + wrap_type (Metis_Term.Fn(fn_isa_to_met_sublevel a, []), ty) + | hol_term_to_fol_FT (tm as CombApp(tm1,tm2)) = + wrap_type (Metis_Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]), + combtyp_of tm) + +fun hol_literal_to_fol FO (FOLLiteral (pos, tm)) = + let val (CombConst((p, _), _, tys), tms) = strip_combterm_comb tm + val tylits = if p = "equal" then [] else map metis_term_from_combtyp tys + val lits = map hol_term_to_fol_FO tms + in metis_lit pos (fn_isa_to_met_toplevel p) (tylits @ lits) end + | hol_literal_to_fol HO (FOLLiteral (pos, tm)) = + (case strip_combterm_comb tm of + (CombConst(("equal", _), _, _), tms) => + metis_lit pos "=" (map hol_term_to_fol_HO tms) + | _ => metis_lit pos "{}" [hol_term_to_fol_HO tm]) (*hBOOL*) + | hol_literal_to_fol FT (FOLLiteral (pos, tm)) = + (case strip_combterm_comb tm of + (CombConst(("equal", _), _, _), tms) => + metis_lit pos "=" (map hol_term_to_fol_FT tms) + | _ => metis_lit pos "{}" [hol_term_to_fol_FT tm]) (*hBOOL*); + +fun literals_of_hol_term thy mode t = + let val (lits, types_sorts) = literals_of_term thy t + in (map (hol_literal_to_fol mode) lits, types_sorts) end; + +(*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*) +fun metis_of_type_literals pos (TyLitVar ((s, _), (s', _))) = + metis_lit pos s [Metis_Term.Var s'] + | metis_of_type_literals pos (TyLitFree ((s, _), (s', _))) = + metis_lit pos s [Metis_Term.Fn (s',[])] + +fun default_sort _ (TVar _) = false + | default_sort ctxt (TFree (x, s)) = (s = the_default [] (Variable.def_sort ctxt (x, ~1))); + +fun metis_of_tfree tf = + Metis_Thm.axiom (Metis_LiteralSet.singleton (metis_of_type_literals true tf)); + +fun hol_thm_to_fol is_conjecture ctxt type_lits mode j skolems th = + let + val thy = ProofContext.theory_of ctxt + val (skolems, (mlits, types_sorts)) = + th |> prop_of |> conceal_skolem_terms j skolems + ||> (HOLogic.dest_Trueprop #> literals_of_hol_term thy mode) + in + if is_conjecture then + (Metis_Thm.axiom (Metis_LiteralSet.fromList mlits), + type_literals_for_types types_sorts, skolems) + else + let + val tylits = filter_out (default_sort ctxt) types_sorts + |> type_literals_for_types + val mtylits = + if type_lits then map (metis_of_type_literals false) tylits else [] + in + (Metis_Thm.axiom (Metis_LiteralSet.fromList(mtylits @ mlits)), [], + skolems) + end + end; + +val helpers = + [("c_COMBI", (false, map (`I) @{thms COMBI_def})), + ("c_COMBK", (false, map (`I) @{thms COMBK_def})), + ("c_COMBB", (false, map (`I) @{thms COMBB_def})), + ("c_COMBC", (false, map (`I) @{thms COMBC_def})), + ("c_COMBS", (false, map (`I) @{thms COMBS_def})), + ("c_fequal", (false, map (rpair @{thm equal_imp_equal}) + @{thms fequal_imp_equal equal_imp_fequal})), + ("c_True", (true, map (`I) @{thms True_or_False})), + ("c_False", (true, map (`I) @{thms True_or_False})), + ("c_If", (true, map (`I) @{thms if_True if_False True_or_False}))] + +(* ------------------------------------------------------------------------- *) +(* Logic maps manage the interface between HOL and first-order logic. *) +(* ------------------------------------------------------------------------- *) + +type logic_map = + {axioms: (Metis_Thm.thm * thm) list, + tfrees: type_literal list, + skolems: (string * term) list} + +fun is_quasi_fol_clause thy = + Meson.is_fol_term thy o snd o conceal_skolem_terms ~1 [] o prop_of + +(*Extract TFree constraints from context to include as conjecture clauses*) +fun init_tfrees ctxt = + let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts in + Vartab.fold add (#2 (Variable.constraints_of ctxt)) [] + |> type_literals_for_types + end; + +(*Insert non-logical axioms corresponding to all accumulated TFrees*) +fun add_tfrees {axioms, tfrees, skolems} : logic_map = + {axioms = map (rpair TrueI o metis_of_tfree) (distinct (op =) tfrees) @ + axioms, + tfrees = tfrees, skolems = skolems} + +(*transform isabelle type / arity clause to metis clause *) +fun add_type_thm [] lmap = lmap + | add_type_thm ((ith, mth) :: cls) {axioms, tfrees, skolems} = + add_type_thm cls {axioms = (mth, ith) :: axioms, tfrees = tfrees, + skolems = skolems} + +fun const_in_metis c (pred, tm_list) = + let + fun in_mterm (Metis_Term.Var _) = 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; + +(* ARITY CLAUSE *) +fun m_arity_cls (TConsLit ((c, _), (t, _), args)) = + metis_lit true c [Metis_Term.Fn(t, map (Metis_Term.Var o fst) args)] + | m_arity_cls (TVarLit ((c, _), (s, _))) = + metis_lit false c [Metis_Term.Var s] +(*TrueI is returned as the Isabelle counterpart because there isn't any.*) +fun arity_cls (ArityClause {conclLit, premLits, ...}) = + (TrueI, + Metis_Thm.axiom (Metis_LiteralSet.fromList (map m_arity_cls (conclLit :: premLits)))); + +(* CLASSREL CLAUSE *) +fun m_class_rel_cls (subclass, _) (superclass, _) = + [metis_lit false subclass [Metis_Term.Var "T"], metis_lit true superclass [Metis_Term.Var "T"]]; +fun class_rel_cls (ClassRelClause {subclass, superclass, ...}) = + (TrueI, Metis_Thm.axiom (Metis_LiteralSet.fromList (m_class_rel_cls subclass superclass))); + +fun type_ext thy tms = + let val subs = tfree_classes_of_terms tms + val supers = tvar_classes_of_terms tms + and tycons = type_consts_of_terms thy tms + val (supers', arity_clauses) = make_arity_clauses thy tycons supers + val class_rel_clauses = make_class_rel_clauses thy subs supers' + in map class_rel_cls class_rel_clauses @ map arity_cls arity_clauses + end; + +(* Function to generate metis clauses, including comb and type clauses *) +fun build_logic_map mode0 ctxt type_lits cls ths = + let val thy = ProofContext.theory_of ctxt + (*The modes FO and FT are sticky. HO can be downgraded to FO.*) + fun set_mode FO = FO + | set_mode HO = + if forall (is_quasi_fol_clause thy) (cls @ ths) then FO else HO + | set_mode FT = FT + val mode = set_mode mode0 + (*transform isabelle clause to metis clause *) + fun add_thm is_conjecture (metis_ith, isa_ith) {axioms, tfrees, skolems} + : logic_map = + let + val (mth, tfree_lits, skolems) = + hol_thm_to_fol is_conjecture ctxt type_lits mode (length axioms) + skolems metis_ith + in + {axioms = (mth, Meson.make_meta_clause isa_ith) :: axioms, + tfrees = union (op =) tfree_lits tfrees, skolems = skolems} + end; + val lmap = {axioms = [], tfrees = init_tfrees ctxt, skolems = []} + |> fold (add_thm true o `I) cls + |> add_tfrees + |> fold (add_thm false o `I) ths + val clause_lists = map (Metis_Thm.clause o #1) (#axioms lmap) + fun is_used c = + exists (Metis_LiteralSet.exists (const_in_metis c o #2)) clause_lists + val lmap = + if mode = FO then + lmap + else + let + val helper_ths = + helpers |> filter (is_used o fst) + |> maps (fn (c, (needs_full_types, thms)) => + if not (is_used c) orelse + needs_full_types andalso mode <> FT then + [] + else + thms) + in lmap |> fold (add_thm false) helper_ths end + in (mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap) end + end;