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

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

     3.1 --- a/src/HOL/Tools/Nitpick/kodkod.ML	Wed Feb 17 11:20:09 2010 +0100
     3.2 +++ b/src/HOL/Tools/Nitpick/kodkod.ML	Wed Feb 17 12:14:08 2010 +0100
     3.3 @@ -167,6 +167,7 @@
     3.4  
     3.5    val max_arity : int -> int
     3.6    val arity_of_rel_expr : rel_expr -> int
     3.7 +  val is_problem_trivially_false : problem -> bool
     3.8    val problems_equivalent : problem -> problem -> bool
     3.9    val solve_any_problem :
    3.10      bool -> Time.time option -> int -> int -> problem list -> outcome
    3.11 @@ -491,6 +492,10 @@
    3.12    | arity_of_decl (DeclSome ((n, _), _)) = n
    3.13    | arity_of_decl (DeclSet ((n, _), _)) = n
    3.14  
    3.15 +(* problem -> bool *)
    3.16 +fun is_problem_trivially_false ({formula = False, ...} : problem) = true
    3.17 +  | is_problem_trivially_false _ = false
    3.18 +
    3.19  (* string -> bool *)
    3.20  val is_relevant_setting = not o member (op =) ["solver", "delay"]
    3.21  
    3.22 @@ -1014,7 +1019,7 @@
    3.23      val indexed_problems = if j >= 0 then
    3.24                               [(j, nth problems j)]
    3.25                             else
    3.26 -                             filter (not_equal False o #formula o snd)
    3.27 +                             filter (is_problem_trivially_false o snd)
    3.28                                      (0 upto length problems - 1 ~~ problems)
    3.29      val triv_js = filter_out (AList.defined (op =) indexed_problems)
    3.30                               (0 upto length problems - 1)

     4.1 --- a/src/HOL/Tools/Nitpick/minipick.ML	Wed Feb 17 11:20:09 2010 +0100
     4.2 +++ b/src/HOL/Tools/Nitpick/minipick.ML	Wed Feb 17 12:14:08 2010 +0100
     4.3 @@ -84,7 +84,7 @@
     4.4  fun atom_from_formula f = RelIf (f, true_atom, false_atom)
     4.5  
     4.6  (* Proof.context -> (typ -> int) -> styp list -> term -> formula *)
     4.7 -fun kodkod_formula_for_term ctxt card frees =
     4.8 +fun kodkod_formula_from_term ctxt card frees =
     4.9    let
    4.10      (* typ -> rel_expr -> rel_expr *)
    4.11      fun R_rep_from_S_rep (T as Type ("fun", [T1, @{typ bool}])) r =
    4.12 @@ -145,7 +145,7 @@
    4.13         | Term.Var _ => raise SAME ()
    4.14         | Bound _ => raise SAME ()
    4.15         | Const (s, _) => raise NOT_SUPPORTED ("constant " ^ quote s)
    4.16 -       | _ => raise TERM ("Minipick.kodkod_formula_for_term.to_F", [t]))
    4.17 +       | _ => raise TERM ("Minipick.kodkod_formula_from_term.to_F", [t]))
    4.18        handle SAME () => formula_from_atom (to_R_rep Ts t)
    4.19      (* typ list -> term -> rel_expr *)
    4.20      and to_S_rep Ts t =
    4.21 @@ -306,7 +306,7 @@
    4.22      val bounds = map2 (bound_for_free card) (index_seq 0 (length frees)) frees
    4.23      val declarative_axioms =
    4.24        map2 (declarative_axiom_for_free card) (index_seq 0 (length frees)) frees
    4.25 -    val formula = kodkod_formula_for_term ctxt card frees neg_t
    4.26 +    val formula = kodkod_formula_from_term ctxt card frees neg_t
    4.27                    |> fold_rev (curry And) declarative_axioms
    4.28      val univ_card = univ_card 0 0 0 bounds formula
    4.29      val problem =

     5.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Wed Feb 17 11:20:09 2010 +0100
     5.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Wed Feb 17 12:14:08 2010 +0100
     5.3 @@ -130,7 +130,7 @@
     5.4    sel_names: nut list,
     5.5    nonsel_names: nut list,
     5.6    rel_table: nut NameTable.table,
     5.7 -  liberal: bool,
     5.8 +  unsound: bool,
     5.9    scope: scope,
    5.10    core: KK.formula,
    5.11    defs: KK.formula list}
    5.12 @@ -157,15 +157,15 @@
    5.13        (Path.variable "ISABELLE_HOME_USER" ::
    5.14         map Path.basic ["etc", "components"]))) ^ "\"."
    5.15  
    5.16 -val max_liberal_delay_ms = 200
    5.17 -val max_liberal_delay_percent = 2
    5.18 +val max_unsound_delay_ms = 200
    5.19 +val max_unsound_delay_percent = 2
    5.20  
    5.21  (* Time.time option -> int *)
    5.22 -fun liberal_delay_for_timeout NONE = max_liberal_delay_ms
    5.23 -  | liberal_delay_for_timeout (SOME timeout) =
    5.24 -    Int.max (0, Int.min (max_liberal_delay_ms,
    5.25 +fun unsound_delay_for_timeout NONE = max_unsound_delay_ms
    5.26 +  | unsound_delay_for_timeout (SOME timeout) =
    5.27 +    Int.max (0, Int.min (max_unsound_delay_ms,
    5.28                           Time.toMilliseconds timeout
    5.29 -                         * max_liberal_delay_percent div 100))
    5.30 +                         * max_unsound_delay_percent div 100))
    5.31  
    5.32  (* Time.time option -> bool *)
    5.33  fun passed_deadline NONE = false
    5.34 @@ -434,7 +434,7 @@
    5.35      val too_big_scopes = Unsynchronized.ref []
    5.36  
    5.37      (* bool -> scope -> rich_problem option *)
    5.38 -    fun problem_for_scope liberal
    5.39 +    fun problem_for_scope unsound
    5.40              (scope as {card_assigns, bits, bisim_depth, datatypes, ofs, ...}) =
    5.41        let
    5.42          val _ = not (exists (fn other => scope_less_eq other scope)
    5.43 @@ -469,10 +469,10 @@
    5.44                           (univ_card nat_card int_card main_j0 [] KK.True)
    5.45          val _ = check_arity min_univ_card min_highest_arity
    5.46  
    5.47 -        val core_u = choose_reps_in_nut scope liberal rep_table false core_u
    5.48 -        val def_us = map (choose_reps_in_nut scope liberal rep_table true)
    5.49 +        val core_u = choose_reps_in_nut scope unsound rep_table false core_u
    5.50 +        val def_us = map (choose_reps_in_nut scope unsound rep_table true)
    5.51                           def_us
    5.52 -        val nondef_us = map (choose_reps_in_nut scope liberal rep_table false)
    5.53 +        val nondef_us = map (choose_reps_in_nut scope unsound rep_table false)
    5.54                              nondef_us
    5.55  (*
    5.56          val _ = List.app (priority o string_for_nut ctxt)
    5.57 @@ -488,21 +488,19 @@
    5.58          val core_u = rename_vars_in_nut pool rel_table core_u
    5.59          val def_us = map (rename_vars_in_nut pool rel_table) def_us
    5.60          val nondef_us = map (rename_vars_in_nut pool rel_table) nondef_us
    5.61 -        (* nut -> KK.formula *)
    5.62 -        val to_f = kodkod_formula_from_nut bits ofs liberal kk
    5.63 -        val core_f = to_f core_u
    5.64 -        val def_fs = map to_f def_us
    5.65 -        val nondef_fs = map to_f nondef_us
    5.66 +        val core_f = kodkod_formula_from_nut bits ofs kk core_u
    5.67 +        val def_fs = map (kodkod_formula_from_nut bits ofs kk) def_us
    5.68 +        val nondef_fs = map (kodkod_formula_from_nut bits ofs kk) nondef_us
    5.69          val formula = fold (fold s_and) [def_fs, nondef_fs] core_f
    5.70 -        val comment = (if liberal then "liberal" else "conservative") ^ "\n" ^
    5.71 +        val comment = (if unsound then "unsound" else "sound") ^ "\n" ^
    5.72                        PrintMode.setmp [] multiline_string_for_scope scope
    5.73          val kodkod_sat_solver =
    5.74            Kodkod_SAT.sat_solver_spec effective_sat_solver |> snd
    5.75          val bit_width = if bits = 0 then 16 else bits + 1
    5.76 -        val delay = if liberal then
    5.77 +        val delay = if unsound then
    5.78                        Option.map (fn time => Time.- (time, Time.now ()))
    5.79                                   deadline
    5.80 -                      |> liberal_delay_for_timeout
    5.81 +                      |> unsound_delay_for_timeout
    5.82                      else
    5.83                        0
    5.84          val settings = [("solver", commas (map quote kodkod_sat_solver)),
    5.85 @@ -540,13 +538,13 @@
    5.86                 expr_assigns = [], formula = formula},
    5.87                {free_names = free_names, sel_names = sel_names,
    5.88                 nonsel_names = nonsel_names, rel_table = rel_table,
    5.89 -               liberal = liberal, scope = scope, core = core_f,
    5.90 +               unsound = unsound, scope = scope, core = core_f,
    5.91                 defs = nondef_fs @ def_fs @ declarative_axioms})
    5.92        end
    5.93        handle TOO_LARGE (loc, msg) =>
    5.94               if loc = "Nitpick_Kodkod.check_arity" andalso
    5.95                  not (Typtab.is_empty ofs) then
    5.96 -               problem_for_scope liberal
    5.97 +               problem_for_scope unsound
    5.98                     {hol_ctxt = hol_ctxt, card_assigns = card_assigns,
    5.99                      bits = bits, bisim_depth = bisim_depth,
   5.100                      datatypes = datatypes, ofs = Typtab.empty}
   5.101 @@ -556,13 +554,13 @@
   5.102               else
   5.103                 (Unsynchronized.change too_big_scopes (cons scope);
   5.104                  print_v (fn () => ("Limit reached: " ^ msg ^
   5.105 -                                   ". Skipping " ^ (if liberal then "potential"
   5.106 +                                   ". Skipping " ^ (if unsound then "potential"
   5.107                                                      else "genuine") ^
   5.108                                     " component of scope."));
   5.109                  NONE)
   5.110             | TOO_SMALL (loc, msg) =>
   5.111               (print_v (fn () => ("Limit reached: " ^ msg ^
   5.112 -                                 ". Skipping " ^ (if liberal then "potential"
   5.113 +                                 ". Skipping " ^ (if unsound then "potential"
   5.114                                                    else "genuine") ^
   5.115                                   " component of scope."));
   5.116                NONE)
   5.117 @@ -577,7 +575,7 @@
   5.118  
   5.119      val scopes = Unsynchronized.ref []
   5.120      val generated_scopes = Unsynchronized.ref []
   5.121 -    val generated_problems = Unsynchronized.ref []
   5.122 +    val generated_problems = Unsynchronized.ref ([] : rich_problem list)
   5.123      val checked_problems = Unsynchronized.ref (SOME [])
   5.124      val met_potential = Unsynchronized.ref 0
   5.125  
   5.126 @@ -711,7 +709,7 @@
   5.127            | KK.Normal (sat_ps, unsat_js) =>
   5.128              let
   5.129                val (lib_ps, con_ps) =
   5.130 -                List.partition (#liberal o snd o nth problems o fst) sat_ps
   5.131 +                List.partition (#unsound o snd o nth problems o fst) sat_ps
   5.132              in
   5.133                update_checked_problems problems (unsat_js @ map fst lib_ps);
   5.134                if null con_ps then
   5.135 @@ -728,9 +726,9 @@
   5.136                      (0, 0, donno)
   5.137                    else
   5.138                      let
   5.139 -                      (* "co_js" is the list of conservative problems whose
   5.140 -                         liberal pendants couldn't be satisfied and hence that
   5.141 -                         most probably can't be satisfied themselves. *)
   5.142 +                      (* "co_js" is the list of sound problems whose unsound
   5.143 +                         pendants couldn't be satisfied and hence that most
   5.144 +                         probably can't be satisfied themselves. *)
   5.145                        val co_js =
   5.146                          map (fn j => j - 1) unsat_js
   5.147                          |> filter (fn j =>
   5.148 @@ -743,7 +741,7 @@
   5.149                        val problems =
   5.150                          problems |> filter_out_indices bye_js
   5.151                                   |> max_potential <= 0
   5.152 -                                    ? filter_out (#liberal o snd)
   5.153 +                                    ? filter_out (#unsound o snd)
   5.154                      in
   5.155                        solve_any_problem max_potential max_genuine donno false
   5.156                                          problems
   5.157 @@ -763,7 +761,7 @@
   5.158                                                   (map fst sat_ps @ unsat_js)
   5.159                        val problems =
   5.160                          problems |> filter_out_indices bye_js
   5.161 -                                 |> filter_out (#liberal o snd)
   5.162 +                                 |> filter_out (#unsound o snd)
   5.163                      in solve_any_problem 0 max_genuine donno false problems end
   5.164                  end
   5.165              end
   5.166 @@ -807,10 +805,10 @@
   5.167              ()
   5.168          (* scope * bool -> rich_problem list * bool
   5.169             -> rich_problem list * bool *)
   5.170 -        fun add_problem_for_scope (scope as {datatypes, ...}, liberal)
   5.171 +        fun add_problem_for_scope (scope as {datatypes, ...}, unsound)
   5.172                                    (problems, donno) =
   5.173            (check_deadline ();
   5.174 -           case problem_for_scope liberal scope of
   5.175 +           case problem_for_scope unsound scope of
   5.176               SOME problem =>
   5.177               (problems
   5.178                |> (null problems orelse
   5.179 @@ -826,6 +824,28 @@
   5.180                 ([], donno)
   5.181          val _ = Unsynchronized.change generated_problems (append problems)
   5.182          val _ = Unsynchronized.change generated_scopes (append scopes)
   5.183 +        val _ =
   5.184 +          if j + 1 = n then
   5.185 +            let
   5.186 +              val (unsound_problems, sound_problems) =
   5.187 +                List.partition (#unsound o snd) (!generated_problems)
   5.188 +            in
   5.189 +              if not (null sound_problems) andalso
   5.190 +                 forall (KK.is_problem_trivially_false o fst)
   5.191 +                        sound_problems then
   5.192 +                print_m (fn () =>
   5.193 +                    "Warning: The conjecture either trivially holds or (more \
   5.194 +                    \likely) lies outside Nitpick's supported fragment." ^
   5.195 +                    (if exists (not o KK.is_problem_trivially_false o fst)
   5.196 +                               unsound_problems then
   5.197 +                       " Only potential counterexamples may be found."
   5.198 +                     else
   5.199 +                       ""))
   5.200 +              else
   5.201 +                ()
   5.202 +            end
   5.203 +          else
   5.204 +            ()
   5.205        in
   5.206          solve_any_problem max_potential max_genuine donno true (rev problems)
   5.207        end
   5.208 @@ -838,7 +858,7 @@
   5.209        let
   5.210          (* rich_problem list -> rich_problem list *)
   5.211          val do_filter =
   5.212 -          if !met_potential = max_potential then filter_out (#liberal o snd)
   5.213 +          if !met_potential = max_potential then filter_out (#unsound o snd)
   5.214            else I
   5.215          val total = length (!scopes)
   5.216          val unsat =

     6.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Wed Feb 17 11:20:09 2010 +0100
     6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Wed Feb 17 12:14:08 2010 +0100
     6.3 @@ -36,7 +36,7 @@
     6.4      hol_context -> int -> int Typtab.table -> kodkod_constrs
     6.5      -> nut NameTable.table -> dtype_spec list -> Kodkod.formula list
     6.6    val kodkod_formula_from_nut :
     6.7 -    int -> int Typtab.table -> bool -> kodkod_constrs -> nut -> Kodkod.formula
     6.8 +    int -> int Typtab.table -> kodkod_constrs -> nut -> Kodkod.formula
     6.9  end;
    6.10  
    6.11  structure Nitpick_Kodkod : NITPICK_KODKOD =
    6.12 @@ -954,8 +954,8 @@
    6.13    acyclicity_axioms_for_datatypes hol_ctxt kk rel_table dtypes @
    6.14    maps (other_axioms_for_datatype hol_ctxt bits ofs kk rel_table) dtypes
    6.15  
    6.16 -(* int -> int Typtab.table -> bool -> kodkod_constrs -> nut -> KK.formula *)
    6.17 -fun kodkod_formula_from_nut bits ofs liberal
    6.18 +(* int -> int Typtab.table -> kodkod_constrs -> nut -> KK.formula *)
    6.19 +fun kodkod_formula_from_nut bits ofs
    6.20          (kk as {kk_all, kk_exist, kk_formula_let, kk_formula_if, kk_or, kk_not,
    6.21                  kk_iff, kk_implies, kk_and, kk_subset, kk_rel_eq, kk_no,
    6.22                  kk_lone, kk_one, kk_some, kk_rel_let, kk_rel_if, kk_union,

     7.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Wed Feb 17 11:20:09 2010 +0100
     7.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Wed Feb 17 12:14:08 2010 +0100
     7.3 @@ -892,7 +892,7 @@
     7.4  (* scope -> bool -> rep NameTable.table -> bool -> nut -> nut *)
     7.5  fun choose_reps_in_nut (scope as {hol_ctxt as {thy, ctxt, ...}, card_assigns,
     7.6                                    bits, datatypes, ofs, ...})
     7.7 -                       liberal table def =
     7.8 +                       unsound table def =
     7.9    let
    7.10      val bool_atom_R = Atom (2, offset_of_type ofs bool_T)
    7.11      (* polarity -> bool -> rep *)
    7.12 @@ -1036,7 +1036,7 @@
    7.13                if is_constructive u then s_op2 Eq T (Formula Neut) u1' u2'
    7.14                else opt_opt_case ()
    7.15            in
    7.16 -            if liberal orelse polar = Neg orelse
    7.17 +            if unsound orelse polar = Neg orelse
    7.18                 is_concrete_type datatypes (type_of u1) then
    7.19                case (is_opt_rep (rep_of u1'), is_opt_rep (rep_of u2')) of
    7.20                  (true, true) => opt_opt_case ()
    7.21 @@ -1138,7 +1138,7 @@
    7.22                else
    7.23                  let val quant_u = s_op2 oper T (Formula polar) u1' u2' in
    7.24                    if def orelse
    7.25 -                     (liberal andalso (polar = Pos) = (oper = All)) orelse
    7.26 +                     (unsound andalso (polar = Pos) = (oper = All)) orelse
    7.27                       is_complete_type datatypes (type_of u1) then
    7.28                      quant_u
    7.29                    else

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