Email Gateway (Aug 19 2022 at 16:47): Email Gateway (Aug 19 2022 at 16:47):From: Makarius <makarius@sketis.net>
Drule.multi_resolves is not relevant here, it is merely a wrapper for
Thm.biresolution, i.e. the main rule composition principle of
Isabelle/Pure.
The key difference of the structured form
then have "∃m. P m" by (rule exI)
compared to the other ones above is the order of higher-order unification
attempts. The 'then' means that some fact is unified with the premise of
exI, which is the worst-case situation ?P ?x and thus can go amiss.
Only in the second stage, the closed conclusion ∃. P m contributes more
specific unification constraints.
This problem has been there in Isar proofs since 1998/1999, and until
today I don't know a better way. The HO-unification code of Isabelle is
ultimately a mystery to me.
Makarius
http://stop-ttip.org 1,070,319 people so far
Email Gateway (Aug 19 2022 at 16:51):From: Lars Noschinski <noschinl@in.tum.de>
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
Last updated: Nov 21 2024 at 12:39 UTC