*To*: Peter Lammich <lammich at in.tum.de>*Subject*: Re: [isabelle] Variables in locale assumptions*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Sat, 22 Feb 2014 11:24:04 +0000*Cc*: "cl-isabelle-users at lists.cam.ac.uk List" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <1393062477.17875.8.camel@lapbroy33>*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>

Clearly every instance of a variable in a single formula must have the same type, and it’s natural to expect that every instance in a list of formulas should also have the same type. The alternative would be very confusing for readers, also in informal mathematics. Larry Paulson 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. > > > -- > Peter > > >

**Follow-Ups**:**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

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

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

- 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