Re: [isabelle] question about locales and locale parameters



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;

lemma label_cong [cong]: "f = g ==> xs = ys ==> test.label n f xs = test.label n g ys"
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







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