Re: [isabelle] Replacing COMP
On Tue, 30 Jul 2013, Andreas Lochbihler wrote:
You will have to restructure your lemmas or proofs unless you want to define
your own COMP attribute, there's no way to do it as before with THEN/OF. Here
are a few ideas.
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]
I suspect that foo1 has the form "asm ==> concl", right?
1. The clean way: Use --> instead of ==> for those parts that you want to
unify in one step, i.e.,
2. Note that "asm" as a premise in the assumes is redundant in lift_foo. The
following lemma is equivalent:
3. Hide the assumption asm in a local context to hide the asm in rule
compositions. Instead of an unnamed context, you might also want to consider
a locale which you can reopen later on.
4. The hack: You can use unfold with an appropriate lemma to get rid of the
"asm ==> asm" premise as follows:
Even after reading the answers by Andreas, I don't understand the purpose
Just technically, you can produce a compact form in the sense of (1) above
on the spot, as a variations of the tricks that were shown already:
thm lift_foo [unfolded atomize_all atomize_imp]
Can you explain the application behind all this?
This archive was generated by a fusion of
Pipermail (Mailman edition) and