*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Sum of first n integers*From*: Peter Lammich <lammich at in.tum.de>*Date*: Wed, 21 Oct 2015 16:06:13 +0200*In-reply-to*: <CAJ+Teod4Pnhw1xvbiwFRc51-6Fb2eDM5W1NSCPLs=b6H_EL90A@mail.gmail.com>*References*: <CAJ+TeofX7WZJ+ubA1dvXs=MNQmGDdr2KzchDHe8bY6p=D6NKSQ@mail.gmail.com> <56272622.1000400@in.tum.de> <CAJ+Teofw1L-vUOe0zU+etRrAopQp+rxUKYmM8FmHG3=-4EbRQg@mail.gmail.com> <CAMUwPhyNFCG97H4OEiMJ3202VycZ-1h_YC5M=7CGBznCN2Gnag@mail.gmail.com> <CAJ+TeodLCpOG-whbat6BKhV+NOet6HfVOEJyB4Nrb7o7GaQFdQ@mail.gmail.com> <CAMUwPhyKn7Kbh8+-3W-nMmCKx-o2_BJC90-cuXR+=ABBzPmy=w@mail.gmail.com> <CAJ+Teoe=y4f2fRvY5MUYnCYRSg003uoT5-_F4sH2+0RS5peQYQ@mail.gmail.com> <CAJ+Teod4Pnhw1xvbiwFRc51-6Fb2eDM5W1NSCPLs=b6H_EL90A@mail.gmail.com>

A theorem is proved, if you finish its proof (by qed or done). Isabelle outputting "theorem" means that it is a proved theorem. If you give the theorem a name, you can also use the command thm name to display the theorem later. However, be careful with the asynchronous processing of the prover IDE: Only if there are no errors in the theories before your theory (check the "Theories"-panel), you have really proven the theorem. Otherwise, it might depend on unproven stuff! E.g. lemma f: False by simp -- "There will be an error here, but False will be registered by name f anyway!" theorem "1=2" using f by simp -- "This outputs: theorem 1=2, and, locally, you cannot distinguish that from a valid proof" To be sure that a theory is valid, without having to inspect the open theories for errors (which gets cumbersome for large developments, even using the theories panel), you have to use the batch-build mode of Isabelle. So, summarized, to develop your own theories, you use the IDE. To verify theories of others, you should use batch-build, which also excludes cheating by the sorry-command. -- Peter On Mi, 2015-10-21 at 19:05 +0530, Rustom Mody wrote: > On Wed, Oct 21, 2015 at 3:50 PM, Rustom Mody <rustompmody at gmail.com> wrote: > > > On Wed, Oct 21, 2015 at 3:01 PM, Harry Butterworth <heb1001 at gmail.com> > > wrote: > > > >> Here you go... > >> > > > > Thanks Harry! > > > > Tried another small example > >From http://www4.in.tum.de/~wenzelm/papers/Calculations-Isar.pdf > I managed to copy-paste and remove all red-marks :-) > [thy file below] > > So now a more basic question > How do I know that the proof is done? > > In more detail > Cursor on "finally", output window shows: > > proof (chain): depth 0 > > picking this: > â{X, Y, {}} = â{X, Y} > calculation: â{X, Y, {}} = â{X, Y} > > Cursor on "qed" output window shows: > > theorem â{?X, ?Y, {}} = â{?X, ?Y} > > Looks quite arcane to me and nothing quite says "Proved!" > > So where/how do I know this proof is successful? > > ----------------------- union.thy -------------- > theory union > imports Main > begin > theorem "\<Union>{X , Y , {}} = \<Union>{X , Y }" > proof - > have "\<Union>{X , Y , {}} = \<Union>({X , Y } \<union> {{}})" by auto > also have "... = \<Union>{X , Y } \<union> \<Union>{{}}" by auto > also have "... = \<Union>{X , Y } \<union> {}" by auto > also have "... = \<Union>{X , Y }" by auto > > finally show "\<Union>{X , Y , {}} = \<Union>{X , Y }" . > qed

**References**:**[isabelle] Sum of first n integers***From:*Rustom Mody

**Re: [isabelle] Sum of first n integers***From:*Lars Noschinski

**Re: [isabelle] Sum of first n integers***From:*Rustom Mody

**Re: [isabelle] Sum of first n integers***From:*Harry Butterworth

**Re: [isabelle] Sum of first n integers***From:*Rustom Mody

**Re: [isabelle] Sum of first n integers***From:*Harry Butterworth

**Re: [isabelle] Sum of first n integers***From:*Rustom Mody

**Re: [isabelle] Sum of first n integers***From:*Rustom Mody

- Previous by Date: Re: [isabelle] Sum of first n integers
- Next by Date: [isabelle] splash?
- Previous by Thread: Re: [isabelle] Sum of first n integers
- Next by Thread: [isabelle] Setting quick_and_dirty mode for a fragment of a theory only
- Cl-isabelle-users October 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