[isabelle-dev] Interpretation in arbitrary targets.

[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.

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 things, not yet graved into stone, to be
able speak about them.

So lets compare our suggestions systematically. I refer to the most
condensed statements available in this thread.

Your suggestion has been:

> a) relating two locales to each other (such as "a total order is a lattice"):
> 
> context B begin
>   …
> end
> sublocale B < A'' 
> 
> b) Non-persistent interpretation
> 
> context B begin
>   ...
>   interpretation A
>   ...
> end
> 
> makes the interpretation of A available in the block up to the closing 'end'.  The interpretation will not be persisted; results are only available temporarily to aid establishing some results in B.

Your argument for a separate top-level sublocale command has been that
it adding a dependency should not happen in a non-global context.

I do not follow that argument for two reasons,

a) on in the frontend:

> 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 < …
> 
>   context B begin
>   …
>   end
> 
>   sublocale B < …
> 
>   context B begin
>   …
>   end
> 
> When giving up the paradigm that sublocale dependencies may only be
> introduced on the global level, you end up with sth. like
> 
>   context B begin
>   …
>   interpretation …
>   …
>   interpretation …
>   …
>   end
> 
> which is compacter and more intuitive.

b) The unification of today's »interpretation« and »sublocale« is
already inherent in the existing code and needs »only« be unburried by
surgery.

I have transformed your argument concerning sublocale to the statement that
* interpretation with permanent effect (what I have been calling
subscription) and
* interpretation without permanent effect
should be issued by different keywords, to make the distinction clear
and to disambiguate situation like

  context B begin
  …
  interpretation
  …
  end

Note you could disambiguate that by requiring that each interpretation
without permanent effect resides in an unnamed context begin … end
block, but this would result in a bulky structure either, with closing
ends dangling towards the end:

  context B begin
  …
  context begin
  …
  interpretation …
  …
  context begin
  …
  interpretation …
  …
  end
  …
  end
  …
  end

So, I argue for separate keywords here.

Overall, my ideas are not driven by a certain desired behaviour.  It is
the code »as it is« which suggests the full integration of locale
interpretation with local theories, as I have shown in the consecutive
series of patches opening this thread.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 261 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130405/3219fcb1/attachment.sig>