*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*: Mon, 18 Sep 2006 16:50:00 +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>

> Here the facts stemming from the Cons case consist of several things > simultaneously. The auto method silently ignores unused facts, while > single-step methods insist on being more thourough. This means a "." > proof has to be able to apply all given facts, which fails in the > above > application. > > You can try something like this to specify facts more precisely: > > from Cons.hyps have "..." . 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. At the end I proved the lemma without explicifying the hypothesis, just by referring to the fact Cons.hyps by its name. But I am still curious why "." or "apply" cannot deal with such seemingly trivial step. > Another option is to retrieve premises out of the blue: > > have "..." . 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. > >> I use the build of 2006 Sep 12. > > In that case you might want to read the NEWS file, which explains a > few > additions to the induction setup, including common proof patterns. In > particular, the above from/have/. invocation can be replaced by > > from `...` Thanks, this can be very useful to make the proof more readable, because now I invent a lot of fancy names to refer to the known facts. > Note that your example in Test.thy will need a type constraint of > "!!ys :: 'a list. ..." here. This may change eventually, when the > `...` > notation becomes polymorphic. I don't know, but I somehow proved it without additional type annotations. Thanks, Vaidas

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

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

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

- Previous by Date: Re: [isabelle] nat properties
- Next by Date: [isabelle] questions
- Previous by Thread: Re: [isabelle] Problem with obtaining induction premises
- Next by Thread: Re: [isabelle] Problem with obtaining induction premises
- 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