merged my Auto Nitpick change with Lukas's Predicate Compiler changes
authorblanchet
Wed Oct 28 18:09:30 2009 +0100 (2009-10-28)
changeset 33562b1e2830ee31a
parent 33273 9290fbf0a30e
parent 33561 ab01b72715ef
child 33563 4c983a9d4207
merged my Auto Nitpick change with Lukas's Predicate Compiler changes
src/HOL/IsaMakefile
src/HOL/Main.thy
src/HOL/Nitpick.thy
src/HOL/Quickcheck.thy
     1.1 --- a/doc-src/Nitpick/nitpick.tex	Wed Oct 28 12:21:38 2009 +0000
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Wed Oct 28 18:09:30 2009 +0100
     1.3 @@ -112,6 +112,13 @@
     1.4  machine called \texttt{java}. The examples presented in this manual can be found
     1.5  in Isabelle's \texttt{src/HOL/Nitpick\_Examples/Manual\_Nits.thy} theory.
     1.6  
     1.7 +Throughout this manual, we will explicitly invoke the \textbf{nitpick} command.
     1.8 +Nitpick also provides an automatic mode that can be enabled using the
     1.9 +``Auto Nitpick'' option from the ``Isabelle'' menu in Proof General. In this
    1.10 +mode, Nitpick is run on every newly entered theorem, much like Auto Quickcheck.
    1.11 +The collective time limit for Auto Nitpick and Auto Quickcheck can be set using
    1.12 +the ``Auto Counterexample Time Limit'' option.
    1.13 +
    1.14  \newbox\boxA
    1.15  \setbox\boxA=\hbox{\texttt{nospam}}
    1.16  
    1.17 @@ -154,16 +161,6 @@
    1.18  configured SAT solvers in Isabelle (e.g., for Refute), these will also be
    1.19  available to Nitpick.
    1.20  
    1.21 -Throughout this manual, we will explicitly invoke the \textbf{nitpick} command.
    1.22 -Nitpick also provides an automatic mode that can be enabled by specifying
    1.23 -
    1.24 -\prew
    1.25 -\textbf{nitpick\_params} [\textit{auto}]
    1.26 -\postw
    1.27 -
    1.28 -at the beginning of the theory file. In this mode, Nitpick is run for up to 5
    1.29 -seconds (by default) on every newly entered theorem, much like Auto Quickcheck.
    1.30 -
    1.31  \subsection{Propositional Logic}
    1.32  \label{propositional-logic}
    1.33  
    1.34 @@ -1595,6 +1592,17 @@
    1.35  (\S\ref{authentication}), optimizations
    1.36  (\S\ref{optimizations}), and timeouts (\S\ref{timeouts}).
    1.37  
    1.38 +You can instruct Nitpick to run automatically on newly entered theorems by
    1.39 +enabling the ``Auto Nitpick'' option from the ``Isabelle'' menu in Proof
    1.40 +General. For automatic runs, \textit{user\_axioms} (\S\ref{mode-of-operation})
    1.41 +and \textit{assms} (\S\ref{mode-of-operation}) are implicitly enabled,
    1.42 +\textit{blocking} (\S\ref{mode-of-operation}), \textit{verbose}
    1.43 +(\S\ref{output-format}), and \textit{debug} (\S\ref{output-format}) are
    1.44 +disabled, \textit{max\_potential} (\S\ref{output-format}) is taken to be 0, and
    1.45 +\textit{timeout} (\S\ref{timeouts}) is superseded by the ``Auto Counterexample
    1.46 +Time Limit'' in Proof General's ``Isabelle'' menu. Nitpick's output is also more
    1.47 +concise.
    1.48 +
    1.49  The number of options can be overwhelming at first glance. Do not let that worry
    1.50  you: Nitpick's defaults have been chosen so that it almost always does the right
    1.51  thing, and the most important options have been covered in context in
    1.52 @@ -1622,35 +1630,19 @@
    1.53  \end{enum}
    1.54  
    1.55  Default values are indicated in square brackets. Boolean options have a negated
    1.56 -counterpart (e.g., \textit{auto} vs.\ \textit{no\_auto}). When setting Boolean
    1.57 -options, ``= \textit{true}'' may be omitted.
    1.58 +counterpart (e.g., \textit{blocking} vs.\ \textit{no\_blocking}). When setting
    1.59 +Boolean options, ``= \textit{true}'' may be omitted.
    1.60  
    1.61  \subsection{Mode of Operation}
    1.62  \label{mode-of-operation}
    1.63  
    1.64  \begin{enum}
    1.65 -\opfalse{auto}{no\_auto}
    1.66 -Specifies whether Nitpick should be run automatically on newly entered theorems.
    1.67 -For automatic runs, \textit{user\_axioms} (\S\ref{mode-of-operation}) and
    1.68 -\textit{assms} (\S\ref{mode-of-operation}) are implicitly enabled,
    1.69 -\textit{blocking} (\S\ref{mode-of-operation}), \textit{verbose}
    1.70 -(\S\ref{output-format}), and \textit{debug} (\S\ref{output-format}) are
    1.71 -disabled, \textit{max\_potential} (\S\ref{output-format}) is taken to be 0, and
    1.72 -\textit{auto\_timeout} (\S\ref{timeouts}) is used as the time limit instead of
    1.73 -\textit{timeout} (\S\ref{timeouts}). The output is also more concise.
    1.74 -
    1.75 -\nopagebreak
    1.76 -{\small See also \textit{auto\_timeout} (\S\ref{timeouts}).}
    1.77 -
    1.78  \optrue{blocking}{non\_blocking}
    1.79  Specifies whether the \textbf{nitpick} command should operate synchronously.
    1.80  The asynchronous (non-blocking) mode lets the user start proving the putative
    1.81  theorem while Nitpick looks for a counterexample, but it can also be more
    1.82  confusing. For technical reasons, automatic runs currently always block.
    1.83  
    1.84 -\nopagebreak
    1.85 -{\small See also \textit{auto} (\S\ref{mode-of-operation}).}
    1.86 -
    1.87  \optrue{falsify}{satisfy}
    1.88  Specifies whether Nitpick should look for falsifying examples (countermodels) or
    1.89  satisfying examples (models). This manual assumes throughout that
    1.90 @@ -1670,16 +1662,15 @@
    1.91  considered.
    1.92  
    1.93  \nopagebreak
    1.94 -{\small See also \textit{auto} (\S\ref{mode-of-operation}), \textit{assms}
    1.95 -(\S\ref{mode-of-operation}), and \textit{debug} (\S\ref{output-format}).}
    1.96 +{\small See also \textit{assms} (\S\ref{mode-of-operation}) and \textit{debug}
    1.97 +(\S\ref{output-format}).}
    1.98  
    1.99  \optrue{assms}{no\_assms}
   1.100  Specifies whether the relevant assumptions in structured proof should be
   1.101  considered. The option is implicitly enabled for automatic runs.
   1.102  
   1.103  \nopagebreak
   1.104 -{\small See also \textit{auto} (\S\ref{mode-of-operation})
   1.105 -and \textit{user\_axioms} (\S\ref{mode-of-operation}).}
   1.106 +{\small See also \textit{user\_axioms} (\S\ref{mode-of-operation}).}
   1.107  
   1.108  \opfalse{overlord}{no\_overlord}
   1.109  Specifies whether Nitpick should put its temporary files in
   1.110 @@ -1836,14 +1827,14 @@
   1.111  
   1.112  \nopagebreak
   1.113  {\small See also \textit{card} (\S\ref{scope-of-search}),
   1.114 -\textit{coalesce\_type\_vars} (\S\ref{scope-of-search}), and \textit{verbose}
   1.115 +\textit{merge\_type\_vars} (\S\ref{scope-of-search}), and \textit{verbose}
   1.116  (\S\ref{output-format}).}
   1.117  
   1.118  \opsmart{mono}{non\_box}
   1.119  Specifies the default monotonicity setting to use. This can be overridden on a
   1.120  per-type basis using the \textit{mono}~\qty{type} option described above.
   1.121  
   1.122 -\opfalse{coalesce\_type\_vars}{dont\_coalesce\_type\_vars}
   1.123 +\opfalse{merge\_type\_vars}{dont\_merge\_type\_vars}
   1.124  Specifies whether type variables with the same sort constraints should be
   1.125  merged. Setting this option to \textit{true} can reduce the number of scopes
   1.126  tried and the size of the generated Kodkod formulas, but it also diminishes the
   1.127 @@ -1861,9 +1852,6 @@
   1.128  option is useful to determine which scopes are tried or which SAT solver is
   1.129  used. This option is implicitly disabled for automatic runs.
   1.130  
   1.131 -\nopagebreak
   1.132 -{\small See also \textit{auto} (\S\ref{mode-of-operation}).}
   1.133 -
   1.134  \opfalse{debug}{no\_debug}
   1.135  Specifies whether Nitpick should display additional debugging information beyond
   1.136  what \textit{verbose} already displays. Enabling \textit{debug} also enables
   1.137 @@ -1871,8 +1859,8 @@
   1.138  option is implicitly disabled for automatic runs.
   1.139  
   1.140  \nopagebreak
   1.141 -{\small See also \textit{auto} (\S\ref{mode-of-operation}), \textit{overlord}
   1.142 -(\S\ref{mode-of-operation}), and \textit{batch\_size} (\S\ref{optimizations}).}
   1.143 +{\small See also \textit{overlord} (\S\ref{mode-of-operation}) and
   1.144 +\textit{batch\_size} (\S\ref{optimizations}).}
   1.145  
   1.146  \optrue{show\_skolems}{hide\_skolem}
   1.147  Specifies whether the values of Skolem constants should be displayed as part of
   1.148 @@ -1910,8 +1898,7 @@
   1.149  enabled.
   1.150  
   1.151  \nopagebreak
   1.152 -{\small See also \textit{auto} (\S\ref{mode-of-operation}),
   1.153 -\textit{check\_potential} (\S\ref{authentication}), and
   1.154 +{\small See also \textit{check\_potential} (\S\ref{authentication}) and
   1.155  \textit{sat\_solver} (\S\ref{optimizations}).}
   1.156  
   1.157  \opt{max\_genuine}{int}{$\mathbf{1}$}
   1.158 @@ -1968,8 +1955,7 @@
   1.159  shown to be genuine, Nitpick displays a message to this effect and terminates.
   1.160  
   1.161  \nopagebreak
   1.162 -{\small See also \textit{max\_potential} (\S\ref{output-format}) and
   1.163 -\textit{auto\_timeout} (\S\ref{timeouts}).}
   1.164 +{\small See also \textit{max\_potential} (\S\ref{output-format}).}
   1.165  
   1.166  \opfalse{check\_genuine}{trust\_genuine}
   1.167  Specifies whether genuine and likely genuine counterexamples should be given to
   1.168 @@ -1979,8 +1965,7 @@
   1.169  \texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@in.tum.de}.
   1.170  
   1.171  \nopagebreak
   1.172 -{\small See also \textit{max\_genuine} (\S\ref{output-format}) and
   1.173 -\textit{auto\_timeout} (\S\ref{timeouts}).}
   1.174 +{\small See also \textit{max\_genuine} (\S\ref{output-format}).}
   1.175  
   1.176  \ops{expect}{string}
   1.177  Specifies the expected outcome, which must be one of the following:
   1.178 @@ -2206,21 +2191,14 @@
   1.179  Specifies the maximum amount of time that the \textbf{nitpick} command should
   1.180  spend looking for a counterexample. Nitpick tries to honor this constraint as
   1.181  well as it can but offers no guarantees. For automatic runs,
   1.182 -\textit{auto\_timeout} is used instead.
   1.183 +\textit{timeout} is ignored; instead, Auto Quickcheck and Auto Nitpick share
   1.184 +a time slot whose length is specified by the ``Auto Counterexample Time
   1.185 +Limit'' option in Proof General.
   1.186  
   1.187  \nopagebreak
   1.188 -{\small See also \textit{auto} (\S\ref{mode-of-operation})
   1.189 -and \textit{max\_threads} (\S\ref{optimizations}).}
   1.190 -
   1.191 -\opt{auto\_timeout}{time}{$\mathbf{5}$ s}
   1.192 -Specifies the maximum amount of time that Nitpick should use to find a
   1.193 -counterexample when running automatically. Nitpick tries to honor this
   1.194 -constraint as well as it can but offers no guarantees.
   1.195 -
   1.196 -\nopagebreak
   1.197 -{\small See also \textit{auto} (\S\ref{mode-of-operation}).}
   1.198 -
   1.199 -\opt{tac\_timeout}{time}{$\mathbf{500}$ ms}
   1.200 +{\small See also \textit{max\_threads} (\S\ref{optimizations}).}
   1.201 +
   1.202 +\opt{tac\_timeout}{time}{$\mathbf{500}$\,ms}
   1.203  Specifies the maximum amount of time that the \textit{auto} tactic should use
   1.204  when checking a counterexample, and similarly that \textit{lexicographic\_order}
   1.205  and \textit{sizechange} should use when checking whether a (co)in\-duc\-tive
   1.206 @@ -2398,11 +2376,11 @@
   1.207  & \textit{subgoal}\end{aligned}$
   1.208  \postw
   1.209  
   1.210 +\let\antiq=\textrm
   1.211 +
   1.212  \subsection{Registration of Coinductive Datatypes}
   1.213  \label{registration-of-coinductive-datatypes}
   1.214  
   1.215 -\let\antiq=\textrm
   1.216 -
   1.217  If you have defined a custom coinductive datatype, you can tell Nitpick about
   1.218  it, so that it can use an efficient Kodkod axiomatization similar to the one it
   1.219  uses for lazy lists. The interface for registering and unregistering coinductive
   1.220 @@ -2467,6 +2445,12 @@
   1.221  representation of functions synthesized by Isabelle, which is an implementation
   1.222  detail.
   1.223  
   1.224 +\item[$\bullet$] Nitpick maintains a global cache of wellfoundedness conditions,
   1.225 +which can become invalid if you change the definition of an inductive predicate
   1.226 +that is registered in the cache. To clear the cache,
   1.227 +run Nitpick with the \textit{tac\_timeout} option set to a new value (e.g.,
   1.228 +501$\,\textit{ms}$).
   1.229 +
   1.230  \item[$\bullet$] Nitpick produces spurious counterexamples when invoked after a
   1.231  \textbf{guess} command in a structured proof.
   1.232  
     2.1 --- a/src/HOL/IsaMakefile	Wed Oct 28 12:21:38 2009 +0000
     2.2 +++ b/src/HOL/IsaMakefile	Wed Oct 28 18:09:30 2009 +0100
     2.3 @@ -102,6 +102,7 @@
     2.4    $(SRC)/Provers/hypsubst.ML \
     2.5    $(SRC)/Provers/quantifier1.ML \
     2.6    $(SRC)/Provers/splitter.ML \
     2.7 +  $(SRC)/Tools/Auto_Counterexample.thy \
     2.8    $(SRC)/Tools/Code/code_haskell.ML \
     2.9    $(SRC)/Tools/Code/code_ml.ML \
    2.10    $(SRC)/Tools/Code/code_preproc.ML \
    2.11 @@ -114,6 +115,7 @@
    2.12    $(SRC)/Tools/IsaPlanner/rw_tools.ML \
    2.13    $(SRC)/Tools/IsaPlanner/zipper.ML \
    2.14    $(SRC)/Tools/atomize_elim.ML \
    2.15 +  $(SRC)/Tools/auto_counterexample.ML \
    2.16    $(SRC)/Tools/auto_solve.ML \
    2.17    $(SRC)/Tools/coherent.ML \
    2.18    $(SRC)/Tools/cong_tac.ML \
     3.1 --- a/src/HOL/Main.thy	Wed Oct 28 12:21:38 2009 +0000
     3.2 +++ b/src/HOL/Main.thy	Wed Oct 28 18:09:30 2009 +0100
     3.3 @@ -1,7 +1,7 @@
     3.4  header {* Main HOL *}
     3.5  
     3.6  theory Main
     3.7 -imports Plain Nitpick Predicate_Compile Recdef
     3.8 +imports Plain Nitpick
     3.9  begin
    3.10  
    3.11  text {*
     4.1 --- a/src/HOL/Nitpick.thy	Wed Oct 28 12:21:38 2009 +0000
     4.2 +++ b/src/HOL/Nitpick.thy	Wed Oct 28 18:09:30 2009 +0100
     4.3 @@ -8,7 +8,7 @@
     4.4  header {* Nitpick: Yet Another Counterexample Generator for Isabelle/HOL *}
     4.5  
     4.6  theory Nitpick
     4.7 -imports Map SAT
     4.8 +imports Map Quickcheck SAT
     4.9  uses ("Tools/Nitpick/kodkod.ML")
    4.10       ("Tools/Nitpick/kodkod_sat.ML")
    4.11       ("Tools/Nitpick/nitpick_util.ML")
    4.12 @@ -117,12 +117,16 @@
    4.13   apply (simp only: unit.cases)
    4.14  by simp
    4.15  
    4.16 +declare unit.cases [nitpick_simp del]
    4.17 +
    4.18  lemma nat_case_def [nitpick_def]:
    4.19  "nat_case x f n \<equiv> if n = 0 then x else f (n - 1)"
    4.20  apply (rule eq_reflection)
    4.21  by (case_tac n) auto
    4.22  
    4.23 -lemmas dvd_def = dvd_eq_mod_eq_0 [THEN eq_reflection, nitpick_def]
    4.24 +declare nat.cases [nitpick_simp del]
    4.25 +
    4.26 +lemmas [nitpick_def] = dvd_eq_mod_eq_0 [THEN eq_reflection]
    4.27  
    4.28  lemma list_size_simp [nitpick_simp]:
    4.29  "list_size f xs = (if xs = [] then 0
    4.30 @@ -206,6 +210,21 @@
    4.31  definition of_frac :: "'a \<Rightarrow> 'b\<Colon>{inverse,ring_1}" where
    4.32  "of_frac q \<equiv> of_int (num q) / of_int (denom q)"
    4.33  
    4.34 +(* While Nitpick normally avoids to unfold definitions for locales, it
    4.35 +   unfortunately needs to unfold them when dealing with the following built-in
    4.36 +   constants. A cleaner approach would be to change "Nitpick_HOL" and
    4.37 +   "Nitpick_Nits" so that they handle the unexpanded overloaded constants
    4.38 +   directly, but this is slightly more tricky to implement. *)
    4.39 +lemmas [nitpick_def] = div_int_inst.div_int div_int_inst.mod_int
    4.40 +    div_nat_inst.div_nat div_nat_inst.mod_nat lower_semilattice_fun_inst.inf_fun
    4.41 +    minus_fun_inst.minus_fun minus_int_inst.minus_int minus_nat_inst.minus_nat
    4.42 +    one_int_inst.one_int one_nat_inst.one_nat ord_fun_inst.less_eq_fun
    4.43 +    ord_int_inst.less_eq_int ord_int_inst.less_int ord_nat_inst.less_eq_nat
    4.44 +    ord_nat_inst.less_nat plus_int_inst.plus_int plus_nat_inst.plus_nat
    4.45 +    times_int_inst.times_int times_nat_inst.times_nat uminus_int_inst.uminus_int
    4.46 +    upper_semilattice_fun_inst.sup_fun zero_int_inst.zero_int
    4.47 +    zero_nat_inst.zero_nat
    4.48 +
    4.49  use "Tools/Nitpick/kodkod.ML"
    4.50  use "Tools/Nitpick/kodkod_sat.ML"
    4.51  use "Tools/Nitpick/nitpick_util.ML"
    4.52 @@ -222,6 +241,8 @@
    4.53  use "Tools/Nitpick/nitpick_tests.ML"
    4.54  use "Tools/Nitpick/minipick.ML"
    4.55  
    4.56 +setup {* Nitpick_Isar.setup *}
    4.57 +
    4.58  hide (open) const unknown undefined_fast_The undefined_fast_Eps bisim 
    4.59      bisim_iterator_max Tha refl' wf' wf_wfrec wf_wfrec' wfrec' card' setsum'
    4.60      fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac
    4.61 @@ -230,10 +251,10 @@
    4.62  hide (open) type bisim_iterator pair_box fun_box
    4.63  hide (open) fact If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def
    4.64      wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def fold_graph'_def
    4.65 -    The_psimp Eps_psimp unit_case_def nat_case_def dvd_def list_size_simp
    4.66 -    nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def zero_frac_def
    4.67 -    one_frac_def num_def denom_def norm_frac_def frac_def plus_frac_def
    4.68 -    times_frac_def uminus_frac_def number_of_frac_def inverse_frac_def
    4.69 -    less_eq_frac_def of_frac_def
    4.70 +    The_psimp Eps_psimp unit_case_def nat_case_def list_size_simp nat_gcd_def
    4.71 +    nat_lcm_def int_gcd_def int_lcm_def Frac_def zero_frac_def one_frac_def
    4.72 +    num_def denom_def norm_frac_def frac_def plus_frac_def times_frac_def
    4.73 +    uminus_frac_def number_of_frac_def inverse_frac_def less_eq_frac_def
    4.74 +    of_frac_def
    4.75  
    4.76  end
     5.1 --- a/src/HOL/Quickcheck.thy	Wed Oct 28 12:21:38 2009 +0000
     5.2 +++ b/src/HOL/Quickcheck.thy	Wed Oct 28 18:09:30 2009 +0100
     5.3 @@ -126,6 +126,8 @@
     5.4    shows "random_aux k = rhs k"
     5.5    using assms by (rule code_numeral.induct)
     5.6  
     5.7 +setup {* Quickcheck.setup *}
     5.8 +
     5.9  subsection {* the Random-Predicate Monad *} 
    5.10  
    5.11  types 'a randompred = "Random.seed \<Rightarrow> ('a Predicate.pred \<times> Random.seed)"
     6.1 --- a/src/HOL/Tools/Nitpick/HISTORY	Wed Oct 28 12:21:38 2009 +0000
     6.2 +++ b/src/HOL/Tools/Nitpick/HISTORY	Wed Oct 28 18:09:30 2009 +0100
     6.3 @@ -6,6 +6,9 @@
     6.4      "nitpick_ind_intro" to "nitpick_intro"
     6.5    * Replaced "special_depth" and "skolemize_depth" options by "specialize"
     6.6      and "skolemize"
     6.7 +  * Renamed "coalesce_type_vars" to "merge_type_vars"
     6.8 +  * Optimized Kodkod encoding of datatypes whose constructors don't appear in
     6.9 +    the formula to falsify
    6.10    * Fixed monotonicity check
    6.11  
    6.12  Version 1.2.2 (16 Oct 2009)
     7.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Wed Oct 28 12:21:38 2009 +0000
     7.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Wed Oct 28 18:09:30 2009 +0100
     7.3 @@ -23,7 +23,7 @@
     7.4      overlord: bool,
     7.5      user_axioms: bool option,
     7.6      assms: bool,
     7.7 -    coalesce_type_vars: bool,
     7.8 +    merge_type_vars: bool,
     7.9      destroy_constrs: bool,
    7.10      specialize: bool,
    7.11      skolemize: bool,
    7.12 @@ -88,7 +88,7 @@
    7.13    overlord: bool,
    7.14    user_axioms: bool option,
    7.15    assms: bool,
    7.16 -  coalesce_type_vars: bool,
    7.17 +  merge_type_vars: bool,
    7.18    destroy_constrs: bool,
    7.19    specialize: bool,
    7.20    skolemize: bool,
    7.21 @@ -175,7 +175,7 @@
    7.22      val ctxt = Proof.context_of state
    7.23      val {cards_assigns, maxes_assigns, iters_assigns, bisim_depths, boxes,
    7.24           monos, wfs, sat_solver, blocking, falsify, debug, verbose, overlord,
    7.25 -         user_axioms, assms, coalesce_type_vars, destroy_constrs, specialize,
    7.26 +         user_axioms, assms, merge_type_vars, destroy_constrs, specialize,
    7.27           skolemize, star_linear_preds, uncurry, fast_descrs, peephole_optim,
    7.28           tac_timeout, sym_break, sharing_depth, flatten_props, max_threads,
    7.29           show_skolems, show_datatypes, show_consts, evals, formats,
    7.30 @@ -187,7 +187,7 @@
    7.31      val pprint =
    7.32        if auto then
    7.33          Unsynchronized.change state_ref o Proof.goal_message o K
    7.34 -        o curry Pretty.blk 0 o cons (Pretty.str "") o single
    7.35 +        o Pretty.chunks o cons (Pretty.str "") o single
    7.36          o Pretty.mark Markup.hilite
    7.37        else
    7.38          priority o Pretty.string_of
    7.39 @@ -220,7 +220,7 @@
    7.40                      neg_t
    7.41      val (assms_t, evals) =
    7.42        assms_t :: evals
    7.43 -      |> coalesce_type_vars ? coalesce_type_vars_in_terms
    7.44 +      |> merge_type_vars ? merge_type_vars_in_terms
    7.45        |> hd pairf tl
    7.46      val original_max_potential = max_potential
    7.47      val original_max_genuine = max_genuine
    7.48 @@ -283,6 +283,21 @@
    7.49              handle TYPE (_, Ts, ts) =>
    7.50                     raise TYPE ("Nitpick.pick_them_nits_in_term", Ts, ts)
    7.51  
    7.52 +    val core_u = nut_from_term thy fast_descrs (!special_funs) Eq core_t
    7.53 +    val def_us = map (nut_from_term thy fast_descrs (!special_funs) DefEq)
    7.54 +                     def_ts
    7.55 +    val nondef_us = map (nut_from_term thy fast_descrs (!special_funs) Eq)
    7.56 +                        nondef_ts
    7.57 +    val (free_names, const_names) =
    7.58 +      fold add_free_and_const_names (core_u :: def_us @ nondef_us) ([], [])
    7.59 +    val (sel_names, nonsel_names) =
    7.60 +      List.partition (is_sel o nickname_of) const_names
    7.61 +    val would_be_genuine = got_all_user_axioms andalso none_true wfs
    7.62 +(*
    7.63 +    val _ = List.app (priority o string_for_nut ctxt)
    7.64 +                     (core_u :: def_us @ nondef_us)
    7.65 +*)
    7.66 +
    7.67      val unique_scope = forall (equal 1 o length o snd) cards_assigns
    7.68      (* typ -> bool *)
    7.69      fun is_free_type_monotonic T =
    7.70 @@ -298,6 +313,8 @@
    7.71          not (is_pure_typedef thy T) orelse is_univ_typedef thy T
    7.72          orelse is_number_type thy T
    7.73          orelse formulas_monotonic ext_ctxt T def_ts nondef_ts core_t
    7.74 +    fun is_datatype_shallow T =
    7.75 +      not (exists (equal T o domain_type o type_of) sel_names)
    7.76      val Ts = ground_types_in_terms ext_ctxt (core_t :: def_ts @ nondef_ts)
    7.77               |> sort TermOrd.typ_ord
    7.78      val (all_dataTs, all_free_Ts) =
    7.79 @@ -326,7 +343,7 @@
    7.80          ()
    7.81      val mono_Ts = mono_dataTs @ mono_free_Ts
    7.82      val nonmono_Ts = nonmono_dataTs @ nonmono_free_Ts
    7.83 -
    7.84 +    val shallow_dataTs = filter is_datatype_shallow mono_dataTs
    7.85  (*
    7.86      val _ = priority "Monotonic datatypes:"
    7.87      val _ = List.app (priority o string_for_type ctxt) mono_dataTs
    7.88 @@ -338,19 +355,6 @@
    7.89      val _ = List.app (priority o string_for_type ctxt) nonmono_free_Ts
    7.90  *)
    7.91  
    7.92 -    val core_u = nut_from_term thy fast_descrs (!special_funs) Eq core_t
    7.93 -    val def_us = map (nut_from_term thy fast_descrs (!special_funs) DefEq)
    7.94 -                     def_ts
    7.95 -    val nondef_us = map (nut_from_term thy fast_descrs (!special_funs) Eq)
    7.96 -                        nondef_ts
    7.97 -    val (free_names, const_names) =
    7.98 -      fold add_free_and_const_names (core_u :: def_us @ nondef_us) ([], [])
    7.99 -    val nonsel_names = filter_out (is_sel o nickname_of) const_names
   7.100 -    val would_be_genuine = got_all_user_axioms andalso none_true wfs
   7.101 -(*
   7.102 -    val _ = List.app (priority o string_for_nut ctxt)
   7.103 -                     (core_u :: def_us @ nondef_us)
   7.104 -*)
   7.105      val need_incremental = Int.max (max_potential, max_genuine) >= 2
   7.106      val effective_sat_solver =
   7.107        if sat_solver <> "smart" then
   7.108 @@ -778,11 +782,9 @@
   7.109                     case scope_count (do_filter (!generated_problems)) scope of
   7.110                       0 => I
   7.111                     | n =>
   7.112 -                     if scope_count (do_filter (these (!checked_problems)))
   7.113 -                                    scope = n then
   7.114 -                       Integer.add 1
   7.115 -                     else
   7.116 -                       I) (!generated_scopes) 0
   7.117 +                     scope_count (do_filter (these (!checked_problems)))
   7.118 +                                 scope = n
   7.119 +                     ? Integer.add 1) (!generated_scopes) 0
   7.120        in
   7.121          "Nitpick " ^ did_so_and_so ^
   7.122          (if is_some (!checked_problems) andalso total > 0 then
   7.123 @@ -814,6 +816,7 @@
   7.124  
   7.125      val _ = scopes := all_scopes ext_ctxt sym_break cards_assigns maxes_assigns
   7.126                                   iters_assigns bisim_depths mono_Ts nonmono_Ts
   7.127 +                                 shallow_dataTs
   7.128      val batches = batch_list batch_size (!scopes)
   7.129      val outcome_code =
   7.130        (run_batches 0 (length batches) batches (max_potential, max_genuine, 0)
     8.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Oct 28 12:21:38 2009 +0000
     8.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Oct 28 18:09:30 2009 +0100
     8.3 @@ -125,7 +125,7 @@
     8.4    val is_inductive_pred : extended_context -> styp -> bool
     8.5    val is_constr_pattern_lhs : theory -> term -> bool
     8.6    val is_constr_pattern_formula : theory -> term -> bool
     8.7 -  val coalesce_type_vars_in_terms : term list -> term list
     8.8 +  val merge_type_vars_in_terms : term list -> term list
     8.9    val ground_types_in_type : extended_context -> typ -> typ list
    8.10    val ground_types_in_terms : extended_context -> term list -> typ list
    8.11    val format_type : int list -> int list -> typ -> typ
    8.12 @@ -1016,24 +1016,6 @@
    8.13        | do_eq _ = false
    8.14    in do_eq end
    8.15  
    8.16 -(* This table is not pretty. A better approach would be to avoid expanding the
    8.17 -   operators to their low-level definitions, but this would require dealing with
    8.18 -   overloading. *)
    8.19 -val built_in_built_in_defs =
    8.20 -  [@{thm div_int_inst.div_int}, @{thm div_int_inst.mod_int},
    8.21 -   @{thm div_nat_inst.div_nat}, @{thm div_nat_inst.mod_nat},
    8.22 -   @{thm lower_semilattice_fun_inst.inf_fun}, @{thm minus_fun_inst.minus_fun},
    8.23 -   @{thm minus_int_inst.minus_int}, @{thm minus_nat_inst.minus_nat},
    8.24 -   @{thm one_int_inst.one_int}, @{thm one_nat_inst.one_nat},
    8.25 -   @{thm ord_fun_inst.less_eq_fun}, @{thm ord_int_inst.less_eq_int},
    8.26 -   @{thm ord_int_inst.less_int}, @{thm ord_nat_inst.less_eq_nat},
    8.27 -   @{thm ord_nat_inst.less_nat}, @{thm plus_int_inst.plus_int},
    8.28 -   @{thm plus_nat_inst.plus_nat}, @{thm times_int_inst.times_int},
    8.29 -   @{thm times_nat_inst.times_nat}, @{thm uminus_int_inst.uminus_int},
    8.30 -   @{thm upper_semilattice_fun_inst.sup_fun}, @{thm zero_int_inst.zero_int},
    8.31 -   @{thm zero_nat_inst.zero_nat}]
    8.32 -  |> map prop_of
    8.33 -
    8.34  (* theory -> term list * term list * term list *)
    8.35  fun all_axioms_of thy =
    8.36    let
    8.37 @@ -1054,8 +1036,7 @@
    8.38      val (built_in_nondefs, user_nondefs) =
    8.39        List.partition (is_typedef_axiom thy false) user_nondefs
    8.40        |>> append built_in_nondefs
    8.41 -    val defs = built_in_built_in_defs @
    8.42 -               (thy |> PureThy.all_thms_of
    8.43 +    val defs = (thy |> PureThy.all_thms_of
    8.44                      |> filter (equal Thm.definitionK o Thm.get_kind o snd)
    8.45                      |> map (prop_of o snd) |> filter is_plain_definition) @
    8.46                 user_defs @ built_in_defs
    8.47 @@ -1309,10 +1290,6 @@
    8.48      |> fold_rev (curry absdummy) (func_Ts @ [dataT])
    8.49    end
    8.50  
    8.51 -val redefined_in_Nitpick_thy =
    8.52 -  [@{const_name option_case}, @{const_name nat_case}, @{const_name list_case},
    8.53 -   @{const_name list_size}]
    8.54 -
    8.55  (* theory -> string -> typ -> typ -> term -> term *)
    8.56  fun optimized_record_get thy s rec_T res_T t =
    8.57    let val constr_x = the_single (datatype_constrs thy rec_T) in
    8.58 @@ -1382,7 +1359,6 @@
    8.59    (is_real_equational_fun ext_ctxt orf is_real_inductive_pred ext_ctxt
    8.60     orf (String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst)
    8.61    andf (not o has_trivial_definition thy def_table)
    8.62 -  andf (not o member (op =) redefined_in_Nitpick_thy o fst)
    8.63  
    8.64  (* term * term -> term *)
    8.65  fun s_betapply (Const (@{const_name If}, _) $ @{const True} $ t, _) = t
    8.66 @@ -1630,6 +1606,7 @@
    8.67                                   (tac ctxt (auto_tac (clasimpset_of ctxt))))
    8.68         #> the #> Goal.finish ctxt) goal
    8.69  
    8.70 +val max_cached_wfs = 100
    8.71  val cached_timeout = Unsynchronized.ref (SOME Time.zeroTime)
    8.72  val cached_wf_props : (term * bool) list Unsynchronized.ref =
    8.73    Unsynchronized.ref []
    8.74 @@ -1663,8 +1640,11 @@
    8.75                   else
    8.76                     ()
    8.77         in
    8.78 -         if tac_timeout = (!cached_timeout) then ()
    8.79 -         else (cached_wf_props := []; cached_timeout := tac_timeout);
    8.80 +         if tac_timeout = (!cached_timeout)
    8.81 +            andalso length (!cached_wf_props) < max_cached_wfs then
    8.82 +           ()
    8.83 +         else
    8.84 +           (cached_wf_props := []; cached_timeout := tac_timeout);
    8.85           case AList.lookup (op =) (!cached_wf_props) prop of
    8.86             SOME wf => wf
    8.87           | NONE =>
    8.88 @@ -1879,9 +1859,7 @@
    8.89  (* extended_context -> styp -> term list *)
    8.90  fun raw_equational_fun_axioms (ext_ctxt as {thy, fast_descrs, simp_table,
    8.91                                              psimp_table, ...}) (x as (s, _)) =
    8.92 -  if s mem redefined_in_Nitpick_thy then
    8.93 -    []
    8.94 -  else case def_props_for_const thy fast_descrs (!simp_table) x of
    8.95 +  case def_props_for_const thy fast_descrs (!simp_table) x of
    8.96      [] => (case def_props_for_const thy fast_descrs psimp_table x of
    8.97               [] => [inductive_pred_axiom ext_ctxt x]
    8.98             | psimps => psimps)
    8.99 @@ -1890,7 +1868,7 @@
   8.100  val equational_fun_axioms = map extensionalize oo raw_equational_fun_axioms
   8.101  
   8.102  (* term list -> term list *)
   8.103 -fun coalesce_type_vars_in_terms ts =
   8.104 +fun merge_type_vars_in_terms ts =
   8.105    let
   8.106      (* typ -> (sort * string) list -> (sort * string) list *)
   8.107      fun add_type (TFree (s, S)) table =
     9.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Wed Oct 28 12:21:38 2009 +0000
     9.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Wed Oct 28 18:09:30 2009 +0100
     9.3 @@ -10,7 +10,9 @@
     9.4  sig
     9.5    type params = Nitpick.params
     9.6  
     9.7 +  val auto: bool Unsynchronized.ref
     9.8    val default_params : theory -> (string * string) list -> params
     9.9 +  val setup : theory -> theory
    9.10  end
    9.11  
    9.12  structure Nitpick_Isar : NITPICK_ISAR =
    9.13 @@ -22,6 +24,14 @@
    9.14  open Nitpick_Nut
    9.15  open Nitpick
    9.16  
    9.17 +val auto = Unsynchronized.ref false;
    9.18 +
    9.19 +val _ = ProofGeneralPgip.add_preference Preferences.category_tracing
    9.20 +            (setmp_CRITICAL auto false
    9.21 +                 (fn () => Preferences.bool_pref auto
    9.22 +                               "auto-nitpick"
    9.23 +                               "Whether to run Nitpick automatically.") ())
    9.24 +
    9.25  type raw_param = string * string list
    9.26  
    9.27  val default_default_params =
    9.28 @@ -33,12 +43,11 @@
    9.29     ("wf", ["smart"]),
    9.30     ("sat_solver", ["smart"]),
    9.31     ("batch_size", ["smart"]),
    9.32 -   ("auto", ["false"]),
    9.33     ("blocking", ["true"]),
    9.34     ("falsify", ["true"]),
    9.35     ("user_axioms", ["smart"]),
    9.36     ("assms", ["true"]),
    9.37 -   ("coalesce_type_vars", ["false"]),
    9.38 +   ("merge_type_vars", ["false"]),
    9.39     ("destroy_constrs", ["true"]),
    9.40     ("specialize", ["true"]),
    9.41     ("skolemize", ["true"]),
    9.42 @@ -47,7 +56,6 @@
    9.43     ("fast_descrs", ["true"]),
    9.44     ("peephole_optim", ["true"]),
    9.45     ("timeout", ["30 s"]),
    9.46 -   ("auto_timeout", ["5 s"]),
    9.47     ("tac_timeout", ["500 ms"]),
    9.48     ("sym_break", ["20"]),
    9.49     ("sharing_depth", ["3"]),
    9.50 @@ -70,12 +78,11 @@
    9.51    [("dont_box", "box"),
    9.52     ("non_mono", "mono"),
    9.53     ("non_wf", "wf"),
    9.54 -   ("no_auto", "auto"),
    9.55     ("non_blocking", "blocking"),
    9.56     ("satisfy", "falsify"),
    9.57     ("no_user_axioms", "user_axioms"),
    9.58     ("no_assms", "assms"),
    9.59 -   ("dont_coalesce_type_vars", "coalesce_type_vars"),
    9.60 +   ("dont_merge_type_vars", "merge_type_vars"),
    9.61     ("dont_destroy_constrs", "destroy_constrs"),
    9.62     ("dont_specialize", "specialize"),
    9.63     ("dont_skolemize", "skolemize"),
    9.64 @@ -126,31 +133,22 @@
    9.65    | NONE => (name, value)
    9.66  
    9.67  structure TheoryData = TheoryDataFun(
    9.68 -  type T = {params: raw_param list, registered_auto: bool}
    9.69 -  val empty = {params = rev default_default_params, registered_auto = false}
    9.70 +  type T = {params: raw_param list}
    9.71 +  val empty = {params = rev default_default_params}
    9.72    val copy = I
    9.73    val extend = I
    9.74 -  fun merge _ ({params = ps1, registered_auto = a1},
    9.75 -               {params = ps2, registered_auto = a2}) =
    9.76 -    {params = AList.merge (op =) (op =) (ps1, ps2),
    9.77 -     registered_auto = a1 orelse a2})
    9.78 +  fun merge _ ({params = ps1}, {params = ps2}) =
    9.79 +    {params = AList.merge (op =) (op =) (ps1, ps2)})
    9.80  
    9.81  (* raw_param -> theory -> theory *)
    9.82  fun set_default_raw_param param thy =
    9.83 -  let val {params, registered_auto} = TheoryData.get thy in
    9.84 +  let val {params} = TheoryData.get thy in
    9.85      TheoryData.put
    9.86 -      {params = AList.update (op =) (unnegate_raw_param param) params,
    9.87 -       registered_auto = registered_auto} thy
    9.88 +        {params = AList.update (op =) (unnegate_raw_param param) params} thy
    9.89    end
    9.90  (* theory -> raw_param list *)
    9.91  val default_raw_params = #params o TheoryData.get
    9.92  
    9.93 -(* theory -> theory *)
    9.94 -fun set_registered_auto thy =
    9.95 -  TheoryData.put {params = default_raw_params thy, registered_auto = true} thy
    9.96 -(* theory -> bool *)
    9.97 -val is_registered_auto = #registered_auto o TheoryData.get
    9.98 -
    9.99  (* string -> bool *)
   9.100  fun is_punctuation s = (s = "," orelse s = "-" orelse s = "\<midarrow>")
   9.101  
   9.102 @@ -305,7 +303,7 @@
   9.103      val overlord = lookup_bool "overlord"
   9.104      val user_axioms = lookup_bool_option "user_axioms"
   9.105      val assms = lookup_bool "assms"
   9.106 -    val coalesce_type_vars = lookup_bool "coalesce_type_vars"
   9.107 +    val merge_type_vars = lookup_bool "merge_type_vars"
   9.108      val destroy_constrs = lookup_bool "destroy_constrs"
   9.109      val specialize = lookup_bool "specialize"
   9.110      val skolemize = lookup_bool "skolemize"
   9.111 @@ -313,8 +311,7 @@
   9.112      val uncurry = lookup_bool "uncurry"
   9.113      val fast_descrs = lookup_bool "fast_descrs"
   9.114      val peephole_optim = lookup_bool "peephole_optim"
   9.115 -    val timeout = if auto then lookup_time "auto_timeout"
   9.116 -                  else lookup_time "timeout"
   9.117 +    val timeout = if auto then NONE else lookup_time "timeout"
   9.118      val tac_timeout = lookup_time "tac_timeout"
   9.119      val sym_break = Int.max (0, lookup_int "sym_break")
   9.120      val sharing_depth = Int.max (1, lookup_int "sharing_depth")
   9.121 @@ -326,8 +323,8 @@
   9.122      val show_consts = show_all orelse lookup_bool "show_consts"
   9.123      val formats = lookup_ints_assigns read_term_polymorphic "format" 0
   9.124      val evals = lookup_term_list "eval"
   9.125 -    val max_potential = if auto then 0
   9.126 -                        else Int.max (0, lookup_int "max_potential")
   9.127 +    val max_potential =
   9.128 +      if auto then 0 else Int.max (0, lookup_int "max_potential")
   9.129      val max_genuine = Int.max (0, lookup_int "max_genuine")
   9.130      val check_potential = lookup_bool "check_potential"
   9.131      val check_genuine = lookup_bool "check_genuine"
   9.132 @@ -341,7 +338,7 @@
   9.133       monos = monos, wfs = wfs, sat_solver = sat_solver, blocking = blocking,
   9.134       falsify = falsify, debug = debug, verbose = verbose, overlord = overlord,
   9.135       user_axioms = user_axioms, assms = assms,
   9.136 -     coalesce_type_vars = coalesce_type_vars, destroy_constrs = destroy_constrs,
   9.137 +     merge_type_vars = merge_type_vars, destroy_constrs = destroy_constrs,
   9.138       specialize = specialize, skolemize = skolemize,
   9.139       star_linear_preds = star_linear_preds, uncurry = uncurry,
   9.140       fast_descrs = fast_descrs, peephole_optim = peephole_optim,
   9.141 @@ -412,79 +409,58 @@
   9.142         | Refute.REFUTE (loc, details) =>
   9.143           error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^ ".")
   9.144  
   9.145 -(* raw_param list -> bool -> int -> Proof.state -> Proof.state *)
   9.146 +(* raw_param list -> bool -> int -> Proof.state -> bool * Proof.state *)
   9.147  fun pick_nits override_params auto subgoal state =
   9.148    let
   9.149      val thy = Proof.theory_of state
   9.150      val ctxt = Proof.context_of state
   9.151 -    val thm = snd (snd (Proof.get_goal state))
   9.152 +    val thm = state |> Proof.get_goal |> snd |> snd
   9.153      val _ = List.app check_raw_param override_params
   9.154      val params as {blocking, debug, ...} =
   9.155        extract_params ctxt auto (default_raw_params thy) override_params
   9.156 -    (* unit -> Proof.state *)
   9.157 +    (* unit -> bool * Proof.state *)
   9.158      fun go () =
   9.159 -      (if auto then perhaps o try
   9.160 -       else if debug then fn f => fn x => f x
   9.161 -       else handle_exceptions ctxt)
   9.162 -      (fn state => pick_nits_in_subgoal state params auto subgoal |> snd)
   9.163 -      state
   9.164 +      (false, state)
   9.165 +      |> (if auto then perhaps o try
   9.166 +          else if debug then fn f => fn x => f x
   9.167 +          else handle_exceptions ctxt)
   9.168 +         (fn (_, state) => pick_nits_in_subgoal state params auto subgoal
   9.169 +                           |>> equal "genuine")
   9.170    in
   9.171 -    if auto orelse blocking then
   9.172 -      go ()
   9.173 -    else
   9.174 -      (SimpleThread.fork true (fn () => (go (); ()));
   9.175 -       state)
   9.176 +    if auto orelse blocking then go ()
   9.177 +    else (SimpleThread.fork true (fn () => (go (); ())); (false, state))
   9.178    end
   9.179  
   9.180  (* (TableFun().key * string list) list option * int option
   9.181     -> Toplevel.transition -> Toplevel.transition *)
   9.182  fun nitpick_trans (opt_params, opt_subgoal) =
   9.183    Toplevel.keep (K ()
   9.184 -      o pick_nits (these opt_params) false (the_default 1 opt_subgoal)
   9.185 +      o snd o pick_nits (these opt_params) false (the_default 1 opt_subgoal)
   9.186        o Toplevel.proof_of)
   9.187  
   9.188  (* raw_param -> string *)
   9.189  fun string_for_raw_param (name, value) =
   9.190    name ^ " = " ^ stringify_raw_param_value value
   9.191  
   9.192 -(* bool -> Proof.state -> Proof.state *)
   9.193 -fun pick_nits_auto interactive state =
   9.194 -  let val thy = Proof.theory_of state in
   9.195 -    ((interactive andalso not (!Toplevel.quiet)
   9.196 -      andalso the (general_lookup_bool false (default_raw_params thy)
   9.197 -                  (SOME false) "auto"))
   9.198 -     ? pick_nits [] true 0) state
   9.199 -  end
   9.200 -
   9.201 -(* theory -> theory *)
   9.202 -fun register_auto thy =
   9.203 -  (not (is_registered_auto thy)
   9.204 -   ? (set_registered_auto
   9.205 -      #> Context.theory_map (Specification.add_theorem_hook pick_nits_auto)))
   9.206 -  thy
   9.207 -
   9.208  (* (TableFun().key * string) list option -> Toplevel.transition
   9.209     -> Toplevel.transition *)
   9.210  fun nitpick_params_trans opt_params =
   9.211    Toplevel.theory
   9.212 -      (fn thy =>
   9.213 -          let val thy = fold set_default_raw_param (these opt_params) thy in
   9.214 -            writeln ("Default parameters for Nitpick:\n" ^
   9.215 -                     (case rev (default_raw_params thy) of
   9.216 -                        [] => "none"
   9.217 -                      | params =>
   9.218 -                        (map check_raw_param params;
   9.219 -                         params |> map string_for_raw_param |> sort_strings
   9.220 -                                |> cat_lines)));
   9.221 -            register_auto thy
   9.222 -          end)
   9.223 +      (fold set_default_raw_param (these opt_params)
   9.224 +       #> tap (fn thy => 
   9.225 +                  writeln ("Default parameters for Nitpick:\n" ^
   9.226 +                           (case rev (default_raw_params thy) of
   9.227 +                              [] => "none"
   9.228 +                            | params =>
   9.229 +                              (map check_raw_param params;
   9.230 +                               params |> map string_for_raw_param
   9.231 +                                      |> sort_strings |> cat_lines)))))
   9.232  
   9.233  (* OuterParse.token list
   9.234     -> (Toplevel.transition -> Toplevel.transition) * OuterParse.token list *)
   9.235 -fun scan_nitpick_command tokens =
   9.236 -  (scan_params -- Scan.option OuterParse.nat) tokens |>> nitpick_trans
   9.237 -fun scan_nitpick_params_command tokens =
   9.238 -  scan_params tokens |>> nitpick_params_trans
   9.239 +val scan_nitpick_command =
   9.240 +  (scan_params -- Scan.option OuterParse.nat) #>> nitpick_trans
   9.241 +val scan_nitpick_params_command = scan_params #>> nitpick_params_trans
   9.242  
   9.243  val _ = OuterSyntax.improper_command "nitpick"
   9.244              "try to find a counterexample for a given subgoal using Kodkod"
   9.245 @@ -493,4 +469,10 @@
   9.246              "set and display the default parameters for Nitpick"
   9.247              OuterKeyword.thy_decl scan_nitpick_params_command
   9.248  
   9.249 +(* Proof.state -> bool * Proof.state *)
   9.250 +fun auto_nitpick state =
   9.251 +  if not (!auto) then (false, state) else pick_nits [] true 1 state
   9.252 +
   9.253 +val setup = Auto_Counterexample.register_tool ("nitpick", auto_nitpick)
   9.254 +
   9.255  end;
    10.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Wed Oct 28 12:21:38 2009 +0000
    10.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Wed Oct 28 18:09:30 2009 +0100
    10.3 @@ -716,8 +716,8 @@
    10.4  (* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
    10.5     -> dtype_spec -> nfa_entry option *)
    10.6  fun nfa_entry_for_datatype _ _ _ _ ({co = true, ...} : dtype_spec) = NONE
    10.7 -  | nfa_entry_for_datatype ext_ctxt kk rel_table dtypes
    10.8 -                           ({typ, constrs, ...} : dtype_spec) =
    10.9 +  | nfa_entry_for_datatype _ _ _ _ {shallow = true, ...} = NONE
   10.10 +  | nfa_entry_for_datatype ext_ctxt kk rel_table dtypes {typ, constrs, ...} =
   10.11      SOME (typ, maps (nfa_transitions_for_constr ext_ctxt kk rel_table dtypes
   10.12                       o #const) constrs)
   10.13  
   10.14 @@ -884,12 +884,13 @@
   10.15  
   10.16  (* extended_context -> int Typtab.table -> kodkod_constrs -> nut NameTable.table
   10.17     -> dtype_spec -> Kodkod.formula list *)
   10.18 -fun other_axioms_for_datatype ext_ctxt ofs kk rel_table (dtype as {typ, ...}) =
   10.19 -  let val j0 = offset_of_type ofs typ in
   10.20 -    sel_axioms_for_datatype ext_ctxt j0 kk rel_table dtype @
   10.21 -    uniqueness_axioms_for_datatype ext_ctxt kk rel_table dtype @
   10.22 -    partition_axioms_for_datatype j0 kk rel_table dtype
   10.23 -  end
   10.24 +fun other_axioms_for_datatype _ _ _ _ {shallow = true, ...} = []
   10.25 +  | other_axioms_for_datatype ext_ctxt ofs kk rel_table (dtype as {typ, ...}) =
   10.26 +    let val j0 = offset_of_type ofs typ in
   10.27 +      sel_axioms_for_datatype ext_ctxt j0 kk rel_table dtype @
   10.28 +      uniqueness_axioms_for_datatype ext_ctxt kk rel_table dtype @
   10.29 +      partition_axioms_for_datatype j0 kk rel_table dtype
   10.30 +    end
   10.31  
   10.32  (* extended_context -> int Typtab.table -> kodkod_constrs -> nut NameTable.table
   10.33     -> dtype_spec list -> Kodkod.formula list *)
    11.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Oct 28 12:21:38 2009 +0000
    11.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Oct 28 18:09:30 2009 +0100
    11.3 @@ -329,7 +329,8 @@
    11.4            HOLogic.mk_number nat_T j
    11.5          else case datatype_spec datatypes T of
    11.6            NONE => atom for_auto T j
    11.7 -        | SOME {constrs, co, ...} =>
    11.8 +        | SOME {shallow = true, ...} => atom for_auto T j
    11.9 +        | SOME {co, constrs, ...} =>
   11.10            let
   11.11              (* styp -> int list *)
   11.12              fun tuples_for_const (s, T) =
   11.13 @@ -600,11 +601,12 @@
   11.14      (* typ -> dtype_spec list *)
   11.15      fun integer_datatype T =
   11.16        [{typ = T, card = card_of_type card_assigns T, co = false,
   11.17 -        precise = false, constrs = []}]
   11.18 +        precise = false, shallow = false, constrs = []}]
   11.19        handle TYPE ("Nitpick_HOL.card_of_type", _, _) => []
   11.20      val (codatatypes, datatypes) =
   11.21 -      List.partition #co datatypes
   11.22 -      ||> append (integer_datatype nat_T @ integer_datatype int_T)
   11.23 +      datatypes |> filter_out #shallow
   11.24 +                |> List.partition #co
   11.25 +                ||> append (integer_datatype nat_T @ integer_datatype int_T)
   11.26      val block_of_datatypes =
   11.27        if show_datatypes andalso not (null datatypes) then
   11.28          [Pretty.big_list ("Datatype" ^ plural_s_for_list datatypes ^ ":")
    12.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Wed Oct 28 12:21:38 2009 +0000
    12.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Wed Oct 28 18:09:30 2009 +0100
    12.3 @@ -749,8 +749,9 @@
    12.4             (~1 upto num_sels_for_constr_type T - 1)
    12.5  (* scope -> dtype_spec -> nut list * rep NameTable.table
    12.6     -> nut list * rep NameTable.table *)
    12.7 -fun choose_rep_for_sels_of_datatype scope ({constrs, ...} : dtype_spec) =
    12.8 -  fold_rev (choose_rep_for_sels_for_constr scope o #const) constrs
    12.9 +fun choose_rep_for_sels_of_datatype _ ({shallow = true, ...} : dtype_spec) = I
   12.10 +  | choose_rep_for_sels_of_datatype scope {constrs, ...} =
   12.11 +    fold_rev (choose_rep_for_sels_for_constr scope o #const) constrs
   12.12  (* scope -> rep NameTable.table -> nut list * rep NameTable.table *)
   12.13  fun choose_reps_for_all_sels (scope as {datatypes, ...}) =
   12.14    fold (choose_rep_for_sels_of_datatype scope) datatypes o pair []
    13.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Wed Oct 28 12:21:38 2009 +0000
    13.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Wed Oct 28 18:09:30 2009 +0100
    13.3 @@ -22,6 +22,7 @@
    13.4      card: int,
    13.5      co: bool,
    13.6      precise: bool,
    13.7 +    shallow: bool,
    13.8      constrs: constr_spec list}
    13.9  
   13.10    type scope = {
   13.11 @@ -44,7 +45,7 @@
   13.12    val all_scopes :
   13.13      extended_context -> int -> (typ option * int list) list
   13.14      -> (styp option * int list) list -> (styp option * int list) list
   13.15 -    -> int list -> typ list -> typ list -> scope list
   13.16 +    -> int list -> typ list -> typ list -> typ list -> scope list
   13.17  end;
   13.18  
   13.19  structure Nitpick_Scope : NITPICK_SCOPE =
   13.20 @@ -66,6 +67,7 @@
   13.21    card: int,
   13.22    co: bool,
   13.23    precise: bool,
   13.24 +  shallow: bool,
   13.25    constrs: constr_spec list}
   13.26  
   13.27  type scope = {
   13.28 @@ -126,7 +128,7 @@
   13.29        card_assigns |> filter_out (equal @{typ bisim_iterator} o fst)
   13.30                     |> List.partition (is_fp_iterator_type o fst)
   13.31      val (unimportant_card_asgns, important_card_asgns) =
   13.32 -      card_asgns |> List.partition ((is_datatype thy orf is_integer_type) o fst)
   13.33 +      card_asgns |> List.partition ((is_integer_type orf is_datatype thy) o fst)
   13.34      val cards =
   13.35        map (fn (T, k) => quote (string_for_type ctxt T) ^ " = " ^
   13.36                          string_of_int k)
   13.37 @@ -431,10 +433,11 @@
   13.38       explicit_max = max, total = total} :: constrs
   13.39    end
   13.40  
   13.41 -(* extended_context -> scope_desc -> typ * int -> dtype_spec *)
   13.42 -fun datatype_spec_from_scope_descriptor (ext_ctxt as {thy, ...})
   13.43 +(* extended_context -> typ list -> scope_desc -> typ * int -> dtype_spec *)
   13.44 +fun datatype_spec_from_scope_descriptor (ext_ctxt as {thy, ...}) shallow_dataTs
   13.45                                          (desc as (card_asgns, _)) (T, card) =
   13.46    let
   13.47 +    val shallow = T mem shallow_dataTs
   13.48      val co = is_codatatype thy T
   13.49      val xs = boxed_datatype_constrs ext_ctxt T
   13.50      val self_recs = map (is_self_recursive_constr_type o snd) xs
   13.51 @@ -448,14 +451,18 @@
   13.52      val constrs =
   13.53        fold_rev (add_constr_spec desc co card sum_dom_cards num_self_recs
   13.54                                  num_non_self_recs) (self_recs ~~ xs) []
   13.55 -  in {typ = T, card = card, co = co, precise = precise, constrs = constrs} end
   13.56 +  in
   13.57 +    {typ = T, card = card, co = co, precise = precise, shallow = shallow,
   13.58 +     constrs = constrs}
   13.59 +  end
   13.60  
   13.61 -(* extended_context -> int -> scope_desc -> scope *)
   13.62 -fun scope_from_descriptor (ext_ctxt as {thy, ...}) sym_break
   13.63 +(* extended_context -> int -> typ list -> scope_desc -> scope *)
   13.64 +fun scope_from_descriptor (ext_ctxt as {thy, ...}) sym_break shallow_dataTs
   13.65                            (desc as (card_asgns, _)) =
   13.66    let
   13.67 -    val datatypes = map (datatype_spec_from_scope_descriptor ext_ctxt desc)
   13.68 -                        (filter (is_datatype thy o fst) card_asgns)
   13.69 +    val datatypes =
   13.70 +      map (datatype_spec_from_scope_descriptor ext_ctxt shallow_dataTs desc)
   13.71 +          (filter (is_datatype thy o fst) card_asgns)
   13.72      val bisim_depth = card_of_type card_asgns @{typ bisim_iterator} - 1
   13.73    in
   13.74      {ext_ctxt = ext_ctxt, card_assigns = card_asgns, datatypes = datatypes,
   13.75 @@ -480,9 +487,9 @@
   13.76  
   13.77  (* extended_context -> int -> (typ option * int list) list
   13.78     -> (styp option * int list) list -> (styp option * int list) list -> int list
   13.79 -   -> typ list -> typ list -> scope list *)
   13.80 +   -> typ list -> typ list -> typ list -> scope list *)
   13.81  fun all_scopes (ext_ctxt as {thy, ctxt, ...}) sym_break cards_asgns maxes_asgns
   13.82 -               iters_asgns bisim_depths mono_Ts nonmono_Ts =
   13.83 +               iters_asgns bisim_depths mono_Ts nonmono_Ts shallow_dataTs =
   13.84    let
   13.85      val cards_asgns = fix_cards_assigns_wrt_boxing thy mono_Ts cards_asgns
   13.86      val blocks = blocks_for_types ctxt cards_asgns maxes_asgns iters_asgns
   13.87 @@ -492,7 +499,7 @@
   13.88                  |> map_filter (scope_descriptor_from_combination thy blocks)
   13.89    in
   13.90      descs |> length descs <= distinct_threshold ? distinct (op =)
   13.91 -          |> map (scope_from_descriptor ext_ctxt sym_break)
   13.92 +          |> map (scope_from_descriptor ext_ctxt sym_break shallow_dataTs)
   13.93    end
   13.94  
   13.95  end;
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/src/Tools/Auto_Counterexample.thy	Wed Oct 28 18:09:30 2009 +0100
    14.3 @@ -0,0 +1,15 @@
    14.4 +(*  Title:   Tools/Auto_Counterexample.thy
    14.5 +    Author:  Jasmin Blanchette, TU Muenchen
    14.6 +
    14.7 +Counterexample Search Unit (do not abbreviate!).
    14.8 +*)
    14.9 +
   14.10 +header {* Counterexample Search Unit *}
   14.11 +
   14.12 +theory Auto_Counterexample
   14.13 +imports Pure
   14.14 +uses
   14.15 +  "~~/src/Tools/auto_counterexample.ML"
   14.16 +begin
   14.17 +
   14.18 +end
    15.1 --- a/src/Tools/Code_Generator.thy	Wed Oct 28 12:21:38 2009 +0000
    15.2 +++ b/src/Tools/Code_Generator.thy	Wed Oct 28 18:09:30 2009 +0100
    15.3 @@ -5,7 +5,7 @@
    15.4  header {* Loading the code generator modules *}
    15.5  
    15.6  theory Code_Generator
    15.7 -imports Pure
    15.8 +imports Auto_Counterexample
    15.9  uses
   15.10    "~~/src/Tools/value.ML"
   15.11    "~~/src/Tools/quickcheck.ML"
   15.12 @@ -25,4 +25,4 @@
   15.13    #> Nbe.setup
   15.14  *}
   15.15  
   15.16 -end
   15.17 \ No newline at end of file
   15.18 +end
    16.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.2 +++ b/src/Tools/auto_counterexample.ML	Wed Oct 28 18:09:30 2009 +0100
    16.3 @@ -0,0 +1,59 @@
    16.4 +(*  Title:      Tools/auto_counterexample.ML
    16.5 +    Author:     Jasmin Blanchette, TU Muenchen
    16.6 +
    16.7 +Counterexample Search Unit (do not abbreviate!).
    16.8 +*)
    16.9 +
   16.10 +signature AUTO_COUNTEREXAMPLE =
   16.11 +sig
   16.12 +  val time_limit: int Unsynchronized.ref
   16.13 +
   16.14 +  val register_tool :
   16.15 +    string * (Proof.state -> bool * Proof.state) -> theory -> theory
   16.16 +end;
   16.17 +
   16.18 +structure Auto_Counterexample : AUTO_COUNTEREXAMPLE =
   16.19 +struct
   16.20 +
   16.21 +(* preferences *)
   16.22 +
   16.23 +val time_limit = Unsynchronized.ref 2500
   16.24 +
   16.25 +val _ =
   16.26 +  ProofGeneralPgip.add_preference Preferences.category_tracing
   16.27 +    (Preferences.nat_pref time_limit
   16.28 +      "auto-counterexample-time-limit"
   16.29 +      "Time limit for automatic counterexample search (in milliseconds).")
   16.30 +
   16.31 +
   16.32 +(* configuration *)
   16.33 +
   16.34 +structure Data = TheoryDataFun(
   16.35 +  type T = (string * (Proof.state -> bool * Proof.state)) list
   16.36 +  val empty = []
   16.37 +  val copy = I
   16.38 +  val extend = I
   16.39 +  fun merge _ (tools1, tools2) = AList.merge (op =) (K true) (tools1, tools2)
   16.40 +)
   16.41 +
   16.42 +val register_tool = Data.map o AList.update (op =)
   16.43 +
   16.44 +
   16.45 +(* automatic testing *)
   16.46 +
   16.47 +val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state =>
   16.48 +  case !time_limit of
   16.49 +    0 => state
   16.50 +  | ms =>
   16.51 +    TimeLimit.timeLimit (Time.fromMilliseconds ms)
   16.52 +        (fn () =>
   16.53 +            if interact andalso not (!Toplevel.quiet) then
   16.54 +              fold_rev (fn (_, tool) => fn (true, state) => (true, state)
   16.55 +                                         | (false, state) => tool state)
   16.56 +                   (Data.get (Proof.theory_of state)) (false, state) |> snd
   16.57 +            else
   16.58 +              state) ()
   16.59 +    handle TimeLimit.TimeOut =>
   16.60 +           (warning "Automatic counterexample search timed out."; state)))
   16.61 +
   16.62 +end;
    17.1 --- a/src/Tools/quickcheck.ML	Wed Oct 28 12:21:38 2009 +0000
    17.2 +++ b/src/Tools/quickcheck.ML	Wed Oct 28 18:09:30 2009 +0100
    17.3 @@ -7,10 +7,10 @@
    17.4  signature QUICKCHECK =
    17.5  sig
    17.6    val auto: bool Unsynchronized.ref
    17.7 -  val auto_time_limit: int Unsynchronized.ref
    17.8    val test_term: Proof.context -> bool -> string option -> int -> int -> term ->
    17.9      (string * term) list option
   17.10    val add_generator: string * (Proof.context -> term -> int -> term list option) -> theory -> theory
   17.11 +  val setup: theory -> theory
   17.12    val quickcheck: (string * string) list -> int -> Proof.state -> (string * term) list option
   17.13  end;
   17.14  
   17.15 @@ -20,20 +20,13 @@
   17.16  (* preferences *)
   17.17  
   17.18  val auto = Unsynchronized.ref false;
   17.19 -val auto_time_limit = Unsynchronized.ref 2500;
   17.20  
   17.21  val _ =
   17.22    ProofGeneralPgip.add_preference Preferences.category_tracing
   17.23    (setmp_CRITICAL auto true (fn () =>
   17.24      Preferences.bool_pref auto
   17.25        "auto-quickcheck"
   17.26 -      "Whether to enable quickcheck automatically.") ());
   17.27 -
   17.28 -val _ =
   17.29 -  ProofGeneralPgip.add_preference Preferences.category_tracing
   17.30 -    (Preferences.nat_pref auto_time_limit
   17.31 -      "auto-quickcheck-time-limit"
   17.32 -      "Time limit for automatic quickcheck (in milliseconds).");
   17.33 +      "Whether to run Quickcheck automatically.") ());
   17.34  
   17.35  
   17.36  (* quickcheck configuration -- default parameters, test generators *)
   17.37 @@ -143,7 +136,7 @@
   17.38      val thy = Proof.theory_of state;
   17.39      fun strip (Const ("all", _) $ Abs (_, _, t)) = strip t
   17.40        | strip t = t;
   17.41 -    val (_, st) = Proof.flat_goal state;
   17.42 +    val (_, (_, st)) = Proof.get_goal state;
   17.43      val (gi, frees) = Logic.goal_params (prop_of st) i;
   17.44      val gi' = Logic.list_implies (assms, subst_bounds (frees, strip gi))
   17.45        |> monomorphic_term thy insts default_T
   17.46 @@ -159,28 +152,26 @@
   17.47  
   17.48  (* automatic testing *)
   17.49  
   17.50 -val _ = Context.>> (Specification.add_theorem_hook (fn int => fn state =>
   17.51 -  let
   17.52 -    val ctxt = Proof.context_of state;
   17.53 -    val assms = map term_of (Assumption.all_assms_of ctxt);
   17.54 -    val Test_Params { size, iterations, default_type } =
   17.55 -      (snd o Data.get o Proof.theory_of) state;
   17.56 -    fun test () =
   17.57 -      let
   17.58 -        val res = TimeLimit.timeLimit (Time.fromMilliseconds (!auto_time_limit))
   17.59 -          (try (test_goal true NONE size iterations default_type [] 1 assms)) state;
   17.60 -      in
   17.61 -        case res of
   17.62 -          NONE => state
   17.63 -        | SOME NONE => state
   17.64 -        | SOME cex => Proof.goal_message (fn () => Pretty.chunks [Pretty.str "",
   17.65 -            Pretty.mark Markup.hilite (pretty_counterex ctxt cex)]) state
   17.66 -      end handle TimeLimit.TimeOut => (warning "Auto quickcheck: timeout."; state);
   17.67 -  in
   17.68 -    if int andalso !auto andalso not (!Toplevel.quiet)
   17.69 -    then test ()
   17.70 -    else state
   17.71 -  end));
   17.72 +fun auto_quickcheck state =
   17.73 +  if not (!auto) then
   17.74 +    (false, state)
   17.75 +  else
   17.76 +    let
   17.77 +      val ctxt = Proof.context_of state;
   17.78 +      val assms = map term_of (Assumption.all_assms_of ctxt);
   17.79 +      val Test_Params { size, iterations, default_type } =
   17.80 +        (snd o Data.get o Proof.theory_of) state;
   17.81 +      val res =
   17.82 +        try (test_goal true NONE size iterations default_type [] 1 assms) state;
   17.83 +    in
   17.84 +      case res of
   17.85 +        NONE => (false, state)
   17.86 +      | SOME NONE => (false, state)
   17.87 +      | SOME cex => (true, Proof.goal_message (K (Pretty.chunks [Pretty.str "",
   17.88 +          Pretty.mark Markup.hilite (pretty_counterex ctxt cex)])) state)
   17.89 +    end
   17.90 +
   17.91 +val setup = Auto_Counterexample.register_tool ("quickcheck", auto_quickcheck)
   17.92  
   17.93  
   17.94  (* Isar commands *)
   17.95 @@ -251,4 +242,3 @@
   17.96  
   17.97  
   17.98  val auto_quickcheck = Quickcheck.auto;
   17.99 -val auto_quickcheck_time_limit = Quickcheck.auto_time_limit;