[isabelle] Auto and set ordering -- unpredictable?



Hi,

I'm trying to prove a very simple lemma in the following simple example:

axiomatization
f :: "nat => nat" and
Set :: "nat set" and
i1 :: nat and
i2 :: nat
where
f1 : "f i1 = 1" and
f2 : "f i2 = 2" and
s1 : "Set = {i1,i2}"

lemma "{i2} = {x : {i2,i1}. fx = 2}"
using f1 f2 s1
by auto

It works and I know s1 is redundant here. Now, let's try:

lemma "{i2} = {x : {i1,i2}. fx = 2}"
using f1 f2 s1
by auto

Auto doesn't work. However, if s1 was removed, it works. So how come using the redundant fact "s1" requires the set to be ordered in a particular way? It doesn't seem intuitive.

Help will be appreciated!

Thanks
John




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