Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] ML "set simp_trace": Congruence Rule question

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

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

I am examining the simplifier's trace for the following lemma:

lemma "(if A=A then AV else if AA=BB then BV else CV) = AV"
by simp

There is a part of the trace I do not understand - specifically I am
talking about the following part:

[1]Applying congruence rule:
A = A == ?c
==> if A = A then AV else if AA = BB then BV else CV ==
if ?c then AV else if AA = BB then BV else CV

trace_simp_depth_limit exceeded!

Where did the A =A == ?c rule came from?

TIA,
George

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

From: Tobias Nipkow <nipkow@in.tum.de>
The premise A = A == ?c is the instantiated premise of the congruence rule

?b == ?c
==> if ?b then ?x else ?y == if ?c then ?x else ?y

This rule is used to limit simplification of if-then-else to the
if-part, in this case A=A. Once that has become True, the if-then-else
collapses and its then-part can be simplified.

Tobias

George Karabotsos wrote:

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

From: Tobias Nipkow <nipkow@in.tum.de>
It is in HOL.thy: if_weak_cong.

Tobias

George Karabotsos wrote:

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

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

thank you for the explanation, but where does it come from? I checked
the HOL.thy theory and I did not see any such rule. Does it have a name?

George

Tobias Nipkow wrote:

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

From: George Karabotsos <g_karab@cs.concordia.ca>
Last question (I promise :) ). Any idea why the name is not displayed
in the trace?
George

Tobias Nipkow wrote:

Last updated: May 03 2024 at 01:09 UTC