Discussion:
[isabelle] a proof on primitive recursion
(too old to reply)
Gergely Buday
2016-07-18 12:13:24 UTC
Permalink
Raw Message
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 Martini
2016-07-18 13:03:22 UTC
Permalink
Raw Message
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 <
Post by Gergely Buday
Hi,
I have proved a simple associativity rule and tried to prove commutativity
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{*
* 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
Loading...