*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] "show" taking very long with goals with many hypothesis*From*: Joachim Breitner <breitner at kit.edu>*Date*: Tue, 11 Jun 2013 15:02:58 +0200*In-reply-to*: <51B71563.7020607@inf.ethz.ch>*References*: <1370951829.4125.31.camel@kirk> <51B71563.7020607@inf.ethz.ch>

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**

**Follow-Ups**:**Re: [isabelle] "show" taking very long with goals with many hypothesis, MWE***From:*Joachim Breitner

**References**:**[isabelle] "show" taking very long with goals with many hypothesis***From:*Joachim Breitner

**Re: [isabelle] "show" taking very long with goals with many hypothesis***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] "show" taking very long with goals with many hypothesis
- Next by Date: Re: [isabelle] No code equations for explode on String.literal
- Previous by Thread: Re: [isabelle] "show" taking very long with goals with many hypothesis
- Next by Thread: Re: [isabelle] "show" taking very long with goals with many hypothesis, MWE
- Cl-isabelle-users June 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list