*To*: Viorel Preoteasa <viorel.preoteasa at abo.fi>*Subject*: Re: [isabelle] question about locales and locale parameters*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Fri, 16 Apr 2010 06:36:32 -0700*Cc*: isabelle-users at cl.cam.ac.uk, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*In-reply-to*: <4BC71F62.5080302@abo.fi>*References*: <4BC4C03F.9060001@abo.fi> <4BC5B709.1030009@informatik.tu-muenchen.de> <4BC71F62.5080302@abo.fi>*Sender*: huffman.brian.c at gmail.com

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

**Follow-Ups**:**Re: [isabelle] question about locales and locale parameters***From:*Viorel Preoteasa

**References**:**[isabelle] question about locales and locale parameters***From:*Viorel Preoteasa

**Re: [isabelle] question about locales and locale parameters***From:*Florian Haftmann

**Re: [isabelle] question about locales and locale parameters***From:*Viorel Preoteasa

- Previous by Date: Re: [isabelle] Extracting assumptions from an Isar proof
- Next by Date: Re: [isabelle] should this use of the datatype package produce an error?
- Previous by Thread: Re: [isabelle] question about locales and locale parameters
- Next by Thread: Re: [isabelle] question about locales and locale parameters
- Cl-isabelle-users April 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list