Re: [isabelle] Replacing COMP



Am 29.07.2013 22:39, schrieb Makarius:
> On Mon, 29 Jul 2013, René Neumann wrote:
> 
>> Now I'm porting to Isabelle2013, where COMP has been removed.
> 
> In such situations, the NEWS file is the first place to look.  It says:

I had a look there. That's how I noted it was gone ...

> * Discontinued obsolete attribute "COMP".  Potential INCOMPATIBILITY,
> use regular rule composition via "OF" / "THEN", 

Can't make it work (that's why I asked here on the list).

> or explicit proof structure instead. 

Don't want it that way.

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

I don't know Isabelle/ML in a way to make it work.

>> Unfortunately, THEN is no sufficient replacement as the resulting
>> foo_impl has a remaining "asm ==> asm" in the premises, which is ugly.
> 
> The usual game is to write statements and proofs in a way that one does
> not have to disobey the nice structure of rules provided by Larry
> Paulson in 1989. There are many ways to do that, but from the given
> example it is hard to guess what is right.

Could you, nevertheless, provide some pointers here, please? Because
currently, I'm unsure how I'd have to refine my example to make my
intention more visible.

- 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




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