Re: [isabelle] Sublocale, subclass and execution.



>> context
>>   fixes …
>>   assumes …
>> begin
>>
>> permanent_interpretation …
>>
>> end
> 
> This looks interesting, but it's not clear to me what it would mean.  I take that this is a makeshift context that cannot be entered again.  Presumably the construct yields some sort of lifting?

The idea is that the context itself is embedded into a target again (for
simplicity, let us assume a locale as canonical candidate):

context foo
begin

…

context
  fixes …
  assumes P
begin

permanent_interpretation bar: bar …

end

…

end


So, technically speaking, this would establish a sublocale dependency
from bar to foo such that facts propagated from bar to foo gain
additional assumptions P.

It can be seen as a proper user-space pattern to avoid raw instantiation
of foundational facts bar… [OF …].

It is not clear to me whether that machinery can handle this out of the
box (or even properly), so this has to be figured out first.

Cheers,
	Florian

-- 

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

Attachment: signature.asc
Description: OpenPGP digital signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.