# HG changeset patch
# User blanchet
# Date 1272147030 -7200
# Node ID 8228b3a4a2baca7c53001488eb15109b1ceb5ef7
# Parent  30f7ce76712da877b078f207a22a9c8e7981a4d2
remove "skolemize" option from Nitpick, since Skolemization is always useful

diff -r 30f7ce76712d -r 8228b3a4a2ba doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex	Sat Apr 24 17:48:21 2010 +0200
+++ b/doc-src/Nitpick/nitpick.tex	Sun Apr 25 00:10:30 2010 +0200
@@ -428,9 +428,6 @@
 $\mathit{sym}.y$ are simply the bound variables $x$ and $y$
 from \textit{sym}'s definition.
 
-Although skolemization is a useful optimization, you can disable it by invoking
-Nitpick with \textit{dont\_skolemize}. See \S\ref{optimizations} for details.
-
 \subsection{Natural Numbers and Integers}
 \label{natural-numbers-and-integers}
 
@@ -2199,9 +2196,6 @@
 formula and usually help us to understand why the counterexample falsifies the
 formula.
 
-\nopagebreak
-{\small See also \textit{skolemize} (\S\ref{optimizations}).}
-
 \opfalse{show\_datatypes}{hide\_datatypes}
 Specifies whether the subsets used to approximate (co)in\-duc\-tive datatypes should
 be displayed as part of counterexamples. Such subsets are sometimes helpful when
@@ -2451,15 +2445,6 @@
 {\small See also \textit{debug} (\S\ref{output-format}) and
 \textit{show\_consts} (\S\ref{output-format}).}
 
-\optrue{skolemize}{dont\_skolemize}
-Specifies whether the formula should be skolemized. For performance reasons,
-(positive) $\forall$-quanti\-fiers that occur in the scope of a higher-order
-(positive) $\exists$-quanti\-fier are left unchanged.
-
-\nopagebreak
-{\small See also \textit{debug} (\S\ref{output-format}) and
-\textit{show\_skolems} (\S\ref{output-format}).}
-
 \optrue{star\_linear\_preds}{dont\_star\_linear\_preds}
 Specifies whether Nitpick should use Kodkod's transitive closure operator to
 encode non-well-founded ``linear inductive predicates,'' i.e., inductive
diff -r 30f7ce76712d -r 8228b3a4a2ba src/HOL/Nitpick_Examples/Mono_Nits.thy
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Sat Apr 24 17:48:21 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Sun Apr 25 00:10:30 2010 +0200
@@ -21,9 +21,9 @@
   {thy = @{theory}, ctxt = @{context}, max_bisim_depth = ~1, boxes = [],
    stds = [(NONE, true)], wfs = [], user_axioms = NONE, debug = false,
    binary_ints = SOME false, destroy_constrs = false, specialize = false,
-   skolemize = false, star_linear_preds = false, uncurry = false,
-   fast_descrs = false, tac_timeout = NONE, evals = [], case_names = [],
-   def_table = def_table, nondef_table = Symtab.empty, user_nondefs = [],
+   star_linear_preds = false, fast_descrs = false, tac_timeout = NONE,
+   evals = [], case_names = [], def_table = def_table,
+   nondef_table = Symtab.empty, user_nondefs = [],
    simp_table = Unsynchronized.ref Symtab.empty, psimp_table = Symtab.empty,
    choice_spec_table = Symtab.empty, intro_table = Symtab.empty,
    ground_thm_table = Inttab.empty, ersatz_table = [],
diff -r 30f7ce76712d -r 8228b3a4a2ba src/HOL/Nitpick_Examples/Special_Nits.thy
--- a/src/HOL/Nitpick_Examples/Special_Nits.thy	Sat Apr 24 17:48:21 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Special_Nits.thy	Sun Apr 25 00:10:30 2010 +0200
@@ -73,8 +73,6 @@
        \<and> (\<forall>u. b = u \<longrightarrow> f3 b b u b b = f3 u u b u u)"
 nitpick [expect = none]
 nitpick [dont_specialize, expect = none]
-nitpick [dont_skolemize, expect = none]
-nitpick [dont_specialize, dont_skolemize, expect = none]
 sorry
 
 function f4 :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
diff -r 30f7ce76712d -r 8228b3a4a2ba src/HOL/Tools/Nitpick/HISTORY
--- a/src/HOL/Tools/Nitpick/HISTORY	Sat Apr 24 17:48:21 2010 +0200
+++ b/src/HOL/Tools/Nitpick/HISTORY	Sun Apr 25 00:10:30 2010 +0200
@@ -16,8 +16,9 @@
   * Fixed soundness bug related to higher-order constructors
   * Added cache to speed up repeated Kodkod invocations on the same problems
   * Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and "SAT4JLight" to
- 	"MiniSat_JNI", "zChaff_JNI", "BerkMin_Alloy", and "SAT4J_Light"
-  * Removed "sym_break", "flatten_prop", "sharing_depth", and "uncurry" options
+    "MiniSat_JNI", "zChaff_JNI", "BerkMin_Alloy", and "SAT4J_Light"
+  * Removed "skolemize", "uncurry", "sym_break", "flatten_prop", and
+    "sharing_depth" options
 
 Version 2009-1
 
diff -r 30f7ce76712d -r 8228b3a4a2ba src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Sat Apr 24 17:48:21 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Sun Apr 25 00:10:30 2010 +0200
@@ -32,7 +32,6 @@
     binary_ints: bool option,
     destroy_constrs: bool,
     specialize: bool,
-    skolemize: bool,
     star_linear_preds: bool,
     fast_descrs: bool,
     peephole_optim: bool,
@@ -104,7 +103,6 @@
   binary_ints: bool option,
   destroy_constrs: bool,
   specialize: bool,
-  skolemize: bool,
   star_linear_preds: bool,
   fast_descrs: bool,
   peephole_optim: bool,
@@ -192,7 +190,7 @@
     val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths,
          boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug,
          verbose, overlord, user_axioms, assms, merge_type_vars, binary_ints,
-         destroy_constrs, specialize, skolemize, star_linear_preds, fast_descrs,
+         destroy_constrs, specialize, star_linear_preds, fast_descrs,
          peephole_optim, tac_timeout, max_threads, show_skolems, show_datatypes,
          show_consts, evals, formats, max_potential, max_genuine,
          check_potential, check_genuine, batch_size, ...} =
@@ -262,15 +260,14 @@
       {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
        stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
        binary_ints = binary_ints, destroy_constrs = destroy_constrs,
-       specialize = specialize, skolemize = skolemize,
-       star_linear_preds = star_linear_preds, fast_descrs = fast_descrs,
-       tac_timeout = tac_timeout, evals = evals, case_names = case_names,
-       def_table = def_table, nondef_table = nondef_table,
-       user_nondefs = user_nondefs, simp_table = simp_table,
-       psimp_table = psimp_table, choice_spec_table = choice_spec_table,
-       intro_table = intro_table, ground_thm_table = ground_thm_table,
-       ersatz_table = ersatz_table, skolems = Unsynchronized.ref [],
-       special_funs = Unsynchronized.ref [],
+       specialize = specialize, star_linear_preds = star_linear_preds,
+       fast_descrs = fast_descrs, tac_timeout = tac_timeout, evals = evals,
+       case_names = case_names, def_table = def_table,
+       nondef_table = nondef_table, user_nondefs = user_nondefs,
+       simp_table = simp_table, psimp_table = psimp_table,
+       choice_spec_table = choice_spec_table, intro_table = intro_table,
+       ground_thm_table = ground_thm_table, ersatz_table = ersatz_table,
+       skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [],
        unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [],
        constr_cache = Unsynchronized.ref []}
     val frees = Term.add_frees assms_t []
diff -r 30f7ce76712d -r 8228b3a4a2ba src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sat Apr 24 17:48:21 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sun Apr 25 00:10:30 2010 +0200
@@ -25,7 +25,6 @@
     binary_ints: bool option,
     destroy_constrs: bool,
     specialize: bool,
-    skolemize: bool,
     star_linear_preds: bool,
     fast_descrs: bool,
     tac_timeout: Time.time option,
@@ -235,7 +234,6 @@
   binary_ints: bool option,
   destroy_constrs: bool,
   specialize: bool,
-  skolemize: bool,
   star_linear_preds: bool,
   fast_descrs: bool,
   tac_timeout: Time.time option,
diff -r 30f7ce76712d -r 8228b3a4a2ba src/HOL/Tools/Nitpick/nitpick_isar.ML
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Sat Apr 24 17:48:21 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Sun Apr 25 00:10:30 2010 +0200
@@ -55,7 +55,6 @@
    ("binary_ints", "smart"),
    ("destroy_constrs", "true"),
    ("specialize", "true"),
-   ("skolemize", "true"),
    ("star_linear_preds", "true"),
    ("fast_descrs", "true"),
    ("peephole_optim", "true"),
@@ -89,7 +88,6 @@
    ("unary_ints", "binary_ints"),
    ("dont_destroy_constrs", "destroy_constrs"),
    ("dont_specialize", "specialize"),
-   ("dont_skolemize", "skolemize"),
    ("dont_star_linear_preds", "star_linear_preds"),
    ("full_descrs", "fast_descrs"),
    ("no_peephole_optim", "peephole_optim"),
@@ -250,7 +248,6 @@
     val binary_ints = lookup_bool_option "binary_ints"
     val destroy_constrs = lookup_bool "destroy_constrs"
     val specialize = lookup_bool "specialize"
-    val skolemize = lookup_bool "skolemize"
     val star_linear_preds = lookup_bool "star_linear_preds"
     val fast_descrs = lookup_bool "fast_descrs"
     val peephole_optim = lookup_bool "peephole_optim"
@@ -281,9 +278,9 @@
      user_axioms = user_axioms, assms = assms,
      merge_type_vars = merge_type_vars, binary_ints = binary_ints,
      destroy_constrs = destroy_constrs, specialize = specialize,
-     skolemize = skolemize, star_linear_preds = star_linear_preds,
-     fast_descrs = fast_descrs, peephole_optim = peephole_optim,
-     timeout = timeout, tac_timeout = tac_timeout, max_threads = max_threads,
+     star_linear_preds = star_linear_preds, fast_descrs = fast_descrs,
+     peephole_optim = peephole_optim, timeout = timeout,
+     tac_timeout = tac_timeout, max_threads = max_threads,
      show_skolems = show_skolems, show_datatypes = show_datatypes,
      show_consts = show_consts, formats = formats, evals = evals,
      max_potential = max_potential, max_genuine = max_genuine,
diff -r 30f7ce76712d -r 8228b3a4a2ba src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Sat Apr 24 17:48:21 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Sun Apr 25 00:10:30 2010 +0200
@@ -843,8 +843,8 @@
 fun reconstruct_hol_model {show_skolems, show_datatypes, show_consts}
         ({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, stds, wfs, user_axioms,
                       debug, binary_ints, destroy_constrs, specialize,
-                      skolemize, star_linear_preds, fast_descrs, tac_timeout,
-                      evals, case_names, def_table, nondef_table, user_nondefs,
+                      star_linear_preds, fast_descrs, tac_timeout, evals,
+                      case_names, def_table, nondef_table, user_nondefs,
                       simp_table, psimp_table, choice_spec_table, intro_table,
                       ground_thm_table, ersatz_table, skolems, special_funs,
                       unrolled_preds, wf_cache, constr_cache},
@@ -858,16 +858,16 @@
       {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
        stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
        binary_ints = binary_ints, destroy_constrs = destroy_constrs,
-       specialize = specialize, skolemize = skolemize,
-       star_linear_preds = star_linear_preds, fast_descrs = fast_descrs,
-       tac_timeout = tac_timeout, evals = evals, case_names = case_names,
-       def_table = def_table, nondef_table = nondef_table,
-       user_nondefs = user_nondefs, simp_table = simp_table,
-       psimp_table = psimp_table, choice_spec_table = choice_spec_table,
-       intro_table = intro_table, ground_thm_table = ground_thm_table,
-       ersatz_table = ersatz_table, skolems = skolems,
-       special_funs = special_funs, unrolled_preds = unrolled_preds,
-       wf_cache = wf_cache, constr_cache = constr_cache}
+       specialize = specialize, star_linear_preds = star_linear_preds,
+       fast_descrs = fast_descrs, tac_timeout = tac_timeout, evals = evals,
+       case_names = case_names, def_table = def_table,
+       nondef_table = nondef_table, user_nondefs = user_nondefs,
+       simp_table = simp_table, psimp_table = psimp_table,
+       choice_spec_table = choice_spec_table, intro_table = intro_table,
+       ground_thm_table = ground_thm_table, ersatz_table = ersatz_table,
+       skolems = skolems, special_funs = special_funs,
+       unrolled_preds = unrolled_preds, wf_cache = wf_cache,
+       constr_cache = constr_cache}
     val scope =
       {hol_ctxt = hol_ctxt, binarize = binarize, card_assigns = card_assigns,
        bits = bits, bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs}
diff -r 30f7ce76712d -r 8228b3a4a2ba src/HOL/Tools/Nitpick/nitpick_preproc.ML
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Sat Apr 24 17:48:21 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Sun Apr 25 00:10:30 2010 +0200
@@ -1226,14 +1226,15 @@
 
 (** Preprocessor entry point **)
 
+val max_skolem_depth = 4
+
 fun preprocess_term (hol_ctxt as {thy, stds, binary_ints, destroy_constrs,
-                                  boxes, skolemize, ...}) finitizes monos t =
+                                  boxes, ...}) finitizes monos t =
   let
-    val skolem_depth = if skolemize then 4 else ~1
     val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms) =
       t |> unfold_defs_in_term hol_ctxt
         |> close_form
-        |> skolemize_term_and_more hol_ctxt skolem_depth
+        |> skolemize_term_and_more hol_ctxt max_skolem_depth
         |> specialize_consts_in_term hol_ctxt 0
         |> axioms_for_term hol_ctxt
     val binarize =