Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] simp only: ... - seems to be doing to much

view this post on Zulip Email Gateway (Aug 18 2022 at 11:14):

From: George Karabotsos <g_karab@cs.concordia.ca>
Hello,

I have the following lemma:
lemma "i_0 + (1::nat) + 1 = i_0 + 2"
that seems to be satisfied by the following simplification rule:
apply(simp only: add_2_eq_Suc')

I would have expected to see the following subgoal:
i_0 + (1::nat) + 1 = Suc(Suc i_0)

Can anyone clarify why this is not the expected result?

TIA,

George

view this post on Zulip Email Gateway (Aug 18 2022 at 11:16):

From: Tobias Nipkow <nipkow@in.tum.de>
Most likely because the simplifier always tries arithmetic to solve the
final subgoal. Which, in your case, is an arithmetic triviality. Hence
the goal is solved.

Tobias

George Karabotsos wrote:

Last updated: May 03 2024 at 08:18 UTC