# Re: [isabelle] A proof for existential

On Thu, 2010-08-05 at 13:21 +0000, munddr at gmail.com wrote:
> Thanks. Just curious, without using metis, what would a manual proof
> look like?
There's usually not much value in writing a manual proof when metis can
solve the goal. Anyway, I've attached both an apply-style proof, and an
Isar-style proof.
I recommend the Isabelle/HOL tutorial and Tobias Nipkow's "Tutorial
Introduction to Structured Isar Proofs" (both available from
http://isabelle.in.tum.de/documentation.html) for further reading.
Regards,
Tjark

theory John imports Complex_Main
begin
axiomatization
f :: "real => real" and
g :: "real => real" and
h :: "real => real" where
ax1: "EX x. ALL y. x ~= y --> h x > h y" and
ax2: "ALL x. (ALL y. x ~= y --> h x > h y) --> g x = 0"
lemma "EX x. g x = 0"
by (metis ax1 ax2)
lemma "EX x. g x = 0"
apply (insert ax1)
apply (erule exE)
apply (rule_tac x="x" in exI)
apply (erule_tac ax2[THEN spec, THEN mp])
done
lemma "EX x. g x = 0"
proof -
from ax1 obtain x where A: "ALL y. x ~= y --> h y < h x" ..
from ax2 have "(ALL y. x ~= y --> h x > h y) --> g x = 0" ..
hence "g x = 0" using A ..
thus "EX x. g x = 0" ..
qed
end

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