# HG changeset patch
# User blanchet
# Date 1258033674 -3600
# Node ID d3af5b21cbaff344ea185fa660898dafa7200c02
# Parent  68e058d061f518c59a62f6606db6131d2619ccde
fixed soundness bug in Nitpick related to sets

diff -r 68e058d061f5 -r d3af5b21cbaf src/HOL/Tools/Nitpick/HISTORY
--- a/src/HOL/Tools/Nitpick/HISTORY	Thu Nov 12 09:11:46 2009 +0100
+++ b/src/HOL/Tools/Nitpick/HISTORY	Thu Nov 12 14:47:54 2009 +0100
@@ -10,7 +10,7 @@
   * Optimized Kodkod encoding of datatypes whose constructors don't appear in
     the formula to falsify
   * Added support for codatatype view of datatypes
-  * Fixed soundness bug related to sets of sets
+  * Fixed soundness bugs related to sets and sets of sets
   * Fixed monotonicity check
   * Fixed error in display of uncurried constants
   * Speeded up scope enumeration
diff -r 68e058d061f5 -r d3af5b21cbaf src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Thu Nov 12 09:11:46 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Thu Nov 12 14:47:54 2009 +0100
@@ -1448,7 +1448,7 @@
           fold kk_join [to_integer u1, to_integer u2] nat_subtract_rel
       | Op2 (Apply, _, R, u1, u2) =>
         if is_Cst Unrep u2 andalso is_set_type (type_of u1)
-           andalso not (is_opt_rep (rep_of u1)) then
+           andalso is_FreeName u1 then
           false_atom
         else
           to_apply R u1 u2
diff -r 68e058d061f5 -r d3af5b21cbaf src/HOL/Tools/Nitpick/nitpick_nut.ML
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Thu Nov 12 09:11:46 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Thu Nov 12 14:47:54 2009 +0100
@@ -96,6 +96,7 @@
   val nickname_of : nut -> string
   val is_skolem_name : nut -> bool
   val is_eval_name : nut -> bool
+  val is_FreeName : nut -> bool
   val is_Cst : cst -> nut -> bool
   val fold_nut : (nut -> 'a -> 'a) -> nut -> 'a -> 'a
   val map_nut : (nut -> nut) -> nut -> nut
@@ -367,6 +368,8 @@
 fun is_eval_name u =
   String.isPrefix eval_prefix (nickname_of u)
   handle NUT ("Nitpick_Nut.nickname_of", _) => false
+fun is_FreeName (FreeName _) = true
+  | is_FreeName _ = false
 (* cst -> nut -> bool *)
 fun is_Cst cst (Cst (cst', _, _)) = (cst = cst')
   | is_Cst _ _ = false
@@ -764,9 +767,8 @@
 
 (* A nut is said to be constructive if whenever it evaluates to unknown in our
    three-valued logic, it would evaluate to a unrepresentable value ("unrep")
-   according to the HOL semantics. For example, "Suc n" is
-   constructive if "n" is representable or "Unrep", because unknown implies
-   unrep. *)
+   according to the HOL semantics. For example, "Suc n" is constructive if "n"
+   is representable or "Unrep", because unknown implies unrep. *)
 (* nut -> bool *)
 fun is_constructive u =
   is_Cst Unrep u orelse
@@ -830,13 +832,9 @@
       else if is_Cst Unrep u2 then
         if is_constructive u1 then
           Cst (Unrep, T, R)
-        else if is_boolean_type T andalso not (is_opt_rep (rep_of u1)) then
-          (* Selectors are an unfortunate exception to the rule that non-"Opt"
-             predicates return "False" for unrepresentable domain values. *)
-          case u1 of
-             ConstName (s, _, _) => if is_sel s then unknown_boolean T R
-                                    else Cst (False, T, Formula Neut)
-           | _ => Cst (False, T, Formula Neut)
+        else if is_boolean_type T then
+          if is_FreeName u1 then Cst (False, T, Formula Neut)
+          else unknown_boolean T R
         else case u1 of
           Op2 (Apply, _, _, ConstName (@{const_name List.append}, _, _), _) =>
           Cst (Unrep, T, R)