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.

David

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

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.
Huh?

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

Cheers,

Jasmin






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