*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Work on a new theorem prover*From*: Bohua Zhan <bzhan at mit.edu>*Date*: Wed, 1 Jul 2015 12:37:35 -0400*In-reply-to*: <CAEMBaCDbaHAjCF4sJ_Xw6-Uo+Pvcg6Dx95GeyzvxBAR2NNgBxQ@mail.gmail.com>*References*: <CAEMBaCBC6Q1_WJYQjQ9r55zX7Ae8+M+6-9PUCF+-9v7+o6wPpg@mail.gmail.com> <alpine.LNX.2.00.1503171146590.14159@lxbroy10.informatik.tu-muenchen.de> <CAEMBaCDbaHAjCF4sJ_Xw6-Uo+Pvcg6Dx95GeyzvxBAR2NNgBxQ@mail.gmail.com>

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

**Follow-Ups**:**Re: [isabelle] Work on a new theorem prover***From:*Jasmin Blanchette

- Previous by Date: [isabelle] using makeindex in document preparation
- Next by Date: [isabelle] Quickcheck counter example of "3 < 4"?
- Previous by Thread: Re: [isabelle] using makeindex in document preparation
- Next by Thread: Re: [isabelle] Work on a new theorem prover
- Cl-isabelle-users July 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list