Re: [isabelle] Locale parameters



Hi John,

[...]

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"

Your question is actually not directly related to locales. Have a look at Isabelle/HOL's term syntax (which should be explained in the Isabelle/HOL tutorial).

All occurrences of c denote the same variable, which is implicitly universally quantified at the outer most level. Also note that --> binds less tightly than & and is right associative. That is, lem1 amounts to this:

  !!c. ALL a b. (L1 c --> ((c = a & L2 c) --> (c = b & a ~= b)))

What you want is a lemma like this:

  L1 a & L2 b --> a ~= b

Clemens






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