Re: [isabelle] Type as argument



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
>




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