Re: [isabelle] Code generation for functions defined in locales

Hi Peter,

the bad news are that there is no direct way to accomplish code
generation from equations stemming from interpretation.  The good news
are that you can use the optional "where" part of interpretation to
manually accomplish this:

locale test =
  fixes a :: "nat => nat"

  primrec test where
    "test [] = (0::nat)" |
    "test (x#xs) = a(x + test xs)"

  definition "c = a (7::nat)"


definition "nf x = x"

(* define constants corresponding to the local specifications *)
definition "t = test.test nf"
definition "c = test.c nf"

interpretation t: test nf where
  (* give these as equations *)
  "test.test nf = t"
  and "test.c nf = c"
qed (simp_all add: t_def c_def)

lemmas [code] = t.c_def t.test.simps

definition "some_fun l = t.c + t.test l"

export_code some_fun in SML file -

Hope this helps



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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