[isabelle] Locale expression and contradiction



Hi,

I was wondering whether two locales that contradict with each other
can be combined in a local expression. For example:

locale LocA =
  fixes F :: "real => real"

locale LocB = LocA +
  assumes "F p = 0"
  and "G p = 1"

locale LocC = LocA +
  assumes "F p = 1"

locale LocExp =
LB: LocB F + LC: LocC F'
for F F'

begin
lemma (in LocB) lem: "EX f s. f s = F' s"
by auto
end

Is the reason why the lemma can be discharged that the locale LocExp
is inconsistent? Is the lemma what I think it is, i.e. there exists
some function f and some argument s to f in the locale LocB such that
all values returned are same as those returned by F in LocC for the
same argument?

Thanks
John





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