dropped find_index_eq
authorhaftmann
Fri Jul 10 07:59:27 2009 +0200 (2009-07-10)
changeset 31986a68f88d264f7
parent 31985 a6e982b1ebba
child 31987 f4c7be4d684f
dropped find_index_eq
src/HOL/Library/comm_ring.ML
src/HOL/Library/reflection.ML
src/HOL/Tools/Datatype/datatype_rep_proofs.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/refute.ML
src/HOL/ex/predicate_compile.ML
src/HOLCF/Tools/domain/domain_extender.ML
src/HOLCF/Tools/domain/domain_library.ML
src/Provers/Arith/fast_lin_arith.ML
src/Pure/library.ML
     1.1 --- a/src/HOL/Library/comm_ring.ML	Fri Jul 10 07:59:25 2009 +0200
     1.2 +++ b/src/HOL/Library/comm_ring.ML	Fri Jul 10 07:59:27 2009 +0200
     1.3 @@ -41,7 +41,7 @@
     1.4  fun reif_pol T vs (t as Free _) =
     1.5        let
     1.6          val one = @{term "1::nat"};
     1.7 -        val i = find_index_eq t vs
     1.8 +        val i = find_index (fn t' => t' = t) vs
     1.9        in if i = 0
    1.10          then pol_PX T $ (pol_Pc T $ cring_one T)
    1.11            $ one $ (pol_Pc T $ cring_zero T)
     2.1 --- a/src/HOL/Library/reflection.ML	Fri Jul 10 07:59:25 2009 +0200
     2.2 +++ b/src/HOL/Library/reflection.ML	Fri Jul 10 07:59:27 2009 +0200
     2.3 @@ -103,8 +103,8 @@
     2.4            NONE => error "index_of : type not found in environements!"
     2.5          | SOME (tbs,tats) =>
     2.6            let
     2.7 -            val i = find_index_eq t tats
     2.8 -            val j = find_index_eq t tbs
     2.9 +            val i = find_index (fn t' => t' = t) tats
    2.10 +            val j = find_index (fn t' => t' = t) tbs
    2.11            in (if j = ~1 then
    2.12                if i = ~1
    2.13                then (length tbs + length tats,
     3.1 --- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Fri Jul 10 07:59:25 2009 +0200
     3.2 +++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Fri Jul 10 07:59:27 2009 +0200
     3.3 @@ -111,7 +111,7 @@
     3.4              else
     3.5                Const ("Sum_Type.Inr", T2 --> T) $ (mk_inj' T2 (n - n2) (i - n2))
     3.6            end
     3.7 -      in mk_inj' sumT (length leafTs) (1 + find_index_eq T' leafTs)
     3.8 +      in mk_inj' sumT (length leafTs) (1 + find_index (fn T'' => T'' = T') leafTs)
     3.9        end;
    3.10  
    3.11      (* make injections for constructors *)
    3.12 @@ -137,7 +137,7 @@
    3.13              if i <= n2 then Const (Suml_name, mkT T1) $ mk_inj T1 n2 i
    3.14              else Const (Sumr_name, mkT T2) $ mk_inj T2 (n - n2) (i - n2)
    3.15            end
    3.16 -      in mk_inj branchT (length branchTs) (1 + find_index_eq T' branchTs)
    3.17 +      in mk_inj branchT (length branchTs) (1 + find_index (fn T'' => T'' = T') branchTs)
    3.18        end;
    3.19  
    3.20      val mk_lim = List.foldr (fn (T, t) => Lim $ mk_fun_inj T (Abs ("x", T, t)));
     4.1 --- a/src/HOL/Tools/inductive.ML	Fri Jul 10 07:59:25 2009 +0200
     4.2 +++ b/src/HOL/Tools/inductive.ML	Fri Jul 10 07:59:27 2009 +0200
     4.3 @@ -222,7 +222,7 @@
     4.4      val k = length params;
     4.5      val (c, ts) = strip_comb t;
     4.6      val (xs, ys) = chop k ts;
     4.7 -    val i = find_index_eq c cs;
     4.8 +    val i = find_index (fn c' => c' = c) cs;
     4.9    in
    4.10      if xs = params andalso i >= 0 then
    4.11        SOME (c, i, ys, chop (length ys)
     5.1 --- a/src/HOL/Tools/inductive_realizer.ML	Fri Jul 10 07:59:25 2009 +0200
     5.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Fri Jul 10 07:59:27 2009 +0200
     5.3 @@ -204,9 +204,9 @@
     5.4  fun indrule_realizer thy induct raw_induct rsets params vs rec_names rss intrs dummies =
     5.5    let
     5.6      val concls = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct));
     5.7 -    val premss = List.mapPartial (fn (s, rs) => if s mem rsets then
     5.8 -      SOME (rs, map (fn (_, r) => List.nth (prems_of raw_induct,
     5.9 -        find_index_eq (prop_of r) (map prop_of intrs))) rs) else NONE) rss;
    5.10 +    val premss = map_filter (fn (s, rs) => if member (op =) rsets s then
    5.11 +      SOME (rs, map (fn (_, r) => nth (prems_of raw_induct)
    5.12 +        (find_index (fn prp => prp = prop_of r) (map prop_of intrs))) rs) else NONE) rss;
    5.13      val fs = maps (fn ((intrs, prems), dummy) =>
    5.14        let
    5.15          val fs = map (fn (rule, (ivs, intr)) =>
     6.1 --- a/src/HOL/Tools/refute.ML	Fri Jul 10 07:59:25 2009 +0200
     6.2 +++ b/src/HOL/Tools/refute.ML	Fri Jul 10 07:59:27 2009 +0200
     6.3 @@ -2401,7 +2401,7 @@
     6.4                    (* by our assumption on the order of recursion operators *)
     6.5                    (* and datatypes, this is the index of the datatype      *)
     6.6                    (* corresponding to the given recursion operator         *)
     6.7 -                  val idt_index = find_index_eq s (#rec_names info)
     6.8 +                  val idt_index = find_index (fn s' => s' = s) (#rec_names info)
     6.9                    (* mutually recursive types must have the same type   *)
    6.10                    (* parameters, unless the mutual recursion comes from *)
    6.11                    (* indirect recursion                                 *)
    6.12 @@ -2535,7 +2535,7 @@
    6.13                    (* returned                                              *)
    6.14                    (* interpretation -> int -> int list option *)
    6.15                    fun get_args (Leaf xs) elem =
    6.16 -                    if find_index_eq True xs = elem then
    6.17 +                    if find_index (fn x => x = True) xs = elem then
    6.18                        SOME []
    6.19                      else
    6.20                        NONE
    6.21 @@ -2606,7 +2606,7 @@
    6.22                          (* corresponding recursive argument                 *)
    6.23                          fun rec_intr (DatatypeAux.DtRec i) (Leaf xs) =
    6.24                            (* recursive argument is "rec_i params elem" *)
    6.25 -                          compute_array_entry i (find_index_eq True xs)
    6.26 +                          compute_array_entry i (find_index (fn x => x = True) xs)
    6.27                            | rec_intr (DatatypeAux.DtRec _) (Node _) =
    6.28                            raise REFUTE ("IDT_recursion_interpreter",
    6.29                              "interpretation for IDT is a node")
    6.30 @@ -3237,7 +3237,7 @@
    6.31                    def_eq=false, next_idx=1, bounds=[], wellformed=True} cTerm
    6.32                  (* interpretation -> int list option *)
    6.33                  fun get_args (Leaf xs) =
    6.34 -                  if find_index_eq True xs = element then
    6.35 +                  if find_index (fn x => x = True) xs = element then
    6.36                      SOME []
    6.37                    else
    6.38                      NONE
     7.1 --- a/src/HOL/ex/predicate_compile.ML	Fri Jul 10 07:59:25 2009 +0200
     7.2 +++ b/src/HOL/ex/predicate_compile.ML	Fri Jul 10 07:59:27 2009 +0200
     7.3 @@ -419,8 +419,8 @@
     7.4                error ("Too few arguments for inductive predicate " ^ name)
     7.5              else chop (length iss) args;
     7.6            val k = length args2;
     7.7 -          val perm = map (fn i => (find_index_eq (Bound (b - i)) args2) + 1)
     7.8 -            (1 upto b)  
     7.9 +          val perm = map (fn i => (find_index (fn t => t = Bound (b - i)) args2) + 1)
    7.10 +            (1 upto b)
    7.11            val partial_mode = (1 upto k) \\ perm
    7.12          in
    7.13            if not (partial_mode subset is) then [] else
    7.14 @@ -627,7 +627,7 @@
    7.15          val (params, args') = chop (length ms) args
    7.16          val (inargs, outargs) = get_args is' args'
    7.17          val b = length vs
    7.18 -        val perm = map (fn i => (find_index_eq (Bound (b - i)) args') + 1) (1 upto b)
    7.19 +        val perm = map (fn i => find_index (fn t => t = Bound (b - i)) args' + 1) (1 upto b)
    7.20          val outp_perm =
    7.21            snd (get_args is perm)
    7.22            |> map (fn i => i - length (filter (fn x => x < i) is'))
     8.1 --- a/src/HOLCF/Tools/domain/domain_extender.ML	Fri Jul 10 07:59:25 2009 +0200
     8.2 +++ b/src/HOLCF/Tools/domain/domain_extender.ML	Fri Jul 10 07:59:27 2009 +0200
     8.3 @@ -121,7 +121,7 @@
     8.4        val thy' = thy'' |> Domain_Syntax.add_syntax comp_dnam eqs';
     8.5        val dts  = map (Type o fst) eqs';
     8.6        val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
     8.7 -      fun strip ss = Library.drop (find_index_eq "'" ss +1, ss);
     8.8 +      fun strip ss = Library.drop (find_index (fn s => s = "'") ss + 1, ss);
     8.9        fun typid (Type  (id,_)) =
    8.10            let val c = hd (Symbol.explode (Long_Name.base_name id))
    8.11            in if Symbol.is_letter c then c else "t" end
     9.1 --- a/src/HOLCF/Tools/domain/domain_library.ML	Fri Jul 10 07:59:25 2009 +0200
     9.2 +++ b/src/HOLCF/Tools/domain/domain_library.ML	Fri Jul 10 07:59:27 2009 +0200
     9.3 @@ -365,7 +365,7 @@
     9.4  fun cpair_pat (p1,p2) = %%: @{const_name cpair_pat} $ p1 $ p2;
     9.5  val mk_ctuple_pat = foldr1 cpair_pat;
     9.6  fun lift_defined f = lift (fn x => defined (f x));
     9.7 -fun bound_arg vns v = Bound(length vns -find_index_eq v vns -1);
     9.8 +fun bound_arg vns v = Bound (length vns - find_index (fn v' => v' = v) vns - 1);
     9.9  
    9.10  fun cont_eta_contract (Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body)) = 
    9.11      (case cont_eta_contract body  of
    10.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Fri Jul 10 07:59:25 2009 +0200
    10.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Fri Jul 10 07:59:27 2009 +0200
    10.3 @@ -391,7 +391,7 @@
    10.4             |> hd
    10.5           val (eq as Lineq(_,_,ceq,_),othereqs) =
    10.6                 extract_first (fn Lineq(_,_,l,_) => c mem l) eqs
    10.7 -         val v = find_index_eq c ceq
    10.8 +         val v = find_index (fn v => v = c) ceq
    10.9           val (ioth,roth) = List.partition (fn (Lineq(_,_,l,_)) => nth l v = 0)
   10.10                                       (othereqs @ noneqs)
   10.11           val others = map (elim_var v eq) roth @ ioth
    11.1 --- a/src/Pure/library.ML	Fri Jul 10 07:59:25 2009 +0200
    11.2 +++ b/src/Pure/library.ML	Fri Jul 10 07:59:27 2009 +0200
    11.3 @@ -97,7 +97,6 @@
    11.4    val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b
    11.5    val split_last: 'a list -> 'a list * 'a
    11.6    val find_index: ('a -> bool) -> 'a list -> int
    11.7 -  val find_index_eq: ''a -> ''a list -> int
    11.8    val find_first: ('a -> bool) -> 'a list -> 'a option
    11.9    val get_index: ('a -> 'b option) -> 'a list -> (int * 'b) option
   11.10    val get_first: ('a -> 'b option) -> 'a list -> 'b option
   11.11 @@ -503,8 +502,6 @@
   11.12          | find n (x :: xs) = if pred x then n else find (n + 1) xs;
   11.13    in find 0 end;
   11.14  
   11.15 -fun find_index_eq x = find_index (equal x);
   11.16 -
   11.17  (*find first element satisfying predicate*)
   11.18  val find_first = List.find;
   11.19