Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] The "inductive" command loops

view this post on Zulip Email Gateway (Aug 19 2022 at 17:11):

From: Joachim Breitner <breitner@kit.edu>
Hi,

the declaration

inductive foo :: "int ⇒ bool" where "P x ⟹ foo x" -- "note the free P!"

makes the system loop during "Proving the simplification rules ...".
Such an inductive predicate is probably not very useful, but it maybe it
is still possible to make "inductive" a mit more robust in this respect?

Thanks,
Joachim
signature.asc

view this post on Zulip Email Gateway (Aug 19 2022 at 17:13):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Joachmim,

thanks for your report. According to your description, the computation
of the inductive.simps seems to be faulty. Is anybody out there who can
investigate this?

All the best,
Florian
signature.asc

Last updated: Apr 25 2024 at 12:23 UTC