[isabelle] Locale expression and contradiction
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'
lemma (in LocB) lem: "EX f s. f s = F' s"
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and