*To*: Vaidas Gasiunas <gasiunas at informatik.tu-darmstadt.de>*Subject*: Re: [isabelle] Problem with obtaining induction premises*From*: Makarius <makarius at sketis.net>*Date*: Tue, 19 Sep 2006 14:05:56 +0200 (CEST)*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <007401c6db31$b7a6f310$24a55382@st.informatik.tudarmstadt.de>*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>

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

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

**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

- Previous by Date: Re: [isabelle] questions
- Next by Date: [isabelle] Sequence case
- 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