For the record, I have now pushed the change to Isabelle, see http://isabelle.in.tum.de/reports/Isabelle/rev/3365c8ec67bd <http://isabelle.in.tum.de/reports/Isabelle/rev/3365c8ec67bd>.
Mathias > On 05 Jul 2016, at 14:03, Mathias Fleury <mathias.fle...@ens-rennes.fr> wrote: > > Hi all, > > 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. > > Instead, I introduced an additional typeclass to the hierarchy. The change > was successfully tested on testboard (mercurial diff > <http://isabelle.in.tum.de/repos/testboard/rev/18f26b6779ad>, status > <https://ci.isabelle.systems/jenkins/job/testboard/117/>), and does not need > any AFP change. > > > Does someone have an opinion on this change? > > > Mathias > >> On 04 Jul 2016, at 14:20, Mathias Fleury <mathias.fle...@ens-rennes.fr >> <mailto:mathias.fle...@ens-rennes.fr>> wrote: >> >> Hi Johannes, >> >> >> the multiset ordering (contrary to the subset ordering) does not have this >> property: >> >> lemma "{#0#} <= {#Suc 0#}” >> unfolding Multiset_Order.le_multiset⇩H⇩O by auto >> >> (the actual notation is #⊆# and not <=). >> >> >> 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 >> Groups.thy, Rings.thy, and Missing_Ring.thy), no other changes were needed >> in Isabelle or the AFP. >> >> >> Thanks for your answer, >> Mathias >> >> >>> On 04 Jul 2016, at 13:22, Johannes Hölzl <hoe...@in.tum.de >>> <mailto:hoe...@in.tum.de>> wrote: >>> >>> Hi Mathias, >>> >>> there is at least the type class 'canonically_ordered_monoid' which has >>> the property a <= b <--> ?c. a + c = b which implies 0 <= a for all a. >>> Are the multisets already in this typeclass? >>> >>> - Johannes >>> >>> >>> Am Dienstag, den 28.06.2016, 10:04 +0100 schrieb Mathias Fleury: >>>> Dear type-classes and simplifier experts, >>>> >>>> in the plan of instantiating multisets with the multiset ordering, I >>>> am trying to instantiate the multisets with additional typeclasses to >>>> get specific simplification theorems. The aim is to mimic the >>>> simplifier’s behaviour of other types like natural numbers. One of my >>>> problems can be nicely illustrated by the following lemma: “M <= M + >>>> N <-> 0 <= N”. >>>> >>>> >>>> Analog simplification rules already exist for rings (e.g., natural >>>> numbers*) and ordered groups too: >>>> thm >>>> Rings.linordered_semiring_class.less_eq_add_cancel_left_greater_eq_ze >>>> ro >>>> thm Groups.ordered_ab_group_add_class.le_add_same_cancel1 >>>> Both rules are stating that “M <= M + N <—> 0 <= N” and are marked as >>>> [simp]. >>>> >>>> >>>> However, the multisets are neither a group (no inverse for the law >>>> “+”) nor a ring (no multiplication). I could duplicate the theorems, >>>> but I noticed that the proofs of the theorems do only rely on the >>>> fact it is a monoid_add (for the zero element) and an >>>> ordered_ab_semigroup_add_imp_le (for the order). The following >>>> theorem would work too and is general enough to include the multiset >>>> case: >>>> >>>> lemma le_add_same_cancel1 [simp]: >>>> “(a :: 'a :: {monoid_add, ordered_ab_semigroup_add_imp_le}) ≤ a + b >>>> ⟷ 0 ≤ b” >>>> using add_le_cancel_left [of a 0] by simp >>>> >>>> >>>> Are there any obvious differences between this more general version >>>> with explicit type class annotations >>>> and Groups.ordered_ab_group_add_class.le_add_same_cancel1? If no, >>>> would it make sense to use this version in Isabelle? >>>> >>>> >>>> >>>> Thanks in advance, >>>> Mathias Fleury >>>> >>>> >>>> >>>> >>>> * for natural numbers, the simproc >>>> Numeral_Simprocs.natle_cancel_numerals is able to do it too. >>>> _______________________________________________ >>>> isabelle-dev mailing list >>>> isabelle-...@in.tum.de <mailto:isabelle-...@in.tum.de> >>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel >>>> <https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel> >>>> le-dev >>> _______________________________________________ >>> isabelle-dev mailing list >>> isabelle-...@in.tum.de <mailto:isabelle-...@in.tum.de> >>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev >>> <https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev> >> >> _______________________________________________ >> isabelle-dev mailing list >> isabelle-...@in.tum.de <mailto:isabelle-...@in.tum.de> >> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev