*To*: Van Staden Stephan <stephan.vanstaden at inf.ethz.ch>*Subject*: Re: [isabelle] Variables in locale assumptions*From*: Jasmin Blanchette <jasmin.blanchette at gmail.com>*Date*: Fri, 21 Feb 2014 18:45:06 +0100*Cc*: John Wickerson <johnwickerson at cantab.net>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <FC4BBC48012AB34DAF828891BA6076320A6BEE7C@MBX21.d.ethz.ch>*References*: <FC4BBC48012AB34DAF828891BA6076320A6BED6F@MBX21.d.ethz.ch>, <D85BDDB5-D8F4-4F4C-A578-35FD64B33584@cantab.net> <FC4BBC48012AB34DAF828891BA6076320A6BEE7C@MBX21.d.ethz.ch>

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

**Follow-Ups**:**Re: [isabelle] Variables in locale assumptions***From:*Stephan van Staden

**References**:**[isabelle] Variables in locale assumptions***From:*Van Staden Stephan

**Re: [isabelle] Variables in locale assumptions***From:*John Wickerson

**Re: [isabelle] Variables in locale assumptions***From:*Van Staden Stephan

- Previous by Date: Re: [isabelle] Variables in locale assumptions
- Next by Date: [isabelle] LFMTP 2014: Call for Papers
- Previous by Thread: Re: [isabelle] Variables in locale assumptions
- Next by Thread: Re: [isabelle] Variables in locale assumptions
- Cl-isabelle-users February 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list