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 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?
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" *)
> lemma pred_is_UNIV: "pred A B"
> by (metis a1)
> 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!
This archive was generated by a fusion of
Pipermail (Mailman edition) and