src/HOL/List.thy

--- a/src/HOL/List.thy	Mon Apr 30 13:33:00 2007 +0200
+++ b/src/HOL/List.thy	Mon Apr 30 22:43:33 2007 +0200
@@ -42,6 +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"
 
 abbreviation
   upto:: "nat => nat => nat list"  ("(1[_../_])") where
@@ -209,6 +210,9 @@
   "splice (x#xs) ys = (if ys=[] then x#xs else x # hd ys # splice xs (tl ys))"
     -- {*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"
 
 subsubsection {* @{const Nil} and @{const Cons} *}
 
@@ -245,6 +249,10 @@
 lemma length_tl [simp]: "length (tl xs) = length xs - 1"
 by (cases xs) auto
 
+lemma length_allpairs[simp]:
+ "length(allpairs xs ys) = length xs * length ys"
+by(induct xs) auto
+
 lemma length_0_conv [iff]: "(length xs = 0) = (xs = [])"
 by (induct xs) auto
 
@@ -676,6 +684,10 @@
 lemma set_map [simp]: "set (map f xs) = f`(set xs)"
 by (induct xs) auto
 
+lemma set_allpairs[simp]:
+ "set(allpairs xs ys) = {(x,y). x : set xs & y : set ys}"
+by(induct xs) auto
+
 lemma set_filter [simp]: "set (filter P xs) = {x. x : set xs \<and> P x}"
 by (induct xs) auto
 
@@ -2206,6 +2218,14 @@
  apply auto
 done
 
+
+subsubsection {* @{const allpairs} *}
+
+lemma allpairs_append:
+ "allpairs (xs @ ys) zs = allpairs xs zs @ allpairs ys zs"
+by(induct xs) auto
+
+
 subsubsection{*Sets of Lists*}
 
 subsubsection {* @{text lists}: the list-forming operator over sets *}