# 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: "\(x, y) \ 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 ==> \(x, y) \ set (zip xs ys). length x = length y ==> xs = ys" +by (simp add: concat_eq_concat_iff) + subsubsection {* @{text nth} *}