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.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"
```