merged
authorwenzelm
Thu, 03 Jan 2013 21:23:14 +0100
changeset 50708 07202e00fe4d
parent 50706 573d84e08f3f (diff)
parent 50707 5b2bf7611662 (current diff)
child 50709 985c081a4f11
merged
--- 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 ^