Re: [isabelle] Extensive case splits

Dominik Luecke wrote:

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.

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


Jeremy Dawson

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.