# HG changeset patch
# User Christian Sternagel
# Date 1346205444 -32400
# Node ID 092668a120cc06f9005b514f0c6b2b5b7ce73aa2
# Parent f60ed8769a9d4f780a337455c47d1d3105cf3393
changed arguement order of suffixeq (to facilitate reading "suffixeq xs ys" as "xs is a (possibly empty) suffix of ys)
diff -r f60ed8769a9d -r 092668a120cc src/HOL/Library/Sublist.thy
--- a/src/HOL/Library/Sublist.thy Wed Aug 29 10:48:28 2012 +0900
+++ b/src/HOL/Library/Sublist.thy Wed Aug 29 10:57:24 2012 +0900
@@ -263,14 +263,14 @@
definition
suffixeq :: "'a list => 'a list => bool" where
- "suffixeq xs ys = (\zs. xs = zs @ ys)"
+ "suffixeq xs ys = (\zs. ys = zs @ xs)"
-lemma suffixeqI [intro?]: "xs = zs @ ys ==> suffixeq xs ys"
+lemma suffixeqI [intro?]: "ys = zs @ xs ==> suffixeq xs ys"
unfolding suffixeq_def by blast
lemma suffixeqE [elim?]:
assumes "suffixeq xs ys"
- obtains zs where "xs = zs @ ys"
+ obtains zs where "ys = zs @ xs"
using assms unfolding suffixeq_def by blast
lemma suffixeq_refl [iff]: "suffixeq xs xs"
@@ -280,63 +280,63 @@
lemma suffixeq_antisym: "\suffixeq xs ys; suffixeq ys xs\ \ xs = ys"
by (auto simp add: suffixeq_def)
-lemma Nil_suffixeq [iff]: "suffixeq xs []"
+lemma Nil_suffixeq [iff]: "suffixeq [] xs"
by (simp add: suffixeq_def)
-lemma suffixeq_Nil [simp]: "(suffixeq [] xs) = (xs = [])"
+lemma suffixeq_Nil [simp]: "(suffixeq xs []) = (xs = [])"
by (auto simp add: suffixeq_def)
-lemma suffixeq_ConsI: "suffixeq xs ys \ suffixeq (x#xs) ys"
+lemma suffixeq_ConsI: "suffixeq xs ys \ suffixeq xs (y#ys)"
by (auto simp add: suffixeq_def)
-lemma suffixeq_ConsD: "suffixeq xs (y#ys) \ suffixeq xs ys"
+lemma suffixeq_ConsD: "suffixeq (x#xs) ys \ suffixeq xs ys"
by (auto simp add: suffixeq_def)
-lemma suffixeq_appendI: "suffixeq xs ys \ suffixeq (zs @ xs) ys"
+lemma suffixeq_appendI: "suffixeq xs ys \ suffixeq xs (zs @ ys)"
by (auto simp add: suffixeq_def)
-lemma suffixeq_appendD: "suffixeq xs (zs @ ys) \ suffixeq xs ys"
+lemma suffixeq_appendD: "suffixeq (zs @ xs) ys \ suffixeq xs ys"
by (auto simp add: suffixeq_def)
-lemma suffixeq_is_subset: "suffixeq xs ys ==> set ys \ set xs"
+lemma suffixeq_is_subset: "suffixeq xs ys ==> set xs \ set ys"
proof -
assume "suffixeq xs ys"
- then obtain zs where "xs = zs @ ys" ..
+ then obtain zs where "ys = zs @ xs" ..
then show ?thesis by (induct zs) auto
qed
lemma suffixeq_ConsD2: "suffixeq (x#xs) (y#ys) ==> suffixeq xs ys"
proof -
assume "suffixeq (x#xs) (y#ys)"
- then obtain zs where "x#xs = zs @ y#ys" ..
+ then obtain zs where "y#ys = zs @ x#xs" ..
then show ?thesis
by (induct zs) (auto intro!: suffixeq_appendI suffixeq_ConsI)
qed
-lemma suffixeq_to_prefixeq [code]: "suffixeq xs ys \ rev ys \ rev xs"
+lemma suffixeq_to_prefixeq [code]: "suffixeq xs ys \ rev xs \ rev ys"
proof
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" ..
+ then obtain zs where "ys = zs @ xs" ..
+ then have "rev ys = rev xs @ rev zs" by simp
+ then show "rev xs <= rev ys" ..
next
- assume "rev ys <= rev xs"
- 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
+ assume "rev xs <= rev ys"
+ then obtain zs where "rev ys = rev xs @ zs" ..
+ then have "rev (rev ys) = rev zs @ rev (rev xs)" by simp
+ then have "ys = rev zs @ xs" by simp
then show "suffixeq xs ys" ..
qed
-lemma distinct_suffixeq: "distinct xs \ suffixeq xs ys \ distinct ys"
+lemma distinct_suffixeq: "distinct ys \ suffixeq xs ys \ distinct xs"
by (clarsimp elim!: suffixeqE)
lemma suffixeq_map: "suffixeq xs ys \ suffixeq (map f xs) (map f ys)"
by (auto elim!: suffixeqE intro: suffixeqI)
-lemma suffixeq_drop: "suffixeq as (drop n as)"
+lemma suffixeq_drop: "suffixeq (drop n as) as"
unfolding suffixeq_def
apply (rule exI [where x = "take n as"])
apply simp
done
-lemma suffixeq_take: "suffixeq xs ys \ xs = take (length xs - length ys) xs @ ys"
+lemma suffixeq_take: "suffixeq xs ys \ ys = take (length ys - length xs) ys @ xs"
by (clarsimp elim!: suffixeqE)
lemma parallelD1: "x \ y \ \ x \ y"