# HG changeset patch # User blanchet # Date 1357153146 -3600 # Node ID 83b8a5a39709b4fd75ab2dab85057d7d74552ebe # Parent e3e707c8ac5720d7a96a3d054a56fb491b53e565 generate "obtain" steps corresponding to skolemization inferences diff -r e3e707c8ac57 -r 83b8a5a39709 src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- 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 diff -r e3e707c8ac57 -r 83b8a5a39709 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- 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,