*To*: Dmitriy Traytel <traytel at inf.ethz.ch>*Subject*: Re: [isabelle] datatype fails in unnamed contexts with assumptions*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Tue, 3 Nov 2015 12:24:10 +0100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <1FCF9E6E-8E9C-4185-828F-98F924E1AD35@inf.ethz.ch>*References*: <56388018.8020002@inf.ethz.ch> <1FCF9E6E-8E9C-4185-828F-98F924E1AD35@inf.ethz.ch>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.3.0

Hi Dmitriy,

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 DmitriyOn 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

**Follow-Ups**:**Re: [isabelle] datatype fails in unnamed contexts with assumptions***From:*Florian Haftmann

**References**:**[isabelle] datatype fails in unnamed contexts with assumptions***From:*Andreas Lochbihler

**Re: [isabelle] datatype fails in unnamed contexts with assumptions***From:*Dmitriy Traytel

- Previous by Date: Re: [isabelle] Interpretation problems of locales with datatype declarations
- Next by Date: [isabelle] 2nd workshop on MILS: Submissions extended until 15 Nov
- Previous by Thread: Re: [isabelle] datatype fails in unnamed contexts with assumptions
- Next by Thread: Re: [isabelle] datatype fails in unnamed contexts with assumptions
- Cl-isabelle-users November 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list