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.