*To*: <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Problem with obtaining induction premises*From*: "Vaidas Gasiunas" <gasiunas at informatik.tu-darmstadt.de>*Date*: Tue, 19 Sep 2006 16:52:35 +0200*References*: <63235.172.179.1.159.1158405517.squirrel@www.st.informatik.tu-darmstadt.de> <Pine.LNX.4.63.0609181216390.32591@atbroy65.informatik.tu-muenchen.de> <007401c6db31$b7a6f310$24a55382@st.informatik.tudarmstadt.de> <Pine.LNX.4.63.0609191349150.7427@atbroy100.informatik.tu-muenchen.de>

Indeed, when I write from Cons.hyps have "!!(ys::'a list). [| length zs = length ys; a \<in> set zs |] ==> !y. lookupEq zs ys a = Some y" . then it works. Now I will know how to deal with such cases. Thanks, Vaidas ----- Original Message ----- From: "Makarius" <makarius at sketis.net> To: "Vaidas Gasiunas" <gasiunas at informatik.tu-darmstadt.de> Cc: <isabelle-users at cl.cam.ac.uk> Sent: Tuesday, September 19, 2006 2:05 PM Subject: Re: [isabelle] Problem with obtaining induction premises > On Mon, 18 Sep 2006, Vaidas Gasiunas wrote: > >> I have tried following in my example: >> >> from Cons.hyps have "!!ys. [| length zs = length ys; a \<in> set zs >> |] >> ==> !y. lookupEq zs ys a = Some y" . >> >> It does not work, "by auto" does not help here either. > > You also need a type constraints "!!ys :: 'a list. ..." here. > Otherwise > this closed formula will be syntactically unrelated to the context of > the > problem. > > >> At the end I proved the lemma without explicifying the hypothesis, >> just >> by referring to the fact Cons.hyps by its name. > > This is a good strategy. It is usually easier (and more informative) > to > derive immediate conclusions from the induction hypotheses, rather > than > duplicate them literally. > > >> But I am still curious why "." or "apply" cannot deal with such >> seemingly trivial step. > > Note that 'apply' merely applies a proof method. The "." abbreviates > ``by > this'', which can be expanded to ``apply this .'' The latter allows > more > fine-grained debugging. > > The single step methods (notably "this" and "rule") insist on being > able > to apply all chained facts, without ignoring anything. Thus providing > excessive facts makes the method invocation fail. > > This principle is important to achive some degree of robustness and > predictability of structured proof checking. In contrast, automated > methods readily ignore irrelevant facts. So it is easy to write > proofs > that tell the wrong story, e.g. like this: > > assume a: A > assume b: B > > from a and b have C by auto > > Here the ``auto'' step can ignore either a or b, or even worse ignore > both > and use different facts declared in the context. The relevance of > facts > is a fundamental problem in most automated proof tools. > > >> If I write >> >> have "[| length zs = length ys; a \<in> set zs |] ==> !y. lookupEq zs >> ys >> a = Some y" . >> >> then it works, but >> >> have "!!ys. [| length zs = length ys; a \<in> set zs |] ==> !y. >> lookupEq >> zs ys a = Some y" . >> >> does not work. But the latter is the hypothesis, which I see in the >> context. > > This is again a problem with unexpectedly general types. The first > form > refers to the fixed variable ys of the context, i.e. gets the expected > type. The second is detached due to !! closure and gets a fresh type. > > > Makarius

**References**:**[isabelle] Problem with obtaining induction premises***From:*Vaidas Gasiunas

**Re: [isabelle] Problem with obtaining induction premises***From:*Makarius

**Re: [isabelle] Problem with obtaining induction premises***From:*Vaidas Gasiunas

**Re: [isabelle] Problem with obtaining induction premises***From:*Makarius

- Previous by Date: [isabelle] Sequence case
- Next by Date: [isabelle] Simplifier questions
- Previous by Thread: Re: [isabelle] Problem with obtaining induction premises
- Next by Thread: [isabelle] nat properties
- Cl-isabelle-users September 2006 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