*To*: <cl-isabelle-users at lists.cam.ac.uk>*Subject*: [isabelle] a proof on primitive recursion*From*: "Gergely Buday" <buday.gergely at uni-eszterhazy.hu>*Date*: Mon, 18 Jul 2016 14:08:55 +0200*Thread-index*: AdHg5YxIohjgJgroTFe7Izu8WtjqIg==

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

**Follow-Ups**:**Re: [isabelle] a proof on primitive recursion***From:*Alfio Martini

- Previous by Date: Re: [isabelle] Surprise!
- Next by Date: Re: [isabelle] a proof on primitive recursion
- Previous by Thread: Re: [isabelle] Surprise!
- Next by Thread: Re: [isabelle] a proof on primitive recursion
- Cl-isabelle-users July 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list