Re: [isabelle] "show" taking very long with goals with many hypothesis


Am Dienstag, den 11.06.2013, 14:17 +0200 schrieb Andreas Lochbihler:
> Isabelle tries to unify the shown goal with the subgoals in the order of the goal state.
> So, if you prove the goals in the order in which they occur in the goal state, there 
> should not be any false unification attempts. That is, at "case (DApplicationInd ...)", 
> this case really should be the first subgoal. If you skip some cases, e.g., because they 
> can be solved in the final qed(...), then there might be such unnecessary unification 
> attempts. 

this does not seem to be the problem here, as I do prove the subgoals in
the order they occur: Even if I discharge all other cases before, the
show takes long. So I still believe it is a problem with the large(?)
number of variables and similar assumptions.

Sorry for not providing a minimal example, but the real code is, for
example, here:
(Lemma reds_fresh', case DApplication, first "thus").


Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter

Attachment: signature.asc
Description: This is a digitally signed message part

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