*To*: Robin Green <greenrd at greenrd.org>*Subject*: Re: [isabelle] Why does "also" fail in this proof?*From*: Makarius <makarius at sketis.net>*Date*: Tue, 9 May 2006 13:53:15 +0200 (CEST)*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <20060509015418.5e81649f@rpath2>*References*: <20060507121126.41636160@rpath2> <Pine.LNX.4.63.0605081406400.24159@atbroy99.informatik.tu-muenchen.de> <20060509015418.5e81649f@rpath2>

On Tue, 9 May 2006, Robin Green wrote: > 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 > (in fact, I would expect the simp rule to do it). You are right. The Simplifier setup does not anything like this for other reasons (including historical ones). > 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 Try this in the body: show "%x. tt f g x == %x. f x (g x)" by simp i.e. you make the Simplifier happy by stating an expanded form. The result then fits into the pending problem due to alpha-beta-eta conversion. All single-step refinements work by higher-order unification, which includes these lambda conversions. Automated tools may have slightly different ideas. > 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." The filtering is on calculational results, not the original facts. Here you did make some progress, becase the final rhs is different from the first lhs. In the first example the latter were the same. > 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? Generally speaking, meta-level !! and ==> connectives express natural deduction rules, which can be used directly. Object-level formula need to be unpacked first, via usual intro/elim rules to reduce them to plain !! and ==>. Concerning equality, there is not much of a difference in HOL theoretically. Practically speaking = is more convenient, because most tools work directly with this form. For example, the calculational rules for = include various mixed forms (substitution etc.) while == is limited to plain transitivity. > Would currying be affected No. > and would my theory file get more verbose? Yes, if you pack everything into ALL --> etc. unnecessarily; proofs will become more complicated. But this is not what the present examples were about. Makarius

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

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

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

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