*To*: John Wickerson <johnwickerson at cantab.net>*Subject*: Re: [isabelle] Variables in locale assumptions*From*: "Van Staden Stephan" <stephan.vanstaden at inf.ethz.ch>*Date*: Fri, 21 Feb 2014 17:04:46 +0000*Accept-language*: en-US, de-CH*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <D85BDDB5-D8F4-4F4C-A578-35FD64B33584@cantab.net>*References*: <FC4BBC48012AB34DAF828891BA6076320A6BED6F@MBX21.d.ethz.ch>, <D85BDDB5-D8F4-4F4C-A578-35FD64B33584@cantab.net>*Thread-index*: Ac8vHtkxnWObjyRgRR64U4+y2zgO/////Y8AgAARDn0=*Thread-topic*: [isabelle] Variables in locale assumptions

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) The question is whether the free variables in an assumption are local to the assumption or not. The locale tutorial suggests that they should be local, but maybe I'm wrong. Thanks, Stephan ________________________________________ From: John Wickerson [johnwickerson at cantab.net] Sent: Friday, February 21, 2014 5:57 PM To: Van Staden Stephan Cc: cl-isabelle-users at lists.cam.ac.uk Subject: Re: [isabelle] Variables in locale assumptions The error seems sensible to me. In a1, R is a relation, and in a2 it's a set. Or maybe I'm missing something? John On 21 Feb 2014, at 16:13, Van Staden Stephan <stephan.vanstaden at inf.ethz.ch> wrote: > Dear all, > > In Isabelle/jEdit 2013-2, the following locale works fine: > > locale Test = > fixes pred :: "'a set ⇒ 'a rel ⇒ bool" > assumes a1: "pred S R" > (* assumes a2: "pred R S" *) > begin > lemma pred_is_UNIV: "pred A B" > by (metis a1) > end > > However, uncommenting assumption a2 gives me the following error: > > Type unification failed > Type error in application: incompatible operand type > Operator: pred :: 'a set ⇒ ('a × 'a) set ⇒ bool > Operand: R :: ('a × 'a) set > > Page 2 of the locale tutorial seems to suggest that this is a bug. Or should I expect this behaviour? > > Thanks in advance! > Stephan >

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

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

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

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

- 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