*To*: isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] sum.sum_case*From*: George Karabotsos <g_karab at cs.concordia.ca>*Date*: Wed, 12 Mar 2008 17:13:30 -0400*Cc*: Patrice Chalin <chalin at encs.concordia.ca>*In-reply-to*: <47D8087D.9080502@cs.concordia.ca>*References*: <47D8087D.9080502@cs.concordia.ca>*User-agent*: Thunderbird 2.0.0.0 (X11/20070326)

Nevermind, the rule is trav1Measure.simps. :) George George Karabotsos wrote:

Hello,I keep seeing *sum.sum_case* referenced withing simplifier traceswhile trying to prove function termination. For example:[1]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:/\data sts. trav1Measure (Inr sts) < trav1Measure (Inl (Tree1.Nodedata 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" insideGenHOL4Base.thy. Unfortunately, I cannot make much out of it. Myguess is that there is a sum_case rule specific for my datatype(hence the ??.uknown). So I would like to know how can I referencethis rule through a "thm" statement?TIA, George

**References**:**[isabelle] sum.sum_case***From:*George Karabotsos

- Previous by Date: [isabelle] sum.sum_case
- Next by Date: Re: [isabelle] TTVSI early registration deadline
- Previous by Thread: [isabelle] sum.sum_case
- Next by Thread: Re: [isabelle] TTVSI early registration deadline
- Cl-isabelle-users March 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list