Re: [isabelle-dev] [isabelle] Theory Prefix_Order
Dear Christian, Yes, I haven't considered AFP entries or anything, this was just my personal hack to get it to work for my theories. I'll adjust the names in my theories to whatever you see fit for Prefix_Order. However, it seems like there is still an issue. The lemma "strict_prefixI" gets unfolded from "prefixeq ?xs ?ys ⟹ ?xs ≠ ?ys ⟹ prefix ?xs ?ys" to "prefixeq ?xs ?ys ⟹ ?xs ≠ ?ys ⟹ ?xs < ?ys". My guess is that it should be unfolded completely to "?xs ≤ ?ys ⟹ ?xs ≠ ?ys ⟹ ?xs < ?ys". For this to happen, the attribute "folded less_eq_list_def less_list_def" has to be used instead of just "folded less_list_def". The lemma "strict_prefixE" behaves the same. Cheers, Julian On Tue, Oct 21, 2014 at 4:28 PM, Christian Sternagel wrote: > (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 >> > ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] Theory Prefix_Order
(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 # 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 \ 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 \ 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 \ length xs \ length ys" by (induct rule: list_emb.induct) auto # 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 \ b \ b \ a" unfolding parallel_def by auto +lemma parallelD1: "x \ y \ \ prefixeq x y" + by blast + +lemma parallelD2: "x \ y \ \ prefixeq y x" + by blast + +lemma parallel_Nil1 [simp]: "\ x \ []" + unfolding parallel_def by simp + +lemma parallel_Nil2 [simp]: "\ [] \ x" + unfolding parallel_def by simp + +lemma Cons_parallelI1: "a \ b \ a # as \ b # bs" + by auto + +lemma Cons_parallelI2: "\ a = b; as \ bs \ \ a # as \ b # bs" + by (metis Cons_prefixeq_Cons parallelE parallelI) + +lemma not_equal_is_parallel: + assumes neq: "xs \ ys" +and len: "length xs = length ys" + shows "xs \ 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 \ bs \ as \ bs" by fact + show ?case + proof (cases "a = b") +case True +then have "as \ bs" using Cons by simp +then show ?thesis by (rule Cons_parallelI2 [OF Tru
