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



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.