Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Without using metis

Email Gateway (Aug 18 2022 at 14:59):

From: John Munroe <munddr@googlemail.com>
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 = FGX t"
and b: "B t = FD tD 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

Email Gateway (Aug 18 2022 at 15:00):

From: Tobias Nipkow <nipkow@in.tum.de>
John Munroe schrieb:

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?

Be thankful that Sledgehammer and metis found the proof for you and get
on with the job. At some point the lazy attitude will fail because the
proof is too complicated, at which point you need to write a real proof
yourself.

Tobias

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 = FGX t"
and b: "B t = FD tD 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

Last updated: Apr 23 2024 at 16:19 UTC