[isabelle] declaring an Assumes with attribute "simp" at the programmer's level



Lots of questions.

I want to set up a locale with an Element.Assumes element that gives
an assumption that I want marked with the "simp" attribute.

In other words, I want to construct something like

        Element.Assumes
          [((<name>, [ ??? ]),
            [(<a term of type bool, or should it be Prop?>, [])])]

where this will be passed to Locale.add_locale_i.

Unfortunately, I can't see what I should put in the place of ???

I hoped that Simplifier.simp_add might be usable (this is what I can
use if I'm doing a PureThy.add_defs_i), but that has the wrong type.

Instead, the ??? has to be a Args.src.  This type looks a bit
confusing, but it seems like it encodes the raw syntax of attributes
at the Isar language level.  The functions Attrib.attribute{_i} then
look like the "parsers" that turn src values into attributes.  If I
could figure out how to create a Args.src value that corresponded to
the string "simp", I could presumably use that, though that seems a
pretty ugly route to have to take.

Or should I just stop trying to use the attribute interface here, and
manually call addsimps on the theory resulting from the call to
add_locale?  And if so, what function do I use to do that?  The
function change_simpset_of function has this scary unit return type,
and I know from recent discussions that I should be wary of those.

Moreover, once I'm at the level of calling addsimps, how do I get
something of type thm out of the context that I just created?   There
are a few functions in Thm that look plausible:

  val get_axiom_i: theory -> string -> thm
  val get_axiom: theory -> xstring -> thm
  val get_def: theory -> xstring -> thm
  val axioms_of: theory -> (string * thm) list

Does an Assumes element count as an axiom?  And what's the difference
between a string and an xstring here?

Michael.





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