[isabelle-dev] Interpretation in arbitrary targets.

[Lars Noschinski]

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"
end

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

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}"
begin

context
   fixes G assumes "G : GG"
begin

permanent_interpretation graph G sorry

end
------------------------------------------

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