Email Gateway (Aug 23 2022 at 08:23): Email Gateway (Aug 23 2022 at 08:23):From: Li Yongjian <lyj238@gmail.com>
Dear expert:
Given a finite set S which has an element s, I want to prove that s \in S.
Obviously, it is correct. But the speed is very slow when S has containing
more than 100 elelemnts.
Are there are tactics which have quicker speed than simp tactic?
See attachment n_germanQuest.thy.
Lines lines 940—973.
from a4 have tmp0:"(inv_239 0) \<in> (set invariantsAbs)" by( simp
del:inv_239_def)
then have tmp:"formEval (inv_239 0) s"
by (force simp del:inv_239_def)
with b0 a1 have c0:"formEval (conclude (inv_239 0)) s" by
auto
from a4 have tmp:"formEval (inv_239 1) s"
by (force simp del:inv_239_def) .
regards
yongjian Li
paraTheory.thy
n_german_baseQues.thy
Last updated: Apr 24 2024 at 04:17 UTC