I was wondering, is there any way to import a locale in a way that changes the names it uses for the axioms, without having to write the whole locale over again? As an example of what I mean, consider the following locale for monoids:
locale monoid =
fixes zero :: "'a"
fixes plus :: "'a \<times> 'a => 'a"
assumes left_zero: "plus (zero, x) = x"
assumes right_zero: "plus (x, zero) = x"
assumes plus_assoc: "plus (plus (x,y),z) = plus (x,plus (y,z))”
Is there a way to change this to use the names “one”, “times”, “left_one”, “right_one”, and “times_assoc” without writing the whole locale over again? I was thinking something like the following, which already does what I want (if the last three lines are dropped) for changing “zero” to “one” and “plus” to “times”:
locale monoid_times = monoid
where zero = one
and plus = times
and left_zero = left_one
and right_zero = right_one
and plus_assoc = times_assoc
for one times left_one right_one times_assoc
I know that, in this particular case, what I wrote above is actually just as long as if I had re-defined monoid_times from scratch, but the context is that we often only want to change a few names, rather than all of them, so some sort of notation like this would be helpful.
Similarly, is there a way to change the type variable used, e.g., from ‘a to in monoid to ‘b in monoid_times? I know that in this case I could annotate “one” with the type variable ‘b, but in general a locale might only have elements with more complex types involving ‘a, so it might be annoying to have to write out the whole type just to change one type variable.