Email Gateway (Aug 18 2022 at 10:56): Email Gateway (Aug 18 2022 at 10:56):From: Daniel Wasserrab <wasserra@infosun.fim.uni-passau.de>
Hello all,
wondering about the strange behaviour of my locale theories, I came
across the following problem:
We define the following locale with an internal inductive definition:
locale A =
fixes P :: "'a => 'b"
fixes Q :: "'c => 'a => bool"
fixes R :: "'c => 'b => bool"
assumes R_def:"R c b = (?a. Q c a & b = P a)"
begin
inductive S :: "'c => 'b => 'a list => 'b => bool"
for c :: "'c"
where S_rule1:"R c b ==> S c b [] b"
| S_rule2:"[|S c b1 as b2; Q c a; P a = b3|] ==> S c b3 (a#as) b2"
end
Furthermore we have a sublocale in which we want to use this internal
definition of S in an assumes. Thus we need the following (really
awkward) notation where we need to specify all the functions P Q R fixed
in locale A for function A.S:
locale B = A +
fixes wf :: "'a list => bool"
assumes wf_def:"A.S P Q R c b1 as b2 ==> wf as"
We now define quite dumb functions:
definition sn :: "nat => nat" where "sn n = n"
definition ve :: "nat => nat => bool" where "ve m n = True"
definition vn :: "nat => nat => bool" where "vn m n = True"
locale B still looks good:
print_locale B
Now we interpret A with the new functions:
interpretation A ["sn" "ve" "vn"] by(unfold_locales,simp add:sn_def
ve_def vn_def)
If we now try again to look at B, the following happens:
print_locale B
*** Duplicate definition of (co)inductive predicate "local.P_Q_R.S"
*** The error(s) above occurred in locale: A P Q R
*** At command "print_locale".
Has anyone any suggestion what is happening here?
Regards
Daniel
Email Gateway (Aug 18 2022 at 10:57):From: Clemens Ballarin <ballarin@in.tum.de>
Hi Daniel,
What happens here is that after the interpretation a global inductive
definition is around. This happens to have the same name
(local.P_Q_R.S) as the inductive definition added to the local
context when evaluating locale A during print_locale B.
This is a bug, presumably due to inaccurate handling of names which
leads to fauly set up of the theory/context data of the inductive
package.
For now you can get around this by adding a name prefix in the
interpretation command:
interpretation my_label: A ["sn" "ve" "vn"]
Clemens
Last updated: May 03 2024 at 04:19 UTC