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.

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]
...
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 of lift_foo.

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?


	Makarius




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