Email Gateway (Aug 22 2022 at 15:33): Email Gateway (Aug 22 2022 at 15:33):From: Mark Wassell <mpwassell@gmail.com>
Hello,
I have a set of mutually defined inductive predicates that Isabelle is
taking more than an hour to prove the monotonicity, intro, elim, simp etc
rules for.
Is it possible to get the details of what facts it is trying to prove?
Is there a flag I can set to get some tracing information? Browsing the
ML code I see that in the signature BASIC_INDUCTIVE there are some flags
that might help but I have no idea if I can set these and how it can be
done.
Is it possible to 'sorry' these proofs?
Cheers
Mark
Email Gateway (Aug 22 2022 at 15:33):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Mark,
There is no way to skip any of the proofs by using the Isar command inductive. The flags
are only accessible from the ML code.
To see whether this actually makes a difference, the easiest way to change this is to go
to the file ~~/src/HOL/Tools/inductive.ML and change the boolean flags in the function
gen_add_inductive. Then re-build HOL (e.g., by restart Isabelle/jEdit) and try again. Make
sure that you really skip the proofs by putting
declare [[quick_and_dirty]]
before the inductive definitions.
Also, as mutually inductive definitions are compiled into a single inductive definition
and then retrieved, it might be faster if you could split the mutual recursion into nested
recursion. That is, you parametrise some of the inductive predicates over the others,
define them first, prove that they preserve monotonicity, and then use them in the other
definitions. In my experience, this often leads to a cleaner design and simpler proofs.
Hope this helps
Andreas
Email Gateway (Aug 22 2022 at 15:33):From: Stefan Berghofer <berghofe@in.tum.de>
Dear Mark and Andreas,
since the inductive definition package uses Goal.prove_sorry internally to prove properties,
all proofs should be 'sorried' automatically when in quick_and_dirty mode, except for the
monotonicity property, which is always proved to avoid inconsistencies. There should be no
need to make any changes to the code. The no_elim and no_ind flags that you were probably
referring to were mainly used by the old datatype package to omit proofs of elimination or
induction rules even when not in quick_and_dirty mode.
Greetings,
Stefan
Last updated: Apr 25 2024 at 20:15 UTC