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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
