# 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