change defaults of Auto Nitpick so that it consumes less resources (time and Kodkod threads)

--- a/src/HOL/Tools/Nitpick/nitpick.ML	Sat Sep 11 10:13:51 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Sat Sep 11 10:20:25 2010 +0200
@@ -144,7 +144,7 @@
    rel_table: nut NameTable.table,
    unsound: bool,
    scope: scope}
- 
+
 type rich_problem = KK.problem * problem_extension
 
 fun pretties_for_formulas _ _ [] = []

--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Sat Sep 11 10:13:51 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Sat Sep 11 10:20:25 2010 +0200
@@ -10,7 +10,7 @@
 sig
   type params = Nitpick.params
 
-  val auto: bool Unsynchronized.ref
+  val auto : bool Unsynchronized.ref
   val default_params : theory -> (string * string) list -> params
   val setup : theory -> theory
 end;
@@ -24,7 +24,7 @@
 open Nitpick_Nut
 open Nitpick
 
-val auto = Unsynchronized.ref false;
+val auto = Unsynchronized.ref false
 
 val _ =
   ProofGeneralPgip.add_preference Preferences.category_tracing
@@ -109,7 +109,7 @@
 
 fun check_raw_param (s, _) =
   if is_known_raw_param s then ()
-  else error ("Unknown parameter: " ^ quote s ^ ".")  
+  else error ("Unknown parameter: " ^ quote s ^ ".")
 
 fun unnegate_param_name name =
   case AList.lookup (op =) negated_params name of
@@ -212,8 +212,8 @@
       lookup_assigns read prefix "" (space_explode " ")
     fun lookup_time name =
       case lookup name of
-        NONE => NONE
-      | SOME s => parse_time_option name s
+        SOME s => parse_time_option name s
+      | NONE => NONE
     val read_type_polymorphic =
       Syntax.read_typ ctxt #> Logic.mk_type
       #> singleton (Variable.polymorphic ctxt) #> Logic.dest_type
@@ -229,11 +229,12 @@
     val bisim_depths = lookup_int_seq "bisim_depth" ~1
     val boxes = lookup_bool_option_assigns read_type_polymorphic "box"
     val finitizes = lookup_bool_option_assigns read_type_polymorphic "finitize"
-    val monos = lookup_bool_option_assigns read_type_polymorphic "mono"
+    val monos = if auto then [(NONE, SOME true)]
+                else lookup_bool_option_assigns read_type_polymorphic "mono"
     val stds = lookup_bool_assigns read_type_polymorphic "std"
     val wfs = lookup_bool_option_assigns read_const_polymorphic "wf"
     val sat_solver = lookup_string "sat_solver"
-    val blocking = not auto andalso lookup_bool "blocking"
+    val blocking = auto orelse lookup_bool "blocking"
     val falsify = lookup_bool "falsify"
     val debug = not auto andalso lookup_bool "debug"
     val verbose = debug orelse (not auto andalso lookup_bool "verbose")
@@ -252,7 +253,7 @@
     val kodkod_sym_break = lookup_int "kodkod_sym_break"
     val timeout = if auto then NONE else lookup_time "timeout"
     val tac_timeout = lookup_time "tac_timeout"
-    val max_threads = Int.max (0, lookup_int "max_threads")
+    val max_threads = if auto then 1 else Int.max (0, lookup_int "max_threads")
     val show_datatypes = debug orelse lookup_bool "show_datatypes"
     val show_consts = debug orelse lookup_bool "show_consts"
     val formats = lookup_ints_assigns read_term_polymorphic "format" 0
@@ -346,10 +347,7 @@
           else handle_exceptions ctxt)
          (fn (_, state) => pick_nits_in_subgoal state params auto i step
                            |>> curry (op =) "genuine")
-  in
-    if auto orelse blocking then go ()
-    else (Toplevel.thread true (tap go); (false, state))  (* FIXME no threads in user-space *)
-  end
+  in if blocking then go () else Future.fork (tap go) |> K (false, state) end
 
 fun nitpick_trans (params, i) =
   Toplevel.keep (fn st =>
@@ -362,7 +360,7 @@
 fun nitpick_params_trans params =
   Toplevel.theory
       (fold set_default_raw_param params
-       #> tap (fn thy => 
+       #> tap (fn thy =>
                   writeln ("Default parameters for Nitpick:\n" ^
                            (case rev (default_raw_params thy) of
                               [] => "none"

--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Sat Sep 11 10:13:51 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Sat Sep 11 10:20:25 2010 +0200
@@ -280,7 +280,7 @@
     (map (bound_for_built_in_rel debug ofs univ_card nat_card int_card main_j0)
          rels,
      map_filter axiom_for_built_in_rel rels)
-  end 
+  end
 
 fun bound_comment ctxt debug nick T R =
   short_name nick ^

--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Sat Sep 11 10:13:51 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Sat Sep 11 10:20:25 2010 +0200
@@ -660,7 +660,7 @@
                 |>> curry3 MFun bool_M (S Minus)
               | @{const_name Pair} => do_pair_constr T accum
               | @{const_name fst} => do_nth_pair_sel 0 T accum
-              | @{const_name snd} => do_nth_pair_sel 1 T accum 
+              | @{const_name snd} => do_nth_pair_sel 1 T accum
               | @{const_name Id} =>
                 (MFun (mtype_for (domain_type T), S Minus, bool_M), accum)
               | @{const_name converse} =>
@@ -894,7 +894,7 @@
                in
                  (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2),
                   accum)
-               end 
+               end
              else
                do_term t accum
            | _ => do_term t accum)
@@ -1105,7 +1105,7 @@
               val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2)
               val (t1', T2') =
                 case T1 of
-                  Type (s, [T11, T12]) => 
+                  Type (s, [T11, T12]) =>
                   (if s = @{type_name fin_fun} then
                      select_nth_constr_arg ctxt stds (fin_fun_constr T11 T12) t1
                                            0 (T11 --> T12)