Re: [isabelle] Type as argument

2011/5/20  <s.wong.731 at>:
>> The problem is that the types don't match: You've specified in the
>> "fixes" clause that f should take an argument of type "'a itself", but
>> in the "defines" clause the argument has type "nat itself". Try the
>> following:
>> consts a :: nat
>> locale A1 =
>> fixes f :: "nat => 'a itself => bool"
>> defines "f s (t::'a itself) == (if s = a then True else False)"
>> Also note that you must use meta-equality (== or \) in the
>> defines clause, rather than ordinary object-equality (=).
> Sure. But what if f is to be overloaded? E.g.,
> instantiation nat :: foo
> begin
> definition d1: "f s (t::nat itself) = (if s = a then True else False)"
> instance ..
> end
> instantiation real :: foo
> begin
> definition d2: "f s (t::real itself) = (if s = a then False else True)"
> instance ..
> end
> but with 'f' and the definitions inside a locale.

I am sorry, but this is not possible. Functions that are fixed by a
"fixes" clause in a locale cannot be overloaded or polymorphic; they
each must have a single, fixed type. (They may mention type variables
like 'a, but this does not make them polymorphic -- such type
variables are treated as fixed types within the locale context).

A workaround may be possible, though: You can define "f" at the top
level, making it polymorphic or overloaded. Then you can put
assumptions about the definitions of "f" at various types inside a
locale. For example:

class foo =
 fixes f :: "nat => 'a itself => bool"

consts a :: nat

locale A =
  assumes "f s TYPE('a::foo) = (if s = a then True else False)"
  assumes "f s TYPE('b::foo) = (if s = a then False else True)"

Later on, you could interpret locale A with type 'a instantiated as
nat, and type 'b as real.

- Brian

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