Email Gateway (Dec 17 2025 at 09:14): Email Gateway (Dec 17 2025 at 09:14):From: 山田晃久 <cl-isabelle-users@lists.cam.ac.uk>
Dear list,
this is just a question, not a request. In HOL/Transcendental.thy, there are two simp rules whose lhss are reducible by other simp rules:
To make them applied, one must disable of_nat_Suc. Is this intended?
Best,
Akihisa
Email Gateway (Dec 17 2025 at 11:10):From: Manuel Eberl <manuel@pruvisto.org>
That doesn't look intentional, no. No idea where this comes from and why
it's written that way. My guess would be that somebody added it without
thinking too much about it.
In my experience rules like that don't work super well to begin with
though. If your "n" is actually a "Suc n" or a numeral or a "m + n" the
rules aren't going to fire. So even if one were to replace the left-hand
side of this rule with its normal form, I don't think it would work
terribly well. I have been wondering whether one could build some sort
of simproc to deal with that sort of thing. But I never really got round
to doing that and it's not entirely clear what the scope would be.
However, in Isabelle 2025-1 there will at least be some material that
might help with this sort of thing in HOL-Library.Real_Mod, e.g.:
lemma sin_rcong: "[x = y] (rmod (2 * pi)) ⟹ sin x = sin y"
Or more generally:
lemma sin_eq_sin_conv_rmod_iff: "sin x = sin y ⟷ [x = y] (rmod 2 *
pi) ∨ [x = pi - y] (rmod 2 * pi)"
Combining this with the collection of intro rules rcong_intros allows
you to simplify expressions involving sin/cos/tan/cis/etc. a lot more
nicely.
Cheers,
Manuel
On 17/12/2025 10:13, 山田晃久 (via cl-isabelle-users Mailing List) wrote:
Dear list,
this is just a question, not a request. In HOL/Transcendental.thy,
there are two simp rules whose lhss are reducible by other simp rules:
- lemma sin_cos_npi [simp]: "sin (real (Suc (2 * n)) * pi/2) = (-1) ^ n"
- lemma cos_pi_eq_zero [simp]: "cos (pi * real (Suc (2 * m)) / 2) = 0"
To make them applied, one must disable of_nat_Suc. Is this intended?
Best,
Akihisa
Email Gateway (Dec 17 2025 at 12:13):From: Makarius <makarius@sketis.net>
On 17/12/2025 12:10, Manuel Eberl wrote:
That doesn't look intentional, no. No idea where this comes from and why it's
written that way. My guess would be that somebody added it without thinking
too much about it.
It comes from this changeset:
changeset: 12196:a3be6b3a9c0b
user: paulson
date: Thu Nov 15 16:12:49 2001 +0100
description:
new theories from Jacques Fleuriot
Interesting to see how things were done > 25 years ago.
Makarius
Email Gateway (Dec 18 2025 at 03:25):From: 山田晃久 <cl-isabelle-users@lists.cam.ac.uk>
Thank you for clarification! I guess that long ago "real" wasn't a synonym of of_nat and the situation was different.
And yes, just simplifying the lhss won't make them very applicable anyway. Then I would propose to add:
lemma sin_add_pi_half [simp]: "sin (x + pi/2) = cos x" by (simp add: sin_add)
lemma cos_add_pi_half [simp]: "cos (x + pi/2) = - sin x" by (simp add: cos_add)
Then the original statements can be derived by adding distribution rules:
lemma sin_cos_npi: "sin (real (Suc (2 * n)) * pi/2) = (-1) ^ n" by (simp add: algebra_simps add_divide_distrib)
lemma cos_pi_eq_zero: "cos (pi * real (Suc (2 * m)) / 2) = 0" by (simp add: algebra_simps add_divide_distrib)
Best,
Akihisa
差出人: cl-isabelle-users-request@lists.cam.ac.uk <cl-isabelle-users-request@lists.cam.ac.uk> が Makarius <makarius@sketis.net> の代理で送信
送信: 2025 年 12 月 17 日 (水曜日) 21:13
宛先: Manuel Eberl <manuel@pruvisto.org>; cl-isabelle-users@lists.cam.ac.uk <cl-isabelle-users@lists.cam.ac.uk>
件名: Re: [isabelle] Simp rules with reducible lhss in Transcendental.thy
On 17/12/2025 12:10, Manuel Eberl wrote:
That doesn't look intentional, no. No idea where this comes from and why it's
written that way. My guess would be that somebody added it without thinking
too much about it.
It comes from this changeset:
changeset: 12196:a3be6b3a9c0b
user: paulson
date: Thu Nov 15 16:12:49 2001 +0100
description:
new theories from Jacques Fleuriot
Interesting to see how things were done > 25 years ago.
Makarius
Email Gateway (Dec 18 2025 at 12:26):From: Lawrence Paulson <lp15@cam.ac.uk>
Many thanks for your suggestion. I'm surprised that those well-known facts are not available already in that exact form, although we have many related identities. As for your original question, I think that sometimes people apply the [simp] attribute without considering whether it makes sense, or else as you suggested, possibly it made sense back in 2001.
Larry
On 18 Dec 2025, at 03:24, 山田晃久 <cl-isabelle-users@lists.cam.ac.uk> wrote:
Thank you for clarification! I guess that long ago "real" wasn't a synonym of of_nat and the situation was different.
And yes, just simplifying the lhss won't make them very applicable anyway. Then I would propose to add:
lemma sin_add_pi_half [simp]: "sin (x + pi/2) = cos x" by (simp add: sin_add)
lemma cos_add_pi_half [simp]: "cos (x + pi/2) = - sin x" by (simp add: cos_add)
Email Gateway (Dec 19 2025 at 14:46):From: 山田晃久 <cl-isabelle-users@lists.cam.ac.uk>
Thank you! It was actually a question regarding how to improve HOL/MacLaurin.thy, which I now propose as in the attached patch.
Initial motivation was just to make proof export succeed (for the project of Frédéric), but I think eventually this is good enough to replace the original.
I did not change the main statements, though I think "1/2 * ..." should better be simplified to "... / 2".
Best,
Akihisa
差出人: Lawrence Paulson <lp15@cam.ac.uk>
送信: 2025 年 12 月 18 日 (木曜日) 21:26
宛先: 山田晃久 <akihisa.yamada@aist.go.jp>
Cc: Makarius <makarius@sketis.net>; Manuel Eberl <manuel@pruvisto.org>; cl-isabelle-users@lists.cam.ac.uk <cl-isabelle-users@lists.cam.ac.uk>
件名: Re: [isabelle] Simp rules with reducible lhss in Transcendental.thy
Many thanks for your suggestion. I'm surprised that those well-known facts are not available already in that exact form, although we have many related identities. As for your original question, I think that sometimes people apply the [simp] attribute without considering whether it makes sense, or else as you suggested, possibly it made sense back in 2001.
Larry
On 18 Dec 2025, at 03:24, 山田晃久 <cl-isabelle-users@lists.cam.ac.uk> wrote:
Thank you for clarification! I guess that long ago "real" wasn't a synonym of of_nat and the situation was different.
And yes, just simplifying the lhss won't make them very applicable anyway. Then I would propose to add:
lemma sin_add_pi_half [simp]: "sin (x + pi/2) = cos x" by (simp add: sin_add)
lemma cos_add_pi_half [simp]: "cos (x + pi/2) = - sin x" by (simp add: cos_add)
Last updated: Dec 21 2025 at 20:24 UTC