# HG changeset patch
# User nipkow
# Date 1080629139 -7200
# Node ID e2a1c31cf6d33af478db86d08c1bce5fb03dfb01
# Parent  48ae8d678d886d3fe950382ee14345ac77b6a734
Added append_eq_append_conv2

diff -r 48ae8d678d88 -r e2a1c31cf6d3 src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Mar 29 15:35:04 2004 +0200
+++ b/src/HOL/List.thy	Tue Mar 30 08:45:39 2004 +0200
@@ -331,6 +331,16 @@
 apply (case_tac ys, force, simp)
 done
 
+lemma append_eq_append_conv2: "!!ys zs ts.
+ (xs @ ys = zs @ ts) =
+ (EX us. xs = zs @ us & us @ ys = ts | xs @ us = zs & ys = us@ ts)"
+apply (induct xs)
+ apply fastsimp
+apply(case_tac zs)
+ apply simp
+apply fastsimp
+done
+
 lemma same_append_eq [iff]: "(xs @ ys = xs @ zs) = (ys = zs)"
 by simp