Re: [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.


From: John Wickerson [johnwickerson at]
Sent: Friday, February 21, 2014 5:57 PM
To: Van Staden  Stephan
Cc: cl-isabelle-users at
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?


On 21 Feb 2014, at 16:13, Van Staden Stephan <stephan.vanstaden at> 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

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.