just one version of fold_rev2;
authorwenzelm
Fri Nov 26 22:04:33 2010 +0100 (2010-11-26)
changeset 40721e5089e903e39
parent 40720 b770df486e5c
child 40722 441260986b63
just one version of fold_rev2;
src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML
src/HOL/Multivariate_Analysis/normarith.ML
src/Pure/library.ML
     1.1 --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Fri Nov 26 21:31:46 2010 +0100
     1.2 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Fri Nov 26 22:04:33 2010 +0100
     1.3 @@ -103,11 +103,6 @@
     1.4  
     1.5  fun iszero (k,r) = r =/ rat_0;
     1.6  
     1.7 -fun fold_rev2 f l1 l2 b =
     1.8 -  case (l1,l2) of
     1.9 -    ([],[]) => b
    1.10 -  | (h1::t1,h2::t2) => f h1 h2 (fold_rev2 f t1 t2 b)
    1.11 -  | _ => error "fold_rev2";
    1.12  
    1.13  (* Vectors. Conventionally indexed 1..n.                                     *)
    1.14  
     2.1 --- a/src/HOL/Multivariate_Analysis/normarith.ML	Fri Nov 26 21:31:46 2010 +0100
     2.2 +++ b/src/HOL/Multivariate_Analysis/normarith.ML	Fri Nov 26 22:04:33 2010 +0100
     2.3 @@ -239,10 +239,6 @@
     2.4    Const(@{const_name norm},_)$_ => arg_conv vector_canon_conv ct
     2.5   | _ => raise CTERM ("norm_canon_conv", [ct])
     2.6  
     2.7 -fun fold_rev2 f [] [] z = z
     2.8 - | fold_rev2 f (x::xs) (y::ys) z = f x y (fold_rev2 f xs ys z)
     2.9 - | fold_rev2 f _ _ _ = raise UnequalLengths;
    2.10 -
    2.11  fun int_flip v eq =
    2.12    if FuncUtil.Intfunc.defined eq v
    2.13    then FuncUtil.Intfunc.update (v, Rat.neg (FuncUtil.Intfunc.apply eq v)) eq else eq;
     3.1 --- a/src/Pure/library.ML	Fri Nov 26 21:31:46 2010 +0100
     3.2 +++ b/src/Pure/library.ML	Fri Nov 26 22:04:33 2010 +0100
     3.3 @@ -97,6 +97,7 @@
     3.4    val eq_list: ('a * 'b -> bool) -> 'a list * 'b list -> bool
     3.5    val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
     3.6    val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
     3.7 +  val fold_rev2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
     3.8    val forall2: ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
     3.9    val zip_options: 'a list -> 'b option list -> ('a * 'b) list
    3.10    val ~~ : 'a list * 'b list -> ('a * 'b) list
    3.11 @@ -544,6 +545,10 @@
    3.12    | fold2 f (x :: xs) (y :: ys) z = fold2 f xs ys (f x y z)
    3.13    | fold2 f _ _ _ = raise UnequalLengths;
    3.14  
    3.15 +fun fold_rev2 f [] [] z = z
    3.16 +  | fold_rev2 f (x :: xs) (y :: ys) z = f x y (fold_rev2 f xs ys z)
    3.17 +  | fold_rev2 f _ _ _ = raise UnequalLengths;
    3.18 +
    3.19  fun forall2 P [] [] = true
    3.20    | forall2 P (x :: xs) (y :: ys) = P x y andalso forall2 P xs ys
    3.21    | forall2 P _ _ = false;