[isabelle] 2007->2008 conversion problems: Introduction rules for set membership
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
\<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'
(auto intro: set_rev_mp[OF _ mp_antimonoD]) gives manies of:
### Unification bound exceeded
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and