Email Gateway (Aug 22 2022 at 20:00): Email Gateway (Aug 22 2022 at 20:00):From: Alexander Maletzky <Alexander.Maletzky@risc-software.at>
Dear list,
I’m currently preparing a new AFP entry about Hilbert’s Nullstellensatz, in which I’d like to make use of the “types-to-sets” approach.
However, I don’t know the current status of this (still experimental?) approach, and whether it can/should be part of AFP entries. Namely, although importing “HOL-Types_To_Sets.Types_To_Sets” in my theory and processing it with Isabelle/jEdit works fine, I’m having trouble to properly set up the ROOT file of the session:
chapter AFP
session Nullstellensatz (AFP) = Groebner_Bases + “HOL-Types_To_Sets” + ...
makes Isabelle complain about the “Types_To_Sets” part.
So, my question is: Can/should one use “types-to-sets” in AFP entries, and if yes, how?
If the answer is “no” it’s not a big problem, because I only need “types-to-sets” for proving the field-theoretic version of the Nullstellensatz from its (more important and better-known) geometric version. This is probably not so important and could thus be omitted.
Thank you and best regards,
Alexander
Email Gateway (Aug 22 2022 at 20:00):From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear Alexander,
I don’t see a problem with using Types_To_Sets in AFP-entries,
in fact it is already used in some AFP entries (e.g., Perron-Frobenius, Berlekamp-Zassenhaus).
A corresponding ROOT file in your case might look like:
chapter AFP
session "Nullstellensatz" (AFP) = Groebner_Bases +
sessions
"HOL-Types_To_Sets"
theories [document = false]
"HOL-Types_To_Sets.Types_To_Sets”
theories
Your_Own_Theories
Best,
René
signature.asc
Email Gateway (Aug 22 2022 at 20:00):From: Andrei Popescu <A.Popescu@mdx.ac.uk>
Hi Alexander,
There is no problem with using Types-to-Sets in AFP entries. For example, this entry uses it: https://www.isa-afp.org/entries/Perron_Frobenius.html. You can have a look at its ROOT file.
Best wishes,
Andrei
Email Gateway (Aug 22 2022 at 20:00):From: Alexander Maletzky <Alexander.Maletzky@risc-software.at>
Dear René and Andrei,
thanks a lot for your answer. I did a quick search in the AFP for occurrences of „types-to-sets“ and didn’t find anything, but apparently my search was bit too quick …
Best regards,
Alexander
Email Gateway (Aug 22 2022 at 20:00):From: Lars Hupel <hupel@in.tum.de>
Note that session-qualified theories are never part of the document, so
listing them as "[document = false]", or even listing them in the "ROOT"
file at all, is redundant.
Cheers
Lars
Email Gateway (Aug 22 2022 at 20:00):From: Lars Hupel <hupel@in.tum.de>
chapter AFP
session Nullstellensatz (AFP) = Groebner_Bases + “HOL-Types_To_Sets” + ...
Merging multiple sessions works for no session: this is not special to
"types-to-sets".
Others have already pointed out that you can use session imports in the
"ROOT" file in order to combine theories from multiple sessions. The
rule of thumb is that you should declare the largest/slowest session as
parent, and import all others.
Cheers
Lars
Email Gateway (Aug 22 2022 at 20:00):From: Lawrence Paulson <lp15@cam.ac.uk>
It amazes me that anybody has figured this out. I can’t make any sense of what’s going on with Types-to-Sets, even when pointed to the exact line where it is being used. Some documentation is well overdue.
Larry Paulson
Email Gateway (Aug 22 2022 at 20:00):From: Alexander Maletzky <Alexander.Maletzky@risc-software.at>
Dear Lars,
thanks for clarifying this. Actually, I have to admit that I’m not very experienced with setting up ROOT files properly; I mainly copy-paste from existing sessions and hope all works well ...
Best,
Alexander
Merging multiple sessions works for no session: this is not special to
"types-to-sets".
Others have already pointed out that you can use session imports in the
"ROOT" file in order to combine theories from multiple sessions. The
rule of thumb is that you should declare the largest/slowest session as
parent, and import all others.
Cheers
Lars
Email Gateway (Aug 22 2022 at 20:01):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
Dear All,
I hope it is appropriate to make a side note on further development work of
Types-To-Sets. In the last several weeks I dedicated a nontrivial amount of
time towards the improvement of the functionality associated with the
package. At the moment, I am in the process of finalising my work on the
update of one of my own large scale application of the Types-To-Sets (
https://github.com/xanonec/HOL-Types_To_Sets_Ext) using the improved
framework and, also, writing a user manual for it. *However, none of the
work that I am referring to is publicly available at the moment.*
To this end, I provided several Isar commands that make the framework much
more convenient to use and, also, drastically reduce the amount of
boilerplate code that was previously needed.
In particular, it is now possible to write
locale preorder_ow =
ord_ow 𝔘 le ls
for 𝔘 :: "'ao set" and le (infix "≤⇩o⇩w" 50) and ls (infix "<⇩o⇩w" 50) +
assumes less_le_not_le:
"⟦ x ∈ 𝔘; y ∈ 𝔘 ⟧ ⟹ x <⇩o⇩w y ⟷ x ≤⇩o⇩w y ∧ ¬ (y ≤⇩o⇩w x)"
and order_refl[iff]: "x ∈ 𝔘 ⟹ x ≤⇩o⇩w x"
and order_trans: "⟦ x ∈ 𝔘; y ∈ 𝔘; z ∈ 𝔘; x ≤⇩o⇩w y; y ≤⇩o⇩w z ⟧ ⟹ x
≤⇩o⇩w z"
(* The relativized definitions and transfer rules still need to be provided
manually. However, the framework does not utilise the locale local_typedef
and other tools associated with it. Once the transfer rules are proven, it
is sufficient to write: *)
context preorder_ow
begin
tts_relativize
types: (?'a 𝔘) (*target type for the relativization and the associated
carrier set*)
substituting preorder_ow_axioms
applying [unfolded implicit_ord, var_simplified ne_simp, simplified]
(*this part is optional - it merely applies a list of attributes after the
relativization is complete*)
in
ne_transp_less = transp_less and
ne_transp_le = transp_le and (...)
(* other theorems...
the names of the relativized facts can be generated automatically and
support for partial relativization is also provided *)
The command also saves the outcome of the relativization in a database and
the framework provides various diagnostic commands. For example, it is now
possible to see a list of theorems that have not been relativised yet for a
given type constructor or a given axiomatic type class by writing something
similar to
tts_statistics sort Orderings.preorder
It is very likely that I will finish the work that I was planning before
the end of the next week and make the tool publicly available through my
repository. However, if anyone is interested in trying out the current
version, I can send it privately within a day or so.
Thank you
Email Gateway (Aug 22 2022 at 20:01):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
Dear All,
Unfortunately, I forgot to attach a screenshot to my previous post (please
note that I never tried submitting any attachments to this mailing list and
I can only hope that it will get uploaded correctly).
Thank you
TTS_application.png
Email Gateway (Aug 22 2022 at 20:01):From: Andrei Popescu <A.Popescu@mdx.ac.uk>
Dear Anonymous,
I can confirm that the screenshot attachment has been received in my mailbox. This looks like very nice work -- myself, I'd be happy to try it when it is ready.
Best wishes,
Andrei
Last updated: Apr 19 2024 at 04:17 UTC