Re: [isabelle] "rewrite_cterm: bad background theory"



On Thu, 28 Aug 2014, Daniel Raggi wrote:

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 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





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