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


theorem th02a:"âx. add x n = add n x"
     apply (induction n)
     apply (simp_all add:lem01 lem02)
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
> of an addition function:
>
>
>
> theory Add
>
> imports Main
>
> begin
>
>
>
> datatype natural = Zero | Succ natural
>
>
>
> primrec add :: "natural â natural â natural"
>
> where
>
>   "add Zero m = m"
>
> | "add (Succ n) m = Succ (add n m)"
>
>
>
> lemma add_assoc: "â k m n . add k (add m n) = add (add k m) n "
>
> proof -
>
> fix k m n
>
> show "add k (add m n) = add (add k m) n"
>
> proof (induct k arbitrary: m n)
>
>   fix m n
>
>   show "add Zero (add m n) = add (add Zero m) n"
>
>   proof (induct m arbitrary: n)
>
>    fix n
>
>    show "add Zero (add Zero n) = add (add Zero Zero) n" by simp
>
>   next
>
>    fix m n
>
>    assume "ân. add Zero (add m n) = add (add Zero m) n"
>
>    from this show "add Zero (add (Succ m) n) = add (add Zero (Succ m)) n"
> by simp
>
>   qed
>
> next
>
>   fix k m n
>
>   assume "âm n. add k (add m n) = add (add k m) n"
>
>   from this show "add (Succ k) (add m n) = add (add (Succ k) m) n" by simp
>
> 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?
>
>
>
> *}
>
>
>
> lemma add_commute: "â m n. add m n = add n m"
>
> proof -
>
> fix m n
>
>  show "add m n = add n m"
>
> proof (induct m arbitrary: n)
>
>   fix n
>
>   show "add Zero n = add n Zero"
>
>   proof (induct n)
>
>    show "add Zero Zero = add Zero Zero" by simp
>
>   next
>
>    fix n
>
>    assume "add Zero n = add n Zero"
>
>    from this show "add Zero (Succ n) = add (Succ n) Zero" by simp
>
>   qed
>
> next
>
>   fix m n
>
>   assume indhyp: "ân. add m n = add n m"
>
>   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.