# 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 \<Rightarrow> 'a list \<Rightarrow> 'a list"
-  allpairs :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a * 'b)list"
+  allpairs :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> '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 \<and> 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