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.haftm...@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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
