Re: [isabelle] Sum of first n integers



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.