Re: [isabelle] Generic Contexts and Generic Data

Dear Dmitriy,

actually I also need polymorphism (hence Const instead of Free) since I get type errors (for different instances) otherwise. So, thanks for the hints! I'll look into the two different possibilities you indicated.

Rene's thread ([2] in your email) seems to indicate that in the same situation the function package uses Free variables for the defined "constant" as well as in its simplification rule. Is that canonical behaviour? If yes, any hints on its advantages compared to declaring a Const?



On 11/11/2014 07:03 PM, Dmitriy Traytel wrote:
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


[1] The invasiveness of restore shows up, e.g. here:


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 =>
  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) => ( 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)

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



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 = (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).



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