author | Christian Sternagel |

Wed Aug 29 10:57:24 2012 +0900 (2012-08-29) | |

changeset 49081 | 092668a120cc |

parent 49080 | f60ed8769a9d |

child 49082 | d71cdd1171c3 |

changed arguement order of suffixeq (to facilitate reading "suffixeq xs ys" as "xs is a (possibly empty) suffix of ys)

1.1 --- a/src/HOL/Library/Sublist.thy Wed Aug 29 10:48:28 2012 +0900 1.2 +++ b/src/HOL/Library/Sublist.thy Wed Aug 29 10:57:24 2012 +0900 1.3 @@ -263,14 +263,14 @@ 1.4 1.5 definition 1.6 suffixeq :: "'a list => 'a list => bool" where 1.7 - "suffixeq xs ys = (\<exists>zs. xs = zs @ ys)" 1.8 + "suffixeq xs ys = (\<exists>zs. ys = zs @ xs)" 1.9 1.10 -lemma suffixeqI [intro?]: "xs = zs @ ys ==> suffixeq xs ys" 1.11 +lemma suffixeqI [intro?]: "ys = zs @ xs ==> suffixeq xs ys" 1.12 unfolding suffixeq_def by blast 1.13 1.14 lemma suffixeqE [elim?]: 1.15 assumes "suffixeq xs ys" 1.16 - obtains zs where "xs = zs @ ys" 1.17 + obtains zs where "ys = zs @ xs" 1.18 using assms unfolding suffixeq_def by blast 1.19 1.20 lemma suffixeq_refl [iff]: "suffixeq xs xs" 1.21 @@ -280,63 +280,63 @@ 1.22 lemma suffixeq_antisym: "\<lbrakk>suffixeq xs ys; suffixeq ys xs\<rbrakk> \<Longrightarrow> xs = ys" 1.23 by (auto simp add: suffixeq_def) 1.24 1.25 -lemma Nil_suffixeq [iff]: "suffixeq xs []" 1.26 +lemma Nil_suffixeq [iff]: "suffixeq [] xs" 1.27 by (simp add: suffixeq_def) 1.28 -lemma suffixeq_Nil [simp]: "(suffixeq [] xs) = (xs = [])" 1.29 +lemma suffixeq_Nil [simp]: "(suffixeq xs []) = (xs = [])" 1.30 by (auto simp add: suffixeq_def) 1.31 1.32 -lemma suffixeq_ConsI: "suffixeq xs ys \<Longrightarrow> suffixeq (x#xs) ys" 1.33 +lemma suffixeq_ConsI: "suffixeq xs ys \<Longrightarrow> suffixeq xs (y#ys)" 1.34 by (auto simp add: suffixeq_def) 1.35 -lemma suffixeq_ConsD: "suffixeq xs (y#ys) \<Longrightarrow> suffixeq xs ys" 1.36 +lemma suffixeq_ConsD: "suffixeq (x#xs) ys \<Longrightarrow> suffixeq xs ys" 1.37 by (auto simp add: suffixeq_def) 1.38 1.39 -lemma suffixeq_appendI: "suffixeq xs ys \<Longrightarrow> suffixeq (zs @ xs) ys" 1.40 +lemma suffixeq_appendI: "suffixeq xs ys \<Longrightarrow> suffixeq xs (zs @ ys)" 1.41 by (auto simp add: suffixeq_def) 1.42 -lemma suffixeq_appendD: "suffixeq xs (zs @ ys) \<Longrightarrow> suffixeq xs ys" 1.43 +lemma suffixeq_appendD: "suffixeq (zs @ xs) ys \<Longrightarrow> suffixeq xs ys" 1.44 by (auto simp add: suffixeq_def) 1.45 1.46 -lemma suffixeq_is_subset: "suffixeq xs ys ==> set ys \<subseteq> set xs" 1.47 +lemma suffixeq_is_subset: "suffixeq xs ys ==> set xs \<subseteq> set ys" 1.48 proof - 1.49 assume "suffixeq xs ys" 1.50 - then obtain zs where "xs = zs @ ys" .. 1.51 + then obtain zs where "ys = zs @ xs" .. 1.52 then show ?thesis by (induct zs) auto 1.53 qed 1.54 1.55 lemma suffixeq_ConsD2: "suffixeq (x#xs) (y#ys) ==> suffixeq xs ys" 1.56 proof - 1.57 assume "suffixeq (x#xs) (y#ys)" 1.58 - then obtain zs where "x#xs = zs @ y#ys" .. 1.59 + then obtain zs where "y#ys = zs @ x#xs" .. 1.60 then show ?thesis 1.61 by (induct zs) (auto intro!: suffixeq_appendI suffixeq_ConsI) 1.62 qed 1.63 1.64 -lemma suffixeq_to_prefixeq [code]: "suffixeq xs ys \<longleftrightarrow> rev ys \<le> rev xs" 1.65 +lemma suffixeq_to_prefixeq [code]: "suffixeq xs ys \<longleftrightarrow> rev xs \<le> rev ys" 1.66 proof 1.67 assume "suffixeq xs ys" 1.68 - then obtain zs where "xs = zs @ ys" .. 1.69 - then have "rev xs = rev ys @ rev zs" by simp 1.70 - then show "rev ys <= rev xs" .. 1.71 + then obtain zs where "ys = zs @ xs" .. 1.72 + then have "rev ys = rev xs @ rev zs" by simp 1.73 + then show "rev xs <= rev ys" .. 1.74 next 1.75 - assume "rev ys <= rev xs" 1.76 - then obtain zs where "rev xs = rev ys @ zs" .. 1.77 - then have "rev (rev xs) = rev zs @ rev (rev ys)" by simp 1.78 - then have "xs = rev zs @ ys" by simp 1.79 + assume "rev xs <= rev ys" 1.80 + then obtain zs where "rev ys = rev xs @ zs" .. 1.81 + then have "rev (rev ys) = rev zs @ rev (rev xs)" by simp 1.82 + then have "ys = rev zs @ xs" by simp 1.83 then show "suffixeq xs ys" .. 1.84 qed 1.85 1.86 -lemma distinct_suffixeq: "distinct xs \<Longrightarrow> suffixeq xs ys \<Longrightarrow> distinct ys" 1.87 +lemma distinct_suffixeq: "distinct ys \<Longrightarrow> suffixeq xs ys \<Longrightarrow> distinct xs" 1.88 by (clarsimp elim!: suffixeqE) 1.89 1.90 lemma suffixeq_map: "suffixeq xs ys \<Longrightarrow> suffixeq (map f xs) (map f ys)" 1.91 by (auto elim!: suffixeqE intro: suffixeqI) 1.92 1.93 -lemma suffixeq_drop: "suffixeq as (drop n as)" 1.94 +lemma suffixeq_drop: "suffixeq (drop n as) as" 1.95 unfolding suffixeq_def 1.96 apply (rule exI [where x = "take n as"]) 1.97 apply simp 1.98 done 1.99 1.100 -lemma suffixeq_take: "suffixeq xs ys \<Longrightarrow> xs = take (length xs - length ys) xs @ ys" 1.101 +lemma suffixeq_take: "suffixeq xs ys \<Longrightarrow> ys = take (length ys - length xs) ys @ xs" 1.102 by (clarsimp elim!: suffixeqE) 1.103 1.104 lemma parallelD1: "x \<parallel> y \<Longrightarrow> \<not> x \<le> y"