renamed suffix(eq)
authornipkow
Wed May 25 17:40:56 2016 +0200 (2016-05-25)
changeset 63149f5dbab18c404
parent 63144 76130b7cc450
child 63150 dbb176f511c5
renamed suffix(eq)
NEWS
src/HOL/Library/Sublist.thy
     1.1 --- a/NEWS	Wed May 25 12:24:00 2016 +0200
     1.2 +++ b/NEWS	Wed May 25 17:40:56 2016 +0200
     1.3 @@ -214,7 +214,11 @@
     1.4  pave way for a possible future different type class instantiation
     1.5  for polynomials over factorial rings.  INCOMPATIBILITY.
     1.6  
     1.7 -* Library/Sublist.thy: renamed prefixeq -> prefix and prefix -> strict_prefix
     1.8 +* Library/Sublist.thy: renamed
     1.9 + prefixeq -> prefix
    1.10 + prefix -> strict_prefix
    1.11 + suffixeq -> suffix
    1.12 + suffix -> strict_suffix
    1.13  
    1.14  * Dropped various legacy fact bindings, whose replacements are often
    1.15  of a more general type also:
     2.1 --- a/src/HOL/Library/Sublist.thy	Wed May 25 12:24:00 2016 +0200
     2.2 +++ b/src/HOL/Library/Sublist.thy	Wed May 25 17:40:56 2016 +0200
     2.3 @@ -264,72 +264,79 @@
     2.4  
     2.5  subsection \<open>Suffix order on lists\<close>
     2.6  
     2.7 -definition suffixeq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
     2.8 -  where "suffixeq xs ys = (\<exists>zs. ys = zs @ xs)"
     2.9 +definition suffix :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
    2.10 +  where "suffix xs ys = (\<exists>zs. ys = zs @ xs)"
    2.11  
    2.12 -definition suffix :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
    2.13 -  where "suffix xs ys \<longleftrightarrow> (\<exists>us. ys = us @ xs \<and> us \<noteq> [])"
    2.14 +definition strict_suffix :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
    2.15 +  where "strict_suffix xs ys \<longleftrightarrow> (\<exists>us. ys = us @ xs \<and> us \<noteq> [])"
    2.16  
    2.17 -lemma suffix_imp_suffixeq:
    2.18 -  "suffix xs ys \<Longrightarrow> suffixeq xs ys"
    2.19 -  by (auto simp: suffixeq_def suffix_def)
    2.20 +lemma strict_suffix_imp_suffix:
    2.21 +  "strict_suffix xs ys \<Longrightarrow> suffix xs ys"
    2.22 +  by (auto simp: suffix_def strict_suffix_def)
    2.23  
    2.24 -lemma suffixeqI [intro?]: "ys = zs @ xs \<Longrightarrow> suffixeq xs ys"
    2.25 -  unfolding suffixeq_def by blast
    2.26 +lemma suffixI [intro?]: "ys = zs @ xs \<Longrightarrow> suffix xs ys"
    2.27 +  unfolding suffix_def by blast
    2.28  
    2.29 -lemma suffixeqE [elim?]:
    2.30 -  assumes "suffixeq xs ys"
    2.31 +lemma suffixE [elim?]:
    2.32 +  assumes "suffix xs ys"
    2.33    obtains zs where "ys = zs @ xs"
    2.34 -  using assms unfolding suffixeq_def by blast
    2.35 +  using assms unfolding suffix_def by blast
    2.36  
    2.37 -lemma suffixeq_refl [iff]: "suffixeq xs xs"
    2.38 -  by (auto simp add: suffixeq_def)
    2.39 +lemma suffix_refl [iff]: "suffix xs xs"
    2.40 +  by (auto simp add: suffix_def)
    2.41 +
    2.42  lemma suffix_trans:
    2.43    "suffix xs ys \<Longrightarrow> suffix ys zs \<Longrightarrow> suffix xs zs"
    2.44    by (auto simp: suffix_def)
    2.45 -lemma suffixeq_trans: "\<lbrakk>suffixeq xs ys; suffixeq ys zs\<rbrakk> \<Longrightarrow> suffixeq xs zs"
    2.46 -  by (auto simp add: suffixeq_def)
    2.47 -lemma suffixeq_antisym: "\<lbrakk>suffixeq xs ys; suffixeq ys xs\<rbrakk> \<Longrightarrow> xs = ys"
    2.48 -  by (auto simp add: suffixeq_def)
    2.49 +
    2.50 +lemma strict_suffix_trans:
    2.51 +  "\<lbrakk>strict_suffix xs ys; strict_suffix ys zs\<rbrakk> \<Longrightarrow> strict_suffix xs zs"
    2.52 +by (auto simp add: strict_suffix_def)
    2.53  
    2.54 -lemma suffixeq_tl [simp]: "suffixeq (tl xs) xs"
    2.55 -  by (induct xs) (auto simp: suffixeq_def)
    2.56 +lemma suffix_antisym: "\<lbrakk>suffix xs ys; suffix ys xs\<rbrakk> \<Longrightarrow> xs = ys"
    2.57 +  by (auto simp add: suffix_def)
    2.58  
    2.59 -lemma suffix_tl [simp]: "xs \<noteq> [] \<Longrightarrow> suffix (tl xs) xs"
    2.60 +lemma suffix_tl [simp]: "suffix (tl xs) xs"
    2.61    by (induct xs) (auto simp: suffix_def)
    2.62  
    2.63 -lemma Nil_suffixeq [iff]: "suffixeq [] xs"
    2.64 -  by (simp add: suffixeq_def)
    2.65 -lemma suffixeq_Nil [simp]: "(suffixeq xs []) = (xs = [])"
    2.66 -  by (auto simp add: suffixeq_def)
    2.67 +lemma strict_suffix_tl [simp]: "xs \<noteq> [] \<Longrightarrow> strict_suffix (tl xs) xs"
    2.68 +  by (induct xs) (auto simp: strict_suffix_def)
    2.69 +
    2.70 +lemma Nil_suffix [iff]: "suffix [] xs"
    2.71 +  by (simp add: suffix_def)
    2.72  
    2.73 -lemma suffixeq_ConsI: "suffixeq xs ys \<Longrightarrow> suffixeq xs (y # ys)"
    2.74 -  by (auto simp add: suffixeq_def)
    2.75 -lemma suffixeq_ConsD: "suffixeq (x # xs) ys \<Longrightarrow> suffixeq xs ys"
    2.76 -  by (auto simp add: suffixeq_def)
    2.77 +lemma suffix_Nil [simp]: "(suffix xs []) = (xs = [])"
    2.78 +  by (auto simp add: suffix_def)
    2.79 +
    2.80 +lemma suffix_ConsI: "suffix xs ys \<Longrightarrow> suffix xs (y # ys)"
    2.81 +  by (auto simp add: suffix_def)
    2.82 +
    2.83 +lemma suffix_ConsD: "suffix (x # xs) ys \<Longrightarrow> suffix xs ys"
    2.84 +  by (auto simp add: suffix_def)
    2.85  
    2.86 -lemma suffixeq_appendI: "suffixeq xs ys \<Longrightarrow> suffixeq xs (zs @ ys)"
    2.87 -  by (auto simp add: suffixeq_def)
    2.88 -lemma suffixeq_appendD: "suffixeq (zs @ xs) ys \<Longrightarrow> suffixeq xs ys"
    2.89 -  by (auto simp add: suffixeq_def)
    2.90 +lemma suffix_appendI: "suffix xs ys \<Longrightarrow> suffix xs (zs @ ys)"
    2.91 +  by (auto simp add: suffix_def)
    2.92 +
    2.93 +lemma suffix_appendD: "suffix (zs @ xs) ys \<Longrightarrow> suffix xs ys"
    2.94 +  by (auto simp add: suffix_def)
    2.95  
    2.96 -lemma suffix_set_subset:
    2.97 -  "suffix xs ys \<Longrightarrow> set xs \<subseteq> set ys" by (auto simp: suffix_def)
    2.98 +lemma strict_suffix_set_subset: "strict_suffix xs ys \<Longrightarrow> set xs \<subseteq> set ys"
    2.99 +by (auto simp: strict_suffix_def)
   2.100  
   2.101 -lemma suffixeq_set_subset:
   2.102 -  "suffixeq xs ys \<Longrightarrow> set xs \<subseteq> set ys" by (auto simp: suffixeq_def)
   2.103 +lemma suffix_set_subset: "suffix xs ys \<Longrightarrow> set xs \<subseteq> set ys"
   2.104 +by (auto simp: suffix_def)
   2.105  
   2.106 -lemma suffixeq_ConsD2: "suffixeq (x # xs) (y # ys) \<Longrightarrow> suffixeq xs ys"
   2.107 +lemma suffix_ConsD2: "suffix (x # xs) (y # ys) \<Longrightarrow> suffix xs ys"
   2.108  proof -
   2.109 -  assume "suffixeq (x # xs) (y # ys)"
   2.110 +  assume "suffix (x # xs) (y # ys)"
   2.111    then obtain zs where "y # ys = zs @ x # xs" ..
   2.112    then show ?thesis
   2.113 -    by (induct zs) (auto intro!: suffixeq_appendI suffixeq_ConsI)
   2.114 +    by (induct zs) (auto intro!: suffix_appendI suffix_ConsI)
   2.115  qed
   2.116  
   2.117 -lemma suffixeq_to_prefix [code]: "suffixeq xs ys \<longleftrightarrow> prefix (rev xs) (rev ys)"
   2.118 +lemma suffix_to_prefix [code]: "suffix xs ys \<longleftrightarrow> prefix (rev xs) (rev ys)"
   2.119  proof
   2.120 -  assume "suffixeq xs ys"
   2.121 +  assume "suffix xs ys"
   2.122    then obtain zs where "ys = zs @ xs" ..
   2.123    then have "rev ys = rev xs @ rev zs" by simp
   2.124    then show "prefix (rev xs) (rev ys)" ..
   2.125 @@ -338,46 +345,29 @@
   2.126    then obtain zs where "rev ys = rev xs @ zs" ..
   2.127    then have "rev (rev ys) = rev zs @ rev (rev xs)" by simp
   2.128    then have "ys = rev zs @ xs" by simp
   2.129 -  then show "suffixeq xs ys" ..
   2.130 +  then show "suffix xs ys" ..
   2.131  qed
   2.132  
   2.133 -lemma distinct_suffixeq: "distinct ys \<Longrightarrow> suffixeq xs ys \<Longrightarrow> distinct xs"
   2.134 -  by (clarsimp elim!: suffixeqE)
   2.135 +lemma distinct_suffix: "distinct ys \<Longrightarrow> suffix xs ys \<Longrightarrow> distinct xs"
   2.136 +  by (clarsimp elim!: suffixE)
   2.137  
   2.138 -lemma suffixeq_map: "suffixeq xs ys \<Longrightarrow> suffixeq (map f xs) (map f ys)"
   2.139 -  by (auto elim!: suffixeqE intro: suffixeqI)
   2.140 +lemma suffix_map: "suffix xs ys \<Longrightarrow> suffix (map f xs) (map f ys)"
   2.141 +  by (auto elim!: suffixE intro: suffixI)
   2.142  
   2.143 -lemma suffixeq_drop: "suffixeq (drop n as) as"
   2.144 -  unfolding suffixeq_def
   2.145 +lemma suffix_drop: "suffix (drop n as) as"
   2.146 +  unfolding suffix_def
   2.147    apply (rule exI [where x = "take n as"])
   2.148    apply simp
   2.149    done
   2.150  
   2.151 -lemma suffixeq_take: "suffixeq xs ys \<Longrightarrow> ys = take (length ys - length xs) ys @ xs"
   2.152 -  by (auto elim!: suffixeqE)
   2.153 +lemma suffix_take: "suffix xs ys \<Longrightarrow> ys = take (length ys - length xs) ys @ xs"
   2.154 +  by (auto elim!: suffixE)
   2.155  
   2.156 -lemma suffixeq_suffix_reflclp_conv: "suffixeq = suffix\<^sup>=\<^sup>="
   2.157 -proof (intro ext iffI)
   2.158 -  fix xs ys :: "'a list"
   2.159 -  assume "suffixeq xs ys"
   2.160 -  show "suffix\<^sup>=\<^sup>= xs ys"
   2.161 -  proof
   2.162 -    assume "xs \<noteq> ys"
   2.163 -    with \<open>suffixeq xs ys\<close> show "suffix xs ys"
   2.164 -      by (auto simp: suffixeq_def suffix_def)
   2.165 -  qed
   2.166 -next
   2.167 -  fix xs ys :: "'a list"
   2.168 -  assume "suffix\<^sup>=\<^sup>= xs ys"
   2.169 -  then show "suffixeq xs ys"
   2.170 -  proof
   2.171 -    assume "suffix xs ys" then show "suffixeq xs ys"
   2.172 -      by (rule suffix_imp_suffixeq)
   2.173 -  next
   2.174 -    assume "xs = ys" then show "suffixeq xs ys"
   2.175 -      by (auto simp: suffixeq_def)
   2.176 -  qed
   2.177 -qed
   2.178 +lemma strict_suffix_reflclp_conv: "strict_suffix\<^sup>=\<^sup>= = suffix"
   2.179 +by (intro ext) (auto simp: suffix_def strict_suffix_def)
   2.180 +
   2.181 +lemma suffix_lists: "suffix xs ys \<Longrightarrow> ys \<in> lists A \<Longrightarrow> xs \<in> lists A"
   2.182 +  unfolding suffix_def by auto
   2.183  
   2.184  lemma parallelD1: "x \<parallel> y \<Longrightarrow> \<not> prefix x y"
   2.185    by blast
   2.186 @@ -419,12 +409,6 @@
   2.187    qed
   2.188  qed
   2.189  
   2.190 -lemma suffix_reflclp_conv: "suffix\<^sup>=\<^sup>= = suffixeq"
   2.191 -  by (intro ext) (auto simp: suffixeq_def suffix_def)
   2.192 -
   2.193 -lemma suffix_lists: "suffix xs ys \<Longrightarrow> ys \<in> lists A \<Longrightarrow> xs \<in> lists A"
   2.194 -  unfolding suffix_def by auto
   2.195 -
   2.196  
   2.197  subsection \<open>Homeomorphic embedding on lists\<close>
   2.198  
   2.199 @@ -500,15 +484,16 @@
   2.200    thus ?case using lh zs sk by (metis (no_types) append_Cons append_assoc)
   2.201  qed
   2.202  
   2.203 +lemma list_emb_strict_suffix:
   2.204 +  assumes "list_emb P xs ys" and "strict_suffix ys zs"
   2.205 +  shows "list_emb P xs zs"
   2.206 +  using assms(2) and list_emb_append2 [OF assms(1)] by (auto simp: strict_suffix_def)
   2.207 +
   2.208  lemma list_emb_suffix:
   2.209    assumes "list_emb P xs ys" and "suffix ys zs"
   2.210    shows "list_emb P xs zs"
   2.211 -  using assms(2) and list_emb_append2 [OF assms(1)] by (auto simp: suffix_def)
   2.212 -
   2.213 -lemma list_emb_suffixeq:
   2.214 -  assumes "list_emb P xs ys" and "suffixeq ys zs"
   2.215 -  shows "list_emb P xs zs"
   2.216 -  using assms and list_emb_suffix unfolding suffixeq_suffix_reflclp_conv by auto
   2.217 +using assms and list_emb_strict_suffix
   2.218 +unfolding strict_suffix_reflclp_conv[symmetric] by auto
   2.219  
   2.220  lemma list_emb_length: "list_emb P xs ys \<Longrightarrow> length xs \<le> length ys"
   2.221    by (induct rule: list_emb.induct) auto