> 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 (* Un
Quoting Lars Noschinski :
How is interpretation related to print_context? It seems that
neither interpret nor interpretation extends the context as
displayed by print_context?
I don't know the answer to that, but for a particular locale x you
should be able to find all active interpretati
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
On 21.05.2013 13:59, Makarius wrote:
I do this usually by searching backwards for "context" (which means I
might miss contexts opened by "locale") or manually search through the
sidekick. To check whether I am in a local context at all, I usually
insert an additional "end" command and look for an
Quoting Makarius :
Does it mean you propose to discontinue "(in a)" at some point?
Exactly. Too early right now, but eventually this might make sense --
especially if the IDE provides suitable refactorings. Of course, this
wouldn't let us scrap a lot of code, but the Isar language could
On Tue, 21 May 2013, Lars Noschinski wrote:
On 21.05.2013 12:46, Makarius wrote:
An old idea on my list is to add some support to the Prover IDE to
rework theories with many consecutive "(in a)" to use just one "context
a begin ... end" around it -- this is also more efficient. Apart from
that
On 21.05.2013 12:46, Makarius wrote:
An old idea on my list is to add some support to the Prover IDE to
rework theories with many consecutive "(in a)" to use just one "context
a begin ... end" around it -- this is also more efficient. Apart from
that I have occasionally considered to provide expl
Naturally this notation is less important than before, and never strictly
essential. But would we save much by eliminating it?
Larry
On 21 May 2013, at 11:46, Makarius wrote:
> Does it mean you propose to discontinue "(in a)" at some point?
>
> An old idea on my list is to add some support to
On Wed, 17 Apr 2013, Clemens Ballarin wrote:
Quoting Makarius :
That is just a matter of modularity of concepts: the older "(in a)"
notation was slightly generalized at some point to allow named contexts as
sketched above
In any case, I'm not sure how useful the old notation still is. Maybe
Hi,
Am Mittwoch, den 24.04.2013, 19:16 +0200 schrieb Florian Haftmann:
> This is a great triumph of the »local everything« approach.
I’m not sure that I understand all that is going on, but I have the
feeling that the theory that I’m working on will greatly benefit from
your development, and I’m
> But for the moment I will leave this aside anyway.
Still one thing to add:
http://isabelle.in.tum.de/repos/isabelle/rev/cb154917a496
avoids the odd reinit entirely, the critical lines being
> fun add_dependency locale dep_morph mixin export =
> (Local_Theory.raw_theory ooo Locale.add_depend
See now http://isabelle.in.tum.de/repos/isabelle/rev/e4b5bebe5235.
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
permanen
Hi Clemens,
> Please let me know if you need to make changes to locales.ML. I want to
> make sure that routes out of certain quirks there don't get blocked
> accidentally.
the only change to locales.ML in the pipeline is
http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/interpretation/rev/218214
This view is correct, but it is not the whole story. Since the system
maintains a graph of interpretations and follows them transitively,
the effect achieved by
sublocale locale < expression
is much like
instance class < sort
of the old user interface to type classes. This relationsh
Hi Florian,
OK, then we agree on this.
Please let me know if you need to make changes to locales.ML. I want
to make sure that routes out of certain quirks there don't get blocked
accidentally.
Clemens
Quoting Florian Haftmann :
Hi Clemens,
I still see us disagree on how far the loca
Hi Clemens,
>> I still see us disagree on how far the local theory game can be driven
>> wrt. interpretation, nevertheless I can imagine that there is an
>> intermediate road map which we can agree on:
>>
>> * Extend sublocale for use within locale targets s.t.
>
> This is fine with me. Will thi
Let me just make some remarks as a user. At ITP 2011 I published a paper
http://www21.in.tum.de/~nipkow/pubs/itp11.html where I showed how to use locales
to structure stepwise development of modules (see p11). In that context I
intentionally used the notation
interpretation (in A) B-expr
instead
Quoting Makarius :
On Fri, 12 Apr 2013, Clemens Ballarin wrote:
That sounds a bit dogmatic. If additional commands are made
available for targets, then the syntax should clearly be more
flexible if better intuition can be achieved.
That is just a matter of modularity of concepts: the old
Hi Florian,
I still see us disagree on how far the local theory game can be driven
wrt. interpretation, nevertheless I can imagine that there is an
intermediate road map which we can agree on:
* Extend sublocale for use within locale targets s.t.
This is fine with me. Will this work for name
Hi Clemens,
> I hope,
> though, it has become clear that I'm not opposed to having
> interpretation in locale contexts by principle, I'm merely opposed to
> explaining them in the way you propose.
I still see us disagree on how far the local theory game can be driven
wrt. interpretation, neverthe
On Fri, 12 Apr 2013, Clemens Ballarin wrote:
foo (in l) ...
is equivalent to
context l
begin
foo ...
end
by construction. We cannot have just one of them.
That sounds a bit dogmatic. If additional commands are made available for
targets, then the syntax should clearly be more flexible
Hi Florian,
I do not object to your suggestion, and it is clearly in reach within
the current code base. But... it is a different thing. Your suggestion
is to make sublocale work in locale targets seamlessly. But something like
instantiation ...
begin
sublocale ...
instance ...
end
then
Hi Clemens,
Let those thoughts sink further few days. If there is no veto until
Apr
7th, I would go ahead to turn the patches upstream.
>
> You have proposed a change about which doubts were raised. I don't
> consider it acceptable to then announce a deadline after which you will
Quoting Florian Haftmann :
Let those thoughts sink further few days. If there is no veto until Apr
7th, I would go ahead to turn the patches upstream.
You have proposed a change about which doubts were raised. I don't
consider it acceptable to then announce a deadline after which you
wil
>> Let those thoughts sink further few days. If there is no veto until Apr
>> 7th, I would go ahead to turn the patches upstream.
>
> Well, here is my veto.
OK. Let's go one step back.
As a preamble, note that I do not care much about »teminology«, but have
to give some ephemeral names to thing
Quoting Florian Haftmann :
Let those thoughts sink further few days. If there is no veto until Apr
7th, I would go ahead to turn the patches upstream.
Well, here is my veto.
I don't see that much of a discussion has taken place yet, and I am
very unhappy about the concepts and terminology
> Right now we should merely have clear terminology in the discussion.
> The language keywords can be finalized later.
Indeed. In this delicate corner, modifying surface syntax makes little
headache. Lets get right the mental model and the internal
implementation first.
> Note that 'interpret'
On Wed, 27 Mar 2013, Florian Haftmann wrote:
After one further round of thinking, I would still suggest
* »interpretation« for interpretation without subscription
* »subscription« for interpretation with subscription
I think it is worth to distinguish these on the surface. Maybe future
will br
After one further round of thinking, I would still suggest
* »interpretation« for interpretation without subscription
* »subscription« for interpretation with subscription
I think it is worth to distinguish these on the surface. Maybe future
will bring different possibilities with »private« or wh
>> You might still argue about syntax, e.g. having separate commands
>> subscription – what is currently interpretation and subscription, not
>> in free-floating contexts (as implemented in the patches).
>> interpretation – only in confined contexts (locales, context begin …
>> end, but not globa
> Does that mean that 'interpretation' within unnamed 'context begin ...
> end' is without permanent subscription, but "in" a named target context
> or the global theory it is still with subscription as before?
This is the idea as it would follow from generalisation of the existing
sources.
> context B begin
> interpretation A
> interpretation A'
> interpretation A''
> end
> sublocale B < A''
What you currently have in many places (e.g.
http://isabelle.in.tum.de/reports/Isabelle/file/757fa47af981/src/HOL/Lattices.thy)
is the pattern.
context B begin
…
end
sublocale B
On Wed, 27 Mar 2013, Makarius wrote:
Note that we have one more aspect in the back-end that could help here: the
'private' modifier.
The "back-end" above should be read as "back-hand", although these are
homophones for Frenchmen.
Makarius
___
On Tue, 26 Mar 2013, Makarius wrote:
Semantically, do you remember reasons why we did not consider it so far, or
was it just forgotton or lost in state-budget problems?
I now recall some aspects from the wild days of all that (2006/2007), when
we built up that national debt. (Unlike Cyprus w
On Tue, 26 Mar 2013, Florian Haftmann wrote:
Clemens Ballarin wrote:
Currently, sublocale is used for two purposes:
a) relating two locales to each other (such as "a total order is a
lattice")
b) import (a typically small number of) lemmas, which are needed for
establishing some result, from
On Tue, 26 Mar 2013, Florian Haftmann wrote:
Recently the local theory concept has been enriched with free-floating
contexts
context
fixes … assumes …
begin
…
end
Now what would
context
…
begin
…
interpre
Hi Clemens,
nice to hear from you.
Let me add my perspective here, and see how we can converge.
> 2. sublocale and interpretation are more different than it looks:
> interpretation provides inheritance of mixins (or, from the user
> perspective, rewrite morphisms) and it is possible to amend mix
Hi Florian,
I'm in favour of generalising interpretation to targets, but in my
opinion it would not be right to provide the sublocale command as the
interpretation command in a locale context. There are two reasons:
1. sublocale modifies the locale graph of the underlying theory. This
i
> Semantically, do you remember reasons why we did not consider it so far,
> or was it just forgotton or lost in state-budget problems? We have a
> little bit of budget now after the release and towards the summer, but
> we need to stay within a reasonable range of complexity.
Well, we always hav
On Sun, 24 Mar 2013, Florian Haftmann wrote:
There is a series of minimal invasive patches to generalize
»interpretation« / »sublocale« to »interpretation« in arbitrary targets,
not just theories and locales. The patches are inspectible at
http://isabelle.in.tum.de/~haftmann/cgi-bin/rep
There is a series of minimal invasive patches to generalize
»interpretation« / »sublocale« to »interpretation« in arbitrary targets,
not just theories and locales. The patches are inspectible at
http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/interpretation
Explanations follow. It is go
41 matches
Mail list logo
