author Christian Sternagel Wed Aug 29 11:05:44 2012 +0900 (2012-08-29) changeset 49082 d71cdd1171c3 parent 49081 092668a120cc child 49083 01081bca31b6
more lemmas on suffixes and embedding
```     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.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
```