src/HOL/Library/List_Prefix.thy
changeset 14300 bf8b8c9425c3
parent 12338 de0f4a63baa5
child 14538 1d9d75a8efae
     1.1 --- a/src/HOL/Library/List_Prefix.thy	Wed Dec 17 16:23:52 2003 +0100
     1.2 +++ b/src/HOL/Library/List_Prefix.thy	Thu Dec 18 08:20:36 2003 +0100
     1.3 @@ -106,6 +106,9 @@
     1.4    thus ?thesis ..
     1.5  qed
     1.6  
     1.7 +lemma append_prefixD: "xs @ ys \<le> zs \<Longrightarrow> xs \<le> zs"
     1.8 +by(simp add:prefix_def) blast
     1.9 +
    1.10  theorem prefix_Cons: "(xs \<le> y # ys) = (xs = [] \<or> (\<exists>zs. xs = y # zs \<and> zs \<le> ys))"
    1.11    by (cases xs) (auto simp add: prefix_def)
    1.12  
    1.13 @@ -130,6 +133,29 @@
    1.14    by (auto simp add: prefix_def)
    1.15  
    1.16  
    1.17 +lemma prefix_same_cases:
    1.18 + "\<lbrakk> (xs\<^isub>1::'a list) \<le> ys; xs\<^isub>2 \<le> ys \<rbrakk> \<Longrightarrow> xs\<^isub>1 \<le> xs\<^isub>2 \<or> xs\<^isub>2 \<le> xs\<^isub>1"
    1.19 +apply(simp add:prefix_def)
    1.20 +apply(erule exE)+
    1.21 +apply(simp add: append_eq_append_conv_if split:if_splits)
    1.22 + apply(rule disjI2)
    1.23 + apply(rule_tac x = "drop (size xs\<^isub>2) xs\<^isub>1" in exI)
    1.24 + apply clarify
    1.25 + apply(drule sym)
    1.26 + apply(insert append_take_drop_id[of "length xs\<^isub>2" xs\<^isub>1])
    1.27 + apply simp
    1.28 +apply(rule disjI1)
    1.29 +apply(rule_tac x = "drop (size xs\<^isub>1) xs\<^isub>2" in exI)
    1.30 +apply clarify
    1.31 +apply(insert append_take_drop_id[of "length xs\<^isub>1" xs\<^isub>2])
    1.32 +apply simp
    1.33 +done
    1.34 +
    1.35 +lemma set_mono_prefix:
    1.36 + "xs \<le> ys \<Longrightarrow> set xs \<subseteq> set ys"
    1.37 +by(fastsimp simp add:prefix_def)
    1.38 +
    1.39 +
    1.40  subsection {* Parallel lists *}
    1.41  
    1.42  constdefs