Re: [isabelle] Variables in locale assumptions



On 21.02.2014 17:45, Jasmin Blanchette wrote:
> Am 21.02.2014 um 18:04 schrieb Van Staden Stephan <stephan.vanstaden at inf.ethz.ch>:
>
>> It's a free variable in each assumption. I would expect the assumptions to be:
>>
>> (!!S R. pred S R) /\ (!!S R. pred R S)
>>
>> but what happens is apparently:
>>
>> (!!S R. pred S R /\ pred R S)
> For the record: I assume you're perfectly aware that conjunction (which is incidentally written &&& if you want the metalogic version) distributes over universal quantification. And since Isabelle magically transforms universals in schematics, you effectively get independent theorems "pred ?S ?R" and "pred ?R ?S", only that there's an additional type constraint that all occurrences of R (resp. S) have the same type.

It's this type constraint that surprised me. The post by Makarius
explains it, but as a user I would prefer to have complete separation.
Is there a compelling reason why it's implemented as it is?

Thanks,
Stephan




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