# Re: [isabelle] a proof on primitive recursion

```Hi Gergely,

You need an auxiliary lemma. Using a slightly different notation. Here is a
very old version.
I would not do it in this way nowadays :-)

Best!

lemma lem01:"add zero n = n"
apply (induction n)
apply (simp)
apply (simp)
done

This is the auxiliary lemma!

lemma lem02: "âx. suc (add x n) = add (suc x) n"
apply (induction n)
apply (simp)
apply (simp)
done

apply (induction n)
done

Best!

On Mon, Jul 18, 2016 at 9:08 AM, Gergely Buday <
buday.gergely at uni-eszterhazy.hu> wrote:

> Hi,
>
>
>
> I have proved a simple associativity rule and tried to prove commutativity
>
>
>
>
> imports Main
>
> begin
>
>
>
> datatype natural = Zero | Succ natural
>
>
>
> primrec add :: "natural â natural â natural"
>
> where
>
>   "add Zero m = m"
>
>
>
>
>
> proof -
>
> fix k m n
>
>
> proof (induct k arbitrary: m n)
>
>   fix m n
>
>
>   proof (induct m arbitrary: n)
>
>    fix n
>
>
>   next
>
>    fix m n
>
>
> by simp
>
>   qed
>
> next
>
>   fix k m n
>
>
>
> qed
>
> qed
>
>
>
> text{*
>
>
>
> Questions:
>
>
>
> * is it usually better in an induction proof to name the other variables
> as arbitrary? Does this make the proof easier?
>
>
>
> * I have created this proof quite mechanically, copying premise as an
> assumption and the conclusion as the show clause.
>
>    Is there a better proof strategy in general, and in particular for this
> proof?
>
>
>
> *}
>
>
>
>
> proof -
>
> fix m n
>
>
> proof (induct m arbitrary: n)
>
>   fix n
>
>
>   proof (induct n)
>
>
>   next
>
>    fix n
>
>
>    from this show "add Zero (Succ n) = add (Succ n) Zero" by simp
>
>   qed
>
> next
>
>   fix m n
>
>
>   from this show "add (Succ m) n = add n (Succ m)"
>
>
>
> ---
>
>
>
> I am stuck here. There is no way of rewriting Succ m in the second
> parameter of Succ. What is the way out of the bottle?
>
>
>
> Should I try another definition?
>
>
>
> Should I use the proven theory of builtin natural numbers, prove an
> adequacy theorem of + and this add function and use the commutativity of +
> ?, or I can make it without this recourse?
>
>
>
> - Gergely
>
>
>
>
>
>

--
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
www.inf.pucrs.br/alfio
Av. Ipiranga, 6681 - PrÃdio 32 - Faculdade de InformÃtica
90619-900 -Porto Alegre - RS - Brasil

```

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