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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.