[isabelle-dev] Interpretation in arbitrary targets.

Lars Noschinski noschinl at in.tum.de
Wed May 22 12:45:03 CEST 2013

On 23.04.2013 19:37, Florian Haftmann wrote:
> See now http://isabelle.in.tum.de/repos/isabelle/rev/e4b5bebe5235.

This does not seem to work for me in 06db08182c4b:

theory Interpretation imports Main begin

locale A begin
definition f :: bool where "f ≡ True"

context begin
interpretation I: A by unfold_locales
thm I.f_def (* Unknown fact "I.f_def" *)

interpretation I: A by unfold_locales
thm I.f_def (* Works *)

It seems that the interpretation inside the context block has no effect 
at all?

> When following the suggestions of the ML code
> http://isabelle.in.tum.de/repos/isabelle/file/9e4220605179/src/Pure/Isar/expression.ML#l42
> I am personally still in favor of only three Isar keywords, corresponding to
> 	permanent_interpretation
> 	ephemeral_interpretation
> 	interpret
> with the perspective to generalize permanent_interpretation from named
> targets to arbitrary targets by means of a dedicated local theory
> operation, like Local_Theory.subscription in the previous series of
> patches.  But for the moment I will leave this aside anyway.

I don't know whether this is what you are talking about, but there is 
one functionality I would like to have for my Graph theory:

I have a locale (or rather, a locale hierarchy) describing a single 
graph. I chose this formalization as I usually talk about a single 
graph. However, if I want to talk about multiple graphs (for example 
because I want to prove properties of union) it would be nice to
switch to a mode of working as in HOL-Algebra (i.e. have an explicit 
domain and all lemmas only hold for elements of the domain).

It seems with your suggestion above, I could do something like

locale graphs =
   defines GG = "{G. graph G}"

   fixes G assumes "G : GG"

permanent_interpretation graph G sorry


to get all the lemmas of graph in graph, with the additional assumption 
"G : GG". Of course, one would need to transfer the automation manually, 
as in particular elim and dest are not stable under such a transformation.

   -- Lars

More information about the isabelle-dev mailing list