Email Gateway (Aug 22 2022 at 10:20): Email Gateway (Aug 22 2022 at 10:20):From: Lars Noschinski <noschinl@in.tum.de>
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"
begin
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*)
sorry
end
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.
Last updated: Nov 21 2024 at 12:39 UTC