[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:126.96.36.199pre) Gecko/20091216 Shredder/3.0.1pre
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.
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