[isabelle-dev] "local_setup" and "Generic_Data"

[Makarius]

On Mon, 9 Aug 2010, Lucas Dixon wrote:

> I was wondering about that also.
>
> Is there conceptual reason that "Local_Theory.target" is needed, or is 
> it just kind of technical hiccup?

These low-level functional adaptions of variations on Context.generic are 
mostly for internal use only.  This applies to ProofContext.theory, 
Local_Theory.theory, Local_Theory.target etc. alike.


>     declaration {* fn phi => Data.map (Integer.add 3) *}

Local_Theory.declaration (or 'declaration' in Isar syntax) is the standard 
way.  Of course, the morphism phi must not be ignored in general -- it 
needs to be applied to your data as explained in the paper by 
Chaieb/Wenzel (CALCULEMUS 2007).

While it is unlikely that integer parameters can be passed through 
morphisms in a sensible way, it is mandatory for standard logical entities 
(types, terms, facts). Otherwise the declaration will only work in the 
global context, where the morphism is identity.


In many practical situations the somewhat simpler 'declare' form with 
user-defined attributes turns out more convenient.  When using the 
standard context parsers Args.typ, Args.term, Attrib.thm etc. the system 
takes care of the gory details, i.e. it is correct my canonical 
construction (in most situations).

Also note that plain bool/int/string parameters can be managed as 
"configuration options".  Then the declaration business is all managed by 
the system.


 	Makarius