Re: [isabelle] A simple (?) lemma



I wonder what you mean by pedagogical reasons. If you want to teach the basics of Peano arithmetic, just do it on paper. You don't need Isabelle to carry out a two step proof. If you imagine that this would be a way to teach the use of Isabelle, I would disagree. The way to prove this sort of trivial fact is indeed using auto. There are plenty of other examples that you could use to demonstrate basic Isabelle skills.

Even so, if you would like to step through the basics of this proof, I first suggest that you state the theorem explicitly using the successor function:

lemma silly: "(Suc 0) + (Suc 0) = (Suc (Suc 0))"

Then perform a couple of substitutions using the theorems add_0 and add_Suc.

Larry Paulson


On 26 May 2010, at 22:53, Marcin Zalewski wrote:

> Dear Isabelle experts,
> 
> This question might have been answered before, but it is rather
> difficult to search for a possible answer. I want to prove the
> following lemma:
> 
> lemma silly: "(1::nat) + 1 = 2"
> 
> I know that I can do "by auto" (or some other automatic tactic), but
> the catch is that I want to perform the proof explicitly for
> pedagogical reasons. It seems to be more difficult than I have
> expected. I am able to see the proof term generated by auto, but the
> proof starts with equal_elim, which I have no idea how to apply. I
> would be extremely grateful for some direction on how to proceed with
> an explicit proof of the above lemma. Is it even practical?
> 
> Thank you,
> Marcin
> 






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