# [isabelle] Without using metis

Hi,
I was wondering whether the 3 lemmas (z_notzero, z_zero and lem1) in
the simple theory below can be proved without using metis. I've been
using sledgehammer to find the axioms needed to discharge the goal,
but is it regarded being too lazy? What is a better way?
Here's the theory:
theory Case
imports Real
begin
typedecl Obj
types E = real
types T = real
consts
p1 :: T
p2 :: T
locale loc1 =
fixes D :: "T => real"
and X :: "T => real"
and Z :: "T => E"
and A :: "T => E"
and B :: " T => E"
and F :: "real"
and G :: real
assumes z: "Z t = A t + B t"
and a: "A t = F*G*X t"
and b: "B t = F*D t*D t"
and cons: "Z t1 = Z t2"
and g: "G > 0"
locale loc2 = loc1 +
assumes d1: "D p1 = 0"
and x1: "X p1 > 0"
and f: "F > 0"
locale loc3 = loc1 +
assumes d2: "D p2 = 0"
and x2: "X p2 = 0"
lemma (in loc2) z_notzero:
shows "EX t. Z t ~= 0"
using z a b d1 x1 g f
by (metis add_0_left class_semiring.semiring_rules(7)
comm_monoid_add.mult_commute less_le_not_le mult_1 mult_zero_left sgn0
sgn_mult sgn_pos)
lemma (in loc3) z_zero:
shows "EX t. Z t = 0"
using z a b d2 x2
by (metis add_0_left mult_zero_right)
locale loc4 =
stuff: loc2 v h z b a m g + loc3 v' h' z' b' a' m' g'
for v h z b a m g v' h' z' b' a' m' g'
lemma (in loc4) lem1: "z ~= z'"
using z_notzero z_zero cons
by metis
end
Thanks a lot
John

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