added allpairs
authornipkow
Mon Apr 30 22:43:33 2007 +0200 (2007-04-30)
changeset 228282064f0fd20c9
parent 22827 7dc27b37f7f7
child 22829 f1db55c7534d
added allpairs
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Mon Apr 30 13:33:00 2007 +0200
     1.2 +++ b/src/HOL/List.thy	Mon Apr 30 22:43:33 2007 +0200
     1.3 @@ -42,6 +42,7 @@
     1.4    "distinct":: "'a list => bool"
     1.5    replicate :: "nat => 'a => 'a list"
     1.6    splice :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
     1.7 +  allpairs :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a * 'b)list"
     1.8  
     1.9  abbreviation
    1.10    upto:: "nat => nat => nat list"  ("(1[_../_])") where
    1.11 @@ -209,6 +210,9 @@
    1.12    "splice (x#xs) ys = (if ys=[] then x#xs else x # hd ys # splice xs (tl ys))"
    1.13      -- {*Warning: simpset does not contain the second eqn but a derived one. *}
    1.14  
    1.15 +primrec
    1.16 +"allpairs [] ys = []"
    1.17 +"allpairs (x # xs) ys = map (Pair x) ys @ allpairs xs ys"
    1.18  
    1.19  subsubsection {* @{const Nil} and @{const Cons} *}
    1.20  
    1.21 @@ -245,6 +249,10 @@
    1.22  lemma length_tl [simp]: "length (tl xs) = length xs - 1"
    1.23  by (cases xs) auto
    1.24  
    1.25 +lemma length_allpairs[simp]:
    1.26 + "length(allpairs xs ys) = length xs * length ys"
    1.27 +by(induct xs) auto
    1.28 +
    1.29  lemma length_0_conv [iff]: "(length xs = 0) = (xs = [])"
    1.30  by (induct xs) auto
    1.31  
    1.32 @@ -676,6 +684,10 @@
    1.33  lemma set_map [simp]: "set (map f xs) = f`(set xs)"
    1.34  by (induct xs) auto
    1.35  
    1.36 +lemma set_allpairs[simp]:
    1.37 + "set(allpairs xs ys) = {(x,y). x : set xs & y : set ys}"
    1.38 +by(induct xs) auto
    1.39 +
    1.40  lemma set_filter [simp]: "set (filter P xs) = {x. x : set xs \<and> P x}"
    1.41  by (induct xs) auto
    1.42  
    1.43 @@ -2206,6 +2218,14 @@
    1.44   apply auto
    1.45  done
    1.46  
    1.47 +
    1.48 +subsubsection {* @{const allpairs} *}
    1.49 +
    1.50 +lemma allpairs_append:
    1.51 + "allpairs (xs @ ys) zs = allpairs xs zs @ allpairs ys zs"
    1.52 +by(induct xs) auto
    1.53 +
    1.54 +
    1.55  subsubsection{*Sets of Lists*}
    1.56  
    1.57  subsubsection {* @{text lists}: the list-forming operator over sets *}