Re: [isabelle] universal quantifiers vs. schematic variables



On 04.10.2015 20:02, David Cock wrote:
> Noam,
>   You'll probably get answers from more knowledgable persons than I, but
> 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.

Schematic variables are equivalent to outermost universal quantifiers.

> (!x. P x) => P y

> holds, but
> 
> P ?x => P y

That is, the theorem "P ?x ==> P y" is equivalent to the theorem "!!x. P
x ==> P y" which is equivalent (in HOL) to "(?x. P x) ==> P y".

  -- Lars




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