Re: [isabelle] Extensive case splits

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.


Dominik Luecke schrieb:

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.

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