Re: [isabelle] question about locales and locale parameters



On Thu, Apr 15, 2010 at 7:14 AM, Viorel Preoteasa
<viorel.preoteasa at abo.fi> 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)".

https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2008-June/msg00089.html

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.