Re: [isabelle] proving a class instantiation.



On Tue, Nov 9, 2010 at 6:02 AM, Makarius <makarius at sketis.net> wrote:
> On Tue, 9 Nov 2010, Brian Huffman wrote:
>> because using 'show' with meta-implications is useful sometimes
>
> Can you give an example for that?  I.e. where show "!!x. A x ==> B x"
> is needed as such

I've used the show "!!x. A x ==> B x" pattern most often in class
instance or locale interpretation proofs, where I have several goals,
and maybe one or two of them have fixes or assumptions. Often I need
to prove a few facts (using have "...") that will be used in multiple
places.

instance
proof
  have lemma1: "..."
  show "... first class assumption ..."
    by (... lemma1 ...)
  show "!!x. A x ==> ... second class assumption ..."
    by (... lemma1 ...)
  show "!!x. B x ==> ... third class assumption ..."
    by (... lemma1 ...)
qed

I can't use "next", since that erases all of my local facts along with
the local assumptions:

instance
proof
  have lemma1: "..."
  show "... first class assumption ..."
    by (... lemma1 ...)
next
  fix x assume "A x" thus "... second class assumption ..."
    by (... lemma1 ...)
(* error: lemma1 is no longer in scope! *)

The only alternative that I knew about before now was to add another
level of nesting, and restate the goal again. For large locale
interpretations this is quite verbose, compared to the original
solution. (Recall that show ?thesis doesn't work for locale
interpretations!)

instance
proof -
  have lemma1: "..."
  show "OFCLASS('a, foo_class)"
  proof
    show "... first class assumption ..."
      by (... lemma1 ...)
  next
    fix x assume "A x" thus "... second class assumption ..."
      by (... lemma1 ...)
  next
    fix x assume "B x" thus "... third class assumption ..."
      by (... lemma1 ...)
  qed
qed

> instead of something that is equivalent to
> { fix x assume "A x" then show "B x" ... } ?

Until now I didn't know that using 'show' inside a proof block { .. }
would even work to discharge a goal. Where is this documented? In the
Isar tutorial, proof blocks are only ever used with 'have'.

Indeed, it seems like this would work well in the situation I
described, and it is only a bit more verbose than the show "!!x. A x
==> B x" approach.

Even though it seems that show "!!x. A x ==> B x" is never strictly
necessary, I think that the handling of it should be changed: It
should have exactly the same effect on the goal state as {fix x assume
"A x" thus "B x" }, which is what most users expect. The only other
design choice that makes sense to me is to have show "!!x. A x ==> B
x" cause an error message. The current behavior is just weird.

- Brian





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