# HG changeset patch
# User blanchet
# Date 1416828913 -3600
# Node ID e50f1973cb0a4103bcae038726391ed1642b0504
# Parent  650dcf62472990687d0d7086633f61153294da7d
no need for subset operation as a primitive in Nitpick, esp. that its implementation was unsound (cf. Rene Thiemann's 16 Oct 2014 email on isabelle mailing list)

diff -r 650dcf624729 -r e50f1973cb0a src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Nov 24 12:35:13 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Nov 24 12:35:13 2014 +0100
@@ -415,8 +415,6 @@
    ((@{const_name uminus_class.uminus}, int_T --> int_T), 0),
    ((@{const_name ord_class.less}, int_T --> int_T --> bool_T), 2),
    ((@{const_name ord_class.less_eq}, int_T --> int_T --> bool_T), 2)]
-val built_in_set_like_consts =
-  [(@{const_name ord_class.less_eq}, 2)]
 
 fun unarize_type @{typ "unsigned_bit word"} = nat_T
   | unarize_type @{typ "signed_bit word"} = int_T
@@ -1382,10 +1380,7 @@
         case s of
           @{const_name zero_class.zero} => if is_iterator_type T then SOME 0 else NONE
         | @{const_name Suc} => if is_iterator_type (domain_type T) then SOME 0 else NONE
-        | _ => if is_fun_type T andalso is_set_like_type (domain_type T) then
-                 AList.lookup (op =) built_in_set_like_consts s
-               else
-                 NONE
+        | _ => NONE
 
 val is_built_in_const = is_some o arity_of_built_in_const
 
diff -r 650dcf624729 -r e50f1973cb0a src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Mon Nov 24 12:35:13 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Mon Nov 24 12:35:13 2014 +0100
@@ -804,36 +804,6 @@
          | Op2 (Less, T, Formula polar, u1, u2) =>
            formula_from_opt_atom polar bool_j0
                (to_r (Op2 (Less, T, Opt bool_atom_R, u1, u2)))
-         | Op2 (Subset, _, _, u1, u2) =>
-           let
-             val dom_T = pseudo_domain_type (type_of u1)
-             val R1 = rep_of u1
-             val R2 = rep_of u2
-             val (dom_R, ran_R) =
-               case min_rep R1 R2 of
-                 Func Rp => Rp
-               | R => (Atom (card_of_domain_from_rep 2 R,
-                             offset_of_type ofs dom_T),
-                       if is_opt_rep R then Opt bool_atom_R else Formula Neut)
-             val set_R = Func (dom_R, ran_R)
-           in
-             if not (is_opt_rep ran_R) then
-               to_set_bool_op kk_implies kk_subset u1 u2
-             else if polar = Neut then
-               raise NUT ("Nitpick_Kodkod.to_f (Subset)", [u])
-             else
-               let
-                 (* FIXME: merge with similar code below *)
-                 fun set_to_r widen u =
-                   if widen then
-                     kk_difference (full_rel_for_rep dom_R)
-                                   (kk_join (to_rep set_R u) false_atom)
-                   else
-                     kk_join (to_rep set_R u) true_atom
-                 val widen1 = (polar = Pos andalso is_opt_rep R1)
-                 val widen2 = (polar = Neg andalso is_opt_rep R2)
-               in kk_subset (set_to_r widen1 u1) (set_to_r widen2 u2) end
-           end
          | Op2 (DefEq, _, _, u1, u2) =>
            (case min_rep (rep_of u1) (rep_of u2) of
               Formula polar =>
@@ -1230,7 +1200,6 @@
                      (to_rep (Func (Struct [b_R, c_R], Formula Neut)) u2)
            | Opt (Atom (2, _)) =>
              let
-               (* FIXME: merge with similar code above *)
                fun must R1 R2 u =
                  kk_join (to_rep (Func (Struct [R1, R2], body_R)) u) true_atom
                fun may R1 R2 u =
diff -r 650dcf624729 -r e50f1973cb0a src/HOL/Tools/Nitpick/nitpick_nut.ML
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Mon Nov 24 12:35:13 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Mon Nov 24 12:35:13 2014 +0100
@@ -49,7 +49,6 @@
     Or |
     And |
     Less |
-    Subset |
     DefEq |
     Eq |
     Triad |
@@ -162,7 +161,6 @@
   Or |
   And |
   Less |
-  Subset |
   DefEq |
   Eq |
   Triad |
@@ -225,7 +223,6 @@
   | string_for_op2 Or = "Or"
   | string_for_op2 And = "And"
   | string_for_op2 Less = "Less"
-  | string_for_op2 Subset = "Subset"
   | string_for_op2 DefEq = "DefEq"
   | string_for_op2 Eq = "Eq"
   | string_for_op2 Triad = "Triad"
@@ -567,9 +564,7 @@
             do_apply t0 ts
         | (t0 as Const (x as (@{const_name ord_class.less_eq}, T)),
            ts as [t1, t2]) =>
-          if is_set_like_type (domain_type T) then
-            Op2 (Subset, bool_T, Any, sub t1, sub t2)
-          else if is_built_in_const x then
+          if is_built_in_const 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
@@ -914,21 +909,6 @@
             val u2 = sub u2
             val R = bool_rep polar (exists (is_opt_rep o rep_of) [u1, u2])
           in s_op2 Less T R u1 u2 end
-        | Op2 (Subset, T, _, u1, u2) =>
-          let
-            val u1 = sub u1
-            val u2 = sub u2
-            val opt = exists (is_opt_rep o rep_of) [u1, u2]
-            val R = bool_rep polar opt
-          in
-            if is_opt_rep R then
-              triad_fn (fn polar => s_op2 Subset T (Formula polar) u1 u2)
-            else if not opt orelse unsound orelse polar = Neg orelse
-                    is_concrete_type data_types true (type_of u1) then
-              s_op2 Subset T R u1 u2
-            else
-              Cst (False, T, Formula Pos)
-          end
         | Op2 (DefEq, T, _, u1, u2) =>
           s_op2 DefEq T (Formula Neut) (sub u1) (sub u2)
         | Op2 (Eq, T, _, u1, u2) =>