author | nipkow |

Wed May 25 17:40:56 2016 +0200 (2016-05-25) | |

changeset 63149 | f5dbab18c404 |

parent 63144 | 76130b7cc450 |

child 63150 | dbb176f511c5 |

renamed suffix(eq)

NEWS | file | annotate | diff | revisions | |

src/HOL/Library/Sublist.thy | file | annotate | diff | revisions |

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