--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Mon Dec 16 17:08:22 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Dec 17 09:52:10 2013 +0100
@@ -1958,6 +1958,10 @@
end
in List.partition (curry (op =) Definition o #role) #>> reorder [] #> op @ end
+fun s_not_prop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
+ | s_not_prop (@{const "==>"} $ t $ @{prop False}) = t
+ | s_not_prop t = @{const "==>"} $ t $ @{prop False}
+
fun translate_formulas ctxt prem_role format type_enc lam_trans presimp hyp_ts
concl_t facts =
let
--- a/src/HOL/Tools/ATP/atp_proof.ML Mon Dec 16 17:08:22 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML Tue Dec 17 09:52:10 2013 +0100
@@ -231,8 +231,7 @@
val dummy_phi = AAtom (ATerm (("", []), []))
val dummy_inference = Inference_Source ("", [])
-(* "skip_term" is there to cope with Waldmeister nonsense such as
- "theory(equality)". *)
+(* "skip_term" is there to cope with Waldmeister nonsense such as "theory(equality)". *)
fun parse_dependency x =
(parse_inference_source >> snd
|| scan_general_id --| skip_term >> single) x
@@ -469,8 +468,7 @@
(* Syntax: core(<name>,[<name>,...,<name>]). *)
fun parse_z3_tptp_line x =
(scan_general_id --| $$ "," --| $$ "[" -- parse_dependencies --| $$ "]"
- >> (fn (name, names) =>
- (("", name :: names), Unknown, dummy_phi, z3_tptp_coreN, []))) x
+ >> (fn (name, names) => (("", name :: names), Unknown, dummy_phi, z3_tptp_coreN, []))) x
(* Syntax: <name> *)
fun parse_satallax_line x =
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Mon Dec 16 17:08:22 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Tue Dec 17 09:52:10 2013 +0100
@@ -11,9 +11,11 @@
type ('a, 'b) atp_term = ('a, 'b) ATP_Problem.atp_term
type ('a, 'b, 'c, 'd) atp_formula = ('a, 'b, 'c, 'd) ATP_Problem.atp_formula
type stature = ATP_Problem_Generate.stature
+ type atp_step_name = ATP_Proof.atp_step_name
type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step
type 'a atp_proof = 'a ATP_Proof.atp_proof
+ val spass_skolemize_rule : string
val metisN : string
val full_typesN : string
val partial_typesN : string
@@ -25,6 +27,7 @@
val full_type_encs : string list
val partial_type_encs : string list
val default_metis_lam_trans : string
+
val metis_call : string -> string -> string
val forall_of : term -> term -> term
val exists_of : term -> term -> term
@@ -40,8 +43,11 @@
'a atp_proof -> string list option
val lam_trans_of_atp_proof : string atp_proof -> string -> string
val is_typed_helper_used_in_atp_proof : string atp_proof -> bool
+ val replace_dependencies_in_line : atp_step_name * atp_step_name list -> ('a, 'b) atp_step ->
+ ('a, 'b) atp_step
val termify_atp_proof : Proof.context -> string Symtab.table -> (string * term) list ->
int Symtab.table -> string atp_proof -> (term, string) atp_step list
+ val introduce_spass_skolem : (term, string) atp_step list -> (term, string) atp_step list
val factify_atp_proof : (string * 'a) list vector -> term list -> term ->
(term, string) atp_step list -> (term, string) atp_step list
end;
@@ -54,6 +60,9 @@
open ATP_Proof
open ATP_Problem_Generate
+val spass_input_rule = "Inp"
+val spass_skolemize_rule = "__Sko" (* arbitrary *)
+
val metisN = "metis"
val full_typesN = "full_types"
@@ -174,6 +183,7 @@
fun loose_aconv (Free (s, _), Free (s', _)) = s = s'
| loose_aconv (t, t') = t aconv t'
+val spass_skolem_prefix = "sk" (* "skc" or "skf" *)
val vampire_skolem_prefix = "sK"
(* First-order translation. No types are known for variables. "HOLogic.typeT"
@@ -268,9 +278,10 @@
[(s, ())] |> Variable.variant_frees ctxt [] |> hd |> fst
val term_ts =
map (do_term [] NONE) us
- (* Vampire (2.6) passes arguments to Skolem functions in reverse
- order *)
- |> String.isPrefix vampire_skolem_prefix s ? rev
+ (* SPASS (3.8ds) and Vampire (2.6) pass arguments to Skolem functions in reverse
+ order, which is incompatible with the new Metis skolemizer. *)
+ |> exists (fn pre => String.isPrefix pre s)
+ [spass_skolem_prefix, vampire_skolem_prefix] ? rev
val ts = term_ts @ extra_ts
val T =
case opt_T of
@@ -334,9 +345,8 @@
| AQuant (q, (s, _) :: xs, phi') =>
do_formula pos (AQuant (q, xs, phi'))
(* FIXME: TFF *)
- #>> quantify_over_var
- (case q of AForall => forall_of | AExists => exists_of)
- (s |> textual ? repair_var_name)
+ #>> quantify_over_var (case q of AForall => forall_of | AExists => exists_of)
+ (s |> textual ? repair_var_name)
| AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not
| AConn (c, [phi1, phi2]) =>
do_formula (pos |> c = AImplies ? not) phi1
@@ -452,6 +462,10 @@
fun is_typed_helper_used_in_atp_proof atp_proof =
is_axiom_used_in_proof is_typed_helper_name atp_proof
+fun replace_one_dependency (old, new) dep = if is_same_atp_step dep old then new else [dep]
+fun replace_dependencies_in_line old_new (name, role, t, rule, deps) =
+ (name, role, t, rule, fold (union (op =) o replace_one_dependency old_new) deps [])
+
fun repair_name "$true" = "c_True"
| repair_name "$false" = "c_False"
| repair_name "$$e" = tptp_equal (* seen in Vampire proofs *)
@@ -529,6 +543,58 @@
#> map (termify_line ctxt lifted sym_tab)
#> repair_waldmeister_endgame
+fun introduce_spass_skolem [] = []
+ | introduce_spass_skolem (proof as (_, _, _, rule1, _) :: _) =
+ if rule1 = spass_input_rule then
+ let
+ fun add_sko (Free (s, _)) = String.isPrefix spass_skolem_prefix s ? insert (op =) s
+ | add_sko _ = I
+
+ (* union-find would be faster *)
+ fun add_cycle _ [] = I
+ | add_cycle name ss =
+ fold (fn s => Graph.default_node (s, ())) ss
+ #> fold Graph.add_edge (ss ~~ tl ss @ [hd ss])
+
+ val (input_steps, other_steps) = List.partition (null o #5) proof
+
+ val skoss = map (fn (_, _, t, _, _) => Term.fold_aterms add_sko t []) input_steps
+ val skoss_input_steps = filter_out (null o fst) (skoss ~~ input_steps)
+
+ val groups =
+ Graph.empty
+ |> fold (fn (skos, (name, _, _, _, _)) => add_cycle name skos) skoss_input_steps
+ |> Graph.strong_conn
+
+ fun step_name_of_group skos = (implode skos, [])
+ fun in_group group = member (op =) group o hd
+ fun group_of sko = the (find_first (fn group => in_group group sko) groups)
+
+ fun new_step group (skoss_steps : ('a * (term, 'b) atp_step) list) =
+ let
+ val t =
+ skoss_steps
+ |> map (snd #> #3 #> HOLogic.dest_Trueprop)
+ |> Library.foldr1 s_conj
+ |> HOLogic.mk_Trueprop
+ val deps = map (snd #> #1) skoss_steps
+ in
+ (step_name_of_group group, Plain, t, spass_skolemize_rule, deps)
+ end
+
+ val sko_steps =
+ map (fn group => new_step group (filter (in_group group o fst) skoss_input_steps)) groups
+
+ val old_news =
+ map (fn (skos, (name, _, _, _, _)) => (name, [step_name_of_group (group_of skos)]))
+ skoss_input_steps
+ val repair_deps = fold replace_dependencies_in_line old_news
+ in
+ input_steps @ sko_steps @ map repair_deps other_steps
+ end
+ else
+ proof
+
fun factify_atp_proof fact_names hyp_ts concl_t atp_proof =
let
fun factify_step ((num, ss), role, t, rule, deps) =
@@ -550,7 +616,8 @@
fun repair_dep (num, ss) = (num, the_default ss (AList.lookup (op =) names num))
fun repair_deps (name, role, t, rule, deps) = (name, role, t, rule, map repair_dep deps)
-
- in map repair_deps atp_proof end
+ in
+ map repair_deps atp_proof
+ end
end;
--- a/src/HOL/Tools/ATP/atp_util.ML Mon Dec 16 17:08:22 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_util.ML Tue Dec 17 09:52:10 2013 +0100
@@ -36,7 +36,6 @@
val s_disj : term * term -> term
val s_imp : term * term -> term
val s_iff : term * term -> term
- val s_not_prop : term -> term
val close_form : term -> term
val hol_close_form_prefix : string
val hol_close_form : term -> term
@@ -308,10 +307,6 @@
| s_iff (t1, @{const False}) = s_not t1
| s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2
-fun s_not_prop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
- | s_not_prop (@{const "==>"} $ t $ @{prop False}) = t
- | s_not_prop t = @{const "==>"} $ t $ @{prop False}
-
fun close_form t =
fold (fn ((s, i), T) => fn t' =>
Logic.all_const T $ Abs (s, T, abstract_over (Var ((s, i), T), t')))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Mon Dec 16 17:08:22 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Tue Dec 17 09:52:10 2013 +0100
@@ -82,8 +82,7 @@
|> pairself (sort_distinct (string_ord o pairself fst))
fun one_line_proof_text num_chained
- (preplay, banner, used_facts, minimize_command, subgoal,
- subgoal_count) =
+ (preplay, banner, used_facts, minimize_command, subgoal, subgoal_count) =
let
val (chained, extra) = split_used_facts used_facts
val (failed, reconstr, ext_time) =
@@ -91,10 +90,9 @@
Played (reconstr, time) => (false, reconstr, (SOME (false, time)))
| Trust_Playable (reconstr, time) =>
(false, reconstr,
- case time of
+ (case time of
NONE => NONE
- | SOME time =>
- if time = Time.zeroTime then NONE else SOME (true, time))
+ | SOME time => if time = Time.zeroTime then NONE else SOME (true, time)))
| Failed_to_Play reconstr => (true, reconstr, NONE)
val try_line =
([], map fst extra)
@@ -105,9 +103,9 @@
\solve this.)"
else
try_command_line banner ext_time)
- in try_line ^ minimize_line minimize_command (map fst (extra @ chained)) end
-
-
+ in
+ try_line ^ minimize_line minimize_command (map fst (extra @ chained))
+ end
(** detailed Isar proofs **)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Dec 16 17:08:22 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Dec 17 09:52:10 2013 +0100
@@ -394,8 +394,7 @@
fun is_fact_chained ((_, (sc, _)), _) = sc = Chained
fun filter_used_facts keep_chained used =
- filter ((member (op =) used o fst) orf
- (if keep_chained then is_fact_chained else K false))
+ filter ((member (op =) used o fst) orf (if keep_chained then is_fact_chained else K false))
fun play_one_line_proof mode debug verbose timeout pairs state i preferred
reconstrs =
@@ -847,6 +846,7 @@
val atp_proof =
atp_proof
|> termify_atp_proof ctxt pool lifted sym_tab
+ |> introduce_spass_skolem
|> factify_atp_proof fact_names hyp_ts concl_t
in
(debug, verbose, metis_type_enc, metis_lam_trans, preplay_timeout,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Mon Dec 16 17:08:22 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Tue Dec 17 09:52:10 2013 +0100
@@ -7,6 +7,7 @@
signature SLEDGEHAMMER_RECONSTRUCT =
sig
+ type atp_step_name = ATP_Proof.atp_step_name
type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step
type 'a atp_proof = 'a ATP_Proof.atp_proof
type stature = ATP_Problem_Generate.stature
@@ -46,19 +47,16 @@
open String_Redirect
-val e_skolemize_rule = "skolemize"
+val e_skolemize_rules = ["skolemize", "shift_quantors"]
val vampire_skolemisation_rule = "skolemisation"
(* TODO: Use "Z3_Proof.string_of_rule" once it is moved to Isabelle *)
-val z3_apply_def_rule = "apply-def"
-val z3_hypothesis_rule = "hypothesis"
-val z3_intro_def_rule = "intro-def"
-val z3_lemma_rule = "lemma"
val z3_skolemize_rule = "sk"
val z3_th_lemma_rule = "th-lemma"
-val is_skolemize_rule =
- member (op =) [e_skolemize_rule, vampire_skolemisation_rule, z3_skolemize_rule]
+val skolemize_rules =
+ e_skolemize_rules @ [spass_skolemize_rule, vampire_skolemisation_rule, z3_skolemize_rule]
+val is_skolemize_rule = member (op =) skolemize_rules
val is_arith_rule = String.isPrefix z3_th_lemma_rule
fun raw_label_of_num num = (num, 0)
@@ -69,69 +67,14 @@
fun add_fact_of_dependencies [(_, ss as _ :: _)] = apsnd (union (op =) ss)
| add_fact_of_dependencies names = apfst (insert (op =) (label_of_clause names))
-fun replace_one_dependency (old, new) dep =
- if is_same_atp_step dep old then new else [dep]
-fun replace_dependencies_in_line p (name, role, t, rule, deps) =
- (name, role, t, rule, fold (union (op =) o replace_one_dependency p) deps [])
-
-fun inline_z3_defs _ [] = []
- | inline_z3_defs defs ((line as (name, role, t, rule, deps)) :: lines) =
- if rule = z3_intro_def_rule then
- let val def = t |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> swap in
- inline_z3_defs (insert (op =) def defs)
- (map (replace_dependencies_in_line (name, [])) lines)
- end
- else if rule = z3_apply_def_rule then
- inline_z3_defs defs (map (replace_dependencies_in_line (name, [])) lines)
- else
- (name, role, Term.subst_atomic defs t, rule, deps) :: inline_z3_defs defs lines
-
-fun alist_cons_list eq (k, v) = AList.map_default eq (k, []) (cons v)
-
-fun add_z3_hypotheses [] = I
- | add_z3_hypotheses hyps =
- HOLogic.dest_Trueprop
- #> curry s_imp (Library.foldr1 s_conj (map HOLogic.dest_Trueprop hyps))
- #> HOLogic.mk_Trueprop
-
-fun inline_z3_hypotheses _ _ [] = []
- | inline_z3_hypotheses hyp_names hyps ((name, role, t, rule, deps) :: lines) =
- if rule = z3_hypothesis_rule then
- inline_z3_hypotheses (name :: hyp_names) (alist_cons_list (op =) (t, name) hyps) lines
- else
- let val deps' = subtract (op =) hyp_names deps in
- if rule = z3_lemma_rule then
- (name, role, t, rule, deps') :: inline_z3_hypotheses hyp_names hyps lines
- else
- let
- val add_hyps = filter_out (null o inter (op =) deps o snd) hyps
- val t' = add_z3_hypotheses (map fst add_hyps) t
- val deps' = subtract (op =) hyp_names deps
- val hyps' = fold (AList.update (op =) o apsnd (insert (op =) name)) add_hyps hyps
- in
- (name, role, t', rule, deps') :: inline_z3_hypotheses hyp_names hyps' lines
- end
- end
-
-fun simplify_prop (@{const Not} $ t) = s_not (simplify_prop t)
- | simplify_prop (@{const conj} $ t $ u) = s_conj (simplify_prop t, simplify_prop u)
- | simplify_prop (@{const disj} $ t $ u) = s_disj (simplify_prop t, simplify_prop u)
- | simplify_prop (@{const implies} $ t $ u) = s_imp (simplify_prop t, simplify_prop u)
- | simplify_prop (@{const HOL.eq (bool)} $ t $ u) = s_iff (simplify_prop t, simplify_prop u)
- | simplify_prop (t $ u) = simplify_prop t $ simplify_prop u
- | simplify_prop (Abs (s, T, t)) = Abs (s, T, simplify_prop t)
- | simplify_prop t = t
-
-fun simplify_line (name, role, t, rule, deps) = (name, role, simplify_prop t, rule, deps)
-
(* No "real" literals means only type information (tfree_tcs, clsrel, or clsarity). *)
fun is_only_type_information t = t aconv @{prop True}
(* Discard facts; consolidate adjacent lines that prove the same formula, since they differ only in
type information. *)
fun add_line_pass1 (line as (name as (_, ss), role, t, rule, [])) lines =
- (* No dependencies: lemma (for Z3), fact, conjecture, or (for Vampire)
- internal facts or definitions. *)
+ (* No dependencies: lemma (for Z3), fact, conjecture, or (for Vampire) internal facts or
+ definitions. *)
if role = Lemma orelse role = Conjecture orelse role = Negated_Conjecture orelse
role = Hypothesis orelse is_arith_rule rule then
line :: lines
@@ -150,8 +93,8 @@
and delete_dependency name lines =
fold_rev add_line_pass2 (map (replace_dependencies_in_line (name, [])) lines) []
-fun add_line_pass3 res [] = rev res
- | add_line_pass3 res ((name as (_, ss), role, t, rule, deps) :: lines) =
+fun add_lines_pass3 res [] = rev res
+ | add_lines_pass3 res ((name as (_, ss), role, t, rule, deps) :: lines) =
if role <> Plain orelse is_skolemize_rule rule orelse is_arith_rule rule orelse
(* the last line must be kept *)
null lines orelse
@@ -159,9 +102,9 @@
andalso length deps >= 2 andalso
(* don't keep next to last line, which usually results in a trivial step *)
not (can the_single lines)) then
- add_line_pass3 ((name, role, simplify_prop t, rule, deps) :: res) lines
+ add_lines_pass3 ((name, role, t, rule, deps) :: res) lines
else
- add_line_pass3 res (map (replace_dependencies_in_line (name, deps)) lines)
+ add_lines_pass3 res (map (replace_dependencies_in_line (name, deps)) lines)
val add_labels_of_proof =
steps_of_proof
@@ -283,12 +226,9 @@
let
val atp_proof =
atp_proof
- |> inline_z3_defs []
- |> map simplify_line
- |> inline_z3_hypotheses [] []
|> rpair [] |-> fold_rev add_line_pass1
|> rpair [] |-> fold_rev add_line_pass2
- |> add_line_pass3 []
+ |> add_lines_pass3 []
val conjs =
map_filter (fn (name, role, _, _, _) =>
@@ -324,8 +264,10 @@
|> fold (fn (name as (s, _), role, t, rule, _) =>
Symtab.update_new (s, (rule, t
|> (if is_clause_tainted [name] then
- role <> Conjecture ? s_not_prop
+ HOLogic.dest_Trueprop
+ #> role <> Conjecture ? s_not
#> fold exists_of (map Var (Term.add_vars t []))
+ #> HOLogic.mk_Trueprop
else
I))))
atp_proof
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML Mon Dec 16 17:08:22 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML Tue Dec 17 09:52:10 2013 +0100
@@ -19,9 +19,7 @@
Failed_to_Play of reconstructor
type minimize_command = string list -> string
-
- type one_line_params =
- play * string * (string * stature) list * minimize_command * int * int
+ type one_line_params = play * string * (string * stature) list * minimize_command * int * int
val smtN : string
end;
@@ -41,9 +39,7 @@
Failed_to_Play of reconstructor
type minimize_command = string list -> string
-
-type one_line_params =
- play * string * (string * stature) list * minimize_command * int * int
+type one_line_params = play * string * (string * stature) list * minimize_command * int * int
val smtN = "smt"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Mon Dec 16 17:08:22 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Dec 17 09:52:10 2013 +0100
@@ -108,13 +108,17 @@
tag_list 1 facts
|> map (fn (j, fact) => fact |> apsnd (K j))
|> filter_used_facts false used_facts
+ |> distinct (eq_fst (op =))
|> map (prefix "@" o string_of_int o snd)
fun filter_info (fact_filter, facts) =
let
val indices = find_indices facts
- val unknowns = replicate (num_used_facts - length indices) "?"
- in (commas (indices @ unknowns), fact_filter) end
+ (* "Int.max" is there for robustness -- it shouldn't be necessary *)
+ val unknowns = replicate (Int.max (0, num_used_facts - length indices)) "?"
+ in
+ (commas (indices @ unknowns), fact_filter)
+ end
val filter_infos =
map filter_info (("actual", used_from) :: factss)