Re: [isabelle] Sublocale, subclass and execution.



Hi Florian,

I like your idea of using more descriptive keywords here.  Following your suggestion, 'where' could be called 'unfolding' and replaced by 'folding' if we decide to turn the rewrite equations around.  However, the ing form tends to be used by the proof language for transformations of the proof state, and 'unfolding' would even make the grammar ambiguous.  It will probably make more sense to settle for 'defines', 'unfolds' and 'folds'.

Clemens


On 30 October, 2014 20:23 CET, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:

> Hi Clemens,
>
> sorry for the delay.
>
> On 16.10.2014 18:57, Clemens Ballarin wrote:
>
> >> permanent_interpretation prefix: expr
> >>   where f = t
> >
> > What if expr contains where clauses?  Sublocale distinguishes this (awkwardly) by slightly different syntax: "where" <term> "=" <term> within the expression vs. "where" <term> for the rewrite morphism.
>
> This was my fault.  The syntax (cf.
> src/Tools/permanent_interpretation.ML) is
>
> permanent_interpretation expr …
>   defining …
>   where …
>
> >> permanent_interpretation prefix: expr
> >>   -- ‹with implicit mixin: f_def [symmetric]›
> >
> > This, I guess, refers to the original sublocale command, right?
>
> In a locale context, yes.
>
> > I wonder whether we can come up with a syntax that permits both rewrite morphisms and definitions.  Obviously one of the two kinds of equations would have to be turned around.  Probably it would be more intuitive to reverse the notation of the rewrite morphisms.
>
> Currently, definitions are orientated the other way round than bare
> equations.  Not sure what would fit best here.
>
> Cheers,
> 	Florian
>
> --
>
> PGP available:
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
>








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