[isabelledev] push request (Sublist.thy)
Christian Sternagel
csterna at jaist.ac.jp
Sun Dec 9 06:27:30 CET 2012
Dear all,
I have the following changes in my local patch queue:
 In src/HOL/Library/Sublist.thy:
renamed "emb" ~> "list_hembeq" and "sub" ~> "sublisteq";
slightly changed definition of list_hembeq to make it reflexive
independent of the base order;
dropped predicate "transp_on"
Reasons: the name "emb" was very unspecific (hence the "list_" prefix to
make clear that it is on lists, and "h" for "homeomorphic" since there
is an important difference between "plain" embedding (which is just the
sublist relation) and homeomorphic embedding, where we are allowed to
replace elements by smaller elements w.r.t. some base order) and in a
later development I will need an irreflexive variant (hence "eq").
Furthermore, since the basic use of embedding is as a wellquasiorder
and wqos are reflexive it seems natural to have a definition where
embedding is reflexive independent of the base order.
I will add "transp_on" to Restricted_Predicates from the AFP. At some
point I would like to have the definitions of "reflp_on", "transp_on",
"irreflp_on", "antisymp_on", ... in the main distribution (but that is
an orthogonal issue).
Any comments? Any takers (for pushing my changes to the main repo)? I
checked the changes against f2241b8d0db5 with 'isabelle build a' and
prepared a changeset for the AFP (which I can push myself).
cheers
chris
PS: As stated above, currently my changes are in my local patch queue
and I attached the corresponding patch file from .hg/patches (which
contains a commit message at the top). Should I transform this into an
hgbundle?
 next part 
# HG changeset patch
# Parent f2241b8d0db588bedd8e1e9b39ad8ad1970c89ff
renamed "emb" to "list_hembeq"; make "list_hembeq" reflexive independent of the base order; renamed "sub" to "sublisteq"; dropped "transp_on" (state transitivity explicitly instead); no need to hide "sub" after renaming; replaced some ASCII symbols by proper Isabelle symbols; NEWS
diff r f2241b8d0db5 NEWS
 a/NEWS Sat Dec 08 22:41:39 2012 +0100
+++ b/NEWS Sun Dec 09 13:57:46 2012 +0900
@@ 173,8 +173,8 @@
syntax "xs >>= ys"; use "suffixeq ys xs" instead. Renamed lemmas
accordingly. INCOMPATIBILITY.
  New constant "emb" for homeomorphic embedding on lists. New
 abbreviation "sub" for special case "emb (op =)".
+  New constant "list_hembeq" for homeomorphic embedding on lists. New
+ abbreviation "sublisteq" for special case "list_hembeq (op =)".
 Library/Sublist does no longer provide "order" and "bot" type class
instances for the prefix order (merely corresponding locale
@@ 182,24 +182,24 @@
Library/Prefix_Order. INCOMPATIBILITY.
 The sublist relation from Library/Sublist_Order is now based on
 "Sublist.sub". Replaced lemmas:

 le_list_append_le_same_iff ~> Sublist.sub_append_le_same_iff
 le_list_append_mono ~> Sublist.emb_append_mono
 le_list_below_empty ~> Sublist.emb_Nil, Sublist.emb_Nil2
 le_list_Cons_EX ~> Sublist.emb_ConsD
 le_list_drop_Cons2 ~> Sublist.sub_Cons2'
 le_list_drop_Cons_neq ~> Sublist.sub_Cons2_neq
 le_list_drop_Cons ~> Sublist.sub_Cons'
 le_list_drop_many ~> Sublist.sub_drop_many
 le_list_filter_left ~> Sublist.sub_filter_left
 le_list_rev_drop_many ~> Sublist.sub_rev_drop_many
 le_list_rev_take_iff ~> Sublist.sub_append
 le_list_same_length ~> Sublist.sub_same_length
 le_list_take_many_iff ~> Sublist.sub_append'
+ "Sublist.sublisteq". Replaced lemmas:
+
+ le_list_append_le_same_iff ~> Sublist.sublisteq_append_le_same_iff
+ le_list_append_mono ~> Sublist.list_hembeq_append_mono
+ le_list_below_empty ~> Sublist.list_hembeq_Nil, Sublist.list_hembeq_Nil2
+ le_list_Cons_EX ~> Sublist.list_hembeq_ConsD
+ le_list_drop_Cons2 ~> Sublist.sublisteq_Cons2'
+ le_list_drop_Cons_neq ~> Sublist.sublisteq_Cons2_neq
+ le_list_drop_Cons ~> Sublist.sublisteq_Cons'
+ le_list_drop_many ~> Sublist.sublisteq_drop_many
+ le_list_filter_left ~> Sublist.sublisteq_filter_left
+ le_list_rev_drop_many ~> Sublist.sublisteq_rev_drop_many
+ le_list_rev_take_iff ~> Sublist.sublisteq_append
+ le_list_same_length ~> Sublist.sublisteq_same_length
+ le_list_take_many_iff ~> Sublist.sublisteq_append'
less_eq_list.drop ~> less_eq_list_drop
less_eq_list.induct ~> less_eq_list_induct
 not_le_list_length ~> Sublist.not_sub_length
+ not_le_list_length ~> Sublist.not_sublisteq_length
INCOMPATIBILITY.
diff r f2241b8d0db5 src/HOL/BNF/Examples/TreeFI.thy
 a/src/HOL/BNF/Examples/TreeFI.thy Sat Dec 08 22:41:39 2012 +0100
+++ b/src/HOL/BNF/Examples/TreeFI.thy Sun Dec 09 13:57:46 2012 +0900
@@ 12,8 +12,6 @@
imports ListF
begin
hide_const (open) Sublist.sub

codata 'a treeFI = Tree (lab: 'a) (sub: "'a treeFI listF")
lemma pre_treeFI_listF_set[simp]: "pre_treeFI_set2 (i, xs) = listF_set xs"
diff r f2241b8d0db5 src/HOL/BNF/Examples/TreeFsetI.thy
 a/src/HOL/BNF/Examples/TreeFsetI.thy Sat Dec 08 22:41:39 2012 +0100
+++ b/src/HOL/BNF/Examples/TreeFsetI.thy Sun Dec 09 13:57:46 2012 +0900
@@ 12,7 +12,6 @@
imports "../BNF"
begin
hide_const (open) Sublist.sub
hide_fact (open) Quotient_Product.prod_rel_def
codata 'a treeFsetI = Tree (lab: 'a) (sub: "'a treeFsetI fset")
diff r f2241b8d0db5 src/HOL/Library/Sublist.thy
 a/src/HOL/Library/Sublist.thy Sat Dec 08 22:41:39 2012 +0100
+++ b/src/HOL/Library/Sublist.thy Sun Dec 09 13:57:46 2012 +0900
@@ 3,7 +3,7 @@
Author: Christian Sternagel, JAIST
*)
header {* List prefixes, suffixes, and embedding*}
+header {* List prefixes, suffixes, and homeomorphic embedding *}
theory Sublist
imports Main
@@ 11,10 +11,10 @@
subsection {* Prefix order on lists *}
definition prefixeq :: "'a list => 'a list => bool"
+definition prefixeq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
where "prefixeq xs ys \<longleftrightarrow> (\<exists>zs. ys = xs @ zs)"
definition prefix :: "'a list => 'a list => bool"
+definition prefix :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
where "prefix xs ys \<longleftrightarrow> prefixeq xs ys \<and> xs \<noteq> ys"
interpretation prefix_order: order prefixeq prefix
@@ 23,7 +23,7 @@
interpretation prefix_bot: bot prefixeq prefix Nil
by default (simp add: prefixeq_def)
lemma prefixeqI [intro?]: "ys = xs @ zs ==> prefixeq xs ys"
+lemma prefixeqI [intro?]: "ys = xs @ zs \<Longrightarrow> prefixeq xs ys"
unfolding prefixeq_def by blast
lemma prefixeqE [elim?]:
@@ 31,7 +31,7 @@
obtains zs where "ys = xs @ zs"
using assms unfolding prefixeq_def by blast
lemma prefixI' [intro?]: "ys = xs @ z # zs ==> prefix xs ys"
+lemma prefixI' [intro?]: "ys = xs @ z # zs \<Longrightarrow> prefix xs ys"
unfolding prefix_def prefixeq_def by blast
lemma prefixE' [elim?]:
@@ 43,7 +43,7 @@
with that show ?thesis by (auto simp add: neq_Nil_conv)
qed
lemma prefixI [intro?]: "prefixeq xs ys ==> xs \<noteq> ys ==> prefix xs ys"
+lemma prefixI [intro?]: "prefixeq xs ys \<Longrightarrow> xs \<noteq> ys \<Longrightarrow> prefix xs ys"
unfolding prefix_def by blast
lemma prefixE [elim?]:
@@ 88,7 +88,7 @@
lemma same_prefixeq_nil [iff]: "prefixeq (xs @ ys) xs = (ys = [])"
by (metis append_Nil2 append_self_conv prefix_order.eq_iff prefixeqI)
lemma prefixeq_prefixeq [simp]: "prefixeq xs ys ==> prefixeq xs (ys @ zs)"
+lemma prefixeq_prefixeq [simp]: "prefixeq xs ys \<Longrightarrow> prefixeq xs (ys @ zs)"
by (metis prefix_order.le_less_trans prefixeqI prefixE prefixI)
lemma append_prefixeqD: "prefixeq (xs @ ys) zs \<Longrightarrow> prefixeq xs zs"
@@ 106,12 +106,12 @@
done
lemma append_one_prefixeq:
 "prefixeq xs ys ==> length xs < length ys ==> prefixeq (xs @ [ys ! length xs]) ys"
+ "prefixeq xs ys \<Longrightarrow> length xs < length ys \<Longrightarrow> prefixeq (xs @ [ys ! length xs]) ys"
unfolding prefixeq_def
by (metis Cons_eq_appendI append_eq_appendI append_eq_conv_conj
eq_Nil_appendI nth_drop')
theorem prefixeq_length_le: "prefixeq xs ys ==> length xs \<le> length ys"
+theorem prefixeq_length_le: "prefixeq xs ys \<Longrightarrow> length xs \<le> length ys"
by (auto simp add: prefixeq_def)
lemma prefixeq_same_cases:
@@ 191,10 +191,10 @@
subsection {* Parallel lists *}
definition parallel :: "'a list => 'a list => bool" (infixl "\<parallel>" 50)
+definition parallel :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infixl "\<parallel>" 50)
where "(xs \<parallel> ys) = (\<not> prefixeq xs ys \<and> \<not> prefixeq ys xs)"
lemma parallelI [intro]: "\<not> prefixeq xs ys ==> \<not> prefixeq ys xs ==> xs \<parallel> ys"
+lemma parallelI [intro]: "\<not> prefixeq xs ys \<Longrightarrow> \<not> prefixeq ys xs \<Longrightarrow> xs \<parallel> ys"
unfolding parallel_def by blast
lemma parallelE [elim]:
@@ 207,7 +207,7 @@
unfolding parallel_def prefix_def by blast
theorem parallel_decomp:
 "xs \<parallel> ys ==> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs"
+ "xs \<parallel> ys \<Longrightarrow> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs"
proof (induct xs rule: rev_induct)
case Nil
then have False by auto
@@ 268,7 +268,7 @@
"suffix xs ys \<Longrightarrow> suffixeq xs ys"
by (auto simp: suffixeq_def suffix_def)
lemma suffixeqI [intro?]: "ys = zs @ xs ==> suffixeq xs ys"
+lemma suffixeqI [intro?]: "ys = zs @ xs \<Longrightarrow> suffixeq xs ys"
unfolding suffixeq_def by blast
lemma suffixeqE [elim?]:
@@ 420,268 +420,262 @@
unfolding suffix_def by auto
subsection {* Embedding on lists *}
+subsection {* Homeomorphic embedding on lists *}
inductive emb :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
+inductive list_hembeq :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
for P :: "('a \<Rightarrow> 'a \<Rightarrow> bool)"
where
 emb_Nil [intro, simp]: "emb P [] ys"
 emb_Cons [intro] : "emb P xs ys \<Longrightarrow> emb P xs (y#ys)"
 emb_Cons2 [intro]: "P x y \<Longrightarrow> emb P xs ys \<Longrightarrow> emb P (x#xs) (y#ys)"
+ list_hembeq_Nil [intro, simp]: "list_hembeq P [] ys"
+ list_hembeq_Cons [intro] : "list_hembeq P xs ys \<Longrightarrow> list_hembeq P xs (y#ys)"
+ list_hembeq_Cons2 [intro]: "P\<^sup>=\<^sup>= x y \<Longrightarrow> list_hembeq P xs ys \<Longrightarrow> list_hembeq P (x#xs) (y#ys)"
lemma emb_Nil2 [simp]:
 assumes "emb P xs []" shows "xs = []"
 using assms by (cases rule: emb.cases) auto
+lemma list_hembeq_Nil2 [simp]:
+ assumes "list_hembeq P xs []" shows "xs = []"
+ using assms by (cases rule: list_hembeq.cases) auto
lemma emb_Cons_Nil [simp]: "emb P (x#xs) [] = False"
+lemma list_hembeq_refl [simp, intro!]:
+ "list_hembeq P xs xs"
+ by (induct xs) auto
+
+lemma list_hembeq_Cons_Nil [simp]: "list_hembeq P (x#xs) [] = False"
proof 
 { assume "emb P (x#xs) []"
 from emb_Nil2 [OF this] have False by simp
+ { assume "list_hembeq P (x#xs) []"
+ from list_hembeq_Nil2 [OF this] have False by simp
} moreover {
assume False
 then have "emb P (x#xs) []" by simp
+ then have "list_hembeq P (x#xs) []" by simp
} ultimately show ?thesis by blast
qed
lemma emb_append2 [intro]: "emb P xs ys \<Longrightarrow> emb P xs (zs @ ys)"
+lemma list_hembeq_append2 [intro]: "list_hembeq P xs ys \<Longrightarrow> list_hembeq P xs (zs @ ys)"
by (induct zs) auto
lemma emb_prefix [intro]:
 assumes "emb P xs ys" shows "emb P xs (ys @ zs)"
+lemma list_hembeq_prefix [intro]:
+ assumes "list_hembeq P xs ys" shows "list_hembeq P xs (ys @ zs)"
using assms
by (induct arbitrary: zs) auto
lemma emb_ConsD:
 assumes "emb P (x#xs) ys"
 shows "\<exists>us v vs. ys = us @ v # vs \<and> P x v \<and> emb P xs vs"
+lemma list_hembeq_ConsD:
+ assumes "list_hembeq P (x#xs) ys"
+ shows "\<exists>us v vs. ys = us @ v # vs \<and> P\<^sup>=\<^sup>= x v \<and> list_hembeq P xs vs"
using assms
proof (induct x \<equiv> "x # xs" ys arbitrary: x xs)
 case emb_Cons
+ case list_hembeq_Cons
then show ?case by (metis append_Cons)
next
 case (emb_Cons2 x y xs ys)
+ case (list_hembeq_Cons2 x y xs ys)
then show ?case by (cases xs) (auto, blast+)
qed
lemma emb_appendD:
 assumes "emb P (xs @ ys) zs"
 shows "\<exists>us vs. zs = us @ vs \<and> emb P xs us \<and> emb P ys vs"
+lemma list_hembeq_appendD:
+ assumes "list_hembeq P (xs @ ys) zs"
+ shows "\<exists>us vs. zs = us @ vs \<and> list_hembeq P xs us \<and> list_hembeq P ys vs"
using assms
proof (induction xs arbitrary: ys zs)
case Nil then show ?case by auto
next
case (Cons x xs)
then obtain us v vs where "zs = us @ v # vs"
 and "P x v" and "emb P (xs @ ys) vs" by (auto dest: emb_ConsD)
 with Cons show ?case by (metis append_Cons append_assoc emb_Cons2 emb_append2)
+ and "P\<^sup>=\<^sup>= x v" and "list_hembeq P (xs @ ys) vs" by (auto dest: list_hembeq_ConsD)
+ with Cons show ?case by (metis append_Cons append_assoc list_hembeq_Cons2 list_hembeq_append2)
qed
lemma emb_suffix:
 assumes "emb P xs ys" and "suffix ys zs"
 shows "emb P xs zs"
 using assms(2) and emb_append2 [OF assms(1)] by (auto simp: suffix_def)
+lemma list_hembeq_suffix:
+ assumes "list_hembeq P xs ys" and "suffix ys zs"
+ shows "list_hembeq P xs zs"
+ using assms(2) and list_hembeq_append2 [OF assms(1)] by (auto simp: suffix_def)
lemma emb_suffixeq:
 assumes "emb P xs ys" and "suffixeq ys zs"
 shows "emb P xs zs"
 using assms and emb_suffix unfolding suffixeq_suffix_reflclp_conv by auto
+lemma list_hembeq_suffixeq:
+ assumes "list_hembeq P xs ys" and "suffixeq ys zs"
+ shows "list_hembeq P xs zs"
+ using assms and list_hembeq_suffix unfolding suffixeq_suffix_reflclp_conv by auto
lemma emb_length: "emb P xs ys \<Longrightarrow> length xs \<le> length ys"
 by (induct rule: emb.induct) auto
+lemma list_hembeq_length: "list_hembeq P xs ys \<Longrightarrow> length xs \<le> length ys"
+ by (induct rule: list_hembeq.induct) auto
(*FIXME: move*)
definition transp_on :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
 where "transp_on P A \<longleftrightarrow> (\<forall>a\<in>A. \<forall>b\<in>A. \<forall>c\<in>A. P a b \<and> P b c \<longrightarrow> P a c)"
lemma transp_onI [Pure.intro]:
 "(\<And>a b c. \<lbrakk>a \<in> A; b \<in> A; c \<in> A; P a b; P b c\<rbrakk> \<Longrightarrow> P a c) \<Longrightarrow> transp_on P A"
 unfolding transp_on_def by blast

lemma transp_on_emb:
 assumes "transp_on P A"
 shows "transp_on (emb P) (lists A)"
proof
+lemma list_hembeq_trans:
+ assumes "\<And>x y z. \<lbrakk>x \<in> A; y \<in> A; z \<in> A; P x y; P y z\<rbrakk> \<Longrightarrow> P x z"
+ shows "\<And>xs ys zs. \<lbrakk>xs \<in> lists A; ys \<in> lists A; zs \<in> lists A;
+ list_hembeq P xs ys; list_hembeq P ys zs\<rbrakk> \<Longrightarrow> list_hembeq P xs zs"
+proof 
fix xs ys zs
 assume "emb P xs ys" and "emb P ys zs"
+ assume "list_hembeq P xs ys" and "list_hembeq P ys zs"
and "xs \<in> lists A" and "ys \<in> lists A" and "zs \<in> lists A"
 then show "emb P xs zs"
+ then show "list_hembeq P xs zs"
proof (induction arbitrary: zs)
 case emb_Nil show ?case by blast
+ case list_hembeq_Nil show ?case by blast
next
 case (emb_Cons xs ys y)
 from emb_ConsD [OF `emb P (y#ys) zs`] obtain us v vs
 where zs: "zs = us @ v # vs" and "P y v" and "emb P ys vs" by blast
 then have "emb P ys (v#vs)" by blast
 then have "emb P ys zs" unfolding zs by (rule emb_append2)
 from emb_Cons.IH [OF this] and emb_Cons.prems show ?case by simp
+ case (list_hembeq_Cons xs ys y)
+ from list_hembeq_ConsD [OF `list_hembeq P (y#ys) zs`] obtain us v vs
+ where zs: "zs = us @ v # vs" and "P\<^sup>=\<^sup>= y v" and "list_hembeq P ys vs" by blast
+ then have "list_hembeq P ys (v#vs)" by blast
+ then have "list_hembeq P ys zs" unfolding zs by (rule list_hembeq_append2)
+ from list_hembeq_Cons.IH [OF this] and list_hembeq_Cons.prems show ?case by simp
next
 case (emb_Cons2 x y xs ys)
 from emb_ConsD [OF `emb P (y#ys) zs`] obtain us v vs
 where zs: "zs = us @ v # vs" and "P y v" and "emb P ys vs" by blast
 with emb_Cons2 have "emb P xs vs" by simp
 moreover have "P x v"
+ case (list_hembeq_Cons2 x y xs ys)
+ from list_hembeq_ConsD [OF `list_hembeq P (y#ys) zs`] obtain us v vs
+ where zs: "zs = us @ v # vs" and "P\<^sup>=\<^sup>= y v" and "list_hembeq P ys vs" by blast
+ with list_hembeq_Cons2 have "list_hembeq P xs vs" by simp
+ moreover have "P\<^sup>=\<^sup>= x v"
proof 
from zs and `zs \<in> lists A` have "v \<in> A" by auto
 moreover have "x \<in> A" and "y \<in> A" using emb_Cons2 by simp_all
 ultimately show ?thesis using `P x y` and `P y v` and assms
 unfolding transp_on_def by blast
+ moreover have "x \<in> A" and "y \<in> A" using list_hembeq_Cons2 by simp_all
+ ultimately show ?thesis
+ using `P\<^sup>=\<^sup>= x y` and `P\<^sup>=\<^sup>= y v` and assms
+ by blast
qed
 ultimately have "emb P (x#xs) (v#vs)" by blast
 then show ?case unfolding zs by (rule emb_append2)
+ ultimately have "list_hembeq P (x#xs) (v#vs)" by blast
+ then show ?case unfolding zs by (rule list_hembeq_append2)
qed
qed
subsection {* Sublists (special case of embedding) *}
+subsection {* Sublists (special case of list_hembeqedding) *}
abbreviation sub :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
 where "sub xs ys \<equiv> emb (op =) xs ys"
+abbreviation sublisteq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
+ where "sublisteq xs ys \<equiv> list_hembeq (op =) xs ys"
lemma sub_Cons2: "sub xs ys \<Longrightarrow> sub (x#xs) (x#ys)" by auto
+lemma sublisteq_Cons2: "sublisteq xs ys \<Longrightarrow> sublisteq (x#xs) (x#ys)" by auto
lemma sub_same_length:
 assumes "sub xs ys" and "length xs = length ys" shows "xs = ys"
 using assms by (induct) (auto dest: emb_length)
+lemma sublisteq_same_length:
+ assumes "sublisteq xs ys" and "length xs = length ys" shows "xs = ys"
+ using assms by (induct) (auto dest: list_hembeq_length)
lemma not_sub_length [simp]: "length ys < length xs \<Longrightarrow> \<not> sub xs ys"
 by (metis emb_length linorder_not_less)
+lemma not_sublisteq_length [simp]: "length ys < length xs \<Longrightarrow> \<not> sublisteq xs ys"
+ by (metis list_hembeq_length linorder_not_less)
lemma [code]:
 "emb P [] ys \<longleftrightarrow> True"
 "emb P (x#xs) [] \<longleftrightarrow> False"
+ "list_hembeq P [] ys \<longleftrightarrow> True"
+ "list_hembeq P (x#xs) [] \<longleftrightarrow> False"
by (simp_all)
lemma sub_Cons': "sub (x#xs) ys \<Longrightarrow> sub xs ys"
 by (induct xs) (auto dest: emb_ConsD)
+lemma sublisteq_Cons': "sublisteq (x#xs) ys \<Longrightarrow> sublisteq xs ys"
+ by (induct xs) (auto dest: list_hembeq_ConsD)
lemma sub_Cons2':
 assumes "sub (x#xs) (x#ys)" shows "sub xs ys"
 using assms by (cases) (rule sub_Cons')
+lemma sublisteq_Cons2':
+ assumes "sublisteq (x#xs) (x#ys)" shows "sublisteq xs ys"
+ using assms by (cases) (rule sublisteq_Cons')
lemma sub_Cons2_neq:
 assumes "sub (x#xs) (y#ys)"
 shows "x \<noteq> y \<Longrightarrow> sub (x#xs) ys"
+lemma sublisteq_Cons2_neq:
+ assumes "sublisteq (x#xs) (y#ys)"
+ shows "x \<noteq> y \<Longrightarrow> sublisteq (x#xs) ys"
using assms by (cases) auto
lemma sub_Cons2_iff [simp, code]:
 "sub (x#xs) (y#ys) = (if x = y then sub xs ys else sub (x#xs) ys)"
 by (metis emb_Cons emb_Cons2 [of "op =", OF refl] sub_Cons2' sub_Cons2_neq)
+lemma sublisteq_Cons2_iff [simp, code]:
+ "sublisteq (x#xs) (y#ys) = (if x = y then sublisteq xs ys else sublisteq (x#xs) ys)"
+ by (metis list_hembeq_Cons sublisteq_Cons2 sublisteq_Cons2' sublisteq_Cons2_neq)
lemma sub_append': "sub (zs @ xs) (zs @ ys) \<longleftrightarrow> sub xs ys"
+lemma sublisteq_append': "sublisteq (zs @ xs) (zs @ ys) \<longleftrightarrow> sublisteq xs ys"
by (induct zs) simp_all
lemma sub_refl [simp, intro!]: "sub xs xs" by (induct xs) simp_all
+lemma sublisteq_refl [simp, intro!]: "sublisteq xs xs" by (induct xs) simp_all
lemma sub_antisym:
 assumes "sub xs ys" and "sub ys xs"
+lemma sublisteq_antisym:
+ assumes "sublisteq xs ys" and "sublisteq ys xs"
shows "xs = ys"
using assms
proof (induct)
 case emb_Nil
 from emb_Nil2 [OF this] show ?case by simp
+ case list_hembeq_Nil
+ from list_hembeq_Nil2 [OF this] show ?case by simp
next
 case emb_Cons2
+ case list_hembeq_Cons2
then show ?case by simp
next
 case emb_Cons
+ case list_hembeq_Cons
then show ?case
 by (metis sub_Cons' emb_length Suc_length_conv Suc_n_not_le_n)
+ by (metis sublisteq_Cons' list_hembeq_length Suc_length_conv Suc_n_not_le_n)
qed
lemma transp_on_sub: "transp_on sub UNIV"
proof 
 have "transp_on (op =) UNIV" by (simp add: transp_on_def)
 from transp_on_emb [OF this] show ?thesis by simp
qed
+lemma sublisteq_trans: "sublisteq xs ys \<Longrightarrow> sublisteq ys zs \<Longrightarrow> sublisteq xs zs"
+ by (rule list_hembeq_trans [of UNIV "op ="]) auto
lemma sub_trans: "sub xs ys \<Longrightarrow> sub ys zs \<Longrightarrow> sub xs zs"
 using transp_on_sub [unfolded transp_on_def] by blast
+lemma sublisteq_append_le_same_iff: "sublisteq (xs @ ys) ys \<longleftrightarrow> xs = []"
+ by (auto dest: list_hembeq_length)
lemma sub_append_le_same_iff: "sub (xs @ ys) ys \<longleftrightarrow> xs = []"
 by (auto dest: emb_length)

lemma emb_append_mono:
 "\<lbrakk> emb P xs xs'; emb P ys ys' \<rbrakk> \<Longrightarrow> emb P (xs at ys) (xs'@ys')"
 apply (induct rule: emb.induct)
 apply (metis eq_Nil_appendI emb_append2)
 apply (metis append_Cons emb_Cons)
 apply (metis append_Cons emb_Cons2)
+lemma list_hembeq_append_mono:
+ "\<lbrakk> list_hembeq P xs xs'; list_hembeq P ys ys' \<rbrakk> \<Longrightarrow> list_hembeq P (xs at ys) (xs'@ys')"
+ apply (induct rule: list_hembeq.induct)
+ apply (metis eq_Nil_appendI list_hembeq_append2)
+ apply (metis append_Cons list_hembeq_Cons)
+ apply (metis append_Cons list_hembeq_Cons2)
done
subsection {* Appending elements *}
lemma sub_append [simp]:
 "sub (xs @ zs) (ys @ zs) \<longleftrightarrow> sub xs ys" (is "?l = ?r")
+lemma sublisteq_append [simp]:
+ "sublisteq (xs @ zs) (ys @ zs) \<longleftrightarrow> sublisteq xs ys" (is "?l = ?r")
proof
 { fix xs' ys' xs ys zs :: "'a list" assume "sub xs' ys'"
 then have "xs' = xs @ zs & ys' = ys @ zs \<longrightarrow> sub xs ys"
+ { fix xs' ys' xs ys zs :: "'a list" assume "sublisteq xs' ys'"
+ then have "xs' = xs @ zs & ys' = ys @ zs \<longrightarrow> sublisteq xs ys"
proof (induct arbitrary: xs ys zs)
 case emb_Nil show ?case by simp
+ case list_hembeq_Nil show ?case by simp
next
 case (emb_Cons xs' ys' x)
 { assume "ys=[]" then have ?case using emb_Cons(1) by auto }
+ case (list_hembeq_Cons xs' ys' x)
+ { assume "ys=[]" then have ?case using list_hembeq_Cons(1) by auto }
moreover
{ fix us assume "ys = x#us"
 then have ?case using emb_Cons(2) by(simp add: emb.emb_Cons) }
+ then have ?case using list_hembeq_Cons(2) by(simp add: list_hembeq.list_hembeq_Cons) }
ultimately show ?case by (auto simp:Cons_eq_append_conv)
next
 case (emb_Cons2 x y xs' ys')
 { assume "xs=[]" then have ?case using emb_Cons2(1) by auto }
+ case (list_hembeq_Cons2 x y xs' ys')
+ { assume "xs=[]" then have ?case using list_hembeq_Cons2(1) by auto }
moreover
 { fix us vs assume "xs=x#us" "ys=x#vs" then have ?case using emb_Cons2 by auto}
+ { fix us vs assume "xs=x#us" "ys=x#vs" then have ?case using list_hembeq_Cons2 by auto}
moreover
 { fix us assume "xs=x#us" "ys=[]" then have ?case using emb_Cons2(2) by bestsimp }
 ultimately show ?case using `x = y` by (auto simp: Cons_eq_append_conv)
+ { fix us assume "xs=x#us" "ys=[]" then have ?case using list_hembeq_Cons2(2) by bestsimp }
+ ultimately show ?case using `op =\<^sup>=\<^sup>= x y` by (auto simp: Cons_eq_append_conv)
qed }
moreover assume ?l
ultimately show ?r by blast
next
 assume ?r then show ?l by (metis emb_append_mono sub_refl)
+ assume ?r then show ?l by (metis list_hembeq_append_mono sublisteq_refl)
qed
lemma sub_drop_many: "sub xs ys \<Longrightarrow> sub xs (zs @ ys)"
+lemma sublisteq_drop_many: "sublisteq xs ys \<Longrightarrow> sublisteq xs (zs @ ys)"
by (induct zs) auto
lemma sub_rev_drop_many: "sub xs ys \<Longrightarrow> sub xs (ys @ zs)"
 by (metis append_Nil2 emb_Nil emb_append_mono)
+lemma sublisteq_rev_drop_many: "sublisteq xs ys \<Longrightarrow> sublisteq xs (ys @ zs)"
+ by (metis append_Nil2 list_hembeq_Nil list_hembeq_append_mono)
subsection {* Relation to standard list operations *}
lemma sub_map:
 assumes "sub xs ys" shows "sub (map f xs) (map f ys)"
+lemma sublisteq_map:
+ assumes "sublisteq xs ys" shows "sublisteq (map f xs) (map f ys)"
using assms by (induct) auto
lemma sub_filter_left [simp]: "sub (filter P xs) xs"
+lemma sublisteq_filter_left [simp]: "sublisteq (filter P xs) xs"
by (induct xs) auto
lemma sub_filter [simp]:
 assumes "sub xs ys" shows "sub (filter P xs) (filter P ys)"
+lemma sublisteq_filter [simp]:
+ assumes "sublisteq xs ys" shows "sublisteq (filter P xs) (filter P ys)"
using assms by (induct) auto
lemma "sub xs ys \<longleftrightarrow> (\<exists>N. xs = sublist ys N)" (is "?L = ?R")
+lemma "sublisteq xs ys \<longleftrightarrow> (\<exists>N. xs = sublist ys N)" (is "?L = ?R")
proof
assume ?L
then show ?R
proof (induct)
 case emb_Nil show ?case by (metis sublist_empty)
+ case list_hembeq_Nil show ?case by (metis sublist_empty)
next
 case (emb_Cons xs ys x)
+ case (list_hembeq_Cons xs ys x)
then obtain N where "xs = sublist ys N" by blast
then have "xs = sublist (x#ys) (Suc ` N)"
by (clarsimp simp add:sublist_Cons inj_image_mem_iff)
then show ?case by blast
next
 case (emb_Cons2 x y xs ys)
+ case (list_hembeq_Cons2 x y xs ys)
then obtain N where "xs = sublist ys N" by blast
then have "x#xs = sublist (x#ys) (insert 0 (Suc ` N))"
by (clarsimp simp add:sublist_Cons inj_image_mem_iff)
 then show ?case unfolding `x = y` by blast
+ moreover from list_hembeq_Cons2 have "x = y" by simp
+ ultimately show ?case by blast
qed
next
assume ?R
then obtain N where "xs = sublist ys N" ..
 moreover have "sub (sublist ys N) ys"
+ moreover have "sublisteq (sublist ys N) ys"
proof (induct ys arbitrary: N)
case Nil show ?case by simp
next
diff r f2241b8d0db5 src/HOL/Library/Sublist_Order.thy
 a/src/HOL/Library/Sublist_Order.thy Sat Dec 08 22:41:39 2012 +0100
+++ b/src/HOL/Library/Sublist_Order.thy Sun Dec 09 13:57:46 2012 +0900
@@ 21,7 +21,7 @@
begin
definition
 "(xs :: 'a list) \<le> ys \<longleftrightarrow> sub xs ys"
+ "(xs :: 'a list) \<le> ys \<longleftrightarrow> sublisteq xs ys"
definition
"(xs :: 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
@@ 40,41 +40,41 @@
next
fix xs ys :: "'a list"
assume "xs <= ys" and "ys <= xs"
 thus "xs = ys" by (unfold less_eq_list_def) (rule sub_antisym)
+ thus "xs = ys" by (unfold less_eq_list_def) (rule sublisteq_antisym)
next
fix xs ys zs :: "'a list"
assume "xs <= ys" and "ys <= zs"
 thus "xs <= zs" by (unfold less_eq_list_def) (rule sub_trans)
+ thus "xs <= zs" by (unfold less_eq_list_def) (rule sublisteq_trans)
qed
lemmas less_eq_list_induct [consumes 1, case_names empty drop take] =
 emb.induct [of "op =", folded less_eq_list_def]
lemmas less_eq_list_drop = emb.emb_Cons [of "op =", folded less_eq_list_def]
lemmas le_list_Cons2_iff [simp, code] = sub_Cons2_iff [folded less_eq_list_def]
lemmas le_list_map = sub_map [folded less_eq_list_def]
lemmas le_list_filter = sub_filter [folded less_eq_list_def]
lemmas le_list_length = emb_length [of "op =", folded less_eq_list_def]
+ list_hembeq.induct [of "op =", folded less_eq_list_def]
+lemmas less_eq_list_drop = list_hembeq.list_hembeq_Cons [of "op =", folded less_eq_list_def]
+lemmas le_list_Cons2_iff [simp, code] = sublisteq_Cons2_iff [folded less_eq_list_def]
+lemmas le_list_map = sublisteq_map [folded less_eq_list_def]
+lemmas le_list_filter = sublisteq_filter [folded less_eq_list_def]
+lemmas le_list_length = list_hembeq_length [of "op =", folded less_eq_list_def]
lemma less_list_length: "xs < ys \<Longrightarrow> length xs < length ys"
 by (metis emb_length sub_same_length le_neq_implies_less less_list_def less_eq_list_def)
+ by (metis list_hembeq_length sublisteq_same_length le_neq_implies_less less_list_def less_eq_list_def)
lemma less_list_empty [simp]: "[] < xs \<longleftrightarrow> xs \<noteq> []"
 by (metis less_eq_list_def emb_Nil order_less_le)
+ by (metis less_eq_list_def list_hembeq_Nil order_less_le)
lemma less_list_below_empty [simp]: "xs < [] \<longleftrightarrow> False"
 by (metis emb_Nil less_eq_list_def less_list_def)
+ by (metis list_hembeq_Nil less_eq_list_def less_list_def)
lemma less_list_drop: "xs < ys \<Longrightarrow> xs < x # ys"
by (unfold less_le less_eq_list_def) (auto)
lemma less_list_take_iff: "x # xs < x # ys \<longleftrightarrow> xs < ys"
 by (metis sub_Cons2_iff less_list_def less_eq_list_def)
+ by (metis sublisteq_Cons2_iff less_list_def less_eq_list_def)
lemma less_list_drop_many: "xs < ys \<Longrightarrow> xs < zs @ ys"
 by (metis sub_append_le_same_iff sub_drop_many order_less_le self_append_conv2 less_eq_list_def)
+ by (metis sublisteq_append_le_same_iff sublisteq_drop_many order_less_le self_append_conv2 less_eq_list_def)
lemma less_list_take_many_iff: "zs @ xs < zs @ ys \<longleftrightarrow> xs < ys"
 by (metis less_list_def less_eq_list_def sub_append')
+ by (metis less_list_def less_eq_list_def sublisteq_append')
lemma less_list_rev_take: "xs @ zs < ys @ zs \<longleftrightarrow> xs < ys"
by (unfold less_le less_eq_list_def) auto
More information about the isabelledev
mailing list