Re: [isabelle] question about locales and locale parameters

On Thu, Apr 15, 2010 at 7:14 AM, Viorel Preoteasa
<viorel.preoteasa at> wrote:
> I have figured out that avoiding unfolding "test.label none" to "test.label
> (f x)", would let me
> progress with the prof. However, as I already mentioned, this is not a good
> option in my case because this problem occurs in a context where the goal
> has many
> components, and auto solves all except the one from this example. It would
> be much
> easier for me to use the global rule instead of splitting the goal little by
> little and make
> sure the unfolding "test.label none" to "test.label (f x)" does not occur.

The workaround using congruence rules that I mentioned before will do
just that: It will prevent simp or auto from rewriting "test.label
none" to "test.label (f x)".

Here's the rule you would want to use in your case (note that there is
no assumption corresponding to subterm "n"):

lemma label_cong [cong]: "f = g ==> xs = ys ==> test.label n f xs =
test.label n g ys"
by simp

By placing this lemma (with its [cong] attribute) before your other
proofs, "test.label none" should never have its argument rewritten by
the simplifier.

Hope this helps,
- Brian

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