Re: [isabelle] proving a class instantiation.



There is one frequent situation where stating a goal in the wysiwyg
style (i.e. with ==>) works very well, namely inductions.

Tobias

Brian Huffman schrieb:
> 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.