# [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
sgn_mult sgn_pos)

lemma (in loc3) z_zero:
shows "EX t. Z t = 0"
using z a b d2 x2

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.