Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] sum.sum_case

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

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

I keep seeing sum.sum_case referenced withing simplifier traces while
trying to prove function termination. For example:

[1]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
/\data sts. trav1Measure (Inr sts) < trav1Measure (Inl (Tree1.Node data
sts))
[1]Applying instance of rewrite rule "??.unknown":
trav1Measure ?x1 : sum.sum_case size length ?x1
[1]Rewriting:
trav1Measure (Inr sts) : sum.sum_case size length (Inr sts)

After looking in the source I was able to find a "definition" inside
GenHOL4Base.thy. Unfortunately, I cannot make much out of it. My guess
is that there is a sum_case rule specific for my datatype (hence the
??.uknown). So I would like to know how can I reference this rule
through a "thm" statement?

TIA,

George

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

From: George Karabotsos <g_karab@cs.concordia.ca>
Nevermind, the rule is trav1Measure.simps. :)

George

George Karabotsos wrote:

Last updated: May 03 2024 at 04:19 UTC