Re: [isabelle] Generic Contexts and Generic Data



Hi Christian,

usually there is no need to "turn free variables into proper constants". Things should mostly happen automagically at the package's boundaries.

One exception is when you need polymorphism. This is actually quite often the case in the new (co)datatype package. To get the polymorphic constants we use lthy' = Local_Theory.restore lthy after the declaration, and apply the difference morphism between lthy' and lthy to the free variable (c.f. src/HOL/Tools/BNF/bnf_lfp.ML for some examples, grep for Local_Theory.define).

Ondřej Kunčar uses a slightly different idiom involving Local_Theory.target_morphism in his code (c.f. src/HOL/Tools/Lifting/lifting_def.ML), which is supposed to be slightly less invasive than Local_Theory.restore [1]. But I'm also not sure if target_morphism is what one wants in any situation.

In your case, I assume that your need to turn Frees into Consts is caused by the mismatch in the output of the primrec package (mentioned in [2]). If this is the case, I recommend to work with a forthcoming (tomorrow) development version of Isabelle, where this mismatch will vanish.

Dmitriy

[1] The invasiveness of restore shows up, e.g. here: https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2014-August/msg00200.html [2] https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2014-October/msg00145.html

On 11.11.2014 16:30, Christian Sternagel wrote:
Maybe the real question is: How do I turn the free variables in "consts" below, into proper constants?

  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 bindings = map ((fn (name,ty) => (Binding.name name, SOME ty, NoSyn)) o dest_Free) cs;
  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
*}

Where the @{print} shows "c" as "Free". What is the proper way of turning this into a "Const"?

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






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