[isabelle] Replacing COMP



Dear all,

I've used COMP so far in the following manner:


lemma lift_foo:
   assumes "asm ==> concl"
   shows   "asm ==> concl'"
proof - ... qed

lemmas foo1_impl = foo1[COMP lift_foo]
lemmas foo2_impl = foo2[COMP lift_foo]
lemmas foo3_impl = foo3[COMP lift_foo]
...

Now I'm porting to Isabelle2013, where COMP has been removed.

Unfortunately, THEN is no sufficient replacement as the resulting
foo_impl has a remaining "asm ==> asm" in the premises, which is ugly.

Is there some nice way of replacing the use of COMP here? Spelling out
the whole proofs (i.e. proving "asm ==> concl'" directly, for each
concl') is no real option here, as concl and concl' are usually quite
large properties which I do not intend to duplicate (maintainability and
such...)

Thanks a lot,
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.