Re: [isabelle] Conflicting locales with a common signature
On 19/07/2010, at 1:13 AM, Michael Chan wrote:
> I have a question about proving theorems about conflicting locales which share a common signature. Suppose the following:
> locale sig_loc =
> fixes f :: "real=>real"
> locale loc1 = sig_loc +
> assumes ax1: "ALL x. f x > 0"
> locale loc2 = sig_loc +
> assumes ax1: "ALL x. f x = 0"
> locale locexp =
> l1: loc1 f + l2: loc2 f'
> for f f'
Did you try this?
to see what Isabelle thinks you are trying to say.
locexp is not inconsistent - loc1 is instantiated with f, and loc2 with f' - distinct parameters. The diamond dependency you're trying to exploit doesn't work the way you think it does (I think :-).
I'd also suggest making the prefixes l1 and l2 mandatory:
locale locexp =
l1!: loc1 f + l2!: loc2 f'
for f f'
Hope this helps.
This archive was generated by a fusion of
Pipermail (Mailman edition) and