*To*: Brian Huffman <brianh at cs.pdx.edu>*Subject*: Re: [isabelle] question about locales and locale parameters*From*: Viorel Preoteasa <viorel.preoteasa at abo.fi>*Date*: Mon, 19 Apr 2010 11:40:14 +0300*Cc*: isabelle-users at cl.cam.ac.uk, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*In-reply-to*: <x2ycc2478ab1004160636k24dbeceey69c4d77449ff3c52@mail.gmail.com>*References*: <4BC4C03F.9060001@abo.fi> <4BC5B709.1030009@informatik.tu-muenchen.de> <4BC71F62.5080302@abo.fi> <x2ycc2478ab1004160636k24dbeceey69c4d77449ff3c52@mail.gmail.com>*User-agent*: Thunderbird 2.0.0.24 (Windows/20100228)

Hello Brian, The trick seems to work for the test theory, but it does not work for my real theory. Also using the global simplification rule does not work for me either because I have assumptions in the locale. I have succeeded to strip down the example for which the cong approach does not work. In the third and forth lemmas the definition label is expanded to test.label and the proofs fail. Best regards, Viorel locale test = fixes none :: "'index" begin; primrec label:: "('a => 'index) => ('a list) => ('a => 'index)" where "label lbl [] = lbl" | "label lbl (y # l) = label (lbl(y := none)) l"; lemma first: "f x = none ==> f = label (f(x := i)) [x]"; by auto;

by simp lemma second: "none = f x ==> f = label (f(x := i)) [x]"; by auto; lemma third: "tl a = [] ==> f (hd a) = none ==> f = label (f(hd a := i)) a"; apply auto; sorry; lemma forth: "? y ys . a = y # ys ==> f (hd a) = none ==> f = label (f(hd a := i)) a"; apply auto; sorry; end; Brian Huffman wrote:

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:*Brian Huffman

**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

**Re: [isabelle] question about locales and locale parameters***From:*Brian Huffman

- Previous by Date: Re: [isabelle] should this use of the datatype package produce an error?
- Next by Date: [isabelle] Questions about . method
- 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