[isabelle] abbreviations and dummy patterns

Hi everyone,

I stumbled upon some interaction between abbreviations and dummy
patterns which strikes me as odd. Consider the following abbreviation:

  f n == c (%x. n + x)

Then n is a constant and independent of x. This expectation fails if
dummy patterns come into play: "f _" is expanded to

  c (%x. ?_dummy_ x + x)

which cannot be written as "f t" for any t (as the bound x was only
introduced by unfolding the abbreviation).

For the "rewrite" proof method, this is problematic. For example, the
pattern 'at "f _"' would match to many terms. On the other hand,
patterns can become (effectively) stricter then expected [1].

Now, the only solution I can see would be adding the bound variables to
dummy patterns before unfolding the abbreviations, at least for
"rewrite". However, there are probably good reasons why expanding dummy
patterns happens at the end of the check phases -- can somebody
enlighten my why this is the case?

  -- Lars

[1]: (thanks to Peter for the example):

  theory Scratch
  imports Main "~~/src/HOL/Library/Rewrite"

  abbreviation hoare_triple' 
    :: "nat â nat â (nat â nat) â bool" ("<_> _ <_>ât") 
    where "<P> c <Q>ât â undefined P c (Îx. Q x + 1)"

  notepad begin
    have "<Suc 1> 1 <Î_. 2>ât"
      (*apply (rewrite in "<â> _ <_>ât" Suc_1) * Does not work *)
      apply (rewrite in "<â> _ <?dummy>ât" Suc_1) (* Works*)

Here, the pattern in the first application is expanded to
  "undefined P c (%x. ?_dummy_ x x + 1)"

which fails to match, as "?_dummy_ x x" is not in the fragment supported by Pattern.match anymore.

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