*To*: isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] Why does "also" fail in this proof?*From*: Robin Green <greenrd at greenrd.org>*Date*: Tue, 09 May 2006 01:54:18 +0100*In-reply-to*: <Pine.LNX.4.63.0605081406400.24159@atbroy99.informatik.tu-muenchen.de>*Organization*: Systems Research Group, University College Dublin*References*: <20060507121126.41636160@rpath2> <Pine.LNX.4.63.0605081406400.24159@atbroy99.informatik.tu-muenchen.de>

On Mon, 8 May 2006 14:13:48 +0200 (CEST) Makarius <makarius at sketis.net> wrote: > > Can someone explain why, in the attached theory file, I get this > > error on the last line: > > Because the calculational step does not make any progress -- your > first step is reflexivity. OK, with this hint I managed to fix that proof - thanks. However, I would disagree that it does not make any progress. Two strange things about this explanation: 1. Sometimes Isabelle does not object to a step which essentially just introduces a lambda - but sometimes it does (assuming your explanation above is correct). I cannot discern any rhyme or reason to this - it appears to me to be arbitrary. 2. What's worse, I find myself in a Catch 22. Given the file I posted previously, I want to prove from lemma tt_simp [simp]: "tt f g x == f x (g x)" the following: lemma doh2 [simp]: "tt f g == %x. f x (g x)" - something that should be completely trivial to prove, because it follows directly from the fact that a function is defined to be a lambda in the lambda calculus (in fact, I would expect the simp rule to do it). So let's try a one-step proof: lemma doh2 [simp]: "tt f g == %x. f x (g x)" by simp No, that fails. OK, let's try a patient, but verbose approach: lemma doh2 [simp]: "tt f g == %x. f x (g x)" proof - have "tt f g == %x. tt f g x" . also have "... == %x. f x (g x)" by simp finally show "tt f g == %x. f x (g x)" qed This yields: *** empty result sequence -- proof command failed *** At command "finally". OK, let's try a compromise: lemma doh2 [simp]: "tt f g == %x. f x (g x)" proof - have "tt f g == %x. tt f g x" . finally show "tt f g == %x. f x (g x)" by simp qed With this, Isabelle complains "No calculation yet". So the Catch 22 is: if I try to do it in 1 step, Isabelle can't seem to simplify that much in one step. If I try to do it in 3 steps, Isabelle effectively complains that I'm insulting its intelligence (going by your explanation of what the problem is, anyway). If I try to do it in 2 steps, Isabelle doesn't recognise a 2-step calculation as a calculation (even though, it clearly is such, from a human POV). I can't win! Now, the weird thing is (and here I'm going back to my point 1), Isabelle happily accepts this proof: lemma doh [simp]: "const x == %y. x" proof - have "const x == %y. const x y" . also have "... == %y. x" by (unfold const_def) finally show "const x == %y. x" . qed even though you claim, about lambda introductions like the one on the first line: "Such redundant cases are filtered out in order to achieve more robust guessing of rule instances." So why is it that my proof of doh works, but my proofs of doh2 don't? There must be something more to it that I'm not getting. > Also note that equality reasoning is usually performed at the > object-level, using "=" instead of "==". (This is in contrast to the > other connectives !! and ==>, which usually work better than ALL and > -->). OK, but I'm confused about the distinction between object-level equality and meta-equality. What advantage would that give me for these types of proofs? What disadvantages? Would currying be affected - and would my theory file get more verbose? -- Robin

**Follow-Ups**:**Re: [isabelle] Why does "also" fail in this proof?***From:*Makarius

**References**:**[isabelle] Why does "also" fail in this proof?***From:*Robin Green

**Re: [isabelle] Why does "also" fail in this proof?***From:*Makarius

- Previous by Date: Re: [isabelle] Why does "also" fail in this proof?
- Next by Date: [isabelle] Something about case rule
- Previous by Thread: Re: [isabelle] Why does "also" fail in this proof?
- Next by Thread: Re: [isabelle] Why does "also" fail in this proof?
- Cl-isabelle-users May 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