Re: [isabelle] Ways to add a checking layer for Theories?
On 8/3/2012 9:15 AM, Yannick Duchêne (Hibou57) wrote:
...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
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and