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 Theory interpretation?

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







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.