[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.