# Re: [isabelle] Type as argument

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.*