[isabelle] rule is sometimes very slow



Hi,

consider the following theory:

theory Scratch imports Main
begin

abbreviation funswapid :: "'a ⇒ 'a ⇒ 'a ⇒ 'a" (infix "⇌⇩F" 90) where
  "x ⇌⇩F y ≡ Fun.swap x y id"

notepad begin
  fix uv uw vu vw wu wv f GM HM m n a
  assume "(vw ⇌⇩F vu ∘ f HM ^^ Suc m ∘ (uw ⇌⇩F uv ∘ vw ⇌⇩F vu)) a = (f
GM ^^ Suc n) a"
  then have "∃m. (vw ⇌⇩F vu ∘ f HM ^^ Suc m ∘ (uw ⇌⇩F uv ∘ vw ⇌⇩F vu)) a
= (f GM ^^ Suc n) a"
    by (rule exI)
end

The proof step "rule exI" takes several seconds to complete on my
machine (in Isabelle 2014). Similar proofs, like

   by (rule_tac exI)
   by -  (rule exI)
   by - (erule exI)
   by metis
   by blast

are instantaneous, as expected. I looked a bit into the implementation
of rule and it seems that most time is spend
in evaluating the result of

   Drule.multi_resolves facts @{thms exI}

 -- Lars




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