Re: [isabelle] universal quantifiers vs. schematic variables

Grr, sorry, hit send without proofreading. That second one should have been

P x => P y

i.e. an *unbound*, not a schematic name.

Noam: in your example, it's not clear whether you have an actual schematic, or just an unbound (blue) variable.


On 04/10/15 11:19, Jasmin Blanchette wrote:

you've just discovered one of Isabelle's most fundamental quirks.  As theorems, you're right that they're (logically) equivalent, but they differ if they appear as assumptions i.e.

(!x. P x) => P y

holds, but

P ?x => P y

does not (necessarily) hold.

schematic_lemma "P ?x ==> P y"
   by assumption



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