more lemmas on suffixes and embedding
authorChristian Sternagel
Wed Aug 29 11:05:44 2012 +0900 (2012-08-29)
changeset 49082d71cdd1171c3
parent 49081 092668a120cc
child 49083 01081bca31b6
more lemmas on suffixes and embedding
src/HOL/Library/Sublist.thy
     1.1 --- a/src/HOL/Library/Sublist.thy	Wed Aug 29 10:57:24 2012 +0900
     1.2 +++ b/src/HOL/Library/Sublist.thy	Wed Aug 29 11:05:44 2012 +0900
     1.3 @@ -265,6 +265,13 @@
     1.4    suffixeq :: "'a list => 'a list => bool" where
     1.5    "suffixeq xs ys = (\<exists>zs. ys = zs @ xs)"
     1.6  
     1.7 +definition suffix :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
     1.8 +  "suffix xs ys \<equiv> \<exists>us. ys = us @ xs \<and> us \<noteq> []"
     1.9 +
    1.10 +lemma suffix_imp_suffixeq:
    1.11 +  "suffix xs ys \<Longrightarrow> suffixeq xs ys"
    1.12 +  by (auto simp: suffixeq_def suffix_def)
    1.13 +
    1.14  lemma suffixeqI [intro?]: "ys = zs @ xs ==> suffixeq xs ys"
    1.15    unfolding suffixeq_def by blast
    1.16  
    1.17 @@ -275,11 +282,20 @@
    1.18  
    1.19  lemma suffixeq_refl [iff]: "suffixeq xs xs"
    1.20    by (auto simp add: suffixeq_def)
    1.21 +lemma suffix_trans:
    1.22 +  "suffix xs ys \<Longrightarrow> suffix ys zs \<Longrightarrow> suffix xs zs"
    1.23 +  by (auto simp: suffix_def)
    1.24  lemma suffixeq_trans: "\<lbrakk>suffixeq xs ys; suffixeq ys zs\<rbrakk> \<Longrightarrow> suffixeq xs zs"
    1.25    by (auto simp add: suffixeq_def)
    1.26  lemma suffixeq_antisym: "\<lbrakk>suffixeq xs ys; suffixeq ys xs\<rbrakk> \<Longrightarrow> xs = ys"
    1.27    by (auto simp add: suffixeq_def)
    1.28  
    1.29 +lemma suffixeq_tl [simp]: "suffixeq (tl xs) xs"
    1.30 +  by (induct xs) (auto simp: suffixeq_def)
    1.31 +
    1.32 +lemma suffix_tl [simp]: "xs \<noteq> [] \<Longrightarrow> suffix (tl xs) xs"
    1.33 +  by (induct xs) (auto simp: suffix_def)
    1.34 +
    1.35  lemma Nil_suffixeq [iff]: "suffixeq [] xs"
    1.36    by (simp add: suffixeq_def)
    1.37  lemma suffixeq_Nil [simp]: "(suffixeq xs []) = (xs = [])"
    1.38 @@ -295,12 +311,11 @@
    1.39  lemma suffixeq_appendD: "suffixeq (zs @ xs) ys \<Longrightarrow> suffixeq xs ys"
    1.40    by (auto simp add: suffixeq_def)
    1.41  
    1.42 -lemma suffixeq_is_subset: "suffixeq xs ys ==> set xs \<subseteq> set ys"
    1.43 -proof -
    1.44 -  assume "suffixeq xs ys"
    1.45 -  then obtain zs where "ys = zs @ xs" ..
    1.46 -  then show ?thesis by (induct zs) auto
    1.47 -qed
    1.48 +lemma suffix_set_subset:
    1.49 +  "suffix xs ys \<Longrightarrow> set xs \<subseteq> set ys" by (auto simp: suffix_def)
    1.50 +
    1.51 +lemma suffixeq_set_subset:
    1.52 +  "suffixeq xs ys \<Longrightarrow> set xs \<subseteq> set ys" by (auto simp: suffixeq_def)
    1.53  
    1.54  lemma suffixeq_ConsD2: "suffixeq (x#xs) (y#ys) ==> suffixeq xs ys"
    1.55  proof -
    1.56 @@ -339,6 +354,27 @@
    1.57  lemma suffixeq_take: "suffixeq xs ys \<Longrightarrow> ys = take (length ys - length xs) ys @ xs"
    1.58    by (clarsimp elim!: suffixeqE)
    1.59  
    1.60 +lemma suffixeq_suffix_reflclp_conv:
    1.61 +  "suffixeq = suffix\<^sup>=\<^sup>="
    1.62 +proof (intro ext iffI)
    1.63 +  fix xs ys :: "'a list"
    1.64 +  assume "suffixeq xs ys"
    1.65 +  show "suffix\<^sup>=\<^sup>= xs ys"
    1.66 +  proof
    1.67 +    assume "xs \<noteq> ys"
    1.68 +    with `suffixeq xs ys` show "suffix xs ys" by (auto simp: suffixeq_def suffix_def)
    1.69 +  qed
    1.70 +next
    1.71 +  fix xs ys :: "'a list"
    1.72 +  assume "suffix\<^sup>=\<^sup>= xs ys"
    1.73 +  thus "suffixeq xs ys"
    1.74 +  proof
    1.75 +    assume "suffix xs ys" thus "suffixeq xs ys" by (rule suffix_imp_suffixeq)
    1.76 +  next
    1.77 +    assume "xs = ys" thus "suffixeq xs ys" by (auto simp: suffixeq_def)
    1.78 +  qed
    1.79 +qed
    1.80 +
    1.81  lemma parallelD1: "x \<parallel> y \<Longrightarrow> \<not> x \<le> y"
    1.82    by blast
    1.83  
    1.84 @@ -379,6 +415,14 @@
    1.85    qed
    1.86  qed
    1.87  
    1.88 +lemma suffix_reflclp_conv:
    1.89 +  "suffix\<^sup>=\<^sup>= = suffixeq"
    1.90 +  by (intro ext) (auto simp: suffixeq_def suffix_def)
    1.91 +
    1.92 +lemma suffix_lists:
    1.93 +  "suffix xs ys \<Longrightarrow> ys \<in> lists A \<Longrightarrow> xs \<in> lists A"
    1.94 +  unfolding suffix_def by auto
    1.95 +
    1.96  
    1.97  subsection {* Embedding on lists *}
    1.98  
    1.99 @@ -427,4 +471,14 @@
   1.100    with Cons show ?case by (metis append_Cons append_assoc emb_Cons2 emb_append2)
   1.101  qed
   1.102  
   1.103 +lemma emb_suffix:
   1.104 +  assumes "emb P xs ys" and "suffix ys zs"
   1.105 +  shows "emb P xs zs"
   1.106 +  using assms(2) and emb_append2 [OF assms(1)] by (auto simp: suffix_def)
   1.107 +
   1.108 +lemma emb_suffixeq:
   1.109 +  assumes "emb P xs ys" and "suffixeq ys zs"
   1.110 +  shows "emb P xs zs"
   1.111 +  using assms and emb_suffix unfolding suffixeq_suffix_reflclp_conv by auto
   1.112 +
   1.113  end