[isabelle] is this expected behaviour? (file attached)



Dear fellow Isabelle users,

as a non-expert, I am surprised to find out that the following is not a theorem in Isabelle/HOL (more details in attached theory file):

consts A :: 'a ⇒ bool
lemma (∀x. A x) ⟶ (∀x. A x) -- counterexample by nitpick

The reason is that A gets instantiated with one type in the antecedent and other in the consequent.
I understand that this might be totally expected behavior (well, not for me, but this is due to me still ignoring many things about how Isabelle works). The issue is that as formulas grow more complex this issue gives rise to more subtle (and mean) problems as shown in the attached file.

Can someone explain which of the illustrated behaviours are expected?
(and again, sorry for the newbie question ;)

Best, David

Attachment: ExpectedBehaviour.thy
Description: Binary data



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