[isabelle] Conflicting locales with a common signature



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.