src/HOL/Tools/Nitpick/nitpick_nut.ML
changeset 41049 0edd245892ed
parent 41047 9f1d3fcef1ca
child 41856 7244589c8ccc
--- 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 |
-    Image |
     Apply |
     Lambda
 
@@ -169,7 +168,6 @@
   Eq |
   Triad |
   Composition |
-  Image |
   Apply |
   Lambda
 
@@ -233,7 +231,6 @@
   | string_for_op2 Eq = "Eq"
   | string_for_op2 Triad = "Triad"
   | string_for_op2 Composition = "Composition"
-  | string_for_op2 Image = "Image"
   | string_for_op2 Apply = "Apply"
   | string_for_op2 Lambda = "Lambda"
 
@@ -525,8 +522,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 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)), []) =>
           if is_built_in_const thy stds x then Cst (Suc, T, Any)
           else if is_constr ctxt stds x then do_construct x []
@@ -936,46 +931,6 @@
               Cst (False, T, Formula Pos)
               |> polar = Neut ? (fn pos_u => triad pos_u (gsub def Neg u))
           end
-        | Op2 (Image, T, _, u1, u2) =>
-          let
-            val u1' = sub u1
-            val u2' = sub u2
-          in
-            (case (rep_of u1', rep_of u2') of
-               (Func (R11, R12), Func (R21, Formula Neut)) =>
-               if R21 = R11 andalso is_lone_rep R12 then
-                 let
-                   val R =
-                     best_non_opt_set_rep_for_type scope T
-                     |> exists (is_opt_rep o rep_of) [u1', u2'] ? opt_rep ofs T
-                 in s_op2 Image T R u1' u2' end
-               else
-                 raise SAME ()
-             | _ => raise SAME ())
-            handle SAME () =>
-                   let
-                     val T1 = type_of u1
-                     val dom_T = domain_type T1
-                     val ran_T = range_type T1
-                     val x_u = BoundName (~1, dom_T, Any, "image.x")
-                     val y_u = BoundName (~2, ran_T, Any, "image.y")
-                   in
-                     Op2 (Lambda, T, Any, y_u,
-                          Op2 (Exist, bool_T, Any, x_u,
-                               Op2 (And, bool_T, Any,
-                                    case u2 of
-                                      Op2 (Lambda, _, _, u21, u22) =>
-                                      if num_occurrences_in_nut u21 u22 = 0 then
-                                        u22
-                                      else
-                                        Op2 (Apply, bool_T, Any, u2, x_u)
-                                    | _ => Op2 (Apply, bool_T, Any, u2, x_u),
-
-                                    Op2 (Eq, bool_T, Any, y_u,
-                                         Op2 (Apply, ran_T, Any, u1, x_u)))))
-                     |> sub
-                   end
-          end
         | Op2 (Apply, T, _, u1, u2) =>
           let
             val u1 = sub u1