added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested

--- a/doc-src/Nitpick/nitpick.tex	Wed Feb 17 11:20:09 2010 +0100
+++ b/doc-src/Nitpick/nitpick.tex	Wed Feb 17 12:14:08 2010 +0100
@@ -472,7 +472,9 @@
 \prew
 \textbf{lemma} ``$\forall n.\; \textit{Suc}~n \mathbin{\not=} n \,\Longrightarrow\, P$'' \\
 \textbf{nitpick} [\textit{card~nat}~= 100, \textit{check\_potential}] \\[2\smallskipamount]
-\slshape Nitpick found a potential counterexample: \\[2\smallskipamount]
+\slshape Warning: The conjecture either trivially holds or (more likely) lies outside Nitpick's supported
+fragment. Only potential counterexamples may be found. \\[2\smallskipamount]
+Nitpick found a potential counterexample: \\[2\smallskipamount]
 \hbox{}\qquad Free variable: \nopagebreak \\
 \hbox{}\qquad\qquad $P = \textit{False}$ \\[2\smallskipamount]
 Confirmation by ``\textit{auto}'': The above counterexample is genuine.

--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Wed Feb 17 11:20:09 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Wed Feb 17 12:14:08 2010 +0100
@@ -266,7 +266,7 @@
 next
   case (Branch t u) thus ?case
   nitpick
-  nitpick [non_std "'a bin_tree", show_consts]
+  nitpick [non_std, show_all]
 oops
 
 lemma "labels (swap t a b) =

--- a/src/HOL/Tools/Nitpick/kodkod.ML	Wed Feb 17 11:20:09 2010 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.ML	Wed Feb 17 12:14:08 2010 +0100
@@ -167,6 +167,7 @@
 
   val max_arity : int -> int
   val arity_of_rel_expr : rel_expr -> int
+  val is_problem_trivially_false : problem -> bool
   val problems_equivalent : problem -> problem -> bool
   val solve_any_problem :
     bool -> Time.time option -> int -> int -> problem list -> outcome
@@ -491,6 +492,10 @@
   | arity_of_decl (DeclSome ((n, _), _)) = n
   | arity_of_decl (DeclSet ((n, _), _)) = n
 
+(* problem -> bool *)
+fun is_problem_trivially_false ({formula = False, ...} : problem) = true
+  | is_problem_trivially_false _ = false
+
 (* string -> bool *)
 val is_relevant_setting = not o member (op =) ["solver", "delay"]
 
@@ -1014,7 +1019,7 @@
     val indexed_problems = if j >= 0 then
                              [(j, nth problems j)]
                            else
-                             filter (not_equal False o #formula o snd)
+                             filter (is_problem_trivially_false o snd)
                                     (0 upto length problems - 1 ~~ problems)
     val triv_js = filter_out (AList.defined (op =) indexed_problems)
                              (0 upto length problems - 1)

--- a/src/HOL/Tools/Nitpick/minipick.ML	Wed Feb 17 11:20:09 2010 +0100
+++ b/src/HOL/Tools/Nitpick/minipick.ML	Wed Feb 17 12:14:08 2010 +0100
@@ -84,7 +84,7 @@
 fun atom_from_formula f = RelIf (f, true_atom, false_atom)
 
 (* Proof.context -> (typ -> int) -> styp list -> term -> formula *)
-fun kodkod_formula_for_term ctxt card frees =
+fun kodkod_formula_from_term ctxt card frees =
   let
     (* typ -> rel_expr -> rel_expr *)
     fun R_rep_from_S_rep (T as Type ("fun", [T1, @{typ bool}])) r =
@@ -145,7 +145,7 @@
        | Term.Var _ => raise SAME ()
        | Bound _ => raise SAME ()
        | Const (s, _) => raise NOT_SUPPORTED ("constant " ^ quote s)
-       | _ => raise TERM ("Minipick.kodkod_formula_for_term.to_F", [t]))
+       | _ => raise TERM ("Minipick.kodkod_formula_from_term.to_F", [t]))
       handle SAME () => formula_from_atom (to_R_rep Ts t)
     (* typ list -> term -> rel_expr *)
     and to_S_rep Ts t =
@@ -306,7 +306,7 @@
     val bounds = map2 (bound_for_free card) (index_seq 0 (length frees)) frees
     val declarative_axioms =
       map2 (declarative_axiom_for_free card) (index_seq 0 (length frees)) frees
-    val formula = kodkod_formula_for_term ctxt card frees neg_t
+    val formula = kodkod_formula_from_term ctxt card frees neg_t
                   |> fold_rev (curry And) declarative_axioms
     val univ_card = univ_card 0 0 0 bounds formula
     val problem =

--- a/src/HOL/Tools/Nitpick/nitpick.ML	Wed Feb 17 11:20:09 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Wed Feb 17 12:14:08 2010 +0100
@@ -130,7 +130,7 @@
   sel_names: nut list,
   nonsel_names: nut list,
   rel_table: nut NameTable.table,
-  liberal: bool,
+  unsound: bool,
   scope: scope,
   core: KK.formula,
   defs: KK.formula list}
@@ -157,15 +157,15 @@
       (Path.variable "ISABELLE_HOME_USER" ::
        map Path.basic ["etc", "components"]))) ^ "\"."
 
-val max_liberal_delay_ms = 200
-val max_liberal_delay_percent = 2
+val max_unsound_delay_ms = 200
+val max_unsound_delay_percent = 2
 
 (* Time.time option -> int *)
-fun liberal_delay_for_timeout NONE = max_liberal_delay_ms
-  | liberal_delay_for_timeout (SOME timeout) =
-    Int.max (0, Int.min (max_liberal_delay_ms,
+fun unsound_delay_for_timeout NONE = max_unsound_delay_ms
+  | unsound_delay_for_timeout (SOME timeout) =
+    Int.max (0, Int.min (max_unsound_delay_ms,
                          Time.toMilliseconds timeout
-                         * max_liberal_delay_percent div 100))
+                         * max_unsound_delay_percent div 100))
 
 (* Time.time option -> bool *)
 fun passed_deadline NONE = false
@@ -434,7 +434,7 @@
     val too_big_scopes = Unsynchronized.ref []
 
     (* bool -> scope -> rich_problem option *)
-    fun problem_for_scope liberal
+    fun problem_for_scope unsound
             (scope as {card_assigns, bits, bisim_depth, datatypes, ofs, ...}) =
       let
         val _ = not (exists (fn other => scope_less_eq other scope)
@@ -469,10 +469,10 @@
                          (univ_card nat_card int_card main_j0 [] KK.True)
         val _ = check_arity min_univ_card min_highest_arity
 
-        val core_u = choose_reps_in_nut scope liberal rep_table false core_u
-        val def_us = map (choose_reps_in_nut scope liberal rep_table true)
+        val core_u = choose_reps_in_nut scope unsound rep_table false core_u
+        val def_us = map (choose_reps_in_nut scope unsound rep_table true)
                          def_us
-        val nondef_us = map (choose_reps_in_nut scope liberal rep_table false)
+        val nondef_us = map (choose_reps_in_nut scope unsound rep_table false)
                             nondef_us
 (*
         val _ = List.app (priority o string_for_nut ctxt)
@@ -488,21 +488,19 @@
         val core_u = rename_vars_in_nut pool rel_table core_u
         val def_us = map (rename_vars_in_nut pool rel_table) def_us
         val nondef_us = map (rename_vars_in_nut pool rel_table) nondef_us
-        (* nut -> KK.formula *)
-        val to_f = kodkod_formula_from_nut bits ofs liberal kk
-        val core_f = to_f core_u
-        val def_fs = map to_f def_us
-        val nondef_fs = map to_f nondef_us
+        val core_f = kodkod_formula_from_nut bits ofs kk core_u
+        val def_fs = map (kodkod_formula_from_nut bits ofs kk) def_us
+        val nondef_fs = map (kodkod_formula_from_nut bits ofs kk) nondef_us
         val formula = fold (fold s_and) [def_fs, nondef_fs] core_f
-        val comment = (if liberal then "liberal" else "conservative") ^ "\n" ^
+        val comment = (if unsound then "unsound" else "sound") ^ "\n" ^
                       PrintMode.setmp [] multiline_string_for_scope scope
         val kodkod_sat_solver =
           Kodkod_SAT.sat_solver_spec effective_sat_solver |> snd
         val bit_width = if bits = 0 then 16 else bits + 1
-        val delay = if liberal then
+        val delay = if unsound then
                       Option.map (fn time => Time.- (time, Time.now ()))
                                  deadline
-                      |> liberal_delay_for_timeout
+                      |> unsound_delay_for_timeout
                     else
                       0
         val settings = [("solver", commas (map quote kodkod_sat_solver)),
@@ -540,13 +538,13 @@
                expr_assigns = [], formula = formula},
               {free_names = free_names, sel_names = sel_names,
                nonsel_names = nonsel_names, rel_table = rel_table,
-               liberal = liberal, scope = scope, core = core_f,
+               unsound = unsound, scope = scope, core = core_f,
                defs = nondef_fs @ def_fs @ declarative_axioms})
       end
       handle TOO_LARGE (loc, msg) =>
              if loc = "Nitpick_Kodkod.check_arity" andalso
                 not (Typtab.is_empty ofs) then
-               problem_for_scope liberal
+               problem_for_scope unsound
                    {hol_ctxt = hol_ctxt, card_assigns = card_assigns,
                     bits = bits, bisim_depth = bisim_depth,
                     datatypes = datatypes, ofs = Typtab.empty}
@@ -556,13 +554,13 @@
              else
                (Unsynchronized.change too_big_scopes (cons scope);
                 print_v (fn () => ("Limit reached: " ^ msg ^
-                                   ". Skipping " ^ (if liberal then "potential"
+                                   ". Skipping " ^ (if unsound then "potential"
                                                     else "genuine") ^
                                    " component of scope."));
                 NONE)
            | TOO_SMALL (loc, msg) =>
              (print_v (fn () => ("Limit reached: " ^ msg ^
-                                 ". Skipping " ^ (if liberal then "potential"
+                                 ". Skipping " ^ (if unsound then "potential"
                                                   else "genuine") ^
                                  " component of scope."));
               NONE)
@@ -577,7 +575,7 @@
 
     val scopes = Unsynchronized.ref []
     val generated_scopes = Unsynchronized.ref []
-    val generated_problems = Unsynchronized.ref []
+    val generated_problems = Unsynchronized.ref ([] : rich_problem list)
     val checked_problems = Unsynchronized.ref (SOME [])
     val met_potential = Unsynchronized.ref 0
 
@@ -711,7 +709,7 @@
           | KK.Normal (sat_ps, unsat_js) =>
             let
               val (lib_ps, con_ps) =
-                List.partition (#liberal o snd o nth problems o fst) sat_ps
+                List.partition (#unsound o snd o nth problems o fst) sat_ps
             in
               update_checked_problems problems (unsat_js @ map fst lib_ps);
               if null con_ps then
@@ -728,9 +726,9 @@
                     (0, 0, donno)
                   else
                     let
-                      (* "co_js" is the list of conservative problems whose
-                         liberal pendants couldn't be satisfied and hence that
-                         most probably can't be satisfied themselves. *)
+                      (* "co_js" is the list of sound problems whose unsound
+                         pendants couldn't be satisfied and hence that most
+                         probably can't be satisfied themselves. *)
                       val co_js =
                         map (fn j => j - 1) unsat_js
                         |> filter (fn j =>
@@ -743,7 +741,7 @@
                       val problems =
                         problems |> filter_out_indices bye_js
                                  |> max_potential <= 0
-                                    ? filter_out (#liberal o snd)
+                                    ? filter_out (#unsound o snd)
                     in
                       solve_any_problem max_potential max_genuine donno false
                                         problems
@@ -763,7 +761,7 @@
                                                  (map fst sat_ps @ unsat_js)
                       val problems =
                         problems |> filter_out_indices bye_js
-                                 |> filter_out (#liberal o snd)
+                                 |> filter_out (#unsound o snd)
                     in solve_any_problem 0 max_genuine donno false problems end
                 end
             end
@@ -807,10 +805,10 @@
             ()
         (* scope * bool -> rich_problem list * bool
            -> rich_problem list * bool *)
-        fun add_problem_for_scope (scope as {datatypes, ...}, liberal)
+        fun add_problem_for_scope (scope as {datatypes, ...}, unsound)
                                   (problems, donno) =
           (check_deadline ();
-           case problem_for_scope liberal scope of
+           case problem_for_scope unsound scope of
              SOME problem =>
              (problems
               |> (null problems orelse
@@ -826,6 +824,28 @@
                ([], donno)
         val _ = Unsynchronized.change generated_problems (append problems)
         val _ = Unsynchronized.change generated_scopes (append scopes)
+        val _ =
+          if j + 1 = n then
+            let
+              val (unsound_problems, sound_problems) =
+                List.partition (#unsound o snd) (!generated_problems)
+            in
+              if not (null sound_problems) andalso
+                 forall (KK.is_problem_trivially_false o fst)
+                        sound_problems then
+                print_m (fn () =>
+                    "Warning: The conjecture either trivially holds or (more \
+                    \likely) lies outside Nitpick's supported fragment." ^
+                    (if exists (not o KK.is_problem_trivially_false o fst)
+                               unsound_problems then
+                       " Only potential counterexamples may be found."
+                     else
+                       ""))
+              else
+                ()
+            end
+          else
+            ()
       in
         solve_any_problem max_potential max_genuine donno true (rev problems)
       end
@@ -838,7 +858,7 @@
       let
         (* rich_problem list -> rich_problem list *)
         val do_filter =
-          if !met_potential = max_potential then filter_out (#liberal o snd)
+          if !met_potential = max_potential then filter_out (#unsound o snd)
           else I
         val total = length (!scopes)
         val unsat =

--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Wed Feb 17 11:20:09 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Wed Feb 17 12:14:08 2010 +0100
@@ -36,7 +36,7 @@
     hol_context -> int -> int Typtab.table -> kodkod_constrs
     -> nut NameTable.table -> dtype_spec list -> Kodkod.formula list
   val kodkod_formula_from_nut :
-    int -> int Typtab.table -> bool -> kodkod_constrs -> nut -> Kodkod.formula
+    int -> int Typtab.table -> kodkod_constrs -> nut -> Kodkod.formula
 end;
 
 structure Nitpick_Kodkod : NITPICK_KODKOD =
@@ -954,8 +954,8 @@
   acyclicity_axioms_for_datatypes hol_ctxt kk rel_table dtypes @
   maps (other_axioms_for_datatype hol_ctxt bits ofs kk rel_table) dtypes
 
-(* int -> int Typtab.table -> bool -> kodkod_constrs -> nut -> KK.formula *)
-fun kodkod_formula_from_nut bits ofs liberal
+(* int -> int Typtab.table -> kodkod_constrs -> nut -> KK.formula *)
+fun kodkod_formula_from_nut bits ofs
         (kk as {kk_all, kk_exist, kk_formula_let, kk_formula_if, kk_or, kk_not,
                 kk_iff, kk_implies, kk_and, kk_subset, kk_rel_eq, kk_no,
                 kk_lone, kk_one, kk_some, kk_rel_let, kk_rel_if, kk_union,

--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Wed Feb 17 11:20:09 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Wed Feb 17 12:14:08 2010 +0100
@@ -892,7 +892,7 @@
 (* scope -> bool -> rep NameTable.table -> bool -> nut -> nut *)
 fun choose_reps_in_nut (scope as {hol_ctxt as {thy, ctxt, ...}, card_assigns,
                                   bits, datatypes, ofs, ...})
-                       liberal table def =
+                       unsound table def =
   let
     val bool_atom_R = Atom (2, offset_of_type ofs bool_T)
     (* polarity -> bool -> rep *)
@@ -1036,7 +1036,7 @@
               if is_constructive u then s_op2 Eq T (Formula Neut) u1' u2'
               else opt_opt_case ()
           in
-            if liberal orelse polar = Neg orelse
+            if unsound orelse polar = Neg orelse
                is_concrete_type datatypes (type_of u1) then
               case (is_opt_rep (rep_of u1'), is_opt_rep (rep_of u2')) of
                 (true, true) => opt_opt_case ()
@@ -1138,7 +1138,7 @@
               else
                 let val quant_u = s_op2 oper T (Formula polar) u1' u2' in
                   if def orelse
-                     (liberal andalso (polar = Pos) = (oper = All)) orelse
+                     (unsound andalso (polar = Pos) = (oper = All)) orelse
                      is_complete_type datatypes (type_of u1) then
                     quant_u
                   else

--- a/src/HOL/Tools/Nitpick/nitpick_tests.ML	Wed Feb 17 11:20:09 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML	Wed Feb 17 12:14:08 2010 +0100
@@ -308,7 +308,7 @@
                        NameTable.empty
     val u = Op1 (Not, type_of u, rep_of u, u)
             |> rename_vars_in_nut pool table
-    val formula = kodkod_formula_from_nut bits Typtab.empty false constrs u
+    val formula = kodkod_formula_from_nut bits Typtab.empty constrs u
     val bounds = map (bound_for_plain_rel ctxt debug) free_rels
     val univ_card = univ_card nat_card int_card j0 bounds formula
     val declarative_axioms = map (declarative_axiom_for_plain_rel constrs)