Actually just "by simp" but "by (simp add: eval_nat_numeral)" works on you first lemma too... :-)
Jørgen
From: Jørgen Villadsen
Sent: 4. september 2018 00:55
To: 'Ching-Tsun Chou'; cl-isabelle-***@lists.cam.ac.uk
Subject: RE: [isabelle] How do I prove "foo 2 = foo (Suc (Suc 0))"?
Hi,
I am no expert on the matter but here is a suggestion:
lemma "foo (Suc (Suc n)) = foo (n + 2)"
by (simp add: eval_nat_numeral)
Regards, Jørgen
PS - Shorter proofs of your first lemma:
lemma "foo 2 = foo (Suc (Suc 0))"
using numeral_nat by metis
lemma "foo 2 = foo (Suc (Suc 0))"
using numeral_2_eq_2 by argo
lemma "foo 2 = foo (Suc (Suc 0))"
unfolding numeral_nat using refl .
From: Ching-Tsun Chou [mailto:***@gmail.com]
Sent: 4. september 2018 00:45
To: Jørgen Villadsen
Cc: cl-isabelle-***@lists.cam.ac.uk
Subject: Re: [isabelle] How do I prove "foo 2 = foo (Suc (Suc 0))"?
Thanks!
How about "foo (Suc (Suc n)) = foo (n + 2)"?
- Ching Tsun
On Mon, Sep 3, 2018 at 3:08 PM Jørgen Villadsen <***@dtu.dk<mailto:***@dtu.dk>> wrote:
Hi,
One-line proof:
lemma test: "foo 2 = foo (Suc (Suc 0))"
unfolding numeral_nat by (rule refl)
Regards, Jørgen
-----Original Message-----
From: cl-isabelle-users-***@lists.cam.ac.uk<mailto:cl-isabelle-users-***@lists.cam.ac.uk> [mailto:cl-isabelle-users-***@lists.cam.ac.uk<mailto:cl-isabelle-users-***@lists.cam.ac.uk>] On Behalf Of Ching-Tsun Chou
Sent: 3. september 2018 23:34
To: cl-isabelle-***@lists.cam.ac.uk<mailto:cl-isabelle-***@lists.cam.ac.uk>
Subject: [isabelle] How do I prove "foo 2 = foo (Suc (Suc 0))"?
Is there a one-line proof of the equation? The following is the shortest
one I can find. I am surprised that arith does not solve it directly.
More generally, how do I tell Isabelle just keep normalizing and then apply
reflexivity, like how refl works in Coq?
Thanks!
- Ching Tsun
lemma test: "foo 2 = foo (Suc (Suc 0))"
proof -
have "2 = Suc (Suc 0)" by arith
t