Email Gateway (Aug 02 2023 at 20:46): Email Gateway (Aug 02 2023 at 20:46):From: Dominique Unruh <cl-isabelle-users@lists.cam.ac.uk>
Dear all,
I am trying to use the rewrite method to instantiate a subterm. The
rewrite rule *sum_single *has a free parameter i (i.e., that does not
occur in the lhs), and I would like to specify what it should be
instantiated to.
The documentation (https://arxiv.org/pdf/2111.04082.pdf) claims that
there is a syntax rewrite ... sum_single where ?i=x to substitute
?i with something bound by rewrite. Unfortunately, this features
has been removed.
That is, I cannot simply write * apply (rewrite at ‹∑x∈UNIV. ⌑›
sum_single where ?i=x)*.
My best guess was that I need to recreate enough of the rhs of
sum_single to indirectly specify *i *by pattern match. I am using
apply (rewrite at ‹∑x∈UNIV. ⌑› to ‹if x∈_ then _ else _› sum_single)
Details are in the attached theory.
Unfortunately, this throws an exception Pattern. (In RC2.)
* Did I use this feature incorrectly? (Or is this a bug?)
* Is there some simpler way to instantiate i without having to
specify a pattern? (It would be a lot easier to just say something
like ?i=x as the documentation promises.)
Best wishes,
Dominique.
Email Gateway (Aug 03 2023 at 07:32):From: Peter Lammich <lammich@in.tum.de>
Hi,
you can use
apply (rewrite at ‹∑x∈UNIV. ⌑› sum_single[where ?i=x])
this yields an instantiation, however, with an ugly internal name for x.
Moreover, the unifier cannot get the extra variable x into f, yielding
the (unprovable) subgoals
1. ⋀x. finite UNIV
2. ⋀xa j. ⟦j ≠ x__; j ∈ UNIV⟧ ⟹ of_bool (xa = j) = 0
3. (∑xa∈UNIV. if x__ ∈ UNIV then of_bool (xa = x__) else 0) = 2
Note that, in subgoal 2, the unifier has inserted a new variable xa. I
don't completely understand this effect, but it's most likely that x is
not a parameter to f in the original rule.
Email Gateway (Aug 03 2023 at 09:09):From: Dominique Unruh <cl-isabelle-users@lists.cam.ac.uk>
Dear all,
I tried transforming a working example with bound variable instantiation
from Rewrite_Examples.thy into one that fails and got a different (but
probably related problem): A call to *rewrite *that succeeds but
instantiates the free variable of the rule with something that comes
from a totally unrelated part of the subgoal. The example is attached.
My best guess from the various errors is that the *rewrite *method does
the pattern match (against the *to *argument) with the wrong term.
Best wishes,
Dominique.
Email Gateway (Aug 03 2023 at 11:32):From: Dominique Unruh <cl-isabelle-users@lists.cam.ac.uk>
Hi Peter,
yes, I tried that, too. The problem is that this simply passes a rewrite
rule with a fixed Var *x *to the rewrite tactic. In contrast, the x
coming from the pattern match is a new Var that is supposed to be fresh
(i.e., distinct from accidentally same-named variables that already
exist in the context somewhere). The name x__ is, I think, purely a
printing artifact; in reality, the x passed to where stays the same,
and the x from the binder becomes mangled internally.
The paper describing the *rewrite *method (called patsubst in the
paper) addresses a specific parameter where to the rewrite method to
overcome this. I assume it has later been replaced by the to
parameter. Which is a little unfortunately because I think the to
parameter should be /in addition/ to the possibility of using where
because it is sometimes hard to emulate where using to.
Best wishes,
Dominique.
Last updated: Apr 29 2024 at 04:18 UTC