Email Gateway (Aug 19 2022 at 09:13): Email Gateway (Aug 19 2022 at 09:13):From: Peter Lammich <lammich@in.tum.de>
Hi all,
I recently stumbled over the following quite confusing behaviour:
definition "foo x \<equiv> x"
thm foo_def[symmetric]
Outputs ?y = foo ?y
Is it really necessary that symmetric is allowed to change variable
names in the theorem? For a user, it may be quite confusing having to
write
foo[where x="bar"], but foo[symmetric, where y="bar"]
-- Peter
Email Gateway (Aug 19 2022 at 09:14):From: Brian Huffman <huffman@in.tum.de>
It looks like this only happens for definitions whose right-hand side
is just a variable. Also, note that this behavior is not due to the
"symmetric" attribute per se; it really starts with Thm.biresolution.
"thm foo_def [THEN symmetric]" yields the same result.
Here's what I think is happening: When you resolve two theorems like
"rule1 [THEN rule2]", and two variable patterns are unified, the
result takes the variable name from rule2.
This seems like a sensible design for Thm.biresolution, because it is
used most often to apply rules during a proof; here rule2 corresponds
to the goal state, and rule1 is the applied rule. It makes sense to
preserve the names of schematic variables during a proof.
Last updated: Nov 21 2024 at 12:39 UTC