Re: [isabelle] Conflicting locales with a common signature



Michael,

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?

Try saying:

print_locale! locexp

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.

cheers
peter




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