[isabelle] Selecting from extended records



Dear mailing list,

I'm trying to develop a theory using modular records built from smaller
records in an arbitrary way. That is, I don't want to have to commit to
the order right at the beginning by using the "+" notation for
extending records. This seems to be partly achievable but has
limitations in that, e.g., selectors are not applicable. For example, I
define the component records:

  record out = out :: string
  record env = env :: "(string * val) list"

I can then define operations on these smaller records that carry over
to the bigger ones, e.g. a notion of composition:

  class composable = 
    fixes compose :: "'a => 'a => 'a" (infix ";;" 60)

  instantiation unit :: composable
  begin
    definition compose_unit_def:
      "u1 ;; u2 = ()"
  ...

  instantiation out_ext :: (composable) composable
  begin
  definition compose_out_def: 
    "r1 ;; r2 = 
     (| out = (out r1) @ (out r2), ... = (out.more r1) ;; (out.more
  r2)  |)"
  ...

  instantiation env_ext :: (composable) composable
  begin
    definition compose_env_def:
      "r1 ;; r2 = ( 
        if (env r1 = env r2) then
          (| env = env r2, ... |) = (env.more r1) ;; (env.more r2) |)
        else undefined)"
   ...


Now I can have values of combined record types ("env out_ext" or "out
env_ext"), e.g.

  value "(| out = ''abc'', env = [ (''x'', v) ] |)"

I can apply the overloaded operations to such values:

  value "(| env = [ (''x'', v) ], out = ''abc'' |) ;;
         ;; (| env = [ (''x'', v) ], out = ''def'' |)"

and I can also select the first element:

  value "out (| out = ''abc'', env = [ (''x'', v) ] |)"

However, since the selector for, e.g., env is only defined on "'a
env_scheme", I cannot apply it if env is not the first element in the
record:

  value "env (| out = ''abc'', env = [ (''x'', v) ] |)"

Is there a way to select any element from such mix-and-match records?

If this is currently not possible, is there an inherent limitation in
the underlying ML implementation of records? I've had a brief look at
"HOL/Tools/record.ML" but didn't have much time to dive into it yet.

It is possible to define an overloaded selector using via type classes
(see attached theory), but this seems too much work.

Alternatively, I think it would also be interesting to have a more
general record definition construct, such as:

  record out = ...
  record env = ...
  record big_record = out + env + ...

which would have the effect of:

  record out = ...
  record env = out + ...
  record big_record = env + ...


My example theory is attached.

Kind regards,
Ferdinand

Attachment: RecordsExample.thy
Description: Binary data



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