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

[Florian Haftmann]

Dear Michael,

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

The key combinator you need is Attrib.internal which lifts an explicit
attribute function to its "src" representation.

Btw. your proposition should be prop (cf. HOLogic.mk_Trueprop (in HOL)
or ObjectLogic.ensure_propT (in Pure)).

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

These functions are indeed only for retrieval of foundational axioms (on
the theory level, not on the (probably local) context level).  Usually
local assumptions are just passed value-oriented, e.g. Assumption.
add_assumes not only extends the context but also hands back the
assumptions as theorems to proceed with.

For locales the case is more delicate since you won't have direct access
to the assumptions.  But you could do an educated guess based on
Locale.intros and Locale.dests - please call back on me if you really
have to go that way.

Hope this helps
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 252 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20080403/830d0e92/attachment.sig>