--- a/src/HOL/List.thy Wed Sep 22 11:46:28 2010 +0200
+++ b/src/HOL/List.thy Wed Sep 22 16:52:09 2010 +0200
@@ -4157,8 +4157,8 @@
lists :: "'a set => 'a list set"
for A :: "'a set"
where
- Nil [intro!]: "[]: lists A"
- | Cons [intro!,no_atp]: "[| a: A; l: lists A|] ==> a#l : lists A"
+ Nil [intro!, simp]: "[]: lists A"
+ | Cons [intro!, simp, no_atp]: "[| a: A; l: lists A|] ==> a#l : lists A"
inductive_cases listsE [elim!,no_atp]: "x#l : lists A"
inductive_cases listspE [elim!,no_atp]: "listsp A (x # l)"
@@ -4184,6 +4184,9 @@
lemmas lists_Int_eq [simp] = listsp_inf_eq [to_set pred_equals_eq]
+lemma Cons_in_lists_iff[simp]: "x#xs : lists A \<longleftrightarrow> x:A \<and> xs : lists A"
+by auto
+
lemma append_in_listsp_conv [iff]:
"(listsp A (xs @ ys)) = (listsp A xs \<and> listsp A ys)"
by (induct xs) auto
@@ -4209,6 +4212,9 @@
lemma lists_eq_set: "lists A = {xs. set xs <= A}"
by auto
+lemma lists_empty [simp]: "lists {} = {[]}"
+by auto
+
lemma lists_UNIV [simp]: "lists UNIV = UNIV"
by auto