*To*: <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Variables in locale assumptions*From*: Stephan van Staden <Stephan.vanStaden at inf.ethz.ch>*Date*: Fri, 21 Feb 2014 22:38:24 +0000*In-reply-to*: <9B97784B-AE5E-4291-B2C0-4285E7894C11@gmail.com>*References*: <FC4BBC48012AB34DAF828891BA6076320A6BED6F@MBX21.d.ethz.ch>, <D85BDDB5-D8F4-4F4C-A578-35FD64B33584@cantab.net> <FC4BBC48012AB34DAF828891BA6076320A6BEE7C@MBX21.d.ethz.ch> <9B97784B-AE5E-4291-B2C0-4285E7894C11@gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.2.0

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

**Follow-Ups**:**Re: [isabelle] Variables in locale assumptions***From:*Peter Lammich

**Re: [isabelle] Variables in locale assumptions***From:*Makarius

**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

**Re: [isabelle] Variables in locale assumptions***From:*Jasmin Blanchette

- Previous by Date: Re: [isabelle] Variables in locale assumptions
- Next by Date: Re: [isabelle] Variables in locale assumptions
- 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