Re: [isabelle] datatype fails in unnamed contexts with assumptions



Hi Dmitriy,

Thanks for the quick reply. Now, I obviously wonder whether this is a fundamental limitation of typedef...

Andreas

On 03/11/15 11:34, Dmitriy Traytel wrote:
Hi Andreas,

note that this is a limitation of typedef already:

  context assumes "True" begin
  typedef f = "UNIV :: nat set" by auto
  end

Dmitriy

On 03 Nov 2015, at 10:36, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch> wrote:

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.