changed arguement order of suffixeq (to facilitate reading "suffixeq xs ys" as "xs is a (possibly empty) suffix of ys)
authorChristian Sternagel
Wed Aug 29 10:57:24 2012 +0900 (2012-08-29)
changeset 49081092668a120cc
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)
src/HOL/Library/Sublist.thy
     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"