Email Gateway (Aug 17 2022 at 13:27): Email Gateway (Aug 17 2022 at 13:27):From: Jeremy Dawson <Jeremy.Dawson@rsise.anu.edu.au>
There seems to be a bug in the processing of inductive definitions in
Isabelle2005
bug = Main +
consts
evens :: "nat set"
inductive "evens"
intrs
evens_0 "0 : evens"
evens_next "n : id evens ==> Suc (Suc n) : evens"
monos id_mono
end
Jeremy
Email Gateway (Aug 17 2022 at 13:28):From: Stefan Berghofer <berghofe@in.tum.de>
Jeremy Dawson wrote:
This problem only affects old theories, for which Isabelle generates
ML files containing the theory extension commands. It seems that
the ML interface of the inductive definition package has been changed,
but the generator for the theory extension code has not been adapted
to these changes. To fix the problem, you have to make the following
modification in the file HOL/thy_syntax.ML:
In function
fun inductive_decl coind =
let
...
fun mk_params ((recs, ipairs), monos) =
let val big_rec_name = space_implode "_" (map (scan_to_id o unenclose) recs)
...
in
";\n\n\
...
\ InductivePackage.add_inductive true " ^
(if coind then "true " else "false ") ^ srec_tms ^
sintrs ^ " " ^ mk_list (no_atts monos) ^ " thy;\n\
replace the line containing (no_atts monos) by
sintrs ^ " " ^ mk_list (no_atts (map (fn s => "Name " ^ s) monos)) ^ " thy;\n\
Note that the old non-Isar theory file format will no longer be supported
in future releases of Isabelle anyway, so porting your theories to the new
format is a good alternative to the above fix.
Greetings,
Stefan
Email Gateway (Aug 17 2022 at 13:28):From: Makarius <makarius@sketis.net>
There is indeed a problem with the ML code generator for 'inductive', but
the above is an old non-Isar theory, which is not really supported any
more.
It is very easy to convert old theories to the current format; ML proof
scripts work as before with the help of use_legacy_bindings. Your theory
then looks like this (ignoring the fact that id_mono may not exist):
theory Scratch
imports Main
begin
consts
evens :: "nat set"
inductive evens
intros
evens_0: "0 : evens"
evens_next: "n : id evens ==> Suc (Suc n) : evens"
monos id_mono
ML {* use_legacy_bindings (the_context ()) *}
end
Note that the above 'bug' is no longer present in the current Isabelle
development version, because the old theory format has been discontinued
altogether.
Makarius
Lukas Stevens (Aug 24 2022 at 08:12):From: Jeremy Dawson <Jeremy.Dawson@rsise.anu.edu.au>
Stefan Berghofer wrote:
Note that the old non-Isar theory file format will no longer be supported
in future releases of Isabelle anyway, so porting your theories to the new
format is a good alternative to the above fix.Greetings,
Stefan
In converting a non_Isar theory file to Isar format,
what is the equivalent in Isar of the "rules" section of a non-Isar theory?
By the way, what has happened to the Introduction to Isabelle - it seems to have disappeared from the doc directory?
Jeremy
Last updated: May 01 2024 at 20:18 UTC