Email Gateway (Aug 18 2022 at 11:59): Email Gateway (Aug 18 2022 at 11:59):From: Peter Lammich <peter.lammich@uni-muenster.de>
And more problems with the new set definition:
I have a lemma that is as follows, for S:: "'a => 'b set"
lemma mp_antimonoD: "\<lbrakk>mp_antimono S;
mc\<subseteq>mc'\<rbrakk> \<Longrightarrow> S mc \<supseteq> S mc'" by
(unfold mp_antimono_def) blast
at some point in a scripted proof (where I definitely DO NOT want to
start an Isar-proof), I have the subgoal
"[| mp_antimono S; mc<=mc'; (qs, qsh, csh) : S mc'; ... |] ==>
(qs,qsh,csh) : S mc"
I usually would say: by (blast intro: set_rev_mp[OF _ mp_antimonoD])
In Isabelle2007, this instantly terminates.
In Isabelle2008, this also terminates, but, depending on the other facts
around, after several second of spitting some strange output to the
trace buffer, many thousands of lines of
Enter MATCH
\<lambda>mc mc' a aa b qs qsh csh qs' cs' c d. d =?= \<lambda>mc mc' a
aa b qs qsh csh qs' cs'. ?S146 mc mc' a aa b qs qsh csh qs' cs'
(\<lambda>a. a)
(auto intro: set_rev_mp[OF _ mp_antimonoD]) gives manies of:
and also needs very long to terminate.
What is going wrong there, and how can I get back my short proof scripts
? In the 2007-version, auto and blast were even able to use the facts
derived from mp_antimonoD as input for other introduction rules, thus
doing really many work with one auto-step.
Regards,
Peter
Last updated: Nov 21 2024 at 12:39 UTC