--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Wed Jan 02 16:32:40 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Wed Jan 02 19:59:06 2013 +0100
@@ -128,10 +128,10 @@
| add_type_constraint false (cl, TVar (ix, _)) = add_var (ix, cl)
| add_type_constraint _ _ = I
-fun repair_variable_name f s =
+fun repair_var_name s =
let
fun subscript_name s n = s ^ nat_subscript n
- val s = String.map f s
+ val s = String.map Char.toLower s
in
case space_explode "_" s of
[_] => (case take_suffix Char.isDigit (String.explode s) of
@@ -240,6 +240,8 @@
end
| NONE => (* a free or schematic variable *)
let
+ fun fresh_up s =
+ [(s, ())] |> Variable.variant_frees ctxt [] |> hd |> fst
val term_ts = map (do_term [] NONE) us
val ts = term_ts @ extra_ts
val T =
@@ -253,10 +255,10 @@
case unprefix_and_unascii schematic_var_prefix s of
SOME s => Var ((s, var_index), T)
| NONE =>
- Var ((s |> textual
- ? (repair_variable_name Char.toLower
- #> Char.isLower (String.sub (s, 0)) ? Name.skolem),
- var_index), T)
+ if textual andalso not (is_tptp_variable s) then
+ Free (s |> textual ? (repair_var_name #> fresh_up), T)
+ else
+ Var ((s |> textual ? repair_var_name, var_index), T)
in list_comb (t, ts) end
in do_term [] end
@@ -301,7 +303,7 @@
(* FIXME: TFF *)
#>> quantify_over_var
(case q of AForall => forall_of | AExists => exists_of)
- (s |> textual ? repair_variable_name Char.toLower)
+ (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
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Jan 02 16:32:40 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Jan 02 19:59:06 2013 +0100
@@ -433,6 +433,9 @@
val e_skolemize_rule = "skolemize"
val vampire_skolemisation_rule = "skolemisation"
+val is_skolemize_rule =
+ member (op =) [e_skolemize_rule, vampire_skolemisation_rule]
+
fun add_desired_line _ _ (line as Definition_Step (name, _, _)) (j, lines) =
(j, line :: map (replace_dependencies_in_line (name, [])) lines)
| add_desired_line fact_names frees
@@ -440,8 +443,7 @@
(j + 1,
if is_fact fact_names ss orelse
is_conjecture ss orelse
- rule = vampire_skolemisation_rule orelse
- rule = e_skolemize_rule orelse
+ is_skolemize_rule rule orelse
(* the last line must be kept *)
j = 0 orelse
(not (is_only_type_information t) andalso
@@ -473,7 +475,7 @@
if member (op =) qs Show then "show" else "have")
fun do_obtain qs xs =
(if member (op =) qs Then then "then " else "") ^ "obtain " ^
- (space_implode " " (map fst xs))
+ (space_implode " " (map fst xs)) ^ " where"
val do_term =
annotate_types ctxt
#> with_vanilla_print_mode (Syntax.string_of_term ctxt)
@@ -673,28 +675,32 @@
val ref_graph = atp_proof |> map_filter dep_of_step |> make_ref_graph
val axioms = axioms_of_ref_graph ref_graph conjs
val tainted = tainted_atoms_of_ref_graph ref_graph conjs
- val is_skolem = can (apfst (apfst Name.dest_skolem))
- val props =
+ val steps =
Symtab.empty
|> fold (fn Definition_Step _ => I (* FIXME *)
- | Inference_Step (name as (s, ss), role, t, _, _) =>
- Symtab.update_new (s,
- if member (op = o apsnd fst) tainted s then
- t |> role <> Conjecture ? s_not
- |> fold exists_of (map Var (Term.add_vars t []))
- else
- t |> fold exists_of (map Var (filter is_skolem
- (Term.add_vars t [])))))
+ | Inference_Step (name as (s, ss), role, t, rule, _) =>
+ Symtab.update_new (s, (rule,
+ t |> (if member (op = o apsnd fst) tainted s then
+ (role <> Conjecture ? s_not)
+ #> fold exists_of (map Var (Term.add_vars t []))
+ else
+ I))))
atp_proof
+ fun is_clause_skolemize_rule [(s, _)] =
+ Option.map (is_skolemize_rule o fst) (Symtab.lookup steps s) =
+ SOME true
+ | is_clause_skolemize_rule _ = false
(* The assumptions and conjecture are "prop"s; the other formulas are
"bool"s. *)
fun prop_of_clause [name as (s, ss)] =
(case resolve_conjecture ss of
[j] => if j = length hyp_ts then concl_t else nth hyp_ts j
- | _ => the_default @{term False} (Symtab.lookup props s)
- |> HOLogic.mk_Trueprop |> close_form)
+ | _ => the_default ("", @{term False}) (Symtab.lookup steps s)
+ |> snd |> HOLogic.mk_Trueprop |> close_form)
| prop_of_clause names =
- let val lits = map_filter (Symtab.lookup props o fst) names in
+ let
+ val lits = map snd (map_filter (Symtab.lookup steps o fst) names)
+ in
case List.partition (can HOLogic.dest_not) lits of
(negs as _ :: _, pos as _ :: _) =>
HOLogic.mk_imp
@@ -707,9 +713,22 @@
(outer andalso length c = 1 andalso subset (op =) (c, conjs))
? cons Show
fun isar_step_of_direct_inf outer (Have (gamma, c)) =
- Prove (maybe_show outer c [], label_of_clause c, prop_of_clause c,
- By_Metis (fold (add_fact_from_dependencies fact_names) gamma
- ([], [])))
+ let
+ val l = label_of_clause c
+ val t = prop_of_clause c
+ val by =
+ By_Metis (fold (add_fact_from_dependencies fact_names) gamma
+ ([], []))
+ in
+ if is_clause_skolemize_rule c then
+ let
+ val xs =
+ Term.add_frees t []
+ |> filter_out (Variable.is_declared ctxt o fst)
+ in Obtain ([], xs, l, t, by) end
+ else
+ Prove (maybe_show outer c [], l, t, by)
+ end
| isar_step_of_direct_inf outer (Cases cases) =
let val c = succedent_of_cases cases in
Prove (maybe_show outer c [Ultimately], label_of_clause c,