summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Fri, 15 Feb 2008 17:36:21 +0100 | |

changeset 26073 | 0e70d3bd2eb4 |

parent 26072 | f65a7fa2da6c |

child 26074 | 44c5419cd9f1 |

more lemmas

src/HOL/List.thy | file | annotate | diff | comparison | revisions |

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