[isabelle] Interpretation problems of locales with datatype declarations



Dear BNF experts,

I have started to use datatype declarations inside locales, but this seems to cause problems at interpretations. Here is an example:

  locale l = fixes n :: nat begin
  datatype 'a foo = Foo 'a
  end
  interpretation l 0 .

The interpretation raises

  exception THM 0 raised (line 1216 of "thm.ML"):
  Type not of sort term_of
  term_of_class.term_of ?x â ?t


If the interpretation is inside a proof (rather than at the top-level), interpret works once, but I get a different error upon the second interpretation:

  locale l2 = fixes b :: bool begin
  datatype 'b bar = Bar | Foobar 'b
  lemma True
  proof -
    interpret t!: l2 True .
  oops
  end

Here, interpret complains that
  Monotocity rule for type "Scratch.l2.bar" is already_defined.

Is this a fundamental problem of the BNF package and locales or just a limitation of the current implementation? Can I disable some plugins to make the examples work?

Best,
Andreas




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