Email Gateway (Aug 19 2022 at 16:26): Email Gateway (Aug 19 2022 at 16:26):From: Makarius <makarius@sketis.net>
Going back to this very abstract level of the original question on this
thread: Yes, two times false is fine as a default.
These options correspond to the following variants of declaration commands
that are described in the isar-ref manual:
\item @{command "declaration"}~@{text d} adds the declaration
function @{text d} of ML type @{ML_type declaration}, to the current
local theory under construction. In later application contexts, the
function is transformed according to the morphisms being involved in
the interpretation hierarchy.
If the @{text "(pervasive)"} option is given, the corresponding
declaration is applied to all possible contexts involved, including
the global background theory.
\item @{command "syntax_declaration"} is similar to @{command
"declaration"}, but is meant to affect only ``syntactic'' tools by
convention (such as notation and type-checking information).
Makarius
http://stop-ttip.org 925,664 people so far
Email Gateway (Aug 19 2022 at 16:37):From: Christian Sternagel <c.sternagel@gmail.com>
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
Email Gateway (Aug 19 2022 at 16:37):From: Christian Sternagel <c.sternagel@gmail.com>
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
Email Gateway (Aug 19 2022 at 16:37):From: Dmitriy Traytel <traytel@in.tum.de>
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
Email Gateway (Aug 19 2022 at 16:38):From: Christian Sternagel <c.sternagel@gmail.com>
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?
cheers
chris
Email Gateway (Aug 19 2022 at 16:39):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Christian,
this is quire regular: usually a declaration in a local theory has
effect on three levels:
Hope this helps,
Florian
signature.asc
Last updated: Oct 31 2025 at 04:26 UTC