[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

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:
### 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.


Regards,
 Peter






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