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



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.