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