*To*: Tobias Nipkow <nipkow at in.tum.de>*Subject*: Re: [isabelle] ML "set simp_trace": Congruence Rule question*From*: George Karabotsos <g_karab at cs.concordia.ca>*Date*: Wed, 12 Dec 2007 08:18:08 -0500*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <475FD54F.6070507@in.tum.de>*References*: <475ECBC1.7050200@cs.concordia.ca> <475FBAFB.8000808@in.tum.de> <475FC37C.20503@cs.concordia.ca> <475FD54F.6070507@in.tum.de>*User-agent*: Thunderbird 2.0.0.0 (X11/20070326)

George Tobias Nipkow wrote:

It is in HOL.thy: if_weak_cong. Tobias George Karabotsos wrote:Hi Tobias,thank you for the explanation, but where does it come from? Ichecked the HOL.thy theory and I did not see any such rule. Does ithave a name?George Tobias Nipkow wrote:The premise A = A == ?c is the instantiated premise of thecongruence rule?b == ?c ==> if ?b then ?x else ?y == if ?c then ?x else ?yThis rule is used to limit simplification of if-then-else to theif-part, in this case A=A. Once that has become True, theif-then-else collapses and its then-part can be simplified.Tobias George Karabotsos wrote: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 simpThere is a part of the trace I do not understand - specifically Iam 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

**References**:**[isabelle] ML "set simp_trace": Congruence Rule question***From:*George Karabotsos

**Re: [isabelle] ML "set simp_trace": Congruence Rule question***From:*Tobias Nipkow

**Re: [isabelle] ML "set simp_trace": Congruence Rule question***From:*George Karabotsos

**Re: [isabelle] ML "set simp_trace": Congruence Rule question***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] ML "set simp_trace": Congruence Rule question
- Next by Date: Re: [isabelle] UNdefining syntax?
- Previous by Thread: Re: [isabelle] ML "set simp_trace": Congruence Rule question
- Next by Thread: [isabelle] isatool convert
- Cl-isabelle-users December 2007 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