Email Gateway (Dec 12 2022 at 16:09): Email Gateway (Dec 12 2022 at 16:09):From: Peter Lammich <lammich@in.tum.de>
Hi List,
any reason why the HOL Multiset theory leaves the lifting setup for
Multisets open?
Whenever I want to do lift-definition/transfer setup that contain types
based on Multisets (heaps in my case), I have to explicitly state
lifting_forget multiset.lifting
in order to avoid the transfer proof method to transfer too far (down to
the 'a=>nat representation of multisets).
Any reason why not to forget this lifting at the end of Multiset.thy?
Email Gateway (Dec 13 2022 at 08:17):From: "\"Blanchette, J.C. (Jasmin Christian)\"" <cl-isabelle-users@lists.cam.ac.uk>
Hi Peter,
I'm not aware of any reason why this forgetting isn't done. It was probably forgotten. ;) I'm testing a change on testboard.
Cheers,
Jasmin
Email Gateway (Dec 16 2022 at 10:14):From: "\"Blanchette, J.C. (Jasmin Christian)\"" <cl-isabelle-users@lists.cam.ac.uk>
Hi Peter,
I just tried forgetting the multiset lifting and this causes problems in five AFP entries: Linear_Recurrences, Factor_Algebraic_Polynomial, Pi_Transcendental, Power_Sum_Polynomials, and Nested_Multisets_Ordinals.
I tried to fix Nested_Multisets_Ordinals (which I coauthored) but it really seems to rely on the multiset lifting being in place (and just calling "setup_lifting type_definition_multiset" wasn't enough to repair things). I don't understand lifting well enough to know what's the best course of action. What do you think?
Cheers,
Jasmin
Email Gateway (Dec 16 2022 at 11:59):From: Dmitriy Traytel <traytel@di.ku.dk>
Hi Jasmin,
From isar-ref
“The command lifting_forget τ.lifting deletes set-up of the Lifting package for τ and deletes all the transfer rules that were introduced by lift_definition using τ as an abstract type.
The stored set-up in a bundle can be reintroduced by the Isar commands for including a bundle (include, includes and including).”
You can also “unbundle” the bundle globally at the beginning of a theory that needs the lifting setup and “lifting_update” and “lifting_forget" it again at the end.
Hope that helps,
Dmitriy
Email Gateway (Dec 19 2022 at 16:20):From: "\"Blanchette, J.C. (Jasmin Christian)\"" <cl-isabelle-users@lists.cam.ac.uk>
Hi Dmitriy,
Thanks for your explanations. Unfortunately, after adding "lifting_forget" at the end of "Multiset.thy", I get errors in the AFP file as before ("Nested_Multisets_Ordinals/Signed_Multiset.thy"): Before, the error was on a "lift_definition", and after adding "unbundle multiset.lifting" to the top of that file, the error is a few lines below on a "transfer" call.
Maybe we could debug this offline?
Cheers,
Jasmin
Email Gateway (Dec 21 2022 at 16:36):From: "\"Blanchette, J.C. (Jasmin Christian)\"" <cl-isabelle-users@lists.cam.ac.uk>
Hi Peter,
With Dmitriy's help, I was able to fix this in the development version of Isabelle and the AFP. Thanks for your report.
Cheers,
Jasmin
Last updated: Apr 25 2024 at 20:15 UTC