*To*: Brian Huffman <brianh at cs.pdx.edu>, Steve W <s.wong.731 at gmail.com>*Subject*: Re: [isabelle] Type as argument*From*: s.wong.731 at gmail.com*Date*: Tue, 17 May 2011 14:46:33 +0000*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>, René Thiemann <rene.thiemann at uibk.ac.at>*In-reply-to*: <BANLkTikqVASoHSvUqZw80RYT_Opw DO5VA@mail.gmail.com>

I see. But, now I have a slightly different problem: class foo1 = fixes f :: "nat => 'a itself => bool" consts a :: "nat" b :: "nat" instantiation nat :: foo1 begin definition "fs (t::nat itself) = (if s = a then True else False)" instance .. end lemma "fa TYPE(nat) = True" by (simp add: f_nat_def) This is fine. But lemma "fb TYPE(nat) = False" by (simp add: f_nat_def) doesn't seem to prove it. Can the simplifier not interpret the else clause? Thanks Steve On May 16, 2011 3:53pm, Brian Huffman <brianh at cs.pdx.edu> wrote:

2011/5/16 Steve W s.wong.731 at gmail.com>:

> Thanks all. One more question: what is the "itself" keyword for in "'a

> itself"?

The "itself" is just a type constructor. It is like what you would get

from the following datatype declaration:

datatype 'a itself = Type (* one constructor with no arguments *)

The syntax "TYPE('a)" is an abbreviation for "Type :: 'a itself".

- Brian

>

> Thanks

> Steve

>

> 2011/5/13 René Thiemann rene.thiemann at uibk.ac.at>

>

>> > Thanks. If I change f to a binary function:

>> >

>> > class foo =

>> > fixes f :: "int => 'a itself => int"

>> >

>> > and with the following instantiation:

>> >

>> > instantiation nat :: foo

>> > begin

>> > definition "f 0 (t::nat itself) = 0"

>> > instance ..

>> > end

>> >

>> > I get an error on "0::int". It works if 0 is replaced by a freevariable

>> > though. Why's that?

>>

>> Because "definition" cannot be used with pattern matching on left-hand

>> sides.

>> Usually, one can use "fun" instead. However, even with "fun" you cannot

>> do pattern matching on "int" instead of "nat".

>>

>> However, you might write "fx (t:: nat itself) = (if x = (0 :: int)then 0

>> else ...)"

>>

>> René

>> --

>> René Thiemann mailto:rene.thiemann at uibk.ac.at

>> Computational Logic Group

>> http://cl-informatik.uibk.ac.at/~thiemann/

>> Institute of Computer Science phone: +43 512 507-6434

>> University of Innsbruck

>>

>>

>

**Follow-Ups**:**Re: [isabelle] Type as argument***From:*Tjark Weber

- Previous by Date: Re: [isabelle] resend question about structured induction
- Next by Date: Re: [isabelle] Type as argument
- Previous by Thread: Re: [isabelle] Type as argument
- Next by Thread: Re: [isabelle] Type as argument
- 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