Email Gateway (Aug 19 2022 at 08:29): Email Gateway (Aug 19 2022 at 08:29):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Hi all,
Just out of curiosity, and because I guess this may be worth in some
circumstances, I wonder if there exist some recommended ways to add custom
obligations to Theory design and make them checked. I mean kind of style
check and design rules check.
As an example, one may want to require all Theories to not contain any
partial functions. Is there a way to do this without externally re-parsing
and re-interpreting *.thy files? (which would be too error‑prone by the
way). Do the Isabelle system have provision to invoke such a layer,
feeding it with a structure corresponding to the Theory interpretation?
Hope my question is clear enough (I'm not sure). If not, just ask me to
reword it.
With thanks
Email Gateway (Aug 19 2022 at 08:29):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Yannick,
I'll do the easy part and point out page 14 of prog-prove.pdf:
"...all HOL functions must be total. This simplifies the logic—terms are
always defined—but means that recursive functions must terminate."
You probably have other examples in mind, and maybe you're not using HOL.
You use the word "system"; the document "system.pdf" is probably what
would describe such a command. It tells us how to run Isabelle programs
that are available, such as "isabelle jedit" and "isabelle make".
I think what you're wanting falls under the general category of
pre-processing one or more .thy files before handing it over to the
Isabelle prover (but maybe that's not what you're talking about).
With any programming language, if you pull out a function another
function is depending on, the compiler is going to choke, and if you
make a change to a library that other files are depending on, the
dependent files will have to be recompiled, but it seems to me that with
Isabelle, there's a level of paranoia that doesn't exist with
programming languages.
If the programming language lets you compile a bogus program, that's
your problem. If Isabelle lets something by that's not logically valid,
their reputation goes down the tubes.
You can do any pre-processing you want on a group of files, but to make
it worth feeding to the Isabelle prover, you'd have to do a ton of
dependency checks and more, where the "dependency checks and more" is
pretty much what the Isabelle prover does. It sounds to me that only a
user would know enough to make lots of changes to a bunch of files
before feeding them to the prover, and have something worth working with.
There could be something out there like that. I haven't seen anything
like that in system.pdf.
Regards,
GB
Email Gateway (Aug 19 2022 at 08:29):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Not that much, I “imports Main”, and that way it's easy to have a “fun”
which does not cover all cases, with no error and just a warning.
Email Gateway (Aug 19 2022 at 08:30):From: Lars Noschinski <noschinl@in.tum.de>
These functions are nevertheless total; you just don't know anything
about the values for the uncovered case.
-- Lars
Last updated: Apr 24 2024 at 04:17 UTC