# HG changeset patch
# User nipkow
# Date 1130719402 -3600
# Node ID 156bba334c123ae06f78bcba934414fee5535666
# Parent  7003308ff73a9f71186e951432b9823e72e8f0fa
A few new lemmas

diff -r 7003308ff73a -r 156bba334c12 src/HOL/List.thy
--- 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
+apply(simp add:nth_Cons split:nat.split)apply blast
+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"
 by(simp add:rotate_add)
 
+lemma rotate1_rotate_swap: "rotate1 (rotate n xs) = rotate n (rotate1 xs)"
+by(simp add:rotate_def funpow_swap1)
+
 lemma rotate1_length01[simp]: "length xs <= 1 \<Longrightarrow> rotate1 xs = xs"
 by(cases xs) simp_all
 
diff -r 7003308ff73a -r 156bba334c12 src/HOL/Relation_Power.thy
--- 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]