# HG changeset patch # User nipkow # Date 1178132406 -7200 # Node ID 72a7b6ad153b4e43ec7547f23468745a58e780cc # Parent f1db55c7534dd70cdb9c2790eb13a7f28c6486c7 tuned allpairs diff -r f1db55c7534d -r 72a7b6ad153b src/HOL/List.thy --- a/src/HOL/List.thy Wed May 02 01:42:23 2007 +0200 +++ b/src/HOL/List.thy Wed May 02 21:00:06 2007 +0200 @@ -42,7 +42,7 @@ "distinct":: "'a list => bool" replicate :: "nat => 'a => 'a list" splice :: "'a list \ 'a list \ 'a list" - allpairs :: "'a list \ 'b list \ ('a * 'b)list" + allpairs :: "('a \ 'b \ 'c) \ 'a list \ 'b list \ 'c list" abbreviation upto:: "nat => nat => nat list" ("(1[_../_])") where @@ -211,8 +211,8 @@ -- {*Warning: simpset does not contain the second eqn but a derived one. *} primrec -"allpairs [] ys = []" -"allpairs (x # xs) ys = map (Pair x) ys @ allpairs xs ys" +"allpairs f [] ys = []" +"allpairs f (x # xs) ys = map (f x) ys @ allpairs f xs ys" subsubsection {* @{const Nil} and @{const Cons} *} @@ -250,7 +250,7 @@ by (cases xs) auto lemma length_allpairs[simp]: - "length(allpairs xs ys) = length xs * length ys" + "length(allpairs f xs ys) = length xs * length ys" by(induct xs) auto lemma length_0_conv [iff]: "(length xs = 0) = (xs = [])" @@ -685,7 +685,7 @@ by (induct xs) auto lemma set_allpairs[simp]: - "set(allpairs xs ys) = {(x,y). x : set xs & y : set ys}" + "set(allpairs f xs ys) = {z. EX x : set xs. EX y : set ys. z = f x y}" by(induct xs) auto lemma set_filter [simp]: "set (filter P xs) = {x. x : set xs \ P x}" @@ -2222,7 +2222,7 @@ subsubsection {* @{const allpairs} *} lemma allpairs_append: - "allpairs (xs @ ys) zs = allpairs xs zs @ allpairs ys zs" + "allpairs f (xs @ ys) zs = allpairs f xs zs @ allpairs f ys zs" by(induct xs) auto