# HG changeset patch
# User blanchet
# Date 1257857200 -3600
# Node ID bdf98e327f0b3686b5a7beda5f20308d40b8f312
# Parent  e1e77265fb1d41b4df65e8f5727a22c429969cd8
fixed soundness bug in Nitpick related to sets of sets;
(detected thanks to the TPTP)

diff -r e1e77265fb1d -r bdf98e327f0b src/HOL/Tools/Nitpick/HISTORY
--- a/src/HOL/Tools/Nitpick/HISTORY	Thu Nov 05 19:06:35 2009 +0100
+++ b/src/HOL/Tools/Nitpick/HISTORY	Tue Nov 10 13:46:40 2009 +0100
@@ -10,6 +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 monotonicity check
   * Fixed error in display of uncurried constants
   * Speeded up scope enumeration
diff -r e1e77265fb1d -r bdf98e327f0b src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Thu Nov 05 19:06:35 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Nov 10 13:46:40 2009 +0100
@@ -580,9 +580,9 @@
            val schema = atom_schema_of_rep R1
            val r1 = fold1 (#kk_product kk) (unary_var_seq ~1 (length schema))
                     |> rel_expr_from_rel_expr kk R1' R1
+           val kk_xeq = (if is_one_rep R1' then #kk_subset else #kk_rel_eq) kk
          in
-           #kk_comprehension kk (decls_for_atom_schema ~1 schema)
-                                (#kk_subset kk r1 r)
+           #kk_comprehension kk (decls_for_atom_schema ~1 schema) (kk_xeq r1 r)
          end
      | Func (Unit, (Atom (2, j0))) =>
        #kk_rel_if kk (#kk_rel_eq kk r (Kodkod.Atom (j0 + 1)))
@@ -616,7 +616,7 @@
                val r3 = atom_from_formula kk j0 (#kk_subset kk r1 r)
              in
                #kk_comprehension kk (decls_for_atom_schema ~1 (schema @ [x]))
-                                 (#kk_rel_eq kk r2 r3)
+                                 (#kk_subset kk r2 r3)
              end
            end
          | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr",
@@ -641,10 +641,11 @@
                                               (length ran_schema))
                          |> rel_expr_from_rel_expr kk R2' R2
           val app = kk_n_fold_join kk true R1' R2' dom_prod r
+          val kk_xeq = (if is_one_rep R2' then #kk_subset else #kk_rel_eq) kk
         in
           #kk_comprehension kk (decls_for_atom_schema ~1
                                                       (dom_schema @ ran_schema))
-                               (#kk_subset kk ran_prod app)
+                               (kk_xeq ran_prod app)
         end
     | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr",
                       [old_R, Func (R1, R2)])