--- a/src/HOL/Tools/ATP/atp_proof.ML Thu Jan 30 16:30:01 2014 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML Thu Jan 30 22:55:52 2014 +0100
@@ -44,6 +44,7 @@
val agsyhol_core_rule : string
val satallax_core_rule : string
val spass_input_rule : string
+ val spass_pre_skolemize_rule : string
val spass_skolemize_rule : string
val z3_tptp_core_rule : string
@@ -73,6 +74,7 @@
val agsyhol_core_rule = "__agsyhol_core" (* arbitrary *)
val satallax_core_rule = "__satallax_core" (* arbitrary *)
val spass_input_rule = "Inp"
+val spass_pre_skolemize_rule = "__Sko0" (* arbitrary *)
val spass_skolemize_rule = "__Sko" (* arbitrary *)
val z3_tptp_core_rule = "__z3_tptp_core" (* arbitrary *)
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Thu Jan 30 16:30:01 2014 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Thu Jan 30 22:55:52 2014 +0100
@@ -535,6 +535,50 @@
#> map (termify_line ctxt lifted sym_tab)
#> repair_waldmeister_endgame
+fun take_distinct_vars seen ((t as Var _) :: ts) =
+ if member (op aconv) seen t then rev seen else take_distinct_vars (t :: seen) ts
+ | take_distinct_vars seen _ = rev seen
+
+fun unskolemize_term skos t =
+ let
+ val is_sko = member (op =) skos
+
+ fun find_args args (t $ u) = find_args (u :: args) t #> find_args [] u
+ | find_args _ (Abs (_, _, t)) = find_args [] t
+ | find_args args (Free (s, _)) =
+ if is_sko s then
+ let val new = take_distinct_vars [] args in
+ (fn [] => new | old => if length new < length old then new else old)
+ end
+ else
+ I
+ | find_args _ _ = I
+
+ val alls = find_args [] t []
+ val num_alls = length alls
+
+ fun fix_skos args (t $ u) = fix_skos (fix_skos [] u :: args) t
+ | fix_skos args (t as Free (s, T)) =
+ if is_sko s then list_comb (Free (s, funpow num_alls body_type T), drop num_alls args)
+ else list_comb (t, args)
+ | fix_skos [] (Abs (s, T, t)) = Abs (s, T, fix_skos [] t)
+ | fix_skos [] t = t
+ | fix_skos args t = list_comb (fix_skos [] t, args)
+
+ val t' = fix_skos [] t
+
+ fun add_sko (t as Free (s, _)) = is_sko s ? insert (op aconv) t
+ | add_sko _ = I
+
+ val exs = Term.fold_aterms add_sko t' []
+ in
+ t'
+ |> HOLogic.dest_Trueprop
+ |> fold exists_of exs |> Term.map_abs_vars (K Name.uu)
+ |> fold_rev forall_of alls
+ |> HOLogic.mk_Trueprop
+ end
+
fun introduce_spass_skolem [] = []
| introduce_spass_skolem (proof as (_, _, _, rule1, _) :: _) =
if rule1 = spass_input_rule then
@@ -558,20 +602,25 @@
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) =
+ fun new_steps (skoss_steps : (string list * (term, 'a) atp_step) list) group =
let
+ val name = step_name_of_group group
+ val name0 = name |>> prefix "0"
val t =
skoss_steps
|> map (snd #> #3 #> HOLogic.dest_Trueprop)
|> Library.foldr1 s_conj
|> HOLogic.mk_Trueprop
+ val skos = fold (union (op =) o fst) skoss_steps []
val deps = map (snd #> #1) skoss_steps
in
- (step_name_of_group group, Plain, t, spass_skolemize_rule, deps)
+ [(name0, Unknown, unskolemize_term skos t, spass_pre_skolemize_rule, deps),
+ (name, Unknown, t, spass_skolemize_rule, [name0])]
end
val sko_steps =
- map (fn group => new_step group (filter (in_group group o fst) skoss_input_steps)) groups
+ maps (fn group => new_steps (filter (in_group group o fst) skoss_input_steps) group)
+ groups
val old_news =
map (fn (skos, (name, _, _, _, _)) => (name, [step_name_of_group (group_of skos)]))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Thu Jan 30 16:30:01 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Thu Jan 30 22:55:52 2014 +0100
@@ -34,9 +34,10 @@
val trace = Attrib.setup_config_bool @{binding sledgehammer_preplay_trace} (K false)
-fun preplay_trace ctxt assms concl result =
+fun preplay_trace ctxt assmsp concl result =
let
val ctxt = ctxt |> Config.put show_markup true
+ val assms = op @ assmsp
val time = "[" ^ string_of_play_outcome result ^ "]" |> Pretty.str
val nr_of_assms = length assms
val assms = assms
@@ -64,8 +65,7 @@
fun resolve_fact_names ctxt names =
(names
|>> map string_of_label
- |> op @
- |> maps (thms_of_name ctxt))
+ |> pairself (maps (thms_of_name ctxt)))
handle ERROR msg => error ("preplay error: " ^ msg)
fun thm_of_proof ctxt (Proof (fixed_frees, assms, steps)) =
@@ -86,15 +86,15 @@
|> Skip_Proof.make_thm thy
end
-fun tac_of_method meth type_enc lam_trans ctxt facts =
+fun tac_of_method meth type_enc lam_trans ctxt (local_facts, global_facts) =
+ Method.insert_tac local_facts THEN'
(case meth of
- Metis_Method => Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts
- | Meson_Method => Meson.meson_tac ctxt facts
+ Meson_Method => Meson.meson_tac ctxt global_facts
+ | Metis_Method => Metis_Tactic.metis_tac [type_enc] lam_trans ctxt global_facts
| _ =>
- Method.insert_tac facts THEN'
+ Method.insert_tac global_facts THEN'
(case meth of
- Metis_New_Skolem_Method => Metis_Tactic.metis_tac [type_enc] lam_trans ctxt []
- | Simp_Method => Simplifier.asm_full_simp_tac ctxt
+ Simp_Method => Simplifier.asm_full_simp_tac ctxt
| Simp_Size_Method =>
Simplifier.asm_full_simp_tac (Simplifier.add_simp @{thm size_ne_size_imp_ne} ctxt)
| Auto_Method => K (Clasimp.auto_tac ctxt)
@@ -128,7 +128,10 @@
Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop))
end)
- val facts = map (thm_of_proof ctxt) subproofs @ resolve_fact_names ctxt fact_names
+ val facts =
+ resolve_fact_names ctxt fact_names
+ |>> append (map (thm_of_proof ctxt) subproofs)
+
val ctxt' = ctxt |> silence_reconstructors debug
fun prove () =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Thu Jan 30 16:30:01 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Thu Jan 30 22:55:52 2014 +0100
@@ -165,12 +165,19 @@
| Meson_Method => "meson"
| _ => raise Fail "Sledgehammer_Print: by_method")
- fun using_facts [] [] = ""
- | using_facts ls ss = "using " ^ space_implode " " (map string_of_label ls @ ss) ^ " "
+ fun with_facts none _ [] [] = none
+ | with_facts _ some ls ss = some (space_implode " " (map string_of_label ls @ ss))
+
+ val using_facts = with_facts "" (enclose "using " " ")
- fun of_metis ls ss = reconstructor_command (Metis (type_enc, lam_trans)) 1 1 [] 0 (ls, ss)
-
- fun of_method ls ss Metis_Method = of_metis ls ss
+ (* Local facts are always passed via "using", which affects "meson" and "metis". This is
+ arguably stylistically superior, because it emphasises the structure of the proof. It is also
+ more robust w.r.t. preplay: Preplay is performed before chaining of local facts with "hence"
+ and "thus" is introduced. See also "tac_of_method" in "Sledgehammer_Preplay". *)
+ fun of_method ls ss Metis_Method =
+ using_facts ls [] ^ reconstructor_command (Metis (type_enc, lam_trans)) 1 1 [] 0 ([], ss)
+ | of_method ls ss Meson_Method =
+ using_facts ls [] ^ with_facts "by meson" (enclose "by (meson " ")") [] ss
| of_method ls ss meth = using_facts ls ss ^ by_method meth
fun of_byline ind (ls, ss) meth =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Thu Jan 30 16:30:01 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Thu Jan 30 22:55:52 2014 +0100
@@ -20,8 +20,8 @@
Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list *
(facts * proof_method list list)
and proof_method =
- Metis_Method | Metis_New_Skolem_Method | Simp_Method | Simp_Size_Method | Auto_Method |
- Fastforce_Method | Force_Method | Arith_Method | Blast_Method | Meson_Method
+ Metis_Method | Simp_Method | Simp_Size_Method | Auto_Method | Fastforce_Method | Force_Method |
+ Arith_Method | Blast_Method | Meson_Method
val no_label : label
val no_facts : facts
@@ -69,8 +69,8 @@
Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list *
(facts * proof_method list list)
and proof_method =
- Metis_Method | Metis_New_Skolem_Method | Simp_Method | Simp_Size_Method | Auto_Method |
- Fastforce_Method | Force_Method | Arith_Method | Blast_Method | Meson_Method
+ Metis_Method | Simp_Method | Simp_Size_Method | Auto_Method | Fastforce_Method | Force_Method |
+ Arith_Method | Blast_Method | Meson_Method
val no_label = ("", ~1)
val no_facts = ([],[])
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Jan 30 16:30:01 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Jan 30 22:55:52 2014 +0100
@@ -85,16 +85,8 @@
map (replace_dependencies_in_line (name, [])) lines
| add_line_pass1 line lines = line :: lines
-(* Recursively delete empty lines (type information) from the proof.
- (FIXME: needed? And why is "delete_dependency" so complicated?) *)
-fun add_line_pass2 (line as (name, _, t, _, [])) lines =
- if is_only_type_information t then delete_dependency name lines else line :: lines
- | add_line_pass2 line lines = line :: lines
-and delete_dependency name lines =
- fold_rev add_line_pass2 (map (replace_dependencies_in_line (name, [])) lines) []
-
-fun add_lines_pass3 res [] = rev res
- | add_lines_pass3 res ((name, role, t, rule, deps) :: lines) =
+fun add_lines_pass2 res [] = rev res
+ | add_lines_pass2 res ((name, role, t, rule, deps) :: lines) =
let
val is_last_line = null lines
@@ -109,9 +101,9 @@
if role <> Plain orelse is_skolemize_rule rule orelse is_arith_rule rule orelse
is_datatype_rule rule orelse is_last_line orelse looks_interesting () orelse
is_before_skolemize_rule () then
- add_lines_pass3 ((name, role, t, rule, deps) :: res) lines
+ add_lines_pass2 ((name, role, t, rule, deps) :: res) lines
else
- add_lines_pass3 res (map (replace_dependencies_in_line (name, deps)) lines)
+ add_lines_pass2 res (map (replace_dependencies_in_line (name, deps)) lines)
end
val add_labels_of_proof =
@@ -209,7 +201,7 @@
Force_Method], [Meson_Method]]
val rewrite_methodss =
[[Auto_Method, Simp_Method, Fastforce_Method, Force_Method, Metis_Method], [Meson_Method]]
-val skolem_methodss = [[Metis_Method, Blast_Method], [Metis_New_Skolem_Method], [Meson_Method]]
+val skolem_methodss = [[Metis_Method, Blast_Method], [Meson_Method]]
fun isar_proof_text ctxt debug isar_proofs isar_params
(one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
@@ -237,8 +229,7 @@
val atp_proof =
atp_proof
|> rpair [] |-> fold_rev add_line_pass1
- |> rpair [] |-> fold_rev add_line_pass2
- |> add_lines_pass3 []
+ |> add_lines_pass2 []
val conjs =
map_filter (fn (name, role, _, _, _) =>