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

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


> 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


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.