# HG changeset patch # User blanchet # Date 1291719361 -3600 # Node ID 0edd245892edd5894a93304792cd750121aef213 # Parent d5ebe94248ad28b5c6e32914ad518cb78020909f removed needless optimization for image -- there might be cases that benefit from it but there are others where it is clearly evil diff -r d5ebe94248ad -r 0edd245892ed 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 image}, 2), (@{const_name finite}, 1), (@{const_name unknown}, 0), (@{const_name is_unknown}, 1), diff -r d5ebe94248ad -r 0edd245892ed 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,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 diff -r d5ebe94248ad -r 0edd245892ed src/HOL/Tools/Nitpick/nitpick_mono.ML --- 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)) diff -r d5ebe94248ad -r 0edd245892ed 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 | - 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