# HG changeset patch # User blanchet # Date 1357230535 -3600 # Node ID 0e943b33d907ff896b121d1525e5545215cb5ecb # Parent cd1fcda1ea88ebcee64a3533e32efdaefe3c631b use new skolemizer for reconstructing skolemization steps in Isar proofs (because the old skolemizer messes up the order of the Skolem arguments) diff -r cd1fcda1ea88 -r 0e943b33d907 src/HOL/Metis_Examples/Binary_Tree.thy --- a/src/HOL/Metis_Examples/Binary_Tree.thy Thu Jan 03 17:10:12 2013 +0100 +++ b/src/HOL/Metis_Examples/Binary_Tree.thy Thu Jan 03 17:28:55 2013 +0100 @@ -11,7 +11,7 @@ imports Main begin -declare [[metis_new_skolemizer]] +declare [[metis_new_skolem]] datatype 'a bt = Lf diff -r cd1fcda1ea88 -r 0e943b33d907 src/HOL/Metis_Examples/Clausification.thy --- a/src/HOL/Metis_Examples/Clausification.thy Thu Jan 03 17:10:12 2013 +0100 +++ b/src/HOL/Metis_Examples/Clausification.thy Thu Jan 03 17:28:55 2013 +0100 @@ -18,7 +18,7 @@ axiomatization q :: "nat \ nat \ bool" where qax: "\b. \a. (q b a \ q 0 0 \ q 1 a \ q a 1) \ (q 0 1 \ q 1 0 \ q a b \ q 1 1)" -declare [[metis_new_skolemizer = false]] +declare [[metis_new_skolem = false]] lemma "\b. \a. (q b a \ q a b)" by (metis qax) @@ -32,7 +32,7 @@ lemma "\b. \a. (q b a \ q 0 0 \ q 1 a \ q a 1) \ (q 0 1 \ q 1 0 \ q a b \ q 1 1)" by (metis (full_types) qax) -declare [[metis_new_skolemizer]] +declare [[metis_new_skolem]] lemma "\b. \a. (q b a \ q a b)" by (metis qax) @@ -54,7 +54,7 @@ (r 2 0 \ r 2 1 \ r 2 2 \ r 2 3) \ (r 3 0 \ r 3 1 \ r 3 2 \ r 3 3)" -declare [[metis_new_skolemizer = false]] +declare [[metis_new_skolem = false]] lemma "r 0 0 \ r 1 1 \ r 2 2 \ r 3 3" by (metis rax) @@ -62,7 +62,7 @@ lemma "r 0 0 \ r 1 1 \ r 2 2 \ r 3 3" by (metis (full_types) rax) -declare [[metis_new_skolemizer]] +declare [[metis_new_skolem]] lemma "r 0 0 \ r 1 1 \ r 2 2 \ r 3 3" by (metis rax) @@ -88,7 +88,7 @@ axiomatization p :: "nat \ nat \ bool" where pax: "\b. \a. (p b a \ p 0 0 \ p 1 a) \ (p 0 1 \ p 1 0 \ p a b)" -declare [[metis_new_skolemizer = false]] +declare [[metis_new_skolem = false]] lemma "\b. \a. \x. (p b a \ x) \ (p 0 0 \ x) \ (p 1 a \ x) \ (p 0 1 \ \ x) \ (p 1 0 \ \ x) \ (p a b \ \ x)" @@ -98,7 +98,7 @@ (p 0 1 \ \ x) \ (p 1 0 \ \ x) \ (p a b \ \ x)" by (metis (full_types) pax) -declare [[metis_new_skolemizer]] +declare [[metis_new_skolem]] lemma "\b. \a. \x. (p b a \ x) \ (p 0 0 \ x) \ (p 1 a \ x) \ (p 0 1 \ \ x) \ (p 1 0 \ \ x) \ (p a b \ \ x)" @@ -111,7 +111,7 @@ text {* New Skolemizer *} -declare [[metis_new_skolemizer]] +declare [[metis_new_skolem]] lemma fixes x :: real diff -r cd1fcda1ea88 -r 0e943b33d907 src/HOL/Metis_Examples/Message.thy --- a/src/HOL/Metis_Examples/Message.thy Thu Jan 03 17:10:12 2013 +0100 +++ b/src/HOL/Metis_Examples/Message.thy Thu Jan 03 17:28:55 2013 +0100 @@ -11,7 +11,7 @@ imports Main begin -declare [[metis_new_skolemizer]] +declare [[metis_new_skolem]] lemma strange_Un_eq [simp]: "A \ (B \ A) = B \ A" by (metis Un_commute Un_left_absorb) diff -r cd1fcda1ea88 -r 0e943b33d907 src/HOL/Metis_Examples/Sets.thy --- a/src/HOL/Metis_Examples/Sets.thy Thu Jan 03 17:10:12 2013 +0100 +++ b/src/HOL/Metis_Examples/Sets.thy Thu Jan 03 17:28:55 2013 +0100 @@ -11,7 +11,7 @@ imports Main begin -declare [[metis_new_skolemizer]] +declare [[metis_new_skolem]] lemma "EX x X. ALL y. EX z Z. (~P(y,y) | P(x,x) | ~S(z,x)) & (S(x,y) | ~S(y,z) | Q(Z,Z)) & diff -r cd1fcda1ea88 -r 0e943b33d907 src/HOL/Metis_Examples/Tarski.thy --- a/src/HOL/Metis_Examples/Tarski.thy Thu Jan 03 17:10:12 2013 +0100 +++ b/src/HOL/Metis_Examples/Tarski.thy Thu Jan 03 17:28:55 2013 +0100 @@ -11,7 +11,7 @@ imports Main "~~/src/HOL/Library/FuncSet" begin -declare [[metis_new_skolemizer]] +declare [[metis_new_skolem]] (*Many of these higher-order problems appear to be impossible using the current linkup. They often seem to need either higher-order unification diff -r cd1fcda1ea88 -r 0e943b33d907 src/HOL/Metis_Examples/Trans_Closure.thy --- a/src/HOL/Metis_Examples/Trans_Closure.thy Thu Jan 03 17:10:12 2013 +0100 +++ b/src/HOL/Metis_Examples/Trans_Closure.thy Thu Jan 03 17:28:55 2013 +0100 @@ -11,7 +11,7 @@ imports Main begin -declare [[metis_new_skolemizer]] +declare [[metis_new_skolem]] type_synonym addr = nat diff -r cd1fcda1ea88 -r 0e943b33d907 src/HOL/Metis_Examples/Type_Encodings.thy --- a/src/HOL/Metis_Examples/Type_Encodings.thy Thu Jan 03 17:10:12 2013 +0100 +++ b/src/HOL/Metis_Examples/Type_Encodings.thy Thu Jan 03 17:28:55 2013 +0100 @@ -12,7 +12,7 @@ imports Main begin -declare [[metis_new_skolemizer]] +declare [[metis_new_skolem]] sledgehammer_params [prover = spass, blocking, fact_filter = mepo, timeout = 30, preplay_timeout = 0, dont_minimize] diff -r cd1fcda1ea88 -r 0e943b33d907 src/HOL/Tools/Meson/meson_clausify.ML --- a/src/HOL/Tools/Meson/meson_clausify.ML Thu Jan 03 17:10:12 2013 +0100 +++ b/src/HOL/Tools/Meson/meson_clausify.ML Thu Jan 03 17:28:55 2013 +0100 @@ -300,20 +300,20 @@ |> Skip_Proof.make_thm @{theory} (* Converts an Isabelle theorem into NNF. *) -fun nnf_axiom choice_ths new_skolemizer ax_no th ctxt = +fun nnf_axiom choice_ths new_skolem ax_no th ctxt = let val thy = Proof_Context.theory_of ctxt val th = th |> transform_elim_theorem |> zero_var_indexes - |> new_skolemizer ? forall_intr_vars + |> new_skolem ? forall_intr_vars val (th, ctxt) = Variable.import true [th] ctxt |>> snd |>> the_single val th = th |> Conv.fconv_rule Object_Logic.atomize |> cong_extensionalize_thm thy |> abs_extensionalize_thm ctxt |> make_nnf ctxt in - if new_skolemizer then + if new_skolem then let fun skolemize choice_ths = skolemize_with_choice_theorems ctxt choice_ths @@ -364,14 +364,14 @@ end (* Convert a theorem to CNF, with additional premises due to skolemization. *) -fun cnf_axiom ctxt0 new_skolemizer combinators ax_no th = +fun cnf_axiom ctxt0 new_skolem combinators ax_no th = let val thy = Proof_Context.theory_of ctxt0 val choice_ths = choice_theorems thy val (opt, (nnf_th, ctxt)) = - nnf_axiom choice_ths new_skolemizer ax_no th ctxt0 + nnf_axiom choice_ths new_skolem ax_no th ctxt0 fun clausify th = - make_cnf (if new_skolemizer orelse null choice_ths then [] + make_cnf (if new_skolem orelse null choice_ths then [] else map (old_skolem_theorem_from_def thy) (old_skolem_defs th)) th ctxt ctxt val (cnf_ths, ctxt) = clausify nnf_th diff -r cd1fcda1ea88 -r 0e943b33d907 src/HOL/Tools/Metis/metis_tactic.ML --- a/src/HOL/Tools/Metis/metis_tactic.ML Thu Jan 03 17:10:12 2013 +0100 +++ b/src/HOL/Tools/Metis/metis_tactic.ML Thu Jan 03 17:28:55 2013 +0100 @@ -11,7 +11,7 @@ sig val trace : bool Config.T val verbose : bool Config.T - val new_skolemizer : bool Config.T + val new_skolem : bool Config.T val advisory_simp : bool Config.T val type_has_top_sort : typ -> bool val metis_tac : @@ -29,8 +29,8 @@ open Metis_Generate open Metis_Reconstruct -val new_skolemizer = - Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false) +val new_skolem = + Attrib.setup_config_bool @{binding metis_new_skolem} (K false) val advisory_simp = Attrib.setup_config_bool @{binding metis_advisory_simp} (K true) @@ -137,8 +137,8 @@ (* Main function to start Metis proof and reconstruction *) fun FOL_SOLVE (type_enc :: fallback_type_encs) lam_trans ctxt cls ths0 = let val thy = Proof_Context.theory_of ctxt - val new_skolemizer = - Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy) + val new_skolem = + Config.get ctxt new_skolem orelse null (Meson.choice_theorems thy) val do_lams = (lam_trans = liftingN orelse lam_trans = lam_liftingN) ? introduce_lam_wrappers ctxt @@ -146,7 +146,7 @@ map2 (fn j => fn th => (Thm.get_name_hint th, th |> Drule.eta_contraction_rule - |> Meson_Clausify.cnf_axiom ctxt new_skolemizer + |> Meson_Clausify.cnf_axiom ctxt new_skolem (lam_trans = combsN) j ||> map do_lams)) (0 upto length ths0 - 1) ths0 diff -r cd1fcda1ea88 -r 0e943b33d907 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Jan 03 17:10:12 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Jan 03 17:28:55 2013 +0100 @@ -482,8 +482,8 @@ #> simplify_spaces #> maybe_quote val reconstr = Metis (type_enc, lam_trans) - fun do_metis ind (ls, ss) = - "\n" ^ do_indent (ind + 1) ^ + fun do_metis ind options (ls, ss) = + "\n" ^ do_indent (ind + 1) ^ options ^ reconstructor_command reconstr 1 1 [] 0 (ls |> sort_distinct (prod_ord string_ord int_ord), ss |> sort_distinct string_ord) @@ -495,15 +495,19 @@ do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n" | do_step ind (Obtain (qs, xs, l, t, By_Metis facts)) = do_indent ind ^ do_obtain qs xs ^ " " ^ - do_label l ^ do_term t ^ do_metis ind facts ^ "\n" + do_label l ^ do_term t ^ + (* The new skolemizer puts the arguments in the same order as the ATPs + (E and Vampire -- but see also "atp_proof_reconstruct.ML" regarding + Vampire). *) + do_metis ind "using [[metis_new_skolem]] " facts ^ "\n" | do_step ind (Prove (qs, l, t, By_Metis facts)) = do_indent ind ^ do_have qs ^ " " ^ - do_label l ^ do_term t ^ do_metis ind facts ^ "\n" + do_label l ^ do_term t ^ do_metis ind "" facts ^ "\n" | do_step ind (Prove (qs, l, t, Case_Split (proofs, facts))) = implode (map (prefix (do_indent ind ^ "moreover\n") o do_block ind) proofs) ^ do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ - do_metis ind facts ^ "\n" + do_metis ind "" facts ^ "\n" and do_steps prefix suffix ind steps = let val s = implode (map (do_step ind) steps) in replicate_string (ind * indent_size - size prefix) " " ^ prefix ^