Re: [isabelle] Without using metis



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