# HG changeset patch
# User nipkow
# Date 1187601487 -7200
# Node ID 21b4350cf5ec3098e26f7961b6a40896387a4571
# Parent  22863f364531cf534a62e0d54b2e3942a80a3652
removed allpairs - use list comprehension!

diff -r 22863f364531 -r 21b4350cf5ec src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Aug 20 04:44:35 2007 +0200
+++ b/src/HOL/List.thy	Mon Aug 20 11:18:07 2007 +0200
@@ -44,7 +44,6 @@
   "distinct":: "'a list => bool"
   replicate :: "nat => 'a => 'a list"
   splice :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
-  allpairs :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list"
 
 abbreviation
   upto:: "nat => nat => nat list"  ("(1[_../_])") where
@@ -221,10 +220,6 @@
   "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 f [] ys = []"
-"allpairs f (x # xs) ys = map (f x) ys @ allpairs f xs ys"
-
 subsubsection {* List comprehension *}
 
 text{* Input syntax for Haskell-like list comprehension
@@ -326,10 +321,6 @@
 lemma length_tl [simp]: "length (tl xs) = length xs - 1"
 by (cases xs) auto
 
-lemma length_allpairs[simp]:
- "length(allpairs f xs ys) = length xs * length ys"
-by(induct xs) auto
-
 lemma length_0_conv [iff]: "(length xs = 0) = (xs = [])"
 by (induct xs) auto
 
@@ -757,10 +748,6 @@
 lemma set_map [simp]: "set (map f xs) = f`(set xs)"
 by (induct xs) auto
 
-lemma set_allpairs [simp]:
- "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}"
 by (induct xs) auto
 
@@ -2371,16 +2358,6 @@
  apply auto
 done
 
-subsubsection {* @{const allpairs} *}
-
-lemma allpairs_conv_concat:
- "allpairs f xs ys = concat(map (%x. map (f x) ys) xs)"
-by(induct xs) auto
-
-lemma allpairs_append:
- "allpairs f (xs @ ys) zs = allpairs f xs zs @ allpairs f ys zs"
-by(induct xs) auto
-
 subsubsection {* @{text lists}: the list-forming operator over sets *}
 
 inductive_set