# HG changeset patch
# User wenzelm
# Date 979238266 -3600
# Node ID 9444e3cf37e11e5bffabe2996e6fd0e80d203d4d
# Parent  904cefa2c3cdbfe7a1c060e5f9971e397fc981a7
added strict_prefixI', strict_prefixE';

diff -r 904cefa2c3cd -r 9444e3cf37e1 src/HOL/Library/List_Prefix.thy
--- a/src/HOL/Library/List_Prefix.thy	Thu Jan 11 19:36:25 2001 +0100
+++ b/src/HOL/Library/List_Prefix.thy	Thu Jan 11 19:37:46 2001 +0100
@@ -27,6 +27,19 @@
 lemma prefixE [elim?]: "xs \<le> ys ==> (!!zs. ys = xs @ zs ==> C) ==> C"
   by (unfold prefix_def) blast
 
+lemma strict_prefixI' [intro?]: "ys = xs @ z # zs ==> xs < ys"
+  by (unfold strict_prefix_def prefix_def) blast
+
+lemma strict_prefixE' [elim?]:
+    "xs < ys ==> (!!z zs. ys = xs @ z # zs ==> C) ==> C"
+proof -
+  assume r: "!!z zs. ys = xs @ z # zs ==> C"
+  assume "xs < ys"
+  then obtain us where "ys = xs @ us" and "xs \<noteq> ys"
+    by (unfold strict_prefix_def prefix_def) blast
+  with r show ?thesis by (auto simp add: neq_Nil_conv)
+qed
+
 lemma strict_prefixI [intro?]: "xs \<le> ys ==> xs \<noteq> ys ==> xs < (ys::'a list)"
   by (unfold strict_prefix_def) blast