[isabelle-dev] pull request (HOL-Library/Sublist(_Order))
Christian Sternagel
c.sternagel at gmail.com
Mon Jun 30 15:59:05 CEST 2014
Dear developers,
would somebody be willing to pull in the attached patches into
HOL/Library? The patches where generated with the help of mercurial's mq
extension (i.e., the "series" file gives the order of application) and
each patch can be imported into a repository by
hg import --user "Christian Sternagel" <patch-file>
In the AFP the attached changes do only influence my entry
Well-Quasi-Orders and (to a tiny amount) Myhill-Nerode, for which I have
corresponding patches in my local AFP repo.
The intention behind the patches is as follows:
* No built-in reflexivity for list embedding. Which is more standard in
the literature. Then reflexivity of list embedding depends on the
reflexivity of the given relation on elements.
* To make this more obvious remove "eq" suffix from "list_hembeq". Plus,
to obtain a slightly shorter (and as I think, more easy to parse) name,
rename "list_hembeq" into "list_emb" (ideally this should be "List.emb"
at some point).
* Added monotonicity lemma for "list_emb" which is needed for inductive
definitions based on it.
* Weaker assumption for transitivity lemma of "list_emb".
* Added lemma that for a list that is embedded in another one, i.e.,
"list_emb P xs ys", all its elements are in the given base relation "P"
with some element of the latter, i.e., "ALL x : set xs. EX y : set ys. P
x y".
cheers
chris
-------------- next part --------------
# HG changeset patch
# Parent 48c582067cb9a6551b85710ea9cf51158cd2e5b9
weaker assumption for "list_emb_trans"; added lemma
diff -r 48c582067cb9 -r d2e2e72eb1a0 src/HOL/Library/Sublist.thy
--- a/src/HOL/Library/Sublist.thy Thu Jun 26 13:24:41 2014 +0200
+++ b/src/HOL/Library/Sublist.thy Thu Jun 26 15:31:04 2014 +0200
@@ -514,34 +514,31 @@
by (induct rule: list_emb.induct) auto
lemma list_emb_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_emb P xs ys; list_emb P ys zs\<rbrakk> \<Longrightarrow> list_emb P xs zs"
+ assumes "\<And>x y z. \<lbrakk>x \<in> set xs; y \<in> set ys; z \<in> set zs; P x y; P y z\<rbrakk> \<Longrightarrow> P x z"
+ shows "\<lbrakk>list_emb P xs ys; list_emb P ys zs\<rbrakk> \<Longrightarrow> list_emb P xs zs"
proof -
- fix xs ys zs
assume "list_emb P xs ys" and "list_emb P ys zs"
- and "xs \<in> lists A" and "ys \<in> lists A" and "zs \<in> lists A"
- then show "list_emb P xs zs"
+ then show "list_emb P xs zs" using assms
proof (induction arbitrary: zs)
case list_emb_Nil show ?case by blast
next
case (list_emb_Cons xs ys y)
from list_emb_ConsD [OF `list_emb P (y#ys) zs`] obtain us v vs
- where zs: "zs = us @ v # vs" and "P y v" and "list_emb P ys vs" by blast
+ where zs: "zs = us @ v # vs" and "P\<^sup>=\<^sup>= y v" and "list_emb P ys vs" by blast
then have "list_emb P ys (v#vs)" by blast
then have "list_emb P ys zs" unfolding zs by (rule list_emb_append2)
- from list_emb_Cons.IH [OF this] and list_emb_Cons.prems show ?case by simp
+ from list_emb_Cons.IH [OF this] and list_emb_Cons.prems show ?case by auto
next
case (list_emb_Cons2 x y xs ys)
from list_emb_ConsD [OF `list_emb P (y#ys) zs`] obtain us v vs
where zs: "zs = us @ v # vs" and "P y v" and "list_emb P ys vs" by blast
- with list_emb_Cons2 have "list_emb P xs vs" by simp
+ with list_emb_Cons2 have "list_emb P xs vs" by auto
moreover have "P 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 list_emb_Cons2 by simp_all
+ from zs have "v \<in> set zs" by auto
+ moreover have "x \<in> set (x#xs)" and "y \<in> set (y#ys)" by simp_all
ultimately show ?thesis
- using `P x y` and `P y v` and assms
+ using `P x y` and `P y v` and list_emb_Cons2
by blast
qed
ultimately have "list_emb P (x#xs) (v#vs)" by blast
@@ -549,6 +546,11 @@
qed
qed
+lemma list_emb_set:
+ assumes "list_emb P xs ys" and "x \<in> set xs"
+ obtains y where "y \<in> set ys" and "P x y"
+ using assms by (induct) auto
+
subsection {* Sublists (special case of homeomorphic embedding) *}
@@ -607,7 +609,7 @@
qed
lemma sublisteq_trans: "sublisteq xs ys \<Longrightarrow> sublisteq ys zs \<Longrightarrow> sublisteq xs zs"
- by (rule list_emb_trans [of UNIV "op ="]) auto
+ by (rule list_emb_trans [of _ _ _ "op ="]) auto
lemma sublisteq_append_le_same_iff: "sublisteq (xs @ ys) ys \<longleftrightarrow> xs = []"
by (auto dest: list_emb_length)
-------------- next part --------------
# HG changeset patch
# Parent fc4d65afdf136a1d54bbd7419aede9cf70defcff
renamed "list_hembeq" into slightly shorter "list_emb"
diff -r fc4d65afdf13 -r f07fe64d9f21 src/HOL/Library/Sublist.thy
--- a/src/HOL/Library/Sublist.thy Mon Jun 23 12:54:48 2014 +0200
+++ b/src/HOL/Library/Sublist.thy Thu Jun 26 13:15:21 2014 +0200
@@ -428,115 +428,115 @@
subsection {* Homeomorphic embedding on lists *}
-inductive list_hembeq :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
+inductive list_emb :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
for P :: "('a \<Rightarrow> 'a \<Rightarrow> bool)"
where
- 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)"
+ list_emb_Nil [intro, simp]: "list_emb P [] ys"
+| list_emb_Cons [intro] : "list_emb P xs ys \<Longrightarrow> list_emb P xs (y#ys)"
+| list_emb_Cons2 [intro]: "P\<^sup>=\<^sup>= x y \<Longrightarrow> list_emb P xs ys \<Longrightarrow> list_emb P (x#xs) (y#ys)"
-lemma list_hembeq_Nil2 [simp]:
- assumes "list_hembeq P xs []" shows "xs = []"
- using assms by (cases rule: list_hembeq.cases) auto
+lemma list_emb_Nil2 [simp]:
+ assumes "list_emb P xs []" shows "xs = []"
+ using assms by (cases rule: list_emb.cases) auto
-lemma list_hembeq_refl [simp, intro!]:
- "list_hembeq P xs xs"
+lemma list_emb_refl [simp, intro!]:
+ "list_emb P xs xs"
by (induct xs) auto
-lemma list_hembeq_Cons_Nil [simp]: "list_hembeq P (x#xs) [] = False"
+lemma list_emb_Cons_Nil [simp]: "list_emb P (x#xs) [] = False"
proof -
- { assume "list_hembeq P (x#xs) []"
- from list_hembeq_Nil2 [OF this] have False by simp
+ { assume "list_emb P (x#xs) []"
+ from list_emb_Nil2 [OF this] have False by simp
} moreover {
assume False
- then have "list_hembeq P (x#xs) []" by simp
+ then have "list_emb P (x#xs) []" by simp
} ultimately show ?thesis by blast
qed
-lemma list_hembeq_append2 [intro]: "list_hembeq P xs ys \<Longrightarrow> list_hembeq P xs (zs @ ys)"
+lemma list_emb_append2 [intro]: "list_emb P xs ys \<Longrightarrow> list_emb P xs (zs @ ys)"
by (induct zs) auto
-lemma list_hembeq_prefix [intro]:
- assumes "list_hembeq P xs ys" shows "list_hembeq P xs (ys @ zs)"
+lemma list_emb_prefix [intro]:
+ assumes "list_emb P xs ys" shows "list_emb P xs (ys @ zs)"
using assms
by (induct arbitrary: zs) auto
-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"
+lemma list_emb_ConsD:
+ assumes "list_emb P (x#xs) ys"
+ shows "\<exists>us v vs. ys = us @ v # vs \<and> P\<^sup>=\<^sup>= x v \<and> list_emb P xs vs"
using assms
proof (induct x \<equiv> "x # xs" ys arbitrary: x xs)
- case list_hembeq_Cons
+ case list_emb_Cons
then show ?case by (metis append_Cons)
next
- case (list_hembeq_Cons2 x y xs ys)
+ case (list_emb_Cons2 x y xs ys)
then show ?case by blast
qed
-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"
+lemma list_emb_appendD:
+ assumes "list_emb P (xs @ ys) zs"
+ shows "\<exists>us vs. zs = us @ vs \<and> list_emb P xs us \<and> list_emb 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: "zs = us @ v # vs" and p: "P\<^sup>=\<^sup>= x v" and lh: "list_hembeq P (xs @ ys) vs"
- by (auto dest: list_hembeq_ConsD)
+ zs: "zs = us @ v # vs" and p: "P\<^sup>=\<^sup>= x v" and lh: "list_emb P (xs @ ys) vs"
+ by (auto dest: list_emb_ConsD)
obtain sk\<^sub>0 :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" and sk\<^sub>1 :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
- sk: "\<forall>x\<^sub>0 x\<^sub>1. \<not> list_hembeq P (xs @ x\<^sub>0) x\<^sub>1 \<or> sk\<^sub>0 x\<^sub>0 x\<^sub>1 @ sk\<^sub>1 x\<^sub>0 x\<^sub>1 = x\<^sub>1 \<and> list_hembeq P xs (sk\<^sub>0 x\<^sub>0 x\<^sub>1) \<and> list_hembeq P x\<^sub>0 (sk\<^sub>1 x\<^sub>0 x\<^sub>1)"
+ sk: "\<forall>x\<^sub>0 x\<^sub>1. \<not> list_emb P (xs @ x\<^sub>0) x\<^sub>1 \<or> sk\<^sub>0 x\<^sub>0 x\<^sub>1 @ sk\<^sub>1 x\<^sub>0 x\<^sub>1 = x\<^sub>1 \<and> list_emb P xs (sk\<^sub>0 x\<^sub>0 x\<^sub>1) \<and> list_emb P x\<^sub>0 (sk\<^sub>1 x\<^sub>0 x\<^sub>1)"
using Cons(1) by (metis (no_types))
- hence "\<forall>x\<^sub>2. list_hembeq P (x # xs) (x\<^sub>2 @ v # sk\<^sub>0 ys vs)" using p lh by auto
+ hence "\<forall>x\<^sub>2. list_emb P (x # xs) (x\<^sub>2 @ v # sk\<^sub>0 ys vs)" using p lh by auto
thus ?case using lh zs sk by (metis (no_types) append_Cons append_assoc)
qed
-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 list_emb_suffix:
+ assumes "list_emb P xs ys" and "suffix ys zs"
+ shows "list_emb P xs zs"
+ using assms(2) and list_emb_append2 [OF assms(1)] by (auto simp: suffix_def)
-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 list_emb_suffixeq:
+ assumes "list_emb P xs ys" and "suffixeq ys zs"
+ shows "list_emb P xs zs"
+ using assms and list_emb_suffix unfolding suffixeq_suffix_reflclp_conv by auto
-lemma list_hembeq_length: "list_hembeq P xs ys \<Longrightarrow> length xs \<le> length ys"
- by (induct rule: list_hembeq.induct) auto
+lemma list_emb_length: "list_emb P xs ys \<Longrightarrow> length xs \<le> length ys"
+ by (induct rule: list_emb.induct) auto
-lemma list_hembeq_trans:
+lemma list_emb_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"
+ list_emb P xs ys; list_emb P ys zs\<rbrakk> \<Longrightarrow> list_emb P xs zs"
proof -
fix xs ys zs
- assume "list_hembeq P xs ys" and "list_hembeq P ys zs"
+ assume "list_emb P xs ys" and "list_emb P ys zs"
and "xs \<in> lists A" and "ys \<in> lists A" and "zs \<in> lists A"
- then show "list_hembeq P xs zs"
+ then show "list_emb P xs zs"
proof (induction arbitrary: zs)
- case list_hembeq_Nil show ?case by blast
+ case list_emb_Nil show ?case by blast
next
- 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
+ case (list_emb_Cons xs ys y)
+ from list_emb_ConsD [OF `list_emb P (y#ys) zs`] obtain us v vs
+ where zs: "zs = us @ v # vs" and "P\<^sup>=\<^sup>= y v" and "list_emb P ys vs" by blast
+ then have "list_emb P ys (v#vs)" by blast
+ then have "list_emb P ys zs" unfolding zs by (rule list_emb_append2)
+ from list_emb_Cons.IH [OF this] and list_emb_Cons.prems show ?case by simp
next
- 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
+ case (list_emb_Cons2 x y xs ys)
+ from list_emb_ConsD [OF `list_emb P (y#ys) zs`] obtain us v vs
+ where zs: "zs = us @ v # vs" and "P\<^sup>=\<^sup>= y v" and "list_emb P ys vs" by blast
+ with list_emb_Cons2 have "list_emb 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 list_hembeq_Cons2 by simp_all
+ moreover have "x \<in> A" and "y \<in> A" using list_emb_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 "list_hembeq P (x#xs) (v#vs)" by blast
- then show ?case unfolding zs by (rule list_hembeq_append2)
+ ultimately have "list_emb P (x#xs) (v#vs)" by blast
+ then show ?case unfolding zs by (rule list_emb_append2)
qed
qed
@@ -544,24 +544,24 @@
subsection {* Sublists (special case of homeomorphic embedding) *}
abbreviation sublisteq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
- where "sublisteq xs ys \<equiv> list_hembeq (op =) xs ys"
+ where "sublisteq xs ys \<equiv> list_emb (op =) xs ys"
lemma sublisteq_Cons2: "sublisteq xs ys \<Longrightarrow> sublisteq (x#xs) (x#ys)" by auto
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)
+ using assms by (induct) (auto dest: list_emb_length)
lemma not_sublisteq_length [simp]: "length ys < length xs \<Longrightarrow> \<not> sublisteq xs ys"
- by (metis list_hembeq_length linorder_not_less)
+ by (metis list_emb_length linorder_not_less)
lemma [code]:
- "list_hembeq P [] ys \<longleftrightarrow> True"
- "list_hembeq P (x#xs) [] \<longleftrightarrow> False"
+ "list_emb P [] ys \<longleftrightarrow> True"
+ "list_emb P (x#xs) [] \<longleftrightarrow> False"
by (simp_all)
lemma sublisteq_Cons': "sublisteq (x#xs) ys \<Longrightarrow> sublisteq xs ys"
- by (induct xs, simp, blast dest: list_hembeq_ConsD)
+ by (induct xs, simp, blast dest: list_emb_ConsD)
lemma sublisteq_Cons2':
assumes "sublisteq (x#xs) (x#ys)" shows "sublisteq xs ys"
@@ -574,7 +574,7 @@
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)
+ by (metis list_emb_Cons sublisteq_Cons2 sublisteq_Cons2' sublisteq_Cons2_neq)
lemma sublisteq_append': "sublisteq (zs @ xs) (zs @ ys) \<longleftrightarrow> sublisteq xs ys"
by (induct zs) simp_all
@@ -586,29 +586,29 @@
shows "xs = ys"
using assms
proof (induct)
- case list_hembeq_Nil
- from list_hembeq_Nil2 [OF this] show ?case by simp
+ case list_emb_Nil
+ from list_emb_Nil2 [OF this] show ?case by simp
next
- case list_hembeq_Cons2
+ case list_emb_Cons2
thus ?case by simp
next
- case list_hembeq_Cons
+ case list_emb_Cons
hence False using sublisteq_Cons' by fastforce
thus ?case ..
qed
lemma sublisteq_trans: "sublisteq xs ys \<Longrightarrow> sublisteq ys zs \<Longrightarrow> sublisteq xs zs"
- by (rule list_hembeq_trans [of UNIV "op ="]) auto
+ by (rule list_emb_trans [of UNIV "op ="]) auto
lemma sublisteq_append_le_same_iff: "sublisteq (xs @ ys) ys \<longleftrightarrow> xs = []"
- by (auto dest: list_hembeq_length)
+ by (auto dest: list_emb_length)
-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)
+lemma list_emb_append_mono:
+ "\<lbrakk> list_emb P xs xs'; list_emb P ys ys' \<rbrakk> \<Longrightarrow> list_emb P (xs at ys) (xs'@ys')"
+ apply (induct rule: list_emb.induct)
+ apply (metis eq_Nil_appendI list_emb_append2)
+ apply (metis append_Cons list_emb_Cons)
+ apply (metis append_Cons list_emb_Cons2)
done
@@ -620,34 +620,34 @@
{ 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 list_hembeq_Nil show ?case by simp
+ case list_emb_Nil show ?case by simp
next
- case (list_hembeq_Cons xs' ys' x)
- { assume "ys=[]" then have ?case using list_hembeq_Cons(1) by auto }
+ case (list_emb_Cons xs' ys' x)
+ { assume "ys=[]" then have ?case using list_emb_Cons(1) by auto }
moreover
{ fix us assume "ys = x#us"
- then have ?case using list_hembeq_Cons(2) by(simp add: list_hembeq.list_hembeq_Cons) }
+ then have ?case using list_emb_Cons(2) by(simp add: list_emb.list_emb_Cons) }
ultimately show ?case by (auto simp:Cons_eq_append_conv)
next
- case (list_hembeq_Cons2 x y xs' ys')
- { assume "xs=[]" then have ?case using list_hembeq_Cons2(1) by auto }
+ case (list_emb_Cons2 x y xs' ys')
+ { assume "xs=[]" then have ?case using list_emb_Cons2(1) by auto }
moreover
- { fix us vs assume "xs=x#us" "ys=x#vs" then have ?case using list_hembeq_Cons2 by auto}
+ { fix us vs assume "xs=x#us" "ys=x#vs" then have ?case using list_emb_Cons2 by auto}
moreover
- { fix us assume "xs=x#us" "ys=[]" then have ?case using list_hembeq_Cons2(2) by bestsimp }
+ { fix us assume "xs=x#us" "ys=[]" then have ?case using list_emb_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 list_hembeq_append_mono sublisteq_refl)
+ assume ?r then show ?l by (metis list_emb_append_mono sublisteq_refl)
qed
lemma sublisteq_drop_many: "sublisteq xs ys \<Longrightarrow> sublisteq xs (zs @ ys)"
by (induct zs) auto
lemma sublisteq_rev_drop_many: "sublisteq xs ys \<Longrightarrow> sublisteq xs (ys @ zs)"
- by (metis append_Nil2 list_hembeq_Nil list_hembeq_append_mono)
+ by (metis append_Nil2 list_emb_Nil list_emb_append_mono)
subsection {* Relation to standard list operations *}
@@ -668,19 +668,19 @@
assume ?L
then show ?R
proof (induct)
- case list_hembeq_Nil show ?case by (metis sublist_empty)
+ case list_emb_Nil show ?case by (metis sublist_empty)
next
- case (list_hembeq_Cons xs ys x)
+ case (list_emb_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 (list_hembeq_Cons2 x y xs ys)
+ case (list_emb_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)
- moreover from list_hembeq_Cons2 have "x = y" by simp
+ moreover from list_emb_Cons2 have "x = y" by simp
ultimately show ?case by blast
qed
next
diff -r fc4d65afdf13 -r f07fe64d9f21 src/HOL/Library/Sublist_Order.thy
--- a/src/HOL/Library/Sublist_Order.thy Mon Jun 23 12:54:48 2014 +0200
+++ b/src/HOL/Library/Sublist_Order.thy Thu Jun 26 13:15:21 2014 +0200
@@ -48,21 +48,21 @@
qed
lemmas less_eq_list_induct [consumes 1, case_names empty drop take] =
- 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]
+ list_emb.induct [of "op =", folded less_eq_list_def]
+lemmas less_eq_list_drop = list_emb.list_emb_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]
+lemmas le_list_length = list_emb_length [of "op =", folded less_eq_list_def]
lemma less_list_length: "xs < ys \<Longrightarrow> length xs < length ys"
- by (metis list_hembeq_length sublisteq_same_length le_neq_implies_less less_list_def less_eq_list_def)
+ by (metis list_emb_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 list_hembeq_Nil order_less_le)
+ by (metis less_eq_list_def list_emb_Nil order_less_le)
lemma less_list_below_empty [simp]: "xs < [] \<longleftrightarrow> False"
- by (metis list_hembeq_Nil less_eq_list_def less_list_def)
+ by (metis list_emb_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)
-------------- next part --------------
# HG changeset patch
# Parent e574ed0a99d227d70283970bb5a45782cf7c7d62
added monotonicity lemma for list embedding
diff -r e574ed0a99d2 -r 48c582067cb9 src/HOL/Library/Sublist.thy
--- a/src/HOL/Library/Sublist.thy Thu Jun 26 13:21:34 2014 +0200
+++ b/src/HOL/Library/Sublist.thy Thu Jun 26 13:24:41 2014 +0200
@@ -435,6 +435,14 @@
| list_emb_Cons [intro] : "list_emb P xs ys \<Longrightarrow> list_emb P xs (y#ys)"
| list_emb_Cons2 [intro]: "P x y \<Longrightarrow> list_emb P xs ys \<Longrightarrow> list_emb P (x#xs) (y#ys)"
+lemma list_emb_mono:
+ assumes "\<And>x y. P x y \<longrightarrow> Q x y"
+ shows "list_emb P xs ys \<longrightarrow> list_emb Q xs ys"
+proof
+ assume "list_emb P xs ys"
+ then show "list_emb Q xs ys" by (induct) (auto simp: assms)
+qed
+
lemma list_emb_Nil2 [simp]:
assumes "list_emb P xs []" shows "xs = []"
using assms by (cases rule: list_emb.cases) auto
-------------- next part --------------
# HG changeset patch
# Parent f07fe64d9f213111884a94ed031a36c93a2c222a
no built-in reflexivity of list embedding (which is more standard; now embedding is reflexive whenever the base-order is)
diff -r f07fe64d9f21 -r e574ed0a99d2 src/HOL/Library/Sublist.thy
--- a/src/HOL/Library/Sublist.thy Thu Jun 26 13:15:21 2014 +0200
+++ b/src/HOL/Library/Sublist.thy Thu Jun 26 13:21:34 2014 +0200
@@ -433,15 +433,16 @@
where
list_emb_Nil [intro, simp]: "list_emb P [] ys"
| list_emb_Cons [intro] : "list_emb P xs ys \<Longrightarrow> list_emb P xs (y#ys)"
-| list_emb_Cons2 [intro]: "P\<^sup>=\<^sup>= x y \<Longrightarrow> list_emb P xs ys \<Longrightarrow> list_emb P (x#xs) (y#ys)"
+| list_emb_Cons2 [intro]: "P x y \<Longrightarrow> list_emb P xs ys \<Longrightarrow> list_emb P (x#xs) (y#ys)"
lemma list_emb_Nil2 [simp]:
assumes "list_emb P xs []" shows "xs = []"
using assms by (cases rule: list_emb.cases) auto
-lemma list_emb_refl [simp, intro!]:
- "list_emb P xs xs"
- by (induct xs) auto
+lemma list_emb_refl:
+ assumes "\<And>x. x \<in> set xs \<Longrightarrow> P x x"
+ shows "list_emb P xs xs"
+ using assms by (induct xs) auto
lemma list_emb_Cons_Nil [simp]: "list_emb P (x#xs) [] = False"
proof -
@@ -463,7 +464,7 @@
lemma list_emb_ConsD:
assumes "list_emb P (x#xs) ys"
- shows "\<exists>us v vs. ys = us @ v # vs \<and> P\<^sup>=\<^sup>= x v \<and> list_emb P xs vs"
+ shows "\<exists>us v vs. ys = us @ v # vs \<and> P x v \<and> list_emb P xs vs"
using assms
proof (induct x \<equiv> "x # xs" ys arbitrary: x xs)
case list_emb_Cons
@@ -482,7 +483,7 @@
next
case (Cons x xs)
then obtain us v vs where
- zs: "zs = us @ v # vs" and p: "P\<^sup>=\<^sup>= x v" and lh: "list_emb P (xs @ ys) vs"
+ zs: "zs = us @ v # vs" and p: "P x v" and lh: "list_emb P (xs @ ys) vs"
by (auto dest: list_emb_ConsD)
obtain sk\<^sub>0 :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" and sk\<^sub>1 :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
sk: "\<forall>x\<^sub>0 x\<^sub>1. \<not> list_emb P (xs @ x\<^sub>0) x\<^sub>1 \<or> sk\<^sub>0 x\<^sub>0 x\<^sub>1 @ sk\<^sub>1 x\<^sub>0 x\<^sub>1 = x\<^sub>1 \<and> list_emb P xs (sk\<^sub>0 x\<^sub>0 x\<^sub>1) \<and> list_emb P x\<^sub>0 (sk\<^sub>1 x\<^sub>0 x\<^sub>1)"
@@ -518,21 +519,21 @@
next
case (list_emb_Cons xs ys y)
from list_emb_ConsD [OF `list_emb P (y#ys) zs`] obtain us v vs
- where zs: "zs = us @ v # vs" and "P\<^sup>=\<^sup>= y v" and "list_emb P ys vs" by blast
+ where zs: "zs = us @ v # vs" and "P y v" and "list_emb P ys vs" by blast
then have "list_emb P ys (v#vs)" by blast
then have "list_emb P ys zs" unfolding zs by (rule list_emb_append2)
from list_emb_Cons.IH [OF this] and list_emb_Cons.prems show ?case by simp
next
case (list_emb_Cons2 x y xs ys)
from list_emb_ConsD [OF `list_emb P (y#ys) zs`] obtain us v vs
- where zs: "zs = us @ v # vs" and "P\<^sup>=\<^sup>= y v" and "list_emb P ys vs" by blast
+ where zs: "zs = us @ v # vs" and "P y v" and "list_emb P ys vs" by blast
with list_emb_Cons2 have "list_emb P xs vs" by simp
- moreover have "P\<^sup>=\<^sup>= x v"
+ moreover have "P 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 list_emb_Cons2 by simp_all
ultimately show ?thesis
- using `P\<^sup>=\<^sup>= x y` and `P\<^sup>=\<^sup>= y v` and assms
+ using `P x y` and `P y v` and assms
by blast
qed
ultimately have "list_emb P (x#xs) (v#vs)" by blast
@@ -635,7 +636,7 @@
{ fix us vs assume "xs=x#us" "ys=x#vs" then have ?case using list_emb_Cons2 by auto}
moreover
{ fix us assume "xs=x#us" "ys=[]" then have ?case using list_emb_Cons2(2) by bestsimp }
- ultimately show ?case using `op =\<^sup>=\<^sup>= x y` by (auto simp: Cons_eq_append_conv)
+ ultimately show ?case using `op = x y` by (auto simp: Cons_eq_append_conv)
qed }
moreover assume ?l
ultimately show ?r by blast
-------------- next part --------------
list_emb
list_emb_refl
list_emb_mono
add
More information about the isabelle-dev
mailing list