src/HOL/List.thy
changeset 14300 bf8b8c9425c3
parent 14247 cb32eb89bddd
child 14302 6c24235e8d5d
--- a/src/HOL/List.thy	Wed Dec 17 16:23:52 2003 +0100
+++ b/src/HOL/List.thy	Thu Dec 18 08:20:36 2003 +0100
@@ -362,6 +362,11 @@
 by (simp add: tl_append split: list.split)
 
 
+lemma Cons_eq_append_conv: "x#xs = ys@zs =
+ (ys = [] & x#xs = zs | (EX ys'. x#ys' = ys & xs = ys'@zs))"
+by(cases ys) auto
+
+
 text {* Trivial rules for solving @{text "@"}-equations automatically. *}
 
 lemma eq_Nil_appendI: "xs = ys ==> xs = [] @ ys"
@@ -902,6 +907,17 @@
 apply (case_tac i, simp_all) 
 done
 
+lemma append_eq_append_conv_if:
+ "!! ys\<^isub>1. (xs\<^isub>1 @ xs\<^isub>2 = ys\<^isub>1 @ ys\<^isub>2) =
+  (if size xs\<^isub>1 \<le> size ys\<^isub>1
+   then xs\<^isub>1 = take (size xs\<^isub>1) ys\<^isub>1 \<and> xs\<^isub>2 = drop (size xs\<^isub>1) ys\<^isub>1 @ ys\<^isub>2
+   else take (size ys\<^isub>1) xs\<^isub>1 = ys\<^isub>1 \<and> drop (size ys\<^isub>1) xs\<^isub>1 @ xs\<^isub>2 = ys\<^isub>2)"
+apply(induct xs\<^isub>1)
+ apply simp
+apply(case_tac ys\<^isub>1)
+apply simp_all
+done
+
 
 subsection {* @{text takeWhile} and @{text dropWhile} *}