Constraining type variables in locales

Question

The Isabelle library contains the classes real_inner and real_normed_vector, the latter of which is declared a subclass of the former in ~~src/HOL/Library/Inner_Product.thy.

Now, suppose we have a locale

locale foo =
  fixes goo :: "'a::{real_normed_vector} => bool"

and wish to extend this locale with some new constants, and also constraining the sort of 'a to be real_inner at the same time, like so:

locale extended = foo +
  fixes ext :: "'a::{real_inner} => nat"

Is there a way to do this? Trying to do this using the examples above sees Isabelle give goo the type 'b::{real_normed_vector} => bool in extended, when I instead require the type 'a::{real_inner} => bool.

Answer 1

You can do it like this:

locale extended = foo goo
  for goo :: "'a :: real_inner ⇒ bool" +
  fixes ext :: "'a => nat"