use new skolemizer for reconstructing skolemization steps in Isar proofs (because the old skolemizer messes up the order of the Skolem arguments)
--- 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
--- 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 \<Rightarrow> nat \<Rightarrow> bool" where
qax: "\<exists>b. \<forall>a. (q b a \<and> q 0 0 \<and> q 1 a \<and> q a 1) \<or> (q 0 1 \<and> q 1 0 \<and> q a b \<and> q 1 1)"
-declare [[metis_new_skolemizer = false]]
+declare [[metis_new_skolem = false]]
lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
by (metis qax)
@@ -32,7 +32,7 @@
lemma "\<exists>b. \<forall>a. (q b a \<and> q 0 0 \<and> q 1 a \<and> q a 1) \<or> (q 0 1 \<and> q 1 0 \<and> q a b \<and> q 1 1)"
by (metis (full_types) qax)
-declare [[metis_new_skolemizer]]
+declare [[metis_new_skolem]]
lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
by (metis qax)
@@ -54,7 +54,7 @@
(r 2 0 \<and> r 2 1 \<and> r 2 2 \<and> r 2 3) \<or>
(r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> r 3 3)"
-declare [[metis_new_skolemizer = false]]
+declare [[metis_new_skolem = false]]
lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
by (metis rax)
@@ -62,7 +62,7 @@
lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
by (metis (full_types) rax)
-declare [[metis_new_skolemizer]]
+declare [[metis_new_skolem]]
lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
by (metis rax)
@@ -88,7 +88,7 @@
axiomatization p :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
pax: "\<exists>b. \<forall>a. (p b a \<and> p 0 0 \<and> p 1 a) \<or> (p 0 1 \<and> p 1 0 \<and> p a b)"
-declare [[metis_new_skolemizer = false]]
+declare [[metis_new_skolem = false]]
lemma "\<exists>b. \<forall>a. \<exists>x. (p b a \<or> x) \<and> (p 0 0 \<or> x) \<and> (p 1 a \<or> x) \<and>
(p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
@@ -98,7 +98,7 @@
(p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
by (metis (full_types) pax)
-declare [[metis_new_skolemizer]]
+declare [[metis_new_skolem]]
lemma "\<exists>b. \<forall>a. \<exists>x. (p b a \<or> x) \<and> (p 0 0 \<or> x) \<and> (p 1 a \<or> x) \<and>
(p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
@@ -111,7 +111,7 @@
text {* New Skolemizer *}
-declare [[metis_new_skolemizer]]
+declare [[metis_new_skolem]]
lemma
fixes x :: real
--- 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 \<union> (B \<union> A) = B \<union> A"
by (metis Un_commute Un_left_absorb)
--- 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)) &
--- 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
--- 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
--- 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]
--- 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
--- 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
--- 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 ^