author nipkow Mon, 31 Oct 2005 01:43:22 +0100 changeset 18049 156bba334c12 parent 18048 7003308ff73a child 18050 652c95961a8b
A few new lemmas
 src/HOL/List.thy file | annotate | diff | comparison | revisions src/HOL/Relation_Power.thy file | annotate | diff | comparison | revisions
```--- 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"

+lemma rotate1_rotate_swap: "rotate1 (rotate n xs) = rotate n (rotate1 xs)"
+
lemma rotate1_length01[simp]: "length xs <= 1 \<Longrightarrow> rotate1 xs = xs"
by(cases xs) simp_all
```
```--- a/src/HOL/Relation_Power.thy	Sun Oct 30 10:55:56 2005 +0100
+++ b/src/HOL/Relation_Power.thy	Mon Oct 31 01:43:22 2005 +0100
@@ -38,6 +38,14 @@
lemma funpow_add: "f ^ (m+n) = f^m o f^n"
by(induct m) simp_all

+lemma funpow_swap1: "f((f^n) x) = (f^n)(f x)"
+proof -
+  have "f((f^n) x) = (f^(n+1)) x" by simp
+  also have "\<dots>  = (f^n o f^1) x" by (simp only:funpow_add)
+  also have "\<dots> = (f^n)(f x)" by simp
+  finally show ?thesis .
+qed
+
lemma rel_pow_1: "!!R:: ('a*'a)set. R^1 = R"
by simp
declare rel_pow_1 [simp]```