Re: [isabelle] Failure to prove a simple transitivity -- what could be the cause?
Ah, yes. Thank you, Andreas.
I completed the original proof by introducing type constraints to avoid the
- 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,
This archive was generated by a fusion of
Pipermail (Mailman edition) and