<html><head><meta http-equiv="Content-Type" content="text/html charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class="">Hi all,<div class=""><br class=""></div><div class="">after some more experiments, I found out that there is another difference between explicit typeclass annotations and lemmas in the context: the former theorems are included in instantiations but are not included in interpretations. This usually does not make a difference, since there is usually a single order on a type.</div><div class=""><br class=""></div><div class="">Instead, I introduced an additional typeclass to the hierarchy. The change was successfully tested on testboard (<a href="http://isabelle.in.tum.de/repos/testboard/rev/18f26b6779ad" class="">mercurial diff</a>, <a href="https://ci.isabelle.systems/jenkins/job/testboard/117/" class="">status</a>), and does not need any AFP change.</div><div class=""><br class=""></div><div class=""><br class=""></div><div class="">Does someone have an opinion on this change?</div><div class=""><br class=""></div><div class=""><br class=""></div><div class="">Mathias</div><div class=""> <br class=""><div><blockquote type="cite" class=""><div class="">On 04 Jul 2016, at 14:20, Mathias Fleury <<a href="mailto:Mathias.Fleury@ens-rennes.fr" class="">Mathias.Fleury@ens-rennes.fr</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><meta http-equiv="Content-Type" content="text/html charset=utf-8" class=""><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class="">Hi Johannes,<div class=""><br class=""></div><div class=""><br class=""></div><div class="">the multiset ordering (contrary to the subset ordering) does not have this property:</div><div class=""><br class=""></div><div class=""><div class=""><span class="Apple-tab-span" style="white-space:pre"> </span><font face="Monaco" class="">lemma "{#0#} <= {#Suc 0#}”</font></div><div class=""><font face="Monaco" class=""><span class="Apple-tab-span" style="white-space:pre"> </span> unfolding Multiset_Order.le_multiset⇩H⇩O by auto</font></div><div class=""><br class=""></div><div class="">(the actual notation is <span style="font-family: Monaco;" class="">#⊆# and not <=).</span></div><div class=""><br class=""></div><div class=""><br class=""></div><div class="">I tried locally to apply the changes of my previous email this week-end. Except some proofs inside the typeclass definitions (i.e. in the files <font face="Monaco" class="">Groups.thy</font>, <font face="Monaco" class="">Rings.thy</font>, and <font face="Monaco" class="">Missing_Ring.thy</font>), no other changes were needed in Isabelle or the AFP.</div><div class=""><br class=""></div><div class=""><br class=""></div><div class="">Thanks for your answer,</div><div class="">Mathias</div><div class=""><br class=""></div><div class=""><br class=""></div><div class=""><blockquote type="cite" class=""><div class="">On 04 Jul 2016, at 13:22, Johannes Hölzl <<a href="mailto:hoelzl@in.tum.de" class="">hoelzl@in.tum.de</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div class="">Hi Mathias,<br class=""><br class="">there is at least the type class 'canonically_ordered_monoid' which has<br class="">the property a <= b <--> ?c. a + c = b which implies 0 <= a for all a.<br class="">Are the multisets already in this typeclass?<br class=""><br class=""> - Johannes<br class=""><br class=""><br class="">Am Dienstag, den 28.06.2016, 10:04 +0100 schrieb Mathias Fleury:<br class=""><blockquote type="cite" class="">Dear type-classes and simplifier experts,<br class=""><br class="">in the plan of instantiating multisets with the multiset ordering, I<br class="">am trying to instantiate the multisets with additional typeclasses to<br class="">get specific simplification theorems. The aim is to mimic the<br class="">simplifier’s behaviour of other types like natural numbers. One of my<br class="">problems can be nicely illustrated by the following lemma: “M <= M +<br class="">N <-> 0 <= N”. <br class=""><br class=""><br class="">Analog simplification rules already exist for rings (e.g., natural<br class="">numbers*) and ordered groups too:<br class=""><span class="Apple-tab-span" style="white-space:pre"> </span>thm<br class="">Rings.linordered_semiring_class.less_eq_add_cancel_left_greater_eq_ze<br class="">ro<br class=""><span class="Apple-tab-span" style="white-space:pre"> </span>thm Groups.ordered_ab_group_add_class.le_add_same_cancel1<br class="">Both rules are stating that “M <= M + N <—> 0 <= N” and are marked as<br class="">[simp].<br class=""><br class=""><br class="">However, the multisets are neither a group (no inverse for the law<br class="">“+”) nor a ring (no multiplication). I could duplicate the theorems,<br class="">but I noticed that the proofs of the theorems do only rely on the<br class="">fact it is a monoid_add (for the zero element) and an<br class="">ordered_ab_semigroup_add_imp_le (for the order). The following<br class="">theorem would work too and is general enough to include the multiset<br class="">case:<br class=""><br class="">lemma le_add_same_cancel1 [simp]:<br class=""> “(a :: 'a :: {monoid_add, ordered_ab_semigroup_add_imp_le}) ≤ a + b<br class="">⟷ 0 ≤ b”<br class=""> using add_le_cancel_left [of a 0] by simp<br class=""><br class=""><br class="">Are there any obvious differences between this more general version<br class="">with explicit type class annotations<br class="">and Groups.ordered_ab_group_add_class.le_add_same_cancel1? If no,<br class="">would it make sense to use this version in Isabelle?<br class=""><br class=""><br class=""><br class="">Thanks in advance,<br class="">Mathias Fleury<br class=""><br class=""><br class=""><br class=""><br class="">* for natural numbers, the simproc<br class="">Numeral_Simprocs.natle_cancel_numerals is able to do it too.<br class="">_______________________________________________<br class="">isabelle-dev mailing list<br class=""><a href="mailto:isabelle-dev@in.tum.de" class="">isabelle-dev@in.tum.de</a><br class=""><a href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel" class="">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel</a><br class="">le-dev<br class=""></blockquote>_______________________________________________<br class="">isabelle-dev mailing list<br class=""><a href="mailto:isabelle-dev@in.tum.de" class="">isabelle-dev@in.tum.de</a><br class=""><a href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev" class="">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a><br class=""></div></div></blockquote></div><br class=""></div></div>_______________________________________________<br class="">isabelle-dev mailing list<br class=""><a href="mailto:isabelle-dev@in.tum.de" class="">isabelle-dev@in.tum.de</a><br class="">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev<br class=""></div></blockquote></div><br class=""></div></body></html>