*To*: Brian Huffman <brianh at cs.pdx.edu>, s.wong.731 at gmail.com*Subject*: Re: [isabelle] Type as argument*From*: s.wong.731 at gmail.com*Date*: Fri, 20 May 2011 14:58:44 +0000*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <BANLkTi=DNn3h3gAwGUCXbcfAM9bJjELKQQ@mail.gmail.com>

On May 20, 2011 2:52pm, Brian Huffman <brianh at cs.pdx.edu> wrote:

2011/5/20 s.wong.731 at gmail.com>:

>> 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 "fs (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? Eg,

>

> instantiation nat :: foo

> begin

> definition d1: "fs (t::nat itself) = (if s = a then True else False)"

> instance ..

> end

>

> instantiation real :: foo

> begin

> definition d2: "fs (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 "fs TYPE('a::foo) = (if s = a then True else False)"

assumes "fs 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.

Steve

- Brian

**References**:**Re: [isabelle] Type as argument***From:*Brian Huffman

- Previous by Date: Re: [isabelle] unexpected behaviour of user defined command in jedit
- Next by Date: [isabelle] FHIES 2011: Deadline Extended
- Previous by Thread: Re: [isabelle] Type as argument
- Next by Thread: [isabelle] structured induction
- Cl-isabelle-users May 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list