[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.