*To*: Cl-isabelle Users <cl-isabelle-users at lists.cam.ac.uk>*Subject*: [isabelle] Selecting from extended records*From*: Ferdinand Vesely <csfvesely at swansea.ac.uk>*Date*: Tue, 25 Nov 2014 18:58:07 +0000*Organization*: Swansea University

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

**Follow-Ups**:**Re: [isabelle] Selecting from extended records***From:*Thomas Sewell

- Previous by Date: [isabelle] AExp.thy
- Next by Date: Re: [isabelle] Selecting from extended records
- Previous by Thread: Re: [isabelle] AExp.thy
- Next by Thread: Re: [isabelle] Selecting from extended records
- Cl-isabelle-users November 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list