# HG changeset patch
# User blanchet
# Date 1325611997 -3600
# Node ID 447cda88adfec014a53b2b437b65ef6ad294513e
# Parent  dd7fb9e651adb0adae55e5f74742eb3046a011a4
fixed a few more bugs in \Nitpick's new "set" support

diff -r dd7fb9e651ad -r 447cda88adfe src/HOL/Nitpick_Examples/Core_Nits.thy
--- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Tue Jan 03 18:33:17 2012 +0100
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Tue Jan 03 18:33:17 2012 +0100
@@ -68,7 +68,7 @@
 by auto
 
 lemma "(a\<Colon>'a\<Rightarrow>'b, a) \<in> Id\<^sup>*"
-nitpick [card = 1\<emdash>3, expect = none]
+nitpick [card = 1\<emdash>2, expect = none]
 by auto
 
 lemma "(a\<Colon>'a\<times>'a, a) \<in> Id\<^sup>* \<union> {(a, b)}\<^sup>*"
@@ -147,7 +147,7 @@
 nitpick [card = 15, expect = none]
 by auto
 
-lemma "(A, B) \<in> R \<or> (\<exists>C. (A, C) \<in> R \<and> (C, B) \<in> R) \<Longrightarrow> 
+lemma "(A, B) \<in> R \<or> (\<exists>C. (A, C) \<in> R \<and> (C, B) \<in> R) \<Longrightarrow>
        A = B \<or> (A, B) \<in> R \<or> (\<exists>C. (A, C) \<in> R \<and> (C, B) \<in> R)"
 nitpick [card = 1\<emdash>25, expect = none]
 by auto
diff -r dd7fb9e651ad -r 447cda88adfe src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Jan 03 18:33:17 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Jan 03 18:33:17 2012 +0100
@@ -1423,8 +1423,9 @@
         | Atom (k, _) =>
           let
             val dom_card = card_of_rep (rep_of arg_u)
-            val ran_R = Atom (exact_root dom_card k,
-                              offset_of_type ofs (range_type (type_of func_u)))
+            val ran_R =
+              Atom (exact_root dom_card k,
+                    offset_of_type ofs (pseudo_range_type (type_of func_u)))
           in
             to_apply_vect dom_card ran_R res_R (to_vect dom_card ran_R func_u)
                           arg_u
diff -r dd7fb9e651ad -r 447cda88adfe src/HOL/Tools/Nitpick/nitpick_mono.ML
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Jan 03 18:33:17 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Jan 03 18:33:17 2012 +0100
@@ -845,7 +845,7 @@
             | @{const_name fst} => do_nth_pair_sel 0 T accum
             | @{const_name snd} => do_nth_pair_sel 1 T accum
             | @{const_name Id} =>
-              (MFun (mtype_for (domain_type T), A Gen, bool_M), accum)
+              (MFun (mtype_for (elem_type T), A Gen, bool_M), accum)
             | @{const_name converse} =>
               let
                 val x = Unsynchronized.inc max_fresh
diff -r dd7fb9e651ad -r 447cda88adfe src/HOL/Tools/Nitpick/nitpick_nut.ML
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Jan 03 18:33:17 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Jan 03 18:33:17 2012 +0100
@@ -562,11 +562,11 @@
             do_apply t0 ts
         | (t0 as Const (x as (@{const_name ord_class.less_eq}, T)),
            ts as [t1, t2]) =>
-          if is_built_in_const thy stds x then
+          if is_set_like_type (domain_type T) then
+            Op2 (Subset, bool_T, Any, sub t1, sub t2)
+          else if is_built_in_const thy stds x then
             (* FIXME: find out if this case is necessary *)
             Op1 (Not, bool_T, Any, Op2 (Less, bool_T, Any, sub t2, sub t1))
-          else if is_set_like_type (domain_type T) then
-            Op2 (Subset, bool_T, Any, sub t1, sub t2)
           else
             do_apply t0 ts
         | (Const (@{const_name nat_gcd}, T), []) => Cst (Gcd, T, Any)
@@ -968,7 +968,7 @@
                val u2' = aux table' false Neut u2
                val R =
                  if is_opt_rep (rep_of u2') orelse
-                    (range_type T = bool_T andalso
+                    (pseudo_range_type T = bool_T andalso
                      not (is_Cst False (unrepify_nut_in_nut table false Neut
                                                             u1 u2))) then
                    opt_rep ofs T R
diff -r dd7fb9e651ad -r 447cda88adfe src/HOL/Tools/Nitpick/nitpick_rep.ML
--- a/src/HOL/Tools/Nitpick/nitpick_rep.ML	Tue Jan 03 18:33:17 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_rep.ML	Tue Jan 03 18:33:17 2012 +0100
@@ -234,7 +234,8 @@
 fun rep_to_binary_rel_rep ofs T R =
   let
     val k = exact_root 2 (card_of_domain_from_rep 2 R)
-    val j0 = offset_of_type ofs (fst (HOLogic.dest_prodT (domain_type T)))
+    val j0 =
+      offset_of_type ofs (fst (HOLogic.dest_prodT (pseudo_domain_type T)))
   in Func (Struct [Atom (k, j0), Atom (k, j0)], Formula Neut) end
 
 fun best_one_rep_for_type (scope as {card_assigns, ...} : scope)