Re: [isabelle] sum.sum_case



Nevermind, the rule is  trav1Measure.simps. :)

George

George Karabotsos wrote:
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







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.