# HG changeset patch
# User nipkow
# Date 1203093381 -3600
# Node ID 0e70d3bd2eb4a494fae8106e017dc6e1974bdd1b
# Parent  f65a7fa2da6c7286f84654b2121a9b8275031ed5
more lemmas

diff -r f65a7fa2da6c -r 0e70d3bd2eb4 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Feb 15 16:09:12 2008 +0100
+++ b/src/HOL/List.thy	Fri Feb 15 17:36:21 2008 +0100
@@ -827,58 +827,125 @@
 apply (erule ssubst, auto)
 done
 
-lemma in_set_conv_decomp: "(x : set xs) = (\<exists>ys zs. xs = ys @ x # zs)"
-proof (induct xs)
-  case Nil show ?case by simp
-next
-  case (Cons a xs)
-  show ?case
-  proof 
-    assume "x \<in> set (a # xs)"
-    with Cons show "\<exists>ys zs. a # xs = ys @ x # zs"
-      by (auto intro: Cons_eq_appendI)
-  next
-    assume "\<exists>ys zs. a # xs = ys @ x # zs"
-    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
 
 lemma split_list: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs"
-  by (rule in_set_conv_decomp [THEN iffD1])
-
-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
+  case Nil thus ?case by simp
+next
+  case Cons thus ?case by (auto intro: Cons_eq_appendI)
+qed
+
+lemma in_set_conv_decomp: "(x : set xs) = (\<exists>ys zs. xs = ys @ x # zs)"
+by (metis Un_upper2 insert_subset set.simps(2) set_append split_list)
+
+lemma split_list_first: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set ys"
+proof (induct xs)
+  case Nil thus ?case by simp
 next
   case (Cons a xs)
   show ?case
   proof cases
     assume "x = a" thus ?case using Cons by fastsimp
   next
-    assume "x \<noteq> a"
-    show ?case
-    proof
-      assume "x \<in> set (a # xs)"
-      with Cons and `x \<noteq> a` 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
+    assume "x \<noteq> a" thus ?case using Cons by(fastsimp intro!: Cons_eq_appendI)
+  qed
+qed
+
+lemma in_set_conv_decomp_first:
+  "(x : set xs) = (\<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set ys)"
+by (metis in_set_conv_decomp split_list_first)
+
+lemma split_list_last: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set zs"
+proof (induct xs rule:rev_induct)
+  case Nil thus ?case by simp
+next
+  case (snoc a xs)
+  show ?case
+  proof cases
+    assume "x = a" thus ?case using snoc by simp (metis ex_in_conv set_empty2)
+  next
+    assume "x \<noteq> a" thus ?case using snoc by fastsimp
   qed
 qed
 
-lemma split_list_first: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set ys"
-  by (rule in_set_conv_decomp_first [THEN iffD1])
-
-
-lemma finite_list: "finite A ==> EX l. set l = A"
+lemma in_set_conv_decomp_last:
+  "(x : set xs) = (\<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set zs)"
+by (metis in_set_conv_decomp split_list_last)
+
+lemma split_list_prop: "\<exists>x \<in> set xs. P x \<Longrightarrow> \<exists>ys x zs. xs = ys @ x # zs & P x"
+proof (induct xs)
+  case Nil thus ?case by simp
+next
+  case Cons thus ?case
+    by(simp add:Bex_def)(metis append_Cons append.simps(1))
+qed
+
+lemma split_list_propE:
+assumes "\<exists>x \<in> set xs. P x"
+obtains ys x zs where "xs = ys @ x # zs" and "P x"
+by(metis split_list_prop[OF assms])
+
+
+lemma split_list_first_prop:
+  "\<exists>x \<in> set xs. P x \<Longrightarrow>
+   \<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>y \<in> set ys. \<not> P y)"
+proof(induct xs)
+  case Nil thus ?case by simp
+next
+  case (Cons x xs)
+  show ?case
+  proof cases
+    assume "P x"
+    thus ?thesis by simp (metis Un_upper1 contra_subsetD in_set_conv_decomp_first self_append_conv2 set_append)
+  next
+    assume "\<not> P x"
+    hence "\<exists>x\<in>set xs. P x" using Cons(2) by simp
+    thus ?thesis using `\<not> P x` Cons(1) by (metis append_Cons set_ConsD)
+  qed
+qed
+
+lemma split_list_first_propE:
+assumes "\<exists>x \<in> set xs. P x"
+obtains ys x zs where "xs = ys @ x # zs" and "P x" and "\<forall>y \<in> set ys. \<not> P y"
+by(metis split_list_first_prop[OF assms])
+
+lemma split_list_first_prop_iff:
+  "(\<exists>x \<in> set xs. P x) \<longleftrightarrow>
+   (\<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>y \<in> set ys. \<not> P y))"
+by(metis split_list_first_prop[where P=P] in_set_conv_decomp)
+
+
+lemma split_list_last_prop:
+  "\<exists>x \<in> set xs. P x \<Longrightarrow>
+   \<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>z \<in> set zs. \<not> P z)"
+proof(induct xs rule:rev_induct)
+  case Nil thus ?case by simp
+next
+  case (snoc x xs)
+  show ?case
+  proof cases
+    assume "P x" thus ?thesis by (metis emptyE set_empty)
+  next
+    assume "\<not> P x"
+    hence "\<exists>x\<in>set xs. P x" using snoc(2) by simp
+    thus ?thesis using `\<not> P x` snoc(1) by fastsimp
+  qed
+qed
+
+lemma split_list_last_propE:
+assumes "\<exists>x \<in> set xs. P x"
+obtains ys x zs where "xs = ys @ x # zs" and "P x" and "\<forall>z \<in> set zs. \<not> P z"
+by(metis split_list_last_prop[OF assms])
+
+lemma split_list_last_prop_iff:
+  "(\<exists>x \<in> set xs. P x) \<longleftrightarrow>
+   (\<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>z \<in> set zs. \<not> P z))"
+by(metis split_list_last_prop[where P=P] in_set_conv_decomp)
+
+
+lemma finite_list: "finite A ==> EX xs. set xs = A"
 apply (erule finite_induct, auto)
-apply (rule_tac x="x#l" in exI, auto)
+apply (metis set.simps(2))
 done
 
 lemma card_length: "card (set xs) \<le> length xs"