--- a/src/HOL/Metis_Examples/Binary_Tree.thy Thu Jan 03 20:42:18 2013 +0100
+++ b/src/HOL/Metis_Examples/Binary_Tree.thy Thu Jan 03 21:23:14 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 20:42:18 2013 +0100
+++ b/src/HOL/Metis_Examples/Clausification.thy Thu Jan 03 21:23:14 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 20:42:18 2013 +0100
+++ b/src/HOL/Metis_Examples/Message.thy Thu Jan 03 21:23:14 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 20:42:18 2013 +0100
+++ b/src/HOL/Metis_Examples/Sets.thy Thu Jan 03 21:23:14 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 20:42:18 2013 +0100
+++ b/src/HOL/Metis_Examples/Tarski.thy Thu Jan 03 21:23:14 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 20:42:18 2013 +0100
+++ b/src/HOL/Metis_Examples/Trans_Closure.thy Thu Jan 03 21:23:14 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 20:42:18 2013 +0100
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy Thu Jan 03 21:23:14 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/ATP/atp_problem_generate.ML Thu Jan 03 20:42:18 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Jan 03 21:23:14 2013 +0100
@@ -1027,7 +1027,7 @@
| add_formula_vars bounds (AConn (_, phis)) =
fold (add_formula_vars bounds) phis
| add_formula_vars bounds (AAtom tm) = add_term_vars bounds tm
- in mk_aquant AForall (add_formula_vars [] phi []) phi end
+ in mk_aquant AForall (rev (add_formula_vars [] phi [])) phi end
fun add_term_vars bounds (ATerm ((name as (s, _), _), tms)) =
(if is_tptp_variable s andalso
@@ -1039,6 +1039,7 @@
#> fold (add_term_vars bounds) tms
| add_term_vars bounds (AAbs (((name, _), tm), args)) =
add_term_vars (name :: bounds) tm #> fold (add_term_vars bounds) args
+
fun close_formula_universally phi = close_universally add_term_vars phi
fun add_iterm_vars bounds (IApp (tm1, tm2)) =
@@ -1277,7 +1278,7 @@
handle TERM _ => @{const True}
(* Satallax prefers "=" to "<=>" (for definitions) and Metis (CNF) requires "="
- for obscure technical reasons. *)
+ for technical reasons. *)
fun should_use_iff_for_eq CNF _ = false
| should_use_iff_for_eq (THF _) format = not (is_type_enc_higher_order format)
| should_use_iff_for_eq _ _ = true
--- a/src/HOL/Tools/ATP/atp_proof.ML Thu Jan 03 20:42:18 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML Thu Jan 03 21:23:14 2013 +0100
@@ -522,23 +522,22 @@
fun clean_up_atp_proof_dependencies proof = clean_up_dependencies [] proof
-fun map_term_names_in_term f (ATerm ((s, tys), ts)) =
- ATerm ((f s, tys), map (map_term_names_in_term f) ts)
-fun map_term_names_in_formula f (AQuant (q, xs, phi)) =
- AQuant (q, xs, map_term_names_in_formula f phi)
- | map_term_names_in_formula f (AConn (c, phis)) =
- AConn (c, map (map_term_names_in_formula f) phis)
- | map_term_names_in_formula f (AAtom t) = AAtom (map_term_names_in_term f t)
-fun map_term_names_in_step f (Definition_Step (name, phi1, phi2)) =
- Definition_Step (name, map_term_names_in_formula f phi1,
- map_term_names_in_formula f phi2)
- | map_term_names_in_step f (Inference_Step (name, role, phi, rule, deps)) =
- Inference_Step (name, role, map_term_names_in_formula f phi, rule, deps)
-fun map_term_names_in_atp_proof f = map (map_term_names_in_step f)
+fun map_term_names_in_atp_proof f =
+ let
+ fun do_term (ATerm ((s, tys), ts)) = ATerm ((f s, tys), map do_term ts)
+ fun do_formula (AQuant (q, xs, phi)) =
+ AQuant (q, map (apfst f) xs, do_formula phi)
+ | do_formula (AConn (c, phis)) = AConn (c, map do_formula phis)
+ | do_formula (AAtom t) = AAtom (do_term t)
+ fun do_step (Definition_Step (name, phi1, phi2)) =
+ Definition_Step (name, do_formula phi1, do_formula phi2)
+ | do_step (Inference_Step (name, role, phi, rule, deps)) =
+ Inference_Step (name, role, do_formula phi, rule, deps)
+ in map do_step end
fun nasty_name pool s = s |> Symtab.lookup pool |> the_default s
+
fun nasty_atp_proof pool =
- if Symtab.is_empty pool then I
- else map_term_names_in_atp_proof (nasty_name pool)
+ not (Symtab.is_empty pool) ? map_term_names_in_atp_proof (nasty_name pool)
end;
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Thu Jan 03 20:42:18 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Thu Jan 03 21:23:14 2013 +0100
@@ -131,7 +131,7 @@
fun repair_var_name s =
let
fun subscript_name s n = s ^ nat_subscript n
- val s = String.map Char.toLower s
+ val s = s |> String.map Char.toLower
in
case space_explode "_" s of
[_] => (case take_suffix Char.isDigit (String.explode s) of
--- a/src/HOL/Tools/Meson/meson_clausify.ML Thu Jan 03 20:42:18 2013 +0100
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Thu Jan 03 21:23:14 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 20:42:18 2013 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Thu Jan 03 21:23:14 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 20:42:18 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Jan 03 21:23:14 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 ^