# HG changeset patch
# User bulwahn
# Date 1288941394 -3600
# Node ID a1456f2e1c9da2417c4354346db28b04fe2ff0cc
# Parent  55a1693affb6f29e04a276ede86a6b5568ec13ca
added two lemmas about injectivity of concat to the list theory

diff -r 55a1693affb6 -r a1456f2e1c9d src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Nov 05 08:16:31 2010 +0100
+++ b/src/HOL/List.thy	Fri Nov 05 08:16:34 2010 +0100
@@ -1298,6 +1298,15 @@
 lemma rev_concat: "rev (concat xs) = concat (map rev (rev xs))"
 by (induct xs) auto
 
+lemma concat_eq_concat_iff: "\<forall>(x, y) \<in> set (zip xs ys). length x = length y ==> length xs = length ys ==> (concat xs = concat ys) = (xs = ys)"
+proof (induct xs arbitrary: ys)
+  case (Cons x xs ys)
+  thus ?case by (cases ys) auto
+qed (auto)
+
+lemma concat_injective: "concat xs = concat ys ==> length xs = length ys ==> \<forall>(x, y) \<in> set (zip xs ys). length x = length y ==> xs = ys"
+by (simp add: concat_eq_concat_iff)
+
 
 subsubsection {* @{text nth} *}