[isabelle] Locale command raises error "Bad head of lhs: existing constant"



Dear locale experts,

Suppose the locale l1 defines one of its parameter using "defines". When another locale l2 imports l1 and tries to instantiate the defined parameter in the locale expression, Isabelle2015 complains about bad left-hand sides and existing constants. Here is the minimal (silly) example:

locale l1 =
  fixes x y :: nat
  defines "y == x"

locale l2 = l1 2 "Suc 1" (* error: Bad head of lhs: existing constant Suc *)

What is the right way to instantiate defined parameters in locale expressions?

Here is some background on my use case. I want to abstract over a monad in some definitions, so I have a locale for monads (I need the monad operation only on a single type, so this works). As every monad is also a functor, I can define the map operation canonically in terms of bind and return. Later, I want to specialise the monad to concrete instances such as 'a option, which I thought could be done by instantiating the locale parameters in the locale expression. Of course, I also want to replace all instances of the canonical map with map_option in all theorems.

If I define the map in the locale for monad as a constant, the replacement has to be done at every interpretation or sublocale command using a where clause (and a corresponding proof of equality of definitions). Unfortunately, I have not found a way to do the replacement during locale imports. Therefore, I tried to use the defines element and move the definition to the locale declaration itself. But this causes trouble, too.

Andreas




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