src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 34121 5e831d805118
parent 33982 1ae222745c4a
child 34123 c4988215a691
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Dec 14 12:14:12 2009 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Dec 14 12:30:26 2009 +0100
     1.3 @@ -60,7 +60,7 @@
     1.4       ? prefix "\<^isub>,"
     1.5  (* string -> typ -> int -> string *)
     1.6  fun atom_name prefix (T as Type (s, _)) j =
     1.7 -    prefix ^ substring (short_name s, 0, 1) ^ atom_suffix s j
     1.8 +    prefix ^ substring (shortest_name s, 0, 1) ^ atom_suffix s j
     1.9    | atom_name prefix (T as TFree (s, _)) j =
    1.10      prefix ^ perhaps (try (unprefix "'")) s ^ atom_suffix s j
    1.11    | atom_name _ T _ = raise TYPE ("Nitpick_Model.atom_name", [T], [])
    1.12 @@ -125,7 +125,8 @@
    1.13          $ aux T1 T2 ps $ t1 $ t2
    1.14    in aux T1 T2 o rev end
    1.15  (* term -> bool *)
    1.16 -fun is_plain_fun (Const (s, _)) = s mem [@{const_name undefined}, non_opt_name]
    1.17 +fun is_plain_fun (Const (s, _)) =
    1.18 +    (s = @{const_name undefined} orelse s = non_opt_name)
    1.19    | is_plain_fun (Const (@{const_name fun_upd}, _) $ t0 $ _ $ _) =
    1.20      is_plain_fun t0
    1.21    | is_plain_fun _ = false
    1.22 @@ -350,7 +351,8 @@
    1.23              val real_j = j + offset_of_type ofs T
    1.24              val constr_x as (constr_s, constr_T) =
    1.25                get_first (fn (jss, {const, ...}) =>
    1.26 -                            if [real_j] mem jss then SOME const else NONE)
    1.27 +                            if member (op =) jss [real_j] then SOME const
    1.28 +                            else NONE)
    1.29                          (discr_jsss ~~ constrs) |> the
    1.30              val arg_Ts = curried_binder_types constr_T
    1.31              val sel_xs = map (boxed_nth_sel_for_constr ext_ctxt constr_x)
    1.32 @@ -369,7 +371,7 @@
    1.33                                          else NONE)) sel_jsss
    1.34              val uncur_arg_Ts = binder_types constr_T
    1.35            in
    1.36 -            if co andalso (T, j) mem seen then
    1.37 +            if co andalso member (op =) seen (T, j) then
    1.38                Var (var ())
    1.39              else
    1.40                let
    1.41 @@ -408,7 +410,7 @@
    1.42                in
    1.43                  if co then
    1.44                    let val var = var () in
    1.45 -                    if exists_subterm (equal (Var var)) t then
    1.46 +                    if exists_subterm (curry (op =) (Var var)) t then
    1.47                        Const (@{const_name The}, (T --> bool_T) --> T)
    1.48                        $ Abs ("\<omega>", T,
    1.49                               Const (@{const_name "op ="}, [T, T] ---> bool_T)
    1.50 @@ -449,7 +451,8 @@
    1.51            val ts1 = map (term_for_rep seen T1 T1 R1 o single) jss1
    1.52            val ts2 =
    1.53              map (fn js => term_for_rep seen T2 T2 (Atom (2, 0))
    1.54 -                                       [[int_for_bool (js mem jss)]]) jss1
    1.55 +                                       [[int_for_bool (member (op =) jss js)]])
    1.56 +                jss1
    1.57          in make_fun false T1 T2 T' ts1 ts2 end
    1.58        | term_for_rep seen (Type ("fun", [T1, T2])) T' (Func (R1, R2)) jss =
    1.59          let
    1.60 @@ -517,7 +520,7 @@
    1.61          let
    1.62            val ((head1, args1), (head2, args2)) =
    1.63              pairself (strip_comb o unfold_outer_the_binders) (t1, t2)
    1.64 -          val max_depth = max_depth - (if T mem coTs then 1 else 0)
    1.65 +          val max_depth = max_depth - (if member (op =) coTs T then 1 else 0)
    1.66          in
    1.67            head1 = head2
    1.68            andalso forall (bisimilar_values coTs max_depth) (args1 ~~ args2)
    1.69 @@ -639,10 +642,12 @@
    1.70      val (eval_names, noneval_nonskolem_nonsel_names) =
    1.71        List.partition (String.isPrefix eval_prefix o nickname_of)
    1.72                       nonskolem_nonsel_names
    1.73 -      ||> filter_out (equal @{const_name bisim_iterator_max} o nickname_of)
    1.74 +      ||> filter_out (curry (op =) @{const_name bisim_iterator_max}
    1.75 +                      o nickname_of)
    1.76      val free_names =
    1.77        map (fn x as (s, T) =>
    1.78 -              case filter (equal x o pairf nickname_of (unbox_type o type_of))
    1.79 +              case filter (curry (op =) x
    1.80 +                           o pairf nickname_of (unbox_type o type_of))
    1.81                            free_names of
    1.82                  [name] => name
    1.83                | [] => FreeName (s, T, Any)