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

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.


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

Attachment: Broken_Typedef.thy
Description: application/extension-thy

Attachment: signature.asc
Description: OpenPGP digital signature

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