[isabelle] Locale command raises error "Bad head of lhs: existing constant"
- To: isabelle-users <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] Locale command raises error "Bad head of lhs: existing constant"
- From: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>
- Date: Fri, 31 Jul 2015 10:27:18 +0200
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.8.0
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and