[isabelle-dev] Simplification theorems with more general typeclasses

[Mathias Fleury]

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.Fleury at 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.Fleury at ens-rennes.fr <mailto:Mathias.Fleury at 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 <hoelzl at in.tum.de <mailto:hoelzl at 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-dev at in.tum.de <mailto:isabelle-dev at 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-dev at in.tum.de <mailto:isabelle-dev at 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-dev at in.tum.de <mailto:isabelle-dev at in.tum.de>
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160712/708004da/attachment-0002.html>