*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>, Dmitriy Traytel <traytel at inf.ethz.ch>*Subject*: Re: [isabelle] datatype fails in unnamed contexts with assumptions*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Thu, 12 Nov 2015 11:25:05 +0100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <5638995A.5090408@inf.ethz.ch>*Organization*: TU Munich*References*: <56388018.8020002@inf.ethz.ch> <1FCF9E6E-8E9C-4185-828F-98F924E1AD35@inf.ethz.ch> <5638995A.5090408@inf.ethz.ch>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:38.0) Gecko/20100101 Thunderbird/38.3.0

Hi all, the dropout seems to happen in a case declaration in induct.ML. Glimpsing at the code there is some low-level analysis of the given rules, e.g.: fun left_var_prem thm = mk_var (hd (vars_of (hd (Thm.prems_of thm)))) handle List.Empty => raise THM ("No variables in major premise of rule", 0, [thm]); My naive impression is that this is just not localized, but I have not spend much time on it. Cheers, Florian Am 03.11.2015 um 12:24 schrieb Andreas Lochbihler: > 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 >>> >> > -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

**Attachment:
Broken_Typedef.thy**

**Attachment:
signature.asc**

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

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

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

- Previous by Date: Re: [isabelle] Interpretation problems of locales with datatype declarations
- Next by Date: Re: [isabelle] Failing afp-2015 build
- Previous by Thread: Re: [isabelle] datatype fails in unnamed contexts with assumptions
- Next by Thread: [isabelle] Interpretation problems of locales with datatype declarations
- 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