# HG changeset patch
# User paulson
# Date 1094043821 -7200
# Node ID 33a08cfc3ae5639086167af0ef184ce751a41205
# Parent  67f9c38557150d1f72a6411d6176a518971ddbe5
new functions for sets of lists

diff -r 67f9c3855715 -r 33a08cfc3ae5 src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Aug 30 14:56:20 2004 +0200
+++ b/src/HOL/List.thy	Wed Sep 01 15:03:41 2004 +0200
@@ -223,9 +223,9 @@
 
 consts lists :: "'a set => 'a list set"
 inductive "lists A"
-intros
-Nil [intro!]: "[]: lists A"
-Cons [intro!]: "[| a: A;l: lists A|] ==> a#l : lists A"
+ intros
+  Nil [intro!]: "[]: lists A"
+  Cons [intro!]: "[| a: A;l: lists A|] ==> a#l : lists A"
 
 inductive_cases listsE [elim!]: "x#l : lists A"
 
@@ -648,6 +648,9 @@
 lemma in_listsI [intro!]: "\<forall>x\<in>set xs. x \<in> A ==> xs \<in> lists A"
 by (rule in_lists_conv_set [THEN iffD2])
 
+lemma lists_UNIV [simp]: "lists UNIV = UNIV"
+by auto
+
 lemma finite_list: "finite A ==> EX l. set l = A"
 apply (erule finite_induct, auto)
 apply (rule_tac x="x#l" in exI, auto)
@@ -656,6 +659,26 @@
 lemma card_length: "card (set xs) \<le> length xs"
 by (induct xs) (auto simp add: card_insert_if)
 
+
+subsection{*Sets of Lists*}
+
+text{*Resembles a Cartesian product: it denotes the set of lists with head
+  drawn from @{term A} and tail drawn from @{term Xs}.*}
+constdefs
+  set_Cons :: "'a set \<Rightarrow> 'a list set \<Rightarrow> 'a list set"
+   "set_Cons A XS == {z. \<exists>x xs. z = x#xs & x \<in> A & xs \<in> XS}"
+
+lemma [simp]: "set_Cons A {[]} = (%x. [x])`A"
+by (auto simp add: set_Cons_def)
+
+text{*Yields the set of lists, all of the same length as the argument and
+with elements drawn from the corresponding element of the argument.*}
+consts  listset :: "'a set list \<Rightarrow> 'a list set"
+primrec
+   "listset []    = {[]}"
+   "listset(A#As) = set_Cons A (listset As)"
+
+
 subsection {* @{text mem} *}
 
 lemma set_mem_eq: "(x mem xs) = (x : set xs)"
@@ -1556,7 +1579,7 @@
 done
 
 lemma lexn_length:
-"!!xs ys. (xs, ys) : lexn r n ==> length xs = n \<and> length ys = n"
+     "!!xs ys. (xs, ys) : lexn r n ==> length xs = n \<and> length ys = n"
 by (induct n) auto
 
 lemma wf_lex [intro!]: "wf r ==> wf (lex r)"
@@ -1619,12 +1642,12 @@
 by (auto simp add: sublist_def)
 
 lemma sublist_shift_lemma:
-"map fst [p:zip xs [i..i + length xs(] . snd p : A] =
-map fst [p:zip xs [0..length xs(] . snd p + i : A]"
+     "map fst [p:zip xs [i..i + length xs(] . snd p : A] =
+      map fst [p:zip xs [0..length xs(] . snd p + i : A]"
 by (induct xs rule: rev_induct) (simp_all add: add_commute)
 
 lemma sublist_append:
-"sublist (l @ l') A = sublist l A @ sublist l' {j. j + length l : A}"
+     "sublist (l @ l') A = sublist l A @ sublist l' {j. j + length l : A}"
 apply (unfold sublist_def)
 apply (induct l' rule: rev_induct, simp)
 apply (simp add: upt_add_eq_append[of 0] zip_append sublist_shift_lemma)
@@ -1648,11 +1671,11 @@
 
 
 lemma take_Cons':
-"take n (x # xs) = (if n = 0 then [] else x # take (n - 1) xs)"
+     "take n (x # xs) = (if n = 0 then [] else x # take (n - 1) xs)"
 by (cases n) simp_all
 
 lemma drop_Cons':
-"drop n (x # xs) = (if n = 0 then x # xs else drop (n - 1) xs)"
+     "drop n (x # xs) = (if n = 0 then x # xs else drop (n - 1) xs)"
 by (cases n) simp_all
 
 lemma nth_Cons': "(x # xs)!n = (if n = 0 then x else xs!(n - 1))"