*To*: Lawrence Paulson <lp15 at cam.ac.uk>*Subject*: Re: [isabelle] Variables in locale assumptions*From*: Makarius <makarius at sketis.net>*Date*: Mon, 24 Feb 2014 13:41:25 +0100 (CET)*Cc*: Peter Lammich <lammich at in.tum.de>, "cl-isabelle-users at lists.cam.ac.uk List" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <BB1863A5-D8C7-41F4-93EC-CA27874FADE5@cam.ac.uk>*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> <5307D560.3010508@inf.ethz.ch> <1393062477.17875.8.camel@lapbroy33> <BB1863A5-D8C7-41F4-93EC-CA27874FADE5@cam.ac.uk>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Sat, 22 Feb 2014, Lawrence Paulson wrote:

Clearly every instance of a variable in a single formula must have thesame type, and it’s natural to expect that every instance in a list offormulas should also have the same type. The alternative would be veryconfusing for readers, also in informal mathematics.On 22 Feb 2014, at 09:47, Peter Lammich <lammich at in.tum.de> wrote: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?I frequently run into another instance of this problem, when writing something like: lemma foo: "x & y --> x" "x = y --> f x = f y" Note that foo(2) is: "?x::bool = ?y ...", which is usually not what was intended.

Makarius

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

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

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

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

**Re: [isabelle] Variables in locale assumptions***From:*Lawrence Paulson

- 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