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



Hi Joachim,

I think you are right that unification is the bottle neck. In your minimal example, you can speed things up by using a different order of the assumptions. If "bar ..." comes first, show is instantaneous. This might also work your application with Nominal2, but you either have to adjust the induction rule (such that the freshness constraints come at the end) or use the manual "fix-assume-show" style instead of "case".

Andreas

On 12/06/13 08:33, Joachim Breitner wrote:
Hi,

Am Dienstag, den 11.06.2013, 15:02 +0200 schrieb Joachim Breitner:
Sorry for not providing a minimal example

here is one:

theory Scratch imports Main begin

consts foo :: "nat => bool"
consts bar :: "nat => nat => nat => nat => nat => nat => nat => nat => bool"
consts A :: bool
consts B :: bool

lemma ind_rule[case_names CaseName]: "(⋀a b c d e f g h .
   foo a ⟹
   foo b ⟹
   foo c ⟹
   foo d ⟹
   foo e ⟹
   foo f ⟹
   foo g ⟹
   foo h ⟹
   bar a b c d e f g h ⟹
   A) ⟹ B" sorry

lemma B
proof (induction rule: ind_rule)
case (CaseName a b c d e f g h)
   show A (* This takes very long *)
   apply (rule ccontr)
   sorry (* This also *)
qed

end

Adding another parameter makes it take longer than I’d like to wait,
while after removing a parameter, things are fast enough so that I
woudn’t bother.

Greetings,
Joachim





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