# HG changeset patch # User Christian Sternagel # Date 1346204771 -32400 # Node ID 919e393510f48de7533c81cbb8299c78c194d570 # Parent 398e8fddabb0190b64b486136080d50796ed5dd8 renamed (in Sublist): postfix ~> suffixeq, and dropped infix syntax >>= diff -r 398e8fddabb0 -r 919e393510f4 src/HOL/Library/Sublist.thy --- a/src/HOL/Library/Sublist.thy Wed Aug 29 10:35:05 2012 +0900 +++ b/src/HOL/Library/Sublist.thy Wed Aug 29 10:46:11 2012 +0900 @@ -2,7 +2,7 @@ Author: Tobias Nipkow and Markus Wenzel, TU Muenchen *) -header {* List prefixes and postfixes *} +header {* List prefixes, suffixes, and embedding*} theory Sublist imports List Main @@ -259,60 +259,60 @@ unfolding parallel_def by auto -subsection {* Postfix order on lists *} +subsection {* Suffix order on lists *} definition - postfix :: "'a list => 'a list => bool" ("(_/ >>= _)" [51, 50] 50) where - "(xs >>= ys) = (\zs. xs = zs @ ys)" + suffixeq :: "'a list => 'a list => bool" where + "suffixeq xs ys = (\zs. xs = zs @ ys)" -lemma postfixI [intro?]: "xs = zs @ ys ==> xs >>= ys" - unfolding postfix_def by blast +lemma suffixeqI [intro?]: "xs = zs @ ys ==> suffixeq xs ys" + unfolding suffixeq_def by blast -lemma postfixE [elim?]: - assumes "xs >>= ys" +lemma suffixeqE [elim?]: + assumes "suffixeq xs ys" obtains zs where "xs = zs @ ys" - using assms unfolding postfix_def by blast + using assms unfolding suffixeq_def by blast -lemma postfix_refl [iff]: "xs >>= xs" - by (auto simp add: postfix_def) -lemma postfix_trans: "\xs >>= ys; ys >>= zs\ \ xs >>= zs" - by (auto simp add: postfix_def) -lemma postfix_antisym: "\xs >>= ys; ys >>= xs\ \ xs = ys" - by (auto simp add: postfix_def) +lemma suffixeq_refl [iff]: "suffixeq xs xs" + by (auto simp add: suffixeq_def) +lemma suffixeq_trans: "\suffixeq xs ys; suffixeq ys zs\ \ suffixeq xs zs" + by (auto simp add: suffixeq_def) +lemma suffixeq_antisym: "\suffixeq xs ys; suffixeq ys xs\ \ xs = ys" + by (auto simp add: suffixeq_def) -lemma Nil_postfix [iff]: "xs >>= []" - by (simp add: postfix_def) -lemma postfix_Nil [simp]: "([] >>= xs) = (xs = [])" - by (auto simp add: postfix_def) +lemma Nil_suffixeq [iff]: "suffixeq xs []" + by (simp add: suffixeq_def) +lemma suffixeq_Nil [simp]: "(suffixeq [] xs) = (xs = [])" + by (auto simp add: suffixeq_def) -lemma postfix_ConsI: "xs >>= ys \ x#xs >>= ys" - by (auto simp add: postfix_def) -lemma postfix_ConsD: "xs >>= y#ys \ xs >>= ys" - by (auto simp add: postfix_def) +lemma suffixeq_ConsI: "suffixeq xs ys \ suffixeq (x#xs) ys" + by (auto simp add: suffixeq_def) +lemma suffixeq_ConsD: "suffixeq xs (y#ys) \ suffixeq xs ys" + by (auto simp add: suffixeq_def) -lemma postfix_appendI: "xs >>= ys \ zs @ xs >>= ys" - by (auto simp add: postfix_def) -lemma postfix_appendD: "xs >>= zs @ ys \ xs >>= ys" - by (auto simp add: postfix_def) +lemma suffixeq_appendI: "suffixeq xs ys \ suffixeq (zs @ xs) ys" + by (auto simp add: suffixeq_def) +lemma suffixeq_appendD: "suffixeq xs (zs @ ys) \ suffixeq xs ys" + by (auto simp add: suffixeq_def) -lemma postfix_is_subset: "xs >>= ys ==> set ys \ set xs" +lemma suffixeq_is_subset: "suffixeq xs ys ==> set ys \ set xs" proof - - assume "xs >>= ys" + assume "suffixeq xs ys" then obtain zs where "xs = zs @ ys" .. then show ?thesis by (induct zs) auto qed -lemma postfix_ConsD2: "x#xs >>= y#ys ==> xs >>= ys" +lemma suffixeq_ConsD2: "suffixeq (x#xs) (y#ys) ==> suffixeq xs ys" proof - - assume "x#xs >>= y#ys" + assume "suffixeq (x#xs) (y#ys)" then obtain zs where "x#xs = zs @ y#ys" .. then show ?thesis - by (induct zs) (auto intro!: postfix_appendI postfix_ConsI) + by (induct zs) (auto intro!: suffixeq_appendI suffixeq_ConsI) qed -lemma postfix_to_prefixeq [code]: "xs >>= ys \ rev ys \ rev xs" +lemma suffixeq_to_prefixeq [code]: "suffixeq xs ys \ rev ys \ rev xs" proof - assume "xs >>= ys" + assume "suffixeq xs ys" then obtain zs where "xs = zs @ ys" .. then have "rev xs = rev ys @ rev zs" by simp then show "rev ys <= rev xs" .. @@ -321,23 +321,23 @@ then obtain zs where "rev xs = rev ys @ zs" .. then have "rev (rev xs) = rev zs @ rev (rev ys)" by simp then have "xs = rev zs @ ys" by simp - then show "xs >>= ys" .. + then show "suffixeq xs ys" .. qed -lemma distinct_postfix: "distinct xs \ xs >>= ys \ distinct ys" - by (clarsimp elim!: postfixE) +lemma distinct_suffixeq: "distinct xs \ suffixeq xs ys \ distinct ys" + by (clarsimp elim!: suffixeqE) -lemma postfix_map: "xs >>= ys \ map f xs >>= map f ys" - by (auto elim!: postfixE intro: postfixI) +lemma suffixeq_map: "suffixeq xs ys \ suffixeq (map f xs) (map f ys)" + by (auto elim!: suffixeqE intro: suffixeqI) -lemma postfix_drop: "as >>= drop n as" - unfolding postfix_def +lemma suffixeq_drop: "suffixeq as (drop n as)" + unfolding suffixeq_def apply (rule exI [where x = "take n as"]) apply simp done -lemma postfix_take: "xs >>= ys \ xs = take (length xs - length ys) xs @ ys" - by (clarsimp elim!: postfixE) +lemma suffixeq_take: "suffixeq xs ys \ xs = take (length xs - length ys) xs @ ys" + by (clarsimp elim!: suffixeqE) lemma parallelD1: "x \ y \ \ x \ y" by blast