summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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