Re: [isabelle-dev] Simplification theorems with more general typeclasses

For the record, I have now pushed the change to Isabelle, see http://isabelle.in.tum.de/reports/Isabelle/rev/3365c8ec67bd . Mathias > On 05 Jul 2016, at 14:03, Mathias Fleury wrote: > > Hi all, > >

Re: [isabelle-dev] Simplification theorems with more general typeclasses

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

Re: [isabelle-dev] Simplification theorems with more general typeclasses

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

Re: [isabelle-dev] Simplification theorems with more general typeclasses

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

[isabelle-dev] Simplification theorems with more general typeclasses

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