Email Gateway (Aug 18 2022 at 10:41): Email Gateway (Aug 18 2022 at 10:41):From: Tobias Nipkow <nipkow@in.tum.de>
Although I don't understand exactly how you are trying to speed things
up, it sounds like you have to write a tactic at the ML level to do
this. Sometimes it is possible to phrase the kind of "reuse" you seem to
be after in a rule:
P ==> (P ==> Q) ==> P & Q
But I'm not sure this helps you.
Tobias
Dominik Luecke schrieb:
Email Gateway (Aug 18 2022 at 10:41):From: Jeremy Dawson <Jeremy.Dawson@rsise.anu.edu.au>
Dominik Luecke wrote:
Dear Dominik,
Do you mean there are 23000 subgoals? Wow!
On the subject of speeding things up:
(1) Does (erule disjE) need to be applied lots of times?
If so, note that using the ML interface, the difference between
REPEAT (etac disjE 1) and
REPEAT_DETERM (etac disjE 1) can be significant.
I don't know whether you can do these in Isar.
(2) If you're applying simp 23000 times, then this is a place to look
for speedups. (simp is a highly "compound" tactic, unlike etac). Find
out exactly which rewrite rules are applied, and use them specifically
(using unfold, not simp).
If you need to use simp, consider whether you can avoid using or
simplifying assumptions (ie, use no_asm).
(3) Where the proofs of many sub-goals look quite similar try to create
a single theorem encapsulating the proof, (call it my_thm)
and try something like TRYALL (eatac n my_thm)
This avoids trying multiple proof steps multiple times
So far as I'm aware you can't do this in Isar
Regards,
Jeremy Dawson
Email Gateway (Aug 18 2022 at 10:41):From: Lawrence Paulson <lp15@cam.ac.uk>
This sort of case-splitting easily gives rise to huge numbers of
goals, but this is best done internally. I assume you have already
tried auto and force on them?
Larry Paulson
Email Gateway (Aug 18 2022 at 10:41):From: Dominik Luecke <luecke@informatik.uni-bremen.de>
Hello,
first of all... Thanks for all the answers.
I did try that, but after several hours of no real life-sign of Isabelle
I got bored and stopped the process. I thought that it might be an idea,
to somehow break down the stuff to smaller steps, so that you can at
least see if anything is really happening, or if Isabelle is just doing
something stupid for hours. The main problem is that the proof goal is
very, very big (already considered in the number of involved
(in)-equations.
I have added a sample goal of the proof to this mail, to make the
description of this Isabelle problem less abstract.
Regards,
Dominik
DRA_1_goal.txt
Email Gateway (Aug 18 2022 at 10:42):From: Paul Graunke <paul.graunke@galois.com>
I've also had issues with large terms, say a list of nats, and just
performing a
single call to subst, let alone simp. I would guess that using
unification for
the P in the conclusion of ssubst, checking equality of terms (like the two
instances of P in the premise of ssubst), and implementing beta reduction
via explicit substitution all contribute. I'm only guessing though.
Regards,
Paul
Dominik Luecke wrote:
Email Gateway (Aug 18 2022 at 10:48):From: Dominik Luecke <luecke@informatik.uni-bremen.de>
Hello,
I am currently trying to prove a theorems that involve lots of case
splits in the proof process. I mean the single sub-goals a solvable by
apply (erule disjE)+
apply (simp)
apply (simp)
where each application of this little sequence of commands takes between
1 and 30 secs. I am currently wondering if it is possible to speed up
the process of proving the single goals by remembering the successful
tactic of the previous step and all automatically added theorems of it.
Especially since the proofs of many sub-goals look quite similar. Any
speedup would help, especially since there are goals that need to be
split up into about 23k cases to solve them.
Regards,
Dominik
Last updated: May 03 2024 at 12:27 UTC