Re: [isabelle] Conditional interpretations?



On 3 Nov 2006, at 0:37, Dr. Brendan Patrick Mahony wrote:

Is there a forum where changes to Isabelle are being discussed with users of Isabelle? Very little is appearing in this mailing list. Am I really expected to maintain 50kloc of Isabelle code against a nightly rebuild of the development version in order to know what changes are being made?

This should probably be commented on by the main Isabelle developers. Clearly there has to be a balance between progress and backwards compatibility.

Well the simple example is:

locale carrier =
  fixes X::"'a set"
  assumes nempty: "X \<noteq> {}"

...

interpretation prod_carrier: carrier ["A \<times> B"]

This all makes sense to me, but my question now would be in what context lemmas about the product are going to be used. Or are you just interested in having a library of those lemmas?

Actually, it occurs to me now that there is a third way, but it really twists the locale framework in my opinion.

Your observation that interpretations in locales are meant to express conditional interpretations is correct. A natural representation of your example would be along the following lines:

Define a context for products:

locale carrier2 =
  fixes A and B
  assumes "A~={}" and "B~={}"

Map theorems from carrier into this context:

interpretation carrier2 < carrier "A <*> B"

Unfortunately, this is not currently possible. You may, as you observe, use defines to replace the substitution and say:

locale carrier2 =
  fixes A and B and P
  assumes "A~={}" and "B~={}"
  defines "X == A <*> B"
interpretation carrier2 < carrier X

BTW Does anyone know why my original posts are not appearing in the list, but the replies are?

Well, this one wasn't posted to Isabelle Users.

Clemens






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