Re: [isabelle] Variables in locale assumptions



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.

The locales tutorial is not entirely clear on this point. If "means" refers to semantics, what is written there is not inaccurate.

Jasmin





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