src/HOL/List.thy
 changeset 18049 156bba334c12 parent 17956 369e2af8ee45 child 18336 1a2e30b37ed3
```--- a/src/HOL/List.thy	Sun Oct 30 10:55:56 2005 +0100
+++ b/src/HOL/List.thy	Mon Oct 31 01:43:22 2005 +0100
@@ -683,6 +683,34 @@
qed
qed

+lemma in_set_conv_decomp_first:
+ "(x : set xs) = (\<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set ys)"
+proof (induct xs)
+  case Nil show ?case by simp
+next
+  case (Cons a xs)
+  show ?case
+  proof cases
+    assume "x = a" thus ?case using Cons by force
+  next
+    assume "x \<noteq> a"
+    show ?case
+    proof
+      assume "x \<in> set (a # xs)"
+      from prems show "\<exists>ys zs. a # xs = ys @ x # zs \<and> x \<notin> set ys"
+	by(fastsimp intro!: Cons_eq_appendI)
+    next
+      assume "\<exists>ys zs. a # xs = ys @ x # zs \<and> x \<notin> set ys"
+      then obtain ys zs where eq: "a # xs = ys @ x # zs" by blast
+      show "x \<in> set (a # xs)" by (cases ys, auto simp add: eq)
+    qed
+  qed
+qed
+
+lemmas split_list       = in_set_conv_decomp[THEN iffD1, standard]
+lemmas split_list_first = in_set_conv_decomp_first[THEN iffD1, standard]
+
+
lemma finite_list: "finite A ==> EX l. set l = A"
apply (erule finite_induct, auto)
apply (rule_tac x="x#l" in exI, auto)
@@ -878,6 +906,16 @@
apply (case_tac n, auto)
done

+
+lemma list_eq_iff_nth_eq:
+ "!!ys. (xs = ys) = (length xs = length ys \<and> (ALL i<length xs. xs!i = ys!i))"
+apply(induct xs)
+ apply simp apply blast
+apply(case_tac ys)
+ apply simp
+done
+
lemma set_conv_nth: "set xs = {xs!i | i. i < length xs}"
apply (induct xs, simp, simp)
apply safe
@@ -1789,6 +1827,11 @@

subsubsection {* @{text remove1} *}

+lemma remove1_append:
+  "remove1 x (xs @ ys) =
+  (if x \<in> set xs then remove1 x xs @ ys else xs @ remove1 x ys)"
+by (induct xs) auto
+
lemma set_remove1_subset: "set(remove1 x xs) <= set xs"
apply(induct xs)
apply simp
@@ -1803,6 +1846,10 @@
apply blast
done

+lemma remove1_filter_not[simp]:
+  "\<not> P x \<Longrightarrow> remove1 x (filter P xs) = filter P xs"
+by(induct xs) auto
+
lemma notin_set_remove1[simp]: "x ~: set xs ==> x ~: set(remove1 y xs)"
apply(insert set_remove1_subset)
apply fast
@@ -1905,6 +1952,9 @@
lemma rotate_rotate: "rotate m (rotate n xs) = rotate (m+n) xs"