Re: [isabelle] proving a class instantiation.



On Tue, 9 Nov 2010, Brian Huffman wrote:

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!)

You can use 'next' -- with plain blocks { ... } without restating a nested goal. See also section "6.1.2 Blocks" in the isar-ref manual of Isabelle2009-2.


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'.

The situation of Isabelle manuals is very complex. In general you cannot expect a tutorial to tell the full story, although the explanation of 'next' in the Isar tutorial is especially misleading, since it suggests a connection to subgoals that does not exist.

While the reference manuals that are maintained by myself are more precise, they are often harder to understand. In recent years I have started to add some examples, so this should become better. (The isar-ref manual is still lagging behind, but the implementation manual already gives many concrete standard schemes that work.)


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.

I'd say it is just a small detail that has not found its proper application yet. The behaviour is not accidental, and I was fully aware of it around 1999 when that part of Isar emerged. If I would have forced other aspects of the language like that in the past, many useful patterns would have been eliminated.

The recurrent user confusion is always of the same pattern: people think in terms of tactical goal states and suddenly find themselves in the world of structured Isar proofs, typically via class instantiation proofs. This problem can be solved by having the system react on user input in a way that immediately guides in the right direction.


	Makarius


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