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



Hi,

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:
http://afp.sourceforge.net/browser_info/current/HOL/HOLCF/Nominal2/Launchbury/LaunchburyStacked.html
(Lemma reds_fresh', case DApplication, first "thus").

Greetings,
Joachim

-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner

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



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