*To*: Brian Huffman <brianh at cs.pdx.edu>*Subject*: Re: [isabelle] Type as argument*From*: Steve W <s.wong.731 at gmail.com>*Date*: Fri, 13 May 2011 17:55:57 +0100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <BANLkTinT-2mQ7--5Y9ADLDCOrt9uW_dbVw@mail.gmail.com>*References*: <BANLkTin0NNwByvPfmmnMZGMo0Wm0yrXCBw@mail.gmail.com> <BANLkTinT-2mQ7--5Y9ADLDCOrt9uW_dbVw@mail.gmail.com>

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 free variable though. Why's that? Thanks Steve On Fri, May 13, 2011 at 5:16 PM, Brian Huffman <brianh at cs.pdx.edu> wrote: > On Fri, May 13, 2011 at 8:16 AM, Steve W <s.wong.731 at gmail.com> wrote: > > Hi, > > > > I have a quick question: does anyone know how to define a function taking > a > > type as an argument? Say, a function f taking the type "nat" as an > argument. > > > > Thank you > > Steve > > > > Well, overloaded constants are a little bit like functions taking > types as arguments. Depending on what you want to do, this kind of > class definition might be useful: > > class foo = > fixes f :: "'a itself => int" > > instantiation nat :: foo > begin > definition "f (t::nat itself) = 0" > instance .. > end > > instantiation list :: (foo) foo > begin > definition "f (t::'a list itself) = 1 + f TYPE('a)" > instance .. > end > > Now you can prove things like > > lemma "f TYPE(nat list list list) = 3" > by (simp add: f_list_def f_nat_def) > > (I haven't tested the above code, so there may be typos.) > > Here you can think of "f" as almost a function from types to integers: > You can essentially do primitive recursion over the structure of the > type argument, defining each case with class instantiations. > > - Brian >

**Follow-Ups**:**Re: [isabelle] Type as argument***From:*René Thiemann

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

**References**:**[isabelle] Type as argument***From:*Steve W

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

- Previous by Date: Re: [isabelle] Type as argument
- 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