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))"