src/HOL/Library/List_Prefix.thy
changeset 10870 9444e3cf37e1
parent 10512 d34192966cd8
child 11780 d17ee2241257
     1.1 --- a/src/HOL/Library/List_Prefix.thy	Thu Jan 11 19:36:25 2001 +0100
     1.2 +++ b/src/HOL/Library/List_Prefix.thy	Thu Jan 11 19:37:46 2001 +0100
     1.3 @@ -27,6 +27,19 @@
     1.4  lemma prefixE [elim?]: "xs \<le> ys ==> (!!zs. ys = xs @ zs ==> C) ==> C"
     1.5    by (unfold prefix_def) blast
     1.6  
     1.7 +lemma strict_prefixI' [intro?]: "ys = xs @ z # zs ==> xs < ys"
     1.8 +  by (unfold strict_prefix_def prefix_def) blast
     1.9 +
    1.10 +lemma strict_prefixE' [elim?]:
    1.11 +    "xs < ys ==> (!!z zs. ys = xs @ z # zs ==> C) ==> C"
    1.12 +proof -
    1.13 +  assume r: "!!z zs. ys = xs @ z # zs ==> C"
    1.14 +  assume "xs < ys"
    1.15 +  then obtain us where "ys = xs @ us" and "xs \<noteq> ys"
    1.16 +    by (unfold strict_prefix_def prefix_def) blast
    1.17 +  with r show ?thesis by (auto simp add: neq_Nil_conv)
    1.18 +qed
    1.19 +
    1.20  lemma strict_prefixI [intro?]: "xs \<le> ys ==> xs \<noteq> ys ==> xs < (ys::'a list)"
    1.21    by (unfold strict_prefix_def) blast
    1.22