Re: [isabelle] Replacing COMP



Am 31.07.2013 14:32, schrieb Makarius:
> On Tue, 30 Jul 2013, Tobias Nipkow wrote:
> 
>> Am 29/07/2013 22:39, schrieb Makarius:
>>> Note that Isabelle/ML provides a variety of
>>> operators like COMP, INCR_COMP, COMP_INCR, which need to be applied
>>> with some care where this is really required.
>>
>> Can you give a concrete example where the use of COMP leads to
>> something the
>> Isabelle user needs to be protected from?
> 
> COMP is conceptually outside the Isabelle/Pure framework (Paulson 1989)
> and the Isabelle/Isar proof language (Wenzel 1999).  It violates certain
> assumptions about the structure of rules.
> 
> We've had a recent isabelle-users thread on COMP in May, with the
> typical situation that someone does not understand the purpose of !! and
> ==> yet, is surprised about its behaviour in rule composition, and wants
> to bypass it without understanding the consequences.
> 
> Before everything is repeated, see especially this explanation by Larry:
> https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2013-May/msg00016.html

I'm with Tobias (as he stated in the thread you mentioned) to have an OF
and/or THEN variant which allows to instantiate the premise without
handling ==> and !! in a special way, because it is sometimes extremely
helpful.

And COMP is this THEN variant, is it not?

Btw: Reading the implementation manual on Drule.compose. It should read
"The unique s that unifies ψ and φ_i" (i.e. φ_i and not φ), shouldn't it?

- René

-- 
René Neumann

Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München

Tel: +49-89-289-17232
Office: MI 03.11.055

Attachment: smime.p7s
Description: S/MIME Kryptografische Unterschrift



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