1.1 --- a/src/HOL/List.thy	Mon Aug 30 14:56:20 2004 +0200
     1.2 +++ b/src/HOL/List.thy	Wed Sep 01 15:03:41 2004 +0200
     1.3 @@ -223,9 +223,9 @@
     1.4  
     1.5  consts lists :: "'a set => 'a list set"
     1.6  inductive "lists A"
     1.7 -intros
     1.8 -Nil [intro!]: "[]: lists A"
     1.9 -Cons [intro!]: "[| a: A;l: lists A|] ==> a#l : lists A"
    1.10 + intros
    1.11 +  Nil [intro!]: "[]: lists A"
    1.12 +  Cons [intro!]: "[| a: A;l: lists A|] ==> a#l : lists A"
    1.13  
    1.14  inductive_cases listsE [elim!]: "x#l : lists A"
    1.15  
    1.16 @@ -648,6 +648,9 @@
    1.17  lemma in_listsI [intro!]: "\<forall>x\<in>set xs. x \<in> A ==> xs \<in> lists A"
    1.18  by (rule in_lists_conv_set [THEN iffD2])
    1.19  
    1.20 +lemma lists_UNIV [simp]: "lists UNIV = UNIV"
    1.21 +by auto
    1.22 +
    1.23  lemma finite_list: "finite A ==> EX l. set l = A"
    1.24  apply (erule finite_induct, auto)
    1.25  apply (rule_tac x="x#l" in exI, auto)
    1.26 @@ -656,6 +659,26 @@
    1.27  lemma card_length: "card (set xs) \<le> length xs"
    1.28  by (induct xs) (auto simp add: card_insert_if)
    1.29  
    1.30 +
    1.31 +subsection{*Sets of Lists*}
    1.32 +
    1.33 +text{*Resembles a Cartesian product: it denotes the set of lists with head
    1.34 +  drawn from @{term A} and tail drawn from @{term Xs}.*}
    1.35 +constdefs
    1.36 +  set_Cons :: "'a set \<Rightarrow> 'a list set \<Rightarrow> 'a list set"
    1.37 +   "set_Cons A XS == {z. \<exists>x xs. z = x#xs & x \<in> A & xs \<in> XS}"
    1.38 +
    1.39 +lemma [simp]: "set_Cons A {[]} = (%x. [x])`A"
    1.40 +by (auto simp add: set_Cons_def)
    1.41 +
    1.42 +text{*Yields the set of lists, all of the same length as the argument and
    1.43 +with elements drawn from the corresponding element of the argument.*}
    1.44 +consts  listset :: "'a set list \<Rightarrow> 'a list set"
    1.45 +primrec
    1.46 +   "listset []    = {[]}"
    1.47 +   "listset(A#As) = set_Cons A (listset As)"
    1.48 +
    1.49 +
    1.50  subsection {* @{text mem} *}
    1.51  
    1.52  lemma set_mem_eq: "(x mem xs) = (x : set xs)"
    1.53 @@ -1556,7 +1579,7 @@
    1.54  done
    1.55  
    1.56  lemma lexn_length:
    1.57 -"!!xs ys. (xs, ys) : lexn r n ==> length xs = n \<and> length ys = n"
    1.58 +     "!!xs ys. (xs, ys) : lexn r n ==> length xs = n \<and> length ys = n"
    1.59  by (induct n) auto
    1.60  
    1.61  lemma wf_lex [intro!]: "wf r ==> wf (lex r)"
    1.62 @@ -1619,12 +1642,12 @@
    1.63  by (auto simp add: sublist_def)
    1.64  
    1.65  lemma sublist_shift_lemma:
    1.66 -"map fst [p:zip xs [i..i + length xs(] . snd p : A] =
    1.67 -map fst [p:zip xs [0..length xs(] . snd p + i : A]"
    1.68 +     "map fst [p:zip xs [i..i + length xs(] . snd p : A] =
    1.69 +      map fst [p:zip xs [0..length xs(] . snd p + i : A]"
    1.70  by (induct xs rule: rev_induct) (simp_all add: add_commute)
    1.71  
    1.72  lemma sublist_append:
    1.73 -"sublist (l @ l') A = sublist l A @ sublist l' {j. j + length l : A}"
    1.74 +     "sublist (l @ l') A = sublist l A @ sublist l' {j. j + length l : A}"
    1.75  apply (unfold sublist_def)
    1.76  apply (induct l' rule: rev_induct, simp)
    1.77  apply (simp add: upt_add_eq_append[of 0] zip_append sublist_shift_lemma)
    1.78 @@ -1648,11 +1671,11 @@
    1.79  
    1.80  
    1.81  lemma take_Cons':
    1.82 -"take n (x # xs) = (if n = 0 then [] else x # take (n - 1) xs)"
    1.83 +     "take n (x # xs) = (if n = 0 then [] else x # take (n - 1) xs)"
    1.84  by (cases n) simp_all
    1.85  
    1.86  lemma drop_Cons':
    1.87 -"drop n (x # xs) = (if n = 0 then x # xs else drop (n - 1) xs)"
    1.88 +     "drop n (x # xs) = (if n = 0 then x # xs else drop (n - 1) xs)"
    1.89  by (cases n) simp_all
    1.90  
    1.91  lemma nth_Cons': "(x # xs)!n = (if n = 0 then x else xs!(n - 1))"