Email Gateway (Aug 22 2022 at 13:33): Email Gateway (Aug 22 2022 at 13:33):From: Tobias Nipkow <nipkow@in.tum.de>
Dear Stanislav,
I had a similar problem when checking some objects that came out of the Kepler
conjecture proof where I had 5 definitions of lists of (in total) 20.000 graphs.
Isabelle choked on those when inputting them as an HOL definition. This is what
I did instead:
I first defined those lists in ML files so they could be read by by the
PolyML parser. Then I used some magic to import those ML definitions as HOL
definitions. Here is the magic code:
http://www.isa-afp.org/browser_info/current/AFP/Flyspeck-Tame/Arch.html
Code_Runtime.polyml_as_definition performs that conversion. You would need to
adapt this to your own situation. It worked because the types used on the ML
existed on the HOL level: integers and lists.
To reduce the time to check the objects I wrote the checker in the executable
subset of HOL. The final theorems
http://www.isa-afp.org/browser_info/current/AFP/Flyspeck-Tame/ArchComp.html
were proved with "eval", a proof method that compiles executable theorems to ML
and runs them there, i.e. reduces them to true or false. (The fact that the
definitions were initially made in ML is orthogonal to the final proof by ML.)
Best
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 13:33):From: Makarius <makarius@sketis.net>
These numbers are not that big, but if you go through surface syntax of
Isabelle (the logical language, the theory and proof language, maybe
even just ML source language) it is likely to choke.
Note that the canonical way to import big things into an LCF-style
prover like Isabelle is to write some ML functions that do that, and
construct terms and proofs by internal means. Never ever generate source
that is then fed into the system.
Examples for reading external material can be seen in src/HOL/SPARK.
In such applications it is important to recall that surface syntax (for
input and output of end-user material) is really just the surface and
not the real system. E.g. the SPARK importer turned out incredible slow,
until someone pointed out that there is redundant output of intermediate
statements.
Makarius
Email Gateway (Aug 22 2022 at 13:34):From: Tobias Nipkow <nipkow@in.tum.de>
On 08/06/2016 15:01, Станислав Владимирович Моисеев wrote:
Dear Tobias and Makarius!
Thank you for your links and suggestions.Now I realize that it's better to import my objects to ML directly. I will
concentrate on this approach.I have a question regarding "eval" proof method.
If one uses "eval", what stack of code will one have to trust? Will the "trusted
base" be larger than that for proofs without "eval"?
Yes, you also need to trust the translation of HOL function definitions into ML
function definitions.
Tobias
If you can give any links discussing the topic of trusted code stack in theorem
provers (whether in case of "eval" method or not) — I would appreciate it.Thank you!
Stanislav.
Email Gateway (Aug 22 2022 at 13:34):From: Станислав Владимирович Моисе ев <stanislav.moiseev@gmail.com>
Dear Tobias and Makarius!
Thank you for your links and suggestions.
Now I realize that it's better to import my objects to ML directly. I will
concentrate on this approach.
I have a question regarding "eval" proof method.
If one uses "eval", what stack of code will one have to trust? Will the
"trusted base" be larger than that for proofs without "eval"?
If you can give any links discussing the topic of trusted code stack in
theorem provers (whether in case of "eval" method or not) — I would
appreciate it.
Thank you!
Stanislav.
Last updated: Nov 21 2024 at 12:39 UTC