*To*: John Munroe <munddr at googlemail.com>*Subject*: Re: [isabelle] Without using metis*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Sat, 27 Mar 2010 19:05:17 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <e4d7be571003260821gbb73b75u906dcfc9caba04d4@mail.gmail.com>*References*: <e4d7be571003260821gbb73b75u906dcfc9caba04d4@mail.gmail.com>*User-agent*: Thunderbird 2.0.0.24 (Macintosh/20100228)

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

**References**:**[isabelle] Without using metis***From:*John Munroe

- Previous by Date: Re: [isabelle] Specification depends on extra type variables
- Next by Date: [isabelle] PG CVS: "error in process filter: Wrong number of arguments"
- Previous by Thread: [isabelle] Without using metis
- Next by Thread: [isabelle] PhD Studentship at De Montfort University
- Cl-isabelle-users March 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list