# HG changeset patch
# User blanchet
# Date 1291719361 -3600
# Node ID 9f1d3fcef1ca91aa4ca63ab297e5f89591b769aa
# Parent  f2e94005d28346afa44133e9f0aa94fd8f72fb8b
simplified special handling of set products

diff -r f2e94005d283 -r 9f1d3fcef1ca src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Dec 07 11:56:01 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Dec 07 11:56:01 2010 +0100
@@ -424,7 +424,6 @@
    (@{const_name converse}, 1),
    (@{const_name trancl}, 1),
    (@{const_name rel_comp}, 2),
-   (@{const_name prod}, 2),
    (@{const_name image}, 2),
    (@{const_name finite}, 1),
    (@{const_name unknown}, 0),
diff -r f2e94005d283 -r 9f1d3fcef1ca src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Dec 07 11:56:01 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Dec 07 11:56:01 2010 +0100
@@ -1510,28 +1510,6 @@
            | _ => raise NUT ("Nitpick_Kodkod.to_r (Composition)", [u]))
           |> rel_expr_from_rel_expr kk R (Func (Struct [a_R, c_R], body_R))
         end
-      | Op2 (Product, T, R, u1, u2) =>
-        let
-          val (a_T, b_T) = HOLogic.dest_prodT (domain_type T)
-          val a_k = card_of_domain_from_rep 2 (rep_of u1)
-          val b_k = card_of_domain_from_rep 2 (rep_of u2)
-          val a_R = Atom (a_k, offset_of_type ofs a_T)
-          val b_R = Atom (b_k, offset_of_type ofs b_T)
-          val body_R = body_rep R
-        in
-          (case body_R of
-             Formula Neut =>
-             kk_product (to_rep (Func (a_R, Formula Neut)) u1)
-                        (to_rep (Func (b_R, Formula Neut)) u2)
-           | Opt (Atom (2, _)) =>
-             let
-               fun do_nut r R u = kk_join (to_rep (Func (R, body_R)) u) r
-               fun do_term r =
-                 kk_product (kk_product (do_nut r a_R u1) (do_nut r b_R u2)) r
-             in kk_union (do_term true_atom) (do_term false_atom) end
-           | _ => raise NUT ("Nitpick_Kodkod.to_r (Product)", [u]))
-          |> rel_expr_from_rel_expr kk R (Func (Struct [a_R, b_R], body_R))
-        end
       | Op2 (Image, T, R, u1, u2) =>
         (case (rep_of u1, rep_of u2) of
            (Func (R11, R12), Func (R21, Formula Neut)) =>
diff -r f2e94005d283 -r 9f1d3fcef1ca src/HOL/Tools/Nitpick/nitpick_nut.ML
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Dec 07 11:56:01 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Dec 07 11:56:01 2010 +0100
@@ -55,7 +55,6 @@
     Eq |
     Triad |
     Composition |
-    Product |
     Image |
     Apply |
     Lambda
@@ -170,7 +169,6 @@
   Eq |
   Triad |
   Composition |
-  Product |
   Image |
   Apply |
   Lambda
@@ -235,7 +233,6 @@
   | string_for_op2 Eq = "Eq"
   | string_for_op2 Triad = "Triad"
   | string_for_op2 Composition = "Composition"
-  | string_for_op2 Product = "Product"
   | string_for_op2 Image = "Image"
   | string_for_op2 Apply = "Apply"
   | string_for_op2 Lambda = "Lambda"
@@ -528,8 +525,6 @@
           Op1 (Closure, range_type T, Any, sub t1)
         | (Const (@{const_name rel_comp}, T), [t1, t2]) =>
           Op2 (Composition, nth_range_type 2 T, Any, sub t1, sub t2)
-        | (Const (@{const_name prod}, T), [t1, t2]) =>
-          Op2 (Product, nth_range_type 2 T, Any, sub t1, sub t2)
         | (Const (@{const_name image}, T), [t1, t2]) =>
           Op2 (Image, nth_range_type 2 T, Any, sub t1, sub t2)
         | (Const (x as (s as @{const_name Suc}, T)), []) =>