Email Gateway (Aug 18 2022 at 11:19): Email Gateway (Aug 18 2022 at 11:19):From: Andreas Lochbihler <lochbihl@infosun.fim.uni-passau.de>
I am trying to do multiple interpretations of the same locale with
different parameters, which gives me an error message at the end of the
interpretation proof.
For example, in a theory Test, suppose we have a locale with one
parameter and no assumptions which does an inductive set definition, say
locale loc =
fixes r :: "('a * 'a) set"
begin
inductive_set R :: "('a * 'a) set"
where
"(a, b) : r ==> (a, b) : R"
end
Then, I try to interpret this locale with two different (named)
instantiations for r:
interpretation i: loc["UNIV"] .
interpretation j: loc["{}"] .
At the . command of the second interpretation, Isabelle complains about
a "Clash of conversion rules for operator Test.loc.R"
Is there a way to make Isabelle accept both interpretations?
Andreas
Email Gateway (Aug 18 2022 at 11:19):From: Brian Huffman <brianh@cs.pdx.edu>
I found that the "Clash of conversion rules for operator" message
originates in HOL/Tools/inductive_set_package.ML, and it has something
to do with a theorem attribute for converting between predicates and
sets.
I can reproduce the same error message, without doing any
interpretations, by running the following commands:
declare loc.Rp_R_eq [where r=UNIV, pred_set_conv]
declare loc.Rp_R_eq [where r="{}", pred_set_conv]
Looking at the code, it seems that the error is caused by having two
pred_set_conv rules for the same predicate at the same type. If you
instantiate r to a more specific type in one or both cases, the error
goes away. Unfortunately, there doesn't seem to be a way to undeclare
the pred_set_conv attribute, so I don't see a workaround.
Apparently each locale instantiation tries to declare its own
pred_set_conv rule for R, when there really only needs to be one of
them. I think this should be considered a bug.
Quoting Andreas Lochbihler <lochbihl@infosun.fim.uni-passau.de>:
Email Gateway (Aug 18 2022 at 11:23):From: Stefan Berghofer <berghofe@in.tum.de>
Brian Huffman wrote:
Unfortunately, there doesn't seem to be a way to undeclare
the pred_set_conv attribute, so I don't see a workaround.
If your theory does not depend on R being a set, a workaround would be to
use inductive (which does not need pred_set_conv) instead of inductive_set.
Greetings,
Stefan
Last updated: Nov 21 2024 at 12:39 UTC