*To*: <stark at cs.stonybrook.edu>, <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Failure to prove a simple transitivity -- what could be the cause?*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Tue, 12 Jan 2016 12:13:47 +0100*In-reply-to*: <5694CFEE.5040403@starkeffect.com>*References*: <569414EE.60800@starkeffect.com> <5694A950.4060009@inf.ethz.ch> <141FC5DA-1BD2-4EB7-9A00-77574F24EBD3@exchange.uibk.ac.at> <5694CFEE.5040403@starkeffect.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.3.0

Dear Gene, On 12/01/16 11:05, Eugene W. Stark wrote:

have XY: "XXX f g x y = YYY f g x x' y y'" using A by (auto simp add: XXX_def YYY_def) moreover have YZ: "YYY f g x x' y y' = ZZZ f g x y y'" using 2 6 by (auto simp add: YYY_def ZZZ_def) ultimately have "XXX f g x y = ZZZ f g x y y'" using HOL.trans [of "XXX f g x y" "YYY f g x x' y y'" "ZZZ f g x y y'"]

using [[show_consts]] apply - Hope this helps, Andreas

**Follow-Ups**:**Re: [isabelle] Failure to prove a simple transitivity -- what could be the cause?***From:*Eugene W. Stark

**References**:**[isabelle] Failure to prove a simple transitivity -- what could be the cause?***From:*Eugene W. Stark

**Re: [isabelle] Failure to prove a simple transitivity -- what could be the cause?***From:*Andreas Lochbihler

**Re: [isabelle] Failure to prove a simple transitivity -- what could be the cause?***From:*Thiemann, Rene

**Re: [isabelle] Failure to prove a simple transitivity -- what could be the cause?***From:*Eugene W. Stark

- Previous by Date: Re: [isabelle] Failure to prove a simple transitivity -- what could be the cause?
- Next by Date: Re: [isabelle] Failure to prove a simple transitivity -- what could be the cause?
- Previous by Thread: Re: [isabelle] Failure to prove a simple transitivity -- what could be the cause?
- Next by Thread: Re: [isabelle] Failure to prove a simple transitivity -- what could be the cause?
- Cl-isabelle-users January 2016 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