[isabelle-dev] Two simple beginners question

[René Thiemann]

Dear all,

I'm currently trying to develop a package for automatic generation of linear orders for datatypes.
I have already defined some functions which generate the corresponding equations which encode the linear order.

Now the first question I have is how to store these functions:
- when registering the equations via the function package (Function.add_function) I essentially have
  a local theory transformer of type "lthy -> lthy"
- afterwards, I would like to store the newly created constant of the function symbol and some other data 
  in some global store so
  that I can reuse it later in other generated orders. Here, I currently use
  structure Ordering_Data = Theory_Data( type T = ...)
  with the update function Ordering_Data.map (Symtab.update ...)
  which is essentially a theory transformer of type "thy -> thy"
- how is it now possible to combine these transformers into one method foo, such that either
  setup {* foo "my_datatype" *} or local_setup {* foo "my_datatype" *}
  can both register the function via the function package, and also store all informations in
  the Ordering_Data store.
  To be more precise: Is there a way to convert a function (lthy -> lthy) into a function (thy -> thy)
  or vice versa?

The second is a rather simple ML question:
- Is it possible to conveniently update single fields in a record as in OCaml?
  E.g., val r1 = {a = 5, b = "foo", c = ..} and many fields
        val r2 = '' r1 where only b is changed to "bar" ''
             (in OCaml: val r2 = {r1 with b = "bar"})

Best regards,
René

-- 
René Thiemann                    mailto:rene.thiemann at uibk.ac.at
Computational Logic Group        http://cl-informatik.uibk.ac.at/~thiemann/
Institute of Computer Science    phone: +43 512 507-6434
University of Innsbruck