[isabelle] Changing axiom names in a locale



Hi,

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.

Thanks,
-Eddy



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