# [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?
```

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.