# Re: [isabelle] Sum of first n integers

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

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