Re: [isabelle] Referring to type variable of a locale



Stephan,

On 17/01/2012, at 12:57 AM, Stephan van Staden wrote:

> Hi, I'm running into a problem whose solution should be simple. The following is fine:
> 
> class cla = fixes foo :: "'a"
> class cla2 = cla + fixes a_set :: "'a set"
> begin
> lemma lem1: "foo \<in> a_set \<Longrightarrow> true"
> sorry
> end
> 
> Yet what I want is not fine:
> 
> locale loc = fixes foo :: "'a"
> locale loc2 = loc + fixes a_set :: "'a set"
> begin
> lemma lem1: "foo \<in> a_set \<Longrightarrow> true"
> sorry
> end
> 
> The error I get is:
> Type unification failed
> Type error in application: incompatible operand type
> Operator: op ∈ foo :: ('b ⇒ bool) ⇒ bool
> Operand: a_set :: 'a ⇒ bool
> 
> Can I somehow tell Isabelle that I want the type of a_set to be "'a::loc set"?

You can use a "for" clause to constrain the type of foo:

locale loc = fixes foo :: "'a"
locale loc2 = loc foo for foo :: "'a" + fixes a_set :: "'a set"
begin
lemma lem1: "foo \<in> a_set \<Longrightarrow> true"
sorry
end

There is a lot of information in the mailing list archives about locales - hopefully you can find it without too much bother.

cheers
peter







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