author | wenzelm |

Thu Jan 11 19:37:46 2001 +0100 (2001-01-11) | |

changeset 10870 | 9444e3cf37e1 |

parent 10869 | 904cefa2c3cd |

child 10871 | 0ff9caa810b1 |

added strict_prefixI', strict_prefixE';

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