# HG changeset patch
# User blanchet
# Date 1258979072 -3600
# Node ID 348c3ea03e58b2a856a489782e333bf8db8674d2
# Parent  3a586209151ea6d333249dc03f5836fb57b2769f
fixed soundness bug in Nitpick that occurred because unrolled predicate iterators were considered to be a "precise" type

diff -r 3a586209151e -r 348c3ea03e58 src/HOL/Tools/Nitpick/HISTORY
--- a/src/HOL/Tools/Nitpick/HISTORY	Mon Nov 23 13:23:39 2009 +0100
+++ b/src/HOL/Tools/Nitpick/HISTORY	Mon Nov 23 13:24:32 2009 +0100
@@ -10,9 +10,11 @@
   * Optimized Kodkod encoding of datatypes whose constructors don't appear in
     the formula to falsify
   * Added support for codatatype view of datatypes
-  * Fixed soundness bugs related to sets and sets of sets
+  * Fixed soundness bugs related to sets, sets of sets, and (co)inductive
+    predicates
   * Fixed monotonicity check
-  * Fixed error when processing definitions that resulted in an exception
+  * Fixed error when processing definitions
+  * Fixed error in "star_linear_preds" optimization
   * Fixed error in Kodkod encoding of "The" and "Eps"
   * Fixed error in display of uncurried constants
   * Speeded up scope enumeration
@@ -70,7 +72,7 @@
   * Improved precision of "trancl" and "rtrancl"
   * Optimized Kodkod encoding of "tranclp" and "rtranclp"
   * Made detection of inconsistent scope specifications more robust
-  * Fixed a few Kodkod generation bugs that resulted in exceptions
+  * Fixed a few Kodkod generation bugs
 
 Version 1.1.1 (24 Jun 2009)
 
@@ -79,8 +81,7 @@
   * Improved precision of some set constructs
   * Fiddled with the automatic monotonicity check
   * Fixed performance issues related to scope enumeration
-  * Fixed a few Kodkod generation bugs that resulted in exceptions or stack
-    overflows
+  * Fixed a few Kodkod generation bugs
 
 Version 1.1.0 (16 Jun 2009)
 
@@ -117,7 +118,7 @@
   * Fixed soundness issue in handling of non-definitional axioms
   * Fixed soundness issue in handling of "Abs_" and "Rep_" functions for "unit",
     "nat", "int", and "*"
-  * Fixed a few Kodkod generation bugs that resulted in exceptions
+  * Fixed a few Kodkod generation bugs
   * Optimized "div", "mod", and "dvd" on "nat" and "int"
 
 Version 1.0.2 (12 Mar 2009)
@@ -152,7 +153,7 @@
     infinite loop for "Nominal.perm"
   * Added support for multiple instantiations of non-well-founded inductive
     predicates, which previously raised an exception
-  * Fixed a Kodkod generation bug that resulted in an exception
+  * Fixed a Kodkod generation bug
   * Altered order of scope enumeration and automatic SAT solver selection
   * Optimized "Eps", "nat_case", and "list_case"
   * Improved output formatting
diff -r 3a586209151e -r 348c3ea03e58 src/HOL/Tools/Nitpick/nitpick_nut.ML
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Mon Nov 23 13:23:39 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Mon Nov 23 13:24:32 2009 +0100
@@ -712,15 +712,16 @@
              else if is_rep_fun thy x then
                Func oo best_non_opt_symmetric_reps_for_fun_type
              else if all_precise orelse is_skolem_name v
-                     orelse s mem [@{const_name undefined_fast_The},
-                                   @{const_name undefined_fast_Eps},
-                                   @{const_name bisim}] then
+                     orelse original_name s
+                            mem [@{const_name undefined_fast_The},
+                                 @{const_name undefined_fast_Eps},
+                                 @{const_name bisim},
+                                 @{const_name bisim_iterator_max}] then
                best_non_opt_set_rep_for_type
              else if original_name s
                      mem [@{const_name set}, @{const_name distinct},
                           @{const_name ord_class.less},
-                          @{const_name ord_class.less_eq},
-                          @{const_name bisim_iterator_max}] then
+                          @{const_name ord_class.less_eq}] then
                best_set_rep_for_type
              else
                best_opt_set_rep_for_type) scope T
diff -r 3a586209151e -r 348c3ea03e58 src/HOL/Tools/Nitpick/nitpick_scope.ML
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Mon Nov 23 13:23:39 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Mon Nov 23 13:24:32 2009 +0100
@@ -100,8 +100,7 @@
     forall (is_precise_type dtypes) Ts
   | is_precise_type dtypes (Type ("*", Ts)) = forall (is_precise_type dtypes) Ts
   | is_precise_type dtypes T =
-    T <> nat_T andalso T <> int_T
-    andalso #precise (the (datatype_spec dtypes T))
+    not (is_integer_type T) andalso #precise (the (datatype_spec dtypes T))
     handle Option.Option => true
 fun is_fully_comparable_type dtypes (Type ("fun", [T1, T2])) =
     is_precise_type dtypes T1 andalso is_fully_comparable_type dtypes T2