Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] [symmetric]-attribute changes variable names


view this post on Zulip 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

view this post on Zulip 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: Mar 29 2024 at 08:18 UTC