proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
--- a/src/HOL/Sledgehammer.thy Fri Jun 11 17:07:27 2010 +0200
+++ b/src/HOL/Sledgehammer.thy Fri Jun 11 17:10:23 2010 +0200
@@ -25,6 +25,12 @@
("Tools/Sledgehammer/metis_tactics.ML")
begin
+definition skolem_Eps :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" where
+[no_atp]: "skolem_Eps = Eps"
+
+lemma skolem_someI_ex [no_atp]: "\<exists>x. P x \<Longrightarrow> P (skolem_Eps (\<lambda>x. P x))"
+unfolding skolem_Eps_def by (rule someI_ex)
+
definition COMBI :: "'a \<Rightarrow> 'a" where
[no_atp]: "COMBI P \<equiv> P"
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Jun 11 17:07:27 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Jun 11 17:10:23 2010 +0200
@@ -18,6 +18,7 @@
structure Metis_Tactics : METIS_TACTICS =
struct
+open Sledgehammer_Util
open Sledgehammer_FOL_Clause
open Sledgehammer_Fact_Preprocessor
open Sledgehammer_HOL_Clause
@@ -118,7 +119,7 @@
metis_lit pol "=" (map hol_term_to_fol_FT tms)
| _ => metis_lit pol "{}" [hol_term_to_fol_FT tm]) (*hBOOL*);
-fun literals_of_hol_thm thy mode t =
+fun literals_of_hol_term thy mode t =
let val (lits, types_sorts) = literals_of_term thy t
in (map (hol_literal_to_fol mode) lits, types_sorts) end;
@@ -134,21 +135,24 @@
fun metis_of_tfree tf =
Metis.Thm.axiom (Metis.LiteralSet.singleton (metis_of_type_literals true tf));
-fun hol_thm_to_fol is_conjecture ctxt mode th =
- let val thy = ProofContext.theory_of ctxt
- val (mlits, types_sorts) =
- (literals_of_hol_thm thy mode o HOLogic.dest_Trueprop o prop_of) th
+fun hol_thm_to_fol is_conjecture ctxt mode j skolem_somes th =
+ let
+ val thy = ProofContext.theory_of ctxt
+ val (skolem_somes, (mlits, types_sorts)) =
+ th |> prop_of |> kill_skolem_Eps j skolem_somes
+ ||> (HOLogic.dest_Trueprop #> literals_of_hol_term thy mode)
in
if is_conjecture then
(Metis.Thm.axiom (Metis.LiteralSet.fromList mlits),
- type_literals_for_types types_sorts)
+ type_literals_for_types types_sorts, skolem_somes)
else
let val tylits = filter_out (default_sort ctxt) types_sorts
|> type_literals_for_types
val mtylits = if Config.get ctxt type_lits
then map (metis_of_type_literals false) tylits else []
in
- (Metis.Thm.axiom (Metis.LiteralSet.fromList(mtylits @ mlits)), [])
+ (Metis.Thm.axiom (Metis.LiteralSet.fromList(mtylits @ mlits)), [],
+ skolem_somes)
end
end;
@@ -231,10 +235,30 @@
SOME tf => mk_tfree ctxt tf
| NONE => error ("fol_type_to_isa: " ^ x));
+fun reintroduce_skolem_Eps thy skolem_somes =
+ let
+ fun aux Ts args t =
+ case t of
+ t1 $ t2 => aux Ts (aux Ts [] t2 :: args) t1
+ | Abs (s, T, t') => list_comb (Abs (s, T, aux (T :: Ts) [] t'), args)
+ | Const (s, T) =>
+ if String.isPrefix skolem_Eps_pseudo_theory s then
+ let
+ val (T', args', def') = AList.lookup (op =) skolem_somes s |> the
+ in
+ def' |> subst_free (args' ~~ args)
+ |> map_types Type_Infer.paramify_vars
+ end
+ else
+ list_comb (t, args)
+ | t => list_comb (t, args)
+ in aux [] [] end
+
(*Maps metis terms to isabelle terms*)
-fun fol_term_to_hol_RAW ctxt fol_tm =
+fun hol_term_from_fol_PT ctxt fol_tm =
let val thy = ProofContext.theory_of ctxt
- val _ = trace_msg (fn () => "fol_term_to_hol: " ^ Metis.Term.toString fol_tm)
+ val _ = trace_msg (fn () => "hol_term_from_fol_PT: " ^
+ Metis.Term.toString fol_tm)
fun tm_to_tt (Metis.Term.Var v) =
(case strip_prefix tvar_prefix v of
SOME w => Type (make_tvar w)
@@ -285,11 +309,16 @@
let val opr = Term.Free(b, HOLogic.typeT)
in apply_list opr (length ts) (map tm_to_tt ts) end
| NONE => error ("unexpected metis function: " ^ a)
- in case tm_to_tt fol_tm of Term t => t | _ => error "fol_tm_to_tt: Term expected" end;
+ in
+ case tm_to_tt fol_tm of
+ Term t => t
+ | _ => error "fol_tm_to_tt: Term expected"
+ end
(*Maps fully-typed metis terms to isabelle terms*)
-fun fol_term_to_hol_FT ctxt fol_tm =
- let val _ = trace_msg (fn () => "fol_term_to_hol_FT: " ^ Metis.Term.toString fol_tm)
+fun hol_term_from_fol_FT ctxt fol_tm =
+ let val _ = trace_msg (fn () => "hol_term_from_fol_FT: " ^
+ Metis.Term.toString fol_tm)
fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) =
(case strip_prefix schematic_var_prefix v of
SOME w => mk_var(w, dummyT)
@@ -302,7 +331,7 @@
| NONE => (*Not a constant. Is it a fixed variable??*)
case strip_prefix fixed_var_prefix x of
SOME v => Free (v, fol_type_to_isa ctxt ty)
- | NONE => error ("fol_term_to_hol_FT bad constant: " ^ x))
+ | NONE => error ("hol_term_from_fol_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*)
@@ -316,21 +345,22 @@
| NONE => (*Not a constant. Is it a fixed variable??*)
case strip_prefix fixed_var_prefix x of
SOME v => Free (v, dummyT)
- | NONE => (trace_msg (fn () => "fol_term_to_hol_FT bad const: " ^ x);
- fol_term_to_hol_RAW ctxt t))
- | cvt t = (trace_msg (fn () => "fol_term_to_hol_FT bad term: " ^ Metis.Term.toString t);
- fol_term_to_hol_RAW ctxt t)
- in cvt fol_tm end;
+ | NONE => (trace_msg (fn () => "hol_term_from_fol_FT bad const: " ^ x);
+ hol_term_from_fol_PT ctxt t))
+ | cvt t = (trace_msg (fn () => "hol_term_from_fol_FT bad term: " ^ Metis.Term.toString t);
+ hol_term_from_fol_PT ctxt t)
+ in fol_tm |> cvt end
-fun fol_term_to_hol ctxt FO = fol_term_to_hol_RAW ctxt
- | fol_term_to_hol ctxt HO = fol_term_to_hol_RAW ctxt
- | fol_term_to_hol ctxt FT = fol_term_to_hol_FT ctxt;
+fun hol_term_from_fol FT = hol_term_from_fol_FT
+ | hol_term_from_fol _ = hol_term_from_fol_PT
-fun fol_terms_to_hol ctxt mode fol_tms =
- let val ts = map (fol_term_to_hol ctxt mode) fol_tms
+fun hol_terms_from_fol ctxt mode skolem_somes fol_tms =
+ let val thy = ProofContext.theory_of ctxt
+ val ts = map (hol_term_from_fol 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' = infer_types ctxt ts;
+ val ts' =
+ ts |> map (reintroduce_skolem_Eps thy skolem_somes) |> 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)))
@@ -371,22 +401,23 @@
(*This causes variables to have an index of 1 by default. SEE ALSO mk_var above.*)
(* INFERENCE RULE: ASSUME *)
-fun assume_inf ctxt mode atm =
+fun assume_inf ctxt mode skolem_somes atm =
inst_excluded_middle
(ProofContext.theory_of ctxt)
- (singleton (fol_terms_to_hol ctxt mode) (Metis.Term.Fn atm));
+ (singleton (hol_terms_from_fol ctxt mode skolem_somes) (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 thpairs fsubst th =
+fun inst_inf ctxt mode skolem_somes 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
- val t = fol_term_to_hol ctxt mode y (*we call infer_types below*)
+ (* We call "reintroduce_skolem_Eps" and "infer_types" below. *)
+ val t = hol_term_from_fol mode ctxt y
in SOME (cterm_of thy (Var v), t) end
handle Option =>
(trace_msg (fn() => "List.find failed for the variable " ^ x ^
@@ -401,7 +432,8 @@
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 = infer_types ctxt rawtms;
+ val tms = rawtms |> map (reintroduce_skolem_Eps thy skolem_somes)
+ |> 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 () =>
@@ -409,10 +441,11 @@
(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
+ in cterm_instantiate substs' i_th end
handle THM (msg, _, _) => error ("metis error (inst_inf):\n" ^ msg)
| ERROR msg => error ("metis error (inst_inf):\n" ^ msg ^
- "\n(Perhaps you want to try \"metisFT\".)")
+ "\n(Perhaps you want to try \"metisFT\" if you \
+ \haven't done so already.)")
(* INFERENCE RULE: RESOLVE *)
@@ -428,7 +461,7 @@
| _ => raise THM ("resolve_inc_tyvars: unique result expected", i, [tha,thb])
end;
-fun resolve_inf ctxt mode thpairs atm th1 th2 =
+fun resolve_inf ctxt mode skolem_somes thpairs atm th1 th2 =
let
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)
@@ -438,7 +471,8 @@
else if is_TrueI i_th2 then i_th1
else
let
- val i_atm = singleton (fol_terms_to_hol ctxt mode) (Metis.Term.Fn atm)
+ val i_atm = singleton (hol_terms_from_fol ctxt mode skolem_somes)
+ (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
@@ -455,9 +489,9 @@
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 t =
+fun refl_inf ctxt mode skolem_somes t =
let val thy = ProofContext.theory_of ctxt
- val i_t = singleton (fol_terms_to_hol ctxt mode) t
+ val i_t = singleton (hol_terms_from_fol ctxt mode skolem_somes) 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;
@@ -467,10 +501,10 @@
| get_ty_arg_size _ _ = 0;
(* INFERENCE RULE: EQUALITY *)
-fun equality_inf ctxt mode (pos, atm) fp fr =
+fun equality_inf ctxt mode skolem_somes (pos, atm) fp fr =
let val thy = ProofContext.theory_of ctxt
val m_tm = Metis.Term.Fn atm
- val [i_atm,i_tm] = fol_terms_to_hol ctxt mode [m_tm, fr]
+ val [i_atm,i_tm] = hol_terms_from_fol ctxt mode skolem_somes [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
@@ -539,24 +573,28 @@
val factor = Seq.hd o distinct_subgoals_tac;
-fun step _ _ thpairs (fol_th, Metis.Proof.Axiom _) = factor (axiom_inf thpairs fol_th)
- | step ctxt mode _ (_, Metis.Proof.Assume f_atm) = assume_inf ctxt mode f_atm
- | step ctxt mode thpairs (_, Metis.Proof.Subst (f_subst, f_th1)) =
- factor (inst_inf ctxt mode thpairs f_subst f_th1)
- | step ctxt mode thpairs (_, Metis.Proof.Resolve(f_atm, f_th1, f_th2)) =
- factor (resolve_inf ctxt mode thpairs f_atm f_th1 f_th2)
- | step ctxt mode _ (_, Metis.Proof.Refl f_tm) = refl_inf ctxt mode f_tm
- | step ctxt mode _ (_, Metis.Proof.Equality (f_lit, f_p, f_r)) =
- equality_inf ctxt mode f_lit f_p f_r;
+fun step ctxt mode skolem_somes 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 skolem_somes f_atm
+ | (_, Metis.Proof.Subst (f_subst, f_th1)) =>
+ factor (inst_inf ctxt mode skolem_somes thpairs f_subst f_th1)
+ | (_, Metis.Proof.Resolve(f_atm, f_th1, f_th2)) =>
+ factor (resolve_inf ctxt mode skolem_somes thpairs f_atm f_th1 f_th2)
+ | (_, Metis.Proof.Refl f_tm) => refl_inf ctxt mode skolem_somes f_tm
+ | (_, Metis.Proof.Equality (f_lit, f_p, f_r)) =>
+ equality_inf ctxt mode skolem_somes f_lit f_p f_r
fun real_literal (_, (c, _)) = not (String.isPrefix class_prefix c);
-fun translate _ _ thpairs [] = thpairs
- | translate mode ctxt thpairs ((fol_th, inf) :: infpairs) =
+(* TODO: use "fold" instead *)
+fun translate _ _ _ thpairs [] = thpairs
+ | translate ctxt mode skolem_somes thpairs ((fol_th, inf) :: infpairs) =
let val _ = trace_msg (fn () => "=============================================")
val _ = trace_msg (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th)
val _ = trace_msg (fn () => "INFERENCE: " ^ Metis.Proof.inferenceToString inf)
- val th = Meson.flexflex_first_order (step ctxt mode thpairs (fol_th, inf))
+ val th = Meson.flexflex_first_order (step ctxt mode skolem_somes
+ thpairs (fol_th, inf))
val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
val _ = trace_msg (fn () => "=============================================")
val n_metis_lits =
@@ -564,7 +602,7 @@
in
if nprems_of th = n_metis_lits then ()
else error "Metis: proof reconstruction has gone wrong";
- translate mode ctxt ((fol_th, th) :: thpairs) infpairs
+ translate ctxt mode skolem_somes ((fol_th, th) :: thpairs) infpairs
end;
(*Determining which axiom clauses are actually used*)
@@ -592,7 +630,8 @@
type logic_map =
{axioms: (Metis.Thm.thm * thm) list,
- tfrees: type_literal list};
+ tfrees: type_literal list,
+ skolem_somes: (string * (typ * term list * term)) list}
fun const_in_metis c (pred, tm_list) =
let
@@ -610,14 +649,15 @@
(*transform isabelle type / arity clause to metis clause *)
fun add_type_thm [] lmap = lmap
- | add_type_thm ((ith, mth) :: cls) {axioms, tfrees} =
- add_type_thm cls {axioms = (mth, ith) :: axioms,
- tfrees = tfrees}
+ | add_type_thm ((ith, mth) :: cls) {axioms, tfrees, skolem_somes} =
+ add_type_thm cls {axioms = (mth, ith) :: axioms, tfrees = tfrees,
+ skolem_somes = skolem_somes}
(*Insert non-logical axioms corresponding to all accumulated TFrees*)
-fun add_tfrees {axioms, tfrees} : logic_map =
- {axioms = (map (fn tf => (metis_of_tfree tf, TrueI)) (distinct op= tfrees)) @ axioms,
- tfrees = tfrees};
+fun add_tfrees {axioms, tfrees, skolem_somes} : logic_map =
+ {axioms = map (rpair TrueI o metis_of_tfree) (distinct (op =) tfrees) @
+ axioms,
+ tfrees = tfrees, skolem_somes = skolem_somes}
fun string_of_mode FO = "FO"
| string_of_mode HO = "HO"
@@ -628,18 +668,26 @@
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 (Meson.is_fol_term thy o prop_of) (cls@ths) then FO else HO
+ | set_mode HO =
+ if forall (is_quasi_fol_term thy o prop_of) (cls @ ths) then FO
+ else HO
| set_mode FT = FT
val mode = set_mode mode0
(*transform isabelle clause to metis clause *)
- fun add_thm is_conjecture ith {axioms, tfrees} : logic_map =
- let val (mth, tfree_lits) = hol_thm_to_fol is_conjecture ctxt mode ith
+ fun add_thm is_conjecture ith {axioms, tfrees, skolem_somes} : logic_map =
+ let
+ val (mth, tfree_lits, skolem_somes) =
+ hol_thm_to_fol is_conjecture ctxt mode (length axioms) skolem_somes
+ ith
in
{axioms = (mth, Meson.make_meta_clause ith) :: axioms,
- tfrees = union (op =) tfree_lits tfrees}
+ tfrees = union (op =) tfree_lits tfrees,
+ skolem_somes = skolem_somes}
end;
- val lmap0 = fold (add_thm true) cls {axioms = [], tfrees = init_tfrees ctxt}
- val lmap = fold (add_thm false) ths (add_tfrees lmap0)
+ val lmap = {axioms = [], tfrees = init_tfrees ctxt, skolem_somes = []}
+ |> fold (add_thm true) cls
+ |> add_tfrees
+ |> fold (add_thm false) ths
val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap)
fun used c = exists (Metis.LiteralSet.exists (const_in_metis c o #2)) clause_lists
(*Now check for the existence of certain combinators*)
@@ -649,10 +697,11 @@
val thC = if used "c_COMBC" then [cnf_th @{theory} @{thm COMBC_def}] else []
val thS = if used "c_COMBS" then [cnf_th @{theory} @{thm COMBS_def}] else []
val thEQ = if used "c_fequal" then [cnf_th @{theory} @{thm fequal_imp_equal}, cnf_th @{theory} @{thm equal_imp_fequal}] else []
- val lmap' = if mode=FO then lmap
- else fold (add_thm false) (thEQ @ thS @ thC @ thB @ thK @ thI) lmap
+ val lmap =
+ lmap |> mode <> FO
+ ? fold (add_thm false) (thEQ @ thS @ thC @ thB @ thK @ thI)
in
- (mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap')
+ (mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap)
end;
fun refute cls =
@@ -664,7 +713,7 @@
exception METIS of string;
-(* Main function to start metis prove and reconstruction *)
+(* Main function to start metis proof and reconstruction *)
fun FOL_SOLVE mode ctxt cls ths0 =
let val thy = ProofContext.theory_of ctxt
val th_cls_pairs =
@@ -674,7 +723,7 @@
val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls
val _ = trace_msg (fn () => "THEOREM CLAUSES")
val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) ths
- val (mode, {axioms,tfrees}) = build_map mode ctxt cls ths
+ val (mode, {axioms, tfrees, skolem_somes}) = build_map mode ctxt cls ths
val _ = if null tfrees then ()
else (trace_msg (fn () => "TFREE CLAUSES");
app (fn tf => trace_msg (fn _ => tptp_of_type_literal true tf NONE |> fst)) tfrees)
@@ -694,7 +743,7 @@
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 = translate mode ctxt' axioms proof
+ val result = translate ctxt' mode skolem_somes axioms proof
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
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Fri Jun 11 17:07:27 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Fri Jun 11 17:10:23 2010 +0200
@@ -21,6 +21,7 @@
val tvar_classes_of_terms : term list -> string list
val tfree_classes_of_terms : term list -> string list
val type_consts_of_terms : theory -> term list -> string list
+ val is_quasi_fol_term : theory -> term -> bool
val relevant_facts :
bool -> bool -> real -> real -> bool -> int -> bool -> relevance_override
-> Proof.context * (thm list * 'a) -> thm list
@@ -116,6 +117,8 @@
add_const_typ_table (const_with_typ thy (c,typ), tab)
| add_term_consts_typs_rm thy (Free(c, typ), tab) =
add_const_typ_table (const_with_typ thy (c,typ), tab)
+ | add_term_consts_typs_rm _ (Const (@{const_name skolem_Eps}, _) $ _, tab) =
+ tab
| add_term_consts_typs_rm thy (t $ u, tab) =
add_term_consts_typs_rm thy (t, add_term_consts_typs_rm thy (u, tab))
| add_term_consts_typs_rm thy (Abs(_,_,t), tab) = add_term_consts_typs_rm thy (t, tab)
@@ -368,38 +371,35 @@
fun valid_facts facts =
(facts, []) |-> Facts.fold_static (fn (name, ths0) =>
- let
- fun check_thms a =
- (case try (ProofContext.get_thms ctxt) a of
- NONE => false
- | SOME ths1 => Thm.eq_thms (ths0, ths1));
+ if Facts.is_concealed facts name orelse
+ (respect_no_atp andalso is_package_def name) orelse
+ member (op =) multi_base_blacklist (Long_Name.base_name name) then
+ I
+ else
+ let
+ fun check_thms a =
+ (case try (ProofContext.get_thms ctxt) a of
+ NONE => false
+ | SOME ths1 => Thm.eq_thms (ths0, ths1));
- val name1 = Facts.extern facts name;
- val name2 = Name_Space.extern full_space name;
- val ths = filter_out is_theorem_bad_for_atps ths0;
- in
- if Facts.is_concealed facts name orelse
- (respect_no_atp andalso is_package_def name) then
- I
- else case find_first check_thms [name1, name2, name] of
- NONE => I
- | SOME name' =>
- cons (name' |> forall (member Thm.eq_thm chained_ths) ths
- ? prefix chained_prefix, ths)
- end);
+ val name1 = Facts.extern facts name;
+ val name2 = Name_Space.extern full_space name;
+ val ths = filter_out is_theorem_bad_for_atps ths0;
+ in
+ case find_first check_thms [name1, name2, name] of
+ NONE => I
+ | SOME name' =>
+ cons (name' |> forall (member Thm.eq_thm chained_ths) ths
+ ? prefix chained_prefix, ths)
+ end)
in valid_facts global_facts @ valid_facts local_facts end;
fun multi_name a th (n, pairs) =
(n + 1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs);
-fun add_single_names (a, []) pairs = pairs
- | add_single_names (a, [th]) pairs = (a, th) :: pairs
- | add_single_names (a, ths) pairs = #2 (fold (multi_name a) ths (1, pairs));
-
-(*Ignore blacklisted basenames*)
-fun add_multi_names (a, ths) pairs =
- if member (op =) multi_base_blacklist (Long_Name.base_name a) then pairs
- else add_single_names (a, ths) pairs;
+fun add_names (a, []) pairs = pairs
+ | add_names (a, [th]) pairs = (a, th) :: pairs
+ | add_names (a, ths) pairs = #2 (fold (multi_name a) ths (1, pairs))
fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;
@@ -408,8 +408,7 @@
fun name_thm_pairs respect_no_atp ctxt name_thms_pairs =
let
val (mults, singles) = List.partition is_multi name_thms_pairs
- val ps = [] |> fold add_single_names singles
- |> fold add_multi_names mults
+ val ps = [] |> fold add_names singles |> fold add_names mults
in ps |> respect_no_atp ? filter_out (No_ATPs.member ctxt o snd) end;
fun is_named ("", th) =
@@ -472,8 +471,11 @@
(* ATP invocation methods setup *)
(***************************************************************)
+fun is_quasi_fol_term thy = Meson.is_fol_term thy o snd o kill_skolem_Eps ~1 []
+
(*Ensures that no higher-order theorems "leak out"*)
-fun restrict_to_logic thy true cls = filter (Meson.is_fol_term thy o prop_of o fst) cls
+fun restrict_to_logic thy true cls =
+ filter (is_quasi_fol_term thy o prop_of o fst) cls
| restrict_to_logic thy false cls = cls;
(**** Predicates to detect unwanted clauses (prolific or likely to cause
@@ -531,7 +533,7 @@
fun remove_dangerous_clauses full_types add_thms =
filter_out (is_dangerous_theorem full_types add_thms o fst)
-fun is_first_order thy = forall (Meson.is_fol_term thy) o map prop_of
+fun is_fol_goal thy = forall (Meson.is_fol_term thy) o map prop_of
fun relevant_facts full_types respect_no_atp relevance_threshold
relevance_convergence defs_relevant max_new theory_relevant
@@ -542,17 +544,17 @@
else
let
val thy = ProofContext.theory_of ctxt
- val add_thms = cnf_for_facts ctxt add
val has_override = not (null add) orelse not (null del)
- val is_FO = is_first_order thy goal_cls
+ val is_FO = is_fol_goal thy goal_cls
val axioms =
- checked_name_thm_pairs respect_no_atp ctxt
+ checked_name_thm_pairs (respect_no_atp andalso not only) ctxt
(if only then map (name_thms_pair_from_ref ctxt chained_ths) add
else all_name_thms_pairs respect_no_atp ctxt chained_ths)
|> cnf_rules_pairs thy
|> not has_override ? make_unique
- |> restrict_to_logic thy is_FO
- |> not only ? remove_dangerous_clauses full_types add_thms
+ |> not only ? restrict_to_logic thy is_FO
+ |> (if only then I
+ else remove_dangerous_clauses full_types (cnf_for_facts ctxt add))
in
relevance_filter ctxt relevance_threshold relevance_convergence
defs_relevant max_new theory_relevant relevance_override
@@ -564,7 +566,7 @@
create additional clauses based on the information from extra_cls *)
fun prepare_clauses dfg goal_cls chained_ths axcls extra_cls thy =
let
- val is_FO = is_first_order thy goal_cls
+ val is_FO = is_fol_goal thy goal_cls
val ccls = subtract_cls extra_cls goal_cls
val _ = app (fn th => trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
val ccltms = map prop_of ccls
@@ -576,7 +578,7 @@
val conjectures = make_conjecture_clauses dfg thy ccls
val (_, extra_clauses) = ListPair.unzip (make_axiom_clauses dfg thy extra_cls)
val (clnames, axiom_clauses) = ListPair.unzip (make_axiom_clauses dfg thy axcls)
- val helper_clauses = get_helper_clauses dfg thy is_FO (conjectures, extra_cls, [])
+ val helper_clauses = get_helper_clauses dfg thy is_FO conjectures extra_cls
val (supers', arity_clauses) = make_arity_clauses_dfg dfg thy tycons supers
val classrel_clauses = make_classrel_clauses thy subs supers'
in
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Fri Jun 11 17:07:27 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Fri Jun 11 17:10:23 2010 +0200
@@ -10,8 +10,11 @@
val chained_prefix: string
val trace: bool Unsynchronized.ref
val trace_msg: (unit -> string) -> unit
+ val skolem_Eps_pseudo_theory: string
val skolem_prefix: string
val skolem_infix: string
+ val is_skolem_const_name: string -> bool
+ val skolem_type_and_args: typ -> term -> typ * term list
val cnf_axiom: theory -> thm -> thm list
val multi_base_blacklist: string list
val is_theorem_bad_for_atps: thm -> bool
@@ -39,6 +42,7 @@
val trace = Unsynchronized.ref false;
fun trace_msg msg = if !trace then tracing (msg ()) else ();
+val skolem_Eps_pseudo_theory = "Sledgehammer.Eps"
val skolem_prefix = "sko_"
val skolem_infix = "$"
@@ -72,13 +76,22 @@
(**** SKOLEMIZATION BY INFERENCE (lcp) ****)
+fun skolem_Eps_const T =
+ Const (@{const_name skolem_Eps}, (T --> HOLogic.boolT) --> T)
+
(*Keep the full complexity of the original name*)
fun flatten_name s = space_implode "_X" (Long_Name.explode s);
-fun skolem_name thm_name nref var_name =
- skolem_prefix ^ thm_name ^ "_" ^ Int.toString (Unsynchronized.inc nref) ^
+fun skolem_name thm_name j var_name =
+ skolem_prefix ^ thm_name ^ "_" ^ Int.toString j ^
skolem_infix ^ (if var_name = "" then "g" else flatten_name var_name)
+(* Hack: Could return false positives (e.g., a user happens to declare a
+ constant called "SomeTheory.sko_means_shoe_in_$wedish". *)
+val is_skolem_const_name =
+ Long_Name.base_name
+ #> String.isPrefix skolem_prefix andf String.isSubstring skolem_infix
+
fun rhs_extra_types lhsT rhs =
let val lhs_vars = Term.add_tfreesT lhsT []
fun add_new_TFrees (TFree v) =
@@ -87,34 +100,39 @@
val rhs_consts = fold_aterms (fn Const c => insert (op =) c | _ => I) rhs []
in fold (#2 #> Term.fold_atyps add_new_TFrees) rhs_consts [] end;
+fun skolem_type_and_args bound_T body =
+ let
+ val args1 = OldTerm.term_frees body
+ val Ts1 = map type_of args1
+ val Ts2 = rhs_extra_types (Ts1 ---> bound_T) body
+ val args2 = map (fn T => Free (gensym "vsk", T)) Ts2
+ in (Ts2 ---> Ts1 ---> bound_T, args2 @ args1) end
+
(* Traverse a theorem, declaring Skolem function definitions. String "s" is the
suggested prefix for the Skolem constants. *)
fun declare_skolem_funs s th thy =
let
- val nref = Unsynchronized.ref 0 (* FIXME ??? *)
- fun dec_sko (Const (@{const_name Ex}, _) $ (xtp as Abs (s', T, p))) (axs, thy) =
- (*Existential: declare a Skolem function, then insert into body and continue*)
- let
- val cname = skolem_name s nref s'
- val args0 = OldTerm.term_frees xtp (*get the formal parameter list*)
- val Ts = map type_of args0
- val extraTs = rhs_extra_types (Ts ---> T) xtp
- val argsx = map (fn T => Free (gensym "vsk", T)) extraTs
- val args = argsx @ args0
- val cT = extraTs ---> Ts ---> T
- val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp)
- (*Forms a lambda-abstraction over the formal parameters*)
- val (c, thy) =
- Sign.declare_const ((Binding.conceal (Binding.name cname), cT), NoSyn) thy
- val cdef = cname ^ "_def"
- val ((_, ax), thy) =
- Thm.add_def true false (Binding.name cdef, Logic.mk_equals (c, rhs)) thy
- val ax' = Drule.export_without_context ax
- in dec_sko (subst_bound (list_comb (c, args), p)) (ax' :: axs, thy) end
+ val skolem_count = Unsynchronized.ref 0 (* FIXME ??? *)
+ fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (s', T, p)))
+ (axs, thy) =
+ (*Existential: declare a Skolem function, then insert into body and continue*)
+ let
+ val id = skolem_name s (Unsynchronized.inc skolem_count) s'
+ val (cT, args) = skolem_type_and_args T body
+ val rhs = list_abs_free (map dest_Free args,
+ skolem_Eps_const T $ body)
+ (*Forms a lambda-abstraction over the formal parameters*)
+ val (c, thy) =
+ Sign.declare_const ((Binding.conceal (Binding.name id), cT), NoSyn) thy
+ val cdef = id ^ "_def"
+ val ((_, ax), thy) =
+ Thm.add_def true false (Binding.name cdef, Logic.mk_equals (c, rhs)) thy
+ val ax' = Drule.export_without_context ax
+ in dec_sko (subst_bound (list_comb (c, args), p)) (ax' :: axs, thy) end
| dec_sko (Const (@{const_name All}, _) $ (Abs (a, T, p))) thx =
- (*Universal quant: insert a free variable into body and continue*)
- let val fname = Name.variant (OldTerm.add_term_names (p, [])) a
- in dec_sko (subst_bound (Free (fname, T), p)) thx end
+ (*Universal quant: insert a free variable into body and continue*)
+ let val fname = Name.variant (OldTerm.add_term_names (p, [])) a
+ in dec_sko (subst_bound (Free (fname, T), p)) thx end
| dec_sko (@{const "op &"} $ p $ q) thx = dec_sko q (dec_sko p thx)
| dec_sko (@{const "op |"} $ p $ q) thx = dec_sko q (dec_sko p thx)
| dec_sko (@{const Trueprop} $ p) thx = dec_sko p thx
@@ -122,29 +140,31 @@
in dec_sko (prop_of th) ([], thy) end
(*Traverse a theorem, accumulating Skolem function definitions.*)
-fun assume_skolem_funs s th =
- let val sko_count = Unsynchronized.ref 0 (* FIXME ??? *)
- fun dec_sko (Const (@{const_name Ex}, _) $ (xtp as Abs (s', T, p))) defs =
- (*Existential: declare a Skolem function, then insert into body and continue*)
- let val skos = map (#1 o Logic.dest_equals) defs (*existing sko fns*)
- val args = subtract (op =) skos (OldTerm.term_frees xtp) (*the formal parameters*)
- val Ts = map type_of args
- val cT = Ts ---> T
- val id = skolem_name s sko_count s'
- val c = Free (id, cT)
- val rhs = list_abs_free (map dest_Free args,
- HOLogic.choice_const T $ xtp)
- (*Forms a lambda-abstraction over the formal parameters*)
- val def = Logic.mk_equals (c, rhs)
- in dec_sko (subst_bound (list_comb(c,args), p)) (def :: defs) end
- | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) defs =
- (*Universal quant: insert a free variable into body and continue*)
- let val fname = Name.variant (OldTerm.add_term_names (p,[])) a
- in dec_sko (subst_bound (Free(fname,T), p)) defs end
- | dec_sko (@{const "op &"} $ p $ q) defs = dec_sko q (dec_sko p defs)
- | dec_sko (@{const "op |"} $ p $ q) defs = dec_sko q (dec_sko p defs)
- | dec_sko (@{const Trueprop} $ p) defs = dec_sko p defs
- | dec_sko t defs = defs (*Do nothing otherwise*)
+fun assume_skolem_funs inline s th =
+ let
+ val skolem_count = Unsynchronized.ref 0 (* FIXME ??? *)
+ fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (s', T, p))) defs =
+ (*Existential: declare a Skolem function, then insert into body and continue*)
+ let
+ val skos = map (#1 o Logic.dest_equals) defs (*existing sko fns*)
+ val args = subtract (op =) skos (OldTerm.term_frees body) (*the formal parameters*)
+ val Ts = map type_of args
+ val cT = Ts ---> T (* FIXME: use "skolem_type_and_args" *)
+ val id = skolem_name s (Unsynchronized.inc skolem_count) s'
+ val c = Free (id, cT)
+ val rhs = list_abs_free (map dest_Free args, skolem_Eps_const T $ body)
+ (*Forms a lambda-abstraction over the formal parameters*)
+ val def = Logic.mk_equals (c, rhs)
+ val comb = list_comb (if inline then rhs else c, args)
+ in dec_sko (subst_bound (comb, p)) (def :: defs) end
+ | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) defs =
+ (*Universal quant: insert a free variable into body and continue*)
+ let val fname = Name.variant (OldTerm.add_term_names (p,[])) a
+ in dec_sko (subst_bound (Free(fname,T), p)) defs end
+ | dec_sko (@{const "op &"} $ p $ q) defs = dec_sko q (dec_sko p defs)
+ | dec_sko (@{const "op |"} $ p $ q) defs = dec_sko q (dec_sko p defs)
+ | dec_sko (@{const Trueprop} $ p) defs = dec_sko p defs
+ | dec_sko t defs = defs (*Do nothing otherwise*)
in dec_sko (prop_of th) [] end;
@@ -273,19 +293,25 @@
(*Given the definition of a Skolem function, return a theorem to replace
an existential formula by a use of that function.
Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B" [.] *)
-fun skolem_of_def def =
- let val (c,rhs) = Thm.dest_equals (cprop_of (freeze_thm def))
+fun skolem_theorem_of_def inline def =
+ let
+ val (c,rhs) = Thm.dest_equals (cprop_of (freeze_thm def))
val (ch, frees) = c_variant_abs_multi (rhs, [])
val (chilbert,cabs) = Thm.dest_comb ch
val thy = Thm.theory_of_cterm chilbert
val t = Thm.term_of chilbert
- val T = case t of
- Const (@{const_name Eps}, Type (@{type_name fun},[_,T])) => T
- | _ => raise THM ("skolem_of_def: expected Eps", 0, [def])
+ val T =
+ case t of
+ Const (@{const_name skolem_Eps}, Type (@{type_name fun}, [_, T])) => T
+ | _ => raise THM ("skolem_theorem_of_def: expected \"Eps\"", 0, [def])
val cex = Thm.cterm_of thy (HOLogic.exists_const T)
val ex_tm = c_mkTrueprop (Thm.capply cex cabs)
- and conc = c_mkTrueprop (Drule.beta_conv cabs (Drule.list_comb(c,frees)));
- fun tacf [prem] = rewrite_goals_tac [def] THEN rtac (prem RS @{thm someI_ex}) 1
+ and conc =
+ Drule.list_comb (if inline then rhs else c, frees)
+ |> Drule.beta_conv cabs |> c_mkTrueprop
+ fun tacf [prem] =
+ (if inline then all_tac else rewrite_goals_tac [def])
+ THEN rtac (prem RS @{thm skolem_someI_ex}) 1
in Goal.prove_internal [ex_tm] conc tacf
|> forall_intr_list frees
|> Thm.forall_elim_vars 0 (*Introduce Vars, but don't discharge defs.*)
@@ -303,9 +329,9 @@
in (th3, ctxt) end;
(*Generate Skolem functions for a theorem supplied in nnf*)
-fun assume_skolem_of_def s th =
- map (skolem_of_def o Thm.assume o cterm_of (theory_of_thm th))
- (assume_skolem_funs s th)
+fun skolem_theorems_of_assume inline s th =
+ map (skolem_theorem_of_def inline o Thm.assume o cterm_of (theory_of_thm th))
+ (assume_skolem_funs inline s th)
(*** Blacklisting (more in "Sledgehammer_Fact_Filter") ***)
@@ -364,7 +390,7 @@
else gensym "unknown_thm_";
(*Skolemize a named theorem, with Skolem functions as additional premises.*)
-fun skolem_thm (s, th) =
+fun skolemize_theorem s th =
if member (op =) multi_base_blacklist (Long_Name.base_name s) orelse
is_theorem_bad_for_atps th then
[]
@@ -372,7 +398,8 @@
let
val ctxt0 = Variable.global_thm_context th
val (nnfth, ctxt) = to_nnf th ctxt0
- val defs = assume_skolem_of_def s nnfth
+ val inline = exists_type (exists_subtype (can dest_TFree)) (prop_of nnfth)
+ val defs = skolem_theorems_of_assume inline s nnfth
val (cnfs, ctxt) = Meson.make_cnf defs nnfth ctxt
in
cnfs |> map introduce_combinators
@@ -402,7 +429,7 @@
fun cnf_axiom thy th0 =
let val th = Thm.transfer thy th0 in
case lookup_cache thy th of
- NONE => map Thm.close_derivation (skolem_thm (fake_name th, th))
+ NONE => map Thm.close_derivation (skolemize_theorem (fake_name th) th)
| SOME cls => cls
end;
@@ -438,7 +465,8 @@
fun skolem_cnfs (th, ctxt0, ctxt, nnfth, defs) =
let
- val (cnfs, ctxt) = Meson.make_cnf (map skolem_of_def defs) nnfth ctxt;
+ val (cnfs, ctxt) =
+ Meson.make_cnf (map (skolem_theorem_of_def false) defs) nnfth ctxt
val cnfs' = cnfs
|> map introduce_combinators
|> Variable.export ctxt ctxt0
@@ -455,14 +483,17 @@
if Facts.is_concealed facts name orelse already_seen thy name then I
else cons (name, ths));
val new_thms = (new_facts, []) |-> fold (fn (name, ths) =>
- if member (op =) multi_base_blacklist (Long_Name.base_name name) then I
- else fold_index (fn (i, th) =>
- if is_theorem_bad_for_atps th orelse is_some (lookup_cache thy th) then
- I
- else
- cons (name ^ "_" ^ string_of_int (i + 1), Thm.transfer thy th)) ths)
+ if member (op =) multi_base_blacklist (Long_Name.base_name name) then
+ I
+ else
+ fold_index (fn (i, th) =>
+ if is_theorem_bad_for_atps th orelse is_some (lookup_cache thy th) then
+ I
+ else
+ cons (name ^ "_" ^ string_of_int (i + 1), Thm.transfer thy th)) ths)
in
- if null new_facts then NONE
+ if null new_facts then
+ NONE
else
let
val (defs, thy') = thy
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Fri Jun 11 17:07:27 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Fri Jun 11 17:10:23 2010 +0200
@@ -29,14 +29,17 @@
val type_of_combterm : combterm -> fol_type
val strip_combterm_comb : combterm -> combterm * combterm list
val literals_of_term : theory -> term -> literal list * typ list
+ val kill_skolem_Eps :
+ int -> (string * (typ * term list * term)) list -> term
+ -> (string * (typ * term list * term)) list * term
exception TRIVIAL
val make_conjecture_clauses : bool -> theory -> thm list -> hol_clause list
val make_axiom_clauses : bool -> theory ->
(thm * (axiom_name * hol_clause_id)) list -> (axiom_name * hol_clause) list
val type_wrapper_name : string
- val get_helper_clauses : bool -> theory -> bool ->
- hol_clause list * (thm * (axiom_name * hol_clause_id)) list * string list ->
- hol_clause list
+ val get_helper_clauses :
+ bool -> theory -> bool -> hol_clause list
+ -> (thm * (axiom_name * hol_clause_id)) list -> hol_clause list
val write_tptp_file : bool -> bool -> bool -> Path.T ->
hol_clause list * hol_clause list * hol_clause list * hol_clause list *
classrel_clause list * arity_clause list -> name_pool option * int
@@ -115,28 +118,31 @@
TyVar (make_schematic_type_var x, string_of_indexname x);
-fun const_type_of dfg thy (c,t) =
- let val (tp,ts) = type_of dfg t
- in (tp, ts, map (simp_type_of dfg) (Sign.const_typargs thy (c,t))) end;
-
(* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
-fun combterm_of dfg thy (Const(c,t)) =
- let val (tp,ts,tvar_list) = const_type_of dfg thy (c,t)
- val c' = CombConst (`(make_fixed_const dfg) c, tp, tvar_list)
+fun combterm_of dfg thy (Const (c, T)) =
+ let
+ val (tp, ts) = type_of dfg T
+ val tvar_list =
+ (if String.isPrefix skolem_Eps_pseudo_theory c then
+ [] |> Term.add_tvarsT T |> map TVar
+ else
+ (c, T) |> Sign.const_typargs thy)
+ |> map (simp_type_of dfg)
+ val c' = CombConst (`(make_fixed_const dfg) c, tp, tvar_list)
in (c',ts) end
- | combterm_of dfg _ (Free(v,t)) =
- let val (tp,ts) = type_of dfg t
+ | combterm_of dfg _ (Free(v, T)) =
+ let val (tp,ts) = type_of dfg T
val v' = CombConst (`make_fixed_var v, tp, [])
in (v',ts) end
- | combterm_of dfg _ (Var(v,t)) =
- let val (tp,ts) = type_of dfg t
+ | combterm_of dfg _ (Var(v, T)) =
+ let val (tp,ts) = type_of dfg T
val v' = CombVar ((make_schematic_var v, string_of_indexname v), tp)
in (v',ts) end
| combterm_of dfg thy (P $ Q) =
let val (P',tsP) = combterm_of dfg thy P
val (Q',tsQ) = combterm_of dfg thy Q
in (CombApp(P',Q'), union (op =) tsP tsQ) end
- | combterm_of _ _ (t as Abs _) = raise CLAUSE ("HOL CLAUSE", t);
+ | combterm_of _ _ (t as Abs _) = raise CLAUSE ("HOL clause", t);
fun predicate_of dfg thy ((@{const Not} $ P), polarity) = predicate_of dfg thy (P, not polarity)
| predicate_of dfg thy (t,polarity) = (combterm_of dfg thy (Envir.eta_contract t), polarity);
@@ -153,36 +159,100 @@
fun literals_of_term_dfg dfg thy P = literals_of_term1 dfg thy ([],[]) P;
val literals_of_term = literals_of_term_dfg false;
+fun skolem_name i j num_T_args =
+ skolem_prefix ^ (space_implode "_" (map Int.toString [i, j, num_T_args])) ^
+ skolem_infix ^ "g"
+
+val flip_type =
+ map_atyps (fn TFree (s, S) => TVar ((s, 0), S)
+ | TVar ((s, 0), S) => TFree (s, S)
+ | T as TVar (_, S) => raise TYPE ("nonzero TVar", [T], [])
+ | T => T)
+val flip_term =
+ map_aterms (fn Free (s, T) => Var ((s, 0), T)
+ | Var ((s, 0), T) => Free (s, T)
+ | t as Var (_, S) => raise TERM ("nonzero Var", [t])
+ | t => t)
+ #> map_types flip_type
+
+fun flipped_skolem_type_and_args bound_T body =
+ skolem_type_and_args (flip_type bound_T) (flip_term body)
+ |>> flip_type ||> map flip_term
+
+fun triple_aconv ((T1, ts1, t1), (T2, ts2, t2)) =
+ T1 = T2 andalso length ts1 = length ts2 andalso
+ forall (op aconv) (ts1 ~~ ts2) andalso t1 aconv t2
+
+fun kill_skolem_Eps i skolem_somes t =
+ if exists_Const (curry (op =) @{const_name skolem_Eps} o fst) t then
+ let
+ fun aux skolem_somes
+ (t as (Const (@{const_name skolem_Eps}, eps_T) $ t2)) =
+ let
+ val bound_T = range_type eps_T
+ val (T, args) = flipped_skolem_type_and_args bound_T t2
+ val (skolem_somes, s) =
+ if i = ~1 then
+ (skolem_somes, @{const_name undefined})
+ else case AList.find triple_aconv skolem_somes (T, args, t) of
+ s :: _ => (skolem_somes, s)
+ | _ =>
+ let
+ val s = skolem_Eps_pseudo_theory ^ "." ^
+ skolem_name i (length skolem_somes)
+ (length (Term.add_tvarsT T []))
+ in ((s, (T, args, t)) :: skolem_somes, s) end
+ in (skolem_somes, list_comb (Const (s, T), args)) end
+ | aux skolem_somes (t1 $ t2) =
+ let
+ val (skolem_somes, t1) = aux skolem_somes t1
+ val (skolem_somes, t2) = aux skolem_somes t2
+ in (skolem_somes, t1 $ t2) end
+ | aux skolem_somes (Abs (s, T, t')) =
+ let val (skolem_somes, t') = aux skolem_somes t' in
+ (skolem_somes, Abs (s, T, t'))
+ end
+ | aux skolem_somes t = (skolem_somes, t)
+ in aux skolem_somes t end
+ else
+ (skolem_somes, t)
+
(* Trivial problem, which resolution cannot handle (empty clause) *)
exception TRIVIAL;
(* making axiom and conjecture clauses *)
-fun make_clause dfg thy (clause_id, axiom_name, kind, th) =
- let val (lits,ctypes_sorts) = literals_of_term_dfg dfg thy (prop_of th)
- in
- if forall isFalse lits then
- raise TRIVIAL
- else
- HOLClause {clause_id = clause_id, axiom_name = axiom_name, th = th,
- kind = kind, literals = lits, ctypes_sorts = ctypes_sorts}
- end;
-
-
-fun add_axiom_clause dfg thy (th, (name, id)) =
- let val cls = make_clause dfg thy (id, name, Axiom, th) in
- not (isTaut cls) ? cons (name, cls)
+fun make_clause dfg thy (clause_id, axiom_name, kind, th) skolem_somes =
+ let
+ val (skolem_somes, t) =
+ th |> prop_of |> kill_skolem_Eps clause_id skolem_somes
+ val (lits, ctypes_sorts) = literals_of_term_dfg dfg thy t
+ in
+ if forall isFalse lits then
+ raise TRIVIAL
+ else
+ (skolem_somes,
+ HOLClause {clause_id = clause_id, axiom_name = axiom_name, th = th,
+ kind = kind, literals = lits, ctypes_sorts = ctypes_sorts})
end
+fun add_axiom_clause dfg thy (th, (name, id)) (skolem_somes, clss) =
+ let
+ val (skolem_somes, cls) =
+ make_clause dfg thy (id, name, Axiom, th) skolem_somes
+ in (skolem_somes, clss |> not (isTaut cls) ? cons (name, cls)) end
+
fun make_axiom_clauses dfg thy clauses =
- fold (add_axiom_clause dfg thy) clauses []
+ ([], []) |> fold (add_axiom_clause dfg thy) clauses |> snd
-fun make_conjecture_clauses_aux _ _ _ [] = []
- | make_conjecture_clauses_aux dfg thy n (th::ths) =
- make_clause dfg thy (n,"conjecture", Conjecture, th) ::
- make_conjecture_clauses_aux dfg thy (n+1) ths;
-
-fun make_conjecture_clauses dfg thy = make_conjecture_clauses_aux dfg thy 0;
-
+fun make_conjecture_clauses dfg thy =
+ let
+ fun aux _ _ [] = []
+ | aux n skolem_somes (th :: ths) =
+ let
+ val (skolem_somes, cls) =
+ make_clause dfg thy (n, "conjecture", Conjecture, th) skolem_somes
+ in cls :: aux (n + 1) skolem_somes ths end
+ in aux 0 [] end
(**********************************************************************)
(* convert clause into ATP specific formats: *)
@@ -415,19 +485,16 @@
fun count_clause (HOLClause {literals, ...}) = fold count_literal literals
-fun count_user_clause user_lemmas (HOLClause {axiom_name, literals, ...}) =
- member (op =) user_lemmas axiom_name ? fold count_literal literals
-
fun cnf_helper_thms thy = cnf_rules_pairs thy o map (`Thm.get_name_hint)
-fun get_helper_clauses dfg thy isFO (conjectures, axcls, user_lemmas) =
+fun get_helper_clauses dfg thy isFO conjectures axcls =
if isFO then
[]
else
let
- val axclauses = map #2 (make_axiom_clauses dfg thy axcls)
- val ct = init_counters |> fold count_clause conjectures
- |> fold (count_user_clause user_lemmas) axclauses
+ val axclauses = map snd (make_axiom_clauses dfg thy axcls)
+ val ct = init_counters
+ |> fold (fold count_clause) [conjectures, axclauses]
fun needed c = the (Symtab.lookup ct c) > 0
val IK = if needed "c_COMBI" orelse needed "c_COMBK"
then cnf_helper_thms thy [@{thm COMBI_def}, @{thm COMBK_def}]
@@ -439,9 +506,7 @@
else []
val other = cnf_helper_thms thy [@{thm fequal_imp_equal},
@{thm equal_imp_fequal}]
- in
- map #2 (make_axiom_clauses dfg thy (other @ IK @ BC @ S))
- end;
+ in map snd (make_axiom_clauses dfg thy (other @ IK @ BC @ S)) end
(*Find the minimal arity of each function mentioned in the term. Also, note which uses
are not at top level, to see if hBOOL is needed.*)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jun 11 17:07:27 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jun 11 17:10:23 2010 +0200
@@ -345,8 +345,8 @@
>> merge_relevance_overrides))
(add_to_relevance_override [])
val parse_sledgehammer_command =
- (Scan.optional Parse.short_ident runN -- parse_params -- parse_relevance_override
- -- Scan.option Parse.nat) #>> sledgehammer_trans
+ (Scan.optional Parse.short_ident runN -- parse_params
+ -- parse_relevance_override -- Scan.option Parse.nat) #>> sledgehammer_trans
val parse_sledgehammer_params_command =
parse_params #>> sledgehammer_params_trans
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri Jun 11 17:07:27 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri Jun 11 17:10:23 2010 +0200
@@ -41,12 +41,6 @@
fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
fun is_head_digit s = Char.isDigit (String.sub (s, 0))
-(* Hack: Could return false positives (e.g., a user happens to declare a
- constant called "SomeTheory.sko_means_shoe_in_$wedish". *)
-val is_skolem_const_name =
- Long_Name.base_name
- #> String.isPrefix skolem_prefix andf String.isSubstring skolem_infix
-
val index_in_shape : int -> int list list -> int =
find_index o exists o curry (op =)
fun is_axiom_clause_number thm_names num = num <= Vector.length thm_names
@@ -263,9 +257,16 @@
fun invert_const c = c |> Symtab.lookup const_trans_table_inv |> the_default c
-(*The number of type arguments of a constant, zero if it's monomorphic*)
+(* 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 =
- length (Sign.const_typargs thy (s, Sign.the_const_type thy s))
+ if String.isPrefix skolem_Eps_pseudo_theory s then
+ s |> unprefix skolem_Eps_pseudo_theory
+ |> space_explode skolem_infix |> hd
+ |> space_explode "_" |> List.last |> Int.fromString |> the
+ else
+ (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
fun fix_atp_variable_name s =
let
@@ -323,9 +324,12 @@
else
(* Extra args from "hAPP" come after any arguments
given directly to the constant. *)
- Sign.const_instance thy (c,
- map (type_from_node tfrees)
- (drop num_term_args us)))
+ if String.isPrefix skolem_Eps_pseudo_theory c then
+ map fastype_of ts ---> HOLogic.typeT
+ else
+ Sign.const_instance thy (c,
+ map (type_from_node tfrees)
+ (drop num_term_args us)))
in list_comb (t, ts) end
| NONE => (* a free or schematic variable *)
let
@@ -580,16 +584,29 @@
| extract_num (num :: "0" :: "Inp" :: _) = Int.fromString num
| extract_num _ = NONE
in atp_proof |> split_lines |> map_filter (extract_num o tokens_of) end
-
-fun apply_command _ 1 = "by "
- | apply_command 1 _ = "apply "
- | apply_command i _ = "prefer " ^ string_of_int i ^ " apply "
-fun metis_command i n [] = apply_command i n ^ "metis"
- | metis_command i n ss =
- apply_command i n ^ "(metis " ^ space_implode " " ss ^ ")"
-fun metis_line i n xs =
+
+val indent_size = 2
+val no_label = ("", ~1)
+
+val raw_prefix = "X"
+val assum_prefix = "A"
+val fact_prefix = "F"
+
+fun string_for_label (s, num) = s ^ string_of_int num
+
+fun metis_using [] = ""
+ | metis_using ls =
+ "using " ^ space_implode " " (map string_for_label ls) ^ " "
+fun metis_apply _ 1 = "by "
+ | metis_apply 1 _ = "apply "
+ | metis_apply i _ = "prefer " ^ string_of_int i ^ " apply "
+fun metis_itself [] = "metis"
+ | metis_itself ss = "(metis " ^ space_implode " " ss ^ ")"
+fun metis_command i n (ls, ss) =
+ metis_using ls ^ metis_apply i n ^ metis_itself ss
+fun metis_line i n ss =
"Try this command: " ^
- Markup.markup Markup.sendback (metis_command i n xs) ^ ".\n"
+ Markup.markup Markup.sendback (metis_command i n ([], ss)) ^ ".\n"
fun minimize_line _ [] = ""
| minimize_line minimize_command facts =
case minimize_command facts of
@@ -639,15 +656,6 @@
fun smart_case_split [] facts = ByMetis facts
| smart_case_split proofs facts = CaseSplit (proofs, facts)
-val indent_size = 2
-val no_label = ("", ~1)
-
-val raw_prefix = "X"
-val assum_prefix = "A"
-val fact_prefix = "F"
-
-fun string_for_label (s, num) = s ^ string_of_int num
-
fun add_fact_from_dep thm_names num =
if is_axiom_clause_number thm_names num then
apsnd (insert (op =) (Vector.sub (thm_names, num - 1)))
@@ -948,7 +956,7 @@
let
val ls = ls |> sort_distinct (prod_ord string_ord int_ord)
val ss = ss |> map unprefix_chained |> sort_distinct string_ord
- in metis_command 1 1 (map string_for_label ls @ ss) end
+ in metis_command 1 1 (ls, ss) end
and do_step ind (Fix xs) =
do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n"
| do_step ind (Let (t1, t2)) =