*To*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Generic Contexts and Generic Data*From*: Christian Sternagel <c.sternagel at gmail.com>*Date*: Tue, 11 Nov 2014 16:30:23 +0100*In-reply-to*: <54622575.1070509@gmail.com>*References*: <54622575.1070509@gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.2.0

val ((cs, c_simps), lthy') = BNF_LFP_Rec_Sugar.add_primrec bindings equations lthy As a more concrete example take: local_setup {* fn lthy => let val cs = [Free ("c", @{typ "'a list => 'a list => 'a list"})] val equations = [ @{prop "c ([]::'a list) (ys::'a list) = ([]::'a list)"}]

val equations' = map (pair Attrib.empty_binding) equations; val ((cs, c_simps), lthy') = BNF_LFP_Rec_Sugar.add_primrec bindings equations' lthy; val _ = @{print} (cs, c_simps) in lthy' end *}

cheers chris On 11/11/2014 04:04 PM, Christian Sternagel wrote:

Dear experts, what is the canonical way of turning a function add :: key => value => Context.generic => Context.generic into a function of type "key => value => local_theory => local_theory"? Btw: The reason for the type of "add" is that it is the add-function for some generic data (i.e., something of the form "structure Data = Generic_Data (...)"). More specifically I have add key value = Data.map (Symtab.update_new (key, value)) Until now I used "Local_Theory.declaration" (and applied the obtained morphism to all elements of my "value", which happen to be terms or theorems). Although I have to admit that I'm clueless about the meaning of the "syntax" and "pervasive" flags of "Local_Theory.declaration" (so I just used "false" for both). Doing the above I obtain the function: add' key value = Local_Theory.declaration {syntax=false,pervasive=false} (fn phi => add x (apply phi value) which is itself of type "key => value => local_theory => local_theory". The reason why I'm asking is that I recently found out that my "add" function is actually called 3 times every time "add'" is called and the morphism applied to "value" seems to be different the last time (i.e., constants, generated via "BNF_LFP_Rec_Sugar.add_primrec" that are "Const"s as expected the first 2 times, are "Free"s the 3rd time). cheers chris

**Follow-Ups**:**Re: [isabelle] Generic Contexts and Generic Data***From:*Dmitriy Traytel

**References**:**[isabelle] Generic Contexts and Generic Data***From:*Christian Sternagel

- Previous by Date: [isabelle] Generic Contexts and Generic Data
- Next by Date: [isabelle] First CFP CICM 2015
- Previous by Thread: [isabelle] Generic Contexts and Generic Data
- Next by Thread: Re: [isabelle] Generic Contexts and Generic Data
- 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