# [isabelle] Conflicting locales with a common signature

*To*: isabelle-users at cl.cam.ac.uk
*Subject*: [isabelle] Conflicting locales with a common signature
*From*: Michael Chan <mchan at inf.ed.ac.uk>
*Date*: Sun, 18 Jul 2010 16:13:43 +0100
*User-agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.9.1.7pre) Gecko/20091216 Shredder/3.0.1pre

Hi all,

`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'

`Clearly, loc1 and loc2 conflict with each other due to loc1.ax1 and
``loc2.ax1. Since they both contain the constant 'f', could one come up
``with a theorem stating that there exists a function 'func' and a real
``number 'x' such that 'func x > 0' holds in one locale (loc1) and 'func x
``= 0' holds in another (loc2)? Something in a similar shape as
`
lemma (in locexp) lem: "EX func x. func x > 0 & func x = 0"

`but that's inconsistent. Are there ways to annotate the variables, e.g.,
``"EX func x. l1.func x > 0 & l2.func x = 0", or something similar?
`
Thanks in advance.
Regards,
Michael
--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

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