removed needless optimization for image -- there might be cases that benefit from it but there are others where it is clearly evil
--- 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 image}, 2),
(@{const_name finite}, 1),
(@{const_name unknown}, 0),
(@{const_name is_unknown}, 1),
--- 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,33 +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 (Image, T, R, u1, u2) =>
- (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
- fun big_join r = kk_n_fold_join kk false R21 R12 r (to_r u1)
- val core_r = big_join (to_r u2)
- val core_R = Func (R12, Formula Neut)
- in
- if is_opt_rep R12 then
- let
- val schema = atom_schema_of_rep R21
- val decls = decls_for_atom_schema ~1 schema
- val vars = unary_var_seq ~1 (length decls)
- val f = kk_some (big_join (fold1 kk_product vars))
- in
- kk_rel_if (kk_all decls f)
- (rel_expr_from_rel_expr kk R core_R core_r)
- (rel_expr_from_rel_expr kk R (opt_rep ofs T core_R)
- (kk_product core_r true_atom))
- end
- else
- rel_expr_from_rel_expr kk R core_R core_r
- end
- else
- raise NUT ("Nitpick_Kodkod.to_r (Image)", [u1, u2])
- | _ => raise NUT ("Nitpick_Kodkod.to_r (Image)", [u1, u2]))
| Op2 (Apply, @{typ nat}, _,
Op2 (Apply, _, _, Cst (Subtract, _, _), u1), u2) =>
if is_Cst Unrep u2 andalso not (is_opt_rep (rep_of u1)) then
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Dec 07 11:56:01 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Dec 07 11:56:01 2010 +0100
@@ -912,17 +912,6 @@
(MFun (bc_set_M, A Gen, MFun (ab_set_M, A Gen, ac_set_M)),
accum ||> add_annotation_atom_comp Neq [] (V x) (A New))
end
- | @{const_name image} =>
- let
- val x = Unsynchronized.inc max_fresh
- val a_M = mtype_for (domain_type (domain_type T))
- val b_M = mtype_for (range_type (domain_type T))
- in
- (MFun (MFun (a_M, A Gen, b_M), A Gen,
- MFun (MFun (a_M, V x, bool_M), A Gen,
- MFun (b_M, V x, bool_M))),
- accum ||> add_annotation_atom_comp Neq [] (V x) (A New))
- end
| @{const_name finite} =>
let
val M1 = mtype_for (domain_type (domain_type T))
--- 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