[isabelle] a proof on primitive recursion



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

 

 




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