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.