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.

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
>





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