# HG changeset patch # User blanchet # Date 1286225109 -7200 # Node ID 78faa9b312029a38cc6105ef839ea0a84d3ab3d9 # Parent 277addece9b71cf1a837f34b67eedf68c5c85756 move Metis into Plain diff -r 277addece9b7 -r 78faa9b31202 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Mon Oct 04 22:01:34 2010 +0200 +++ b/src/HOL/IsaMakefile Mon Oct 04 22:45:09 2010 +0200 @@ -155,6 +155,7 @@ Inductive.thy \ Lattices.thy \ Meson.thy \ + Metis.thy \ Nat.thy \ Option.thy \ Orderings.thy \ @@ -204,6 +205,9 @@ Tools/lin_arith.ML \ Tools/Meson/meson.ML \ Tools/Meson/meson_clausify.ML \ + Tools/Metis/metis_reconstruct.ML \ + Tools/Metis/metis_translate.ML \ + Tools/Metis/metis_tactics.ML \ Tools/nat_arith.ML \ Tools/primrec.ML \ Tools/prop_logic.ML \ @@ -222,6 +226,7 @@ $(SRC)/Provers/Arith/fast_lin_arith.ML \ $(SRC)/Provers/order.ML \ $(SRC)/Provers/trancl.ML \ + $(SRC)/Tools/Metis/metis.ML \ $(SRC)/Tools/rat.ML $(OUT)/HOL-Plain: plain.ML $(PLAIN_DEPENDENCIES) @@ -267,7 +272,6 @@ $(SRC)/Provers/Arith/cancel_numerals.ML \ $(SRC)/Provers/Arith/combine_numerals.ML \ $(SRC)/Provers/Arith/extract_common_term.ML \ - $(SRC)/Tools/Metis/metis.ML \ Tools/async_manager.ML \ Tools/ATP/atp_problem.ML \ Tools/ATP/atp_proof.ML \ @@ -317,9 +321,6 @@ Tools/recdef.ML \ Tools/record.ML \ Tools/semiring_normalizer.ML \ - Tools/Sledgehammer/metis_reconstruct.ML \ - Tools/Sledgehammer/metis_translate.ML \ - Tools/Sledgehammer/metis_tactics.ML \ Tools/Sledgehammer/sledgehammer.ML \ Tools/Sledgehammer/sledgehammer_filter.ML \ Tools/Sledgehammer/sledgehammer_minimize.ML \ diff -r 277addece9b7 -r 78faa9b31202 src/HOL/List.thy --- a/src/HOL/List.thy Mon Oct 04 22:01:34 2010 +0200 +++ b/src/HOL/List.thy Mon Oct 04 22:45:09 2010 +0200 @@ -5,7 +5,7 @@ header {* The datatype of finite lists *} theory List -imports Plain Quotient Presburger Code_Numeral Sledgehammer Recdef +imports Plain Quotient Presburger Code_Numeral Recdef uses ("Tools/list_code.ML") begin diff -r 277addece9b7 -r 78faa9b31202 src/HOL/Meson.thy --- a/src/HOL/Meson.thy Mon Oct 04 22:01:34 2010 +0200 +++ b/src/HOL/Meson.thy Mon Oct 04 22:45:09 2010 +0200 @@ -8,7 +8,7 @@ header {* MESON Proof Procedure (Model Elimination) *} theory Meson -imports Nat +imports Datatype uses ("Tools/Meson/meson.ML") ("Tools/Meson/meson_clausify.ML") begin diff -r 277addece9b7 -r 78faa9b31202 src/HOL/Metis.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Metis.thy Mon Oct 04 22:45:09 2010 +0200 @@ -0,0 +1,35 @@ +(* Title: HOL/Metis.thy + Author: Lawrence C. Paulson, Cambridge University Computer Laboratory + Author: Jia Meng, Cambridge University Computer Laboratory and NICTA + Author: Jasmin Blanchette, TU Muenchen +*) + +header {* Metis Proof Method *} + +theory Metis +imports Meson +uses "~~/src/Tools/Metis/metis.ML" + ("Tools/Metis/metis_translate.ML") + ("Tools/Metis/metis_reconstruct.ML") + ("Tools/Metis/metis_tactics.ML") +begin + +definition fequal :: "'a \ 'a \ bool" where [no_atp]: +"fequal X Y \ (X = Y)" + +lemma fequal_imp_equal [no_atp]: "\ fequal X Y \ X = Y" +by (simp add: fequal_def) + +lemma equal_imp_fequal [no_atp]: "\ X = Y \ fequal X Y" +by (simp add: fequal_def) + +lemma equal_imp_equal [no_atp]: "X = Y ==> X = Y" +by auto + +use "Tools/Metis/metis_translate.ML" +use "Tools/Metis/metis_reconstruct.ML" +use "Tools/Metis/metis_tactics.ML" + +setup Metis_Tactics.setup + +end diff -r 277addece9b7 -r 78faa9b31202 src/HOL/Plain.thy --- a/src/HOL/Plain.thy Mon Oct 04 22:01:34 2010 +0200 +++ b/src/HOL/Plain.thy Mon Oct 04 22:45:09 2010 +0200 @@ -1,7 +1,7 @@ header {* Plain HOL *} theory Plain -imports Datatype FunDef Extraction Meson +imports Datatype FunDef Extraction Metis begin text {* diff -r 277addece9b7 -r 78faa9b31202 src/HOL/Quotient.thy --- a/src/HOL/Quotient.thy Mon Oct 04 22:01:34 2010 +0200 +++ b/src/HOL/Quotient.thy Mon Oct 04 22:45:09 2010 +0200 @@ -5,7 +5,7 @@ header {* Definition of Quotient Types *} theory Quotient -imports Plain Sledgehammer +imports Plain Hilbert_Choice uses ("Tools/Quotient/quotient_info.ML") ("Tools/Quotient/quotient_typ.ML") diff -r 277addece9b7 -r 78faa9b31202 src/HOL/Refute.thy --- a/src/HOL/Refute.thy Mon Oct 04 22:01:34 2010 +0200 +++ b/src/HOL/Refute.thy Mon Oct 04 22:45:09 2010 +0200 @@ -8,7 +8,7 @@ header {* Refute *} theory Refute -imports Hilbert_Choice List +imports Hilbert_Choice List Sledgehammer uses "Tools/refute.ML" begin diff -r 277addece9b7 -r 78faa9b31202 src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Mon Oct 04 22:01:34 2010 +0200 +++ b/src/HOL/Sledgehammer.thy Mon Oct 04 22:45:09 2010 +0200 @@ -8,15 +8,11 @@ header {* Sledgehammer: Isabelle--ATP Linkup *} theory Sledgehammer -imports Plain Hilbert_Choice +imports Plain uses ("Tools/ATP/atp_problem.ML") ("Tools/ATP/atp_proof.ML") ("Tools/ATP/atp_systems.ML") - ("~~/src/Tools/Metis/metis.ML") - ("Tools/Sledgehammer/metis_translate.ML") - ("Tools/Sledgehammer/metis_reconstruct.ML") - ("Tools/Sledgehammer/metis_tactics.ML") ("Tools/Sledgehammer/sledgehammer_util.ML") ("Tools/Sledgehammer/sledgehammer_filter.ML") ("Tools/Sledgehammer/sledgehammer_translate.ML") @@ -26,88 +22,11 @@ ("Tools/Sledgehammer/sledgehammer_isar.ML") begin -lemma TruepropI: "P \ Q \ Trueprop P \ Trueprop Q" -by simp - -definition skolem :: "'a \ 'a" where -[no_atp]: "skolem = (\x. x)" - -definition COMBI :: "'a \ 'a" where -[no_atp]: "COMBI P = P" - -definition COMBK :: "'a \ 'b \ 'a" where -[no_atp]: "COMBK P Q = P" - -definition COMBB :: "('b => 'c) \ ('a => 'b) \ 'a \ 'c" where [no_atp]: -"COMBB P Q R = P (Q R)" - -definition COMBC :: "('a \ 'b \ 'c) \ 'b \ 'a \ 'c" where -[no_atp]: "COMBC P Q R = P R Q" - -definition COMBS :: "('a \ 'b \ 'c) \ ('a \ 'b) \ 'a \ 'c" where -[no_atp]: "COMBS P Q R = P R (Q R)" - -definition fequal :: "'a \ 'a \ bool" where [no_atp]: -"fequal X Y \ (X = Y)" - -lemma fequal_imp_equal [no_atp]: "\ fequal X Y \ X = Y" -by (simp add: fequal_def) - -lemma equal_imp_fequal [no_atp]: "\ X = Y \ fequal X Y" -by (simp add: fequal_def) - -lemma equal_imp_equal [no_atp]: "X = Y ==> X = Y" -by auto - -lemma skolem_COMBK_iff: "P \ skolem (COMBK P (i\nat))" -unfolding skolem_def COMBK_def by (rule refl) - -lemmas skolem_COMBK_I = iffD1 [OF skolem_COMBK_iff] -lemmas skolem_COMBK_D = iffD2 [OF skolem_COMBK_iff] - -text{*Theorems for translation to combinators*} - -lemma abs_S [no_atp]: "\x. (f x) (g x) \ COMBS f g" -apply (rule eq_reflection) -apply (rule ext) -apply (simp add: COMBS_def) -done - -lemma abs_I [no_atp]: "\x. x \ COMBI" -apply (rule eq_reflection) -apply (rule ext) -apply (simp add: COMBI_def) -done - -lemma abs_K [no_atp]: "\x. y \ COMBK y" -apply (rule eq_reflection) -apply (rule ext) -apply (simp add: COMBK_def) -done - -lemma abs_B [no_atp]: "\x. a (g x) \ COMBB a g" -apply (rule eq_reflection) -apply (rule ext) -apply (simp add: COMBB_def) -done - -lemma abs_C [no_atp]: "\x. (f x) b \ COMBC f b" -apply (rule eq_reflection) -apply (rule ext) -apply (simp add: COMBC_def) -done - use "Tools/ATP/atp_problem.ML" use "Tools/ATP/atp_proof.ML" use "Tools/ATP/atp_systems.ML" setup ATP_Systems.setup -use "~~/src/Tools/Metis/metis.ML" -use "Tools/Sledgehammer/metis_translate.ML" -use "Tools/Sledgehammer/metis_reconstruct.ML" -use "Tools/Sledgehammer/metis_tactics.ML" -setup Metis_Tactics.setup - use "Tools/Sledgehammer/sledgehammer_util.ML" use "Tools/Sledgehammer/sledgehammer_filter.ML" use "Tools/Sledgehammer/sledgehammer_translate.ML" diff -r 277addece9b7 -r 78faa9b31202 src/HOL/Tools/Metis/metis_reconstruct.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Mon Oct 04 22:45:09 2010 +0200 @@ -0,0 +1,557 @@ +(* Title: HOL/Tools/Sledgehammer/metis_reconstruct.ML + Author: Kong W. Susanto, Cambridge University Computer Laboratory + Author: Lawrence C. Paulson, Cambridge University Computer Laboratory + Author: Jasmin Blanchette, TU Muenchen + Copyright Cambridge University 2007 + +Proof reconstruction for Metis. +*) + +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 untyped_aconv : term -> term -> bool + 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 = SomeTerm of term | SomeType of typ + +fun terms_of [] = [] + | terms_of (SomeTerm t :: tts) = t :: terms_of tts + | terms_of (SomeType _ :: tts) = terms_of tts; + +fun types_of [] = [] + | types_of (SomeTerm (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 (SomeTerm _ :: tts) = types_of tts + | types_of (SomeType T :: tts) = T :: types_of tts; + +fun apply_list rator nargs rands = + let val trands = terms_of rands + in if length trands = nargs then SomeTerm (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) = 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 => 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 => SomeType (make_tvar w) + | NONE => + case strip_prefix_and_unascii schematic_var_prefix v of + SOME w => SomeTerm (mk_var (w, HOLogic.typeT)) + | NONE => SomeTerm (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 + SomeTerm t => SomeTerm (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) = + SomeTerm (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)) + val t = + if String.isPrefix new_skolem_const_prefix c then + Var (new_skolem_var_from_const c, + Type_Infer.paramify_vars (tl tys ---> hd tys)) + else + Const (c, dummyT) + in if length tys = ntypes then + apply_list t 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 => + SomeType (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 => SomeType (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 = 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 + SomeTerm t => t + | SomeType T => raise TYPE ("fol_tm_to_tt: Term expected", [T], []) + 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 old_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_old_skolem_terms old_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 old_skolems atm = + inst_excluded_middle + (ProofContext.theory_of ctxt) + (singleton (hol_terms_from_fol ctxt mode old_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 old_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_old_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.Option => + (trace_msg (fn () => "\"find_var\" failed for " ^ x ^ + " in " ^ Display.string_of_thm ctxt i_th); + NONE) + | TYPE _ => + (trace_msg (fn () => "\"hol_term_from_metis\" failed for " ^ 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_old_skolem_terms old_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 + +(* Permute a rule's premises to move the i-th premise to the last position. *) +fun make_last i th = + let val n = nprems_of th + in if 1 <= i andalso i <= n + then Thm.permute_prems (i-1) 1 th + else raise THM("select_literal", i, [th]) + end; + +(* Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing + double-negations. *) +val negate_head = rewrite_rule [@{thm atomize_not}, not_not RS eq_reflection] + +(* Maps the clause [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *) +val select_literal = negate_head oo make_last + +fun resolve_inf ctxt mode old_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 old_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 (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 old_skolems t = + let val thy = ProofContext.theory_of ctxt + val i_t = singleton (hol_terms_from_fol ctxt mode old_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 old_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 old_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, 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, 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 ("Cannot replay Metis proof in Isabelle:\n" ^ + "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, 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 ("Cannot replay Metis proof in Isabelle:\n" ^ + "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 = 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 old_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 old_skolems f_atm + | (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) => + factor (inst_inf ctxt mode old_skolems thpairs f_subst f_th1) + | (_, Metis_Proof.Resolve(f_atm, f_th1, f_th2)) => + factor (resolve_inf ctxt mode old_skolems thpairs f_atm f_th1 f_th2) + | (_, Metis_Proof.Refl f_tm) => refl_inf ctxt mode old_skolems f_tm + | (_, Metis_Proof.Equality (f_lit, f_p, f_r)) => + equality_inf ctxt mode old_skolems f_lit f_p f_r + +fun flexflex_first_order th = + case Thm.tpairs_of th of + [] => th + | pairs => + let val thy = theory_of_thm th + val (_, tenv) = + fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty) + val t_pairs = map Meson.term_pair_of (Vartab.dest tenv) + val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th + in th' end + handle THM _ => th; + +fun is_metis_literal_genuine (_, (s, _)) = not (String.isPrefix class_prefix s) +fun is_isabelle_literal_genuine t = + case t of _ $ (Const (@{const_name skolem}, _) $ _) => false | _ => true + +fun count p xs = fold (fn x => if p x then Integer.add 1 else I) xs 0 + +fun replay_one_inference ctxt mode old_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 = step ctxt mode old_skolems thpairs (fol_th, inf) + |> flexflex_first_order + val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th) + val _ = trace_msg (fn () => "=============================================") + val num_metis_lits = + fol_th |> Metis_Thm.clause |> Metis_LiteralSet.toList + |> count is_metis_literal_genuine + val num_isabelle_lits = + th |> prems_of |> count is_isabelle_literal_genuine + val _ = if num_metis_lits = num_isabelle_lits then () + else error "Cannot replay Metis proof in Isabelle: Out of sync." + in (fol_th, th) :: thpairs end + +end; diff -r 277addece9b7 -r 78faa9b31202 src/HOL/Tools/Metis/metis_tactics.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Metis/metis_tactics.ML Mon Oct 04 22:45:09 2010 +0200 @@ -0,0 +1,449 @@ +(* Title: HOL/Tools/Sledgehammer/metis_tactics.ML + Author: Kong W. Susanto, Cambridge University Computer Laboratory + Author: Lawrence C. Paulson, Cambridge University Computer Laboratory + Author: Jasmin Blanchette, TU Muenchen + Copyright Cambridge University 2007 + +HOL setup for the Metis prover. +*) + +signature METIS_TACTICS = +sig + val trace : bool Unsynchronized.ref + val type_lits : bool Config.T + val new_skolemizer : 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 + +structure Int_Pair_Graph = + Graph(type key = int * int val ord = prod_ord int_ord int_ord) + +fun trace_msg msg = if !trace then tracing (msg ()) else () + +val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" (K true) +val (new_skolemizer, new_skolemizer_setup) = + Attrib.config_bool "metis_new_skolemizer" (K false) + +fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const); + +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; + +val clause_params = + {ordering = Metis_KnuthBendixOrder.default, + orderLiterals = Metis_Clause.UnsignedLiteralOrder, + orderTerms = true} +val active_params = + {clause = clause_params, + prefactor = #prefactor Metis_Active.default, + postfactor = #postfactor Metis_Active.default} +val waiting_params = + {symbolsWeight = 1.0, + variablesWeight = 0.0, + literalsWeight = 0.0, + models = []} +val resolution_params = {active = active_params, waiting = waiting_params} + +fun instantiate_theorem thy inst th = + let + val tyenv = Vartab.empty |> fold (Type.raw_unify o pairself fastype_of) inst + val instT = + [] |> Vartab.fold (fn (z, (S, T)) => + cons (TVar (z, S), Type.devar tyenv T)) tyenv + val inst = inst |> map (pairself (subst_atomic_types instT)) + val _ = tracing (cat_lines (map (fn (T, U) => + Syntax.string_of_typ @{context} T ^ " |-> " ^ + Syntax.string_of_typ @{context} U) instT)) + val _ = tracing (cat_lines (map (fn (t, u) => + Syntax.string_of_term @{context} t ^ " |-> " ^ + Syntax.string_of_term @{context} u) inst)) + val cinstT = instT |> map (pairself (ctyp_of thy)) + val cinst = inst |> map (pairself (cterm_of thy)) + in th |> Thm.instantiate (cinstT, cinst) end + +(* In principle, it should be sufficient to apply "assume_tac" to unify the + conclusion with one of the premises. However, in practice, this is unreliable + because of the mildly higher-order nature of the unification problems. + Typical constraints are of the form + "?SK_a_b_c_x SK_d_e_f_y ... SK_a_b_c_x ... SK_g_h_i_z =?= SK_a_b_c_x", + where the nonvariables are goal parameters. *) +fun unify_first_prem_with_concl thy i th = + let + val goal = Logic.get_goal (prop_of th) i |> Envir.beta_eta_contract + val prem = goal |> Logic.strip_assums_hyp |> hd + val concl = goal |> Logic.strip_assums_concl + fun pair_untyped_aconv (t1, t2) (u1, u2) = + untyped_aconv t1 u1 andalso untyped_aconv t2 u2 + fun add_terms tp inst = + if exists (pair_untyped_aconv tp) inst then inst + else tp :: map (apsnd (subst_atomic [tp])) inst + fun is_flex t = + case strip_comb t of + (Var _, args) => forall is_Bound args + | _ => false + fun unify_flex flex rigid = + case strip_comb flex of + (Var (z as (_, T)), args) => + add_terms (Var z, + fold_rev (curry absdummy) (take (length args) (binder_types T)) rigid) + | _ => raise TERM ("unify_flex: expected flex", [flex]) + fun unify_potential_flex comb atom = + if is_flex comb then unify_flex comb atom + else if is_Var atom then add_terms (atom, comb) + else raise TERM ("unify_terms", [comb, atom]) + fun unify_terms (t, u) = + case (t, u) of + (t1 $ t2, u1 $ u2) => + if is_flex t then unify_flex t u + else if is_flex u then unify_flex u t + else fold unify_terms [(t1, u1), (t2, u2)] + | (_ $ _, _) => unify_potential_flex t u + | (_, _ $ _) => unify_potential_flex u t + | (Var _, _) => add_terms (t, u) + | (_, Var _) => add_terms (u, t) + | _ => if untyped_aconv t u then I else raise TERM ("unify_terms", [t, u]) + in th |> instantiate_theorem thy (unify_terms (prem, concl) []) end + +fun shuffle_key (((axiom_no, (_, index_no)), _), _) = (index_no, axiom_no) +fun shuffle_ord p = + rev_order (prod_ord int_ord int_ord (pairself shuffle_key p)) + +val copy_prem = @{lemma "P ==> (P ==> P ==> Q) ==> Q" by fast} + +fun copy_prems_tac [] ns i = + if forall (curry (op =) 1) ns then all_tac else copy_prems_tac (rev ns) [] i + | copy_prems_tac (1 :: ms) ns i = + rotate_tac 1 i THEN copy_prems_tac ms (1 :: ns) i + | copy_prems_tac (m :: ms) ns i = + etac copy_prem i THEN copy_prems_tac ms (m div 2 :: (m + 1) div 2 :: ns) i + +fun instantiate_forall_tac thy params t i = + let + fun repair (t as (Var ((s, _), _))) = + (case find_index (fn ((s', _), _) => s' = s) params of + ~1 => t + | j => Bound j) + | repair (t $ u) = repair t $ repair u + | repair t = t + val t' = t |> repair |> fold (curry absdummy) (map snd params) + fun do_instantiate th = + let val var = Term.add_vars (prop_of th) [] |> the_single in + th |> instantiate_theorem thy [(Var var, t')] + end + in + etac @{thm allE} i + THEN rotate_tac ~1 i + THEN PRIMITIVE do_instantiate + end + +fun release_clusters_tac _ _ _ _ [] = K all_tac + | release_clusters_tac thy ax_counts substs params + ((ax_no, cluster_no) :: clusters) = + let + fun in_right_cluster s = + (s |> Meson_Clausify.cluster_of_zapped_var_name |> fst |> snd |> fst) + = cluster_no + val cluster_substs = + substs + |> map_filter (fn (ax_no', (_, (_, tsubst))) => + if ax_no' = ax_no then + tsubst |> filter (in_right_cluster + o fst o fst o dest_Var o fst) + |> map snd |> SOME + else + NONE) + val n = length cluster_substs + fun do_cluster_subst cluster_subst = + map (instantiate_forall_tac thy params) cluster_subst @ [rotate_tac 1] + val params' = params (* FIXME ### existentials! *) + val first_prem = find_index (fn (ax_no', _) => ax_no' = ax_no) substs + in + rotate_tac first_prem + THEN' (EVERY' (maps do_cluster_subst cluster_substs)) + THEN' rotate_tac (~ first_prem - length cluster_substs) + THEN' release_clusters_tac thy ax_counts substs params' clusters + end + +val cluster_ord = + prod_ord (prod_ord int_ord (prod_ord int_ord int_ord)) bool_ord + +val tysubst_ord = + list_ord (prod_ord Term_Ord.fast_indexname_ord + (prod_ord Term_Ord.sort_ord Term_Ord.typ_ord)) + +structure Int_Tysubst_Table = + Table(type key = int * (indexname * (sort * typ)) list + val ord = prod_ord int_ord tysubst_ord) + +(* Attempts to derive the theorem "False" from a theorem of the form + "P1 ==> ... ==> Pn ==> False", where the "Pi"s are to be discharged using the + specified axioms. The axioms have leading "All" and "Ex" quantifiers, which + must be eliminated first. *) +fun discharge_skolem_premises ctxt axioms prems_imp_false = + if prop_of prems_imp_false aconv @{prop False} then + prems_imp_false + else + let + val thy = ProofContext.theory_of ctxt + (* distinguish variables with same name but different types *) + val prems_imp_false' = + prems_imp_false |> try (forall_intr_vars #> gen_all) + |> the_default prems_imp_false + val prems_imp_false = + if prop_of prems_imp_false aconv prop_of prems_imp_false' then + prems_imp_false + else + prems_imp_false' + fun match_term p = + let + val (tyenv, tenv) = + Pattern.first_order_match thy p (Vartab.empty, Vartab.empty) + val tsubst = + tenv |> Vartab.dest + |> sort (cluster_ord + o pairself (Meson_Clausify.cluster_of_zapped_var_name + o fst o fst)) + |> map (Meson.term_pair_of + #> pairself (Envir.subst_term_types tyenv)) + val tysubst = tyenv |> Vartab.dest + in (tysubst, tsubst) end + fun subst_info_for_prem subgoal_no prem = + case prem of + _ $ (Const (@{const_name skolem}, _) $ (_ $ t $ num)) => + let val ax_no = HOLogic.dest_nat num in + (ax_no, (subgoal_no, + match_term (nth axioms ax_no |> the |> snd, t))) + end + | _ => raise TERM ("discharge_skolem_premises: Malformed premise", + [prem]) + fun cluster_of_var_name skolem s = + let + val ((ax_no, (cluster_no, _)), skolem') = + Meson_Clausify.cluster_of_zapped_var_name s + in + if skolem' = skolem andalso cluster_no > 0 then + SOME (ax_no, cluster_no) + else + NONE + end + fun clusters_in_term skolem t = + Term.add_var_names t [] |> map_filter (cluster_of_var_name skolem o fst) + fun deps_for_term_subst (var, t) = + case clusters_in_term false var of + [] => NONE + | [(ax_no, cluster_no)] => + SOME ((ax_no, cluster_no), + clusters_in_term true t + |> cluster_no > 1 ? cons (ax_no, cluster_no - 1)) + | _ => raise TERM ("discharge_skolem_premises: Expected Var", [var]) + val prems = Logic.strip_imp_prems (prop_of prems_imp_false) + val substs = prems |> map2 subst_info_for_prem (1 upto length prems) + |> sort (int_ord o pairself fst) + val depss = maps (map_filter deps_for_term_subst o snd o snd o snd) substs + val clusters = maps (op ::) depss + val ordered_clusters = + Int_Pair_Graph.empty + |> fold Int_Pair_Graph.default_node (map (rpair ()) clusters) + |> fold Int_Pair_Graph.add_deps_acyclic depss + |> Int_Pair_Graph.topological_order + handle Int_Pair_Graph.CYCLES _ => + error "Cannot replay Metis proof in Isabelle without axiom of \ + \choice." + val params0 = + [] |> fold (Term.add_vars o snd) (map_filter I axioms) + |> map (`(Meson_Clausify.cluster_of_zapped_var_name o fst o fst)) + |> filter (fn (((_, (cluster_no, _)), skolem), _) => + cluster_no = 0 andalso skolem) + |> sort shuffle_ord |> map snd + val ax_counts = + Int_Tysubst_Table.empty + |> fold (fn (ax_no, (_, (tysubst, _))) => + Int_Tysubst_Table.map_default ((ax_no, tysubst), 0) + (Integer.add 1)) substs + |> Int_Tysubst_Table.dest +(* for debugging: + fun string_for_subst_info (ax_no, (subgoal_no, (tysubst, tsubst))) = + "ax: " ^ string_of_int ax_no ^ "; asm: " ^ string_of_int subgoal_no ^ + "; tysubst: " ^ PolyML.makestring tysubst ^ "; tsubst: {" ^ + commas (map ((fn (s, t) => s ^ " |-> " ^ t) + o pairself (Syntax.string_of_term ctxt)) tsubst) ^ "}" + val _ = tracing ("SUBSTS (" ^ string_of_int (length substs) ^ "):\n" ^ + cat_lines (map string_for_subst_info substs)) + val _ = tracing ("OUTERMOST SKOLEMS: " ^ PolyML.makestring params0) + val _ = tracing ("ORDERED CLUSTERS: " ^ PolyML.makestring ordered_clusters) + val _ = tracing ("AXIOM COUNTS: " ^ PolyML.makestring ax_counts) +*) + fun rotation_for_subgoal i = + find_index (fn (_, (subgoal_no, _)) => subgoal_no = i) substs + in + Goal.prove ctxt [] [] @{prop False} + (K (cut_rules_tac + (map (fst o the o nth axioms o fst o fst) ax_counts) 1 + THEN print_tac "cut:" + THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1) + THEN copy_prems_tac (map snd ax_counts) [] 1 + THEN print_tac "eliminated exist and copied prems:" + THEN release_clusters_tac thy ax_counts substs params0 + ordered_clusters 1 + THEN print_tac "released clusters:" + THEN match_tac [prems_imp_false] 1 + THEN print_tac "applied rule:" + THEN ALLGOALS (fn i => + rtac @{thm skolem_COMBK_I} i + THEN rotate_tac (rotation_for_subgoal i) i + THEN PRIMITIVE (unify_first_prem_with_concl thy i) + THEN assume_tac i))) + end + +(* 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 new_skolemizer = + Config.get ctxt new_skolemizer orelse null (Meson_Choices.get ctxt) + val th_cls_pairs = + map2 (fn j => fn th => + (Thm.get_name_hint th, + Meson_Clausify.cnf_axiom ctxt new_skolemizer j th)) + (0 upto length ths0 - 1) ths0 + val thss = map (snd o snd) th_cls_pairs + val dischargers = map (fst o snd) th_cls_pairs + val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES") + val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls + val _ = trace_msg (fn () => "THEOREM CLAUSES") + val _ = app (app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th))) thss + val (mode, {axioms, tfrees, old_skolems}) = + build_logic_map mode ctxt type_lits cls thss + val _ = if null tfrees then () + else (trace_msg (fn () => "TFREE CLAUSES"); + app (fn TyLitFree ((s, _), (s', _)) => + trace_msg (fn () => s ^ "(" ^ s' ^ ")")) tfrees) + val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS") + val thms = map #1 axioms + val _ = app (fn th => trace_msg (fn () => Metis_Thm.toString th)) thms + val _ = trace_msg (fn () => "mode = " ^ string_of_mode mode) + val _ = trace_msg (fn () => "START METIS PROVE PROCESS") + in + case filter (is_false o prop_of) cls of + false_th::_ => [false_th RS @{thm FalseE}] + | [] => + 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 (replay_one_inference ctxt' mode old_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 have_common_thm used cls then NONE else SOME name) + in + if not (null cls) andalso not (have_common_thm used cls) then + warning "Metis: The assumptions are inconsistent." + else + (); + if not (null unused) then + warning ("Metis: Unused theorems: " ^ commas_quote unused + ^ ".") + else + (); + case result of + (_,ith)::_ => + (trace_msg (fn () => "Success: " ^ Display.string_of_thm ctxt ith); + [discharge_skolem_premises ctxt dischargers ith]) + | _ => (trace_msg (fn () => "Metis: No result"); []) + end + | Metis_Resolution.Satisfiable _ => + (trace_msg (fn () => "Metis: No first-order proof with the lemmas supplied"); + []) + end; + +(* Extensionalize "th", because that makes sense and that's what Sledgehammer + does, but also keep an unextensionalized version of "th" for backward + compatibility. *) +fun also_extensionalize_theorem th = + let val th' = Meson_Clausify.extensionalize_theorem th in + if Thm.eq_thm (th, th') then [th] + else th :: Meson.make_clauses_unsorted [th'] + end + +val neg_clausify = + single + #> Meson.make_clauses_unsorted + #> maps also_extensionalize_theorem + #> map Meson_Clausify.introduce_combinators_in_theorem + #> Meson.finish_cnf + +fun preskolem_tac ctxt st0 = + (if exists (Meson.has_too_many_clauses ctxt) + (Logic.prems_of_goal (prop_of st0) 1) then + cnf.cnfx_rewrite_tac ctxt 1 + else + all_tac) st0 + +val type_has_top_sort = + exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false) + +fun generic_metis_tac mode ctxt ths i st0 = + let + val _ = trace_msg (fn () => + "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths)) + in + if exists_type type_has_top_sort (prop_of st0) then + (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty) + else + Meson.MESON (preskolem_tac ctxt) (maps neg_clausify) + (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) + ctxt i st0 + end + +val metis_tac = generic_metis_tac HO +val metisF_tac = generic_metis_tac FO +val metisFT_tac = generic_metis_tac FT + +(* Whenever "X" has schematic type variables, we treat "using X by metis" as + "by (metis X)", to prevent "Subgoal.FOCUS" from freezing the type variables. + We don't do it for nonschematic facts "X" because this breaks a few proofs + (in the rare and subtle case where a proof relied on extensionality not being + applied) and brings few benefits. *) +val has_tvar = + exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of +fun method name mode = + Method.setup name (Attrib.thms >> (fn ths => fn ctxt => + METHOD (fn facts => + let + val (schem_facts, nonschem_facts) = + List.partition has_tvar facts + in + HEADGOAL (Method.insert_tac nonschem_facts THEN' + CHANGED_PROP + o generic_metis_tac mode ctxt (schem_facts @ ths)) + end))) + +val setup = + type_lits_setup + #> new_skolemizer_setup + #> method @{binding metis} HO "Metis for FOL/HOL problems" + #> method @{binding metisF} FO "Metis for FOL problems" + #> method @{binding metisFT} FT + "Metis for FOL/HOL problems with fully-typed translation" + +end; diff -r 277addece9b7 -r 78faa9b31202 src/HOL/Tools/Metis/metis_translate.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Metis/metis_translate.ML Mon Oct 04 22:45:09 2010 +0200 @@ -0,0 +1,771 @@ +(* 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. +*) + +signature METIS_TRANSLATE = +sig + type name = string * string + datatype type_literal = + TyLitVar of name * name | + TyLitFree of name * name + datatype arLit = + TConsLit of name * name * name list | + TVarLit of name * name + datatype arity_clause = + ArityClause of {name: string, conclLit: arLit, premLits: arLit list} + datatype class_rel_clause = + ClassRelClause of {name: string, subclass: name, superclass: name} + datatype combtyp = + CombTVar of name | + CombTFree of name | + CombType of name * combtyp list + datatype combterm = + CombConst of name * combtyp * combtyp list (* Const and Free *) | + CombVar of name * combtyp | + 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, + old_skolems: (string * term) list} + + val type_wrapper_name : string + val bound_var_prefix : string + val schematic_var_prefix: string + val fixed_var_prefix: string + val tvar_prefix: string + val tfree_prefix: string + val const_prefix: string + val type_const_prefix: string + val class_prefix: string + val new_skolem_const_prefix : string + val invert_const: string -> string + val ascii_of: string -> string + val unascii_of: string -> string + val strip_prefix_and_unascii: string -> string -> string option + val make_bound_var : string -> string + val make_schematic_var : string * int -> string + val make_fixed_var : string -> string + val make_schematic_type_var : string * int -> string + val make_fixed_type_var : string -> string + val make_fixed_const : string -> string + val make_fixed_type_const : string -> string + val make_type_class : string -> string + val num_type_args: theory -> string -> int + val new_skolem_var_from_const: string -> indexname + val type_literals_for_types : typ list -> type_literal list + val make_class_rel_clauses : + theory -> class list -> class list -> class_rel_clause list + val make_arity_clauses : + theory -> string list -> class list -> class list * arity_clause list + val combtyp_of : combterm -> combtyp + val strip_combterm_comb : combterm -> combterm * combterm list + val combterm_from_term : + theory -> int -> (string * typ) list -> term -> combterm * typ list + val reveal_old_skolem_terms : (string * term) list -> term -> term + 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 list + -> mode * logic_map +end + +structure Metis_Translate : METIS_TRANSLATE = +struct + +val type_wrapper_name = "ti" + +val bound_var_prefix = "B_" +val schematic_var_prefix = "V_" +val fixed_var_prefix = "v_" + +val tvar_prefix = "T_"; +val tfree_prefix = "t_"; + +val const_prefix = "c_"; +val type_const_prefix = "tc_"; +val class_prefix = "class_"; + +val skolem_const_prefix = "Sledgehammer" ^ Long_Name.separator ^ "Sko" +val old_skolem_const_prefix = skolem_const_prefix ^ "o" +val new_skolem_const_prefix = skolem_const_prefix ^ "n" + +fun union_all xss = fold (union (op =)) xss [] + +(* Readable names for the more common symbolic functions. Do not mess with the + last nine entries of the table unless you know what you are doing. *) +val const_trans_table = + Symtab.make [(@{type_name Product_Type.prod}, "prod"), + (@{type_name Sum_Type.sum}, "sum"), + (@{const_name HOL.eq}, "equal"), + (@{const_name HOL.conj}, "and"), + (@{const_name HOL.disj}, "or"), + (@{const_name HOL.implies}, "implies"), + (@{const_name Set.member}, "member"), + (@{const_name fequal}, "fequal"), + (@{const_name COMBI}, "COMBI"), + (@{const_name COMBK}, "COMBK"), + (@{const_name COMBB}, "COMBB"), + (@{const_name COMBC}, "COMBC"), + (@{const_name COMBS}, "COMBS"), + (@{const_name True}, "True"), + (@{const_name False}, "False"), + (@{const_name If}, "If")] + +(* Invert the table of translations between Isabelle and ATPs. *) +val const_trans_table_inv = + Symtab.update ("fequal", @{const_name HOL.eq}) + (Symtab.make (map swap (Symtab.dest const_trans_table))) + +val invert_const = perhaps (Symtab.lookup const_trans_table_inv) + +(*Escaping of special characters. + Alphanumeric characters are left unchanged. + The character _ goes to __ + Characters in the range ASCII space to / go to _A to _P, respectively. + Other characters go to _nnn where nnn is the decimal ASCII code.*) +val A_minus_space = Char.ord #"A" - Char.ord #" "; + +fun stringN_of_int 0 _ = "" + | stringN_of_int k n = stringN_of_int (k-1) (n div 10) ^ Int.toString (n mod 10); + +fun ascii_of_c c = + if Char.isAlphaNum c then String.str c + else if c = #"_" then "__" + else if #" " <= c andalso c <= #"/" + then "_" ^ String.str (Char.chr (Char.ord c + A_minus_space)) + else ("_" ^ stringN_of_int 3 (Char.ord c)) (*fixed width, in case more digits follow*) + +val ascii_of = String.translate ascii_of_c; + +(** Remove ASCII armouring from names in proof files **) + +(*We don't raise error exceptions because this code can run inside the watcher. + Also, the errors are "impossible" (hah!)*) +fun unascii_aux rcs [] = String.implode(rev rcs) + | unascii_aux rcs [#"_"] = unascii_aux (#"_"::rcs) [] (*ERROR*) + (*Three types of _ escapes: __, _A to _P, _nnn*) + | unascii_aux rcs (#"_" :: #"_" :: cs) = unascii_aux (#"_"::rcs) cs + | unascii_aux rcs (#"_" :: c :: cs) = + if #"A" <= c andalso c<= #"P" (*translation of #" " to #"/"*) + then unascii_aux (Char.chr(Char.ord c - A_minus_space) :: rcs) cs + else + let val digits = List.take (c::cs, 3) handle Subscript => [] + in + case Int.fromString (String.implode digits) of + NONE => unascii_aux (c:: #"_"::rcs) cs (*ERROR*) + | SOME n => unascii_aux (Char.chr n :: rcs) (List.drop (cs, 2)) + end + | unascii_aux rcs (c::cs) = unascii_aux (c::rcs) cs +val unascii_of = unascii_aux [] o String.explode + +(* If string s has the prefix s1, return the result of deleting it, + un-ASCII'd. *) +fun strip_prefix_and_unascii s1 s = + if String.isPrefix s1 s then + SOME (unascii_of (String.extract (s, size s1, NONE))) + else + NONE + +(*Remove the initial ' character from a type variable, if it is present*) +fun trim_type_var s = + if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE) + else error ("trim_type: Malformed type variable encountered: " ^ s); + +fun ascii_of_indexname (v,0) = ascii_of v + | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ Int.toString i; + +fun make_bound_var x = bound_var_prefix ^ ascii_of x +fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v +fun make_fixed_var x = fixed_var_prefix ^ ascii_of x + +fun make_schematic_type_var (x,i) = + tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i)); +fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x)); + +fun lookup_const c = + case Symtab.lookup const_trans_table c of + SOME c' => c' + | NONE => ascii_of c + +(* HOL.eq MUST BE "equal" because it's built into ATPs. *) +fun make_fixed_const @{const_name HOL.eq} = "equal" + | make_fixed_const c = const_prefix ^ lookup_const c + +fun make_fixed_type_const c = type_const_prefix ^ lookup_const c + +fun make_type_class clas = class_prefix ^ ascii_of clas; + +(* The number of type arguments of a constant, zero if it's monomorphic. For + (instances of) Skolem pseudoconstants, this information is encoded in the + constant name. *) +fun num_type_args thy s = + if String.isPrefix skolem_const_prefix s then + s |> space_explode Long_Name.separator |> List.last |> Int.fromString |> the + else + (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length + +fun new_skolem_var_from_const s = + let + val ss = s |> space_explode Long_Name.separator + val n = length ss + in (nth ss (n - 2), nth ss (n - 3) |> Int.fromString |> the) end + + +(**** Definitions and functions for FOL clauses for TPTP format output ****) + +type name = string * string + +(**** Isabelle FOL clauses ****) + +(* The first component is the type class; the second is a TVar or TFree. *) +datatype type_literal = + TyLitVar of name * name | + TyLitFree of name * name + +(*Make literals for sorted type variables*) +fun sorts_on_typs_aux (_, []) = [] + | sorts_on_typs_aux ((x,i), s::ss) = + let val sorts = sorts_on_typs_aux ((x,i), ss) + in + if s = "HOL.type" then sorts + else if i = ~1 then TyLitFree (`make_type_class s, `make_fixed_type_var x) :: sorts + else TyLitVar (`make_type_class s, (make_schematic_type_var (x,i), x)) :: sorts + end; + +fun sorts_on_typs (TFree (a,s)) = sorts_on_typs_aux ((a,~1),s) + | sorts_on_typs (TVar (v,s)) = sorts_on_typs_aux (v,s); + +(*Given a list of sorted type variables, return a list of type literals.*) +fun type_literals_for_types Ts = + fold (union (op =)) (map sorts_on_typs Ts) [] + +(** make axiom and conjecture clauses. **) + +(**** Isabelle arities ****) + +datatype arLit = + TConsLit of name * name * name list | + TVarLit of name * name + +datatype arity_clause = + ArityClause of {name: string, conclLit: arLit, premLits: arLit list} + + +fun gen_TVars 0 = [] + | gen_TVars n = ("T_" ^ Int.toString n) :: gen_TVars (n-1); + +fun pack_sort(_,[]) = [] + | pack_sort(tvar, "HOL.type"::srt) = pack_sort (tvar, srt) (*IGNORE sort "type"*) + | pack_sort(tvar, cls::srt) = + (`make_type_class cls, (tvar, tvar)) :: pack_sort (tvar, srt) + +(*Arity of type constructor tcon :: (arg1,...,argN)res*) +fun make_axiom_arity_clause (tcons, name, (cls,args)) = + let + val tvars = gen_TVars (length args) + val tvars_srts = ListPair.zip (tvars, args) + in + ArityClause {name = name, + conclLit = TConsLit (`make_type_class cls, + `make_fixed_type_const tcons, + tvars ~~ tvars), + premLits = map TVarLit (union_all (map pack_sort tvars_srts))} + end + + +(**** Isabelle class relations ****) + +datatype class_rel_clause = + ClassRelClause of {name: string, subclass: name, superclass: name} + +(*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*) +fun class_pairs _ [] _ = [] + | class_pairs thy subs supers = + let + val class_less = Sorts.class_less (Sign.classes_of thy) + fun add_super sub super = class_less (sub, super) ? cons (sub, super) + fun add_supers sub = fold (add_super sub) supers + in fold add_supers subs [] end + +fun make_class_rel_clause (sub,super) = + ClassRelClause {name = sub ^ "_" ^ super, + subclass = `make_type_class sub, + superclass = `make_type_class super} + +fun make_class_rel_clauses thy subs supers = + map make_class_rel_clause (class_pairs thy subs supers); + + +(** Isabelle arities **) + +fun arity_clause _ _ (_, []) = [] + | arity_clause seen n (tcons, ("HOL.type",_)::ars) = (*ignore*) + arity_clause seen n (tcons,ars) + | arity_clause seen n (tcons, (ar as (class,_)) :: ars) = + if member (op =) seen class then (*multiple arities for the same tycon, class pair*) + make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class ^ "_" ^ Int.toString n, ar) :: + arity_clause seen (n+1) (tcons,ars) + else + make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class, ar) :: + arity_clause (class::seen) n (tcons,ars) + +fun multi_arity_clause [] = [] + | multi_arity_clause ((tcons, ars) :: tc_arlists) = + arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists + +(*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy + provided its arguments have the corresponding sorts.*) +fun type_class_pairs thy tycons classes = + let val alg = Sign.classes_of thy + fun domain_sorts tycon = Sorts.mg_domain alg tycon o single + fun add_class tycon class = + cons (class, domain_sorts tycon class) + handle Sorts.CLASS_ERROR _ => I + fun try_classes tycon = (tycon, fold (add_class tycon) classes []) + in map try_classes tycons end; + +(*Proving one (tycon, class) membership may require proving others, so iterate.*) +fun iter_type_class_pairs _ _ [] = ([], []) + | iter_type_class_pairs thy tycons classes = + let val cpairs = type_class_pairs thy tycons classes + val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs))) + |> subtract (op =) classes |> subtract (op =) HOLogic.typeS + val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses + in (union (op =) classes' classes, union (op =) cpairs' cpairs) end; + +fun make_arity_clauses thy tycons classes = + let val (classes', cpairs) = iter_type_class_pairs thy tycons classes + in (classes', multi_arity_clause cpairs) end; + +datatype combtyp = + CombTVar of name | + CombTFree of name | + CombType of name * combtyp list + +datatype combterm = + CombConst of name * combtyp * combtyp list (* Const and Free *) | + CombVar of name * combtyp | + CombApp of combterm * combterm + +datatype fol_literal = FOLLiteral of bool * combterm + +(*********************************************************************) +(* convert a clause with type Term.term to a clause with type clause *) +(*********************************************************************) + +(*Result of a function type; no need to check that the argument type matches.*) +fun result_type (CombType (_, [_, tp2])) = tp2 + | result_type _ = raise Fail "non-function type" + +fun combtyp_of (CombConst (_, tp, _)) = tp + | combtyp_of (CombVar (_, tp)) = tp + | combtyp_of (CombApp (t1, _)) = result_type (combtyp_of t1) + +(*gets the head of a combinator application, along with the list of arguments*) +fun strip_combterm_comb u = + let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts) + | stripc x = x + in stripc(u,[]) end + +fun combtype_of (Type (a, Ts)) = + let val (folTypes, ts) = combtypes_of Ts in + (CombType (`make_fixed_type_const a, folTypes), ts) + end + | 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 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 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) + +fun new_skolem_const_name th_no s num_T_args = + [new_skolem_const_prefix, string_of_int th_no, s, string_of_int num_T_args] + |> space_implode Long_Name.separator + +(* Converts a term (with combinators) into a combterm. Also accummulates sort + infomation. *) +fun combterm_from_term thy th_no bs (P $ Q) = + let val (P', tsP) = combterm_from_term thy th_no bs P + val (Q', tsQ) = combterm_from_term thy th_no bs Q + in (CombApp (P', Q'), union (op =) tsP tsQ) end + | combterm_from_term thy _ _ (Const (c, T)) = + let + val (tp, ts) = combtype_of T + val tvar_list = + (if String.isPrefix old_skolem_const_prefix c then + [] |> Term.add_tvarsT T |> map TVar + else + (c, T) |> Sign.const_typargs thy) + |> 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) = combtype_of T + val v' = CombConst (`make_fixed_var v, tp, []) + in (v',ts) end + | combterm_from_term _ th_no _ (Var (v as (s, _), T)) = + let + val (tp, ts) = combtype_of T + val v' = + if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then + let + val tys = T |> strip_type |> swap |> op :: + val s' = new_skolem_const_name th_no s (length tys) + in + CombConst (`make_fixed_const s', tp, map simple_combtype_of tys) + end + else + 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) = combtype_of T + val v' = CombConst (`make_bound_var s, tp, []) + in (v', ts) end + | combterm_from_term _ _ _ (Abs _) = raise Fail "HOL clause: Abs" + +fun predicate_of thy th_no ((@{const Not} $ P), pos) = + predicate_of thy th_no (P, not pos) + | predicate_of thy th_no (t, pos) = + (combterm_from_term thy th_no [] (Envir.eta_contract t), pos) + +fun literals_of_term1 args thy th_no (@{const Trueprop} $ P) = + literals_of_term1 args thy th_no P + | literals_of_term1 args thy th_no (@{const HOL.disj} $ P $ Q) = + literals_of_term1 (literals_of_term1 args thy th_no P) thy th_no Q + | literals_of_term1 (lits, ts) thy th_no P = + let val ((pred, ts'), pol) = predicate_of thy th_no (P, true) in + (FOLLiteral (pol, pred) :: lits, union (op =) ts ts') + end +val literals_of_term = literals_of_term1 ([], []) + +fun old_skolem_const_name i j num_T_args = + old_skolem_const_prefix ^ Long_Name.separator ^ + (space_implode Long_Name.separator (map Int.toString [i, j, num_T_args])) + +fun conceal_old_skolem_terms i old_skolems t = + if exists_Const (curry (op =) @{const_name skolem} o fst) t then + let + fun aux old_skolems + (t as (Const (@{const_name skolem}, Type (_, [_, T])) $ _)) = + let + val (old_skolems, s) = + if i = ~1 then + (old_skolems, @{const_name undefined}) + else case AList.find (op aconv) old_skolems t of + s :: _ => (old_skolems, s) + | [] => + let + val s = old_skolem_const_name i (length old_skolems) + (length (Term.add_tvarsT T [])) + in ((s, t) :: old_skolems, s) end + in (old_skolems, Const (s, T)) end + | aux old_skolems (t1 $ t2) = + let + val (old_skolems, t1) = aux old_skolems t1 + val (old_skolems, t2) = aux old_skolems t2 + in (old_skolems, t1 $ t2) end + | aux old_skolems (Abs (s, T, t')) = + let val (old_skolems, t') = aux old_skolems t' in + (old_skolems, Abs (s, T, t')) + end + | aux old_skolems t = (old_skolems, t) + in aux old_skolems t end + else + (old_skolems, t) + +fun reveal_old_skolem_terms old_skolems = + map_aterms (fn t as Const (s, _) => + if String.isPrefix old_skolem_const_prefix s then + AList.lookup (op =) old_skolems s |> the + |> map_types Type_Infer.paramify_vars + else + t + | t => t) + + +(***************************************************************) +(* Type Classes Present in the Axiom or Conjecture Clauses *) +(***************************************************************) + +fun set_insert (x, s) = Symtab.update (x, ()) s + +fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts) + +(*Remove this trivial type class*) +fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset; + +fun tfree_classes_of_terms ts = + let val sorts_list = map (map #2 o OldTerm.term_tfrees) ts + in Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list)) end; + +fun tvar_classes_of_terms ts = + let val sorts_list = map (map #2 o OldTerm.term_tvars) ts + in Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list)) end; + +(*fold type constructors*) +fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x)) + | fold_type_consts _ _ x = x; + +(*Type constructors used to instantiate overloaded constants are the only ones needed.*) +fun add_type_consts_in_term thy = + let + fun aux (Const x) = + fold (fold_type_consts set_insert) (Sign.const_typargs thy x) + | aux (Abs (_, _, u)) = aux u + | aux (Const (@{const_name skolem}, _) $ _) = I + | aux (t $ u) = aux t #> aux u + | aux _ = I + in aux end + +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 (type_wrapper_name, [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 th_no mode t = + let val (lits, types_sorts) = literals_of_term thy th_no 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 th_no ctxt type_lits mode j old_skolems th = + let + val thy = ProofContext.theory_of ctxt + val (old_skolems, (mlits, types_sorts)) = + th |> prop_of |> Logic.strip_imp_concl + |> conceal_old_skolem_terms j old_skolems + ||> (HOLogic.dest_Trueprop #> literals_of_hol_term thy th_no mode) + in + if is_conjecture then + (Metis_Thm.axiom (Metis_LiteralSet.fromList mlits), + type_literals_for_types types_sorts, old_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)), [], + old_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, + old_skolems: (string * term) list} + +fun is_quasi_fol_clause thy = + Meson.is_fol_term thy o snd o conceal_old_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, old_skolems} : logic_map = + {axioms = map (rpair TrueI o metis_of_tfree) (distinct (op =) tfrees) @ + axioms, + tfrees = tfrees, old_skolems = old_skolems} + +(*transform isabelle type / arity clause to metis clause *) +fun add_type_thm [] lmap = lmap + | add_type_thm ((ith, mth) :: cls) {axioms, tfrees, old_skolems} = + add_type_thm cls {axioms = (mth, ith) :: axioms, tfrees = tfrees, + old_skolems = old_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 thss = + 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 (forall (is_quasi_fol_clause thy)) (cls :: thss) then FO + else HO + | set_mode FT = FT + val mode = set_mode mode0 + (*transform isabelle clause to metis clause *) + fun add_thm th_no is_conjecture (metis_ith, isa_ith) + {axioms, tfrees, old_skolems} : logic_map = + let + val (mth, tfree_lits, old_skolems) = + hol_thm_to_fol is_conjecture th_no ctxt type_lits mode (length axioms) + old_skolems metis_ith + in + {axioms = (mth, Meson.make_meta_clause isa_ith) :: axioms, + tfrees = union (op =) tfree_lits tfrees, old_skolems = old_skolems} + end; + val lmap = {axioms = [], tfrees = init_tfrees ctxt, old_skolems = []} + |> fold (add_thm 0 true o `I) cls + |> add_tfrees + |> fold (fn (th_no, ths) => fold (add_thm th_no false o `I) ths) + (1 upto length thss ~~ thss) + 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 ~1 false) helper_ths end + in + (mode, add_type_thm (type_ext thy (maps (map prop_of) (cls :: thss))) lmap) + end + +end; diff -r 277addece9b7 -r 78faa9b31202 src/HOL/Tools/Sledgehammer/metis_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/metis_reconstruct.ML Mon Oct 04 22:01:34 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,557 +0,0 @@ -(* Title: HOL/Tools/Sledgehammer/metis_reconstruct.ML - Author: Kong W. Susanto, Cambridge University Computer Laboratory - Author: Lawrence C. Paulson, Cambridge University Computer Laboratory - Author: Jasmin Blanchette, TU Muenchen - Copyright Cambridge University 2007 - -Proof reconstruction for Metis. -*) - -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 untyped_aconv : term -> term -> bool - 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 = SomeTerm of term | SomeType of typ - -fun terms_of [] = [] - | terms_of (SomeTerm t :: tts) = t :: terms_of tts - | terms_of (SomeType _ :: tts) = terms_of tts; - -fun types_of [] = [] - | types_of (SomeTerm (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 (SomeTerm _ :: tts) = types_of tts - | types_of (SomeType T :: tts) = T :: types_of tts; - -fun apply_list rator nargs rands = - let val trands = terms_of rands - in if length trands = nargs then SomeTerm (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) = 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 => 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 => SomeType (make_tvar w) - | NONE => - case strip_prefix_and_unascii schematic_var_prefix v of - SOME w => SomeTerm (mk_var (w, HOLogic.typeT)) - | NONE => SomeTerm (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 - SomeTerm t => SomeTerm (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) = - SomeTerm (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)) - val t = - if String.isPrefix new_skolem_const_prefix c then - Var (new_skolem_var_from_const c, - Type_Infer.paramify_vars (tl tys ---> hd tys)) - else - Const (c, dummyT) - in if length tys = ntypes then - apply_list t 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 => - SomeType (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 => SomeType (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 = 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 - SomeTerm t => t - | SomeType T => raise TYPE ("fol_tm_to_tt: Term expected", [T], []) - 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 old_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_old_skolem_terms old_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 old_skolems atm = - inst_excluded_middle - (ProofContext.theory_of ctxt) - (singleton (hol_terms_from_fol ctxt mode old_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 old_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_old_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.Option => - (trace_msg (fn () => "\"find_var\" failed for " ^ x ^ - " in " ^ Display.string_of_thm ctxt i_th); - NONE) - | TYPE _ => - (trace_msg (fn () => "\"hol_term_from_metis\" failed for " ^ 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_old_skolem_terms old_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 - -(* Permute a rule's premises to move the i-th premise to the last position. *) -fun make_last i th = - let val n = nprems_of th - in if 1 <= i andalso i <= n - then Thm.permute_prems (i-1) 1 th - else raise THM("select_literal", i, [th]) - end; - -(* Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing - double-negations. *) -val negate_head = rewrite_rule [@{thm atomize_not}, not_not RS eq_reflection] - -(* Maps the clause [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *) -val select_literal = negate_head oo make_last - -fun resolve_inf ctxt mode old_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 old_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 (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 old_skolems t = - let val thy = ProofContext.theory_of ctxt - val i_t = singleton (hol_terms_from_fol ctxt mode old_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 old_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 old_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, 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, 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 ("Cannot replay Metis proof in Isabelle:\n" ^ - "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, 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 ("Cannot replay Metis proof in Isabelle:\n" ^ - "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 = 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 old_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 old_skolems f_atm - | (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) => - factor (inst_inf ctxt mode old_skolems thpairs f_subst f_th1) - | (_, Metis_Proof.Resolve(f_atm, f_th1, f_th2)) => - factor (resolve_inf ctxt mode old_skolems thpairs f_atm f_th1 f_th2) - | (_, Metis_Proof.Refl f_tm) => refl_inf ctxt mode old_skolems f_tm - | (_, Metis_Proof.Equality (f_lit, f_p, f_r)) => - equality_inf ctxt mode old_skolems f_lit f_p f_r - -fun flexflex_first_order th = - case Thm.tpairs_of th of - [] => th - | pairs => - let val thy = theory_of_thm th - val (_, tenv) = - fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty) - val t_pairs = map Meson.term_pair_of (Vartab.dest tenv) - val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th - in th' end - handle THM _ => th; - -fun is_metis_literal_genuine (_, (s, _)) = not (String.isPrefix class_prefix s) -fun is_isabelle_literal_genuine t = - case t of _ $ (Const (@{const_name skolem}, _) $ _) => false | _ => true - -fun count p xs = fold (fn x => if p x then Integer.add 1 else I) xs 0 - -fun replay_one_inference ctxt mode old_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 = step ctxt mode old_skolems thpairs (fol_th, inf) - |> flexflex_first_order - val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th) - val _ = trace_msg (fn () => "=============================================") - val num_metis_lits = - fol_th |> Metis_Thm.clause |> Metis_LiteralSet.toList - |> count is_metis_literal_genuine - val num_isabelle_lits = - th |> prems_of |> count is_isabelle_literal_genuine - val _ = if num_metis_lits = num_isabelle_lits then () - else error "Cannot replay Metis proof in Isabelle: Out of sync." - in (fol_th, th) :: thpairs end - -end; diff -r 277addece9b7 -r 78faa9b31202 src/HOL/Tools/Sledgehammer/metis_tactics.ML --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Oct 04 22:01:34 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,449 +0,0 @@ -(* Title: HOL/Tools/Sledgehammer/metis_tactics.ML - Author: Kong W. Susanto, Cambridge University Computer Laboratory - Author: Lawrence C. Paulson, Cambridge University Computer Laboratory - Author: Jasmin Blanchette, TU Muenchen - Copyright Cambridge University 2007 - -HOL setup for the Metis prover. -*) - -signature METIS_TACTICS = -sig - val trace : bool Unsynchronized.ref - val type_lits : bool Config.T - val new_skolemizer : 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 - -structure Int_Pair_Graph = - Graph(type key = int * int val ord = prod_ord int_ord int_ord) - -fun trace_msg msg = if !trace then tracing (msg ()) else () - -val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" (K true) -val (new_skolemizer, new_skolemizer_setup) = - Attrib.config_bool "metis_new_skolemizer" (K false) - -fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const); - -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; - -val clause_params = - {ordering = Metis_KnuthBendixOrder.default, - orderLiterals = Metis_Clause.UnsignedLiteralOrder, - orderTerms = true} -val active_params = - {clause = clause_params, - prefactor = #prefactor Metis_Active.default, - postfactor = #postfactor Metis_Active.default} -val waiting_params = - {symbolsWeight = 1.0, - variablesWeight = 0.0, - literalsWeight = 0.0, - models = []} -val resolution_params = {active = active_params, waiting = waiting_params} - -fun instantiate_theorem thy inst th = - let - val tyenv = Vartab.empty |> fold (Type.raw_unify o pairself fastype_of) inst - val instT = - [] |> Vartab.fold (fn (z, (S, T)) => - cons (TVar (z, S), Type.devar tyenv T)) tyenv - val inst = inst |> map (pairself (subst_atomic_types instT)) - val _ = tracing (cat_lines (map (fn (T, U) => - Syntax.string_of_typ @{context} T ^ " |-> " ^ - Syntax.string_of_typ @{context} U) instT)) - val _ = tracing (cat_lines (map (fn (t, u) => - Syntax.string_of_term @{context} t ^ " |-> " ^ - Syntax.string_of_term @{context} u) inst)) - val cinstT = instT |> map (pairself (ctyp_of thy)) - val cinst = inst |> map (pairself (cterm_of thy)) - in th |> Thm.instantiate (cinstT, cinst) end - -(* In principle, it should be sufficient to apply "assume_tac" to unify the - conclusion with one of the premises. However, in practice, this is unreliable - because of the mildly higher-order nature of the unification problems. - Typical constraints are of the form - "?SK_a_b_c_x SK_d_e_f_y ... SK_a_b_c_x ... SK_g_h_i_z =?= SK_a_b_c_x", - where the nonvariables are goal parameters. *) -fun unify_first_prem_with_concl thy i th = - let - val goal = Logic.get_goal (prop_of th) i |> Envir.beta_eta_contract - val prem = goal |> Logic.strip_assums_hyp |> hd - val concl = goal |> Logic.strip_assums_concl - fun pair_untyped_aconv (t1, t2) (u1, u2) = - untyped_aconv t1 u1 andalso untyped_aconv t2 u2 - fun add_terms tp inst = - if exists (pair_untyped_aconv tp) inst then inst - else tp :: map (apsnd (subst_atomic [tp])) inst - fun is_flex t = - case strip_comb t of - (Var _, args) => forall is_Bound args - | _ => false - fun unify_flex flex rigid = - case strip_comb flex of - (Var (z as (_, T)), args) => - add_terms (Var z, - fold_rev (curry absdummy) (take (length args) (binder_types T)) rigid) - | _ => raise TERM ("unify_flex: expected flex", [flex]) - fun unify_potential_flex comb atom = - if is_flex comb then unify_flex comb atom - else if is_Var atom then add_terms (atom, comb) - else raise TERM ("unify_terms", [comb, atom]) - fun unify_terms (t, u) = - case (t, u) of - (t1 $ t2, u1 $ u2) => - if is_flex t then unify_flex t u - else if is_flex u then unify_flex u t - else fold unify_terms [(t1, u1), (t2, u2)] - | (_ $ _, _) => unify_potential_flex t u - | (_, _ $ _) => unify_potential_flex u t - | (Var _, _) => add_terms (t, u) - | (_, Var _) => add_terms (u, t) - | _ => if untyped_aconv t u then I else raise TERM ("unify_terms", [t, u]) - in th |> instantiate_theorem thy (unify_terms (prem, concl) []) end - -fun shuffle_key (((axiom_no, (_, index_no)), _), _) = (index_no, axiom_no) -fun shuffle_ord p = - rev_order (prod_ord int_ord int_ord (pairself shuffle_key p)) - -val copy_prem = @{lemma "P ==> (P ==> P ==> Q) ==> Q" by fast} - -fun copy_prems_tac [] ns i = - if forall (curry (op =) 1) ns then all_tac else copy_prems_tac (rev ns) [] i - | copy_prems_tac (1 :: ms) ns i = - rotate_tac 1 i THEN copy_prems_tac ms (1 :: ns) i - | copy_prems_tac (m :: ms) ns i = - etac copy_prem i THEN copy_prems_tac ms (m div 2 :: (m + 1) div 2 :: ns) i - -fun instantiate_forall_tac thy params t i = - let - fun repair (t as (Var ((s, _), _))) = - (case find_index (fn ((s', _), _) => s' = s) params of - ~1 => t - | j => Bound j) - | repair (t $ u) = repair t $ repair u - | repair t = t - val t' = t |> repair |> fold (curry absdummy) (map snd params) - fun do_instantiate th = - let val var = Term.add_vars (prop_of th) [] |> the_single in - th |> instantiate_theorem thy [(Var var, t')] - end - in - etac @{thm allE} i - THEN rotate_tac ~1 i - THEN PRIMITIVE do_instantiate - end - -fun release_clusters_tac _ _ _ _ [] = K all_tac - | release_clusters_tac thy ax_counts substs params - ((ax_no, cluster_no) :: clusters) = - let - fun in_right_cluster s = - (s |> Meson_Clausify.cluster_of_zapped_var_name |> fst |> snd |> fst) - = cluster_no - val cluster_substs = - substs - |> map_filter (fn (ax_no', (_, (_, tsubst))) => - if ax_no' = ax_no then - tsubst |> filter (in_right_cluster - o fst o fst o dest_Var o fst) - |> map snd |> SOME - else - NONE) - val n = length cluster_substs - fun do_cluster_subst cluster_subst = - map (instantiate_forall_tac thy params) cluster_subst @ [rotate_tac 1] - val params' = params (* FIXME ### existentials! *) - val first_prem = find_index (fn (ax_no', _) => ax_no' = ax_no) substs - in - rotate_tac first_prem - THEN' (EVERY' (maps do_cluster_subst cluster_substs)) - THEN' rotate_tac (~ first_prem - length cluster_substs) - THEN' release_clusters_tac thy ax_counts substs params' clusters - end - -val cluster_ord = - prod_ord (prod_ord int_ord (prod_ord int_ord int_ord)) bool_ord - -val tysubst_ord = - list_ord (prod_ord Term_Ord.fast_indexname_ord - (prod_ord Term_Ord.sort_ord Term_Ord.typ_ord)) - -structure Int_Tysubst_Table = - Table(type key = int * (indexname * (sort * typ)) list - val ord = prod_ord int_ord tysubst_ord) - -(* Attempts to derive the theorem "False" from a theorem of the form - "P1 ==> ... ==> Pn ==> False", where the "Pi"s are to be discharged using the - specified axioms. The axioms have leading "All" and "Ex" quantifiers, which - must be eliminated first. *) -fun discharge_skolem_premises ctxt axioms prems_imp_false = - if prop_of prems_imp_false aconv @{prop False} then - prems_imp_false - else - let - val thy = ProofContext.theory_of ctxt - (* distinguish variables with same name but different types *) - val prems_imp_false' = - prems_imp_false |> try (forall_intr_vars #> gen_all) - |> the_default prems_imp_false - val prems_imp_false = - if prop_of prems_imp_false aconv prop_of prems_imp_false' then - prems_imp_false - else - prems_imp_false' - fun match_term p = - let - val (tyenv, tenv) = - Pattern.first_order_match thy p (Vartab.empty, Vartab.empty) - val tsubst = - tenv |> Vartab.dest - |> sort (cluster_ord - o pairself (Meson_Clausify.cluster_of_zapped_var_name - o fst o fst)) - |> map (Meson.term_pair_of - #> pairself (Envir.subst_term_types tyenv)) - val tysubst = tyenv |> Vartab.dest - in (tysubst, tsubst) end - fun subst_info_for_prem subgoal_no prem = - case prem of - _ $ (Const (@{const_name skolem}, _) $ (_ $ t $ num)) => - let val ax_no = HOLogic.dest_nat num in - (ax_no, (subgoal_no, - match_term (nth axioms ax_no |> the |> snd, t))) - end - | _ => raise TERM ("discharge_skolem_premises: Malformed premise", - [prem]) - fun cluster_of_var_name skolem s = - let - val ((ax_no, (cluster_no, _)), skolem') = - Meson_Clausify.cluster_of_zapped_var_name s - in - if skolem' = skolem andalso cluster_no > 0 then - SOME (ax_no, cluster_no) - else - NONE - end - fun clusters_in_term skolem t = - Term.add_var_names t [] |> map_filter (cluster_of_var_name skolem o fst) - fun deps_for_term_subst (var, t) = - case clusters_in_term false var of - [] => NONE - | [(ax_no, cluster_no)] => - SOME ((ax_no, cluster_no), - clusters_in_term true t - |> cluster_no > 1 ? cons (ax_no, cluster_no - 1)) - | _ => raise TERM ("discharge_skolem_premises: Expected Var", [var]) - val prems = Logic.strip_imp_prems (prop_of prems_imp_false) - val substs = prems |> map2 subst_info_for_prem (1 upto length prems) - |> sort (int_ord o pairself fst) - val depss = maps (map_filter deps_for_term_subst o snd o snd o snd) substs - val clusters = maps (op ::) depss - val ordered_clusters = - Int_Pair_Graph.empty - |> fold Int_Pair_Graph.default_node (map (rpair ()) clusters) - |> fold Int_Pair_Graph.add_deps_acyclic depss - |> Int_Pair_Graph.topological_order - handle Int_Pair_Graph.CYCLES _ => - error "Cannot replay Metis proof in Isabelle without axiom of \ - \choice." - val params0 = - [] |> fold (Term.add_vars o snd) (map_filter I axioms) - |> map (`(Meson_Clausify.cluster_of_zapped_var_name o fst o fst)) - |> filter (fn (((_, (cluster_no, _)), skolem), _) => - cluster_no = 0 andalso skolem) - |> sort shuffle_ord |> map snd - val ax_counts = - Int_Tysubst_Table.empty - |> fold (fn (ax_no, (_, (tysubst, _))) => - Int_Tysubst_Table.map_default ((ax_no, tysubst), 0) - (Integer.add 1)) substs - |> Int_Tysubst_Table.dest -(* for debugging: - fun string_for_subst_info (ax_no, (subgoal_no, (tysubst, tsubst))) = - "ax: " ^ string_of_int ax_no ^ "; asm: " ^ string_of_int subgoal_no ^ - "; tysubst: " ^ PolyML.makestring tysubst ^ "; tsubst: {" ^ - commas (map ((fn (s, t) => s ^ " |-> " ^ t) - o pairself (Syntax.string_of_term ctxt)) tsubst) ^ "}" - val _ = tracing ("SUBSTS (" ^ string_of_int (length substs) ^ "):\n" ^ - cat_lines (map string_for_subst_info substs)) - val _ = tracing ("OUTERMOST SKOLEMS: " ^ PolyML.makestring params0) - val _ = tracing ("ORDERED CLUSTERS: " ^ PolyML.makestring ordered_clusters) - val _ = tracing ("AXIOM COUNTS: " ^ PolyML.makestring ax_counts) -*) - fun rotation_for_subgoal i = - find_index (fn (_, (subgoal_no, _)) => subgoal_no = i) substs - in - Goal.prove ctxt [] [] @{prop False} - (K (cut_rules_tac - (map (fst o the o nth axioms o fst o fst) ax_counts) 1 - THEN print_tac "cut:" - THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1) - THEN copy_prems_tac (map snd ax_counts) [] 1 - THEN print_tac "eliminated exist and copied prems:" - THEN release_clusters_tac thy ax_counts substs params0 - ordered_clusters 1 - THEN print_tac "released clusters:" - THEN match_tac [prems_imp_false] 1 - THEN print_tac "applied rule:" - THEN ALLGOALS (fn i => - rtac @{thm skolem_COMBK_I} i - THEN rotate_tac (rotation_for_subgoal i) i - THEN PRIMITIVE (unify_first_prem_with_concl thy i) - THEN assume_tac i))) - end - -(* 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 new_skolemizer = - Config.get ctxt new_skolemizer orelse null (Meson_Choices.get ctxt) - val th_cls_pairs = - map2 (fn j => fn th => - (Thm.get_name_hint th, - Meson_Clausify.cnf_axiom ctxt new_skolemizer j th)) - (0 upto length ths0 - 1) ths0 - val thss = map (snd o snd) th_cls_pairs - val dischargers = map (fst o snd) th_cls_pairs - val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES") - val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls - val _ = trace_msg (fn () => "THEOREM CLAUSES") - val _ = app (app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th))) thss - val (mode, {axioms, tfrees, old_skolems}) = - build_logic_map mode ctxt type_lits cls thss - val _ = if null tfrees then () - else (trace_msg (fn () => "TFREE CLAUSES"); - app (fn TyLitFree ((s, _), (s', _)) => - trace_msg (fn () => s ^ "(" ^ s' ^ ")")) tfrees) - val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS") - val thms = map #1 axioms - val _ = app (fn th => trace_msg (fn () => Metis_Thm.toString th)) thms - val _ = trace_msg (fn () => "mode = " ^ string_of_mode mode) - val _ = trace_msg (fn () => "START METIS PROVE PROCESS") - in - case filter (is_false o prop_of) cls of - false_th::_ => [false_th RS @{thm FalseE}] - | [] => - 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 (replay_one_inference ctxt' mode old_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 have_common_thm used cls then NONE else SOME name) - in - if not (null cls) andalso not (have_common_thm used cls) then - warning "Metis: The assumptions are inconsistent." - else - (); - if not (null unused) then - warning ("Metis: Unused theorems: " ^ commas_quote unused - ^ ".") - else - (); - case result of - (_,ith)::_ => - (trace_msg (fn () => "Success: " ^ Display.string_of_thm ctxt ith); - [discharge_skolem_premises ctxt dischargers ith]) - | _ => (trace_msg (fn () => "Metis: No result"); []) - end - | Metis_Resolution.Satisfiable _ => - (trace_msg (fn () => "Metis: No first-order proof with the lemmas supplied"); - []) - end; - -(* Extensionalize "th", because that makes sense and that's what Sledgehammer - does, but also keep an unextensionalized version of "th" for backward - compatibility. *) -fun also_extensionalize_theorem th = - let val th' = Meson_Clausify.extensionalize_theorem th in - if Thm.eq_thm (th, th') then [th] - else th :: Meson.make_clauses_unsorted [th'] - end - -val neg_clausify = - single - #> Meson.make_clauses_unsorted - #> maps also_extensionalize_theorem - #> map Meson_Clausify.introduce_combinators_in_theorem - #> Meson.finish_cnf - -fun preskolem_tac ctxt st0 = - (if exists (Meson.has_too_many_clauses ctxt) - (Logic.prems_of_goal (prop_of st0) 1) then - cnf.cnfx_rewrite_tac ctxt 1 - else - all_tac) st0 - -val type_has_top_sort = - exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false) - -fun generic_metis_tac mode ctxt ths i st0 = - let - val _ = trace_msg (fn () => - "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths)) - in - if exists_type type_has_top_sort (prop_of st0) then - (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty) - else - Meson.MESON (preskolem_tac ctxt) (maps neg_clausify) - (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) - ctxt i st0 - end - -val metis_tac = generic_metis_tac HO -val metisF_tac = generic_metis_tac FO -val metisFT_tac = generic_metis_tac FT - -(* Whenever "X" has schematic type variables, we treat "using X by metis" as - "by (metis X)", to prevent "Subgoal.FOCUS" from freezing the type variables. - We don't do it for nonschematic facts "X" because this breaks a few proofs - (in the rare and subtle case where a proof relied on extensionality not being - applied) and brings few benefits. *) -val has_tvar = - exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of -fun method name mode = - Method.setup name (Attrib.thms >> (fn ths => fn ctxt => - METHOD (fn facts => - let - val (schem_facts, nonschem_facts) = - List.partition has_tvar facts - in - HEADGOAL (Method.insert_tac nonschem_facts THEN' - CHANGED_PROP - o generic_metis_tac mode ctxt (schem_facts @ ths)) - end))) - -val setup = - type_lits_setup - #> new_skolemizer_setup - #> method @{binding metis} HO "Metis for FOL/HOL problems" - #> method @{binding metisF} FO "Metis for FOL problems" - #> method @{binding metisFT} FT - "Metis for FOL/HOL problems with fully-typed translation" - -end; diff -r 277addece9b7 -r 78faa9b31202 src/HOL/Tools/Sledgehammer/metis_translate.ML --- a/src/HOL/Tools/Sledgehammer/metis_translate.ML Mon Oct 04 22:01:34 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,771 +0,0 @@ -(* 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. -*) - -signature METIS_TRANSLATE = -sig - type name = string * string - datatype type_literal = - TyLitVar of name * name | - TyLitFree of name * name - datatype arLit = - TConsLit of name * name * name list | - TVarLit of name * name - datatype arity_clause = - ArityClause of {name: string, conclLit: arLit, premLits: arLit list} - datatype class_rel_clause = - ClassRelClause of {name: string, subclass: name, superclass: name} - datatype combtyp = - CombTVar of name | - CombTFree of name | - CombType of name * combtyp list - datatype combterm = - CombConst of name * combtyp * combtyp list (* Const and Free *) | - CombVar of name * combtyp | - 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, - old_skolems: (string * term) list} - - val type_wrapper_name : string - val bound_var_prefix : string - val schematic_var_prefix: string - val fixed_var_prefix: string - val tvar_prefix: string - val tfree_prefix: string - val const_prefix: string - val type_const_prefix: string - val class_prefix: string - val new_skolem_const_prefix : string - val invert_const: string -> string - val ascii_of: string -> string - val unascii_of: string -> string - val strip_prefix_and_unascii: string -> string -> string option - val make_bound_var : string -> string - val make_schematic_var : string * int -> string - val make_fixed_var : string -> string - val make_schematic_type_var : string * int -> string - val make_fixed_type_var : string -> string - val make_fixed_const : string -> string - val make_fixed_type_const : string -> string - val make_type_class : string -> string - val num_type_args: theory -> string -> int - val new_skolem_var_from_const: string -> indexname - val type_literals_for_types : typ list -> type_literal list - val make_class_rel_clauses : - theory -> class list -> class list -> class_rel_clause list - val make_arity_clauses : - theory -> string list -> class list -> class list * arity_clause list - val combtyp_of : combterm -> combtyp - val strip_combterm_comb : combterm -> combterm * combterm list - val combterm_from_term : - theory -> int -> (string * typ) list -> term -> combterm * typ list - val reveal_old_skolem_terms : (string * term) list -> term -> term - 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 list - -> mode * logic_map -end - -structure Metis_Translate : METIS_TRANSLATE = -struct - -val type_wrapper_name = "ti" - -val bound_var_prefix = "B_" -val schematic_var_prefix = "V_" -val fixed_var_prefix = "v_" - -val tvar_prefix = "T_"; -val tfree_prefix = "t_"; - -val const_prefix = "c_"; -val type_const_prefix = "tc_"; -val class_prefix = "class_"; - -val skolem_const_prefix = "Sledgehammer" ^ Long_Name.separator ^ "Sko" -val old_skolem_const_prefix = skolem_const_prefix ^ "o" -val new_skolem_const_prefix = skolem_const_prefix ^ "n" - -fun union_all xss = fold (union (op =)) xss [] - -(* Readable names for the more common symbolic functions. Do not mess with the - last nine entries of the table unless you know what you are doing. *) -val const_trans_table = - Symtab.make [(@{type_name Product_Type.prod}, "prod"), - (@{type_name Sum_Type.sum}, "sum"), - (@{const_name HOL.eq}, "equal"), - (@{const_name HOL.conj}, "and"), - (@{const_name HOL.disj}, "or"), - (@{const_name HOL.implies}, "implies"), - (@{const_name Set.member}, "member"), - (@{const_name fequal}, "fequal"), - (@{const_name COMBI}, "COMBI"), - (@{const_name COMBK}, "COMBK"), - (@{const_name COMBB}, "COMBB"), - (@{const_name COMBC}, "COMBC"), - (@{const_name COMBS}, "COMBS"), - (@{const_name True}, "True"), - (@{const_name False}, "False"), - (@{const_name If}, "If")] - -(* Invert the table of translations between Isabelle and ATPs. *) -val const_trans_table_inv = - Symtab.update ("fequal", @{const_name HOL.eq}) - (Symtab.make (map swap (Symtab.dest const_trans_table))) - -val invert_const = perhaps (Symtab.lookup const_trans_table_inv) - -(*Escaping of special characters. - Alphanumeric characters are left unchanged. - The character _ goes to __ - Characters in the range ASCII space to / go to _A to _P, respectively. - Other characters go to _nnn where nnn is the decimal ASCII code.*) -val A_minus_space = Char.ord #"A" - Char.ord #" "; - -fun stringN_of_int 0 _ = "" - | stringN_of_int k n = stringN_of_int (k-1) (n div 10) ^ Int.toString (n mod 10); - -fun ascii_of_c c = - if Char.isAlphaNum c then String.str c - else if c = #"_" then "__" - else if #" " <= c andalso c <= #"/" - then "_" ^ String.str (Char.chr (Char.ord c + A_minus_space)) - else ("_" ^ stringN_of_int 3 (Char.ord c)) (*fixed width, in case more digits follow*) - -val ascii_of = String.translate ascii_of_c; - -(** Remove ASCII armouring from names in proof files **) - -(*We don't raise error exceptions because this code can run inside the watcher. - Also, the errors are "impossible" (hah!)*) -fun unascii_aux rcs [] = String.implode(rev rcs) - | unascii_aux rcs [#"_"] = unascii_aux (#"_"::rcs) [] (*ERROR*) - (*Three types of _ escapes: __, _A to _P, _nnn*) - | unascii_aux rcs (#"_" :: #"_" :: cs) = unascii_aux (#"_"::rcs) cs - | unascii_aux rcs (#"_" :: c :: cs) = - if #"A" <= c andalso c<= #"P" (*translation of #" " to #"/"*) - then unascii_aux (Char.chr(Char.ord c - A_minus_space) :: rcs) cs - else - let val digits = List.take (c::cs, 3) handle Subscript => [] - in - case Int.fromString (String.implode digits) of - NONE => unascii_aux (c:: #"_"::rcs) cs (*ERROR*) - | SOME n => unascii_aux (Char.chr n :: rcs) (List.drop (cs, 2)) - end - | unascii_aux rcs (c::cs) = unascii_aux (c::rcs) cs -val unascii_of = unascii_aux [] o String.explode - -(* If string s has the prefix s1, return the result of deleting it, - un-ASCII'd. *) -fun strip_prefix_and_unascii s1 s = - if String.isPrefix s1 s then - SOME (unascii_of (String.extract (s, size s1, NONE))) - else - NONE - -(*Remove the initial ' character from a type variable, if it is present*) -fun trim_type_var s = - if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE) - else error ("trim_type: Malformed type variable encountered: " ^ s); - -fun ascii_of_indexname (v,0) = ascii_of v - | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ Int.toString i; - -fun make_bound_var x = bound_var_prefix ^ ascii_of x -fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v -fun make_fixed_var x = fixed_var_prefix ^ ascii_of x - -fun make_schematic_type_var (x,i) = - tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i)); -fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x)); - -fun lookup_const c = - case Symtab.lookup const_trans_table c of - SOME c' => c' - | NONE => ascii_of c - -(* HOL.eq MUST BE "equal" because it's built into ATPs. *) -fun make_fixed_const @{const_name HOL.eq} = "equal" - | make_fixed_const c = const_prefix ^ lookup_const c - -fun make_fixed_type_const c = type_const_prefix ^ lookup_const c - -fun make_type_class clas = class_prefix ^ ascii_of clas; - -(* The number of type arguments of a constant, zero if it's monomorphic. For - (instances of) Skolem pseudoconstants, this information is encoded in the - constant name. *) -fun num_type_args thy s = - if String.isPrefix skolem_const_prefix s then - s |> space_explode Long_Name.separator |> List.last |> Int.fromString |> the - else - (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length - -fun new_skolem_var_from_const s = - let - val ss = s |> space_explode Long_Name.separator - val n = length ss - in (nth ss (n - 2), nth ss (n - 3) |> Int.fromString |> the) end - - -(**** Definitions and functions for FOL clauses for TPTP format output ****) - -type name = string * string - -(**** Isabelle FOL clauses ****) - -(* The first component is the type class; the second is a TVar or TFree. *) -datatype type_literal = - TyLitVar of name * name | - TyLitFree of name * name - -(*Make literals for sorted type variables*) -fun sorts_on_typs_aux (_, []) = [] - | sorts_on_typs_aux ((x,i), s::ss) = - let val sorts = sorts_on_typs_aux ((x,i), ss) - in - if s = "HOL.type" then sorts - else if i = ~1 then TyLitFree (`make_type_class s, `make_fixed_type_var x) :: sorts - else TyLitVar (`make_type_class s, (make_schematic_type_var (x,i), x)) :: sorts - end; - -fun sorts_on_typs (TFree (a,s)) = sorts_on_typs_aux ((a,~1),s) - | sorts_on_typs (TVar (v,s)) = sorts_on_typs_aux (v,s); - -(*Given a list of sorted type variables, return a list of type literals.*) -fun type_literals_for_types Ts = - fold (union (op =)) (map sorts_on_typs Ts) [] - -(** make axiom and conjecture clauses. **) - -(**** Isabelle arities ****) - -datatype arLit = - TConsLit of name * name * name list | - TVarLit of name * name - -datatype arity_clause = - ArityClause of {name: string, conclLit: arLit, premLits: arLit list} - - -fun gen_TVars 0 = [] - | gen_TVars n = ("T_" ^ Int.toString n) :: gen_TVars (n-1); - -fun pack_sort(_,[]) = [] - | pack_sort(tvar, "HOL.type"::srt) = pack_sort (tvar, srt) (*IGNORE sort "type"*) - | pack_sort(tvar, cls::srt) = - (`make_type_class cls, (tvar, tvar)) :: pack_sort (tvar, srt) - -(*Arity of type constructor tcon :: (arg1,...,argN)res*) -fun make_axiom_arity_clause (tcons, name, (cls,args)) = - let - val tvars = gen_TVars (length args) - val tvars_srts = ListPair.zip (tvars, args) - in - ArityClause {name = name, - conclLit = TConsLit (`make_type_class cls, - `make_fixed_type_const tcons, - tvars ~~ tvars), - premLits = map TVarLit (union_all (map pack_sort tvars_srts))} - end - - -(**** Isabelle class relations ****) - -datatype class_rel_clause = - ClassRelClause of {name: string, subclass: name, superclass: name} - -(*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*) -fun class_pairs _ [] _ = [] - | class_pairs thy subs supers = - let - val class_less = Sorts.class_less (Sign.classes_of thy) - fun add_super sub super = class_less (sub, super) ? cons (sub, super) - fun add_supers sub = fold (add_super sub) supers - in fold add_supers subs [] end - -fun make_class_rel_clause (sub,super) = - ClassRelClause {name = sub ^ "_" ^ super, - subclass = `make_type_class sub, - superclass = `make_type_class super} - -fun make_class_rel_clauses thy subs supers = - map make_class_rel_clause (class_pairs thy subs supers); - - -(** Isabelle arities **) - -fun arity_clause _ _ (_, []) = [] - | arity_clause seen n (tcons, ("HOL.type",_)::ars) = (*ignore*) - arity_clause seen n (tcons,ars) - | arity_clause seen n (tcons, (ar as (class,_)) :: ars) = - if member (op =) seen class then (*multiple arities for the same tycon, class pair*) - make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class ^ "_" ^ Int.toString n, ar) :: - arity_clause seen (n+1) (tcons,ars) - else - make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class, ar) :: - arity_clause (class::seen) n (tcons,ars) - -fun multi_arity_clause [] = [] - | multi_arity_clause ((tcons, ars) :: tc_arlists) = - arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists - -(*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy - provided its arguments have the corresponding sorts.*) -fun type_class_pairs thy tycons classes = - let val alg = Sign.classes_of thy - fun domain_sorts tycon = Sorts.mg_domain alg tycon o single - fun add_class tycon class = - cons (class, domain_sorts tycon class) - handle Sorts.CLASS_ERROR _ => I - fun try_classes tycon = (tycon, fold (add_class tycon) classes []) - in map try_classes tycons end; - -(*Proving one (tycon, class) membership may require proving others, so iterate.*) -fun iter_type_class_pairs _ _ [] = ([], []) - | iter_type_class_pairs thy tycons classes = - let val cpairs = type_class_pairs thy tycons classes - val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs))) - |> subtract (op =) classes |> subtract (op =) HOLogic.typeS - val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses - in (union (op =) classes' classes, union (op =) cpairs' cpairs) end; - -fun make_arity_clauses thy tycons classes = - let val (classes', cpairs) = iter_type_class_pairs thy tycons classes - in (classes', multi_arity_clause cpairs) end; - -datatype combtyp = - CombTVar of name | - CombTFree of name | - CombType of name * combtyp list - -datatype combterm = - CombConst of name * combtyp * combtyp list (* Const and Free *) | - CombVar of name * combtyp | - CombApp of combterm * combterm - -datatype fol_literal = FOLLiteral of bool * combterm - -(*********************************************************************) -(* convert a clause with type Term.term to a clause with type clause *) -(*********************************************************************) - -(*Result of a function type; no need to check that the argument type matches.*) -fun result_type (CombType (_, [_, tp2])) = tp2 - | result_type _ = raise Fail "non-function type" - -fun combtyp_of (CombConst (_, tp, _)) = tp - | combtyp_of (CombVar (_, tp)) = tp - | combtyp_of (CombApp (t1, _)) = result_type (combtyp_of t1) - -(*gets the head of a combinator application, along with the list of arguments*) -fun strip_combterm_comb u = - let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts) - | stripc x = x - in stripc(u,[]) end - -fun combtype_of (Type (a, Ts)) = - let val (folTypes, ts) = combtypes_of Ts in - (CombType (`make_fixed_type_const a, folTypes), ts) - end - | 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 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 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) - -fun new_skolem_const_name th_no s num_T_args = - [new_skolem_const_prefix, string_of_int th_no, s, string_of_int num_T_args] - |> space_implode Long_Name.separator - -(* Converts a term (with combinators) into a combterm. Also accummulates sort - infomation. *) -fun combterm_from_term thy th_no bs (P $ Q) = - let val (P', tsP) = combterm_from_term thy th_no bs P - val (Q', tsQ) = combterm_from_term thy th_no bs Q - in (CombApp (P', Q'), union (op =) tsP tsQ) end - | combterm_from_term thy _ _ (Const (c, T)) = - let - val (tp, ts) = combtype_of T - val tvar_list = - (if String.isPrefix old_skolem_const_prefix c then - [] |> Term.add_tvarsT T |> map TVar - else - (c, T) |> Sign.const_typargs thy) - |> 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) = combtype_of T - val v' = CombConst (`make_fixed_var v, tp, []) - in (v',ts) end - | combterm_from_term _ th_no _ (Var (v as (s, _), T)) = - let - val (tp, ts) = combtype_of T - val v' = - if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then - let - val tys = T |> strip_type |> swap |> op :: - val s' = new_skolem_const_name th_no s (length tys) - in - CombConst (`make_fixed_const s', tp, map simple_combtype_of tys) - end - else - 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) = combtype_of T - val v' = CombConst (`make_bound_var s, tp, []) - in (v', ts) end - | combterm_from_term _ _ _ (Abs _) = raise Fail "HOL clause: Abs" - -fun predicate_of thy th_no ((@{const Not} $ P), pos) = - predicate_of thy th_no (P, not pos) - | predicate_of thy th_no (t, pos) = - (combterm_from_term thy th_no [] (Envir.eta_contract t), pos) - -fun literals_of_term1 args thy th_no (@{const Trueprop} $ P) = - literals_of_term1 args thy th_no P - | literals_of_term1 args thy th_no (@{const HOL.disj} $ P $ Q) = - literals_of_term1 (literals_of_term1 args thy th_no P) thy th_no Q - | literals_of_term1 (lits, ts) thy th_no P = - let val ((pred, ts'), pol) = predicate_of thy th_no (P, true) in - (FOLLiteral (pol, pred) :: lits, union (op =) ts ts') - end -val literals_of_term = literals_of_term1 ([], []) - -fun old_skolem_const_name i j num_T_args = - old_skolem_const_prefix ^ Long_Name.separator ^ - (space_implode Long_Name.separator (map Int.toString [i, j, num_T_args])) - -fun conceal_old_skolem_terms i old_skolems t = - if exists_Const (curry (op =) @{const_name skolem} o fst) t then - let - fun aux old_skolems - (t as (Const (@{const_name skolem}, Type (_, [_, T])) $ _)) = - let - val (old_skolems, s) = - if i = ~1 then - (old_skolems, @{const_name undefined}) - else case AList.find (op aconv) old_skolems t of - s :: _ => (old_skolems, s) - | [] => - let - val s = old_skolem_const_name i (length old_skolems) - (length (Term.add_tvarsT T [])) - in ((s, t) :: old_skolems, s) end - in (old_skolems, Const (s, T)) end - | aux old_skolems (t1 $ t2) = - let - val (old_skolems, t1) = aux old_skolems t1 - val (old_skolems, t2) = aux old_skolems t2 - in (old_skolems, t1 $ t2) end - | aux old_skolems (Abs (s, T, t')) = - let val (old_skolems, t') = aux old_skolems t' in - (old_skolems, Abs (s, T, t')) - end - | aux old_skolems t = (old_skolems, t) - in aux old_skolems t end - else - (old_skolems, t) - -fun reveal_old_skolem_terms old_skolems = - map_aterms (fn t as Const (s, _) => - if String.isPrefix old_skolem_const_prefix s then - AList.lookup (op =) old_skolems s |> the - |> map_types Type_Infer.paramify_vars - else - t - | t => t) - - -(***************************************************************) -(* Type Classes Present in the Axiom or Conjecture Clauses *) -(***************************************************************) - -fun set_insert (x, s) = Symtab.update (x, ()) s - -fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts) - -(*Remove this trivial type class*) -fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset; - -fun tfree_classes_of_terms ts = - let val sorts_list = map (map #2 o OldTerm.term_tfrees) ts - in Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list)) end; - -fun tvar_classes_of_terms ts = - let val sorts_list = map (map #2 o OldTerm.term_tvars) ts - in Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list)) end; - -(*fold type constructors*) -fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x)) - | fold_type_consts _ _ x = x; - -(*Type constructors used to instantiate overloaded constants are the only ones needed.*) -fun add_type_consts_in_term thy = - let - fun aux (Const x) = - fold (fold_type_consts set_insert) (Sign.const_typargs thy x) - | aux (Abs (_, _, u)) = aux u - | aux (Const (@{const_name skolem}, _) $ _) = I - | aux (t $ u) = aux t #> aux u - | aux _ = I - in aux end - -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 (type_wrapper_name, [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 th_no mode t = - let val (lits, types_sorts) = literals_of_term thy th_no 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 th_no ctxt type_lits mode j old_skolems th = - let - val thy = ProofContext.theory_of ctxt - val (old_skolems, (mlits, types_sorts)) = - th |> prop_of |> Logic.strip_imp_concl - |> conceal_old_skolem_terms j old_skolems - ||> (HOLogic.dest_Trueprop #> literals_of_hol_term thy th_no mode) - in - if is_conjecture then - (Metis_Thm.axiom (Metis_LiteralSet.fromList mlits), - type_literals_for_types types_sorts, old_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)), [], - old_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, - old_skolems: (string * term) list} - -fun is_quasi_fol_clause thy = - Meson.is_fol_term thy o snd o conceal_old_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, old_skolems} : logic_map = - {axioms = map (rpair TrueI o metis_of_tfree) (distinct (op =) tfrees) @ - axioms, - tfrees = tfrees, old_skolems = old_skolems} - -(*transform isabelle type / arity clause to metis clause *) -fun add_type_thm [] lmap = lmap - | add_type_thm ((ith, mth) :: cls) {axioms, tfrees, old_skolems} = - add_type_thm cls {axioms = (mth, ith) :: axioms, tfrees = tfrees, - old_skolems = old_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 thss = - 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 (forall (is_quasi_fol_clause thy)) (cls :: thss) then FO - else HO - | set_mode FT = FT - val mode = set_mode mode0 - (*transform isabelle clause to metis clause *) - fun add_thm th_no is_conjecture (metis_ith, isa_ith) - {axioms, tfrees, old_skolems} : logic_map = - let - val (mth, tfree_lits, old_skolems) = - hol_thm_to_fol is_conjecture th_no ctxt type_lits mode (length axioms) - old_skolems metis_ith - in - {axioms = (mth, Meson.make_meta_clause isa_ith) :: axioms, - tfrees = union (op =) tfree_lits tfrees, old_skolems = old_skolems} - end; - val lmap = {axioms = [], tfrees = init_tfrees ctxt, old_skolems = []} - |> fold (add_thm 0 true o `I) cls - |> add_tfrees - |> fold (fn (th_no, ths) => fold (add_thm th_no false o `I) ths) - (1 upto length thss ~~ thss) - 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 ~1 false) helper_ths end - in - (mode, add_type_thm (type_ext thy (maps (map prop_of) (cls :: thss))) lmap) - end - -end; diff -r 277addece9b7 -r 78faa9b31202 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Mon Oct 04 22:01:34 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Mon Oct 04 22:45:09 2010 +0200 @@ -585,6 +585,7 @@ fun is_formula_too_complex t = apply_depth t > max_apply_depth orelse formula_has_too_many_lambdas [] t +(* FIXME: Extend to "Meson" and "Metis" *) val exists_sledgehammer_const = exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s)