[isabelle] datatype fails in unnamed contexts with assumptions



Dear BNF developers,

I noticed that the datatype does not work inside unnamed contexts which make assumptions. Here's a minimal example:

  context assumes "True" begin
  datatype f = F
  end

The error message varies with the form of the assumptions. In the above example, it is

  exception THM 0 raised (line 111 of "~~/src/Tools/induct.ML"):
  No variables in major premise of rule
  âTrue; ây. â?x = ??.Scratch.f.Abs_f_IITN_f y; y â UNIVâ â ?Pâ â ?P

Is this not supported at all (I have not found it listed in the limitations section of the datatype tutorial) or just an implementation insufficiency?

Some background on my usecase: I want to define a datatype which I just need to reduce a complex problem to a simpler one (a typical "without loss of generality" step), so I'd want to hide the datatype using "private" (once this will work properly). However, the theorem already lives in an unnamed context with assumptions, so I cannot easily move the datatype out of the context with assumptions.

Best,
Andreas




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