[isabelle-dev] [isabelle] Theory Prefix_Order
Christian Sternagel
c.sternagel at gmail.com
Tue Oct 21 16:28:25 CEST 2014
(moved from isabelle-users since I'm referring to the development
versions of Isabelle and the AFP below)
Dear Julian,
unexpectedly I found some time to have a look earlier.
First, the "naming layer" provided by the "lemmas" statements in
Prefix_Order is there to keep compatibility with some AFP entries.
(There are mainly two naming schemes around, either "Peq" "P" for weak
and strict part of an order or "P" and "strict_P" for the same; and
Sublist uses the former, while some AFP entries use the latter.)
I think (without trying, however) your suggested changes would break
some AFP entries.
Instead I suggest the attached changes (the order of patches is to be
found in "series") which are tested against
Isabelle: 9239a33935c6 and
AFP: 42be0138cfe5
Thanks for spotting this.
cheers
chris
On 10/20/2014 05:00 PM, Julian Brunner wrote:
> Dear all,
>
> I've stumbled upon a few issues with the theory
> Library/Prefix_Order.thy. This theory instantiates the order type
> class for lists like this:
>
> definition "(xs::'a list) <= ys == prefixeq xs ys"
> definition "(xs::'a list) < ys == xs <= ys & Not (ys <= xs)"
>
> It then goes on to lift theorems about the constants 'prefixeq' and
> 'prefix' to the constants 'op <=' and 'op <', adding simp/intro/elim
> attributes in the process. However, a few things seem to have gone
> wrong here. First off, we have:
>
> lemmas prefixI [intro?] = prefixeqI [folded less_eq_list_def]
> lemmas strict_prefixI [intro?] = prefixI [folded less_list_def]
>
> The first line hides the fact Sublist.prefixI, so the theorem declared
> in the second line is just a duplicate of the one in the first and the
> 'folded less_list_def' attribute is applied in vain.
>
> However, even when using the fully qualified fact Sublist.prefixI, it
> doesn't work the way I assume it was intended to, since 'op <' is not
> defined in terms of 'prefix', so the 'folded less_list_def' attribute
> still doesn't apply.
>
> Attached are my attempts at fixing these and a few other issues.
> Please let me know if I should have posted this on the developer
> mailing list.
>
> Cheers,
> Julian
>
-------------- next part --------------
# HG changeset patch
# Parent d5b36d47d92dfbeebeb5f2e86889296cabdbc457
dropped duplicate fact
diff -r d5b36d47d92d -r 1541b682d41d src/HOL/Library/Sublist.thy
--- a/src/HOL/Library/Sublist.thy Tue Oct 21 14:27:28 2014 +0200
+++ b/src/HOL/Library/Sublist.thy Tue Oct 21 14:30:02 2014 +0200
@@ -396,29 +396,6 @@
lemma suffixeq_take: "suffixeq xs ys \<Longrightarrow> ys = take (length ys - length xs) ys @ xs"
by (auto elim!: suffixeqE)
-lemma suffixeq_suffix_reflclp_conv: "suffixeq = suffix\<^sup>=\<^sup>="
-proof (intro ext iffI)
- fix xs ys :: "'a list"
- assume "suffixeq xs ys"
- show "suffix\<^sup>=\<^sup>= xs ys"
- proof
- assume "xs \<noteq> ys"
- with `suffixeq xs ys` show "suffix xs ys"
- by (auto simp: suffixeq_def suffix_def)
- qed
-next
- fix xs ys :: "'a list"
- assume "suffix\<^sup>=\<^sup>= xs ys"
- then show "suffixeq xs ys"
- proof
- assume "suffix xs ys" then show "suffixeq xs ys"
- by (rule suffix_imp_suffixeq)
- next
- assume "xs = ys" then show "suffixeq xs ys"
- by (auto simp: suffixeq_def)
- qed
-qed
-
lemma suffix_reflclp_conv: "suffix\<^sup>=\<^sup>= = suffixeq"
by (intro ext) (auto simp: suffixeq_def suffix_def)
@@ -508,7 +485,7 @@
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
+ using assms and list_emb_suffix unfolding suffix_reflclp_conv [symmetric] by auto
lemma list_emb_length: "list_emb P xs ys \<Longrightarrow> length xs \<le> length ys"
by (induct rule: list_emb.induct) auto
-------------- next part --------------
# HG changeset patch
# Parent e8ecc79aee432d084a1539f69bb95a656f4140fd
move facts about parallel to corresponding document section
diff -r e8ecc79aee43 -r d5b36d47d92d src/HOL/Library/Sublist.thy
--- a/src/HOL/Library/Sublist.thy Mon Oct 20 18:33:14 2014 +0200
+++ b/src/HOL/Library/Sublist.thy Tue Oct 21 14:27:28 2014 +0200
@@ -261,6 +261,46 @@
lemma parallel_commute: "a \<parallel> b \<longleftrightarrow> b \<parallel> a"
unfolding parallel_def by auto
+lemma parallelD1: "x \<parallel> y \<Longrightarrow> \<not> prefixeq x y"
+ by blast
+
+lemma parallelD2: "x \<parallel> y \<Longrightarrow> \<not> prefixeq y x"
+ by blast
+
+lemma parallel_Nil1 [simp]: "\<not> x \<parallel> []"
+ unfolding parallel_def by simp
+
+lemma parallel_Nil2 [simp]: "\<not> [] \<parallel> x"
+ unfolding parallel_def by simp
+
+lemma Cons_parallelI1: "a \<noteq> b \<Longrightarrow> a # as \<parallel> b # bs"
+ by auto
+
+lemma Cons_parallelI2: "\<lbrakk> a = b; as \<parallel> bs \<rbrakk> \<Longrightarrow> a # as \<parallel> b # bs"
+ by (metis Cons_prefixeq_Cons parallelE parallelI)
+
+lemma not_equal_is_parallel:
+ assumes neq: "xs \<noteq> ys"
+ and len: "length xs = length ys"
+ shows "xs \<parallel> ys"
+ using len neq
+proof (induct rule: list_induct2)
+ case Nil
+ then show ?case by simp
+next
+ case (Cons a as b bs)
+ have ih: "as \<noteq> bs \<Longrightarrow> as \<parallel> bs" by fact
+ show ?case
+ proof (cases "a = b")
+ case True
+ then have "as \<noteq> bs" using Cons by simp
+ then show ?thesis by (rule Cons_parallelI2 [OF True ih])
+ next
+ case False
+ then show ?thesis by (rule Cons_parallelI1)
+ qed
+qed
+
subsection {* Suffix order on lists *}
@@ -379,46 +419,6 @@
qed
qed
-lemma parallelD1: "x \<parallel> y \<Longrightarrow> \<not> prefixeq x y"
- by blast
-
-lemma parallelD2: "x \<parallel> y \<Longrightarrow> \<not> prefixeq y x"
- by blast
-
-lemma parallel_Nil1 [simp]: "\<not> x \<parallel> []"
- unfolding parallel_def by simp
-
-lemma parallel_Nil2 [simp]: "\<not> [] \<parallel> x"
- unfolding parallel_def by simp
-
-lemma Cons_parallelI1: "a \<noteq> b \<Longrightarrow> a # as \<parallel> b # bs"
- by auto
-
-lemma Cons_parallelI2: "\<lbrakk> a = b; as \<parallel> bs \<rbrakk> \<Longrightarrow> a # as \<parallel> b # bs"
- by (metis Cons_prefixeq_Cons parallelE parallelI)
-
-lemma not_equal_is_parallel:
- assumes neq: "xs \<noteq> ys"
- and len: "length xs = length ys"
- shows "xs \<parallel> ys"
- using len neq
-proof (induct rule: list_induct2)
- case Nil
- then show ?case by simp
-next
- case (Cons a as b bs)
- have ih: "as \<noteq> bs \<Longrightarrow> as \<parallel> bs" by fact
- show ?case
- proof (cases "a = b")
- case True
- then have "as \<noteq> bs" using Cons by simp
- then show ?thesis by (rule Cons_parallelI2 [OF True ih])
- next
- case False
- then show ?thesis by (rule Cons_parallelI1)
- qed
-qed
-
lemma suffix_reflclp_conv: "suffix\<^sup>=\<^sup>= = suffixeq"
by (intro ext) (auto simp: suffixeq_def suffix_def)
-------------- next part --------------
# HG changeset patch
# Parent e6e47becd94bf8396180fbc4891af645adff4434
base "less" of order instance on "prefix"
diff -r e6e47becd94b -r 269953ee1f56 src/HOL/Library/Prefix_Order.thy
--- a/src/HOL/Library/Prefix_Order.thy Tue Oct 21 14:34:22 2014 +0200
+++ b/src/HOL/Library/Prefix_Order.thy Tue Oct 21 14:42:36 2014 +0200
@@ -12,9 +12,9 @@
begin
definition "(xs::'a list) \<le> ys \<equiv> prefixeq xs ys"
-definition "(xs::'a list) < ys \<equiv> xs \<le> ys \<and> \<not> (ys \<le> xs)"
+definition "(xs::'a list) < ys \<equiv> prefix xs ys"
-instance by (default, unfold less_eq_list_def less_list_def) auto
+instance by (default, unfold less_eq_list_def less_list_def prefix_def) auto
end
-------------- next part --------------
# HG changeset patch
# Parent 269953ee1f5625ff0f24949bff30662a43baad13
use qualified fact names due to shadowing
diff -r 269953ee1f56 -r 9239a33935c6 src/HOL/Library/Prefix_Order.thy
--- a/src/HOL/Library/Prefix_Order.thy Tue Oct 21 14:42:36 2014 +0200
+++ b/src/HOL/Library/Prefix_Order.thy Tue Oct 21 14:51:15 2014 +0200
@@ -22,8 +22,8 @@
lemmas prefixE [elim?] = prefixeqE [folded less_eq_list_def]
lemmas strict_prefixI' [intro?] = prefixI' [folded less_list_def]
lemmas strict_prefixE' [elim?] = prefixE' [folded less_list_def]
-lemmas strict_prefixI [intro?] = prefixI [folded less_list_def]
-lemmas strict_prefixE [elim?] = prefixE [folded less_list_def]
+lemmas strict_prefixI [intro?] = Sublist.prefixI [folded less_list_def]
+lemmas strict_prefixE [elim?] = Sublist.prefixE [folded less_list_def]
theorems Nil_prefix [iff] = Nil_prefixeq [folded less_eq_list_def]
theorems prefix_Nil [simp] = prefixeq_Nil [folded less_eq_list_def]
lemmas prefix_snoc [simp] = prefixeq_snoc [folded less_eq_list_def]
-------------- next part --------------
par
dup
uni
prefix
qual
-------------- next part --------------
# HG changeset patch
# Parent 1541b682d41d9c0d4518d241c50b3105799b42bd
prefer unicode symbols
diff -r 1541b682d41d -r e6e47becd94b src/HOL/Library/Sublist_Order.thy
--- a/src/HOL/Library/Sublist_Order.thy Tue Oct 21 14:30:02 2014 +0200
+++ b/src/HOL/Library/Sublist_Order.thy Tue Oct 21 14:34:22 2014 +0200
@@ -39,12 +39,12 @@
show "xs \<le> xs" by (simp add: less_eq_list_def)
next
fix xs ys :: "'a list"
- assume "xs <= ys" and "ys <= xs"
+ assume "xs \<le> ys" and "ys \<le> xs"
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 sublisteq_trans)
+ assume "xs \<le> ys" and "ys \<le> zs"
+ thus "xs \<le> zs" by (unfold less_eq_list_def) (rule sublisteq_trans)
qed
lemmas less_eq_list_induct [consumes 1, case_names empty drop take] =
More information about the isabelle-dev
mailing list