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

Ah, yes. Thank you, Andreas. I completed the original proof by introducing type constraints to avoid the unwanted polymorphism. - Gene Stark On 01/12/2016 06:13 AM, Andreas Lochbihler wrote: > 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'"] > > In this example, polymorphism gets in the way. Type inference assigns different types to the ZZZ instances. You can see > this by hovering over the ZZZs in the theory file (unfortunately, this does not work in the Output buffer) or with > > using [[show_consts]] > apply - > > Hope this helps, > Andreas >

**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

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

- Previous by Date: Re: [isabelle] Failure to prove a simple transitivity -- what could be the cause?
- Next by Date: [isabelle] building session confuses paths to theories
- Previous by Thread: Re: [isabelle] Failure to prove a simple transitivity -- what could be the cause?
- Next by Thread: [isabelle] building session confuses paths to theories
- 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