Email Gateway (Aug 19 2022 at 15:39): Email Gateway (Aug 19 2022 at 15:39):From: Daniel Raggi <danielraggi@gmail.com>
I'm experimenting with modifying theorems via attributes.
Let's say I make a function
fun my_fun ctxt thm =
Simplifier.simplify (modify_context ctxt) thm
where modify_context adds a couple of simp rules via function
addsimps. I run the function at the ML level on an example theorem and
it does what I want.
Then I make a function
fun my_attr ctxt = Thm.rule_attribute (K (my_fun ctxt))
and set it up in Isabelle:
attribute_setup my_attr = {* Scan.succeed (my_attr @{context})*} " "
This seems to succeed, but when I run "thm some_theorem[my_attr]" I
get an exception from the raw simplifier with message "rewrite_cterm:
bad background theory". Why would this be?
Thanks.
Daniel
Email Gateway (Aug 19 2022 at 15:39):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Daniel,
attribute_setup my_attr = {* Scan.succeed (my_attr @{context})*} " "
@{context} injects the static context, i. e. the context at the
position you are writing your declaration. But here you need the
dynamic context, e.g. via something like
attribute_setup my_attr = {* Scan.peek (my_attr o Context.proof_of) *}
Note that static contexts are rather seldom appropriate, mostly for
experimenting. The system is built in a way that the appropriate
dynamic contexts is provided for nearly all crucial slots as a
functional argument.
AFAIR the Isabelle implementation manual provided more detail (I did not
take a look quite now).
Hope this helps,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 16:03):From: Makarius <makarius@sketis.net>
This is non-canonical in various respects, and thus fails as expected.
Moreover, the terminology "the ML level" for Isabelle/ML and "Isabelle"
for Isabelle/Isar is suspicious, and probably stems from unreliably
sources of information.
Here are some general principles of survival in Isabelle tool
development:
* Look around what the official reference manuals say. Usually the
"isar-ref" manual has an topmost entry point for each command,
sometimes pointing to other manuals. The "implementation" manual is
particularly important to understand the underlying principles of
Isabelle/ML. It is often considered as dry, but contains a lot of
relevant information in relatively little space.
* Look around for applications that are analogous to what you are
trying to do, and develop a sense how close they are to a standard
approach, and what needs to be changed for your particular
application. Stick to the Isabelle standards you see in canonical
sources.
The "looking around" is particularly easy with Isabelle/jEdit that
serves as Prover IDE and IDE for Isabelle tool development at the same
time. Just use the hover-click idiom to figure out the definitions of
well-known attributes from Isabelle/Pure or Isabelle/HOL. Or use
hyper-search for "attribute_setup" in authoritative sources: it quickly
yields some abstract examples of some rule attribute and declaration
attribute in $ISABELLE_HOME/src/Doc/Isar_Ref/Spec.thy namely:
attribute_setup my_rule = {*
Attrib.thms >> (fn ths =>
Thm.rule_attribute
(fn context: Context.generic => fn th: thm =>
let val th' = th OF ths
in th' end)) *}
attribute_setup my_declaration = {*
Attrib.thms >> (fn ths =>
Thm.declaration_attribute
(fn th: thm => fn context: Context.generic =>
let val context' = context
in context' end)) *}
Makarius
Last updated: Apr 25 2024 at 01:08 UTC