Re: [isabelle] Replacing COMP



Dear René,

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

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

lemmas foo1_impl = foo1[THEN lift_foo]


2. Note that "asm" as a premise in the assumes is redundant in lift_foo. The following lemma is equivalent:

  lift_foo': "[| concl; asm |] ==> concl"

If you now do rule composition with THEN, you get "[| asm; asm |] ==> concl'"
instead of "[| asm ==> asm; asm |] ==> concl'". I don't know if that's better.
If you can prove "concl ==> concl'" without the assumption asm, then that works perfectly.


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.

context assumes asm begin

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

lemma foo1: "concl"

lemmas foo1_impl = foo1[THEN lift_foo]

end


4. The hack: You can use unfold with an appropriate lemma to get rid of the "asm ==> asm" premise as follows:

lemma remove_trivial_assumption: "((PROP A ==> PROP A) ==> PROP B) == PROP B"
  by(rule equal_intr_rule)
lemmas foo1_impl = foo1[THEN lift_foo, unfolded remove_trivial_assumption]

lemma remove_double_assumption: "(PROP A ==> PROP A ==> PROP B) == (PROP A ==> PROP B)"
  by(rule equal_intr_rule)
lemmas foo1_impl = foo[THEN lift_foo', unfolded remove_double_assumption]

Hope this helps,
Andreas

On 29/07/13 22:51, René Neumann wrote:
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é





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