[isabelle-dev] Interpretation with definitions [was Locale interpretation with mixins]

[Clemens Ballarin]

Hi Florian,

I appreciate that you now follow my reasoning that changes to the  
locales core machinery are not necessary for getting this  
functionality.  However, I don't think we should change how locale  
expressions work.  Currently we have:

   locale loc = fixes x assumes about_x: "x = x"

   interpretation const: loc less_eq by unfold_locales (rule refl)
   thm const.about_x -- {* op \<le> = op \<le> *}

   interpretation var: loc less_eq for less_eq by unfold_locales (rule refl)
   thm var.about_x  -- {* ?less_eq = ?less_eq *}

Also, I'm afraid I fail to understand the difference between 'where x  
= t' and 'where x is t'.

Clemens


Quoting Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>:

> Hi Clemens, hi Makarius,
>
> let me continue concerning syntax:
>
> The current syntax in Tools/interpretation_with_defs.ML is just a proof
> of concept:
>
> interpretation L inst
>   where
>     "bar = t"
>   defines f is foo
>
> A much better idea could be to give the new defs in a for-clause:
>
> interpretation L inst
>   for f :: T
>   where
>     "foo = f"
>     "bar = t"
>
> where the implicit definitions (f) are mentioned in the for-clause.
>
> One could also think about hiding away the full generality of a) from
> the user (for which there might be good reasons) and have something like
>
> interpretation L inst
>   for f :: T
>   where
>     f is foo
>     t is bar
>
> Or the where clause could be integrated completely into the locale
> expression using named syntax:
>
> interpretation L (| f := foo, t := bar |)
>   for f :: T
>
> Cheers,
> 	Florian
>
> --
>
> PGP available:
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
>
>