Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] datatype fails in unnamed contexts with assump...

view this post on Zulip Email Gateway (Aug 22 2022 at 11:52):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
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
Broken_Typedef.thy
signature.asc

view this post on Zulip Email Gateway (Aug 22 2022 at 11:54):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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

view this post on Zulip Email Gateway (Aug 22 2022 at 11:56):

From: Dmitriy Traytel <traytel@inf.ethz.ch>
Hi Andreas,

note that this is a limitation of typedef already:

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

Dmitriy

view this post on Zulip Email Gateway (Aug 22 2022 at 11:58):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Dmitriy,

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

Andreas

Last updated: Apr 24 2024 at 08:20 UTC