# [isabelle] Locale parameters

Hi,
Suppose I have two locales L1 and L2:
locale L1 =
fixes c :: nat
assumes ax: "c = 0"
locale L2 =
fixes c :: nat
assumes ax: "c = 1"
and I want to prove a lemma stating that the constant 'c' in L1 does
not have the same value as the constant 'c' in L2:
lemma lem1: "ALL a b. L1 c --> c = a & L2 c --> c = b & a ~= b"
using L1.ax L2.ax
by auto
(hopefully the formulation matches my intended meaning.)
Now, if I change the parametrisation slightly:
lemma lem2: "ALL a b. L1 c --> c = a & L2 d --> d = b & a ~= b"
using L1.ax L2.ax
by auto
The proof fails. Aren't the occurrences of 'c' in lem1 distinct
instances? Which lemma actually matches my intended meaning, if any?
Any help will be appreciated. Thanks.
John

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