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


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


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.


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.