Email Gateway (Aug 18 2022 at 11:39): Email Gateway (Aug 18 2022 at 11:39):From: Michael Norrish <Michael.Norrish@nicta.com.au>
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.
Last updated: May 03 2024 at 08:18 UTC