Re: [isabelle] Why is 'auto' slow here?



Possibly because your lemma doesn't follow?

Firstly, don't use axiom unless you really know what you're doing, try use normal lemmas instead. Also, try simplify them to see where isabelle gets stuck. If we take this simpler lemma and try to prove it with simple proof steps:

lemma "∃Z⊂S. ∀x∈Z. P x ⟹ ∃Z⊂S. ∃x∈Z. P x"
apply (erule exE)
apply (rule_tac x=Z in exI)
apply (rule conjI, simp)
apply (elim conjE)

we get to this state: ⋀Z. ⟦Z ⊂ S; ∀x∈Z. P x⟧ ⟹ ∃x∈Z. P x

The only thing we can apply now is ballE or ballI, which asks that we prove the statement for some x in the set Z. Since we don't know whether Z is empty or not... well, there might not be any x existing in Z at all. Using auto can't make it so. Simplify it further and you get:

lemma "∀x∈Z. P x ⟹ ∃x∈Z. P x"
apply (case_tac "Z = {}")
 apply simp
which asks you to prove "False".

You might want to investigate the Isabelle tutorial for simpler proof methods than just blasting things with metis and auto. While powerful, automation in higher-order logic is hard and will require hand-holding eventually, like in this case.

Also, I highly recommend switching to unicode tokens / xsymbols, I don't think anyone uses the ASCII syntax much anymore, doesn't look very pretty.

Sincerely,

Rafal Kolanski.

munddr at googlemail.com wrote:
Hi,

I have the following and somehow 'auto' spends a lot of time and not doesn't terminate:

consts
f :: "real => real"
g :: "real => real"
S :: "real set"

types S = "real set"

axioms
a1: "EX Z < S. ALL x : Z. fx ~= g x"

lemma lem: "EX Z < S. EX x : Z. fx ~= g x"
using a1
apply auto

For some reason, auto doesn't terminate. Shouldn't the lemma be straightforward to prove given a1?

Thanks
John





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