Re: [isabelle] Work on a new theorem prover



Hi, everyone

I have uploaded the second version of auto2 at
https://github.com/bzhan/auto2

It now supports Isabelle2015. The biggest internal addition is proof
scripts, which allows the user to specify intermediate steps of a
proof, similar to (but currently independent from) Isar. There is also
much better support for induction.

There are now more examples from different areas:
- Number theory: infinitude of primes and unique factorization theorem.
- Lists, trees, and red-black trees.
- Hoare logic.

Please see README and the updated documentation for details. Again I
would welcome any comments and suggestions.

Best,
Bohua

On Tue, Mar 17, 2015 at 2:51 PM, Bohua Zhan <bzhan at mit.edu> wrote:
> Hi, Makarius
>
> Thanks. Updated with capitalization of theory names, and moved to
> support Isabelle2014.
>
> It seems when a schematic variable without specified type is read in
> mode_schematic, the type is set to be a free variable rather than
> schematic variable. I would actually prefer it to be schematic, since
> there is potential for type matchings.
>
> I will need more time to figure out mkroot. The general structure is:
> Auto2 depends on Arith_Thms, Logic_Thms
> Auto2_Test depends on Auto2 (unit testing)
> Primes_Ex depends on Auto2.
>
> Best,
> Bohua
>
> On Tue, Mar 17, 2015 at 6:54 AM, Makarius <makarius at sketis.net> wrote:
>> On Mon, 16 Mar 2015, Bohua Zhan wrote:
>>
>>> Recently I have been working on writing a new theorem prover based on
>>> Isabelle.
>>
>>
>> I was first confused by this wording, but "auto2" seems to be a plain proof
>> tool inside Isabelle, i.e. just a normal application of the existing
>> framework.
>>
>>
>>> https://github.com/bzhan/auto2
>>
>>
>> I recommend to add a formal session ROOT to make clear what is the project
>> structure.  See also "isabelle mkroot" in the "system" manual.
>>
>> BTW, using some unspecified "development version of Isabelle" means this is
>> mainly a private experiment of yours.  I you have good reasons for not using
>> the latest Isabelle release (Which ones?) the minimum is to say which
>> changeset id of the Isabelle repository is required.  It is also possible to
>> make a formal Mercurial subrepository reference (in a Mercurial repository,
>> probably not a git one).
>>
>>
>>> I am posting it here to see if there are any suggestions, things that
>>> are known that could help with this project, or (even better)
>>> contributions.
>>
>>
>> Just some notes from looking briefly:
>>
>> * Theory names are always capitalized in Isabelle.
>>
>> * The @{term_pat} antiqutation is a bit strange.  If you really mean to
>>   refer to schematic terms, you should say so via
>>   Proof_Context.mode_schematic, and not Proof_Context.mode_pattern.
>>
>>
>>         Makarius




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